GridCoordinateFilling.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Smooth coordinate fillings from the actual boundary grids

The contour theorem gives one possible active label at each boundary. The reciprocal-grid calculation turns its avoidance conclusions into inactive-lattice avoidance for the actual local real branches. Thus the smooth filling theorem applies at all sufficiently small widths.

theorem OAI.CircleDomainRigidity.FiniteTransfer.frontier_realJordanInterior line 21
theorem OAI.CircleDomainRigidity.FiniteTransfer.branch_avoids_lattice_on_real_boundary line 26

theorem OAI.CircleDomainRigidity.FiniteTransfer.eventually_filled_coordinates_from_boundary_grids line 47

Source documentation

The active label and all inactive lattice-avoidance premises are constructed from the physical contour output. Only the actual local branches and collar agreement remain as coordinate data.

theorem eventually_filled_coordinates_from_boundary_grids
    {I : Type*} [Fintype I] {n N : ℕ} (hn : 0 < n)
    (H : I → ℂ ≃ₜ ℂ)
    (hH : Pairwise (Disjoint on fun i => closure (jordanInterior (H i))))
    {X : Type*} [TopologicalSpace X] (U : Set X) (hU : IsOpen U)
    (f : Fin n → X → ℝ) (hf : ∀ l, ContinuousOn (f l) U) (q : ℂ → X)
    (hUq : ∀ i z, z ∈ frontier (jordanInterior (H i)) → q z ∈ U)
    (θ : Fin n → ℝ)
    (hgrid : ∀ i, ∃ k : ℕ, ∀ l : Fin n, l.val ≠ k →
      Disjoint (frontier (jordanInterior (H i)))
        (q ⁻¹' (⋃ j, reciprocalBandLevel U (f l) (θ l) N j)))
    (O : I → Set (ℝ × ℝ)) (hO : ∀ i, IsOpen (O i))
…

Mentions: OAI.CircleDomainRigidity.jordanInterior, OAI.CircleDomainRigidity.FiniteTransfer.reciprocalBandLevel

theorem OAI.CircleDomainRigidity.FiniteTransfer.eventually_fill_actual_cutoff_coordinates line 84

Source documentation

For real coordinates, the collars and their branch agreement are constructed directly from the region where the actual cutoff equals one.

theorem eventually_fill_actual_cutoff_coordinates
    {I : Type*} [Fintype I] {n N : ℕ} (hn : 0 < n)
    (H : I → ℂ ≃ₜ ℂ)
    (hH : Pairwise (Disjoint on fun i => closure (jordanInterior (H i))))
    {G : Set (ℝ × ℝ)} (hG : IsOpen G)
    (u : Fin n → (ℝ × ℝ) → ℝ) (hu : ∀ l, ContDiffOn ℝ ∞ (u l) G)
    (χ : (ℝ × ℝ) → ℝ) (hχ : ContDiff ℝ ∞ χ)
    (hboundary : ∀ i z, z ∈ frontier (jordanInterior (H i)) →
      Complex.equivRealProdCLM z ∈ G ∩ interior {x | χ x = 1})
    {X : Type*} [TopologicalSpace X] (U : Set X) (hU : IsOpen U)
    (f : Fin n → X → ℝ) (hf : ∀ l, ContinuousOn (f l) U) (q : ℂ → X)
    (hUq : ∀ i z, z ∈ frontier (jordanInterior (H i)) → q z ∈ U)
…

Mentions: OAI.CircleDomainRigidity.jordanInterior