UnmarkedRealEnds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Collapse from a selected cover by local real plateaus

Arbitrarily small anchored one-plateaus force each target component with an unmarked source address to be a singleton, by the line-payment estimate.

def OAI.CircleDomainRigidity.FiniteTransfer.CountableRealCoordinates.barrierNorm line 25
Source documentation
Original energy and original band norm of one real coordinate.
```
def CountableRealCoordinates.barrierNorm (d : CountableRealCoordinates G π σ) (l : ℕ) : ℝ :=
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.CountableRealCoordinates
theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd.eq_singleton_of_plateau_cover line 30

theorem OAI.CircleDomainRigidity.FiniteTransfer.AssignedRealModelLimit.singleton_or_marked_disk line 55

Source documentation

All non-singleton limit components carry a marked source address, and each contains its corresponding round limiting disk.

theorem AssignedRealModelLimit.singleton_or_marked_disk
    (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))
    (V : ℕ → ℕ → Set Sphere) (hV : ∀ k l, IsOpen (V k l))
    (hone : ∀ k l, ∀ x ∈ V k l ∩ d.source, d.coordinate l x = 1)
    (hzero : ∀ k l, (V k l).Nonempty → ∀ z ∈ sphere (0 : ℂ) (2 * M.radius),
      d.physical l (Complex.equivRealProdCLM z) = 0)
    (hnorm : ∀ k l, (V k l).Nonempty → d.barrierNorm l < modelError k)
    (hcover : ∀ b ∈ (π '' Gᶜ) \ range σ, ∀ k, ∃ l, b ∈ V k l)
    {p : Sphere} (hp : p ∈ (extendAtInfinity L.function '' G)ᶜ) :
…

Mentions: OAI.CircleDomainRigidity.SmoothPlanarSard, OAI.CircleDomainRigidity.PlanarSchoenflies, OAI.CircleDomainRigidity.ExteriorCoefficientAreaTheorem, OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.FiniteTransfer.modelError, OAI.CircleDomainRigidity.extendAtInfinity