ActualProductRank.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Product-rank estimates specialized to the actual rounded rank parameters.

def OAI.Problem335.LowerParameters.sourceDimension line 14
Source documentation
Dimension of the source of the actual mixed operator.
```
def sourceDimension (n : ℕ) : ℝ :=
…
```
theorem OAI.Problem335.LowerParameters.sourceDimension_pos line 17
theorem OAI.Problem335.LowerParameters.slope_lambda line 22
theorem OAI.Problem335.LowerParameters.twice_k_le_a_add_v line 28
theorem OAI.Problem335.LowerParameters.actual_mixed_product_rank_le line 36
Source documentation
All numerical hypotheses of the mixed product-rank lemma hold for our chosen parameters. Only the cardinalities of the variable partition remain.
```
theorem actual_mixed_product_rank_le
    {σ K ι : Type*} [Fintype σ] [Field K] [Fintype ι] [DecidableEq ι]
    {n : ℕ} (hn : 4 ≤ n) (side : σ → Bool)
    (hvcard : Fintype.card {x : σ // side x = true} = v n)
    (hucard : Fintype.card {x : σ // side x = false} = u n)
    (Q : ι → MvPolynomial σ K) (e : ι → ℕ)
    (hQ : ∀ j, (Q j).IsHomogeneous (e j)) (he : ∑ j, e j = n) :
    (RankMeasure.mapRank (sourceMixedOperator side (a n) (b n)
      (bidegreeComponent side (k n) (m n) (∏ j, Q j))) : ℝ) ≤
      2 * sourceDimension n * ∏ j, degreeWeight (q n) (lambda n) (e j) := by
…
```
Mentions: OAI.Problem335.LowerParameters.v, OAI.Problem335.LowerParameters.u, OAI.Problem335.RankMeasure.mapRank, OAI.Problem335.sourceMixedOperator, OAI.Problem335.LowerParameters.a, OAI.Problem335.LowerParameters.b, OAI.Problem335.bidegreeComponent, OAI.Problem335.LowerParameters.k, OAI.Problem335.LowerParameters.m, OAI.Problem335.LowerParameters.sourceDimension, OAI.Problem335.degreeWeight, OAI.Problem335.LowerParameters.q, OAI.Problem335.LowerParameters.lambda
theorem OAI.Problem335.LowerParameters.sourceDimension_eq_finrank line 54
Source documentation
The dimension factor is exactly the dimension of the chosen source space.
```
theorem sourceDimension_eq_finrank {σ : Type*} [Fintype σ]
    (K : Type*) [Field K] (n : ℕ) (side : σ → Bool)
    (hvcard : Fintype.card {x : σ // side x = true} = v n)
    (hucard : Fintype.card {x : σ // side x = false} = u n) :
    sourceDimension n =
      (Module.finrank K (bidegreeSubmodule (K := K) side (a n) (b n)) : ℝ) := by
…
```
Mentions: OAI.Problem335.LowerParameters.v, OAI.Problem335.LowerParameters.u, OAI.Problem335.LowerParameters.sourceDimension, OAI.Problem335.bidegreeSubmodule, OAI.Problem335.LowerParameters.a, OAI.Problem335.LowerParameters.b

theorem OAI.Problem335.LowerParameters.actual_bidegreeRank_product_le line 64

Source documentation

The canonical finite-source rank has the actual-parameter product bound.

theorem actual_bidegreeRank_product_le
    {σ K ι : Type*} [Fintype σ] [Field K] [Fintype ι] [DecidableEq ι]
    {n : ℕ} (hn : 4 ≤ n) (side : σ → Bool)
    (hvcard : Fintype.card {x : σ // side x = true} = v n)
    (hucard : Fintype.card {x : σ // side x = false} = u n)
    (Q : ι → MvPolynomial σ K) (e : ι → ℕ)
    (hQ : ∀ j, (Q j).IsHomogeneous (e j)) (he : ∑ j, e j = n) :
    (bidegreeRank side (a n) (b n) (k n) (m n) (∏ j, Q j) : ℝ) ≤
      2 * sourceDimension n * ∏ j, degreeWeight (q n) (lambda n) (e j) := by
…

Mentions: OAI.Problem335.LowerParameters.v, OAI.Problem335.LowerParameters.u, OAI.Problem335.bidegreeRank, OAI.Problem335.LowerParameters.a, OAI.Problem335.LowerParameters.b, OAI.Problem335.LowerParameters.k, OAI.Problem335.LowerParameters.m, OAI.Problem335.LowerParameters.sourceDimension, OAI.Problem335.degreeWeight, OAI.Problem335.LowerParameters.q, OAI.Problem335.LowerParameters.lambda

theorem OAI.Problem335.LowerParameters.actual_homogeneousProductRankBound line 78
Source documentation
The full list interface consumed by the circuit estimate, with every analytic and operator-rank hypothesis discharged for the actual parameters.
```
theorem actual_homogeneousProductRankBound
    {σ K : Type*} [Fintype σ] [Field K]
    {n : ℕ} (hn : 4 ≤ n) (side : σ → Bool)
    (hvcard : Fintype.card {x : σ // side x = true} = v n)
    (hucard : Fintype.card {x : σ // side x = false} = u n) :
    HomogeneousProductRankBound
      (fun p : MvPolynomial σ K =>
        (bidegreeRank side (a n) (b n) (k n) (m n) p : ℝ))
      n (q n) (lambda n) (sourceDimension n) := by
…
```
Mentions: OAI.Problem335.LowerParameters.v, OAI.Problem335.LowerParameters.u, OAI.Problem335.HomogeneousProductRankBound, OAI.Problem335.bidegreeRank, OAI.Problem335.LowerParameters.a, OAI.Problem335.LowerParameters.b, OAI.Problem335.LowerParameters.k, OAI.Problem335.LowerParameters.m, OAI.Problem335.LowerParameters.q, OAI.Problem335.LowerParameters.lambda, OAI.Problem335.LowerParameters.sourceDimension