OAI/Probability/SLE/KernelConsistency.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Kernel Consistency for chordal SLE.

  1. lemma OAI.SLEExactGauge.halfPlaneGreen_derivative line 15
  2. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.green_kernel_derivative line 42
  3. lemma OAI.SLEExactGauge.diskToHalfPlane_halfPlaneToDisk line 74
  4. lemma OAI.SLEExactGauge.halfPlaneGreen_eq_disk line 85
  5. lemma OAI.SLEExactGauge.halfPlaneGreen_nonneg line 95
  6. lemma OAI.SLEExactGauge.halfplane_boundary_layer_green_le line 102
  7. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.boundary_layer_green line 132
  8. def OAI.SLEExactGauge.chartPoissonRate line 161
  9. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.poissonRate_continuousOn line 166
  10. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.poissonRate_nonneg line 178
  11. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.green_pair_integral line 183
  12. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.green_pair_bound line 220
  13. lemma OAI.SLEExactGauge.lintegral_lower_interval_le line 244
  14. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.live_green_pair_bound line 283
  15. def OAI.SLEExactGauge.greenBrownianCoefficient line 337
  16. lemma OAI.SLEExactGauge.greenExponent_ge_one line 344
  17. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.green_coefficient_le_poisson line 352
  18. lemma OAI.SLEExactGauge.surviving_frontier_distance_le_past line 404
  19. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.radius_ge_of_no_trace_approach line 422
  20. def OAI.SLEExactGauge.AngularLocalization.physicalWeight line 446
  21. lemma OAI.SLEExactGauge.AngularLocalization.physicalWeight_bound line 450
  22. lemma OAI.SLEExactGauge.AngularLocalization.physicalWeight_adapted line 457
  23. lemma OAI.SLEExactGauge.AngularLocalization.physicalWeight_integrable line 475
  24. theorem OAI.SLEExactGauge.AngularLocalization.physicalWeight_martingale line 488
  25. lemma OAI.SLEExactGauge.AngularLocalization.stopping_le_of_hit line 558
  26. lemma OAI.SLEExactGauge.AngularLocalization.power_stopped_measurable line 568
  27. lemma OAI.SLEExactGauge.AngularLocalization.radiusKernel_terminal line 584
  28. lemma OAI.SLEExactGauge.localization_le_radiusStop line 603
  29. lemma OAI.SLEExactGauge.localizedRadiusStop_mono line 613
  30. lemma OAI.SLEExactGauge.limitRadiusKernel_terminal_measurable line 629
  31. def OAI.SLEExactGauge.radiusFiltration line 652