OAI/Probability/SLEGauge/RadialFactors.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.ExactSLEFiniteTilt.regFactor_hasDerivAt line 24
  2. lemma OAI.ExactSLEFiniteTilt.sineDerivative_hasDerivAt line 32
  3. lemma OAI.ExactSLEFiniteTilt.regFactor_secondDeriv line 41
  4. lemma OAI.ExactSLEFiniteTilt.regFactor_generator line 54
  5. lemma OAI.ExactSLEFiniteTilt.sinePower_mul_cot_sq line 64
  6. lemma OAI.ExactSLEFiniteTilt.regFactor_exact_drift line 71
  7. lemma OAI.ExactSLEFiniteTilt.regFactor_bounds line 94
  8. lemma OAI.ExactSLEFiniteTilt.regDrift_bound line 114
  9. lemma OAI.ExactSLEFiniteTilt.regFactor_derivative_simple line 164
  10. lemma OAI.ExactSLEFiniteTilt.regFactor_interpolation line 186
  11. lemma OAI.ExactSLEFiniteTilt.regDerivative_bound line 211
  12. theorem OAI.ExactSLEFiniteTilt.regularized_factor_estimates line 226
  13. def OAI.ExactSLEGreen.physicalDelta line 242
  14. def OAI.ExactSLEGreen.physicalRegularized line 244
  15. lemma OAI.ExactSLEGreen.clockExp_shift line 246
  16. lemma OAI.ExactSLEGreen.physicalRegularized_decomposition line 252
  17. lemma OAI.ExactSLEGreen.physicalRegularized_smooth line 261
  18. lemma OAI.ExactSLEGreen.physicalRegularized_L line 272
  19. lemma OAI.ExactSLEGreen.physicalRegularized_N line 296
  20. theorem OAI.ExactSLEGreen.actual_regularized_factor line 320
  21. lemma OAI.ExactSLEFiniteTilt.weighted_pair_young line 360
  22. def OAI.ExactSLEFiniteTilt.regC2 line 395
  23. def OAI.ExactSLEFiniteTilt.regYoungC line 396
  24. lemma OAI.ExactSLEFiniteTilt.regC2_pos line 400
  25. theorem OAI.ExactSLEFiniteTilt.regularized_pair_absorption line 407