English
If a sequence is ae-strongly measurable and eLpNorm tends to 0, the limit is in MemLp.
Русский
Если последовательность ae-измерима и eLpNorm стремится к 0, предел принадлежит MemLp.
LaTeX
$$$\text{MemLp}(f_\lim, p, μ)$$$
Lean4
theorem memLp_of_cauchy_tendsto (hp : 1 ≤ p) {f : ℕ → α → E} (hf : ∀ n, MemLp (f n) p μ) (f_lim : α → E)
(h_lim_meas : AEStronglyMeasurable f_lim μ) (h_tendsto : atTop.Tendsto (fun n => eLpNorm (f n - f_lim) p μ) (𝓝 0)) :
MemLp f_lim p μ := by
refine ⟨h_lim_meas, ?_⟩
rw [ENNReal.tendsto_atTop_zero] at h_tendsto
obtain ⟨N, h_tendsto_1⟩ := h_tendsto 1 zero_lt_one
specialize h_tendsto_1 N (le_refl N)
have h_add : f_lim = f_lim - f N + f N := by abel
rw [h_add]
refine lt_of_le_of_lt (eLpNorm_add_le (h_lim_meas.sub (hf N).1) (hf N).1 hp) ?_
rw [ENNReal.add_lt_top]
constructor
· refine lt_of_le_of_lt ?_ ENNReal.one_lt_top
have h_neg : f_lim - f N = -(f N - f_lim) := by simp
rwa [h_neg, eLpNorm_neg]
· exact (hf N).2
