InactiveCollars.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Staircases are constant on collars avoiding their grids

A compact connected collar has a compact connected real branch image. If this image misses the translated lattice, it has positive distance from that closed lattice. Every sufficiently narrow staircase therefore has zero derivative on the image and is constant on the collar. The width bound can be chosen simultaneously for finitely many collars.

def OAI.CircleDomainRigidity.FiniteTransfer.shiftedLattice line 24
theorem OAI.CircleDomainRigidity.FiniteTransfer.isClosed_shiftedLattice line 26
theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_uniform_lattice_distance line 42

theorem OAI.CircleDomainRigidity.FiniteTransfer.eventually_constant_staircase_on_collar line 56

Source documentation

The same positive width bound works for the whole collar, and the proof yields both derivative vanishing and constancy.

theorem eventually_constant_staircase_on_collar
    {X : Type*} [TopologicalSpace X] {C : Set X} (hC : IsCompact C)
    (hconn : IsPreconnected C) (u : X → ℝ) (hu : ContinuousOn u C)
    {h θ : ℝ} (hh : 0 < h) (havoid : Disjoint (u '' C) (shiftedLattice h θ)) :
    ∀ᶠ δ : ℝ in 𝓝[>] 0,
      (∀ x ∈ C, deriv (shiftedStaircase h δ θ) (u x) = 0) ∧
      ∀ x ∈ C, ∀ y ∈ C, shiftedStaircase h δ θ (u x) = shiftedStaircase h δ θ (u y) := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.shiftedLattice, OAI.CircleDomainRigidity.FiniteTransfer.shiftedStaircase

theorem OAI.CircleDomainRigidity.FiniteTransfer.eventually_constant_staircases_on_finite_collars line 90

Source documentation

Finitely many inactive collars impose one common eventual width condition; the grid choice and all collars stay fixed.

theorem eventually_constant_staircases_on_finite_collars
    {X I : Type*} [TopologicalSpace X] [Fintype I]
    (C : I → Set X) (hC : ∀ i, IsCompact (C i))
    (hconn : ∀ i, IsPreconnected (C i)) (u : I → X → ℝ)
    (hu : ∀ i, ContinuousOn (u i) (C i)) {h : ℝ} (hh : 0 < h) (θ : I → ℝ)
    (havoid : ∀ i, Disjoint (u i '' C i) (shiftedLattice h (θ i))) :
    ∀ᶠ δ : ℝ in 𝓝[>] 0, ∀ i, ∀ x ∈ C i, ∀ y ∈ C i,
      shiftedStaircase h δ (θ i) (u i x) = shiftedStaircase h δ (θ i) (u i y) := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.shiftedLattice, OAI.CircleDomainRigidity.FiniteTransfer.shiftedStaircase