OAI/Combinatorics/EditApproximation/Geometry/Bands.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Predicted-band geometry

The prefix-cost predictor is 1-Lipschitz, while its velocity has a strict margin below one. This gives narrow bands without a convexity assumption on the set of allowed endpoints (Sections 5 and 6 of the manuscript).

  1. def OAI.EditApproximation.inPredictedBand line 15
  2. theorem OAI.EditApproximation.predicted_band_diameter line 18
  3. theorem OAI.EditApproximation.comparison_prefix_prediction_error line 42

    Source documentation

    The comparison prefix error is the weighted deviation plus two warmup-mass discrepancy charges.

    theorem comparison_prefix_prediction_error
    {point origin velocity predictedVelocity prefixMass prefixCost totalMass discrepancy deviation : ℝ}
    (hprefix : 0 ≤ prefixMass) (hprefixTotal : prefixMass ≤ totalMass)
    (hprediction : |velocity - predictedVelocity| * totalMass ≤ discrepancy)
    (hvelocity : |predictedVelocity| ≤ 1)
    (hcostLower : prefixMass - discrepancy ≤ prefixCost)
    (hcostUpper : prefixCost ≤ prefixMass)
    (hdeviation : |point - origin - velocity * prefixMass| ≤ deviation) :
    |point - origin - predictedVelocity * prefixCost| ≤ deviation + 2 * discrepancy := by
…