Documentation

TauCeti.Analysis.Green.Examples.CurveArea.SignedArea

Signed area of a plane curve #

For a plane curve γ = x + i y : ℝ → ℂ on [a, b], its signed area is the boundary integral ½ ∫ₐᵇ (x y' - y x') (TauCeti.signedArea), the circulation of the area form (x dy - y dx) / 2 along γ (TauCeti.signedArea_eq_integral_circulationFun). For a circle traversed once counterclockwise, from any initial angle, it is the area of the disc (TauCeti.signedArea_circleMap).

The area–energy inequality bounding the signed area of a closed curve by its energy is in TauCeti.Analysis.Fourier.AreaEnergy.

Main definitions #

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

The signed area ½ ∫ₐᵇ (x y' - y x') of the plane curve γ = x + i y on [a, b], computed from its velocity deriv γ. For an absolutely continuous curve any almost-everywhere derivative may be used in place of deriv γ (TauCeti.signedArea_eq_of_ae_hasDerivAt).

Instances For
    source
    theorem TauCeti.signedArea_def (γ : ℝ → ℂ) (a b : ℝ) :
    signedArea γ a b = (∫ (t : ℝ) in a..b, (γ t).re * (deriv γ t).im - (γ t).im * (deriv γ t).re) / 2

    The defining formula of TauCeti.signedArea.

    source
    @[simp]
    theorem TauCeti.signedArea_const (c : ℂ) (a b : ℝ) :
    signedArea (fun (x : ℝ) => c) a b = 0

    A constant curve has signed area zero.

    source
    @[simp]
    theorem TauCeti.signedArea_self (γ : ℝ → ℂ) (a : ℝ) :
    signedArea γ a a = 0

    The signed area over a degenerate interval is zero.

    source
    theorem TauCeti.signedArea_symm (γ : ℝ → ℂ) (a b : ℝ) :
    signedArea γ b a = -signedArea γ a b

    Reversing the interval of integration negates the signed area.

    source
    theorem TauCeti.signedArea_eq_of_ae_hasDerivAt {a b : ℝ} {γ γ' : ℝ → ℂ} (hγ' : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → HasDerivAt γ (γ' t) t) :
    signedArea γ a b = (∫ (t : ℝ) in a..b, (γ t).re * (γ' t).im - (γ t).im * (γ' t).re) / 2

    The signed area may be computed from any almost-everywhere derivative of the curve.

    source
    theorem TauCeti.signedArea_eq_integral_circulationFun (γ : ℝ → ℂ) (a b : ℝ) :
    signedArea γ a b = ∫ (t : ℝ) in a..b, Green.circulationFun Green.Examples.areaP Green.Examples.areaQ γ t

    The signed area is the circulation along γ of the area form (x dy - y dx) / 2, whose coefficients are TauCeti.Green.Examples.areaP and TauCeti.Green.Examples.areaQ.

    source
    @[simp]
    theorem TauCeti.signedArea_circleMap (c : ℂ) (R θ : ℝ) :
    signedArea (circleMap c R) θ (θ + 2 * Real.pi) = Real.pi * R ^ 2

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