RangedComplexityBudget.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual range partition cost is polynomial at fixed depth

theorem OAI.Ostmann.ranged_word_complexity_le line 12

Source documentation

Include the extra root product interval in D; the same bound then covers the normalized reciprocal-product comparison.

theorem ranged_word_complexity_le {V : Type*} {n : ℕ}
    (D D' : WordRangeDecoration V n) (B : ℕ) (b d m : ℝ)
    (hd : 0 ≤ d) (hm : 0 ≤ m)
    (hB : (B : ℝ) ≤ b * (1 + m))
    (hD : (D.count : ℝ) ≤ d * (1 + m))
    (hD' : (D'.count : ℝ) ≤ d * (1 + m)) :
    (((3 * 2 ^ n + 3 * (2 ^ n - 1) + 2 * (D.count + D'.count)) * B ^ (n + 1) : ℕ) : ℝ) ≤
      (((3 * 2 ^ n + 3 * (2 ^ n - 1) : ℕ) : ℝ) + 4 * d) *
        b ^ (n + 1) * (1 + m) ^ (n + 2) := by
…

Mentions: OAI.Ostmann.WordRangeDecoration

theorem OAI.Ostmann.ranged_boolean_partition_le line 35