OAI/Analysis/LipschitzHilbert/Estimates/MaximalL2Energy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The p=2 maximal energy argument. A localized weak-L1 estimate, layer cake, and Cauchy--Schwarz give the strong L2 constant four.

  1. theorem OAI.LipschitzHilbert.maximal_square_lintegral line 16
  2. theorem OAI.LipschitzHilbert.maximal_L2_energy line 47