FractionRounding.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.fraction_rounding_ratio_bounds line 9

Source documentation

Quantitative monotonicity of the fraction used in the rounded rank parameters.

theorem fraction_rounding_ratio_bounds {x v a : ℝ} (hx : 0 < x) (hv : 0 < v)
    (hxa : x ≤ a) (hax : a ≤ x + 1) :
    1 ≤ (a / (a + v)) / (x / (x + v)) ∧
      (a / (a + v)) / (x / (x + v)) ≤ 1 + 1 / x := by
…

theorem OAI.Problem335.fraction_rounding_log_bounds line 28

Source documentation

Rounding upward by at most one changes the logarithm by at most 1/x.

theorem fraction_rounding_log_bounds {x v a : ℝ} (hx : 0 < x) (hv : 0 < v)
    (hxa : x ≤ a) (hax : a ≤ x + 1) :
    0 ≤ Real.log ((a / (a + v)) / (x / (x + v))) ∧
      Real.log ((a / (a + v)) / (x / (x + v))) ≤ 1 / x := by
…

theorem OAI.Problem335.fraction_rounding_log_le_two_div line 40

Source documentation

Once the unrounded value is at least one, the logarithmic loss is 2/a.

theorem fraction_rounding_log_le_two_div {x v a : ℝ} (hx : 1 ≤ x) (hv : 0 < v)
    (hxa : x ≤ a) (hax : a ≤ x + 1) :
    Real.log ((a / (a + v)) / (x / (x + v))) ≤ 2 / a := by
…

theorem OAI.Problem335.fraction_rounding_bounds line 50

Source documentation

Equivalent multiplicative exponential form of the rounding estimate.

theorem fraction_rounding_bounds {x v a : ℝ} (hx : 0 < x) (hv : 0 < v)
    (hxa : x ≤ a) (hax : a ≤ x + 1) :
    x / (x + v) ≤ a / (a + v) ∧
      a / (a + v) ≤ x / (x + v) * Real.exp (1 / x) := by
…

theorem OAI.Problem335.fraction_natCeil_log_bounds line 64

Source documentation

The ceiling specialization used for both parameters a and b.

theorem fraction_natCeil_log_bounds {x v : ℝ} (hx : 0 < x) (hv : 0 < v) :
    0 ≤ Real.log (((⌈x⌉₊ : ℝ) / ((⌈x⌉₊ : ℝ) + v)) / (x / (x + v))) ∧
      Real.log (((⌈x⌉₊ : ℝ) / ((⌈x⌉₊ : ℝ) + v)) / (x / (x + v))) ≤ 1 / x := by
…

theorem OAI.Problem335.fraction_natCeil_inverse_bounds line 72
Source documentation
The first rank parameter has ideal fraction 1/s; here s = sqrt n.
```
theorem fraction_natCeil_inverse_bounds {s v : ℝ} (hs : 1 < s) (hv : 0 < v) :
    let a : ℝ := ⌈v / (s - 1)⌉₊
…
```
theorem OAI.Problem335.fraction_natCeil_reciprocal_le line 87
Source documentation
The first rounded parameter has reciprocal at most its ideal reciprocal.
```
theorem fraction_natCeil_reciprocal_le {s v : ℝ} (hs : 1 < s) (hv : 0 < v) :
    let a : ℝ := ⌈v / (s - 1)⌉₊
…
```
theorem OAI.Problem335.fraction_natCeil_target_bounds line 100
Source documentation
The second rank parameter is rounded from a prescribed target fraction p.
```
theorem fraction_natCeil_target_bounds {p v : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hv : 0 < v) :
    let b : ℝ := ⌈v * p / (1 - p)⌉₊
…
```