OAI/Probability/SLEGauge/DynkinIdentity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. theorem OAI.ExactSLEGenerator.additive_brownian_dynkin line 20
  2. theorem OAI.ExactSLEGenerator.weighted_dynkin_of_mixed_taylor line 114
  3. theorem OAI.ExactSLEGenerator.additive_brownian_weighted_dynkin line 178
  4. lemma OAI.ExactSLEFlow.stronglyMeasurable_intervalIntegral_of_continuous line 272
  5. lemma OAI.ExactSLEFlow.bounded_forcing_picard line 286
  6. lemma OAI.ExactSLEFlow.picard_iterates_tendsto line 302
  7. theorem OAI.ExactSLEFlow.measurable_additive_flow_on_interval line 325
  8. lemma OAI.ExactSLEFlow.additive_flow_unique line 381
  9. theorem OAI.ExactSLEFlow.measurable_additive_flow line 396