OAI/Analysis/CircleDomains/Modulus/FilledScalarNormBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform norm bounds for the actual bounded scalar fillings and their two L² differential components.

  1. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.HoleFilling.filled_norm_bound line 20
  2. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.eventually_filled_partial_norm_bounds line 31