OperatorRankBridge.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Equality of the finite-source APIs used by the product bound and the trace bound.

theorem OAI.Problem335.sourceMixedOperator_eq_rawOperatorFamily line 15
Source documentation
The independently useful source-only constructions define the same linear family.
```
theorem sourceMixedOperator_eq_rawOperatorFamily (side : σ → Bool) (a b : ℕ) :
    sourceMixedOperator (K := K) side a b = rawOperatorFamily side a b := by
…
```
Mentions: OAI.Problem335.sourceMixedOperator, OAI.Problem335.rawOperatorFamily
theorem OAI.Problem335.bidegreeRank_eq_source_measure line 21
Source documentation
The canonical rank is the source-only rank of the paired projection.
```
theorem bidegreeRank_eq_source_measure (side : σ → Bool) (a b k m : ℕ)
    (q : MvPolynomial σ K) :
    bidegreeRank side a b k m q =
      RankMeasure.measure (sourceMixedOperator side a b) (bidegreeComponent side k m q) := by
…
```
Mentions: OAI.Problem335.bidegreeRank, OAI.Problem335.RankMeasure.measure, OAI.Problem335.sourceMixedOperator, OAI.Problem335.bidegreeComponent
theorem OAI.Problem335.bidegreeRank_eq_source_component line 29
Source documentation
For a homogeneous defining polynomial, the indicator projection suffices.
```
theorem bidegreeRank_eq_source_component (side : σ → Bool) (a b k m : ℕ)
    {q : MvPolynomial σ K} (hq : q.IsHomogeneous (k + m)) :
    bidegreeRank side a b k m q =
      RankMeasure.measure (sourceMixedOperator side a b) (Bidegree.component side k q) := by
…
```
Mentions: OAI.Problem335.bidegreeRank, OAI.Problem335.RankMeasure.measure, OAI.Problem335.sourceMixedOperator, OAI.Problem335.Bidegree.component
theorem OAI.Problem335.finiteMixedOperator_rank_eq_source_measure line 36
Source documentation
The rank used in finite-matrix moment estimates equals the source-only rank.
```
theorem finiteMixedOperator_rank_eq_source_measure (side : σ → Bool) (a b k m : ℕ)
    (q : MvPolynomial σ K) :
    RankMeasure.mapRank (finiteMixedOperator side a b k m q) =
      RankMeasure.measure (sourceMixedOperator side a b) (bidegreeComponent side k m q) := by
…
```
Mentions: OAI.Problem335.RankMeasure.mapRank, OAI.Problem335.finiteMixedOperator, OAI.Problem335.RankMeasure.measure, OAI.Problem335.sourceMixedOperator, OAI.Problem335.bidegreeComponent
theorem OAI.Problem335.finiteMixedOperator_rank_eq_source_of_mem line 43
Source documentation
When projection is redundant, no conversion of defining polynomials is needed.
```
theorem finiteMixedOperator_rank_eq_source_of_mem (side : σ → Bool) (a b k m : ℕ)
    {q : MvPolynomial σ K} (hq : q ∈ bidegreeSubmodule side k m) :
    RankMeasure.mapRank (finiteMixedOperator side a b k m q) =
      RankMeasure.mapRank (sourceMixedOperator side a b q) := by
…
```
Mentions: OAI.Problem335.bidegreeSubmodule, OAI.Problem335.RankMeasure.mapRank, OAI.Problem335.finiteMixedOperator, OAI.Problem335.sourceMixedOperator