English
For hc_ge ≥ (2)⁻¹ and hc_le ≥ c ≤ 1, we have 0 ≤ logRatio(c).
Русский
Для hc_ge ≥ (1/2) и hc_le в отношении c ≤ 1 имеем 0 ≤ logRatio(c).
LaTeX
$$\\text{If } (2)^{-1} \\le c \\le 1, \\quad 0 \\le \\operatorname{logRatio}(c)$$
Lean4
theorem logRatio_mul_normThreshold_add_one_le {c : ℝ≥0∞} (hc_gt : (2 : ℝ≥0∞)⁻¹ < c) (hc_lt : c < 1) (n : ℕ) :
logRatio c * normThreshold a (n + 1) ^ 2 * a⁻¹ ^ 2 ≤ 2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n :=
by
by_cases ha : a = 0
· simp only [ha, inv_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, mul_zero, Nat.ofNat_pos, pow_pos,
mul_nonneg_iff_of_pos_right, inv_pos, mul_nonneg_iff_of_pos_left]
refine Real.log_nonneg ?_
rw [one_le_div]
· refine (ENNReal.toReal_le_toReal (by finiteness) (by finiteness)).mpr ?_
refine tsub_le_iff_left.mpr ?_
rw [← two_mul]
rw [inv_eq_one_div, ENNReal.div_lt_iff (by simp) (by simp), mul_comm] at hc_gt
exact hc_gt.le
· simp only [ENNReal.toReal_pos_iff, tsub_pos_iff_lt, hc_lt, true_and]
finiteness
calc
logRatio c * normThreshold a (n + 1) ^ 2 * a⁻¹ ^ 2
_ ≤ logRatio c * (a ^ 2 * (1 + √2) ^ 2 * 2 ^ (n + 2)) * a⁻¹ ^ 2 :=
by
gcongr
· exact (logRatio_pos hc_gt hc_lt).le
· exact sq_normThreshold_add_one_le n
_ = 2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n :=
by
unfold logRatio
field_simp
ring
