OAI/Probability/SLEGauge/CenteredSequenceLaw.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.CenteredMoments.centeredMass_raw_measurable_of_le line 18
  2. lemma OAI.SLEExactGauge.CenteredMoments.centered_vector_consistent line 29
  3. theorem OAI.SLEExactGauge.CenteredMoments.exists_centered_sequence_law line 59
  4. def OAI.SLEExactGauge.CenteredMoments.diskSequenceMass line 100
  5. lemma OAI.SLEExactGauge.CenteredMoments.diskSequenceMass_measurable line 102
  6. lemma OAI.SLEExactGauge.CenteredMoments.diskSequenceMass_tendsto line 105
  7. theorem OAI.SLEExactGauge.CenteredMoments.diskSequence_moment line 110
  8. theorem OAI.SLEExactGauge.CenteredMoments.actual_centered_finite_moments line 146
  9. lemma OAI.SLEExactGauge.CenteredMoments.diskMap_norm_lt_one line 234
  10. lemma OAI.SLEExactGauge.CenteredMoments.diskWeight_pos line 244
  11. lemma OAI.SLEExactGauge.CenteredMoments.diskMass_unit_pos line 254
  12. def OAI.SLEExactGauge.CenteredMoments.subdiskMass line 272
  13. lemma OAI.SLEExactGauge.CenteredMoments.subdiskMass_quarter line 276
  14. lemma OAI.SLEExactGauge.CenteredMoments.subdiskMass_measurable line 279
  15. lemma OAI.SLEExactGauge.CenteredMoments.centeredTime_pos line 289
  16. def OAI.SLEExactGauge.CenteredMoments.subdiskRadius line 303
  17. lemma OAI.SLEExactGauge.CenteredMoments.subdiskRadius_pos line 305
  18. lemma OAI.SLEExactGauge.CenteredMoments.subdiskRadius_lt_one line 311
  19. lemma OAI.SLEExactGauge.CenteredMoments.unitBall_eq_iUnion_subdisk line 316
  20. theorem OAI.SLEExactGauge.CenteredMoments.exists_subdisk_positive_mean line 333
  21. lemma OAI.SLEExactGauge.CenteredMoments.cayley_subdisk_bounds line 373
  22. lemma OAI.SLEExactGauge.CenteredMoments.subdisk_region_compact line 405
  23. lemma OAI.SLEExactGauge.CenteredMoments.subdisk_cutoff_exists line 420
  24. def OAI.SLEExactGauge.CenteredMoments.subdiskCutoff line 433
  25. lemma OAI.SLEExactGauge.CenteredMoments.subdiskCutoff_nonneg line 436
  26. lemma OAI.SLEExactGauge.CenteredMoments.subdiskCutoff_le_one line 439
  27. lemma OAI.SLEExactGauge.CenteredMoments.subdiskCutoff_one line 442
  28. lemma OAI.SLEExactGauge.CenteredMoments.subdiskCutoff_support line 445
  29. def OAI.SLEExactGauge.CenteredMoments.subdiskTest line 449
  30. lemma OAI.SLEExactGauge.CenteredMoments.subdiskTest_nonneg line 453
  31. lemma OAI.SLEExactGauge.CenteredMoments.subdiskTest_bound line 458
  32. lemma OAI.SLEExactGauge.CenteredMoments.subdiskTest_support line 467
  33. lemma OAI.SLEExactGauge.CenteredMoments.diskWeight_le_subdiskTest line 476
  34. lemma OAI.SLEExactGauge.CenteredMoments.subdiskMass_le_enorm line 497