OAI/Probability/SLE/Mass/L2MeanConvergence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Passing expectations through the common L² convex extraction.

  1. lemma OAI.SLEExactGauge.continuous_L2_integral line 13
  2. lemma OAI.SLEExactGauge.weighted_randomVariable_integral_tendsto line 26
  3. lemma OAI.SLEExactGauge.continuous_L2_pairing line 43
  4. lemma OAI.SLEExactGauge.weighted_randomVariable_pairing_tendsto line 56