OAI/Probability/SLEGauge/FrozenExpectations.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.BrownianCalculus.expected_frozen_nodes line 28
  2. theorem OAI.SLEExactGauge.BrownianCalculus.expected_frozen_limit line 63
  3. def OAI.SLEExactGauge.EulerGeneral.nodes line 124
  4. def OAI.SLEExactGauge.EulerGeneral.interpolate line 128
  5. lemma OAI.SLEExactGauge.EulerGeneral.finite_gronwall line 133
  6. lemma OAI.SLEExactGauge.EulerGeneral.nodes_error line 169
  7. lemma OAI.SLEExactGauge.EulerGeneral.residual_bound line 205
  8. lemma OAI.SLEExactGauge.EulerGeneral.exists_residual_bound line 225
  9. lemma OAI.SLEExactGauge.EulerGeneral.norm_interpolate_sub_le line 243
  10. lemma OAI.SLEExactGauge.EulerGeneral.interpolate_error line 259
  11. lemma OAI.SLEExactGauge.EulerGeneral.converge line 300
  12. lemma OAI.SLEExactGauge.EulerGeneral.converge_uniformOn line 345
  13. lemma OAI.SLEExactGauge.EulerGeneral.norm_nodes_sub_interpolate line 397
  14. lemma OAI.SLEExactGauge.EulerGeneral.nodes_converge line 420
  15. lemma OAI.SLEExactGauge.EulerGeneral.mesh_times_converge line 437