OAI/Probability/SLEGauge/RiemannIntegrals.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.ExactSLEGenerator.riemann_sum_tendsto line 16
  2. lemma OAI.ExactSLEGenerator.riemann_sum_bound line 44
  3. lemma OAI.ExactSLEGenerator.expected_riemann_sum_tendsto line 66
  4. lemma OAI.ExactSLEGenerator.stieltjes_riemann_error_le line 93
  5. lemma OAI.ExactSLEGenerator.stieltjes_sum_tendsto line 159
  6. lemma OAI.ExactSLEGenerator.stieltjes_sum_bound line 198
  7. lemma OAI.ExactSLEGenerator.expected_stieltjes_sum_tendsto line 241
  8. theorem OAI.ExactSLEGenerator.dynkin_of_mixed_taylor line 276
  9. lemma OAI.ExactSLEGenerator.stronglyMeasurable_intervalIntegral_of_continuous line 382