Signed area of rectifiable plane curves

The signed area TauCeti.signedArea γ a b = ½ ∫ₐᵇ (x y' - y x') is computed from the derivative of the parameter, so it is the right notion only for absolutely continuous curves: a circle composed with the Cantor function is continuous, of bounded variation, and has zero derivative almost everywhere, so its derivative integral vanishes.

The geometric signed area TauCeti.rectifiableSignedArea γ a b is instead the geometric integral TauCeti.rectifiableCurveIntegral of the area form (x dy - y dx) / 2 along γ. It is computed along the natural (arclength) parameterization of γ on its length interval, and it is meaningful for every continuous plane curve of bounded variation.

Main results

• TauCeti.rectifiableSignedArea_eq_signedArea_naturalParameterization: the geometric signed area is the signed area of the natural parameterization on the length interval.
• TauCeti.rectifiableSignedArea_eq_signedArea_of_eqOn_comp_variationOnFromTo: it is the signed area of any curve through which γ factors by cumulative variation.
• AbsolutelyContinuousOnInterval.rectifiableSignedArea_eq_signedArea: agreement with TauCeti.signedArea for absolutely continuous curves.
• TauCeti.rectifiableSignedArea_eq_signedArea_of_eqOn_comp: independence of the factorization through an absolutely continuous curve and an increasing continuous map.
• TauCeti.rectifiableSignedArea_comp_of_monotoneOn, TauCeti.rectifiableSignedArea_comp_of_antitoneOn: invariance under increasing, and sign reversal under decreasing, continuous onto reparametrizations, which need not be absolutely continuous.

The isoperimetric inequality bounding the geometric signed area of a closed curve by its length is in TauCeti.Analysis.Fourier.AreaEnergy.

noncomputable def TauCeti.rectifiableSignedArea (γ : ℝ → ℂ) (a b : ℝ) : ℝ

The geometric signed area of a plane curve γ on [a, b]: the geometric integral TauCeti.rectifiableCurveIntegral of the area form (x dy - y dx) / 2 along γ, computed along the natural parameterization of γ on its length interval. For a continuous curve of bounded variation it is invariant under increasing continuous reparametrizations, and it agrees with TauCeti.signedArea for absolutely continuous curves (AbsolutelyContinuousOnInterval.rectifiableSignedArea_eq_signedArea). It is zero for a curve of infinite length on [a, b] and for b < a.

theorem TauCeti.rectifiableSignedArea_def (γ : ℝ → ℂ) (a b : ℝ) : rectifiableSignedArea γ a b = rectifiableCurveIntegral (Green.oneForm Green.Examples.areaP Green.Examples.areaQ) γ a b

The defining formula of TauCeti.rectifiableSignedArea.

theorem TauCeti.rectifiableSignedArea_eq_signedArea_naturalParameterization (γ : ℝ → ℂ) (a b : ℝ) : rectifiableSignedArea γ a b = signedArea (naturalParameterization γ (Set.Icc a b) a) 0 (eVariationOn γ (Set.Icc a b)).toReal

The geometric signed area of γ on [a, b] is the signed area of its natural parameterization on the length interval [0, L], where L is the total variation of γ on [a, b].

theorem TauCeti.rectifiableSignedArea_eq_signedArea_of_eqOn_comp_variationOnFromTo {γ : ℝ → ℂ} {a b : ℝ} (hcont : ContinuousOn γ (Set.Icc a b)) {g : ℝ → ℂ} (hg : Set.EqOn (g ∘ variationOnFromTo γ (Set.Icc a b) a) γ (Set.Icc a b)) : rectifiableSignedArea γ a b = signedArea g 0 (eVariationOn γ (Set.Icc a b)).toReal

The geometric signed area of a continuous curve is the signed area, on the length interval, of any curve g through which the curve factors by cumulative variation, such as the factor given by BoundedVariationOn.exists_arclength_factorization.

theorem TauCeti.rectifiableSignedArea_congr {γ : ℝ → ℂ} {a b : ℝ} {γ' : ℝ → ℂ} (h : Set.EqOn γ γ' (Set.Icc a b)) : rectifiableSignedArea γ a b = rectifiableSignedArea γ' a b

