OAI/Algebra/DepthFive/Bidegree.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem335.Bidegree.weight line 16

   Source documentation

   The indicator weight of the derivative-variable side of a partition.

   def weight (side : σ → Bool) (x : σ) : ℕ := if side x then 1 else 0

2. def OAI.Problem335.Bidegree.component line 19

   Source documentation

   Projection onto one degree in the selected variables.

   def component (side : σ → Bool) (i : ℕ) :
       MvPolynomial σ R →ₗ[R] MvPolynomial σ R :=
   …

3. theorem OAI.Problem335.Bidegree.coeff_component line 23
4. theorem OAI.Problem335.Bidegree.weight_add_complement line 29
5. theorem OAI.Problem335.Bidegree.weight_le_degree line 39
6. theorem OAI.Problem335.Bidegree.component_isWeightedHomogeneous line 44
7. theorem OAI.Problem335.Bidegree.component_isHomogeneous line 49
8. theorem OAI.Problem335.Bidegree.component_complement_degree line 57
9. theorem OAI.Problem335.Bidegree.component_eq_zero_of_lt line 68
10. theorem OAI.Problem335.Bidegree.sum_components line 83

    Source documentation

    A homogeneous polynomial is the sum of its bidegree components.

    theorem sum_components (side : σ → Bool) {p : MvPolynomial σ R} {n : ℕ}
        (hp : p.IsHomogeneous n) :
        (∑ i ∈ Finset.range (n + 1), component side i p) = p := by
    …

    Mentions: OAI.Problem335.Bidegree.component

11. theorem OAI.Problem335.Bidegree.component_same line 104
12. theorem OAI.Problem335.Bidegree.component_ne line 108
13. theorem OAI.Problem335.Bidegree.component_of_weightedHomogeneous line 113
14. theorem OAI.Problem335.Bidegree.prod_eq_sum_components line 121

    Source documentation

    Distributing a finite product over all choices of bidegrees.

    theorem prod_eq_sum_components {ι : Type*} [Fintype ι] [DecidableEq ι]
        (side : σ → Bool) (p : ι → MvPolynomial σ R) (e : ι → ℕ)
        (hp : ∀ a, (p a).IsHomogeneous (e a)) :
        (∏ a, p a) =
          ∑ f ∈ Fintype.piFinset (fun a => Finset.range (e a + 1)),
            ∏ a, component side (f a) (p a) := by
    …

    Mentions: OAI.Problem335.Bidegree.component

15. theorem OAI.Problem335.Bidegree.component_prod line 136

    Source documentation

    Projection of the product keeps exactly degree assignments whose sum is k.

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

    Mentions: OAI.Problem335.Bidegree.component