OAI/Probability/SLEGauge/PhaseIntegrals.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.ExactSLEPasting.integral_finite_partition line 26
  2. lemma OAI.ExactSLEPasting.integral_le_of_finite_partition line 34
  3. lemma OAI.ExactSLEGreen.clamped_delta_continuous line 48
  4. lemma OAI.ExactSLEGreen.clamped_speed_continuous line 56
  5. lemma OAI.ExactSLEGreen.regimeState_discount_le line 63
  6. def OAI.ExactSLEGreen.pairDiscountConstant line 118
  7. lemma OAI.ExactSLEGreen.pairDiscountConstant_pos line 120
  8. def OAI.ExactSLEGreen.phaseDiscountConstant line 125
  9. lemma OAI.ExactSLEGreen.phaseDiscountConstant_nonneg line 127
  10. lemma OAI.ExactSLEGreen.actual_phase_discount line 143
  11. lemma OAI.ExactSLEGreen.stopped_phaseProduct_measurable line 232
  12. lemma OAI.ExactSLEGreen.actual_phase_expectation_step line 248
  13. lemma OAI.ExactSLEGreen.actualState_zero line 398
  14. lemma OAI.ExactSLEGreen.actual_phaseProduct_initial line 406
  15. lemma OAI.ExactSLEGreen.actual_phaseProduct_completed line 444