OAI/Analysis/LipschitzHilbert/Estimates/RawBMOMoments.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uncentered interval moments from the proved John--Nirenberg estimate and a bound for the interval mean.

  1. theorem OAI.LipschitzHilbert.FiniteLineGrid.continuous_raw_moment line 14