CircuitProductBound.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.LowProductBound line 14

Source documentation

The product estimate required when every positive formal degree is small.

def LowProductBound {K : Type u} [CommSemiring K] {σ : Type v}
    (R : MvPolynomial σ K → ℝ) (d : ℕ) (t B : ℝ) : Prop :=
…

def OAI.Problem335.HighProductBound line 22

Source documentation

The product estimate required after opening one large middle factor.

def HighProductBound {K : Type u} [CommSemiring K] {σ : Type v}
    (R : MvPolynomial σ K → ℝ) (d : ℕ) (t B : ℝ) : Prop :=
…

theorem OAI.Problem335.positive_middle_product_measure_le line 33

Source documentation

Opening one high middle factor, or applying the all-low estimate, bounds an actual list of positive-degree middle-gate occurrences.

theorem positive_middle_product_measure_le
    {K : Type u} [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)
    (d : ℕ) (t B : ℝ) (hB : 0 ≤ B)
    (hlow : LowProductBound R d t B) (hhigh : HighProductBound R d t B)
    (l : List (Fin c.middleCount))
    (hpos : ∀ j ∈ l, 0 < c.middleDegree j)
    (hdegree : (l.map c.middleDegree).sum = d) :
    R (l.map (middleValue c)).prod ≤ (circuitSize c : ℝ) * B := by
…

Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.LowProductBound, OAI.Problem335.HighProductBound, OAI.Problem335.middleValue, OAI.Problem335.circuitSize

theorem OAI.Problem335.circuit_measure_le_of_product_estimates line 110

Source documentation

The manuscript's gate-count reduction instantiated with the actual circuit normal forms. All remaining hypotheses are bounds on homogeneous products, not circuit-specific summands or wire counts.

theorem circuit_measure_le_of_product_estimates
    {K : Type u} [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)
    (d : ℕ) (houtput : c.outputDegree = d) (t B : ℝ) (hB : 0 ≤ B)
    (hlow : LowProductBound R d t B) (hhigh : HighProductBound R d t B) :
    R (circuitValue c) ≤ (circuitSize c : ℝ) ^ 2 * B := by
…

Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.LowProductBound, OAI.Problem335.HighProductBound, OAI.Problem335.circuitValue, OAI.Problem335.circuitSize