OAI/Algebra/DepthFive/OccupationRatioAlgebra.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.occupationRatio_mul_mean_pow line 11

   Source documentation

   Algebraic removal of the geometric normalization from the occupation ratio.

   theorem occupationRatio_mul_mean_pow {t r : ℝ} (ht : 0 < t) (hr : 0 < r) (H : ℕ) :
       occupationRatio t r H * (t / r) ^ H =
         (∏ j ∈ Finset.range H, (t - (j : ℝ))) /
           (∏ j ∈ Finset.range H, (r + (j : ℝ))) := by
   …

   Mentions: OAI.Problem335.occupationRatio

2. theorem OAI.Problem335.descFactorial_div_ascFactorial_eq_ratio line 24

   Source documentation

   The exact factorial-moment ratio over weak compositions.

   theorem descFactorial_div_ascFactorial_eq_ratio {t r H : ℕ}
       (ht : 0 < t) (hr : 0 < r) (hH : H ≤ t) :
       (t.descFactorial H : ℝ) / (r.ascFactorial H : ℝ) =
         occupationRatio t r H * ((t : ℝ) / r) ^ H := by
   …

   Mentions: OAI.Problem335.occupationRatio

3. theorem OAI.Problem335.descFactorial_div_ascFactorial_le_mean_pow line 40

   Source documentation

   Every factorial order admits the independent geometric upper comparison.

   theorem descFactorial_div_ascFactorial_le_mean_pow {t r H : ℕ}
       (ht : 0 < t) (hr : 0 < r) :
       (t.descFactorial H : ℝ) / (r.ascFactorial H : ℝ) ≤ ((t : ℝ) / r) ^ H := by
   …

4. theorem OAI.Problem335.exp_mul_mean_pow_le_descFactorial_div_ascFactorial line 56

   Source documentation

   The lower comparison is uniform over all factorial orders up to half the total.

   theorem exp_mul_mean_pow_le_descFactorial_div_ascFactorial {t r H : ℕ}
       (ht : 0 < t) (hr : 0 < r) (hH : 2 * H ≤ t) :
       Real.exp (-(H : ℝ) ^ 2 / t - (H : ℝ) ^ 2 / (2 * r)) *
           ((t : ℝ) / r) ^ H ≤ (t.descFactorial H : ℝ) / (r.ascFactorial H : ℝ) := by
   …

5. theorem OAI.Problem335.exp_mul_mean_pow_le_descFactorial_div_ascFactorial_of_le line 68

   Source documentation

   A common loss bound can be used for all orders bounded by H₀.

   theorem exp_mul_mean_pow_le_descFactorial_div_ascFactorial_of_le {t r H H₀ : ℕ}
       (ht : 0 < t) (hr : 0 < r) (hH : H ≤ H₀) (hH₀ : 2 * H₀ ≤ t) :
       Real.exp (-(H₀ : ℝ) ^ 2 / t - (H₀ : ℝ) ^ 2 / (2 * r)) *
           ((t : ℝ) / r) ^ H ≤ (t.descFactorial H : ℝ) / (r.ascFactorial H : ℝ) := by
   …

6. theorem OAI.Problem335.descFactorial_div_ascFactorial_le_mean_pow_of_pos line 85

   Source documentation

   Zero total occupation is also allowed in the geometric upper comparison.

   theorem descFactorial_div_ascFactorial_le_mean_pow_of_pos {t r H : ℕ} (hr : 0 < r) :
       (t.descFactorial H : ℝ) / (r.ascFactorial H : ℝ) ≤ ((t : ℝ) / r) ^ H := by
   …