OAI/Probability/SLEGauge/FlowDerivatives.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.ExactSLEFlow.integral_flow_hasDerivWithinAt line 21
  2. lemma OAI.ExactSLEFlow.integral_flow_unique line 37
  3. theorem OAI.ExactSLEFlow.additive_flow_adapted line 60
  4. theorem OAI.ExactSLEGenerator.exists_adapted_additive_brownian line 93
  5. lemma OAI.ExactSLEGenerator.adapted_intervalIntegral line 134
  6. theorem OAI.ExactSLEGenerator.martingale_compensated_of_weighted line 164
  7. lemma OAI.ExactSLEGenerator.intervalIntegral_nnreal_shift line 230
  8. lemma OAI.ExactSLEGenerator.shift_additive_equation line 248
  9. lemma OAI.ExactSLEGenerator.integrable_intervalIntegral_of_bound line 258
  10. theorem OAI.ExactSLEGenerator.additive_brownian_martingale line 272
  11. def OAI.ExactSLEGenerator.directional line 365
  12. lemma OAI.ExactSLEGenerator.directional_contDiff line 369
  13. lemma OAI.ExactSLEGenerator.directional_compact line 377
  14. lemma OAI.ExactSLEGenerator.iteratedDeriv_line line 384
  15. lemma OAI.ExactSLEGenerator.compact_smooth_fderiv_bound line 396
  16. lemma OAI.ExactSLEGenerator.compact_smooth_line_bound line 411
  17. lemma OAI.ExactSLEGenerator.compact_smooth_test_bounds line 422