OAI/Analysis/CircleDomains/Modulus/FiniteGapPayment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Variation payment across finitely many gaps

The domain intervals of a line crossing a finite circle domain contribute their actual derivative variation. Each intervening hole contributes only the difference of the two endpoint traces. This is the finite telescoping step in the manuscript's parallel-line payment estimate.

  1. theorem OAI.CircleDomainRigidity.abs_sub_le_sum_segments_and_jumps line 18
  2. theorem OAI.CircleDomainRigidity.variation_le_integral_abs_deriv line 48
  3. theorem OAI.CircleDomainRigidity.line_payment_across_finite_gaps line 55