OAI/Probability/SLE/RetainedSeedMoments.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Retained Seed Moments for chordal SLE.

  1. lemma OAI.SLEExactGauge.source_unit_ball_height line 15
  2. lemma OAI.SLEExactGauge.source_open_closed_ball_ae line 23
  3. lemma OAI.SLEExactGauge.source_finite_mass_le_unit_mass line 34
  4. lemma OAI.SLEExactGauge.source_unit_mesh_second_moment line 58
  5. def OAI.SLEExactGauge.SourceRetainedSeedTarget line 108
  6. theorem OAI.SLEExactGauge.sourceRetainedSeed_proved line 120
  7. lemma OAI.SLEExactGauge.source_first_sphere_free line 147
  8. lemma OAI.SLEExactGauge.source_live_hit_spatial_eq line 158
  9. lemma OAI.SLEExactGauge.source_live_collar_free line 168
  10. lemma OAI.SLEExactGauge.source_enter_implies_live_contact line 178
  11. lemma OAI.SLEExactGauge.source_weight_zero_no_unit_entrance line 195
  12. lemma OAI.SLEExactGauge.source_event_bound_from_past line 222
  13. lemma OAI.SLEExactGauge.source_live_unit_mesh_tail line 238
  14. lemma OAI.SLEExactGauge.source_live_entrance_bound line 285
  15. lemma OAI.SLEExactGauge.source_mesh_tail_to_stretched line 316
  16. def OAI.SLEExactGauge.SourceLiveEntranceTailTarget line 377
  17. theorem OAI.SLEExactGauge.sourceLiveEntranceTail_proved line 387
  18. lemma OAI.SLEExactGauge.source_scaled_radius_hit_iff line 436
  19. lemma OAI.SLEExactGauge.source_scale_spatial_hit line 445
  20. lemma OAI.SLEExactGauge.source_scale_spatial_hit_top line 475
  21. lemma OAI.SLEExactGauge.source_scale_spatial_hit_value line 482
  22. lemma OAI.SLEExactGauge.source_scale_spatial_hit_le line 491
  23. lemma OAI.SLEExactGauge.source_scale_chart_deriv line 501
  24. lemma OAI.SLEExactGauge.source_scale_fullRadius line 512
  25. lemma OAI.SLEExactGauge.source_scale_greenDensity line 523
  26. lemma OAI.SLEExactGauge.source_scale_spatial_greenWeight line 544
  27. def OAI.SLEExactGauge.RegularSLEPresentation.sourceScaled line 569
  28. lemma OAI.SLEExactGauge.source_scale_initialGreen line 589
  29. lemma OAI.SLEExactGauge.source_scale_area_real_integral line 606
  30. lemma OAI.SLEExactGauge.source_scale_spatialRealMass line 631
  31. lemma OAI.SLEExactGauge.source_scale_ball line 647
  32. lemma OAI.SLEExactGauge.RegularSLEPresentation.sourceScaled_mass line 653
  33. lemma OAI.source_tail_threshold_normalize line 670
  34. lemma OAI.SLEExactGauge.source_live_entrance_all_tail line 722
  35. def OAI.SLEExactGauge.SourcePhysicalBallAllTailTarget line 773
  36. theorem OAI.SLEExactGauge.sourcePhysicalBallAllTail_proved line 783