OAI/Probability/SLE/Multipoint/MultipointActiveCosts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The raw active costs and their bounds on individual completion intervals. Disjoint active intervals contribute zero pair cost.

  1. def OAI.SLEExactGauge.Multipoint.actualSingleCost line 15
  2. def OAI.SLEExactGauge.Multipoint.actualPairCost line 20
  3. lemma OAI.SLEExactGauge.Multipoint.actualSingleCost_nonneg line 27
  4. lemma OAI.SLEExactGauge.Multipoint.actualPairCost_nonneg line 31
  5. theorem OAI.SLEExactGauge.Multipoint.actualSingleCost_bound line 37
  6. def OAI.SLEExactGauge.Multipoint.overlapStart line 60
  7. def OAI.SLEExactGauge.Multipoint.overlapEnd line 62
  8. theorem OAI.SLEExactGauge.Multipoint.actualPairCost_bound line 64