PolynomialVariableSupport.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Variables absent from the arithmetic coefficient tests

Clearing ancestor denominators introduces only variables from the existing slots. In particular a compensation type omitted from those slots stays absent from every coefficient polynomial and every minor formed from them.

def OAI.Ostmann.PolynomialGiantRows.UsesOnly line 18
theorem OAI.Ostmann.PolynomialGiantRows.vars_mul_subset line 22
theorem OAI.Ostmann.PolynomialGiantRows.vars_sub_subset line 26
theorem OAI.Ostmann.PolynomialGiantRows.usesOnly_identity line 30
theorem OAI.Ostmann.PolynomialGiantRows.usesOnly_reverse line 33

theorem OAI.Ostmann.PolynomialGiantRows.minor_usesOnly line 48

Source documentation

A two-by-two minor has no variables beyond those of its four entries.

theorem minor_usesOnly [DecidableEq σ] {a b c d : MvPolynomial σ ℤ} {S : Finset σ}
    (ha : a.vars ⊆ S) (hb : b.vars ⊆ S) (hc : c.vars ⊆ S) (hd : d.vars ⊆ S) :
    (a * d - b * c).vars ⊆ S :=
…

theorem OAI.Ostmann.PolynomialGiantRows.normalized_eq_of_agree line 56
Source documentation
Changing all variables outside the indicated slots leaves both normalized coefficient rows unchanged. This supplies the independence needed for the separate compensation-prime prior in the coincidence estimate.
```
theorem normalized_eq_of_agree {K : Type*} [Field K]
    (T : PolynomialGiantRows σ) (S : Finset σ) (hT : T.UsesOnly S)
    (x y : σ → K) (hxy : ∀ i ∈ S, x i = y i) :
    T.normalized (MvPolynomial.eval₂Hom (Int.castRingHom K) x) =
      T.normalized (MvPolynomial.eval₂Hom (Int.castRingHom K) y) := by
…
```
Mentions: OAI.Ostmann.PolynomialGiantRows

theorem OAI.Ostmann.PolynomialGiantRows.minor_degree_le line 70

Source documentation

Forming a rank test doubles the available coefficient degree bound.

theorem minor_degree_le {a b c d : MvPolynomial σ ℤ} (D : ℕ)
    (ha : a.totalDegree ≤ D) (hb : b.totalDegree ≤ D)
    (hc : c.totalDegree ≤ D) (hd : d.totalDegree ≤ D) :
    (a * d - b * c).totalDegree ≤ 2 * D := by
…

theorem OAI.Ostmann.polynomialAncestorRows_usesOnly line 80