FiniteOperator.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

The finite-source rank measure and its product decomposition.

def OAI.Problem335.rawOperatorFamily line 19
Source documentation
The full substitution operator restricted to a fixed bidegree source. Keeping the ambient polynomial codomain avoids unnecessary degree transports.
```
def rawOperatorFamily (isV : σ → Bool) (a b : ℕ) :
    MvPolynomial σ K →ₗ[K]
      (bidegreeSubmodule (K := K) isV a b →ₗ[K] MvPolynomial σ K) :=
…
```
Mentions: OAI.Problem335.bidegreeSubmodule
theorem OAI.Problem335.rawOperatorFamily_apply line 25
def OAI.Problem335.bidegreeOperatorFamily line 30
Source documentation
Project the defining polynomial to bidegree (k,m) before substitution.
```
def bidegreeOperatorFamily (isV : σ → Bool) (a b k m : ℕ) :
    MvPolynomial σ K →ₗ[K]
      (bidegreeSubmodule (K := K) isV a b →ₗ[K] MvPolynomial σ K) :=
…
```
Mentions: OAI.Problem335.bidegreeSubmodule
theorem OAI.Problem335.bidegreeOperatorFamily_apply line 35
def OAI.Problem335.bidegreeRank line 41
Source documentation
The rank measure from the manuscript, with an ambient codomain.
```
def bidegreeRank (isV : σ → Bool) (a b k m : ℕ) (q : MvPolynomial σ K) : ℕ :=
…
```
theorem OAI.Problem335.bidegreeRank_zero line 44
theorem OAI.Problem335.bidegreeRank_smul line 48
theorem OAI.Problem335.bidegreeRank_add_le line 53
theorem OAI.Problem335.bidegreeRank_sum_le line 59
theorem OAI.Problem335.bidegreeRank_eq_raw_of_mem line 65

theorem OAI.Problem335.bidegreeOperatorFamily_product line 73

Source documentation

The projected product map is a sum of maps with fixed factor bidegrees.

theorem bidegreeOperatorFamily_product {ι : Type*} [Fintype ι] [DecidableEq ι]
    (isV : σ → Bool) (a b k m : ℕ) (e : ι → ℕ)
    (q : ι → MvPolynomial σ K) (hq : ∀ j, (q j).IsHomogeneous (e j)) :
    bidegreeOperatorFamily isV a b k m (∏ j, q j) =
      ∑ d : (∀ j : ι, Fin (e j + 1)),
        if (∑ j : ι, (d j : ℕ)) = k ∧ (∑ j : ι, (e j - (d j : ℕ))) = m then
          rawOperatorFamily isV a b
            (∏ j, bidegreeComponent isV (d j) (e j - d j) (q j))
        else 0 := by
…

Mentions: OAI.Problem335.bidegreeOperatorFamily, OAI.Problem335.rawOperatorFamily, OAI.Problem335.bidegreeComponent

theorem OAI.Problem335.bidegreeRank_product_le line 91

Source documentation

Subadditivity reduces product rank to the constrained assignments.

theorem bidegreeRank_product_le [Finite σ] {ι : Type*} [Fintype ι] [DecidableEq ι]
    (isV : σ → Bool) (a b k m : ℕ) (e : ι → ℕ)
    (q : ι → MvPolynomial σ K) (hq : ∀ j, (q j).IsHomogeneous (e j)) :
    bidegreeRank isV a b k m (∏ j, q j) ≤
      ∑ d : (∀ j : ι, Fin (e j + 1)),
        if (∑ j : ι, (d j : ℕ)) = k ∧ (∑ j : ι, (e j - (d j : ℕ))) = m then
          RankMeasure.mapRank (rawOperatorFamily isV a b
            (∏ j, bidegreeComponent isV (d j) (e j - d j) (q j)))
        else 0 := by
…

Mentions: OAI.Problem335.bidegreeRank, OAI.Problem335.RankMeasure.mapRank, OAI.Problem335.rawOperatorFamily, OAI.Problem335.bidegreeComponent

theorem OAI.Problem335.rawOperatorFamily_rank_codRestrict line 115
Source documentation
Replacing an ambient codomain with any subspace containing the image preserves the rank measure exactly.
```
theorem rawOperatorFamily_rank_codRestrict (isV : σ → Bool) (a b : ℕ)
    (q : MvPolynomial σ K) (T : Submodule K (MvPolynomial σ K))
    (hT : ∀ p : bidegreeSubmodule (K := K) isV a b,
…
```
Mentions: OAI.Problem335.bidegreeSubmodule
def OAI.Problem335.finiteMixedOperator line 127
Source documentation
The finite-dimensional operator with its exact target bidegree. The map is zero when k > a, so no degree-inequality argument is needed.
```
def finiteMixedOperator (isV : σ → Bool) (a b k m : ℕ) :
    MvPolynomial σ K →ₗ[K]
      (bidegreeSubmodule (K := K) isV a b →ₗ[K]
…
```
Mentions: OAI.Problem335.bidegreeSubmodule
theorem OAI.Problem335.finiteMixedOperator_apply_coe line 142

theorem OAI.Problem335.finiteMixedOperator_apply_of_mem line 148

Source documentation

On a polynomial of bidegree (k,m), projection is redundant.

theorem finiteMixedOperator_apply_of_mem (isV : σ → Bool) (a b k m : ℕ)
    {q : MvPolynomial σ K} (hq : q ∈ bidegreeSubmodule isV k m)
    (p : bidegreeSubmodule (K := K) isV a b) :
…

Mentions: OAI.Problem335.bidegreeSubmodule

theorem OAI.Problem335.finiteMixedOperator_rank line 156
Source documentation
The intrinsic finite-dimensional map and the ambient-codomain rank agree.
```
theorem finiteMixedOperator_rank (isV : σ → Bool) (a b k m : ℕ)
    (q : MvPolynomial σ K) :
    RankMeasure.mapRank (finiteMixedOperator isV a b k m q) =
      bidegreeRank isV a b k m q := by
…
```
Mentions: OAI.Problem335.RankMeasure.mapRank, OAI.Problem335.finiteMixedOperator, OAI.Problem335.bidegreeRank