OAI/Probability/SLE/WindowPropagation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Window Propagation for chordal SLE.

  1. lemma OAI.SLEExactGauge.geometric_over_quartic_ge_linear line 15
  2. lemma OAI.SLEExactGauge.all_levels_exceptional_sum line 42
  3. lemma OAI.SLEExactGauge.reciprocal_square_partial_sum_strong line 74
  4. lemma OAI.SLEExactGauge.reciprocal_square_partial_sum_le_two line 92
  5. lemma OAI.SLEExactGauge.discrete_gronwall_exp line 101
  6. lemma OAI.SLEExactGauge.two_recurrences_normalized line 135
  7. lemma OAI.SLEExactGauge.window_recurrences_uniform line 171
  8. def OAI.SLEExactGauge.SourceWindowPropagationTarget line 229
  9. theorem OAI.SLEExactGauge.sourceWindowPropagation line 246
  10. lemma OAI.SLEExactGauge.source_mesh_finite_measure_propagation line 286
  11. lemma OAI.SLEExactGauge.source_mesh_uniform_past_tail line 339
  12. lemma OAI.SLEExactGauge.source_conditional_indicator_bound_on line 421
  13. def OAI.SLEExactGauge.SourcePhysicalMeshTailTarget line 459
  14. theorem OAI.SLEExactGauge.sourcePhysicalMeshTail_proved line 474
  15. lemma OAI.SLEExactGauge.source_indicator_integral_tail line 548
  16. lemma OAI.SLEExactGauge.source_initial_unit_mesh_tail line 562
  17. lemma OAI.SLEExactGauge.source_mesh_tail_to_linear line 591
  18. lemma OAI.SLEExactGauge.source_linear_tail_all line 649
  19. lemma OAI.SLEExactGauge.source_exponential_second_moment line 682