OAI/Probability/SLE/RetainedDyadicGeometry.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Retained Dyadic Geometry for chordal SLE.

  1. def OAI.SLEExactGauge.retainedDyadicSquare line 13
  2. def OAI.SLEExactGauge.retainedDyadicAddress line 16
  3. def OAI.SLEExactGauge.retainedCandidates line 18
  4. lemma OAI.SLEExactGauge.retainedSquare_measurable line 22
  5. lemma OAI.SLEExactGauge.retainedSquare_iff_address line 30
  6. lemma OAI.SLEExactGauge.retainedSquare_address line 36
  7. lemma OAI.SLEExactGauge.retainedAddress_mem_candidates line 40
  8. lemma OAI.SLEExactGauge.compact_retained_candidate_radius line 60
  9. lemma OAI.SLEExactGauge.retainedCandidates_cover line 68
  10. lemma OAI.SLEExactGauge.retainedCandidates_card line 75
  11. lemma OAI.SLEExactGauge.retainedCandidates_scale_card line 88
  12. def OAI.SLEExactGauge.sourceDyadicCenter line 109
  13. lemma OAI.SLEExactGauge.source_dyadic_side_eq line 111
  14. lemma OAI.SLEExactGauge.source_dyadic_side_pos line 114
  15. lemma OAI.SLEExactGauge.source_dyadic_side_le line 115
  16. lemma OAI.SLEExactGauge.source_square_subset_ball line 118
  17. lemma OAI.SLEExactGauge.source_square_center_height line 144
  18. lemma OAI.SLEExactGauge.source_small_dyadic_level line 160
  19. lemma OAI.SLEExactGauge.source_finite_mass_le_ball line 189
  20. def OAI.SLEExactGauge.SourceActualSquareTailTarget line 233
  21. theorem OAI.SLEExactGauge.sourceActualSquareTail_proved line 243