English
Indicator of a constant vector c, with full formulas for eLpNorm.
Русский
Индикатор константы вектора c и формулы eLpNorm.
LaTeX
$$$eLpNorm_indicator_const (hs) (hp) (hp_top) : eLpNorm (s.indicator (fun x => c)) p μ = \|c\|_ε * μ(s)^{1/p}$$$
Lean4
theorem eLpNorm_indicator_const_le (p : ℝ≥0∞) : eLpNorm (s.indicator fun _ => c) p μ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal) :=
by
obtain rfl | hp := eq_or_ne p 0
· simp only [eLpNorm_exponent_zero, zero_le']
obtain rfl | h'p := eq_or_ne p ∞
· simp only [eLpNorm_exponent_top, ENNReal.toReal_top, _root_.div_zero, ENNReal.rpow_zero, mul_one]
exact eLpNormEssSup_indicator_const_le _ _
let t := toMeasurable μ s
calc
eLpNorm (s.indicator fun _ => c) p μ ≤ eLpNorm (t.indicator fun _ ↦ c) p μ :=
eLpNorm_mono_enorm (enorm_indicator_le_of_subset (subset_toMeasurable _ _) _)
_ = ‖c‖ₑ * μ t ^ (1 / p.toReal) := (eLpNorm_indicator_const (measurableSet_toMeasurable ..) hp h'p)
_ = ‖c‖ₑ * μ s ^ (1 / p.toReal) := by rw [measure_toMeasurable]
