OAI/Analysis/LipschitzHilbert/Estimates/SquareMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Passing a local square bound to a local mean bound.

  1. theorem OAI.LipschitzHilbert.integral_le_of_square_mean_bound line 12