OccupationComparison.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.occupation_factorial_ratio_lower_of_le line 11

Source documentation

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

theorem occupation_factorial_ratio_lower_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
…

theorem OAI.Problem335.weighted_factorialMoment_sum_le line 28

Source documentation

Termwise occupation comparison for every nonnegative factorial-basis expansion.

theorem weighted_factorialMoment_sum_le {ι : Type*} (s : Finset ι)
    (c : ι → ℝ) (H : ι → ℕ) {t r : ℕ} (hr : 0 < r)
    (hc : ∀ i ∈ s, 0 ≤ c i) :
    (∑ i ∈ s, c i * ((t.descFactorial (H i) : ℝ) / (r.ascFactorial (H i) : ℝ))) ≤
      ∑ i ∈ s, c i * ((t : ℝ) / r) ^ H i := by
…

theorem OAI.Problem335.exp_mul_weighted_mean_sum_le line 39

Source documentation

Uniform lower occupation comparison for a nonnegative finite expansion.

theorem exp_mul_weighted_mean_sum_le {ι : Type*} (s : Finset ι)
    (c : ι → ℝ) (H : ι → ℕ) {t r H₀ : ℕ} (ht : 0 < t) (hr : 0 < r)
    (hH₀ : 2 * H₀ ≤ t) (hc : ∀ i ∈ s, 0 ≤ c i) (hH : ∀ i ∈ s, H i ≤ H₀) :
    Real.exp (-(H₀ : ℝ) ^ 2 / t - (H₀ : ℝ) ^ 2 / (2 * r)) *
        (∑ i ∈ s, c i * ((t : ℝ) / r) ^ H i) ≤
      ∑ i ∈ s, c i * ((t.descFactorial (H i) : ℝ) / (r.ascFactorial (H i) : ℝ)) := by
…

theorem OAI.Problem335.two_group_factorial_ratio_lower_of_le line 56

Source documentation

Independent variable groups multiply their moment comparisons and add losses.

theorem two_group_factorial_ratio_lower_of_le {a v b u h k H J : ℕ}
    (ha : 0 < a) (hv : 0 < v) (hb : 0 < b) (hu : 0 < u)
    (hh : h ≤ H) (hk : k ≤ J) (hH : 2 * H ≤ a) (hJ : 2 * J ≤ b) :
    Real.exp ((-(H : ℝ) ^ 2 / a - (H : ℝ) ^ 2 / (2 * v)) +
        (-(J : ℝ) ^ 2 / b - (J : ℝ) ^ 2 / (2 * u))) *
      (((a : ℝ) / v) ^ h * ((b : ℝ) / u) ^ k) ≤
    ((a.descFactorial h : ℝ) / (v.ascFactorial h : ℝ)) *
      ((b.descFactorial k : ℝ) / (u.ascFactorial k : ℝ)) := by
…

theorem OAI.Problem335.weighted_two_group_factorialMoment_sum_le line 71

Source documentation

Upper comparison for nonnegative expansions in two independent groups.

theorem weighted_two_group_factorialMoment_sum_le {ι : Type*} (s : Finset ι)
    (c : ι → ℝ) (h k : ι → ℕ) {a v b u : ℕ} (hv : 0 < v) (hu : 0 < u)
    (hc : ∀ i ∈ s, 0 ≤ c i) :
    (∑ i ∈ s, c i *
      (((a.descFactorial (h i) : ℝ) / (v.ascFactorial (h i) : ℝ)) *
       ((b.descFactorial (k i) : ℝ) / (u.ascFactorial (k i) : ℝ)))) ≤
    ∑ i ∈ s, c i * (((a : ℝ) / v) ^ h i * ((b : ℝ) / u) ^ k i) := by
…

theorem OAI.Problem335.exp_mul_weighted_two_group_mean_sum_le line 85

Source documentation

Uniform lower comparison for the two-group factorial expansions in both traces.

theorem exp_mul_weighted_two_group_mean_sum_le {ι : Type*} (s : Finset ι)
    (c : ι → ℝ) (h k : ι → ℕ) {a v b u H J : ℕ}
    (ha : 0 < a) (hv : 0 < v) (hb : 0 < b) (hu : 0 < u)
    (hH : 2 * H ≤ a) (hJ : 2 * J ≤ b) (hc : ∀ i ∈ s, 0 ≤ c i)
    (hh : ∀ i ∈ s, h i ≤ H) (hk : ∀ i ∈ s, k i ≤ J) :
    Real.exp ((-(H : ℝ) ^ 2 / a - (H : ℝ) ^ 2 / (2 * v)) +
        (-(J : ℝ) ^ 2 / b - (J : ℝ) ^ 2 / (2 * u))) *
      (∑ i ∈ s, c i * (((a : ℝ) / v) ^ h i * ((b : ℝ) / u) ^ k i)) ≤
    ∑ i ∈ s, c i *
      (((a.descFactorial (h i) : ℝ) / (v.ascFactorial (h i) : ℝ)) *
       ((b.descFactorial (k i) : ℝ) / (u.ascFactorial (k i) : ℝ))) := by
…