OAI/Probability/SLE/Multipoint/MultipointActualPhases.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The three actual radius stops and their phase identities along the constructed localized state.

  1. def OAI.SLEExactGauge.Multipoint.factorRadiusLevel line 16
  2. lemma OAI.SLEExactGauge.Multipoint.factorRadiusLevel_nonneg line 19
  3. lemma OAI.SLEExactGauge.Multipoint.factorRadiusLevel_monotone line 23
  4. def OAI.SLEExactGauge.Multipoint.actualFactorStops line 28
  5. def OAI.SLEExactGauge.Multipoint.factorSwitchList line 34
  6. lemma OAI.SLEExactGauge.Multipoint.factorSwitchList_zero line 38
  7. lemma OAI.SLEExactGauge.Multipoint.factorSwitchList_mem line 42
  8. lemma OAI.SLEExactGauge.Multipoint.factorSwitchList_forall line 46
  9. theorem OAI.SLEExactGauge.Multipoint.actualFactorStops_regular line 55
  10. lemma OAI.SLEExactGauge.Multipoint.LocalizedState.actual_at line 80
  11. theorem OAI.SLEExactGauge.Multipoint.actual_phase_regulator line 91
  12. theorem OAI.SLEExactGauge.Multipoint.actual_phase_switch_clock line 135