OAI/Probability/SLELocalization/AngularMoments.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Angular Barrier estimates.

  1. lemma OAI.SLEExactGauge.AngularBarrier.value_decay line 18
  2. def OAI.SLEExactGauge.AngularBarrier.squaredSine line 57
  3. def OAI.SLEExactGauge.AngularBarrier.profile line 59
  4. def OAI.SLEExactGauge.AngularBarrier.profileT line 61
  5. def OAI.SLEExactGauge.AngularBarrier.profileW line 63
  6. def OAI.SLEExactGauge.AngularBarrier.profileWW line 65
  7. lemma OAI.SLEExactGauge.AngularBarrier.squaredSine_pos line 68
  8. lemma OAI.SLEExactGauge.AngularBarrier.squaredSine_le_one line 70
  9. lemma OAI.SLEExactGauge.AngularBarrier.hasDerivAt_squaredSine line 73
  10. lemma OAI.SLEExactGauge.AngularBarrier.contDiff_squaredSine line 78
  11. lemma OAI.SLEExactGauge.AngularBarrier.contDiffAt_profile line 82
  12. lemma OAI.SLEExactGauge.AngularBarrier.hasDerivAt_profile_w line 92
  13. lemma OAI.SLEExactGauge.AngularBarrier.hasDerivAt_profile_t line 98
  14. lemma OAI.SLEExactGauge.AngularBarrier.deriv_squaredSine_hasDerivAt line 102
  15. lemma OAI.SLEExactGauge.AngularBarrier.hasDerivAt_profileW line 111
  16. lemma OAI.SLEExactGauge.AngularBarrier.deriv_profile line 120
  17. lemma OAI.SLEExactGauge.AngularBarrier.second_profile line 123
  18. lemma OAI.SLEExactGauge.AngularBarrier.parameter_deriv_smooth line 128
  19. lemma OAI.SLEExactGauge.AngularBarrier.parameter_iteratedDeriv_smooth line 138
  20. lemma OAI.SLEExactGauge.AngularBarrier.profile_derivative_continuousAt line 147
  21. lemma OAI.SLEExactGauge.AngularBarrier.profile_super line 153
  22. lemma OAI.SLEExactGauge.AngularBarrier.hasDerivAt_value_path line 167
  23. lemma OAI.SLEExactGauge.AngularBarrier.hasDerivAt_profile_path line 184
  24. lemma OAI.SLEExactGauge.AngularBarrier.profile_smooth line 195
  25. lemma OAI.SLEExactGauge.AngularBarrier.iteratedDeriv_affine line 203
  26. structure OAI.SLEExactGauge.BrownianLocal.LocalRegular line 233
  27. lemma OAI.SLEExactGauge.BrownianLocal.family_remainder_tendsto_of_eventually_bounded line 241
  28. lemma OAI.SLEExactGauge.BrownianLocal.stopped_field_taylor_limit line 276
  29. theorem OAI.SLEExactGauge.BrownianLocal.stopped_fieldSum_tendsto_ae line 386
  30. theorem OAI.SLEExactGauge.BrownianLocal.stopped_field_ito_centered_ae line 461
  31. lemma OAI.SLEExactGauge.AngularBarrier.profileT_continuousAt line 508
  32. def OAI.SLEExactGauge.GammaField.rawRemaining line 537
  33. def OAI.SLEExactGauge.GammaField.remaining line 540
  34. def OAI.SLEExactGauge.GammaField.angleRatio line 543
  35. def OAI.SLEExactGauge.GammaField.field line 546
  36. def OAI.SLEExactGauge.GammaField.drift line 549
  37. lemma OAI.SLEExactGauge.GammaField.remaining_pos line 557
  38. lemma OAI.SLEExactGauge.GammaField.continuous_height line 560
  39. lemma OAI.SLEExactGauge.GammaField.continuous_rawRemaining line 564
  40. lemma OAI.SLEExactGauge.GammaField.continuous_remaining line 570
  41. lemma OAI.SLEExactGauge.GammaField.continuous_angleRatio line 574
  42. lemma OAI.SLEExactGauge.GammaField.smooth line 581
  43. lemma OAI.SLEExactGauge.GammaField.iteratedDeriv_eq line 588
  44. lemma OAI.SLEExactGauge.GammaField.continuous_derivative line 601
  45. lemma OAI.SLEExactGauge.GammaField.continuous_field line 613
  46. lemma OAI.SLEExactGauge.GammaField.continuous_drift line 618
  47. lemma OAI.SLEExactGauge.GammaField.rawRemaining_eq line 641
  48. lemma OAI.SLEExactGauge.GammaField.rawRemaining_gt line 649
  49. lemma OAI.SLEExactGauge.GammaField.time_deriv line 656
  50. lemma OAI.SLEExactGauge.GammaField.field_prefix_eq line 692
  51. lemma OAI.SLEExactGauge.GammaField.regular line 702
  52. lemma OAI.SLEExactGauge.GammaField.coefficient_bound line 728
  53. lemma OAI.SLEExactGauge.GammaField.physical_algebra line 752
  54. lemma OAI.SLEExactGauge.GammaField.drift_nonpos line 761
  55. def OAI.SLEExactGauge.GammaPredictable.coeffAt line 808
  56. lemma OAI.SLEExactGauge.GammaPredictable.coeffAt_measurable line 814
  57. def OAI.SLEExactGauge.GammaPredictable.rawCoeff line 829
  58. lemma OAI.SLEExactGauge.GammaPredictable.rawCoeff_measurable_past line 833
  59. lemma OAI.SLEExactGauge.GammaPredictable.rawCoeff_aemeasurable line 847
  60. lemma OAI.SLEExactGauge.GammaPredictable.rawCoeff_eq line 861
  61. lemma OAI.SLEExactGauge.GammaPredictable.rawCoeff_stoppedCoeff_ae line 884
  62. lemma OAI.SLEExactGauge.GammaField.ratio_bound line 909