Superquadratic sensitivity separation: profile arithmetic

Arithmetic reducing the four raw recurrences for the side sensitivities s₀, s₁ and the joint sensitivities j₀, j₁ of consecutive recursive levels to two scalar recurrences. Each pair is normalized by normalizedMax, which divides the zero-side value by M ^ n and the one-side value by M ^ (n + 1); the normalized side and joint maxima u, v then satisfy u' ≤ (1 + ε) * u + 3 * v and v' ≤ ε * u + 3 * v.

Main definitions

• normalizedMax: the maximum max (s₀ / M ^ n) (s₁ / M ^ (n + 1)).

Main results

• normalizedMax_le: normalizedMax M n s₀ s₁ ≤ u whenever s₀ ≤ u * M ^ n and s₁ ≤ u * M ^ (n + 1).
• raw_profiles_step: the one-step bound for the four raw recurrences in unnormalized form.
• normalized_profiles_step: the four raw recurrences imply the two normalized scalar recurrences.

References

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

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.normalizedMax (M : ℝ) (n : ℕ) (s₀ s₁ : ℝ) : ℝ

Maximum of the two sensitivity bounds after their level-dependent normalization.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.normalizedMax_nonneg {M s₀ s₁ : ℝ} {n : ℕ} (hM : 0 < M) (hs₀ : 0 ≤ s₀) : 0 ≤ normalizedMax M n s₀ s₁

For 0 < M and 0 ≤ s₀, the normalized maximum is nonnegative.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.le_normalizedMax_zero {M s₀ s₁ : ℝ} {n : ℕ} (hM : 0 < M) : s₀ ≤ normalizedMax M n s₀ s₁ * M ^ n

For 0 < M, s₀ ≤ normalizedMax M n s₀ s₁ * M ^ n.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.le_normalizedMax_one {M s₀ s₁ : ℝ} {n : ℕ} (hM : 0 < M) : s₁ ≤ normalizedMax M n s₀ s₁ * M ^ (n + 1)

For 0 < M, s₁ ≤ normalizedMax M n s₀ s₁ * M ^ (n + 1).

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.normalizedMax_le {M s₀ s₁ u : ℝ} {n : ℕ} (hM : 0 < M) (h₀ : s₀ ≤ u * M ^ n) (h₁ : s₁ ≤ u * M ^ (n + 1)) : normalizedMax M n s₀ s₁ ≤ u

For 0 < M, if s₀ ≤ u * M ^ n and s₁ ≤ u * M ^ (n + 1), then normalizedMax M n s₀ s₁ ≤ u.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.raw_profiles_step {M r ε u v p : ℝ} (hM : 0 < M) (hp : 0 ≤ p) (hu : 0 ≤ u) (hv : 0 ≤ v) (hr : 0 ≤ r) (hεr : r ≤ ε * M) (hεt : 16 ≤ ε * M) {s₀ s₁ j₀ j₁ s₀' s₁' j₀' j₁' : ℝ} (hs₀ : s₀ ≤ u * p) (hs₁ : s₁ ≤ u * (p * M)) (hj₀ : j₀ ≤ v * p) (hj₁ : j₁ ≤ v * (p * M)) (hS₀ : s₀' ≤ 16 * s₀ + s₁ + 3 * j₁) (hS₁ : s₁' ≤ M ^ 2 * s₀ + r * s₁) (hJ₀ : j₀' ≤ 16 * s₀ + 3 * j₁) (hJ₁ : j₁' ≤ M ^ 2 * j₀ + r * s₁) : s₀' ≤ ((1 + ε) * u + 3 * v) * (p * M) ∧ s₁' ≤ ((1 + ε) * u + 3 * v) * (p * M * M) ∧ j₀' ≤ (ε * u + 3 * v) * (p * M) ∧ j₁' ≤ (ε * u + 3 * v) * (p * M * M)

Unnormalized one-step bound: suppose s₀ ≤ u * p, s₁ ≤ u * (p * M), j₀ ≤ v * p, j₁ ≤ v * (p * M), r ≤ ε * M and 16 ≤ ε * M, and that the primed quantities satisfy the four raw recurrences. Then s₀' and s₁' are at most ((1 + ε) * u + 3 * v) times p * M and p * M * M respectively, and j₀' and j₁' are at most (ε * u + 3 * v) times p * M and p * M * M respectively.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.normalized_profiles_step {M r ε : ℝ} {n : ℕ} (hM : 0 < M) (hr : 0 ≤ r) (hεr : r / M ≤ ε) (hεt : 16 / M ≤ ε) {s₀ s₁ j₀ j₁ s₀' s₁' j₀' j₁' : ℝ} (hs₀ : 0 ≤ s₀) (hj₀ : 0 ≤ j₀) (hS₀ : s₀' ≤ 16 * s₀ + s₁ + 3 * j₁) (hS₁ : s₁' ≤ M ^ 2 * s₀ + r * s₁) (hJ₀ : j₀' ≤ 16 * s₀ + 3 * j₁) (hJ₁ : j₁' ≤ M ^ 2 * j₀ + r * s₁) : normalizedMax M (n + 1) s₀' s₁' ≤ (1 + ε) * normalizedMax M n s₀ s₁ + 3 * normalizedMax M n j₀ j₁ ∧ normalizedMax M (n + 1) j₀' j₁' ≤ ε * normalizedMax M n s₀ s₁ + 3 * normalizedMax M n j₀ j₁

If r / M ≤ ε, 16 / M ≤ ε, s₀, j₀ ≥ 0 and the primed quantities satisfy the four raw recurrences, then the normalized side maximum at level n + 1 is at most (1 + ε) * u + 3 * v and the normalized joint maximum at most ε * u + 3 * v, where u = normalizedMax M n s₀ s₁ and v = normalizedMax M n j₀ j₁.