OAI/Probability/SLELocalization/SlabMoments.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Mesh estimates.

  1. lemma OAI.SLEExactGauge.Mesh.asynchronous_bracket_bound_active line 18
  2. lemma OAI.SLEExactGauge.MeshSlab.measurable_halfPlaneGreen line 72
  3. lemma OAI.SLEExactGauge.MeshSlab.observed_bracket line 76
  4. lemma OAI.SLEExactGauge.BrownianPredictable.gaussian_exp_compensated line 181
  5. lemma OAI.SLEExactGauge.BrownianPredictable.past_exp_step line 198
  6. def OAI.SLEExactGauge.BrownianPredictable.exponentialLogSum line 225
  7. lemma OAI.SLEExactGauge.BrownianPredictable.exponentialLogSum_past line 230
  8. lemma OAI.SLEExactGauge.BrownianPredictable.exponentialLogSum_aemeasurable line 242
  9. lemma OAI.SLEExactGauge.BrownianPredictable.exponentialLogSum_identity line 252
  10. def OAI.SLEExactGauge.BrownianPredictable.dyadicVariance line 282
  11. lemma OAI.SLEExactGauge.BrownianPredictable.exponentialLogSum_dyadic line 286
  12. theorem OAI.SLEExactGauge.BrownianPredictable.limit_exponential_bound line 296
  13. lemma OAI.SLEExactGauge.BrownianPredictable.tail_of_exponential_bound line 345
  14. lemma OAI.SLEExactGauge.Mesh.spatial_variance_tendsto line 384
  15. lemma OAI.SLEExactGauge.Mesh.spatial_dyadicVariance_tendsto line 455
  16. def OAI.SLEExactGauge.MeshSlab.slabCoeff line 494
  17. def OAI.SLEExactGauge.MeshSlab.pathFirst line 498
  18. def OAI.SLEExactGauge.MeshSlab.pathSlab line 502
  19. lemma OAI.SLEExactGauge.MeshSlab.continuous_pathFirst line 507
  20. lemma OAI.SLEExactGauge.MeshSlab.measurable_pathSlab line 516
  21. lemma OAI.SLEExactGauge.MeshSlab.pathSlab_uniform_bound line 523
  22. lemma OAI.SLEExactGauge.MeshSlab.slabCoeff_eq line 538
  23. lemma OAI.SLEExactGauge.MeshSlab.slabCoeff_variance_tendsto line 559
  24. lemma OAI.SLEExactGauge.SpatialLimit.uniformIntegrable_one_of_eLpNorm_two_bounded line 609
  25. lemma OAI.SLEExactGauge.SpatialLimit.L1_tendsto_of_square_bound line 657
  26. lemma OAI.SLEExactGauge.SpatialLimit.integrate_L1_le line 675
  27. lemma OAI.SLEExactGauge.SpatialLimit.spatial_L1_limit line 692
  28. lemma OAI.SLEExactGauge.SpatialLimit.memLp_two_prod_of_fiber_bound line 723
  29. lemma OAI.SLEExactGauge.SpatialLimit.ae_prod_tendsto_of_fibers line 746
  30. theorem OAI.SLEExactGauge.BrownianPredictable.limit_exponential_bound_subseq line 785
  31. lemma OAI.SLEExactGauge.SpatialLimit.dyadicDriverSum_integrate line 847
  32. theorem OAI.SLEExactGauge.SpatialLimit.spatial_exponential_bound line 861
  33. lemma OAI.SLEExactGauge.SpatialLimit.sums_aemeasurable line 899
  34. lemma OAI.SLEExactGauge.SpatialLimit.bounded_sums line 911
  35. def OAI.SLEExactGauge.MeshSlab.observedDifference line 962
  36. lemma OAI.SLEExactGauge.MeshSlab.observedDifference_aemeasurable line 967
  37. lemma OAI.SLEExactGauge.MeshSlab.slab_sum_tendsto line 980