BoundaryGridAvoidance.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

From physical grid avoidance to inactive staircase branches

At reciprocal spacing every integer lattice level represents one of the finite circle levels. Consequently the actual physical boundary avoidance constructed by the contour theorem gives exactly the shifted-lattice avoidance needed by the smooth filling theorem, including for local real lifts of circle coordinates.

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_reciprocal_level_of_mem_lattice line 22
theorem OAI.CircleDomainRigidity.FiniteTransfer.mem_reciprocal_grid_of_lift_lattice line 44

theorem OAI.CircleDomainRigidity.FiniteTransfer.branch_image_disjoint_lattice_of_boundary_grid_avoidance line 55

Source documentation

A local branch projecting to the original circle coordinate inherits exact shifted-lattice avoidance from the physical quotient grid.

theorem branch_image_disjoint_lattice_of_boundary_grid_avoidance
    {X Y : Type*} [TopologicalSpace X] {U : Set X} (hU : IsOpen U)
    {f : X → ℝ} (hf : ContinuousOn f U) (q : Y → X) (A : Set Y)
    (u : Y → ℝ) (hA : ∀ y ∈ A, q y ∈ U)
    (hlift : ∀ y ∈ A, (u y : UnitAddCircle) = (f (q y) : UnitAddCircle))
    {N : ℕ} {θ : ℝ}
    (havoid : Disjoint A (q ⁻¹' (⋃ j, reciprocalBandLevel U f θ N j))) :
    Disjoint (u '' A) (shiftedLattice (reciprocalGridStep N) θ) := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.reciprocalBandLevel, OAI.CircleDomainRigidity.FiniteTransfer.shiftedLattice, OAI.CircleDomainRigidity.FiniteTransfer.reciprocalGridStep

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_active_coordinate_of_single_exception line 70
Source documentation
A possible exception indexed in the natural numbers can be replaced by one actual coordinate, even if the exception lies outside the list.
```
theorem exists_active_coordinate_of_single_exception
    {n : ℕ} (hn : 0 < n) (P : Fin n → Prop)
    (hP : ∃ k : ℕ, ∀ i : Fin n, i.val ≠ k → P i) :
    ∃ a : Fin n, ∀ i, i ≠ a → P i := by
…
```