OAI/Analysis/LipschitzHilbert/Estimates/PolynomialMomentBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Put the explicit John--Nirenberg moment expression in the polynomial form needed when the moment order grows with the manuscript parameter.

  1. theorem OAI.LipschitzHilbert.polynomial_moment_majorant line 13
  2. theorem OAI.LipschitzHilbert.ennreal_polynomial_moment_majorant line 39
  3. def OAI.LipschitzHilbert.lineMomentBase line 51
  4. theorem OAI.LipschitzHilbert.lineMomentBase_pos line 55
  5. theorem OAI.LipschitzHilbert.line_moment_expression_le line 61