OAI/Combinatorics/EditApproximation/Geometry/BandEnvelopes.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.rationalMaximum_le line 22
2. theorem OAI.EditApproximation.le_rationalMaximum_member line 30
3. theorem OAI.EditApproximation.rationalDyadicCeiling_bounds line 41
4. theorem OAI.EditApproximation.bandChildEnvelope_lower line 56

   Source documentation

   Zero is a harmless duplicated fallback under the initial table lower invariant. The positive b/M floor ensures that the ceiling input is positive.

   theorem bandChildEnvelope_lower {ny M : ℕ} (b : ℕ)
       (band : List (Fin M → TargetInterval ny))
       (initial : Fin M → TargetInterval ny → ℚ) (i : Fin M) :
       (b : ℚ) / M ≤ bandChildEnvelope b band initial i ∧
         ∀ action ∈ band, initial i (action i) ≤ bandChildEnvelope b band initial i := by
   …

   Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.bandChildEnvelope

5. theorem OAI.EditApproximation.bandChildEnvelope_upper line 70

   Source documentation

   Every finite envelope is bounded using the actual computed-band endpoint diameter and the initial table's spatial inequality.

   theorem bandChildEnvelope_upper {nx ny M : ℕ} (parent : TargetInterval nx)
       (r : TargetInterval ny) (b P : ℕ) (hb : 0 < b) (hM : 0 < M)
       (tau theta velocity : ℚ) (htau : 0 < tau) (htheta : 0 ≤ theta)
       (child initial : Fin M → TargetInterval ny → ℚ)
       (comparison : Fin M → TargetInterval ny)
       (hcomparison : comparison ∈ computedBandActions parent r b P tau theta velocity child)
       (L0 : ℚ) (hL0 : 0 ≤ L0)
       (hinitial : ∀ i, 0 ≤ initial i (comparison i))
       (hspatial : ∀ i s t, initial i s ≤ initial i t + L0 * targetEndpointDistance s t)
       (i : Fin M) :
       bandChildEnvelope b (computedBandActions parent r b P tau theta velocity child) initial i ≤
         2 * ((b : ℚ) / M) + 2 * initial i (comparison i) + 8 * L0 * theta * b / M := by
   …

   Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.computedBandActions, OAI.EditApproximation.targetEndpointDistance, OAI.EditApproximation.bandChildEnvelope

6. theorem OAI.EditApproximation.bandChildEnvelope_sum_guard line 113

   Source documentation

   The actual sum guard follows from the concrete envelopes, the initial cone bounds at the comparison child states, and their actual edit costs.

   theorem bandChildEnvelope_sum_guard {α : Type*} (source target : List α)
       {M : ℕ} (parent : TargetInterval source.length) (r : TargetInterval target.length)
       (b P : ℕ) (hb : 0 < b) (hM : 0 < M)
       (tau theta velocity : ℚ) (htau : 0 < tau) (htheta : 0 ≤ theta)
       (child initial : Fin M → TargetInterval target.length → ℚ)
       (comparison : Fin M → TargetInterval target.length)
       (hcomparison : comparison ∈ computedBandActions parent r b P tau theta velocity child)
       (L0 F : ℚ) (hL0 : 0 ≤ L0) (hF : 1 ≤ F) (hsmall : L0 * theta ≤ 1)
       (hinitial : ∀ i, 0 ≤ initial i (comparison i))
       (hspatial : ∀ i s t, initial i s ≤ initial i t + L0 * targetEndpointDistance s t)
       (hinitialUpper : ∀ i, initial i (comparison i) ≤ 2 * F * (stateEditCost
         (substring source (sourceChild parent i).lo (sourceChild parent i).hi) target (comparison i) : ℚ))
   …

   Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.computedBandActions, OAI.EditApproximation.targetEndpointDistance, OAI.EditApproximation.stateEditCost, OAI.EditApproximation.substring, OAI.EditApproximation.sourceChild