OAI/Algebra/DepthFive/CircuitRankAssembly.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.measure_finset_sum_le line 11

   Source documentation

   Finite subadditivity, with no assumptions on the individual summands.

   theorem measure_finset_sum_le {A ι : Type*} [AddCommMonoid A]
       (R : A → ℝ) (hzero : R 0 = 0)
       (hadd : ∀ x y, R (x + y) ≤ R x + R y)
       (s : Finset ι) (f : ι → A) :
       R (∑ j ∈ s, f j) ≤ ∑ j ∈ s, R (f j) := by
   …

2. theorem OAI.Problem335.measure_weighted_sum_le line 24

   Source documentation

   Scalar weighting cannot increase a subadditive rank-like measure.

   theorem measure_weighted_sum_le {K σ ι : Type*} [CommSemiring K]
       (R : MvPolynomial σ 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 : Finset ι) (a : ι → K) (p : ι → MvPolynomial σ K) :
       R (∑ j ∈ s, MvPolynomial.C (a j) * p j) ≤ ∑ j ∈ s, R (p j) := by
   …

3. theorem OAI.Problem335.measure_one_factor_expansion_le line 36

   Source documentation

   Expand one selected factor and leave all other occurrences unchanged. This is the algebraic step behind the high-degree-factor case: in particular, other occurrences of the very same middle gate are not expanded.

   theorem measure_one_factor_expansion_le {K σ ι : Type*} [CommSemiring K]
       (R : MvPolynomial σ 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 : Finset ι) (a : ι → K) (p : ι → MvPolynomial σ K)
       (before after : MvPolynomial σ K) :
       R (before * (∑ j ∈ s, MvPolynomial.C (a j) * p j) * after) ≤
         ∑ j ∈ s, R (before * p j * after) := by
   …

4. theorem OAI.Problem335.measure_weighted_sum_le_card_mul line 57

   Source documentation

   Only predecessors with nonzero aggregate coefficient need a bound. This matters for homogeneous circuits, since inactive gates can have arbitrary formal degree.

   theorem measure_weighted_sum_le_card_mul {K σ ι : Type*} [CommSemiring K]
       (R : MvPolynomial σ 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 : Finset ι) (a : ι → K) (p : ι → MvPolynomial σ K)
       (B : ℝ) (hB : 0 ≤ B)
       (hbound : ∀ j ∈ s, a j ≠ 0 → R (p j) ≤ B) :
       R (∑ j ∈ s, MvPolynomial.C (a j) * p j) ≤ (s.card : ℝ) * B := by
   …

5. theorem OAI.Problem335.circuit_measure_le_upperCount_mul line 79

   Source documentation

   A uniform bound on active output predecessors costs the number of upper product gates, never the number of output wires.

   theorem circuit_measure_le_upperCount_mul {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)
       (B : ℝ) (hB : 0 ≤ B)
       (hbound : ∀ j, gateCoefficient c.outputInputs j ≠ 0 → R (upperValue c j) ≤ B) :
       R (circuitValue c) ≤ (c.upperCount : ℝ) * B := by
   …

   Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.gateCoefficient, OAI.Problem335.upperValue, OAI.Problem335.circuitValue

6. theorem OAI.Problem335.upper_measure_le_lowerCount_mul_of_split line 95

   Source documentation

   Expanding one middle-gate occurrence costs at most the number of lower product gates. All other occurrences, including shared copies of the selected gate, are retained as factors in before and after.

   theorem upper_measure_le_lowerCount_mul_of_split
       {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)
       (u : Fin c.upperCount) (j : Fin c.middleCount)
       (before after : List (Fin c.middleCount))
       (hsplit : c.upperInputs u = before ++ j :: after)
       (B : ℝ) (hB : 0 ≤ B)
       (hbound : ∀ l, gateCoefficient (c.middleInputs j) l ≠ 0 →
         R ((before.map (middleValue c)).prod * lowerValue c l *
           (after.map (middleValue c)).prod) ≤ B) :
   …

   Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.gateCoefficient, OAI.Problem335.middleValue, OAI.Problem335.lowerValue

7. theorem OAI.Problem335.circuit_measure_le_size_sq_mul_of_low_or_split line 130

   Source documentation

   The gate-count assembly step in the depth-five rank upper bound. Each active upper product is either bounded directly, or one occurrence can be expanded into active lower products with the same bound.

   theorem circuit_measure_le_size_sq_mul_of_low_or_split
       {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)
       (B : ℝ) (hB : 0 ≤ B)
       (hupper : ∀ u, gateCoefficient c.outputInputs u ≠ 0 →
         R (upperValue c u) ≤ B ∨
           ∃ (j : Fin c.middleCount) (before after : List (Fin c.middleCount)),
             c.upperInputs u = before ++ j :: after ∧
             ∀ l, gateCoefficient (c.middleInputs j) l ≠ 0 →
               R ((before.map (middleValue c)).prod * lowerValue c l *
   …

   Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.gateCoefficient, OAI.Problem335.upperValue, OAI.Problem335.middleValue, OAI.Problem335.lowerValue