OAI/Probability/SLEGauge/EulerFlow.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. def OAI.SLEExactGauge.Euler.interpolate line 20
  2. lemma OAI.SLEExactGauge.Euler.finite_gronwall line 25
  3. lemma OAI.SLEExactGauge.Euler.nodes_error line 60
  4. lemma OAI.SLEExactGauge.Euler.residual_bound line 95
  5. lemma OAI.SLEExactGauge.Euler.exists_residual_bound line 114
  6. lemma OAI.SLEExactGauge.Euler.norm_interpolate_sub_le line 131
  7. lemma OAI.SLEExactGauge.Euler.interpolate_error line 146
  8. lemma OAI.SLEExactGauge.Euler.converge line 186
  9. lemma OAI.SLEExactGauge.Euler.converge_uniformOn line 230
  10. lemma OAI.SLEExactGauge.LiteralTrace.continuous_driverValue line 280
  11. lemma OAI.SLEExactGauge.LiteralTrace.mesh_pos line 283
  12. lemma OAI.SLEExactGauge.LiteralTrace.mesh_tendsto_zero line 285
  13. lemma OAI.SLEExactGauge.LiteralTrace.cutoffField_eq line 292
  14. lemma OAI.SLEExactGauge.LiteralTrace.eulerSteps_eq_nodes line 300
  15. lemma OAI.SLEExactGauge.LiteralTrace.eulerFlow_eq_interpolate line 307
  16. theorem OAI.SLEExactGauge.LiteralTrace.cutoffFlow_solution line 314
  17. def OAI.SLEExactGauge.LiteralTrace.PositiveSolution line 358
  18. lemma OAI.SLEExactGauge.LiteralTrace.cutoffField_of_height line 363
  19. lemma OAI.SLEExactGauge.LiteralTrace.cutoffFlow_continuous line 385
  20. lemma OAI.SLEExactGauge.LiteralTrace.cutoff_solution_unique line 389
  21. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.cutoff_eq line 413
  22. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.exists_cutoff line 422
  23. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.unique line 433