OAI/Algebra/DepthFive/BidegreeOccupationSum.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.bidegreeExponentsEquiv_fst_apply line 11
2. theorem OAI.Problem335.bidegreeExponentsEquiv_snd_apply line 16
3. theorem OAI.Problem335.bidegreeExponentsEquiv_symm_true line 21
4. theorem OAI.Problem335.bidegreeExponentsEquiv_symm_false line 29
5. theorem OAI.Problem335.sum_bidegree_occupation_products line 44

   Source documentation

   Uniform bidegree exponents split into the independent uniform occupation vectors of the differentiated and multiplied coordinate sets.

   theorem sum_bidegree_occupation_products
       (s : Finset {i // isV i = true}) (t : Finset {i // ¬ isV i = true}) :
       (∑ d : {d : σ →₀ ℕ // Finsupp.weight (bidegreeWeight isV) d = (a, b)},
         (∏ i ∈ s, (d.1 i : ℝ)) * (∏ i ∈ t, ((d.1 i : ℝ) + 1))) =
       (∑ d : {d : {i // isV i = true} → ℕ // ∑ i, d i = a},
         ∏ i ∈ s, (d.1 i : ℝ)) *
       (∑ d : {d : {i // ¬ isV i = true} → ℕ // ∑ i, d i = b},
         ∏ i ∈ t, ((d.1 i : ℝ) + 1)) := by
   …

   Mentions: OAI.Problem335.bidegreeWeight

6. theorem OAI.Problem335.mean_bidegree_occupation_products line 61

   Source documentation

   The corresponding normalized-average identity. It remains valid for empty index sets because both sides use the field convention for division by zero.

   theorem mean_bidegree_occupation_products
       (s : Finset {i // isV i = true}) (t : Finset {i // ¬ isV i = true}) :
       (∑ d : {d : σ →₀ ℕ // Finsupp.weight (bidegreeWeight isV) d = (a, b)},
         (∏ i ∈ s, (d.1 i : ℝ)) * (∏ i ∈ t, ((d.1 i : ℝ) + 1))) /
         Fintype.card {d : σ →₀ ℕ // Finsupp.weight (bidegreeWeight isV) d = (a, b)} =
       ((∑ d : {d : {i // isV i = true} → ℕ // ∑ i, d i = a},
         ∏ i ∈ s, (d.1 i : ℝ)) /
         Fintype.card {d : {i // isV i = true} → ℕ // ∑ i, d i = a}) *
       ((∑ d : {d : {i // ¬ isV i = true} → ℕ // ∑ i, d i = b},
         ∏ i ∈ t, ((d.1 i : ℝ) + 1)) /
         Fintype.card {d : {i // ¬ isV i = true} → ℕ // ∑ i, d i = b}) := by
   …

   Mentions: OAI.Problem335.bidegreeWeight