CircleFillings.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous smooth fillings of circle coordinates

Connected collars and one active staircase per disk give actual real rank-one extensions. Their projections patch into the retained circle maps. The construction requires only the existing local branches and does not assert any unproved period or winding statement.

def OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCircleFamily line 21

theorem OAI.CircleDomainRigidity.FiniteTransfer.eventually_exists_rank_one_collar_families line 32

Source documentation

One common small width produces real rank-one collar extensions on all disks before any global projection or patching is performed.

theorem eventually_exists_rank_one_collar_families
    {I L : Type*} [Fintype I] [Fintype L]
    (D : I → Set (ℝ × ℝ))
    (hfrontc : ∀ i, IsCompact (frontier (D i)))
    (hfrontconn : ∀ i, IsConnected (frontier (D i)))
    (O : I → Set (ℝ × ℝ)) (hO : ∀ i, IsOpen (O i))
    (hDO : ∀ i, frontier (D i) ⊆ O i)
    (u : I → L → (ℝ × ℝ) → ℝ)
    (hu : ∀ i l, ContDiffOn ℝ ∞ (u i l) (O i))
    (active : I → L) {h : ℝ} (hh : 0 < h) (θ : L → ℝ)
    (havoid : ∀ i l, l ≠ active i →
      Disjoint (u i l '' frontier (D i)) (shiftedLattice h (θ l))) :
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.shiftedLattice

theorem OAI.CircleDomainRigidity.FiniteTransfer.eventually_exists_filled_circle_coordinates line 93

Source documentation

Actual circle maps are filled simultaneously from their real collar branches. The agreement is on full neighborhoods of the boundaries.

theorem eventually_exists_filled_circle_coordinates
    {I L : Type*} [Fintype I] [Fintype L]
    (D : I → Set (ℝ × ℝ)) (hD : ∀ i, IsOpen (D i))
    (hdisj : Pairwise (Disjoint on fun i => closure (D i)))
    (hfrontc : ∀ i, IsCompact (frontier (D i)))
    (hfrontconn : ∀ i, IsConnected (frontier (D i)))
    (O : I → Set (ℝ × ℝ)) (hO : ∀ i, IsOpen (O i))
    (hDO : ∀ i, frontier (D i) ⊆ O i)
    (u : I → L → (ℝ × ℝ) → ℝ)
    (hu : ∀ i l, ContDiffOn ℝ ∞ (u i l) (O i))
    (active : I → L) {h : ℝ} (hh : 0 < h) (θ : L → ℝ)
    (havoid : ∀ i l, l ≠ active i →
…