OAI/Probability/SLE/Gauge/LocalAffinePassage.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Affine transport uses the progress coordinate only on the successful physical envelope. This avoids imposing any condition on the arbitrary off-image values of coordinateInverse.

  1. theorem OAI.SLEExactGauge.frontSuccess_mass_eq_of_eqOn line 18
  2. def OAI.SLEExactGauge.affineInverse line 44
  3. theorem OAI.SLEExactGauge.affineInverse_left line 46
  4. theorem OAI.SLEExactGauge.frontSuccess_mass_probability_affine_local line 51
  5. theorem OAI.SLEExactGauge.longitudinalCoordinate_affine_on_image line 80