ProductRankAssembly.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.ProductRankAssembly.measure_sum_le line 16

Source documentation

The rank subadditivity step, stated for a real-valued polynomial measure.

theorem measure_sum_le (R : MvPolynomial σ K → ℝ)
    (hzero : R 0 = 0) (hadd : ∀ p q, R (p + q) ≤ R p + R q)
    {α : Type*} (s : Finset α) (f : α → MvPolynomial σ K) :
    R (∑ a ∈ s, f a) ≤ ∑ a ∈ s, R (f a) := by
…

theorem OAI.Problem335.ProductRankAssembly.measure_component_product_le_sum line 29

Source documentation

A product's fixed bidegree has rank at most the sum over exactly those assignments with matching total degree.

theorem measure_component_product_le_sum
    (R : MvPolynomial σ K → ℝ)
    (hzero : R 0 = 0) (hadd : ∀ p q, R (p + q) ≤ R p + R q)
    (side : σ → Bool) (p : ι → MvPolynomial σ K) (e : ι → ℕ)
    (hp : ∀ j, (p j).IsHomogeneous (e j)) (k : ℕ) :
    R (Bidegree.component side k (∏ j, p j)) ≤
      ∑ i ∈ (Fintype.piFinset (fun j => Finset.range (e j + 1))).filter
        (fun i => ∑ j, i j = k), R (∏ j, Bidegree.component side (i j) (p j)) := by
…

Mentions: OAI.Problem335.Bidegree.component

theorem OAI.Problem335.ProductRankAssembly.measure_component_product_le_degreeWeight line 47

Source documentation

The constrained bidegree decomposition and the nonnegative assignment sum turn per-assignment weight bounds into the product-rank estimate.

theorem measure_component_product_le_degreeWeight
    (R : MvPolynomial σ K → ℝ)
    (hzero : R 0 = 0) (hadd : ∀ p q, R (p + q) ≤ R p + R q)
    (side : σ → Bool) (p : ι → MvPolynomial σ K) (e : ι → ℕ)
    (hp : ∀ j, (p j).IsHomogeneous (e j)) (k : ℕ)
    (C q lam : ℝ) (hC : 0 ≤ C) (hq : 0 ≤ q)
    (hterm : ∀ i : ι → ℕ, (∀ j, i j ≤ e j) → (∑ j, i j) = k →
      R (∏ j, Bidegree.component side (i j) (p j)) ≤
        C * ∏ j, q ^ |(i j : ℝ) - lam * e j|) :
    R (Bidegree.component side k (∏ j, p j)) ≤
      C * ∏ j, degreeWeight q lam (e j) := by
…

Mentions: OAI.Problem335.Bidegree.component, OAI.Problem335.degreeWeight

theorem OAI.Problem335.ProductRankAssembly.measure_component_product_le_of_intermediate_bounds line 80

Source documentation

The full algebraic product-rank assembly: the remaining input is the geometric bound through the selected intermediate homogeneous space.

theorem measure_component_product_le_of_intermediate_bounds
    (R : MvPolynomial σ K → ℝ)
    (hzero : R 0 = 0) (hadd : ∀ p q, R (p + q) ≤ R p + R q)
    (side : σ → Bool) (p : ι → MvPolynomial σ K) (e : ι → ℕ)
    (hp : ∀ j, (p j).IsHomogeneous (e j)) (k : ℕ)
    (D alpha rho lam : ℝ) (hD : 0 ≤ D) (halpha : 0 < alpha)
    (hslope : (1 + rho) * lam = rho)
    (hbalance : lam * (∑ j, (e j : ℝ)) = k)
    (hterm : ∀ i : ι → ℕ, (∀ j, i j ≤ e j) → (∑ j, i j) = k →
      R (∏ j, Bidegree.component side (i j) (p j)) ≤
        2 * D * alpha ^ ((∑ j ∈ Finset.univ.filter
          (fun j => 0 < (i j : ℝ) - lam * e j), (i j : ℝ)) -
…

Mentions: OAI.Problem335.Bidegree.component

theorem OAI.Problem335.ProductRankAssembly.rank_component_product_le_of_intermediate_bounds line 114

Source documentation

Specialization to the actual finite-dimensional rank measure of a linear operator family, without any extra subadditivity hypotheses.

theorem rank_component_product_le_of_intermediate_bounds
    (A : MvPolynomial σ F →ₗ[F] (V →ₗ[F] W))
    (side : σ → Bool) (p : ι → MvPolynomial σ F) (e : ι → ℕ)
    (hp : ∀ j, (p j).IsHomogeneous (e j)) (k : ℕ)
    (D alpha rho lam : ℝ) (hD : 0 ≤ D) (halpha : 0 < alpha)
    (hslope : (1 + rho) * lam = rho)
    (hbalance : lam * (∑ j, (e j : ℝ)) = k)
    (hterm : ∀ i : ι → ℕ, (∀ j, i j ≤ e j) → (∑ j, i j) = k →
      (RankMeasure.measure A (∏ j, Bidegree.component side (i j) (p j)) : ℝ) ≤
        2 * D * alpha ^ ((∑ j ∈ Finset.univ.filter
          (fun j => 0 < (i j : ℝ) - lam * e j), (i j : ℝ)) -
          rho * (∑ j ∈ Finset.univ.filter
…

Mentions: OAI.Problem335.RankMeasure.measure, OAI.Problem335.Bidegree.component