Superquadratic sensitivity separation: scalar bounds

Solution of the coupled scalar recurrences u (n + 1) ≤ (1 + ε) * u n + 3 * v n and v (n + 1) ≤ ε * u n + 3 * v n with u 0 ≤ L and v 0 ≤ 0. Under the budget ε * 3 ^ (d + 1) ≤ 2, the normalized side profile u stays below 2 * L for the first d levels, while the joint profile v is at most ε * L * (3 ^ n - 1).

Main results

• geometric_error_le: under the budget, the accumulated error (3 / 2) * ε * L * (3 ^ n - 1) is at most L for n ≤ d.
• coupled_profiles_bound: solutions of the coupled recurrences satisfy u n ≤ 2 * L and v n ≤ ε * L * (3 ^ n - 1) for n ≤ d.

References

• Adapted from OpenAI's formalization [OAI26b] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (file lean/OAI/Combinatorics/Sensitivity/ScalarBounds.lean), via the complexitylib port [Sch26e] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.geometric_error_le {d n : ℕ} (hn : n ≤ d) {ε L : ℝ} (hε : 0 ≤ ε) (hL : 0 ≤ L) (hbudget : ε * 3 ^ (d + 1) ≤ 2) : 3 / 2 * ε * L * (3 ^ n - 1) ≤ L

If n ≤ d, 0 ≤ ε, 0 ≤ L and ε * 3 ^ (d + 1) ≤ 2, then (3 / 2) * ε * L * (3 ^ n - 1) ≤ L.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.coupled_profiles_bound (d : ℕ) (u v : ℕ → ℝ) (ε L : ℝ) (hε : 0 ≤ ε) (hL : 0 ≤ L) (hbudget : ε * 3 ^ (d + 1) ≤ 2) (hu0 : u 0 ≤ L) (hv0 : v 0 ≤ 0) (hu : ∀ n < d, u (n + 1) ≤ (1 + ε) * u n + 3 * v n) (hv : ∀ n < d, v (n + 1) ≤ ε * u n + 3 * v n) (n : ℕ) : n ≤ d → u n ≤ 2 * L ∧ v n ≤ ε * L * (3 ^ n - 1)

If 0 ≤ ε, 0 ≤ L, ε * 3 ^ (d + 1) ≤ 2, u 0 ≤ L, v 0 ≤ 0, and for all n < d both u (n + 1) ≤ (1 + ε) * u n + 3 * v n and v (n + 1) ≤ ε * u n + 3 * v n, then u n ≤ 2 * L and v n ≤ ε * L * (3 ^ n - 1) for all n ≤ d.