English
For a simple function f represented as a finite sum of constants times indicator of measurable sets, its L1 norm equals the sum of the real numbers times the measure of the corresponding sets.
Русский
Для простой функции f, представимой как конечная сумма констант, умноженных на индикаторы множеств, её нормa L1 равна сумме констант, умноженных на меры соответствующих множеств.
LaTeX
$$$\\|f\\| = \\sum_{x \\in \\mathrm{range}(toSimpleFunc f)} \\mu( f^{-1}({x}) ) \\cdot \\|x\\|.$$$
Lean4
theorem norm_eq_sum_mul (f : α →₁ₛ[μ] G) :
‖f‖ = ∑ x ∈ (toSimpleFunc f).range, μ.real (toSimpleFunc f ⁻¹' { x }) * ‖x‖ :=
by
rw [norm_toSimpleFunc, eLpNorm_one_eq_lintegral_enorm]
have h_eq := SimpleFunc.map_apply (‖·‖ₑ) (toSimpleFunc f)
simp_rw [← h_eq, measureReal_def]
rw [SimpleFunc.lintegral_eq_lintegral, SimpleFunc.map_lintegral, ENNReal.toReal_sum]
· congr
ext1 x
rw [ENNReal.toReal_mul, mul_comm, ← ofReal_norm_eq_enorm, ENNReal.toReal_ofReal (norm_nonneg _)]
· intro x _
by_cases hx0 : x = 0
· rw [hx0]; simp
· have := SimpleFunc.measure_preimage_lt_top_of_integrable _ (SimpleFunc.integrable f) hx0
finiteness
