FiniteCircleGreen.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The precise classical Green input used below.

M. Spivak, Calculus on Manifolds (1965), Theorem 5-5, p.124, Stokes' theorem on a compact oriented manifold with boundary. The specialization is a bounded smooth Jordan region with finitely many pairwise disjoint round holes and a smooth real one-form. Circle boundaries have positive disk orientation, so their integrals are subtracted. The compact region lies inside the open set of smoothness. https://www.cimat.mx/~gil/docencia/2013/topologia_variedades/spivak-calculus-on-manifolds.pdf

structure OAI.CircleDomainRigidity.PositiveJordanParametrization line 28
Source documentation
A positively oriented regular parametrization of the actual Jordan boundary. Positivity is specified by the real argument lift around interior points, independently of any integration formula.
```
structure PositiveJordanParametrization (H : ℂ ≃ₜ ℂ) (γ : ℝ → ℂ) : Prop where
…
```
def OAI.CircleDomainRigidity.planarFormIntegral line 38
Source documentation
Real line integral of P dx + Q dy, with parameter interval [0,1].
```
def planarFormIntegral (P Q : ℂ → ℝ) (γ : ℝ → ℂ) : ℝ :=
…
```
def OAI.CircleDomainRigidity.unitCircleParam line 41
def OAI.CircleDomainRigidity.FiniteCircleGreenFormula line 45
Source documentation
Published input: the finite-round-hole planar specialization of Spivak's Theorem5-5. All geometric boundaries and integrals are explicit.
```
def FiniteCircleGreenFormula : Prop :=
…
```

theorem OAI.CircleDomainRigidity.finiteCircleGreen_weighted_closed_form line 60

Source documentation

The weighted Green identity for an actual closed real one-form. Closedness removes the second-derivative term; no Stokes estimate is assumed.

theorem finiteCircleGreen_weighted_closed_form
    (hgreen : FiniteCircleGreenFormula)
    (H : ℂ ≃ₜ ℂ) (γ : ℝ → ℂ) (hγ : PositiveJordanParametrization H γ)
    (n : ℕ) (c : Fin n → ℂ) (r : Fin n → ℝ) (hr : ∀ i, 0 < r i)
    (hd : Pairwise (Disjoint on fun i => Metric.closedBall (c i) (r i)))
    (hin : ∀ i, Metric.closedBall (c i) (r i) ⊆ jordanInterior H)
    (O : Set ℂ) (hO : IsOpen O)
    (hsub : (closure (jordanInterior H) \ ⋃ i, Metric.ball (c i) (r i)) ⊆ O)
    (φ P Q : ℂ → ℝ) (hφ : ContDiffOn ℝ (⊤ : ℕ∞) φ O)
    (hP : ContDiffOn ℝ (⊤ : ℕ∞) P O) (hQ : ContDiffOn ℝ (⊤ : ℕ∞) Q O)
    (hclosed : ∀ z ∈ O, (fderiv ℝ Q z) 1 = (fderiv ℝ P z) Complex.I) :
    planarFormIntegral (φ * P) (φ * Q) γ -
…

Mentions: OAI.CircleDomainRigidity.FiniteCircleGreenFormula, OAI.CircleDomainRigidity.PositiveJordanParametrization, OAI.CircleDomainRigidity.jordanInterior, OAI.CircleDomainRigidity.planarFormIntegral