OAI/Probability/SLE/GreenCovariance.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Green Covariance for chordal SLE.

  1. lemma OAI.SLEExactGauge.SpatialAngularFamily.physicalWeight_joint_measurable line 60
  2. lemma OAI.SLEExactGauge.SpatialAngularFamily.physicalWeight_uniform_bound line 74
  3. lemma OAI.SLEExactGauge.spatial_angular_weight_integral_tendsto line 87
  4. theorem OAI.SLEExactGauge.RegularSLEPresentation.spatial_slab_finite_exponential_of_localizations line 139
  5. lemma OAI.SLEExactGauge.logAngleSq_initial line 207
  6. lemma OAI.SLEExactGauge.initial_spatial_bounds line 220
  7. lemma OAI.SLEExactGauge.exists_uniform_radius_level line 249
  8. theorem OAI.SLEExactGauge.RegularSLEPresentation.spatial_slab_finite_exponential line 269
  9. lemma OAI.SLEExactGauge.RegularSLEPresentation.boundedSpatialGreen_measurable line 341
  10. theorem OAI.SLEExactGauge.RegularSLEPresentation.spatialGreen_tendsto_and_bound_of_level line 356
  11. theorem OAI.SLEExactGauge.RegularSLEPresentation.spatialGreen_ae_spatial_limit line 405
  12. theorem OAI.SLEExactGauge.RegularSLEPresentation.spatial_slab_area_tendsto line 453
  13. def OAI.SLEExactGauge.spatialSlabIncrement line 493
  14. lemma OAI.SLEExactGauge.RegularSLEPresentation.spatialSlabIncrement_measurable line 501
  15. theorem OAI.SLEExactGauge.RegularSLEPresentation.spatial_slab_terminal_exponential line 508
  16. theorem OAI.SLEExactGauge.RegularSLEPresentation.spatial_slab_terminal_tail line 540
  17. lemma OAI.SLEExactGauge.hasSubgaussianMGF_of_compensated line 588
  18. lemma OAI.SLEExactGauge.HasSubgaussianMGF.mono_parameter line 612
  19. lemma OAI.SLEExactGauge.subgaussian_sum_amplitudes line 621
  20. def OAI.SLEExactGauge.slabAmplitude line 641
  21. lemma OAI.SLEExactGauge.slabAmplitude_nonneg line 645
  22. lemma OAI.SLEExactGauge.slabVariance_real_formula line 648
  23. lemma OAI.SLEExactGauge.slabVariance_scale line 656
  24. lemma OAI.SLEExactGauge.slabVariance_scale_le line 669
  25. lemma OAI.SLEExactGauge.RegularSLEPresentation.spatialRealMass_sub_eq_slab line 695