ProductCost.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Numerical assembly of the product-rank estimates

These lemmas isolate the finite-product and real-power calculations in the all-low and one-high cases of the circuit rank estimate. All hypotheses on individual factor costs and parameters remain explicit.

theorem OAI.Problem335.prod_cost_le_exp_mul_rpow line 19

Source documentation

Assemble individual exponential errors and favorable powers of a base at most one. This applies regardless of the source of the factor estimates.

theorem prod_cost_le_exp_mul_rpow {ι : Type*} (s : Finset ι)
    (H err d : ι → ℝ) (q E D : ℝ) (hq : 0 < q) (hq1 : q ≤ 1)
    (hH : ∀ j ∈ s, 0 ≤ H j)
    (hcost : ∀ j ∈ s, H j ≤ Real.exp (err j) * q ^ d j)
    (herr : (∑ j ∈ s, err j) ≤ E) (hd : D ≤ ∑ j ∈ s, d j) :
    (∏ j ∈ s, H j) ≤ Real.exp E * q ^ D := by
…

theorem OAI.Problem335.all_low_power_saving line 37

Source documentation

The favorable power in the all-low case saves the exact manuscript exponent sqrt(n)/20.

theorem all_low_power_saving (n q s : ℝ) (hn : 1 ≤ n) (hq : 0 ≤ q)
    (hqbound : q ≤ n ^ (-(2 : ℝ) / 5)) (hs : Real.sqrt n / 2 ≤ s) :
    q ^ (s / 4) ≤ n ^ (-Real.sqrt n / 20) := by
…

theorem OAI.Problem335.one_high_power_saving line 53

Source documentation

The favorable power from expanding one high-degree factor saves the exact manuscript exponent 3*sqrt(n)/160.

theorem one_high_power_saving (n q lam t : ℝ) (hn : 1 ≤ n) (hq : 0 ≤ q)
    (hqbound : q ≤ n ^ (-(2 : ℝ) / 5)) (hlam : (3 : ℝ) / 8 ≤ lam)
    (ht : Real.sqrt n / 4 ≤ t) :
    q ^ (lam * t / 2) ≤ n ^ (-(3 * Real.sqrt n) / 160) := by
…

theorem OAI.Problem335.high_factor_exponential_bound line 72

Source documentation

The bounded loss per remaining large factor is exponential in sqrt n.

theorem high_factor_exponential_bound (n s : ℝ) (hs : s ≤ Real.sqrt n) :
    (5 : ℝ) ^ (4 * s) ≤ Real.exp (4 * Real.log 5 * Real.sqrt n) := by
…

theorem OAI.Problem335.large_degree_count_mul_le_sum line 81
Source documentation
The number of large positive-degree factor occurrences is charged to their total degree, rather than to the number of distinct circuit gates.
```
theorem large_degree_count_mul_le_sum {ι : Type*} (s : Finset ι)
    (e : ι → ℝ) (t : ℝ) (he : ∀ j ∈ s, 0 ≤ e j) :
    ((s.filter (fun j => t ≤ e j)).card : ℝ) * t ≤ ∑ j ∈ s, e j := by
…
```

theorem OAI.Problem335.large_degree_count_le line 97

Source documentation

Division form of the large-degree occurrence count.

theorem large_degree_count_le {ι : Type*} (s : Finset ι)
    (e : ι → ℝ) (t : ℝ) (ht : 0 < t) (he : ∀ j ∈ s, 0 ≤ e j) :
    ((s.filter (fun j => t ≤ e j)).card : ℝ) ≤ (∑ j ∈ s, e j) / t := by
…

theorem OAI.Problem335.all_low_common_rank_bound line 104

Source documentation

The all-low branch fits the common circuit-rank envelope. No sign assumption on the error constant C is required.

theorem all_low_common_rank_bound (n S D C : ℝ) (hn : 1 ≤ n)
    (hS : 1 ≤ S) (hD : 0 ≤ D) :
    2 * D * Real.exp (4 * C * Real.sqrt n) * n ^ (-Real.sqrt n / 20) ≤
      2 * S * D * Real.exp ((4 * C + 4 * Real.log 5) * Real.sqrt n) *
        n ^ (-Real.sqrt n / 100) := by
…

theorem OAI.Problem335.one_high_common_rank_bound line 124

Source documentation

The one-high branch fits the same envelope, absorbing the bounded cost of all remaining high-degree factors.

theorem one_high_common_rank_bound (n s S D C : ℝ) (hn : 1 ≤ n)
    (hs : s ≤ Real.sqrt n) (hS : 0 ≤ S) (hD : 0 ≤ D) :
    2 * S * D * (5 : ℝ) ^ (4 * s) * Real.exp (4 * C * Real.sqrt n) *
        n ^ (-(3 * Real.sqrt n) / 160) ≤
      2 * S * D * Real.exp ((4 * C + 4 * Real.log 5) * Real.sqrt n) *
        n ^ (-Real.sqrt n / 100) := by
