Affine coordinates on nondegenerate triangles

The positive real basis (1,I) gives an invertible affine coordinate map from the standard triangle to any nondegenerate ordered triangle. Its determinant is the existing triangleDet. Area uses the absolute determinant; the oriented three-segment circulation retains its sign.

noncomputable def TauCeti.Green.triangleLinearMap (c p q : ℂ) : ℂ →ₗ[ℝ] ℂ

The real linear map sending the positive basis to the two edges based at c.

Equations

• TauCeti.Green.triangleLinearMap c p q = (Complex.basisOneI.constr ℝ) ![p - c, q - c]

@[simp]

theorem TauCeti.Green.triangleLinearMap_one (c p q : ℂ) : (triangleLinearMap c p q) 1 = p - c

The first basis vector is sent to the first edge.

@[simp]

theorem TauCeti.Green.triangleLinearMap_I (c p q : ℂ) : (triangleLinearMap c p q) Complex.I = q - c

The second basis vector is sent to the second edge.

theorem TauCeti.Green.det_triangleLinearMap (c p q : ℂ) : LinearMap.det (triangleLinearMap c p q) = triangleDet c p q

The determinant of the triangle coordinate map is the existing oriented triangle determinant.

noncomputable def TauCeti.Green.triangleCoordinates (c p q : ℂ) (hdet : triangleDet c p q ≠ 0) : ℂ ≃L[ℝ] ℂ

Nonzero triangle determinant gives an invertible real continuous linear coordinate map.

Equations

• TauCeti.Green.triangleCoordinates c p q hdet = (LinearMap.equivOfIsUnitDet ⋯).toContinuousLinearEquiv

theorem TauCeti.Green.triangleCoordinates_toLinearMap (c p q : ℂ) (hdet : triangleDet c p q ≠ 0) : ↑↑(triangleCoordinates c p q hdet) = triangleLinearMap c p q

The invertible triangle coordinates have the prescribed underlying linear map.

@[simp]

theorem TauCeti.Green.triangleCoordinates_one (c p q : ℂ) (hdet : triangleDet c p q ≠ 0) : (triangleCoordinates c p q hdet) 1 = p - c

Triangle coordinates send 1 to the first edge vector.

@[simp]

theorem TauCeti.Green.triangleCoordinates_I (c p q : ℂ) (hdet : triangleDet c p q ≠ 0) : (triangleCoordinates c p q hdet) Complex.I = q - c

Triangle coordinates send I to the second edge vector.

theorem TauCeti.Green.det_triangleCoordinates (c p q : ℂ) (hdet : triangleDet c p q ≠ 0) : LinearMap.det ↑↑(triangleCoordinates c p q hdet) = triangleDet c p q

The coordinate determinant is the oriented triangle determinant.

theorem TauCeti.Green.affineMap_image_standardTriangle (c p q : ℂ) (hdet : triangleDet c p q ≠ 0) : affineMap (↑(triangleCoordinates c p q hdet)) c '' standardTriangle = (convexHull ℝ) {c, p, q}

Triangle coordinates identify the actual closed convex hulls.

theorem TauCeti.Green.affineMap_image_interior_standardTriangle (c p q : ℂ) (hdet : triangleDet c p q ≠ 0) : affineMap (↑(triangleCoordinates c p q hdet)) c '' interior standardTriangle = interior ((convexHull ℝ) {c, p, q})

The actual open triangle is the image of the standard triangle interior.

theorem TauCeti.Green.curveIntegral_triangle_affineMap (A : ℂ →L[ℝ] ℂ) (c p q r : ℂ) (P Q : ℂ → ℝ) : (Finsupp.linearCombination ℤ fun (γ : Arc) => curveIntegral (oneForm P Q) γ.snd.snd) (BoundaryChain.triangle (affineMap A c p) (affineMap A c q) (affineMap A c r)) = (Finsupp.linearCombination ℤ fun (γ : Arc) => curveIntegral (oneForm (affinePullbackP A c P Q) (affinePullbackQ A c P Q)) γ.snd.snd) (BoundaryChain.triangle p q r)

The literal three-segment triangle chain transports its actual curve-integral sum.

theorem TauCeti.Green.volume_convexHull_triangle (c p q : ℂ) : MeasureTheory.volume ((convexHull ℝ) {c, p, q}) = ENNReal.ofReal |triangleDet c p q| * MeasureTheory.volume standardTriangle

Positive planar area on an ordered triangle scales by the absolute triangle determinant.

theorem TauCeti.Green.integral_convexHull_triangle (c p q : ℂ) (hdet : triangleDet c p q ≠ 0) (f : ℂ → ℝ) : ∫ (z : ℂ) in (convexHull ℝ) {c, p, q}, f z = |triangleDet c p q| * ∫ (z : ℂ) in standardTriangle, f (affineMap (↑(triangleCoordinates c p q hdet)) c z)

Area integration on an actual triangle agrees with the affine-coordinate integral.

theorem TauCeti.Green.green_triangle_of_det_ne_zero {c p q : ℂ} (hdet : triangleDet c p q ≠ 0) {U : Set ℂ} (hU : IsOpen U) (hTU : (convexHull ℝ) {c, p, q} ⊆ U) {P Q : ℂ → ℝ} (hP : ContDiffOn ℝ 1 P U) (hQ : ContDiffOn ℝ 1 Q U) : MeasureTheory.IntegrableOn (curl P Q) ((convexHull ℝ) {c, p, q}) MeasureTheory.volume ∧ curveIntegral (oneForm P Q) (Path.segment c p) + curveIntegral (oneForm P Q) (Path.segment p q) - curveIntegral (oneForm P Q) (Path.segment c q) = triangleDet c p q / |triangleDet c p q| * ∫ (z : ℂ) in (convexHull ℝ) {c, p, q}, curl P Q z

Green's theorem on any nondegenerate ordered triangle. The sign of its orientation is triangleDet / |triangleDet|, and the area integral uses the usual positive planar volume.