CircleTerminalBranches.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Actual terminal branches of the transferred circle maps

A real branch on a terminal collar remains a branch after cutoff and filling. Its boundary oscillation therefore has the stated staircase bound, even when the completed circle map has no global real lift.

theorem OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCircleFamily.eventuallyEq_near_set line 21

theorem OAI.CircleDomainRigidity.FiniteTransfer.terminal_staircase_is_actual_branch line 32

Source documentation

The explicit terminal staircase is a smooth real lift of the actual transferred circle map on a full neighborhood of the terminal boundary.

theorem terminal_staircase_is_actual_branch
    {I : Type*} [Fintype I]
    {D : I → Set (ℝ × ℝ)} (hD : ∀ i, IsOpen (D i))
    {Ω A O : Set (ℝ × ℝ)} (hO : IsOpen O) (hAO : A ⊆ O)
    (hA : ∀ x ∈ A, ∀ i, x ∉ D i)
    (f F : (ℝ × ℝ) → UnitAddCircle) (u χ : (ℝ × ℝ) → ℝ)
    (hu : ContDiffOn ℝ ∞ u O)
    (hproj : ∀ x ∈ O, (u x : UnitAddCircle) = f x)
    (hχone : ∀ x ∈ O, χ x = 1)
    (N : ℕ) {δ : ℝ} (hδ : 0 < δ) (hδh : δ < reciprocalGridStep N / 4) (θ : ℝ)
    (hF : IsFilledCircleFamily D Ω
      (fun _ : Unit => circleCutoff f χ (shiftedStaircase (reciprocalGridStep N) δ θ))
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.reciprocalGridStep, OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCircleFamily, OAI.CircleDomainRigidity.FiniteTransfer.circleCutoff, OAI.CircleDomainRigidity.FiniteTransfer.shiftedStaircase

theorem OAI.CircleDomainRigidity.FiniteTransfer.staircase_branch_diameter_le line 59

Source documentation

Boundary diameter of the actual chosen real branch.

theorem staircase_branch_diameter_le
    {A : Set (ℝ × ℝ)} (u : (ℝ × ℝ) → ℝ) (P : ℝ → ℝ) {a h : ℝ}
    (hbound : 0 ≤ a + 4 * h)
    (hosc : ∀ x ∈ A, ∀ y ∈ A, |P (u x) - P (u y)| ≤ a + 4 * h) :
    Metric.diam ((fun x => P (u x)) '' A) ≤ a + 4 * h := by
…