OAI/Algebra/DepthFive/ProductRankCanonical.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.bidegreeRank_product_le_degreeWeight line 15

   Source documentation

   The product-rank estimate in the common rank API used by both circuit and moment bounds. Its dimension factor is the actual source dimension.

   theorem bidegreeRank_product_le_degreeWeight
       (side : σ → Bool) (Q : ι → MvPolynomial σ K) (e : ι → ℕ)
       (hQ : ∀ j, (Q j).IsHomogeneous (e j))
       (k m v u a b : ℕ) (rho lam : ℝ)
       (hvcard : Fintype.card {x : σ // side x = true} = v)
       (hucard : Fintype.card {x : σ // side x = false} = u)
       (he : ∑ j, e j = k + m) (hproportion : lam * (k + m) = k)
       (hslope : (1 + rho) * lam = rho)
       (hv : 1 ≤ v) (hu : 1 ≤ u) (ha : 0 < a) (hb : 0 < b)
       (hka : k ≤ a) (hbudget : 2 * k ≤ a + v)
       (hbalance : ((a : ℝ) / ((a : ℝ) + v)) ^ rho ≤
         (b : ℝ) / ((b : ℝ) + u)) :
   …