English
If f,g are AES-measurable and ‖f‖ = ‖g‖ almost everywhere, then MemLp f p μ ↔ MemLp g p μ.
Русский
Если f,g AES-измеримы и их нормализации равны μ-почти везде, то принадлежность L^p одинакова.
LaTeX
$$$\text{AEStronglyMeasurable}(f,\mu) \wedge \text{AEStronglyMeasurable}(g,\mu) \wedge (\forall^{\mathrm{a}} x, \|f(x)\| = \|g(x)\|) \rightarrow (\text{MemLp}(f,p,\mu) \leftrightarrow \text{MemLp}(g,p,\mu))$$$
Lean4
theorem memLp_of_bounded [IsFiniteMeasure μ] {a b : ℝ} {f : α → ℝ} (h : ∀ᵐ x ∂μ, f x ∈ Set.Icc a b)
(hX : AEStronglyMeasurable f μ) (p : ENNReal) : MemLp f p μ :=
have ha : ∀ᵐ x ∂μ, a ≤ f x := h.mono fun ω h => h.1
have hb : ∀ᵐ x ∂μ, f x ≤ b := h.mono fun ω h => h.2
(memLp_const (max |a| |b|)).mono' hX (by filter_upwards [ha, hb] with x using abs_le_max_abs_abs)
