RealAnchoredBarriers.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Collapse with a fixed outer zero contour, as used by the selected barriers.

theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd.exists_positive_level_in_source_open line 19

theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd.target_eq_singleton_of_small_anchored_plateaus line 29

Source documentation

The source outer contour is fixed independently of the shrinking tests. Its target contour and the common radius bound are constructed once.

theorem target_eq_singleton_of_small_anchored_plateaus
    (hsard : SmoothPlanarSard) (hsch : PlanarSchoenflies) (harea : ExteriorCoefficientAreaTheorem)
    (hG : IsOpen G) (hconn : IsConnected G) (hε : Tendsto ε atTop (𝓝 0))
    (hπ : Continuous π)
    (hr : ∀ x y, π x = π y ↔ x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x))
    (hq : q ∈ Gᶜ) (A : SmoothJordanCore G) (j : Fin A.count)
    (hCA : connectedComponentIn Gᶜ q ⊆ ((↑) : ℂ → Sphere) '' jordanInterior (A.disk j))
    (hsmall : ∀ δ : ℝ, 0 < δ → ∃ (l : ℕ) (U : Set Sphere),
      IsOpen U ∧ π q ∈ U ∧ (∀ x ∈ U ∩ d.source, d.coordinate l x = 1) ∧
      (∀ z ∈ frontier (jordanInterior (A.disk j)),
        d.physical l (Complex.equivRealProdCLM z) = 0) ∧
      Real.sqrt (∫ x in realChartDomain G,
…

Mentions: OAI.CircleDomainRigidity.SmoothPlanarSard, OAI.CircleDomainRigidity.PlanarSchoenflies, OAI.CircleDomainRigidity.ExteriorCoefficientAreaTheorem, OAI.CircleDomainRigidity.SmoothJordanCore, OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.jordanInterior, OAI.CircleDomainRigidity.FiniteTransfer.realChartDomain