Affine pullback and invertible changes of planar coordinates

The pullback of P dx + Q dy along z ↦ A z + c transports circulation along absolutely continuous curves. Its curl scales by the signed real determinant of A, whereas planar area scales by its absolute value. The coordinate interchange has determinant -1.

def TauCeti.Green.affineMap (A : ℂ →L[ℝ] ℂ) (c z : ℂ) : ℂ

A real affine map, including singular linear parts.

Equations

• TauCeti.Green.affineMap A c z = A z + c

@[simp]

theorem TauCeti.Green.affineMap_apply (A : ℂ →L[ℝ] ℂ) (c z : ℂ) : affineMap A c z = A z + c

Evaluation of the affine coordinate map.

noncomputable def TauCeti.Green.affinePullbackP (A : ℂ →L[ℝ] ℂ) (c : ℂ) (P Q : ℂ → ℝ) (z : ℂ) : ℝ

The horizontal coefficient of the pullback of P dx + Q dy.

Equations

• TauCeti.Green.affinePullbackP A c P Q z = (TauCeti.Green.oneForm P Q (TauCeti.Green.affineMap A c z)) (A 1)

noncomputable def TauCeti.Green.affinePullbackQ (A : ℂ →L[ℝ] ℂ) (c : ℂ) (P Q : ℂ → ℝ) (z : ℂ) : ℝ

The vertical coefficient of the pullback of P dx + Q dy.

Equations

• TauCeti.Green.affinePullbackQ A c P Q z = (TauCeti.Green.oneForm P Q (TauCeti.Green.affineMap A c z)) (A Complex.I)

@[simp]

theorem TauCeti.Green.affinePullbackP_apply (A : ℂ →L[ℝ] ℂ) (c : ℂ) (P Q : ℂ → ℝ) (z : ℂ) : affinePullbackP A c P Q z = P (affineMap A c z) * (A 1).re + Q (affineMap A c z) * (A 1).im

The horizontal pullback coefficient in real coordinates.

@[simp]

theorem TauCeti.Green.affinePullbackQ_apply (A : ℂ →L[ℝ] ℂ) (c : ℂ) (P Q : ℂ → ℝ) (z : ℂ) : affinePullbackQ A c P Q z = P (affineMap A c z) * (A Complex.I).re + Q (affineMap A c z) * (A Complex.I).im

The vertical pullback coefficient in real coordinates.

theorem TauCeti.Green.oneForm_affinePullback (A : ℂ →L[ℝ] ℂ) (c : ℂ) (P Q : ℂ → ℝ) (z : ℂ) : oneForm (affinePullbackP A c P Q) (affinePullbackQ A c P Q) z = oneForm P Q (affineMap A c z) ∘SL A

The coefficient definitions give the actual pullback as a continuous linear map.

theorem TauCeti.Green.hasFDerivAt_affineMap (A : ℂ →L[ℝ] ℂ) (c z : ℂ) : HasFDerivAt (affineMap A c) A z

The affine coordinate map has constant derivative A.

theorem TauCeti.Green.curl_affinePullback (A : ℂ →L[ℝ] ℂ) (c : ℂ) {P Q : ℂ → ℝ} {z : ℂ} (hP : DifferentiableAt ℝ P (affineMap A c z)) (hQ : DifferentiableAt ℝ Q (affineMap A c z)) : curl (affinePullbackP A c P Q) (affinePullbackQ A c P Q) z = LinearMap.det ↑A * curl P Q (affineMap A c z)

Curl transforms by the signed determinant under an affine pullback. Only differentiability at the image point is needed, in particular this applies to locally real C¹ fields.

theorem TauCeti.Green.absolutelyContinuousOnInterval_affineMap (A : ℂ →L[ℝ] ℂ) (c : ℂ) {γ : ℝ → ℂ} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) : AbsolutelyContinuousOnInterval (affineMap A c ∘ γ) a b

Affine transport preserves absolute continuity without a bounded-speed assumption.

