OAI/Analysis/CircleDomains/Modulus/TerminalNormBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

From terminal excess to the full oscillation norm

The finite transfer bounds the square-sum of the positive excess above the original band widths. The elementary Euclidean triangle inequality then gives the full oscillation norm needed in parallel-line payment.

  1. theorem OAI.CircleDomainRigidity.sqrt_sum_sq_add_le line 17
  2. theorem OAI.CircleDomainRigidity.sqrt_sum_sq_le_band_add_excess line 37
  3. theorem OAI.CircleDomainRigidity.sqrt_sum_sq_le_of_excess_budget line 50