CompatibleFillingDisks.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Filling disks for the actual free/flagged grid setup

The levels below are the actual equally spaced circle levels of the compact band graph. At a free point a singleton real band gives one level per label. At a flagged point outside the terminal collision set, two distinct label grids cannot occur. The pair family may represent each unordered pair in either orientation. These facts discharge the lower-obstacle premise of the descending contour construction.

def OAI.CircleDomainRigidity.FiniteTransfer.reciprocalBandLevel line 23
def OAI.CircleDomainRigidity.FiniteTransfer.OrderedBandGridCompatibility line 30
Source documentation
The manuscript's ordered compatibility: a new label meets no nontrivial component formed using only earlier labels at a free point.
```
def OrderedBandGridCompatibility {X S : Type*} [TopologicalSpace X] {n : ℕ}
    (G : Set X) (f : Fin n → X → ℝ) (θ : Fin n → ℝ) (N : ℕ)
    (A : Set X) (σ : S → X) : Prop :=
…
```
theorem OAI.CircleDomainRigidity.FiniteTransfer.isClosed_reciprocalBandLevel line 39
theorem OAI.CircleDomainRigidity.FiniteTransfer.reciprocal_circle_levels_injective line 46
theorem OAI.CircleDomainRigidity.FiniteTransfer.reciprocalBandLevel_unique_of_singleton_fiber line 71
theorem OAI.CircleDomainRigidity.FiniteTransfer.latticeBandIncidence_of_reciprocalBandLevel line 90

theorem OAI.CircleDomainRigidity.FiniteTransfer.no_two_flagged_grids_outside_terminals line 114

Source documentation

Actual collision terminals exclude every pair of distinct flagged grids.

theorem no_two_flagged_grids_outside_terminals
    {n N : ℕ} {P S X : Type*} [TopologicalSpace X]
    (G : Set X) (f : Fin n → X → ℝ) (σ : S → X)
    (a b : Fin n → S → ℝ) (θ : Fin n → ℝ)
    (pairs : P → Fin n × Fin n)
    (hpairs : ∀ i j : Fin n, i ≠ j → ∃ p, pairs p = (i, j) ∨ pairs p = (j, i))
    (F : Set S)
    (hband : ∀ i s, {r : ℝ | (σ s, r) ∈ intervalFiberHull (clusterGraph G (f i))} =
      Icc (a i s) (b i s))
    {s : S} (hs : s ∉ gridTerminalIndices F (reciprocalGridStep N) pairs a b θ)
    {i j : Fin n} (hij : i ≠ j)
    (hi : σ s ∈ ⋃ k, reciprocalBandLevel G (f i) (θ i) N k)
…

Mentions: OAI.CircleDomainRigidity.intervalFiberHull, OAI.CircleDomainRigidity.clusterGraph, OAI.CircleDomainRigidity.FiniteTransfer.gridTerminalIndices, OAI.CircleDomainRigidity.FiniteTransfer.reciprocalGridStep, OAI.CircleDomainRigidity.FiniteTransfer.reciprocalBandLevel

theorem OAI.CircleDomainRigidity.FiniteTransfer.lower_obstacle_singleton_of_compatible_bands line 143

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_filling_disks_of_compatible_bands line 217

Source documentation

Compact band grids admit filling disks by free-point compatibility and the selected collision terminals.

theorem exists_filling_disks_of_compatible_bands
    (hsard : SmoothPlanarSard) (hschoenflies : PlanarSchoenflies)
    (G : Set Sphere) (π : Sphere → Sphere) (hπ : Continuous π)
    (hclosed : IsClosedMap π) (hsurj : Surjective π)
    (hr : ∀ x y, π x = π y ↔
      x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x))
    {n N : ℕ} {P S : Type*} (U : Set Sphere) (f : Fin n → Sphere → ℝ)
    (M : Fin n → ℝ) (hbounded : ∀ i x, x ∈ U → |f i x| ≤ M i)
    (σ : S → Sphere) (a b : Fin n → S → ℝ) (θ : Fin n → ℝ)
    (pairs : P → Fin n × Fin n)
    (hpairs : ∀ i j : Fin n, i ≠ j → ∃ p, pairs p = (i, j) ∨ pairs p = (j, i))
    (F : Set S)
…

Mentions: OAI.CircleDomainRigidity.SmoothPlanarSard, OAI.CircleDomainRigidity.PlanarSchoenflies, OAI.CircleDomainRigidity.Sphere