Unrestricted depth-three lower bound: restriction tails

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/RestrictionTails.lean

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

theorem Complexity.DepthThreeLowerBound.restrictionAvg_pow_card_live {V : Type uDepth1} [Fintype V] [DecidableEq V] (p a : ℝ) : (restrictionAvg p fun (σ : Restriction V) => a ^ Fintype.card (Live σ)) = (1 - p + p * a) ^ Fintype.card V

theorem Complexity.DepthThreeLowerBound.restrictionAvg_two_pow_live {V : Type uDepth1} [Fintype V] [DecidableEq V] (p : ℝ) : (restrictionAvg p fun (σ : Restriction V) => 2 ^ ↑(Fintype.card (Live σ))) = (1 + p) ^ Fintype.card V

theorem Complexity.DepthThreeLowerBound.restrictionAvg_two_neg_pow_live {V : Type uDepth1} [Fintype V] [DecidableEq V] (p : ℝ) : (restrictionAvg p fun (σ : Restriction V) => 2 ^ (-↑(Fintype.card (Live σ)))) = (1 - p / 2) ^ Fintype.card V

theorem Complexity.DepthThreeLowerBound.one_add_pow_le_exp (p : ℝ) (hp : 0 ≤ p) (n : ℕ) : (1 + p) ^ n ≤ Real.exp (p * ↑n)

theorem Complexity.DepthThreeLowerBound.one_sub_half_pow_le_exp (p : ℝ) (hp1 : p ≤ 1) (n : ℕ) : (1 - p / 2) ^ n ≤ Real.exp (-(p * ↑n) / 2)

theorem Complexity.DepthThreeLowerBound.restrictionAvg_lower_tail {V : Type uDepth1} [Fintype V] [DecidableEq V] (p : ℝ) (hp : 0 ≤ p) (hp1 : p ≤ 1) : (restrictionAvg p fun (σ : Restriction V) => if ↑(Fintype.card (Live σ)) < p * ↑(Fintype.card V) / 2 then 1 else 0) ≤ 2 ^ (-(p * ↑(Fintype.card V)) / 16)

theorem Complexity.DepthThreeLowerBound.restrictionAvg_upper_tail {V : Type uDepth1} [Fintype V] [DecidableEq V] (p : ℝ) (hp : 0 ≤ p) (hp1 : p ≤ 1) : (restrictionAvg p fun (σ : Restriction V) => if 2 * (p * ↑(Fintype.card V)) < ↑(Fintype.card (Live σ)) then 1 else 0) ≤ 2 ^ (-(p * ↑(Fintype.card V)) / 16)

theorem Complexity.DepthThreeLowerBound.restrictionAvg_outside_window {V : Type uDepth1} [Fintype V] [DecidableEq V] (p : ℝ) (hp : 0 ≤ p) (hp1 : p ≤ 1) : (restrictionAvg p fun (σ : Restriction V) => if ¬(p * ↑(Fintype.card V) / 2 ≤ ↑(Fintype.card (Live σ)) ∧ ↑(Fintype.card (Live σ)) ≤ 2 * (p * ↑(Fintype.card V))) then 1 else 0) ≤ 2 * 2 ^ (-(p * ↑(Fintype.card V)) / 16)