OAI/Algebra/DepthFive/OccupationSum.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem335.fallingFactorialSeries line 10
2. lemma OAI.Problem335.fallingFactorialSeries_eq line 13
3. lemma OAI.Problem335.fallingFactorialSeries_prod line 25
4. theorem OAI.Problem335.occupation_factorial_sum line 37

   Source documentation

   Exact weighted weak-composition sum, with the impossible-degree case explicitly zero. This is the coefficient-extraction form of the occupation factorial moment identity.

   theorem occupation_factorial_sum {ι : Type*} [Fintype ι] [DecidableEq ι] [Nonempty ι]
       (d : ι → ℕ) (t : ℕ) :
       (∑ M ∈ Finset.finsuppAntidiag (Finset.univ : Finset ι) t,
         ∏ i, ((M i).descFactorial (d i) : ℝ)) =
         (∏ i, (d i).factorial : ℝ) *
           if (∑ i, d i) ≤ t then
             ((t + Fintype.card ι - 1).choose (t - ∑ i, d i) : ℝ) else 0 := by
   …

5. theorem OAI.Problem335.occupation_composition_card line 70

   Source documentation

   Stars-and-bars count for the same finite weak-composition index set.

   theorem occupation_composition_card {ι : Type*} [Fintype ι] [DecidableEq ι] [Nonempty ι] (t : ℕ) :
       (Finset.finsuppAntidiag (Finset.univ : Finset ι) t).card =
         (t + Fintype.card ι - 1).choose t := by
   …

6. lemma OAI.Problem335.occupation_choose_ratio line 78
7. theorem OAI.Problem335.occupation_factorial_moment line 101

   Source documentation

   The normalized factorial moment of the uniform distribution on weak compositions. The result includes total orders above t, where both sides vanish.

   theorem occupation_factorial_moment {ι : Type*} [Fintype ι] [DecidableEq ι]
       [Nonempty ι] (d : ι → ℕ) (t : ℕ) :
       (∑ M ∈ Finset.finsuppAntidiag (Finset.univ : Finset ι) t,
         ∏ i, ((M i).descFactorial (d i) : ℝ)) /
           (Finset.finsuppAntidiag (Finset.univ : Finset ι) t).card =
         (t.descFactorial (∑ i, d i) : ℝ) /
           ((Fintype.card ι).ascFactorial (∑ i, d i) : ℝ) *
             (∏ i, (d i).factorial : ℝ) := by
   …