OAI/Analysis/CircleDomains/Modulus/BalloonLinePayment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual smooth balloon cutoffs pay for all unit-speed affine line segments with their indicator densities.

  1. theorem OAI.CircleDomainRigidity.smooth_affine_line_increment line 12
  2. theorem OAI.CircleDomainRigidity.balloon_line_density_intervalIntegrable line 25
  3. theorem OAI.CircleDomainRigidity.balloon_cutoff_line_payment line 39