OAI/Analysis/CircleDomains/Modulus/DisjointBallPayments.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Cauchy--Schwarz for finitely many disjoint payment regions inside balloons. Only their containing ball areas enter the estimate.

  1. theorem OAI.CircleDomainRigidity.integral_sq_le_measure_mul_energy line 13
  2. theorem OAI.CircleDomainRigidity.sum_disjoint_ball_payments_sq_le line 22