OAI/Probability/SLE/Loewner/LinearReverseTrajectory.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Linear drivers and their autonomous centered reverse trajectories. These give concrete steering curves for the geometric support construction.

  1. def OAI.SLEExactGauge.Target.linearDriver line 14
  2. lemma OAI.SLEExactGauge.Target.linearDriver_apply line 17
  3. lemma OAI.SLEExactGauge.Target.linearDriver_value line 20
  4. lemma OAI.SLEExactGauge.Target.linearDriver_derivative line 24
  5. lemma OAI.SLEExactGauge.Target.approximation_height_pos line 30
  6. def OAI.SLEExactGauge.Target.linearReverseBase line 32
  7. lemma OAI.SLEExactGauge.Target.linearReverseBase_spec line 36
  8. def OAI.SLEExactGauge.Target.linearReverseApprox line 46
  9. lemma OAI.SLEExactGauge.Target.linearReverseApprox_derivative line 49
  10. lemma OAI.SLEExactGauge.Target.linearReverseApprox_height line 62
  11. lemma OAI.SLEExactGauge.Target.linearReverseApprox_eq_inverse line 67