English
If a sequence of peak functions φ_i converges uniformly to zero away from a point x0 and the target g is integrable with a limit a at x0, then φ_i • g converges to a.
Русский
Если последовательность пиковых функций φ_i сходится равномерно к нулю вне точки x0, а g интегрируема и имеет предел a в x0, то φ_i • g сходится к a.
LaTeX
$$$\\forall \\text{sets } s,t,\\; φ_i:X→ℝ,\\; hf: AEMeasurable f μ,\\; hf^{p},\\; \\Rightarrow \\lim_{i\\to\\infty} ∫ f_i x • g x = a$$$
Lean4
theorem lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top {p : ℝ} {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ)
(hf_top : (∫⁻ a, f a ^ p ∂μ) < ⊤) (hg_top : (∫⁻ a, g a ^ p ∂μ) < ⊤) (hp1 : 1 ≤ p) : (∫⁻ a, (f + g) a ^ p ∂μ) < ⊤ :=
by
have hp0_lt : 0 < p := lt_of_lt_of_le zero_lt_one hp1
have hp0 : 0 ≤ p := le_of_lt hp0_lt
calc
(∫⁻ a : α, (f a + g a) ^ p ∂μ) ≤ ∫⁻ a, (2 : ℝ≥0∞) ^ (p - 1) * f a ^ p + (2 : ℝ≥0∞) ^ (p - 1) * g a ^ p ∂μ :=
by
refine lintegral_mono fun a => ?_
dsimp only
have h_zero_lt_half_rpow : (0 : ℝ≥0∞) < (1 / 2 : ℝ≥0∞) ^ p :=
by
rw [← ENNReal.zero_rpow_of_pos hp0_lt]
exact ENNReal.rpow_lt_rpow (by simp) hp0_lt
have h_rw : (1 / 2 : ℝ≥0∞) ^ p * (2 : ℝ≥0∞) ^ (p - 1) = 1 / 2 := by
rw [sub_eq_add_neg, ENNReal.rpow_add _ _ two_ne_zero ENNReal.coe_ne_top, ← mul_assoc, ←
ENNReal.mul_rpow_of_nonneg _ _ hp0, one_div, ENNReal.inv_mul_cancel two_ne_zero ENNReal.coe_ne_top,
ENNReal.one_rpow, one_mul, ENNReal.rpow_neg_one]
rw [← ENNReal.mul_le_mul_left (ne_of_lt h_zero_lt_half_rpow).symm _]
· rw [mul_add, ← mul_assoc, ← mul_assoc, h_rw, ← ENNReal.mul_rpow_of_nonneg _ _ hp0, mul_add]
refine ENNReal.rpow_arith_mean_le_arith_mean2_rpow (1 / 2 : ℝ≥0∞) (1 / 2 : ℝ≥0∞) (f a) (g a) ?_ hp1
rw [ENNReal.div_add_div_same, one_add_one_eq_two, ENNReal.div_self two_ne_zero ENNReal.coe_ne_top]
· finiteness
_ < ⊤ :=
by
rw [lintegral_add_left', lintegral_const_mul'' _ (hf.pow_const p), lintegral_const_mul' _ _ (by finiteness),
ENNReal.add_lt_top]
· constructor <;> finiteness
· fun_prop
