BidegreeBridge.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.bidegreeWeight_eq_pair line 15

Source documentation

The paired weight is exactly the two complementary indicator weights.

theorem bidegreeWeight_eq_pair (side : σ → Bool) (d : σ →₀ ℕ) :
    Finsupp.weight (bidegreeWeight side) d =
      (Finsupp.weight (Bidegree.weight side) d,
       Finsupp.weight (Bidegree.weight (fun x => !(side x))) d) := by
…

Mentions: OAI.Problem335.bidegreeWeight, OAI.Problem335.Bidegree.weight

theorem OAI.Problem335.mem_bidegreeSubmodule_iff_indicator line 27
theorem OAI.Problem335.bidegreeComponent_sub_eq_component line 47
Source documentation
On total degree n, a single degree projection already fixes the other degree.
```
theorem bidegreeComponent_sub_eq_component (side : σ → Bool) (i : ℕ)
    {p : MvPolynomial σ R} {n : ℕ} (hp : p.IsHomogeneous n) :
    bidegreeComponent side i (n - i) p = Bidegree.component side i p := by
…
```
Mentions: OAI.Problem335.bidegreeComponent, OAI.Problem335.Bidegree.component
theorem OAI.Problem335.bidegreeComponent_eq_component line 65
theorem OAI.Problem335.component_mem_bidegreeSubmodule line 70
theorem OAI.Problem335.sum_bidegreeComponents line 76

theorem OAI.Problem335.bidegreeComponent_prod line 83

Source documentation

The product-rank expansion, expressed in the paired bidegree API.

theorem bidegreeComponent_prod {ι : Type*} [Fintype ι] [DecidableEq ι]
    (side : σ → Bool) (p : ι → MvPolynomial σ R) (e : ι → ℕ)
    (hp : ∀ a, (p a).IsHomogeneous (e a)) (k m : ℕ)
    (hkm : k + m = ∑ a, e a) :
    bidegreeComponent side k m (∏ a, p a) =
      ∑ f ∈ Fintype.piFinset (fun a => Finset.range (e a + 1)),
        if (∑ a, f a) = k then
          ∏ a, bidegreeComponent side (f a) (e a - f a) (p a) else 0 := by
…

Mentions: OAI.Problem335.bidegreeComponent

theorem OAI.Problem335.component_product_mem_bidegree line 100

Source documentation

A summand in the constrained expansion has the intended target bidegree.

theorem component_product_mem_bidegree {ι : Type*} [Fintype ι]
    (side : σ → Bool) (p : ι → MvPolynomial σ R) (e f : ι → ℕ)
    (hp : ∀ a, (p a).IsHomogeneous (e a)) (k m : ℕ)
    (hkm : k + m = ∑ a, e a) (hf : ∑ a, f a = k) :
    (∏ a, Bidegree.component side (f a) (p a)) ∈ bidegreeSubmodule side k m := by
…

Mentions: OAI.Problem335.Bidegree.component, OAI.Problem335.bidegreeSubmodule