RealAnchorRetention.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The source anchor's fixed zero plateau is retained on a compact target anchor in the actual finite models.

theorem OAI.CircleDomainRigidity.FiniteTransfer.AssignedRealModelLimit.plane_open_embedding line 22
theorem OAI.CircleDomainRigidity.FiniteTransfer.AssignedRealModelLimit.eventually_compact_subset_anchor_image line 34

theorem OAI.CircleDomainRigidity.FiniteTransfer.AssignedRealModelLimit.eventually_zero_on_anchor_image line 64

Source documentation

A compact portion of the limiting anchor image has the original test value zero in all sufficiently late finite models, and lies in their actual target domains.

theorem eventually_zero_on_anchor_image
    (hsch : PlanarSchoenflies) (hG : IsOpen G) (H : ℂ ≃ₜ ℂ)
    (hHG : closure (jordanInterior H) ⊆ ((↑) : ℂ → Sphere) ⁻¹' G)
    (l : ℕ) (hzero : ∀ z ∈ closure (jordanInterior H), d.physical l (Complex.equivRealProdCLM z) = 0)
    {K : Set ℂ} (hK : IsCompact K) (hKA : K ⊆ A.function '' jordanInterior H) :
    ∀ᶠ n in atTop, ∀ z ∈ K,
      (z : Sphere) ∈ (M.stages (A.subsequence n)).domain ∧
      sphereRealFunction ((M.stages (A.subsequence n)).functions (prefixIndex l (A.subsequence n)))
        ((M.stages (A.subsequence n)).inverse z) = 0 := by
…

Mentions: OAI.CircleDomainRigidity.PlanarSchoenflies, OAI.CircleDomainRigidity.jordanInterior, OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.sphereRealFunction, OAI.CircleDomainRigidity.FiniteTransfer.prefixIndex