IntermediateFactorization.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Factorization of mixed operators through intermediate bidegree spaces. The codomain is initially the full polynomial space. Restricting it to a bidegree submodule leaves the range dimension unchanged, as proved below.

def OAI.Problem335.sourceMixedOperator line 21
Source documentation
The full operator restricted to a finite-bidegree source, as a linear family in the polynomial defining the operator.
```
def sourceMixedOperator (isV : σ → Bool) (a b : ℕ) :
    MvPolynomial σ K →ₗ[K]
      (bidegreeSubmodule (K := K) isV a b →ₗ[K] MvPolynomial σ K) where
…
```
Mentions: OAI.Problem335.bidegreeSubmodule
theorem OAI.Problem335.sourceMixedOperator_apply line 32
def OAI.Problem335.intermediateStart line 37
Source documentation
The operator for p maps the source into the proposed intermediate space.
```
def intermediateStart (isV : σ → Bool) (a b c d : ℕ)
    (p : MvPolynomial σ K)
    (h : ∀ f : bidegreeSubmodule (K := K) isV a b,
…
```
Mentions: OAI.Problem335.bidegreeSubmodule
theorem OAI.Problem335.sourceMixedOperator_mul_factorization line 46
Source documentation
Factorization is an equality of actual linear maps, not merely a rank inequality. The rightmost polynomial factor operates first.
```
theorem sourceMixedOperator_mul_factorization (isV : σ → Bool) (a b c d : ℕ)
    (p q : MvPolynomial σ K)
    (h : ∀ f : bidegreeSubmodule (K := K) isV a b,
…
```
Mentions: OAI.Problem335.bidegreeSubmodule
theorem OAI.Problem335.sourceMixedOperator_mul_rank_le line 59
Source documentation
Any factorization through an intermediate bidegree space bounds rank by that space's dimension.
```
theorem sourceMixedOperator_mul_rank_le [Finite σ]
    (isV : σ → Bool) (a b c d : ℕ) (p q : MvPolynomial σ K)
    (h : ∀ f : bidegreeSubmodule (K := K) isV a b,
…
```
Mentions: OAI.Problem335.bidegreeSubmodule

theorem OAI.Problem335.selected_bidegree_product_mem line 70

Source documentation

The bidegree of a selected subproduct is the sum of the selected bidegrees, with no condition on the unselected factors.

theorem selected_bidegree_product_mem {ι : Type*} (s : Finset ι)
    (selected : ι → Prop) [DecidablePred selected]
    (Q : ι → MvPolynomial σ K) (i j : ι → ℕ) (isV : σ → Bool)
    (hQ : ∀ l ∈ s, Q l ∈ bidegreeSubmodule isV (i l) (j l)) :
    (∏ l ∈ s.filter selected, Q l) ∈
      bidegreeSubmodule isV (∑ l ∈ s.filter selected, i l)
        (∑ l ∈ s.filter selected, j l) := by
…

Mentions: OAI.Problem335.bidegreeSubmodule

theorem OAI.Problem335.sourceMixedOperator_prod_rank_le line 86
Source documentation
In a commutative polynomial product, any chosen group of factors can be applied first. In the product-rank proof this group consists of the factors with positive proportional bidegree discrepancy.
```
theorem sourceMixedOperator_prod_rank_le [Finite σ] {ι : Type*}
    (s : Finset ι) (selected : ι → Prop) [DecidablePred selected]
    (Q : ι → MvPolynomial σ K) (isV : σ → Bool) (a b c d : ℕ)
    (h : ∀ f : bidegreeSubmodule (K := K) isV a b,
…
```
Mentions: OAI.Problem335.bidegreeSubmodule

theorem OAI.Problem335.sourceMixedOperator_homogeneous_prod_rank_le line 100

Source documentation

A selected homogeneous subproduct gives the actual intermediate dimension bound. Only its total derivative degree needs to fit inside the source.

