OAI/Probability/SLEGauge/NormalizedDiskMass.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.LoewnerRestart.diskAt_fromDisk line 19
  2. lemma OAI.SLEExactGauge.LoewnerRestart.diskAt_scaled line 27
  3. lemma OAI.SLEExactGauge.LoewnerRestart.diskAt_deriv_norm_scaled line 32
  4. def OAI.SLEExactGauge.LoewnerRestart.pointDiskRegion line 43
  5. def OAI.SLEExactGauge.LoewnerRestart.pointDiskWeight line 45
  6. def OAI.SLEExactGauge.LoewnerRestart.pointDiskMass line 48
  7. lemma OAI.SLEExactGauge.LoewnerRestart.pointDiskRegion_measurable line 51
  8. lemma OAI.SLEExactGauge.LoewnerRestart.pointDiskWeight_measurable line 55
  9. lemma OAI.SLEExactGauge.LoewnerRestart.pointDiskMass_diskMass line 63
  10. lemma OAI.SLEExactGauge.LoewnerRestart.pointDiskMass_smul line 74
  11. lemma OAI.SLEExactGauge.LoewnerRestart.pointDiskMass_map_dilation line 79
  12. lemma OAI.SLEExactGauge.LoewnerRestart.pointDiskMass_recovered_scaled line 109
  13. lemma OAI.SLEExactGauge.LoewnerRestart.normalized_subdiskMass_eq line 123
  14. lemma OAI.SLEExactGauge.LoewnerRestart.inverseUpper_measurableEmbedding line 156
  15. def OAI.SLEExactGauge.LoewnerRestart.spatialDiskRegion line 166
  16. lemma OAI.SLEExactGauge.LoewnerRestart.spatialDiskRegion_measurable line 170
  17. lemma OAI.SLEExactGauge.LoewnerRestart.spatialDiskRegion_subset_alive line 175
  18. lemma OAI.SLEExactGauge.LoewnerRestart.subtype_spatialDiskRegion line 181
  19. lemma OAI.SLEExactGauge.LoewnerRestart.restartPush_spatialDisk line 191
  20. def OAI.SLEExactGauge.LoewnerRestart.diskLower line 202
  21. def OAI.SLEExactGauge.LoewnerRestart.diskUpper line 203
  22. lemma OAI.SLEExactGauge.LoewnerRestart.diskLower_pos line 205
  23. lemma OAI.SLEExactGauge.LoewnerRestart.diskUpper_pos line 209
  24. lemma OAI.SLEExactGauge.LoewnerRestart.restartWeight_disk_bounds line 215
  25. theorem OAI.SLEExactGauge.LoewnerRestart.restartPush_disk_bounds line 251
  26. def OAI.SLEExactGauge.LoewnerRestart.radialDiskRegion line 287
  27. lemma OAI.SLEExactGauge.LoewnerRestart.radialPoint_spatial_radius line 290
  28. lemma OAI.SLEExactGauge.LoewnerRestart.radialDiskRegion_localization line 301
  29. theorem OAI.SLEExactGauge.LoewnerRestart.actual_radial_spatial_bounds line 325
  30. lemma OAI.SLEExactGauge.PastMass.denseRange_nnrat_nnreal line 388
  31. lemma OAI.SLEExactGauge.PastMass.accumulated_continuous line 402
  32. lemma OAI.SLEExactGauge.PastMass.accumulated_zero line 420
  33. lemma OAI.SLEExactGauge.PastMass.exists_rational_threshold line 427
  34. lemma OAI.SLEExactGauge.PastMass.mass_le_twice_strict_past line 447
  35. def OAI.SLEExactGauge.PastMass.rationalTestEnumeration line 482
  36. lemma OAI.SLEExactGauge.PastMass.rationalTestEnumeration_surjective line 484
  37. def OAI.SLEExactGauge.PastMass.rationalPastKernel line 487
  38. lemma OAI.SLEExactGauge.PastMass.TracePalmData.rational_Palm line 497
  39. lemma OAI.SLEExactGauge.PastMass.TracePalmData.rational_kernel_measurable line 506
  40. lemma OAI.SLEExactGauge.PastMass.TracePalmData.expected_bad_mass_le line 513