MaskedTerminalBranches.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Actual nonsingular terminal branches and their summed excess

Only the nonsingular terminal subfamily is used for each coordinate. The real branches project to the filled circle maps on full collars, and the original band bound gives the required square-sum estimate.

theorem OAI.CircleDomainRigidity.FiniteTransfer.terminal_staircase_is_actual_masked_branch line 21

theorem OAI.CircleDomainRigidity.FiniteTransfer.actual_masked_terminal_branches_of_staircase_bound line 47

Source documentation

Directly consume the uniform staircase oscillation supplied by the physical terminal construction. The width may be selected afterwards.

theorem actual_masked_terminal_branches_of_staircase_bound
    {I J : Type*} [Fintype I] [Fintype J] {n : ℕ}
    {D : J → Set (ℝ × ℝ)} (hD : ∀ j, IsOpen (D j))
    {Ω : Set (ℝ × ℝ)} (A O : I → Set (ℝ × ℝ)) (hO : ∀ i, IsOpen (O i))
    (hAO : ∀ i, A i ⊆ O i) (hAD : ∀ i x, x ∈ A i → ∀ j, x ∉ D j)
    (M : Fin n → Set (ℝ × ℝ)) (f F : Fin n → (ℝ × ℝ) → UnitAddCircle)
    (χ : (ℝ × ℝ) → ℝ) (u : I → Fin n → (ℝ × ℝ) → ℝ)
    (S : Fin n → Finset I) (a : I → Fin n → ℝ)
    (hu : ∀ l i, i ∈ S l → ContDiffOn ℝ ∞ (u i l) (O i))
    (hproj : ∀ l i, i ∈ S l → ∀ x ∈ O i, (u i l x : UnitAddCircle) = f l x)
    (hχone : ∀ i x, x ∈ O i → χ x = 1)
    (N : ℕ) {δ η : ℝ} (hδ : 0 < δ) (hδh : δ < reciprocalGridStep N / 4) (θ : Fin n → ℝ)
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.reciprocalGridStep

theorem OAI.CircleDomainRigidity.FiniteTransfer.actual_masked_terminal_branches_and_excess line 86