English
The function log_b is defined by log_b x = log x / log b for real b ≠ 0, with log_b 0 understood as 0 and logb b x as log x / log b.
Русский
Функция log_b задается как log_b x = log x / log b при b ≠ 0, logb b 0 трактуется как 0, а logb b x как log x / log b.
LaTeX
$$$$\text{log}_b x = \frac{\log x}{\log b} \quad (b \neq 0).$$$$
Lean4
theorem finite_integral_rpow_sub_one_pow_aux {r : ℝ} (n : ℕ) (hnr : (n : ℝ) < r) :
(∫⁻ x : ℝ in Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n)) < ∞ :=
by
have hr : 0 < r := lt_of_le_of_lt n.cast_nonneg hnr
have h_int x (hx : x ∈ Ioc (0 : ℝ) 1) := by
calc
ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ .ofReal ((x ^ (-r⁻¹) - 0) ^ n) :=
by
gcongr
· rw [sub_nonneg]
exact Real.one_le_rpow_of_pos_of_le_one_of_nonpos hx.1 hx.2 (by simpa using hr.le)
· simp
_ = .ofReal (x ^ (-(r⁻¹ * n))) := by simp [rpow_mul hx.1.le, ← neg_mul]
refine lt_of_le_of_lt (setLIntegral_mono' measurableSet_Ioc h_int) ?_
refine IntegrableOn.setLIntegral_lt_top ?_
rw [← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]
apply intervalIntegral.intervalIntegrable_rpow'
rwa [neg_lt_neg_iff, inv_mul_lt_iff₀' hr, one_mul]