…

theorem OAI.Problem335.sum_branch_rank_bound line 148

Source documentation

Summing at most S upper-product contributions gives the quadratic gate factor in the circuit-rank proposition.

theorem sum_branch_rank_bound {ι : Type*} (s : Finset ι) (R : ι → ℝ)
    (n S D C : ℝ) (hn : 0 ≤ n) (hS : 0 ≤ S) (hD : 0 ≤ D)
    (hcard : (s.card : ℝ) ≤ S)
    (hR : ∀ j ∈ s, R j ≤
      2 * S * D * Real.exp (C * Real.sqrt n) * n ^ (-Real.sqrt n / 100)) :
    (∑ j ∈ s, R j) ≤
      2 * S ^ 2 * D * Real.exp (C * Real.sqrt n) * n ^ (-Real.sqrt n / 100) := by
…

theorem OAI.Problem335.prod_high_low_cost_le line 168

Source documentation

Splitting large and small degrees multiplies their two distinct types of cost, with the large-factor multiplicity retained exactly.

theorem prod_high_low_cost_le {ι : Type*} (s : Finset ι)
    (H err e : ι → ℝ) (t B E : ℝ)
    (hH : ∀ j ∈ s, 0 ≤ H j) (hB : 0 ≤ B)
    (hhigh : ∀ j ∈ s, t ≤ e j → H j ≤ B)
    (hlow : ∀ j ∈ s, e j < t → H j ≤ Real.exp (err j))
    (herr : (∑ j ∈ s with e j < t, err j) ≤ E) :
    (∏ j ∈ s, H j) ≤
      B ^ (s.filter (fun j => t ≤ e j)).card * Real.exp E := by
…

theorem OAI.Problem335.prod_high_low_cost_le_rpow line 192

Source documentation

A degree budget replaces the number of high factors by N/t.

theorem prod_high_low_cost_le_rpow {ι : Type*} (s : Finset ι)
    (H err e : ι → ℝ) (t B E N : ℝ) (ht : 0 < t)
    (hH : ∀ j ∈ s, 0 ≤ H j) (hB : 1 ≤ B)
    (he : ∀ j ∈ s, 0 ≤ e j) (hbudget : (∑ j ∈ s, e j) ≤ N)
    (hhigh : ∀ j ∈ s, t ≤ e j → H j ≤ B)
    (hlow : ∀ j ∈ s, e j < t → H j ≤ Real.exp (err j))
    (herr : (∑ j ∈ s with e j < t, err j) ≤ E) :
    (∏ j ∈ s, H j) ≤ B ^ (N / t) * Real.exp E := by
…

theorem OAI.Problem335.linear_factor_cost_power_le line 213

Source documentation

Expanding one factor of degree at least t supplies enough linear-factor cost to obtain the favorable power q^(lam*t/2).

theorem linear_factor_cost_power_le (H q lam t : ℝ) (e : ℕ)
    (hH : 0 ≤ H) (hq : 0 < q) (hq1 : q ≤ 1) (hlam : 0 ≤ lam)
    (hcost : H ≤ q ^ (lam / 2)) (he : t ≤ (e : ℝ)) :
    H ^ e ≤ q ^ (lam * t / 2) := by
…

theorem OAI.Problem335.expanded_high_product_cost_le line 228

Source documentation

The abstract one-high expansion estimate, before inserting the analytic parameter bounds. The finite family represents the unexpanded occurrences.

theorem expanded_high_product_cost_le {ι : Type*} (s : Finset ι)
    (H err e : ι → ℝ) (Hlin q lam t B E N : ℝ) (d : ℕ)
    (ht : 0 < t) (hH : ∀ j ∈ s, 0 ≤ H j) (hB : 1 ≤ B)
    (he : ∀ j ∈ s, 0 ≤ e j) (hbudget : (∑ j ∈ s, e j) ≤ N)
    (hhigh : ∀ j ∈ s, t ≤ e j → H j ≤ B)
    (hlow : ∀ j ∈ s, e j < t → H j ≤ Real.exp (err j))
    (herr : (∑ j ∈ s with e j < t, err j) ≤ E)
    (hHlin : 0 ≤ Hlin) (hq : 0 < q) (hq1 : q ≤ 1) (hlam : 0 ≤ lam)
    (hlinear : Hlin ≤ q ^ (lam / 2)) (hd : t ≤ (d : ℝ)) :
    Hlin ^ d * (∏ j ∈ s, H j) ≤
      B ^ (N / t) * Real.exp E * q ^ (lam * t / 2) := by
…