OAI/Probability/SLE/Gauge/SerpentineMarkedReflection.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Reflection of the concrete experiment and its actual narrow-prefix certificate. It reduces a marked point on the left to the right-hand layout.

  1. lemma OAI.SLEExactGauge.Serpentine.fitX_mirror line 16
  2. lemma OAI.SLEExactGauge.Serpentine.fitY_mirror line 19
  3. lemma OAI.SLEExactGauge.Serpentine.fitChart_mirror line 22
  4. lemma OAI.SLEExactGauge.Serpentine.physicalFitChart_mirror line 26
  5. lemma OAI.SLEExactGauge.Serpentine.fitEntry_mirror line 30
  6. lemma OAI.SLEExactGauge.Serpentine.fitCompletion_mirror line 34
  7. lemma OAI.SLEExactGauge.Serpentine.fitTerminalX_mirror line 38
  8. lemma OAI.SLEExactGauge.Serpentine.fitTerminalHeight_mirror line 41
  9. lemma OAI.SLEExactGauge.Serpentine.fitHighTime_mirror line 45
  10. lemma OAI.SLEExactGauge.Serpentine.physicalExperimentChart_negative line 49
  11. lemma OAI.SLEExactGauge.Serpentine.experimentChart_negative line 55
  12. lemma OAI.SLEExactGauge.Serpentine.ribbonCore_reflected_iff line 60
  13. lemma OAI.SLEExactGauge.Serpentine.goodRibbonPrefix_reflected line 74
  14. lemma OAI.SLEExactGauge.Serpentine.goodRibbonPrefix_physical_negative line 88
  15. lemma OAI.SLEExactGauge.Serpentine.physicalExperimentChart_reflect_point line 96
  16. def OAI.SLEExactGauge.Serpentine.mirroredProgress line 103
  17. lemma OAI.SLEExactGauge.Serpentine.mirroredProgress_trace line 106
  18. lemma OAI.SLEExactGauge.Serpentine.mirroredProgress_chart line 110
  19. lemma OAI.SLEExactGauge.Serpentine.mirroredProgress_firstFrontTime line 118