OAI/Probability/SLE/ClippedCoordinates.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Clipped Coordinates for chordal SLE.

  1. lemma OAI.SLEExactGauge.clippedCenter_norm_lower line 13
  2. lemma OAI.SLEExactGauge.clippedCenter_inv_norm_bound line 20
  3. lemma OAI.SLEExactGauge.clippedCenter_dist line 25
  4. lemma OAI.SLEExactGauge.clippedCenter_inv_dist line 55
  5. def OAI.SLEExactGauge.logLoewnerVector line 70
  6. lemma OAI.SLEExactGauge.bounded_normSq_dist line 74
  7. lemma OAI.SLEExactGauge.bounded_sq_dist line 86
  8. lemma OAI.SLEExactGauge.logLoewnerVector_dist line 94
  9. lemma OAI.SLEExactGauge.logLoewnerVector_norm line 127
  10. lemma OAI.SLEExactGauge.clippedLogLoewnerField_bounds line 134
  11. lemma OAI.SLEExactGauge.continuous_clippedLogLoewnerField line 161
  12. theorem OAI.SLEExactGauge.clipped_log_loewner_solution line 173
  13. theorem OAI.SLEExactGauge.exists_measurable_bounded_ode_picard line 202
  14. lemma OAI.SLEExactGauge.picardApprox_congr_on line 267
  15. lemma OAI.SLEExactGauge.measurable_driver_frozen line 284
  16. theorem OAI.SLEExactGauge.clipped_log_loewner_adapted_solution line 302
  17. theorem OAI.SLEExactGauge.exists_measurable_global_bounded_ode_picard line 364
  18. theorem OAI.SLEExactGauge.clipped_log_loewner_global_adapted_solution line 431
  19. def OAI.SLEExactGauge.spatialPartial line 485
  20. lemma OAI.SLEExactGauge.spatialPartial_smooth line 490
  21. lemma OAI.SLEExactGauge.spatialPartial_compact line 498
  22. lemma OAI.SLEExactGauge.spatialPartial_eq_iteratedDeriv line 506
  23. lemma OAI.SLEExactGauge.compact_smooth_bounded_lipschitz line 518
  24. theorem OAI.SLEExactGauge.compact_state_smooth_brownian_field line 535
  25. def OAI.SLEExactGauge.dimension line 658

    Also declared: ComparatorChallenges/SLELowerPositivity.lean:13 (same declaration text).

  26. def OAI.SLEExactGauge.codimension line 659

    Also declared: ComparatorChallenges/SLELowerPositivity.lean:15 (same declaration text).

  27. def OAI.SLEExactGauge.greenExponent line 660
  28. def OAI.SLEExactGauge.greenLogNormSq line 664
  29. def OAI.SLEExactGauge.greenLogDensity line 666
  30. def OAI.SLEExactGauge.physicalLogLoewnerField line 670
  31. lemma OAI.SLEExactGauge.greenLogNormSq_pos line 676
  32. lemma OAI.SLEExactGauge.greenLogDensity_contDiff line 680
  33. lemma OAI.SLEExactGauge.greenLogDensity_spatial_derivative line 695
  34. lemma OAI.SLEExactGauge.greenLogDensity_spatial_second line 712
  35. lemma OAI.SLEExactGauge.greenLogDensity_directional line 745
  36. lemma OAI.SLEExactGauge.physicalLogLoewnerField_components line 788
  37. theorem OAI.SLEExactGauge.green_physical_generator_zero line 823
  38. lemma OAI.SLEExactGauge.greenLogDensity_pair_directional line 854
  39. lemma OAI.SLEExactGauge.exists_compact_green_field line 866
  40. lemma OAI.SLEExactGauge.clippedLogLoewnerField_eq_physical line 893