OAI/Probability/SLEGauge/ModelFiniteTests.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.subdisk_measurable line 21
  2. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.subdisk_raw_measurable line 25
  3. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.subdisk_ge_law line 32
  4. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.subdisk_tail_le line 47
  5. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.normalized_tail_le line 58
  6. lemma OAI.SLEExactGauge.LoewnerGeometry.hasDerivWithinAt_primitive_Icc line 104
  7. def OAI.SLEExactGauge.LoewnerGeometry.logVariation line 122
  8. def OAI.SLEExactGauge.LoewnerGeometry.firstVariation line 125
  9. lemma OAI.SLEExactGauge.LoewnerGeometry.firstVariation_eq_deriv line 128
  10. lemma OAI.SLEExactGauge.LoewnerGeometry.logVariation_hasDerivWithinAt line 133
  11. lemma OAI.SLEExactGauge.LoewnerGeometry.firstVariation_hasDerivWithinAt line 144
  12. lemma OAI.SLEExactGauge.LoewnerGeometry.firstVariation_continuousOn line 151
  13. def OAI.SLEExactGauge.LoewnerGeometry.secondVariationIntegral line 157
  14. lemma OAI.SLEExactGauge.LoewnerGeometry.secondVariationIntegral_hasDerivWithinAt line 161
  15. lemma OAI.SLEExactGauge.LoewnerGeometry.secondVariationIntegral_continuousOn line 174
  16. theorem OAI.SLEExactGauge.LoewnerGeometry.hasDerivAt_deriv_loewnerMap line 181
  17. lemma OAI.SLEExactGauge.LoewnerGeometry.real_inner_mul_self line 303
  18. lemma OAI.SLEExactGauge.LoewnerGeometry.norm_le_of_affine_dissipative line 311
  19. lemma OAI.SLEExactGauge.LoewnerGeometry.loewner_time_hasDerivWithinAt line 363
  20. lemma OAI.SLEExactGauge.LoewnerGeometry.loewner_height_hasDerivWithinAt line 371
  21. def OAI.SLEExactGauge.LoewnerGeometry.coefficientDrift line 383
  22. def OAI.SLEExactGauge.LoewnerGeometry.coefficientForcing line 386
  23. lemma OAI.SLEExactGauge.LoewnerGeometry.coefficientDrift_re line 389
  24. lemma OAI.SLEExactGauge.LoewnerGeometry.coefficientForcing_eq line 400
  25. lemma OAI.SLEExactGauge.LoewnerGeometry.coefficientForcing_norm line 414
  26. def OAI.SLEExactGauge.LoewnerGeometry.secondCoefficient line 423
  27. lemma OAI.SLEExactGauge.LoewnerGeometry.secondCoefficient_hasDerivWithinAt line 427
  28. lemma OAI.SLEExactGauge.LoewnerGeometry.secondCoefficient_zero line 449
  29. theorem OAI.SLEExactGauge.LoewnerGeometry.secondCoefficient_norm_le line 454
  30. lemma OAI.SLEExactGauge.LoewnerGeometry.hasDerivAt_deriv_inverseMap line 490
  31. lemma OAI.SLEExactGauge.LoewnerGeometry.inverseMap_second_coefficient line 511
  32. lemma OAI.SLEExactGauge.LoewnerGeometry.inverseMap_second_coefficient_norm_le line 527
  33. theorem OAI.SLEExactGauge.LoewnerGeometry.inverseMap_preSchwarzian_bound line 534