FilledCoordinates.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous smooth coordinate fillings

Compact connected collars are chosen inside the supplied real-branch domains and away from all inactive lattices. A single sufficiently small width makes every inactive staircase constant there. Rank-one collar extensions then patch into the retained coordinates across all the pairwise disjoint filling disks. No lifting theorem is assumed.

def OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCoordinateFamily line 22
theorem OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCoordinateFamily.eventuallyEq_outside line 31

theorem OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCoordinateFamily.abs_wedge_le line 52

Source documentation

The actual pairwise wedge magnitude cannot increase under the filling: it is unchanged off the disks and vanishes inside them.

theorem IsFilledCoordinateFamily.abs_wedge_le
    {I L : Type*} [Fintype I] {D : I → Set (ℝ × ℝ)} {Ω : Set (ℝ × ℝ)}
    {v F : L → (ℝ × ℝ) → ℝ} (hF : IsFilledCoordinateFamily D Ω v F)
    (hD : ∀ i, IsOpen (D i)) (l m : L) (hlm : l ≠ m) (x : ℝ × ℝ) :
    |planarWedge (planarGradient (F l) x) (planarGradient (F m) x)| ≤
      |planarWedge (planarGradient (v l) x) (planarGradient (v m) x)| := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCoordinateFamily, OAI.CircleDomainRigidity.FiniteTransfer.planarWedge, OAI.CircleDomainRigidity.FiniteTransfer.planarGradient

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_inactive_connected_collar line 67

Source documentation

The open collar can be chosen to avoid every inactive lattice even when the real branches are smooth only on their supplied open domains.

theorem exists_inactive_connected_collar
    {L : Type*} [Fintype L] {A O : Set (ℝ × ℝ)}
    (hAc : IsCompact A) (hAconn : IsConnected A) (hO : IsOpen O) (hAO : A ⊆ O)
    (u : L → (ℝ × ℝ) → ℝ) (hu : ∀ l, ContDiffOn ℝ ∞ (u l) O)
    (active : L) {h : ℝ} (hh : 0 < h) (θ : L → ℝ)
    (havoid : ∀ l, l ≠ active → Disjoint (u l '' A) (shiftedLattice h (θ l))) :
    ∃ C : Set (ℝ × ℝ), IsCompact C ∧ IsConnected C ∧ C ∈ 𝓝ˢ A ∧ C ⊆ O ∧
      ∀ l, l ≠ active → Disjoint (u l '' C) (shiftedLattice h (θ l)) := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.shiftedLattice

theorem OAI.CircleDomainRigidity.FiniteTransfer.eventually_exists_filled_coordinates line 103

Source documentation

A common eventual width works for all disks and all inactive coordinates. The old coordinates need only be smooth off the filling interiors; on the collars their actual real staircase branches are supplied.

theorem eventually_exists_filled_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 →
…

def OAI.CircleDomainRigidity.FiniteTransfer.realJordanInterior line 202
Source documentation
A physical Jordan disk in the real coordinates used for the energy and patching calculation.
```
def realJordanInterior (H : ℂ ≃ₜ ℂ) : Set (ℝ × ℝ) :=
…
```
theorem OAI.CircleDomainRigidity.FiniteTransfer.realJordanInterior_geometry line 205
theorem OAI.CircleDomainRigidity.FiniteTransfer.pairwise_disjoint_realJordan_closures line 219

theorem OAI.CircleDomainRigidity.FiniteTransfer.eventually_exists_filled_jordan_coordinates line 232

Source documentation

Concrete finite-Jordan-disk version of the filling theorem. The compact connected collars and all inactive constants are constructed.

theorem eventually_exists_filled_jordan_coordinates
    {I L : Type*} [Fintype I] [Fintype L]
    (H : I → ℂ ≃ₜ ℂ)
    (hH : Pairwise (Disjoint on fun i => closure (jordanInterior (H i))))
    (O : I → Set (ℝ × ℝ)) (hO : ∀ i, IsOpen (O i))
    (hHO : ∀ i, frontier (realJordanInterior (H 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 (realJordanInterior (H i))) (shiftedLattice h (θ l)))
    (v : ℝ → L → (ℝ × ℝ) → ℝ) (Ω : Set (ℝ × ℝ))
…

Mentions: OAI.CircleDomainRigidity.jordanInterior, OAI.CircleDomainRigidity.FiniteTransfer.realJordanInterior, OAI.CircleDomainRigidity.FiniteTransfer.shiftedLattice

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_good_width_filled_coordinates line 259

Source documentation

Once the grid and collars are fixed, a frequently good actual cost has an arbitrarily late index at which all smooth fillings are possible.

theorem exists_good_width_filled_coordinates
    {I L : Type*} (D : I → Set (ℝ × ℝ)) (Ω : Set (ℝ × ℝ))
    (v : ℝ → L → (ℝ × ℝ) → ℝ) {h : ℝ} (hh : 0 < h)
    (hfill : ∀ᶠ δ : ℝ in 𝓝[>] 0, ∃ F : L → (ℝ × ℝ) → ℝ,
      IsFilledCoordinateFamily D Ω (v δ) F)
    (cost : ℕ → ℝ) {η : ℝ} (hcost : ∃ᶠ k in atTop, cost k < η)
    (K : ℕ) :
    ∃ (k : ℕ) (F : L → (ℝ × ℝ) → ℝ),
      K ≤ k ∧ cost k < η ∧ IsFilledCoordinateFamily D Ω (v (staircaseWidth h k)) F := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCoordinateFamily, OAI.CircleDomainRigidity.FiniteTransfer.staircaseWidth