OAI/Probability/SLE/StochasticIntegrals.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Stochastic Integrals for chordal SLE.

  1. def OAI.SLEExactGauge.spatialLaterKernel line 36
  2. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.spatial_later_kernel_integral line 45
  3. lemma OAI.SLEExactGauge.slab_product_zero_of_not_live_at_start line 74
  4. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.slab_pair_ordered line 87
  5. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.slab_pair_kernel_bound line 122
  6. lemma OAI.SLEExactGauge.spatialHitTime_measurable_point line 147
  7. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.joint_live_measurable line 153
  8. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.killed_chart_measurable line 161
  9. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.spatial_later_kernel_measurable line 171
  10. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.spatial_later_kernel_double line 230
  11. lemma OAI.SLEExactGauge.sym_pair_lintegral line 241
  12. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.spatial_pair_lintegral_le line 258
  13. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.spatial_slab_pair_area_bound line 276
  14. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.killed_green_measurable line 301
  15. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.green_coefficient_measurable line 318
  16. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.spatial_slab_coefficient_measurable line 333
  17. lemma OAI.SLEExactGauge.area_square_tonelli line 362
  18. lemma OAI.SLEExactGauge.spatial_integral_square_le line 388
  19. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.spatial_slab_absolute_bracket_bound line 409
  20. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.spatial_slab_bracket_bound line 434
  21. lemma OAI.SLEExactGauge.BrownianPredictable.gaussian_fourth_moment line 458
  22. lemma OAI.SLEExactGauge.BrownianPredictable.gaussian_second_moment line 497
  23. lemma OAI.SLEExactGauge.BrownianPredictable.gaussian_square_memLp line 502
  24. lemma OAI.SLEExactGauge.BrownianPredictable.gaussian_square_variance line 512
  25. lemma OAI.SLEExactGauge.BrownianPredictable.increment_hasLaw line 523
  26. lemma OAI.SLEExactGauge.BrownianPredictable.increment_square_memLp line 530
  27. lemma OAI.SLEExactGauge.BrownianPredictable.increment_square_integral line 537
  28. lemma OAI.SLEExactGauge.BrownianPredictable.increment_square_variance line 546
  29. abbrev OAI.SLEExactGauge.BrownianPredictable.pastSigma line 559
  30. lemma OAI.SLEExactGauge.BrownianPredictable.brownian_indep_of_past_measurable line 562
  31. lemma OAI.SLEExactGauge.BrownianPredictable.pastSigma_mono line 573
  32. lemma OAI.SLEExactGauge.BrownianPredictable.past_measurable_eval line 583
  33. lemma OAI.SLEExactGauge.BrownianPredictable.past_mul_feature_integral line 588
  34. lemma OAI.SLEExactGauge.BrownianPredictable.independent_product_memLp_two line 606
  35. def OAI.SLEExactGauge.BrownianPredictable.predictableFeatureSum line 617
  36. lemma OAI.SLEExactGauge.BrownianPredictable.predictableTerm_memLp_two line 621
  37. lemma OAI.SLEExactGauge.BrownianPredictable.predictableTerm_integral line 636
  38. lemma OAI.SLEExactGauge.BrownianPredictable.predictableTerm_past_measurable line 647
  39. lemma OAI.SLEExactGauge.BrownianPredictable.predictableTerm_covariance_zero line 658