English
Equivalence of MemLp for f,g when norms match μ-a.e. and g is AES-measurable.
Русский
Эквивалентность MemLp для f,g когда их нормы совпадают μ-почти везде и g измерима.
LaTeX
$$$\text{AEStronglyMeasurable}(f,μ) \wedge \text{AEStronglyMeasurable}(g,μ) \wedge (\forall^{\mathrm{a}} x, \|f(x)\|_ε = \|g(x)\|_ε) \rightarrow (\text{MemLp}(f,p,μ) \leftrightarrow \text{MemLp}(g,p,μ))$$$
Lean4
theorem eLpNorm_indicator_eq_eLpNorm_restrict {f : α → ε} {s : Set α} (hs : MeasurableSet s) :
eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s) :=
by
by_cases hp_zero : p = 0
· simp only [hp_zero, eLpNorm_exponent_zero]
by_cases hp_top : p = ∞
·
simp_rw [hp_top, eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm, enorm_indicator_eq_indicator_enorm,
ENNReal.essSup_indicator_eq_essSup_restrict hs]
simp_rw [eLpNorm_eq_lintegral_rpow_enorm hp_zero hp_top]
rw [← lintegral_indicator hs]
congr
simp_rw [enorm_indicator_eq_indicator_enorm]
rw [eq_comm, ← Function.comp_def (fun x : ℝ≥0∞ => x ^ p.toReal), Set.indicator_comp_of_zero, Function.comp_def]
simp [ENNReal.toReal_pos hp_zero hp_top]
