OAI/Probability/SLEGauge/NormalizedMarkedMoment.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.KernelSimilarity.pi_restrict_mono line 18
  2. lemma OAI.SLEExactGauge.KernelSimilarity.normalization_cancel line 24
  3. lemma OAI.SLEExactGauge.KernelSimilarity.affine_im_real line 53
  4. theorem OAI.SLEExactGauge.KernelSimilarity.actual_normalized_hit_moment_bound line 59
  5. lemma OAI.SLEExactGauge.CenteredMoments.radialWeight_measurable line 170
  6. lemma OAI.SLEExactGauge.CenteredMoments.radialLaw_lintegral_le_hit line 178
  7. lemma OAI.SLEExactGauge.CenteredMoments.center_affine line 212
  8. lemma OAI.SLEExactGauge.CenteredMoments.tilt_cancel line 218
  9. theorem OAI.SLEExactGauge.CenteredMoments.actual_normalized_tilted_moment_bound line 231
  10. def OAI.SLEExactGauge.CenteredMoments.upperAffine line 285
  11. lemma OAI.SLEExactGauge.CenteredMoments.upperAffine_apply line 298
  12. def OAI.SLEExactGauge.CenteredMoments.normalizedTest line 302
  13. lemma OAI.SLEExactGauge.CenteredMoments.normalizedTest_support line 307
  14. lemma OAI.SLEExactGauge.CenteredMoments.normalizedTest_nonneg line 317
  15. lemma OAI.SLEExactGauge.CenteredMoments.normalizedTest_bound line 321
  16. lemma OAI.SLEExactGauge.CenteredMoments.disk_negative_endpoint line 328
  17. lemma OAI.SLEExactGauge.CenteredMoments.disk_denominator_ne line 335
  18. lemma OAI.SLEExactGauge.CenteredMoments.diskMap_affine line 345
  19. lemma OAI.SLEExactGauge.CenteredMoments.disk_deriv line 356
  20. lemma OAI.SLEExactGauge.CenteredMoments.disk_deriv_bound line 369
  21. lemma OAI.SLEExactGauge.CenteredMoments.cayley_inner line 384
  22. lemma OAI.SLEExactGauge.CenteredMoments.disk_preimage_inner line 404
  23. lemma OAI.SLEExactGauge.CenteredMoments.height_of_ball line 429
  24. lemma OAI.SLEExactGauge.CenteredMoments.upper_inner_compact line 435
  25. lemma OAI.SLEExactGauge.CenteredMoments.cutoff_exists line 448
  26. def OAI.SLEExactGauge.CenteredMoments.diskCutoff line 460
  27. lemma OAI.SLEExactGauge.CenteredMoments.diskCutoff_nonneg line 462
  28. lemma OAI.SLEExactGauge.CenteredMoments.diskCutoff_le_one line 464
  29. lemma OAI.SLEExactGauge.CenteredMoments.diskCutoff_one line 466
  30. lemma OAI.SLEExactGauge.CenteredMoments.diskCutoff_support line 468
  31. def OAI.SLEExactGauge.CenteredMoments.diskWeight line 473
  32. def OAI.SLEExactGauge.CenteredMoments.diskMass line 475
  33. lemma OAI.SLEExactGauge.CenteredMoments.diskMap_measurable line 478
  34. lemma OAI.SLEExactGauge.CenteredMoments.diskWeight_measurable line 482
  35. lemma OAI.SLEExactGauge.CenteredMoments.dimension_pos line 490
  36. def OAI.SLEExactGauge.CenteredMoments.diskTest line 497
  37. lemma OAI.SLEExactGauge.CenteredMoments.diskTest_nonneg line 501
  38. lemma OAI.SLEExactGauge.CenteredMoments.diskTest_bound line 506
  39. lemma OAI.SLEExactGauge.CenteredMoments.diskTest_support line 514
  40. lemma OAI.SLEExactGauge.CenteredMoments.diskWeight_le_diskTest line 522
  41. lemma OAI.SLEExactGauge.CenteredMoments.diskMass_inner_le_test line 537