OccupationRatio.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.log_one_sub_ge_neg_two_mul line 11
Source documentation
The elementary logarithmic lower bound used for factorial moment ratios.
```
theorem log_one_sub_ge_neg_two_mul {x : ℝ} (hx : 0 ≤ x) (hxhalf : x ≤ 1 / 2) :
    -2 * x ≤ Real.log (1 - x) := by
…
```

theorem OAI.Problem335.exp_le_occupation_factor line 21

Source documentation

A single factor of the occupation ratio has an exponential lower bound.

theorem exp_le_occupation_factor {x y : ℝ}
    (hx : 0 ≤ x) (hxhalf : x ≤ 1 / 2) (hy : 0 ≤ y) :
    Real.exp (-2 * x - y) ≤ (1 - x) / (1 + y) := by
…

def OAI.Problem335.occupationRatio line 35
Source documentation
The finite product appearing when a composition factorial moment is normalized by the independent geometric factorial moment.
```
def occupationRatio (t r : ℝ) (H : ℕ) : ℝ :=
…
```
theorem OAI.Problem335.sum_range_cast_le_half_sq line 38
theorem OAI.Problem335.occupationRatio_le_one line 48
Source documentation
Uniform upper bound for the occupation ratio.
```
theorem occupationRatio_le_one {t r : ℝ} {H : ℕ}
    (ht : 0 < t) (hr : 0 < r) (hH : (H : ℝ) ≤ t) :
    occupationRatio t r H ≤ 1 := by
…
```
Mentions: OAI.Problem335.occupationRatio

theorem OAI.Problem335.exp_le_occupationRatio line 64

Source documentation

The exponential lower bound for the occupation ratio from the manuscript.

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

Mentions: OAI.Problem335.occupationRatio

theorem OAI.Problem335.exp_le_occupationRatio_of_le line 90

Source documentation

A common loss bound applies uniformly to all factorial orders at most H₀.

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

Mentions: OAI.Problem335.occupationRatio

theorem OAI.Problem335.occupationRatio_pos line 104
Source documentation
In the lower-bound range the ratio is strictly positive.
```
theorem occupationRatio_pos {t r : ℝ} {H : ℕ}
    (ht : 0 < t) (hr : 0 < r) (hH : (H : ℝ) ≤ t / 2) :
    0 < occupationRatio t r H :=
…
```
Mentions: OAI.Problem335.occupationRatio