OAI/Probability/SLELocalization/StoppedMeshes.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Localization estimates.

  1. lemma OAI.SLEExactGauge.physical_clock_bounds line 18
  2. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.finite_clock_bounds line 99
  3. structure OAI.SLEExactGauge.PartitionMeshes.PartitionSequence line 158
  4. lemma OAI.SLEExactGauge.PartitionMeshes.PartitionSequence.nonneg line 199
  5. lemma OAI.SLEExactGauge.PartitionMeshes.PartitionSequence.mem line 202
  6. lemma OAI.SLEExactGauge.PartitionMeshes.PartitionSequence.increments_small line 207
  7. lemma OAI.SLEExactGauge.PartitionMeshes.PartitionSequence.riemann_tendsto line 218
  8. lemma OAI.SLEExactGauge.PartitionMeshes.PartitionSequence.family_remainder_tendsto line 277
  9. def OAI.SLEExactGauge.PartitionMeshes.clippedDyadic line 342
  10. lemma OAI.SLEExactGauge.PartitionMeshes.PartitionSequence.time_increment_tendsto line 392
  11. lemma OAI.SLEExactGauge.StoppedMeshes.one_crossing_sum_bound line 498
  12. lemma OAI.SLEExactGauge.StoppedMeshes.clipped_increment_eq line 526
  13. lemma OAI.SLEExactGauge.StoppedMeshes.clipped_timeSum_difference_tendsto line 534
  14. lemma OAI.SLEExactGauge.StoppedMeshes.clipped_linearSum_difference_tendsto line 559
  15. lemma OAI.SLEExactGauge.StoppedMeshes.abs_sq_sub_sq_le line 599
  16. lemma OAI.SLEExactGauge.StoppedMeshes.clipped_quadraticSum_difference_tendsto line 607
  17. lemma OAI.SLEExactGauge.StoppedMeshes.clipped_mem line 659
  18. lemma OAI.SLEExactGauge.StoppedMeshes.prestop_riemann_tendsto line 665
  19. lemma OAI.SLEExactGauge.PartitionMeshes.PartitionSequence.family_remainder_tendsto_of_eventually_bounded line 715
  20. lemma OAI.SLEExactGauge.StoppedMeshes.clipped_quadratic_eventually_bounded line 777
  21. lemma OAI.SLEExactGauge.BrownianStopped.coefficient_clipped_bound line 826
  22. lemma OAI.SLEExactGauge.BrownianStopped.stopped_field_taylor_limit line 835
  23. def OAI.SLEExactGauge.BrownianStopped.stoppedCoeff line 966
  24. theorem OAI.SLEExactGauge.BrownianStopped.stopped_fieldSum_tendsto line 971
  25. theorem OAI.SLEExactGauge.BrownianStopped.stopped_field_ito_centered line 1035