OAI/Analysis/LipschitzHilbert/Trees/SourceLpExhaustion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Bounded logarithmic-coefficient exhaustions preserve the uniform Lp estimate. Integrability of the full power is proved by monotone Lebesgue integration, before passing back to the real integral.

  1. def OAI.LipschitzHilbert.sourceExhaustion line 15
  2. theorem OAI.LipschitzHilbert.sourceExhaustion_measurable line 17
  3. theorem OAI.LipschitzHilbert.sourceExhaustion_mono line 21
  4. theorem OAI.LipschitzHilbert.sourceExhaustion_covers line 28
  5. theorem OAI.LipschitzHilbert.source_lp_of_exhaustion line 34