theorem TauCeti.Green.intervalIntegrable_circulationFun_affineMap_iff (A : ℂ →L[ℝ] ℂ) (c : ℂ) (P Q : ℂ → ℝ) {γ : ℝ → ℂ} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) : IntervalIntegrable (circulationFun P Q (affineMap A c ∘ γ)) MeasureTheory.volume a b ↔ IntervalIntegrable (circulationFun (affinePullbackP A c P Q) (affinePullbackQ A c P Q) γ) MeasureTheory.volume a b

Integrability of circulation is preserved by pulling back the field along affine transport.

theorem TauCeti.Green.integral_circulationFun_affineMap (A : ℂ →L[ℝ] ℂ) (c : ℂ) (P Q : ℂ → ℝ) {γ : ℝ → ℂ} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) : ∫ (t : ℝ) in a..b, circulationFun P Q (affineMap A c ∘ γ) t = ∫ (t : ℝ) in a..b, circulationFun (affinePullbackP A c P Q) (affinePullbackQ A c P Q) γ t

The actual raw circulation integrals agree under affine pullback.

theorem TauCeti.Green.map_withDensity_affineMap (A : ℂ ≃L[ℝ] ℂ) (c : ℂ) {s : Set ℂ} (hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) : MeasureTheory.Measure.map (affineMap (↑A) c) ((MeasureTheory.volume.restrict s).withDensity fun (x : ℂ) => ENNReal.ofReal |LinearMap.det ↑↑A|) = MeasureTheory.volume.restrict (affineMap (↑A) c '' s)

The area measure on an affine image is the pushforward of the absolute determinant density.

theorem TauCeti.Green.integral_affineMap_image (A : ℂ ≃L[ℝ] ℂ) (c : ℂ) {s : Set ℂ} (hs : MeasurableSet s) (f : ℂ → ℝ) : ∫ (z : ℂ) in affineMap (↑A) c '' s, f z = |LinearMap.det ↑↑A| * ∫ (z : ℂ) in s, f (affineMap (↑A) c z)

Change of variables for planar area under an invertible affine coordinate map.

theorem TauCeti.Green.volume_affineMap_image (A : ℂ ≃L[ℝ] ℂ) (c : ℂ) {s : Set ℂ} (hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) : MeasureTheory.volume (affineMap (↑A) c '' s) = ENNReal.ofReal |LinearMap.det ↑↑A| * MeasureTheory.volume s

Affine images scale planar area by the absolute real determinant.

theorem TauCeti.Green.integrableOn_affineMap_image_iff (A : ℂ ≃L[ℝ] ℂ) (c : ℂ) {s : Set ℂ} (hs : MeasurableSet s) (f : ℂ → ℝ) : MeasureTheory.IntegrableOn f (affineMap (↑A) c '' s) MeasureTheory.volume ↔ MeasureTheory.IntegrableOn (f ∘ affineMap (↑A) c) s MeasureTheory.volume

Area integrability is preserved under an invertible affine coordinate map.

theorem TauCeti.Green.integrableOn_curl_affinePullback_iff (A : ℂ ≃L[ℝ] ℂ) (c : ℂ) {s : Set ℂ} (hs : MeasurableSet s) {P Q : ℂ → ℝ} (hP : ∀ z ∈ s, DifferentiableAt ℝ P (affineMap (↑A) c z)) (hQ : ∀ z ∈ s, DifferentiableAt ℝ Q (affineMap (↑A) c z)) : MeasureTheory.IntegrableOn (curl (affinePullbackP (↑A) c P Q) (affinePullbackQ (↑A) c P Q)) s MeasureTheory.volume ↔ MeasureTheory.IntegrableOn (curl P Q) (affineMap (↑A) c '' s) MeasureTheory.volume

Integrability of curl is preserved by affine pullback for differentiable fields.

theorem TauCeti.Green.integral_curl_affinePullback (A : ℂ ≃L[ℝ] ℂ) (c : ℂ) {s : Set ℂ} (hs : MeasurableSet s) {P Q : ℂ → ℝ} (hP : ∀ z ∈ s, DifferentiableAt ℝ P (affineMap (↑A) c z)) (hQ : ∀ z ∈ s, DifferentiableAt ℝ Q (affineMap (↑A) c z)) : ∫ (z : ℂ) in s, curl (affinePullbackP (↑A) c P Q) (affinePullbackQ (↑A) c P Q) z = LinearMap.det ↑↑A / |LinearMap.det ↑↑A| * ∫ (z : ℂ) in affineMap (↑A) c '' s, curl P Q z

