OAI/Analysis/CircleDomains/Modulus/DistinguishedStokesBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The singular terminal is absent from the Stokes boundary sum. Restrict both the finite terminal norm and the original countable band budget to its complement before applying Cauchy--Schwarz.

  1. theorem OAI.CircleDomainRigidity.sum_off_distinguished line 15
  2. theorem OAI.CircleDomainRigidity.sum_off_distinguished_le line 20
  3. theorem OAI.CircleDomainRigidity.circle_stokes_bound_off_distinguished line 27