Documentation

LeanPool.Zeta3Irrational.Bound

LeanPool.Zeta3Irrational.Bound #

source
theorem LeanPool.Zeta3Irrational.max_value {x : ℝ} (x0 : 0 < x) (x1 : x < 1) :
√x * √(1 - x) ≤ 1 / 2
source
theorem LeanPool.Zeta3Irrational.max_value' {x : ℝ} (x0 : 0 < x) (x1 : x < 1) :
√x * (1 - x) ≤ 2 / 5
source
theorem LeanPool.Zeta3Irrational.nonneg {x : ℝ} :
0 < x → x < 1 → 0 ≤ √x * √(1 - x)
source
theorem LeanPool.Zeta3Irrational.bound_aux (x z : ℝ) (x0 : 0 < x) (x1 : x < 1) (z0 : 0 < z) :
z < 1 → 2 * √(1 - x) * √(x * z) ≤ 1 - (1 - z) * x
source
theorem LeanPool.Zeta3Irrational.bound (x y z : ℝ) (x0 : 0 < x) (x1 : x < 1) (y0 : 0 < y) (y1 : y < 1) (z0 : 0 < z) (z1 : z < 1) :
x * (1 - x) * y * (1 - y) * z * (1 - z) / ((1 - (1 - z) * x) * (1 - y * z)) < 1 / 30
source
theorem LeanPool.Zeta3Irrational.bound_aux' (x y z : ℝ) (x0 : 0 < x) :
x < 1 → ∀ (y0 : 0 < y), y < 1 → ∀ (z0 : 0 < z) (z1 : z < 1), 2 * √(1 - z) * √(x * y * z) ≤ 1 - (1 - x * y) * z
source
theorem LeanPool.Zeta3Irrational.bound'' (x y z : ℝ) (x0 : 0 < x) (x1 : x < 1) (y0 : 0 < y) (y1 : y < 1) (z0 : 0 < z) (z1 : z < 1) :
x * (1 - x) * y * (1 - y) * z * (1 - z) / (1 - (1 - x * y) * z) < 1 / 30
source
theorem LeanPool.Zeta3Irrational.bound' (x y z : ℝ) (x0 : 0 < x) (x1 : x < 1) (y0 : 0 < y) (y1 : y < 1) (z0 : 0 < z) (z1 : z < 1) :
x * (1 - x) * y * (1 - y) * z * (1 - z) / (1 - (1 - x * y) * z) < 1 / 24