Superquadratic sensitivity separation: parameter bounds

Real-number estimates on the size parameter M under the hypotheses 1 ≤ d and 9 ^ (d + 1) ≤ M. The label count r = max (Nat.ceil (Real.sqrt M)) 16 is at most 2 * Real.sqrt M, so the relative label budget satisfies r / M ≤ 2 / Real.sqrt M ≤ 2 / 3 ^ (d + 1); equivalently r / M * 3 ^ (d + 1) ≤ 2, which is the budget condition required by the sensitivity bound of the construction.

Main results

• parameter_ge_eighty_one: 81 ≤ M.
• ceil_sqrt_max_le_two_sqrt: max (Nat.ceil (Real.sqrt M)) 16 ≤ 2 * Real.sqrt M for 81 ≤ M.
• parameter_epsilon_budget: max (Nat.ceil (Real.sqrt M)) 16 / M * 3 ^ (d + 1) ≤ 2.
• parameter_epsilon_sqrt: max (Nat.ceil (Real.sqrt M)) 16 / M ≤ 2 / Real.sqrt M ≤ 2 / 3 ^ (d + 1).

References

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

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.parameter_ge_eighty_one {d M : ℕ} (hd : 1 ≤ d) (hM : 9 ^ (d + 1) ≤ M) : 81 ≤ M

If 1 ≤ d and 9 ^ (d + 1) ≤ M, then 81 ≤ M.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.ceil_sqrt_max_le_two_sqrt {M : ℕ} (hM : 81 ≤ M) : ↑(max ⌈√↑M⌉₊ 16) ≤ 2 * √↑M

For 81 ≤ M, max (Nat.ceil (Real.sqrt M)) 16 ≤ 2 * Real.sqrt M in ℝ.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.parameter_epsilon_budget {d M : ℕ} (hd : 1 ≤ d) (hM : 9 ^ (d + 1) ≤ M) : ↑(max ⌈√↑M⌉₊ 16) / ↑M * 3 ^ (d + 1) ≤ 2

If 1 ≤ d and 9 ^ (d + 1) ≤ M, then max (Nat.ceil (Real.sqrt M)) 16 / M * 3 ^ (d + 1) ≤ 2 in ℝ.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.parameter_epsilon_sqrt {d M : ℕ} (hd : 1 ≤ d) (hM : 9 ^ (d + 1) ≤ M) : ↑(max ⌈√↑M⌉₊ 16) / ↑M ≤ 2 / √↑M ∧ 2 / √↑M ≤ 2 / 3 ^ (d + 1)

If 1 ≤ d and 9 ^ (d + 1) ≤ M, then max (Nat.ceil (Real.sqrt M)) 16 / M ≤ 2 / Real.sqrt M and 2 / Real.sqrt M ≤ 2 / 3 ^ (d + 1) in ℝ.