OAI/Probability/SLEGauge/MarkedMomentBound.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.ExactSLEGreen.target_cap_cancellation line 18
  2. theorem OAI.ExactSLEGreen.actual_hit_density_product_bound line 42
  3. theorem OAI.ExactSLEGreen.actual_hit_mass_moment_bound line 137
  4. lemma OAI.ExactSLEGreen.convex_limit_moment_bound line 288
  5. theorem OAI.ExactSLEGreen.actual_hit_radon_moment_bound line 329
  6. def OAI.SLEExactGauge.KernelSimilarity.affine line 397
  7. lemma OAI.SLEExactGauge.KernelSimilarity.affine_apply line 401
  8. lemma OAI.SLEExactGauge.KernelSimilarity.dist_affine line 404
  9. lemma OAI.SLEExactGauge.KernelSimilarity.cappedDistance_affine line 409
  10. lemma OAI.SLEExactGauge.KernelSimilarity.kernel_affine line 426
  11. lemma OAI.SLEExactGauge.KernelSimilarity.pi_const_smul line 436
  12. lemma OAI.SLEExactGauge.KernelSimilarity.affine_area line 444
  13. lemma OAI.SLEExactGauge.KernelSimilarity.affine_pi_integral line 464
  14. theorem OAI.SLEExactGauge.KernelSimilarity.fixed_center_integral_affine line 482