English
Let p be a fixed p-integrable index, and let s be a measurable set with finite measure under μ. Then the map c ↦ indicatorConstLp(p, s, μ, c) is linear in c. In particular, for all c, c' in the target normed group E, indicatorConstLp(p, s, μ, c) − indicatorConstLp(p, s, μ, c') = indicatorConstLp(p, s, μ, c − c').
Русский
Пусть p задаёт нормируемый показатель, а s — измеримое множество с конечной мерой по μ. Тогда отображение c ↦ indicatorConstLp(p, s, μ, c) линейно относительно сложения в E. То есть для любых c, c' ∈ E выполняется indicatorConstLp(p, s, μ, c) − indicatorConstLp(p, s, μ, c') = indicatorConstLp(p, s, μ, c − c').
LaTeX
$$$indicatorConstLp(p, s, hμs, c) - indicatorConstLp(p, s, hμs, c') = indicatorConstLp(p, s, hμs, (c - c')).$$$
Lean4
/-- A version of `Set.indicator_sub` for `MeasureTheory.indicatorConstLp` -/
theorem indicatorConstLp_sub {c' : E} :
indicatorConstLp p hs hμs c - indicatorConstLp p hs hμs c' = indicatorConstLp p hs hμs (c - c') :=
by
simp_rw [indicatorConstLp, ← MemLp.toLp_sub, indicator_sub]
rfl
