OAI/Analysis/CircleDomains/Sobolev/BoundedDensityEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Adding a bounded nonnegative penalty preserves finite quadratic energy on a finite measure space, including densities with null-set infinities.

  1. theorem OAI.CircleDomainRigidity.ennreal_add_sq_le line 14
  2. theorem OAI.CircleDomainRigidity.lintegral_add_sq_lt_top_of_bounded line 23