OAI/Probability/SLE/SimpleFields.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Simple Fields for chordal SLE.

  1. lemma OAI.SLEExactGauge.stoppedDyadicIndex_bounds line 50
  2. lemma OAI.SLEExactGauge.stoppedDyadicIndex_tendsto line 63
  3. lemma OAI.SLEExactGauge.stopping_before_measurable line 77
  4. lemma OAI.SLEExactGauge.stopped_coefficient_measurable line 83
  5. lemma OAI.SLEExactGauge.prefix_mask_sum line 100
  6. def OAI.SLEExactGauge.stoppedFieldSum line 112
  7. lemma OAI.SLEExactGauge.stoppedFieldSum_eq_prefix line 118
  8. theorem OAI.SLEExactGauge.stopped_fieldSum_tendsto line 131
  9. theorem OAI.SLEExactGauge.ClippedLogSolution.compact_stopped_field_ito line 252
  10. lemma OAI.SLEExactGauge.deriv_fiber_fderiv line 298
  11. def OAI.SLEExactGauge.greenLogCoefficient line 309
  12. theorem OAI.SLEExactGauge.ClippedLogSolution.stopped_green_ito line 315
  13. lemma OAI.SLEExactGauge.stopped_energy_tendsto line 392
  14. lemma OAI.SLEExactGauge.gaussian_exponential_lintegral line 426
  15. lemma OAI.SLEExactGauge.gaussian_compensated_exponential line 434
  16. lemma OAI.SLEExactGauge.independent_gaussian_exponential line 450
  17. def OAI.SLEExactGauge.driverPredictableSum line 480
  18. def OAI.SLEExactGauge.driverPredictableEnergy line 484
  19. lemma OAI.SLEExactGauge.driverPredictableSum_measurable_past line 488
  20. lemma OAI.SLEExactGauge.driverPredictableEnergy_measurable_past line 502
  21. theorem OAI.SLEExactGauge.driverPredictable_exponential line 515
  22. lemma OAI.SLEExactGauge.greenLogCoefficient_eq_deriv line 577
  23. lemma OAI.SLEExactGauge.greenLogCoefficient_continuous line 581
  24. lemma OAI.SLEExactGauge.ClippedLogSolution.green_coefficient_adapted line 594
  25. theorem OAI.SLEExactGauge.ClippedLogSolution.stopped_green_exponential line 604
  26. lemma OAI.SLEExactGauge.clipped_family_initial_continuous line 662
  27. lemma OAI.SLEExactGauge.clipped_family_past_measurable line 683
  28. lemma OAI.SLEExactGauge.clipped_family_joint_measurable line 693