Sensitivity separation: profile arithmetic

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/ProfileArithmetic.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

noncomputable def Complexity.BooleanAnalysis.Sensitivity.Internal.normalizedMax (M : ℝ) (n : ℕ) (s₀ s₁ : ℝ) : ℝ

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

Equations

• Complexity.BooleanAnalysis.Sensitivity.Internal.normalizedMax M n s₀ s₁ = max (s₀ / M ^ n) (s₁ / M ^ (n + 1))

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.normalizedMax_nonneg {M s₀ s₁ : ℝ} {n : ℕ} (hM : 0 < M) (hs₀ : 0 ≤ s₀) : 0 ≤ normalizedMax M n s₀ s₁

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.le_normalizedMax_zero {M s₀ s₁ : ℝ} {n : ℕ} (hM : 0 < M) : s₀ ≤ normalizedMax M n s₀ s₁ * M ^ n

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

theorem Complexity.BooleanAnalysis.Sensitivity.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

theorem Complexity.BooleanAnalysis.Sensitivity.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)

theorem Complexity.BooleanAnalysis.Sensitivity.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₁