OAI/Probability/SLE/StoppedFields.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Stopped Fields for chordal SLE.

  1. lemma OAI.SLEExactGauge.boundedSpatialHit_antitone_radius line 55
  2. lemma OAI.SLEExactGauge.RegularSLEPresentation.joint_spatialHit_stopping line 68
  3. lemma OAI.SLEExactGauge.RegularSLEPresentation.joint_boundedSpatialHit_stopping line 82
  4. lemma OAI.SLEExactGauge.clipped_spatial_window_coefficient_le line 97
  5. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.spatial_masked_bracket_bound line 135
  6. lemma OAI.SLEExactGauge.clipped_family_uniform_bound line 167
  7. theorem OAI.SLEExactGauge.spatial_angular_cutoff line 197
  8. structure OAI.SLEExactGauge.SpatialAngularFamily line 320
  9. def OAI.SLEExactGauge.SpatialAngularFamily.section line 345
  10. lemma OAI.SLEExactGauge.exists_spatial_angular_family line 363
  11. lemma OAI.SLEExactGauge.clipped_area_window_measurable line 416
  12. lemma OAI.SLEExactGauge.spatial_stopping_lift line 480
  13. theorem OAI.SLEExactGauge.exists_common_brownian_compact_stops line 489
  14. theorem OAI.SLEExactGauge.clipped_spatial_green_window_unbounded_driver line 530
  15. lemma OAI.SLEExactGauge.interval_square_energy_bound line 633
  16. def OAI.SLEExactGauge.slabVariance line 655
  17. lemma OAI.SLEExactGauge.slabVariance_nonneg line 659
  18. lemma OAI.SLEExactGauge.ofReal_slabVariance line 662
  19. theorem OAI.SLEExactGauge.RegularSLEPresentation.localized_spatial_slab_exponential line 676