OAI/Probability/SLELocalization/BoundaryDiffusion.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Boundary Green estimates.

  1. lemma OAI.SLEExactGauge.BoundaryGreen.deterministic_budget line 19
  2. def OAI.SLEExactGauge.Swallowing.coeffAt line 84
  3. lemma OAI.SLEExactGauge.Swallowing.coeffAt_measurable line 90
  4. def OAI.SLEExactGauge.Swallowing.rawCoeff line 105
  5. lemma OAI.SLEExactGauge.Swallowing.rawCoeff_measurable_past line 109
  6. lemma OAI.SLEExactGauge.Swallowing.rawCoeff_aemeasurable line 123
  7. lemma OAI.SLEExactGauge.Swallowing.rawCoeff_eq line 137
  8. lemma OAI.SLEExactGauge.Swallowing.rawCoeff_stoppedCoeff_ae line 160
  9. theorem OAI.SLEExactGauge.Swallowing.localized_centered line 171
  10. abbrev OAI.SLEExactGauge.Swallowing.correction line 248
  11. def OAI.SLEExactGauge.Swallowing.budget line 258
  12. lemma OAI.SLEExactGauge.Swallowing.field_initial line 263
  13. lemma OAI.SLEExactGauge.Swallowing.generator_field line 268
  14. lemma OAI.SLEExactGauge.Swallowing.deterministic_budget line 284
  15. lemma OAI.SLEExactGauge.Swallowing.budget_mean line 352
  16. lemma OAI.SLEExactGauge.Swallowing.measure_eventually_budget line 414
  17. abbrev OAI.SLEExactGauge.BoundaryGreen.correction line 456
  18. def OAI.SLEExactGauge.BoundaryGreen.budget line 466
  19. lemma OAI.SLEExactGauge.BoundaryGreen.budget_nonneg line 470
  20. lemma OAI.SLEExactGauge.BoundaryGreen.budget_mean line 474
  21. def OAI.SLEExactGauge.BoundaryGreen.reach line 501
  22. lemma OAI.SLEExactGauge.BoundaryGreen.reached_terminal line 504
  23. lemma OAI.SLEExactGauge.BoundaryGreen.budget_dominates_reach line 525
  24. theorem OAI.SLEExactGauge.BoundaryGreen.maximal_bound line 550
  25. lemma OAI.SLEExactGauge.BoundaryFunctional.continuous_position_time line 575
  26. lemma OAI.SLEExactGauge.BoundaryFunctional.continuous_logDerivative_time line 582
  27. lemma OAI.SLEExactGauge.BoundaryGreen.continuous_gap_time line 601
  28. lemma OAI.SLEExactGauge.BoundaryGreen.norm_sum_lower line 621
  29. lemma OAI.SLEExactGauge.BoundaryGreen.ratio_real_lower line 628
  30. lemma OAI.SLEExactGauge.BoundaryGreen.normSq_slope line 644
  31. lemma OAI.SLEExactGauge.BoundaryGreen.energy_deriv line 659
  32. lemma OAI.SLEExactGauge.BoundaryGreen.energy_antitone line 677
  33. lemma OAI.SLEExactGauge.BoundaryGreen.gap_coefficients line 704
  34. lemma OAI.SLEExactGauge.BoundaryGreen.gap_difference_deriv line 721
  35. lemma OAI.SLEExactGauge.BoundaryGreen.ratio_energy line 739
  36. lemma OAI.SLEExactGauge.BoundaryGreen.energy_weight_bound line 784
  37. lemma OAI.SLEExactGauge.BoundaryGreen.first_zero_of_nonpos line 844
  38. lemma OAI.SLEExactGauge.BoundaryGreen.first_zero_of_nonpos_on line 874
  39. lemma OAI.SLEExactGauge.BoundaryGreen.tip_forces_reach line 903
  40. lemma OAI.SLEExactGauge.BoundaryGreen.inverse_tip_point line 986
  41. def OAI.SLEExactGauge.ReverseLoewner.velocity line 1016
  42. lemma OAI.SLEExactGauge.ReverseLoewner.velocity_lipschitz line 1018