Documentation

TauCeti.Analysis.Green.Examples.CurveArea.Basic

Circular area examples #

The area form (-y dx + x dy)/2 has curl one. Its actual circulation around a radius-R circle is π R². The existing winding number makes its winding weight exactly the indicator of the open disc, including the prescribed zero value on the trace.

source
noncomputable def TauCeti.Green.Examples.areaP (z : ℂ) :
ℝ

The horizontal coefficient of the standard signed-area form.

Instances For
    source
    noncomputable def TauCeti.Green.Examples.areaQ (z : ℂ) :
    ℝ

    The vertical coefficient of the standard signed-area form.

    Instances For
      source
      @[simp]
      theorem TauCeti.Green.Examples.areaP_apply (z : ℂ) :
      areaP z = -z.im / 2

      Evaluation of the horizontal area coefficient.

      source
      @[simp]
      theorem TauCeti.Green.Examples.areaQ_apply (z : ℂ) :
      areaQ z = z.re / 2

      Evaluation of the vertical area coefficient.

      source
      theorem TauCeti.Green.Examples.contDiff_areaP {n : WithTop ℕ∞} :
      ContDiff ℝ n areaP

      The horizontal coefficient areaP of the signed-area form is smooth.

      source
      theorem TauCeti.Green.Examples.contDiff_areaQ {n : WithTop ℕ∞} :
      ContDiff ℝ n areaQ

      The vertical coefficient areaQ of the signed-area form is smooth.

      source
      theorem TauCeti.Green.Examples.continuous_oneForm_area :
      Continuous (oneForm areaP areaQ)

      The signed-area form (x dy - y dx) / 2 is a continuous field of real 1-forms.

      source
      @[simp]
      theorem TauCeti.Green.Examples.curl_area (z : ℂ) :
      curl areaP areaQ z = 1

      The signed-area form has curl one in the positive basis (1,I).

      source
      theorem TauCeti.Green.Examples.circulationFun_area_circleMap (R t : ℝ) :
      circulationFun areaP areaQ (circleMap 0 R) t = R ^ 2 / 2

      The actual signed-area circulation integrand on a centered circle is R²/2.

      source
      theorem TauCeti.Green.Examples.integral_circulationFun_area_circleMap (R : ℝ) :
      ∫ (t : ℝ) in 0..2 * Real.pi, circulationFun areaP areaQ (circleMap 0 R) t = Real.pi * R ^ 2

      Actual circulation of the signed-area form around a radius-R circle.

      source
      theorem TauCeti.Green.Examples.windingWeight_circleMap {R : ℝ} (hR : 0 < R) (z : ℂ) :
      windingWeight (circleMap 0 R) 0 (2 * Real.pi) z = (Metric.ball 0 R).indicator 1 z

      The winding weight of a positively sized circle is the indicator of its open disc.

      source
      theorem TauCeti.Green.Examples.integral_windingWeight_circleMap {R : ℝ} (hR : 0 < R) :
      ∫ (z : ℂ), windingWeight (circleMap 0 R) 0 (2 * Real.pi) z = Real.pi * R ^ 2

      The actual area integral of the circular winding weight is π R².