OAI/Probability/SLEGauge/EulerMoments.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.EulerGeneral.interpolate_at_node line 30
  2. lemma OAI.SLEExactGauge.EulerGeneral.nodes_converge_moving line 37
  3. lemma OAI.SLEExactGauge.BrownianCalculus.frozenNodes_eq_min line 62
  4. lemma OAI.SLEExactGauge.EulerGeneral.ceil_mesh_times_converge line 88
  5. lemma OAI.SLEExactGauge.EulerGeneral.effective_stop_times_converge line 102
  6. lemma OAI.SLEExactGauge.BrownianCalculus.ordinary_nodes_eventually_inside line 118
  7. theorem OAI.SLEExactGauge.BrownianCalculus.frozen_nodes_path_limit line 155
  8. theorem OAI.SLEExactGauge.BrownianCalculus.expected_stopped_smooth line 218
  9. def OAI.SLEExactGauge.BrownianCalculus.driverJets line 271
  10. lemma OAI.SLEExactGauge.BrownianCalculus.driverJets_smooth line 276
  11. lemma OAI.SLEExactGauge.BrownianCalculus.driverJets_compact line 284
  12. lemma OAI.SLEExactGauge.BrownianCalculus.driverJets_restriction line 291
  13. theorem OAI.SLEExactGauge.BrownianCalculus.exists_smoothTest_of_compact line 307
  14. theorem OAI.SLEExactGauge.Localization.compact_extension line 388