OAI/Probability/SLE/Mass/SignedMeasureConvergence.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Small analytic passages used for the conditional mass kernel.

  1. theorem OAI.SLEExactGauge.integral_tendsto_of_lintegral_pos_neg line 16
  2. theorem OAI.SLEExactGauge.real_convex_tail_tendsto line 32
  3. lemma OAI.SLEExactGauge.integral_indicator_one_mul line 56
  4. theorem OAI.SLEExactGauge.setIntegral_tendsto_of_L2_pairings line 67
  5. theorem OAI.SLEExactGauge.mean_test_tendsto_of_L2_pairings line 79