English
If hg is MemLp g p μ, hf AEStronglyMeasurable, and hfg a.e. bound on ENorm, then MemLp f p μ.
Русский
Если hg ∈ MemLp g p μ, hf измеримо, и hfg ограничивает ENorm, то MemLp f p μ.
LaTeX
$$$MemLp g p μ \to AEStronglyMeasurable f μ \to (\text{ae bound}) ⇒ MemLp f p μ.$$$
Lean4
theorem eLpNorm_enorm_rpow (f : α → ε) (hq_pos : 0 < q) :
eLpNorm (‖f ·‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q :=
by
by_cases h0 : p = 0
· simp [h0, ENNReal.zero_rpow_of_pos hq_pos]
by_cases hp_top : p = ∞
· simp only [hp_top, eLpNorm_exponent_top, ENNReal.top_mul', hq_pos.not_ge, ENNReal.ofReal_eq_zero, if_false,
eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm]
have h_rpow : essSup (‖‖f ·‖ₑ ^ q‖ₑ) μ = essSup (‖f ·‖ₑ ^ q) μ := by congr
rw [h_rpow]
have h_rpow_mono := ENNReal.strictMono_rpow_of_pos hq_pos
have h_rpow_surj := (ENNReal.rpow_left_bijective hq_pos.ne.symm).2
let iso := h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj
exact (iso.essSup_apply (fun x => ‖f x‖ₑ) μ).symm
rw [eLpNorm_eq_eLpNorm' h0 hp_top, eLpNorm_eq_eLpNorm' _ (by finiteness)]
swap
· refine mul_ne_zero h0 ?_
rwa [Ne, ENNReal.ofReal_eq_zero, not_le]
rw [ENNReal.toReal_mul, ENNReal.toReal_ofReal hq_pos.le]
exact eLpNorm'_enorm_rpow f p.toReal q hq_pos
