OAI/Probability/SLE/Mass/MassUniquenessSeparation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A bounded smooth test detecting a nonzero continuous finite-variation martingale. Its bounded derivatives permit an integrable-variation argument.

  1. def OAI.SLEExactGauge.massSeparationTest line 17
  2. def OAI.SLEExactGauge.massSeparationSlope line 18
  3. theorem OAI.SLEExactGauge.massSeparationTest_nonneg line 20
  4. theorem OAI.SLEExactGauge.massSeparationTest_zero line 24
  5. theorem OAI.SLEExactGauge.massSeparationTest_eq_zero line 27
  6. theorem OAI.SLEExactGauge.massSeparationTest_hasDerivAt line 31
  7. theorem OAI.SLEExactGauge.massSeparationSlope_hasDerivAt line 41
  8. theorem OAI.SLEExactGauge.massSeparationSlope_abs_le line 52
  9. theorem OAI.SLEExactGauge.massSeparationSlope_deriv_abs_le line 62
  10. theorem OAI.SLEExactGauge.massSeparationTest_lipschitz line 75
  11. theorem OAI.SLEExactGauge.massSeparationSlope_lipschitz line 84
  12. theorem OAI.SLEExactGauge.massSeparationTest_remainder_le line 93
  13. theorem OAI.SLEExactGauge.massSeparationTest_remainder_linear line 112