CircuitWeightBound.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.Problem335.WeightParameters line 11
Source documentation
The numerical parameter estimates needed by the circuit upper rank bound.
```
structure WeightParameters (n : ℕ) (s q : ℝ) : Prop where
…
```
def OAI.Problem335.HomogeneousProductRankBound line 23
Source documentation
The product-rank statement is kept explicit as the one algebraic input.
```
def HomogeneousProductRankBound {K σ : Type*} [CommSemiring K]
    (R : MvPolynomial σ K → ℝ) (n : ℕ) (q lam D : ℝ) : Prop :=
…
```
def OAI.Problem335.circuitProductEnvelope line 32
Source documentation
A common bound for a small product and for one expanded high product.
```
def circuitProductEnvelope (n : ℕ) (D : ℝ) : ℝ :=
…
```
lemma OAI.Problem335.sum_get_eq_map_sum line 36
lemma OAI.Problem335.prod_get_eq_map_prod line 43

theorem OAI.Problem335.homogeneousProductRankBound_of_fin line 51

Source documentation

A Fin-indexed product-rank theorem supplies the list interface used by circuits.

theorem homogeneousProductRankBound_of_fin {K σ : Type*} [CommSemiring K]
    (R : MvPolynomial σ K → ℝ) (n : ℕ) (q lam D : ℝ)
    (h : ∀ (m : ℕ) (P : Fin m → MvPolynomial σ K) (e : Fin m → ℕ),
      (∀ i, 0 < e i) → (∀ i, (P i).IsHomogeneous (e i)) →
      (∑ i, e i) = n → R (∏ i, P i) ≤ 2 * D * ∏ i, degreeWeight q lam (e i)) :
    HomogeneousProductRankBound R n q lam D := by
…

Mentions: OAI.Problem335.degreeWeight, OAI.Problem335.HomogeneousProductRankBound

lemma OAI.Problem335.lowProductBound_of_product_rank line 67
lemma OAI.Problem335.highProductBound_of_product_rank line 95

theorem OAI.Problem335.circuit_rank_bound_from_product_rank line 143

Source documentation

The full circuit upper rank estimate, reducing the actual circuit only to the homogeneous-product rank theorem and explicit numerical parameters.

theorem circuit_rank_bound_from_product_rank
    {K : Type*} [CommSemiring K] {n : ℕ} (c : Depth5Circuit K n)
    (R : MvPolynomial (Fin n × Fin n × Fin n) K → ℝ)
    (hzero : R 0 = 0) (hadd : ∀ x y, R (x + y) ≤ R x + R y)
    (hscale : ∀ a p, R (MvPolynomial.C a * p) ≤ R p)
    (s q D : ℝ) (hp : WeightParameters n s q) (hD : 0 ≤ D)
    (houtput : c.outputDegree = n)
    (hprod : HomogeneousProductRankBound R n q (1 / 2 - s / (2 * n)) D) :
    R (circuitValue c) ≤ 2 * (circuitSize c : ℝ) ^ 2 * D *
      Real.exp ((24 + 4 * Real.log 5) * Real.sqrt n) * (n : ℝ) ^ (-Real.sqrt n / 100) := by
…

Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.WeightParameters, OAI.Problem335.HomogeneousProductRankBound, OAI.Problem335.circuitValue, OAI.Problem335.circuitSize