OAI/Analysis/LipschitzHilbert/Estimates/RelativeExitEnergy.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Summable quadratic energies of the relative sampled martingales.

  1. def OAI.LipschitzHilbert.relativeExitEnergy line 14
  2. theorem OAI.LipschitzHilbert.relativeExitEnergy_nonneg line 18
  3. theorem OAI.LipschitzHilbert.relativeExitEnergy_bound line 21
  4. theorem OAI.LipschitzHilbert.relativeExitScale_summable line 42
  5. theorem OAI.LipschitzHilbert.relativeExitScale_tsum line 45
  6. theorem OAI.LipschitzHilbert.relativeExitEnergy_summable line 50
  7. def OAI.LipschitzHilbert.weightedRelativeExitEnergy line 57
  8. theorem OAI.LipschitzHilbert.weightedRelativeExitEnergy_nonneg line 60
  9. theorem OAI.LipschitzHilbert.weightedRelativeExitEnergy_bound line 64
  10. theorem OAI.LipschitzHilbert.relativeExitEnergy_measurable line 77
  11. theorem OAI.LipschitzHilbert.relativeExitEnergy_integrable line 88
  12. theorem OAI.LipschitzHilbert.relativeExitEnergy_integral_le line 100
  13. theorem OAI.LipschitzHilbert.weightedRelativeExitEnergy_measurable line 130
  14. theorem OAI.LipschitzHilbert.weightedRelativeExitEnergy_integrable line 135
  15. theorem OAI.LipschitzHilbert.weightedRelativeExitEnergy_integral_le line 146