OAI/Analysis/CircleDomains/Sobolev/SquareAverageBounded.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Integrable fields have finite centered-square maximal averages almost everywhere.

  1. lemma OAI.CircleDomainRigidity.abs_squareAverage_le_global_integral line 13
  2. lemma OAI.CircleDomainRigidity.ae_squareAverage_bounded line 23