OAI/Probability/SLE/ActualRetainedKernel.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Actual Retained Kernel for chordal SLE.

  1. def OAI.SLEExactGauge.RegularSLEPresentation.sourceFiniteGreenKernel line 17
  2. lemma OAI.SLEExactGauge.RegularSLEPresentation.sourceFiniteGreenDensity_measurable line 21
  3. lemma OAI.SLEExactGauge.RegularSLEPresentation.sourceFiniteGreenKernel_apply line 29
  4. lemma OAI.SLEExactGauge.RegularSLEPresentation.sourceFiniteGreenKernel_univ line 36
  5. lemma OAI.SLEExactGauge.RegularSLEPresentation.sourceFiniteGreenKernel_K line 40
  6. lemma OAI.SLEExactGauge.RegularSLEPresentation.sourceFiniteGreenKernel_supported line 44
  7. lemma OAI.SLEExactGauge.RegularSLEPresentation.sourceFiniteGreenKernel_finite line 48
  8. lemma OAI.SLEExactGauge.RegularSLEPresentation.sourceFiniteGreenKernel_carrier line 88
  9. lemma OAI.SLEExactGauge.source_dyadic_tendsto line 100
  10. lemma OAI.SLEExactGauge.source_dyadic_eventually_le line 103
  11. lemma OAI.SLEExactGauge.retainedMeasure_zero_of_zero line 106
  12. lemma OAI.SLEExactGauge.RegularSLEPresentation.source_actual_retained_experiment line 124
  13. lemma OAI.SLEExactGauge.RegularSLEPresentation.source_actual_retained_pathwise line 174
  14. def OAI.SLEExactGauge.SourceActualRetainedLowerTarget line 219
  15. theorem OAI.SLEExactGauge.sourceActualRetainedLower_proved line 227
  16. lemma OAI.SLEExactGauge.source_gauge_lipschitz_image_le line 258
  17. lemma OAI.SLEExactGauge.source_gauge_lipschitz_null line 309
  18. lemma OAI.SLEExactGauge.source_gauge_holomorphic_compact_null line 326
  19. lemma OAI.SLEExactGauge.source_inverse_chart_gauge_positive line 347
  20. theorem OAI.SLEExactGauge.source_retained_compact_interior_lower_bound line 385
  21. theorem OAI.SLEExactGauge.source_retained_compact_interior_lower_bound_of_frequently line 447
  22. def OAI.SLEExactGauge.SourceRetainedDyadicInteriorTarget line 478
  23. theorem OAI.SLEExactGauge.sourceRetainedDyadicInterior_proved line 491
  24. lemma OAI.SLEExactGauge.RegularSLEPresentation.source_actual_retained_interior_pathwise line 559
  25. def OAI.SLEExactGauge.SourceInteriorRetainedTransferTarget line 604
  26. theorem OAI.SLEExactGauge.sourceInteriorRetainedTransfer_proved line 616
  27. lemma OAI.SLEExactGauge.source_brownian_continuous_law_unique line 656
  28. def OAI.SLEExactGauge.SourceTraceLawUniqueTarget line 681
  29. theorem OAI.SLEExactGauge.sourceTraceLawUnique_proved line 691