English
logb 0 x = 0 for all x.
Русский
logb 0 x = 0 для всех x.
LaTeX
$$$$log_b 0 = 0.$$$$
Lean4
theorem finite_integral_one_add_norm {r : ℝ} (hnr : (finrank ℝ E : ℝ) < r) :
(∫⁻ x : E, ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) ∂μ) < ∞ :=
by
have hr : 0 < r := lt_of_le_of_lt (finrank ℝ E).cast_nonneg hnr
have h_meas : Measurable fun ω : E => (1 + ‖ω‖) ^ (-r) := by fun_prop
have h_pos : ∀ x : E, 0 ≤ (1 + ‖x‖) ^ (-r) := fun x ↦ by positivity
rw [lintegral_eq_lintegral_meas_le μ (Eventually.of_forall h_pos) h_meas.aemeasurable]
have h_int : ∀ t, 0 < t → μ {a : E | t ≤ (1 + ‖a‖) ^ (-r)} = μ (Metric.closedBall (0 : E) (t ^ (-r⁻¹) - 1)) :=
fun t ht ↦ by
congr 1
ext x
simp only [mem_setOf_eq, mem_closedBall_zero_iff]
exact le_rpow_one_add_norm_iff_norm_le hr (mem_Ioi.mp ht) x
rw [setLIntegral_congr_fun measurableSet_Ioi h_int]
set f := fun t : ℝ ↦ μ (Metric.closedBall (0 : E) (t ^ (-r⁻¹) - 1))
set mB :=
μ
(Metric.ball (0 : E) 1)
-- the next two inequalities are in fact equalities but we don't need that
calc
∫⁻ t in Ioi 0, f t ≤ ∫⁻ t in Ioc 0 1 ∪ Ioi 1, f t := lintegral_mono_set Ioi_subset_Ioc_union_Ioi
_ ≤ (∫⁻ t in Ioc 0 1, f t) + ∫⁻ t in Ioi 1, f t := (lintegral_union_le _ _ _)
_ < ∞ := ENNReal.add_lt_top.2 ⟨?_, ?_⟩
· -- We use estimates from auxiliary lemmas to deal with integral from `0` to `1`
have h_int' : ∀ t ∈ Ioc (0 : ℝ) 1, f t = ENNReal.ofReal ((t ^ (-r⁻¹) - 1) ^ finrank ℝ E) * mB := fun t ht ↦
by
refine μ.addHaar_closedBall (0 : E) ?_
rw [sub_nonneg]
exact Real.one_le_rpow_of_pos_of_le_one_of_nonpos ht.1 ht.2 (by simp [hr.le])
rw [setLIntegral_congr_fun measurableSet_Ioc h_int', lintegral_mul_const' _ _ measure_ball_lt_top.ne]
exact ENNReal.mul_lt_top (finite_integral_rpow_sub_one_pow_aux (finrank ℝ E) hnr) measure_ball_lt_top
· -- The integral from 1 to ∞ is zero:
have h_int'' : ∀ t ∈ Ioi (1 : ℝ), f t = 0 := fun t ht => by
simp only [f, closedBall_rpow_sub_one_eq_empty_aux E hr ht, measure_empty]
-- The integral over the constant zero function is finite:
rw [setLIntegral_congr_fun measurableSet_Ioi h_int'', lintegral_const 0, zero_mul]
exact WithTop.top_pos
