OAI/Algebra/DepthFive/BidegreeCompositionReindex.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.double_sum_coe_sort line 9
2. def OAI.Problem335.bidegreeAntidiagEquiv line 20

   Source documentation

   Reindex a bidegree exponent by its two finite occupation antidiagonals.

   def bidegreeAntidiagEquiv (side : σ → Bool) (a b : ℕ) :
       {d : σ →₀ ℕ // Finsupp.weight (bidegreeWeight side) d = (a,b)} ≃
         (Finset.finsuppAntidiag (Finset.univ : Finset {i // side i = true}) a) ×
         (Finset.finsuppAntidiag (Finset.univ : Finset {i // ¬ side i = true}) b) :=
   …

   Mentions: OAI.Problem335.bidegreeWeight

3. theorem OAI.Problem335.bidegreeAntidiagEquiv_join line 28
4. theorem OAI.Problem335.bidegree_sum_eq_double_antidiag line 39

   Source documentation

   Arbitrary, not necessarily separated, functions may be summed in the two groups.

   theorem bidegree_sum_eq_double_antidiag (side : σ → Bool) (a b : ℕ)
       [Fintype {d : σ →₀ ℕ // Finsupp.weight (bidegreeWeight side) d = (a,b)}]
       (f : (σ → ℕ) → ℝ) :
       (∑ d : {d : σ →₀ ℕ // Finsupp.weight (bidegreeWeight side) d = (a,b)}, f d.val) =
         ∑ M ∈ Finset.finsuppAntidiag (Finset.univ : Finset {i // side i = true}) a,
           ∑ N ∈ Finset.finsuppAntidiag (Finset.univ : Finset {i // ¬ side i = true}) b,
             f (fun i => if h : side i = true then M ⟨i,h⟩ else N ⟨i,h⟩) := by
   …

   Mentions: OAI.Problem335.bidegreeWeight

5. theorem OAI.Problem335.bidegree_average_eq_double_antidiag line 59

   Source documentation

   Uniform bidegree averages are the nested uniform occupation means.

   theorem bidegree_average_eq_double_antidiag (side : σ → Bool) (a b : ℕ)
       [Fintype {d : σ →₀ ℕ // Finsupp.weight (bidegreeWeight side) d = (a,b)}]
       (f : (σ → ℕ) → ℝ) :
       (∑ d : {d : σ →₀ ℕ // Finsupp.weight (bidegreeWeight side) d = (a,b)}, f d.val) /
         (Fintype.card {d : σ →₀ ℕ // Finsupp.weight (bidegreeWeight side) d = (a,b)} : ℝ) =
         (∑ M ∈ Finset.finsuppAntidiag (Finset.univ : Finset {i // side i = true}) a,
           (∑ N ∈ Finset.finsuppAntidiag (Finset.univ : Finset {i // ¬ side i = true}) b,
             f (fun i => if h : side i = true then M ⟨i,h⟩ else N ⟨i,h⟩)) /
             ((Finset.finsuppAntidiag (Finset.univ : Finset {i // ¬ side i = true}) b).card : ℝ)) /
           ((Finset.finsuppAntidiag (Finset.univ : Finset {i // side i = true}) a).card : ℝ) := by
   …

   Mentions: OAI.Problem335.bidegreeWeight