OAI/Probability/SLELocalization/CommonClocks.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Finite Tilt estimates.

  1. structure OAI.SLEExactGauge.FiniteTilt.CommonCutoff line 18
  2. def OAI.SLEExactGauge.FiniteTilt.CommonCutoff.at line 29
  3. lemma OAI.SLEExactGauge.FiniteTilt.commonCutoffs line 41
  4. lemma OAI.SLEExactGauge.LoewnerCutoff.solution_mark_dist_le line 102
  5. lemma OAI.SLEExactGauge.LoewnerCutoff.solutionPath_joint_lipschitz line 138
  6. lemma OAI.SLEExactGauge.LoewnerCutoff.continuous_mark_position line 156
  7. lemma OAI.SLEExactGauge.LoewnerCutoff.continuous_mark_variation line 161
  8. lemma OAI.SLEExactGauge.LoewnerCutoff.continuous_mark_logDerivative line 169
  9. lemma OAI.SLEExactGauge.LoewnerCutoff.continuous_mark_green line 177
  10. lemma OAI.SLEExactGauge.LoewnerCutoff.continuous_mark_field line 205
  11. lemma OAI.SLEExactGauge.LoewnerCutoff.continuous_mark_first line 217
  12. lemma OAI.SLEExactGauge.LoewnerCutoff.continuous_mark_deficit line 231
  13. lemma OAI.SLEExactGauge.LoewnerCutoff.continuous_mark_exitPath line 246
  14. lemma OAI.SLEExactGauge.LoewnerCutoff.measurable_mark_stop line 252
  15. lemma OAI.SLEExactGauge.LoewnerCutoff.isOpen_mark_positive_on line 256
  16. lemma OAI.SLEExactGauge.LoewnerCutoff.measurable_mark_coeffAt line 275
  17. lemma OAI.SLEExactGauge.PhysicalPast.joint_avoids_measurable_past line 297
  18. lemma OAI.SLEExactGauge.LoewnerLocalized.joint_rawCoeff_measurable_past line 329
  19. lemma OAI.SLEExactGauge.PhysicalPast.joint_avoids_nullMeasurable line 358
  20. lemma OAI.SLEExactGauge.LoewnerLocalized.joint_rawCoeff_aemeasurable line 386
  21. def OAI.SLEExactGauge.MeshSlab.coeff line 415
  22. lemma OAI.SLEExactGauge.MeshSlab.coeff_measurable_past line 420
  23. lemma OAI.SLEExactGauge.MeshSlab.coeff_aemeasurable line 427
  24. lemma OAI.SLEExactGauge.MeshSlab.coeff_uniform_bound line 435
  25. def OAI.SLEExactGauge.CompactHit.hits line 474
  26. def OAI.SLEExactGauge.CompactHit.time line 476
  27. lemma OAI.SLEExactGauge.CompactHit.hits_closed line 478
  28. lemma OAI.SLEExactGauge.CompactHit.time_mem line 488
  29. lemma OAI.SLEExactGauge.CompactHit.time_le line 492
  30. lemma OAI.SLEExactGauge.CompactHit.before line 495
  31. lemma OAI.SLEExactGauge.CompactHit.time_eq_one_of_not_hits line 500
  32. lemma OAI.SLEExactGauge.CompactHit.time_le_iff line 508
  33. lemma OAI.SLEExactGauge.CompactHit.measurable_time line 520
  34. def OAI.SLEExactGauge.CompactHit.realTime line 562
  35. lemma OAI.SLEExactGauge.CompactHit.realTime_bounds line 564
  36. lemma OAI.SLEExactGauge.CompactHit.realTime_le line 569
  37. lemma OAI.SLEExactGauge.CompactHit.realTime_hits line 579
  38. lemma OAI.SLEExactGauge.CompactHit.realTime_stop line 588
  39. lemma OAI.SLEExactGauge.CompactHit.live_byTime_iff line 609
  40. lemma OAI.SLEExactGauge.CompactHit.cap_eq_realTime line 626
  41. lemma OAI.SLEExactGauge.CompactHit.realTime_antitone line 661
  42. def OAI.SLEExactGauge.MeshSlab.observedTime line 686
  43. lemma OAI.SLEExactGauge.MeshSlab.measurable_observedTime line 690
  44. def OAI.SLEExactGauge.MeshSlab.observedValue line 701
  45. lemma OAI.SLEExactGauge.MeshSlab.measurable_observedValue line 706
  46. lemma OAI.SLEExactGauge.MeshSlab.coeff_common line 716
  47. lemma OAI.SLEExactGauge.MeshSlab.observedValue_eq line 723
  48. def OAI.SLEExactGauge.Mesh.slab line 768
  49. lemma OAI.SLEExactGauge.Mesh.prestop_product line 771
  50. lemma OAI.SLEExactGauge.Mesh.slab_product line 777
  51. lemma OAI.SLEExactGauge.Mesh.slab_riemann_tendsto line 788
  52. lemma OAI.SLEExactGauge.Mesh.integral_prestop line 806
  53. lemma OAI.SLEExactGauge.Mesh.prestop_intervalIntegrable line 817
  54. lemma OAI.SLEExactGauge.Mesh.slab_product_integral line 825
  55. lemma OAI.SLEExactGauge.Mesh.slab_riemann_tendsto_integral line 844
  56. lemma OAI.SLEExactGauge.Mesh.slab_eq_zero_of_not_mem line 867
  57. lemma OAI.SLEExactGauge.Mesh.slab_abs_le line 875
  58. lemma OAI.SLEExactGauge.Mesh.measurable_slab line 884
  59. lemma OAI.SLEExactGauge.MeshSlab.observedTime_bounds line 907
  60. lemma OAI.SLEExactGauge.MeshSlab.observedTime_antitone line 913
  61. lemma OAI.SLEExactGauge.MeshSlab.observedTime_eq line 918
  62. lemma OAI.SLEExactGauge.MeshSlab.observedTime_approach line 936
  63. lemma OAI.SLEExactGauge.Mesh.coefficient_le_poisson line 966
  64. lemma OAI.SLEExactGauge.Layer.hessian_scalar_comp line 999
  65. lemma OAI.SLEExactGauge.Layer.laplacian_scalar_comp line 1023
  66. def OAI.SLEExactGauge.Layer.diskFactor line 1044
  67. lemma OAI.SLEExactGauge.Layer.diskFactor_pos line 1046
  68. lemma OAI.SLEExactGauge.Layer.diskFactor_smooth line 1050
  69. lemma OAI.SLEExactGauge.Layer.diskFactor_fderiv line 1053
  70. lemma OAI.SLEExactGauge.Layer.diskFactor_hessian line 1057
  71. lemma OAI.SLEExactGauge.Layer.diskFactor_gradient line 1063
  72. lemma OAI.SLEExactGauge.Layer.diskFactor_laplacian line 1069
  73. lemma OAI.SLEExactGauge.Layer.logFactor_smooth line 1074