Curl integration transports with the orientation factor det A / |det A|. The source hypotheses hold, in particular, for fields locally real C¹ on the affine image.

theorem TauCeti.Green.oneForm_coordinateSwap (P Q : ℂ → ℝ) (z : ℂ) : oneForm P Q (Complex.coordinateSwapCLE z) ∘SL ↑Complex.coordinateSwapCLE = oneForm (Q ∘ ⇑Complex.coordinateSwapCLE) (P ∘ ⇑Complex.coordinateSwapCLE) z

Coordinate interchange exchanges the two coefficients of a pulled-back 1-form.

theorem TauCeti.Green.curl_coordinateSwap {P Q : ℂ → ℝ} {z : ℂ} (hP : DifferentiableAt ℝ P (Complex.coordinateSwapCLE z)) (hQ : DifferentiableAt ℝ Q (Complex.coordinateSwapCLE z)) : curl (Q ∘ ⇑Complex.coordinateSwapCLE) (P ∘ ⇑Complex.coordinateSwapCLE) z = -curl P Q (Complex.coordinateSwapCLE z)

Interchanging real and imaginary coordinates negates the curl.

theorem TauCeti.Green.affineMap_image_convexHull (A : ℂ →L[ℝ] ℂ) (c : ℂ) (s : Set ℂ) : affineMap A c '' (convexHull ℝ) s = (convexHull ℝ) (affineMap A c '' s)

An affine coordinate map carries convex hulls to the convex hulls of their images.

theorem TauCeti.Green.affineMap_image_interior (A : ℂ ≃L[ℝ] ℂ) (c : ℂ) (s : Set ℂ) : affineMap (↑A) c '' interior s = interior (affineMap (↑A) c '' s)

Affine coordinates commute with taking interiors.

theorem TauCeti.Green.affineMap_lineMap (A : ℂ →L[ℝ] ℂ) (c p q : ℂ) (t : ℝ) : affineMap A c ((AffineMap.lineMap p q) t) = (AffineMap.lineMap (affineMap A c p) (affineMap A c q)) t

Affine transport commutes with parameterization of straight segments.

theorem TauCeti.Green.curveIntegrable_segment_affineMap_iff (A : ℂ →L[ℝ] ℂ) (c p q : ℂ) (P Q : ℂ → ℝ) : CurveIntegrable (oneForm P Q) (Path.segment (affineMap A c p) (affineMap A c q)) ↔ CurveIntegrable (oneForm (affinePullbackP A c P Q) (affinePullbackQ A c P Q)) (Path.segment p q)

Genuine segment integrability is preserved by affine pullback of the planar 1-form.

theorem TauCeti.Green.curveIntegral_segment_affineMap (A : ℂ →L[ℝ] ℂ) (c p q : ℂ) (P Q : ℂ → ℝ) : curveIntegral (oneForm P Q) (Path.segment (affineMap A c p) (affineMap A c q)) = curveIntegral (oneForm (affinePullbackP A c P Q) (affinePullbackQ A c P Q)) (Path.segment p q)

Actual segment circulation transports to the pulled-back planar 1-form.

theorem TauCeti.Green.contDiff_affineMap (A : ℂ →L[ℝ] ℂ) (c : ℂ) {n : WithTop ℕ∞} : ContDiff ℝ n (affineMap A c)

Affine coordinate maps are real smooth.

theorem TauCeti.Green.contDiffOn_affinePullback {n : WithTop ℕ∞} {A : ℂ →L[ℝ] ℂ} {c : ℂ} {U : Set ℂ} {P Q : ℂ → ℝ} (hP : ContDiffOn ℝ n P U) (hQ : ContDiffOn ℝ n Q U) : ContDiffOn ℝ n (affinePullbackP A c P Q) (affineMap A c ⁻¹' U) ∧ ContDiffOn ℝ n (affinePullbackQ A c P Q) (affineMap A c ⁻¹' U)

Both coefficients of an affine pullback retain regularity on the preimage domain.