The geometric signed area only depends on the curve on [a, b].

theorem TauCeti.rectifiableSignedArea_of_not_boundedVariationOn {γ : ℝ → ℂ} {a b : ℝ} (h : ¬BoundedVariationOn γ (Set.Icc a b)) : rectifiableSignedArea γ a b = 0

The geometric signed area of a curve of infinite length on [a, b] is zero.

theorem TauCeti.rectifiableSignedArea_of_lt {γ : ℝ → ℂ} {a b : ℝ} (h : b < a) : rectifiableSignedArea γ a b = 0

The geometric signed area on [a, b] with b < a is zero.

@[simp]

theorem TauCeti.rectifiableSignedArea_self {γ : ℝ → ℂ} {a : ℝ} : rectifiableSignedArea γ a a = 0

The geometric signed area on a degenerate interval [a, a] is zero.

@[simp]

theorem TauCeti.rectifiableSignedArea_const (z : ℂ) (a b : ℝ) : rectifiableSignedArea (fun (x : ℝ) => z) a b = 0

A constant curve has geometric signed area zero.

theorem AbsolutelyContinuousOnInterval.rectifiableSignedArea_eq_signedArea {γ : ℝ → ℂ} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hab : a ≤ b) : TauCeti.rectifiableSignedArea γ a b = TauCeti.signedArea γ a b

Agreement with the derivative integral. For an absolutely continuous curve, the geometric signed area is the signed area ½ ∫ₐᵇ (x y' - y x') computed from the derivative of the parameter.

theorem TauCeti.rectifiableSignedArea_eq_signedArea_of_eqOn_comp {γ : ℝ → ℂ} {a b c d : ℝ} {η : ℝ → ℂ} {ψ : ℝ → ℝ} (hη : AbsolutelyContinuousOnInterval η c d) (hab : a ≤ b) (hψ : ContinuousOn ψ (Set.Icc a b)) (hψm : MonotoneOn ψ (Set.Icc a b)) (hψa : ψ a = c) (hψb : ψ b = d) (h : Set.EqOn (η ∘ ψ) γ (Set.Icc a b)) : rectifiableSignedArea γ a b = signedArea η c d

Independence of the factorization. If a curve factors on [a, b] as an absolutely continuous curve η on [c, d] composed with a continuous increasing map of [a, b] onto [c, d], then its geometric signed area is the signed area of η on [c, d].

theorem TauCeti.rectifiableSignedArea_comp_of_monotoneOn {γ : ℝ → ℂ} {a b c d : ℝ} (hcont : ContinuousOn γ (Set.Icc a b)) {φ : ℝ → ℝ} (hcd : c ≤ d) (hφ : ContinuousOn φ (Set.Icc c d)) (hφm : MonotoneOn φ (Set.Icc c d)) (hφc : φ c = a) (hφd : φ d = b) : rectifiableSignedArea (γ ∘ φ) c d = rectifiableSignedArea γ a b

The geometric signed area is invariant under increasing continuous reparametrizations of [c, d] onto [a, b]. The reparametrization need not be absolutely continuous.

theorem TauCeti.rectifiableSignedArea_comp_of_antitoneOn {γ : ℝ → ℂ} {a b c d : ℝ} (hcont : ContinuousOn γ (Set.Icc a b)) {φ : ℝ → ℝ} (hcd : c ≤ d) (hφ : ContinuousOn φ (Set.Icc c d)) (hφm : AntitoneOn φ (Set.Icc c d)) (hφc : φ c = b) (hφd : φ d = a) : rectifiableSignedArea (γ ∘ φ) c d = -rectifiableSignedArea γ a b

The geometric signed area changes sign under decreasing continuous reparametrizations of [c, d] onto [a, b]. The reparametrization need not be absolutely continuous.

@[simp]

theorem TauCeti.rectifiableSignedArea_circleMap (c : ℂ) (R θ : ℝ) : rectifiableSignedArea (circleMap c R) θ (θ + 2 * Real.pi) = Real.pi * R ^ 2

A circle of radius R, traversed once counterclockwise from any initial angle θ, has geometric signed area π R².