English
For any s, the essSup of indicator of constant c equals norm of c, provided μ(s)>0.
Русский
Для любого s essSup(indicator c) = ||c||, если μ(s) > 0.
LaTeX
$$$eLpNormEssSup (s.indicator (fun _ => c) ) \mu = \|c\|_ε$$$
Lean4
theorem eLpNorm_indicator_const₀ (hs : NullMeasurableSet s μ) (hp : p ≠ 0) (hp_top : p ≠ ∞) :
eLpNorm (s.indicator fun _ => c) p μ = ‖c‖ₑ * μ s ^ (1 / p.toReal) :=
have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp hp_top
calc
eLpNorm (s.indicator fun _ => c) p μ = (∫⁻ x, (‖(s.indicator fun _ ↦ c) x‖ₑ ^ p.toReal) ∂μ) ^ (1 / p.toReal) :=
eLpNorm_eq_lintegral_rpow_enorm hp hp_top
_ = (∫⁻ x, (s.indicator fun _ ↦ ‖c‖ₑ ^ p.toReal) x ∂μ) ^ (1 / p.toReal) :=
by
congr 2
refine (Set.comp_indicator_const c (fun x ↦ (‖x‖ₑ) ^ p.toReal) ?_)
simp [hp_pos]
_ = ‖c‖ₑ * μ s ^ (1 / p.toReal) :=
by
rw [lintegral_indicator_const₀ hs, ENNReal.mul_rpow_of_nonneg, ← ENNReal.rpow_mul, mul_one_div_cancel hp_pos.ne',
ENNReal.rpow_one]
positivity
