OAI/Probability/SLELocalization/MeshExponents.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Mesh estimates.

  1. lemma OAI.SLEExactGauge.Mesh.interval_square_bound line 18
  2. theorem OAI.SLEExactGauge.MeshSlab.common_slab_mgf line 66
  3. lemma OAI.SLEExactGauge.FiniteTilt.eventually_physicalValue_at_hit_general line 149
  4. lemma OAI.SLEExactGauge.FiniteTilt.tendsto_physicalValue_killed_general line 178
  5. def OAI.SLEExactGauge.JointStopped.good line 224
  6. lemma OAI.SLEExactGauge.JointStopped.good_height line 228
  7. lemma OAI.SLEExactGauge.JointStopped.good_closed line 240
  8. lemma OAI.SLEExactGauge.JointStopped.good_live line 251
  9. lemma OAI.SLEExactGauge.JointStopped.good_of_live line 266
  10. lemma OAI.SLEExactGauge.JointStopped.log_of_good line 288
  11. lemma OAI.SLEExactGauge.JointStopped.field_good line 321
  12. def OAI.SLEExactGauge.JointStopped.killedGreen line 337
  13. def OAI.SLEExactGauge.JointStopped.greenApprox line 342
  14. lemma OAI.SLEExactGauge.JointStopped.measurable_greenApprox line 348
  15. lemma OAI.SLEExactGauge.JointStopped.eventually_greenApprox line 354
  16. def OAI.SLEExactGauge.JointStopped.observedGreen line 373
  17. lemma OAI.SLEExactGauge.JointStopped.measurable_observedGreen line 376
  18. lemma OAI.SLEExactGauge.JointStopped.observedGreen_eq line 380
  19. def OAI.SLEExactGauge.JointStopped.observedPhysical line 407
  20. lemma OAI.SLEExactGauge.JointStopped.measurable_observedPhysical line 412
  21. lemma OAI.SLEExactGauge.JointStopped.observedPhysical_eq line 423
  22. def OAI.SLEExactGauge.ContinuousDriver.complexParts line 464
  23. lemma OAI.SLEExactGauge.ContinuousDriver.continuous_complexParts line 469
  24. def OAI.SLEExactGauge.ContinuousDriver.complexPath line 474
  25. lemma OAI.SLEExactGauge.ContinuousDriver.complexPath_eval line 477
  26. lemma OAI.SLEExactGauge.ContinuousDriver.aemeasurable_complexPath line 483
  27. lemma OAI.SLEExactGauge.ContinuousDriver.exists_measurable_trace_path line 490
  28. theorem OAI.SLEExactGauge.jointFiniteTimePhysicalDensity line 521
  29. theorem OAI.SLEExactGauge.jointPhysicalDensity line 566
  30. lemma OAI.SLEExactGauge.MeshSlab.physicalStoppedDensity_ne_top line 614
  31. lemma OAI.SLEExactGauge.MeshSlab.physicalValue_real_tendsto line 619
  32. lemma OAI.SLEExactGauge.MeshSlab.exponential_bound_of_ae_tendsto line 635
  33. lemma OAI.SLEExactGauge.MeshSlab.common_slab_limit line 656
  34. lemma OAI.SLEExactGauge.FiniteTilt.compact_log_cutoffs line 713
  35. lemma OAI.SLEExactGauge.FiniteTilt.logRadius_pos line 730
  36. lemma OAI.SLEExactGauge.FiniteTilt.logRadius_eq line 733
  37. lemma OAI.SLEExactGauge.FiniteTilt.collar_height line 738
  38. theorem OAI.SLEExactGauge.MeshSlab.physical_slab_mgf line 772
  39. lemma OAI.SLEExactGauge.MeshSlab.physicalDensity_bound line 825
  40. def OAI.SLEExactGauge.MeshSlab.physicalMass line 854
  41. lemma OAI.SLEExactGauge.MeshSlab.physicalMass_nonneg line 858
  42. lemma OAI.SLEExactGauge.MeshSlab.physicalMass_aemeasurable line 882
  43. lemma OAI.SLEExactGauge.MeshSlab.physicalDensity_integrable line 889
  44. lemma OAI.SLEExactGauge.MeshSlab.physicalMass_lintegral line 904
  45. lemma OAI.SLEExactGauge.MeshSlab.physicalMass_bound line 914
  46. lemma OAI.SLEExactGauge.MeshSlab.slab_radius_scale line 935
  47. theorem OAI.SLEExactGauge.MeshSlab.slab_mass_mgf line 941
  48. lemma OAI.SLEExactGauge.MeshSlab.finite_mgf_sum line 1017
  49. lemma OAI.SLEExactGauge.MeshSlab.geo_radius_power line 1071