theorem sourceMixedOperator_homogeneous_prod_rank_le [Finite σ] {ι : Type*}
    (s : Finset ι) (selected : ι → Prop) [DecidablePred selected]
    (Q : ι → MvPolynomial σ K) (i j : ι → ℕ) (isV : σ → Bool) (a b : ℕ)
    (hQ : ∀ l ∈ s, Q l ∈ bidegreeSubmodule isV (i l) (j l))
    (hi : (∑ l ∈ s.filter selected, i l) ≤ a) :
    RankMeasure.mapRank (sourceMixedOperator isV a b (∏ l ∈ s, Q l)) ≤
      Module.finrank K (bidegreeSubmodule (K := K) isV
…

Mentions: OAI.Problem335.bidegreeSubmodule, OAI.Problem335.RankMeasure.mapRank, OAI.Problem335.sourceMixedOperator

theorem OAI.Problem335.sourceMixedOperator_component_prod_rank_le line 117

Source documentation

Specialization to the component product belonging to one bidegree assignment. This is the geometric rank estimate used before summing over assignments in the product-rank lemma.

theorem sourceMixedOperator_component_prod_rank_le [Finite σ] {ι : Type*}
    (s : Finset ι) (selected : ι → Prop) [DecidablePred selected]
    (Q : ι → MvPolynomial σ K) (e i : ι → ℕ) (isV : σ → Bool) (a b : ℕ)
    (hi : (∑ l ∈ s.filter selected, i l) ≤ a) :
    RankMeasure.mapRank (sourceMixedOperator isV a b
      (∏ l ∈ s, bidegreeComponent isV (i l) (e l - i l) (Q l))) ≤
      Module.finrank K (bidegreeSubmodule (K := K) isV
…

Mentions: OAI.Problem335.RankMeasure.mapRank, OAI.Problem335.sourceMixedOperator, OAI.Problem335.bidegreeComponent, OAI.Problem335.bidegreeSubmodule

theorem OAI.Problem335.sourceMixedOperator_component_prod_rank_le_of_sum_le line 133

Source documentation

A total derivative-degree bound suffices for every selection of factors. This version is convenient for constrained assignments whose degrees sum to k.

theorem sourceMixedOperator_component_prod_rank_le_of_sum_le [Finite σ]
    {ι : Type*} (s : Finset ι) (selected : ι → Prop) [DecidablePred selected]
    (Q : ι → MvPolynomial σ K) (e i : ι → ℕ) (isV : σ → Bool) (a b : ℕ)
    (hi : (∑ l ∈ s, i l) ≤ a) :
    RankMeasure.mapRank (sourceMixedOperator isV a b
      (∏ l ∈ s, bidegreeComponent isV (i l) (e l - i l) (Q l))) ≤
      Module.finrank K (bidegreeSubmodule (K := K) isV
…

Mentions: OAI.Problem335.RankMeasure.mapRank, OAI.Problem335.sourceMixedOperator, OAI.Problem335.bidegreeComponent, OAI.Problem335.bidegreeSubmodule

theorem OAI.Problem335.mapRank_subtype_comp line 148
Source documentation
Passing from a fixed-bidegree codomain to the full polynomial codomain does not alter the dimension of the range.
```
theorem mapRank_subtype_comp {V : Type*} [AddCommGroup V] [Module K V]
    (Z : Submodule K (MvPolynomial σ K)) (f : V →ₗ[K] Z) :
    RankMeasure.mapRank (Z.subtype.comp f) = RankMeasure.mapRank f := by
…
```
Mentions: OAI.Problem335.RankMeasure.mapRank
theorem OAI.Problem335.sourceMixedOperator_codRestrict_rank line 157
Source documentation
Consequently a codomain-restricted mixed operator and its source-only restriction have exactly the same rank.
```
theorem sourceMixedOperator_codRestrict_rank (isV : σ → Bool) (a b c d : ℕ)
    (p : MvPolynomial σ K)
    (h : ∀ f : bidegreeSubmodule (K := K) isV a b,
…
```
Mentions: OAI.Problem335.bidegreeSubmodule