TerminalDisks.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Selecting finite terminal neighborhoods with simultaneous band control

Section 2, Step 2 of the Koebe manuscript first fixes finitely many terminal points and then chooses their neighborhoods, before choosing the staircase width. Here positive-radius metric balls are selected inside prescribed neighborhoods with pairwise disjoint closed balls. Their physical coordinate values lie in the boundary bands enlarged by h; hence all shifted staircases have oscillation at most a + 4h there, simultaneously for every staircase width.

For the complex plane these selected balls are actual round disks. On a general quotient metric sphere they are only metric neighborhoods: the separate smooth-contour construction is still needed to obtain physical smooth Jordan boundaries around non-point fibers.

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_disjoint_closedBalls_in_neighborhoods line 33

Source documentation

Finitely many distinct points have disjoint closed-ball neighborhoods inside arbitrary prescribed neighborhoods, with any prescribed positive upper bounds for their radii.

theorem exists_disjoint_closedBalls_in_neighborhoods
    {X I : Type*} [MetricSpace X] [Fintype I]
    (p : I → X) (hp : Injective p) (O : I → Set X)
    (hO : ∀ i, O i ∈ 𝓝 (p i)) (ρ : I → ℝ) (hρ : ∀ i, 0 < ρ i) :
    ∃ r : I → ℝ, (∀ i, 0 < r i ∧ r i < ρ i) ∧
      (∀ i, closedBall (p i) (r i) ⊆ O i) ∧
      Pairwise (Disjoint on fun i => closedBall (p i) (r i)) := by
…

theorem OAI.CircleDomainRigidity.FiniteTransfer.eventually_mem_enlarged_boundary_band line 68

Source documentation

The values near a boundary point lie in its actual liminf/limsup band enlarged by any positive margin.

theorem eventually_mem_enlarged_boundary_band
    {X : Type*} [TopologicalSpace X] {G : Set X} {f : X → ℝ} {M : ℝ}
    (hM : ∀ y ∈ G, |f y| ≤ M) (x : X) {h : ℝ} (hh : 0 < h) :
    ∀ᶠ y in 𝓝[G] x,
      liminf f (𝓝[G] x) - h < f y ∧ f y < limsup f (𝓝[G] x) + h := by
…

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_terminal_balls_with_band_control line 87

Source documentation

Actual finite-radius selection, with all nonsingular coordinate band bounds imposed at once. active i j specifies which coordinates need a real branch at terminal point i; the physical domain and branch may depend on that terminal point, as for periodic coordinates.

theorem exists_terminal_balls_with_band_control
    {X I J : Type*} [MetricSpace X] [Fintype I] [Fintype J]
    (p : I → X) (hp : Injective p) (O : I → Set X)
    (hO : ∀ i, O i ∈ 𝓝 (p i)) (ρ : I → ℝ) (hρ : ∀ i, 0 < ρ i)
    (G : I → Set X) (f : I → J → X → ℝ) (M : I → J → ℝ)
    (hM : ∀ i j y, y ∈ G i → |f i j y| ≤ M i j)
    (active : I → J → Prop) {h : ℝ} (hh : 0 < h) :
    ∃ r : I → ℝ, (∀ i, 0 < r i ∧ r i < ρ i) ∧
      (∀ i, closedBall (p i) (r i) ⊆ O i) ∧
      Pairwise (Disjoint on fun i => closedBall (p i) (r i)) ∧
      ∀ i j, active i j → ∀ y ∈ closedBall (p i) (r i) ∩ G i,
        liminf (f i j) (𝓝[G i] (p i)) - h < f i j y ∧
…

theorem OAI.CircleDomainRigidity.FiniteTransfer.abs_sub_le_of_enlarged_boundary_band line 117

Source documentation

Enlarging the coordinate band by h at each end gives oscillation at most its band budget plus 2h.

theorem abs_sub_le_of_enlarged_boundary_band
    {X : Type*} [TopologicalSpace X] {G : Set X} {f : X → ℝ}
    {s x y : X} {a h : ℝ}
    (hband : limsup f (𝓝[G] s) - liminf f (𝓝[G] s) ≤ a)
    (hx : liminf f (𝓝[G] s) - h < f x ∧ f x < limsup f (𝓝[G] s) + h)
    (hy : liminf f (𝓝[G] s) - h < f y ∧ f y < limsup f (𝓝[G] s) + h) :
    |f x - f y| ≤ a + 2 * h := by
…

theorem OAI.CircleDomainRigidity.FiniteTransfer.terminal_staircase_oscillation_le line 130

Source documentation

The terminal oscillation estimate is uniform in the staircase width. Thus disk neighborhoods can be fixed before taking that width to zero, exactly as required in Step 2.

theorem terminal_staircase_oscillation_le
    {X : Type*} [TopologicalSpace X] {G : Set X} {f : X → ℝ}
    {s x y : X} {a h : ℝ} (hh : 0 < h)
    (hband : limsup f (𝓝[G] s) - liminf f (𝓝[G] s) ≤ a)
    (hx : liminf f (𝓝[G] s) - h < f x ∧ f x < limsup f (𝓝[G] s) + h)
    (hy : liminf f (𝓝[G] s) - h < f y ∧ f y < limsup f (𝓝[G] s) + h)
    (δ θ : ℝ) :
    |shiftedStaircase h δ θ (f x) - shiftedStaircase h δ θ (f y)| ≤ a + 4 * h := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.shiftedStaircase

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_terminal_balls_with_uniform_staircase_oscillation line 147

Source documentation

The radii are chosen once for all staircase widths and shifts. Any subsequently constructed physical terminal contour lying in these closed balls inherits the paper's a + 4h oscillation bound.

theorem exists_terminal_balls_with_uniform_staircase_oscillation
    {X I J : Type*} [MetricSpace X] [Fintype I] [Fintype J]
    (p : I → X) (hp : Injective p) (O : I → Set X)
    (hO : ∀ i, O i ∈ 𝓝 (p i)) (ρ : I → ℝ) (hρ : ∀ i, 0 < ρ i)
    (G : I → Set X) (f : I → J → X → ℝ) (M : I → J → ℝ)
    (hM : ∀ i j y, y ∈ G i → |f i j y| ≤ M i j)
    (active : I → J → Prop) (a : I → J → ℝ)
    (hbudget : ∀ i j, active i j →
      limsup (f i j) (𝓝[G i] (p i)) - liminf (f i j) (𝓝[G i] (p i)) ≤ a i j)
    {h : ℝ} (hh : 0 < h) :
    ∃ r : I → ℝ, (∀ i, 0 < r i ∧ r i < ρ i) ∧
      (∀ i, closedBall (p i) (r i) ⊆ O i) ∧
…