TerminalTransfer.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual terminal oscillations after smooth filling

The fillings leave terminal boundaries unchanged. Since these boundaries lie in the one-plateau of the cutoff, their transferred coordinates are exactly the selected staircases. The original pointwise oscillation bound therefore gives the required square-sum bound for the actual boundary diameters, rather than for separately supplied numbers.

def OAI.CircleDomainRigidity.FiniteTransfer.terminalOscillation line 23
theorem OAI.CircleDomainRigidity.FiniteTransfer.filled_eq_staircase_on_terminal line 26
theorem OAI.CircleDomainRigidity.FiniteTransfer.terminalOscillation_le_of_staircase_bound line 46

theorem OAI.CircleDomainRigidity.FiniteTransfer.transferred_terminal_oscillation_bound line 72

Source documentation

The selected terminal-count bound controls the actual square-sum of excess boundary oscillations for every transferred coordinate.

theorem transferred_terminal_oscillation_bound
    {I J : Type*} [Fintype I] {n : ℕ} (T : I → ℂ ≃ₜ ℂ) (H : J → ℂ ≃ₜ ℂ)
    (hTH : ∀ i j, Disjoint (closure (jordanInterior (T i))) (closure (jordanInterior (H j))))
    {Ω : Set (ℝ × ℝ)} (u : Fin n → (ℝ × ℝ) → ℝ) (χ : (ℝ × ℝ) → ℝ)
    {h δ η : ℝ} (hh : 0 ≤ h) (θ : Fin n → ℝ) {F : Fin n → (ℝ × ℝ) → ℝ}
    (hF : IsFilledCoordinateFamily (fun j => realJordanInterior (H j)) Ω
      (cutoffCoordinateFamily u χ h δ θ) F)
    (hTC : ∀ i, Disjoint (((↑) : ℂ → Sphere) '' closure (jordanInterior (T i))) (cutoffCore χ))
    (a : I → Fin n → ℝ) (ha : ∀ i l, 0 ≤ a i l)
    (hbound : ∀ i l x, x ∈ frontier (jordanInterior (T i)) →
      ∀ y ∈ frontier (jordanInterior (T i)),
        |shiftedStaircase h δ (θ l) (u l (Complex.equivRealProdCLM x)) -
…

Mentions: OAI.CircleDomainRigidity.jordanInterior, OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCoordinateFamily, OAI.CircleDomainRigidity.FiniteTransfer.realJordanInterior, OAI.CircleDomainRigidity.FiniteTransfer.cutoffCoordinateFamily, OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.FiniteTransfer.cutoffCore, OAI.CircleDomainRigidity.FiniteTransfer.shiftedStaircase