ProductRank.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The mixed-operator product-rank estimate. Unlike the abstract assembly lemma, the intermediate-space rank bounds here are proved from the actual operator, and its dimension is computed from the two variable groups.

theorem OAI.Problem335.mixed_product_rank_le line 23

Source documentation

The product-rank lemma for a homogeneous product, under the elementary numerical hypotheses on the source degrees and balancing ratios. There is no circuit or polynomial rank hypothesis in this statement.

theorem mixed_product_rank_le
    (side : σ → Bool) (Q : ι → MvPolynomial σ K) (e : ι → ℕ)
    (hQ : ∀ j, (Q j).IsHomogeneous (e j))
    (k n 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 = n) (hproportion : lam * n = 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)) :
…