OAI/Analysis/CircleDomains/Modulus/TerminalOscillation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Summing the terminal oscillation errors

The simultaneous boundary estimate A ≤ a + 4h on finitely many terminal disks gives the required square-sum error 4h√J. Singular indices can be omitted by using any subfamily of the terminal indices.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.sqrt_sum_terminal_excess_sq_le line 17
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.sqrt_sum_terminal_excess_sq_lt line 41

    Source documentation

    The terminal-count selection directly gives the finite-transfer oscillation budget for every nonsingular subfamily.

    theorem sqrt_sum_terminal_excess_sq_lt {I : Type*} (S T : Finset I)
    (hST : S ⊆ T) (A a : I → ℝ) {h η : ℝ} (hh : 0 ≤ h)
    (hA : ∀ s ∈ S, A s ≤ a s + 4 * h)
    (hsmall : h * Real.sqrt (T.card : ℝ) < η) :
    Real.sqrt (∑ s ∈ S, max (A s - a s) 0 ^ 2) < 4 * η := by
…