OAI/Probability/SLELocalization/ConditionalTilts.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Brownian Predictable estimates.

  1. lemma OAI.SLEExactGauge.BrownianPredictable.indicator_difference_centered line 20
  2. def OAI.SLEExactGauge.GammaTwoRadius.coeffAt line 95
  3. lemma OAI.SLEExactGauge.GammaTwoRadius.coeffAt_measurable line 101
  4. def OAI.SLEExactGauge.GammaTwoRadius.rawCoeff line 116
  5. lemma OAI.SLEExactGauge.GammaTwoRadius.rawCoeff_measurable_past line 120
  6. lemma OAI.SLEExactGauge.GammaTwoRadius.rawCoeff_aemeasurable line 134
  7. lemma OAI.SLEExactGauge.GammaTwoRadius.rawCoeff_eq line 148
  8. lemma OAI.SLEExactGauge.GammaTwoRadius.rawCoeff_stoppedCoeff_ae line 171
  9. lemma OAI.SLEExactGauge.LoewnerExit.stop_antitone_radius line 195
  10. def OAI.SLEExactGauge.FiniteTilt.Cutoff.retarget line 221
  11. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.retarget_stop_le line 237
  12. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.retarget_has_hit_of_lt line 243
  13. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.stopTime_zero line 271
  14. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.value_zero line 282
  15. lemma OAI.SLEExactGauge.BrownianLocal.LocalRegular.mono line 303
  16. def OAI.SLEExactGauge.FiniteTilt.Cutoff.targetField line 327
  17. def OAI.SLEExactGauge.FiniteTilt.Cutoff.targetDrift line 331
  18. def OAI.SLEExactGauge.FiniteTilt.Cutoff.targetCoeff line 335
  19. def OAI.SLEExactGauge.FiniteTilt.Cutoff.targetRemainder line 339
  20. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.targetCoeff_eq line 346
  21. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.targetCoeff_measurable line 354
  22. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.targetCoeff_aemeasurable line 364
  23. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.targetCoeff_bound line 374
  24. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.target_sum_tendsto line 401
  25. lemma OAI.SLEExactGauge.GammaField.integral_drift_nonpos_from line 458
  26. def OAI.SLEExactGauge.FiniteTilt.Cutoff.targetValue line 502
  27. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.targetValue_nonneg line 507
  28. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.targetValue_aemeasurable line 516
  29. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.target_difference_le_remainder line 541
  30. lemma OAI.SLEExactGauge.AngularBarrier.value_decay_from line 585
  31. theorem OAI.SLEExactGauge.radiusApproachBoundFrom line 637
  32. def OAI.SLEExactGauge.finiteCenteredMeasure line 671
  33. def OAI.SLEExactGauge.radiusStoppedInverseAngle line 678
  34. lemma OAI.SLEExactGauge.finiteStoppedDensity_aemeasurable line 684
  35. lemma OAI.SLEExactGauge.finiteStoppedDensity_lt_top line 704
  36. lemma OAI.SLEExactGauge.localizationInitialGreen_pos line 709
  37. lemma OAI.SLEExactGauge.finiteCenteredMeasure_probability line 714
  38. lemma OAI.SLEExactGauge.finiteStoppedDensity_mul_inverseAngle line 732
  39. lemma OAI.SLEExactGauge.radius_green_cancel line 768
  40. theorem OAI.SLEExactGauge.finiteCenteredInverseAngleBound line 782
  41. lemma OAI.SLEExactGauge.GammaField.profile_green_bound line 862
  42. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.height_radius_at_stop line 919
  43. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.targetValue_bound line 934