English
The constant-valued simple Lp function at x can be obtained by applying the span-singleton linear functional to the simple Lp function that takes the value 1 on the set and 0 elsewhere.
Русский
Постоянно-значная простая функция Lp на x может быть получена путём применения линейного функционала «span singleton» к функции-индикатору, принимающей значение 1 на заданном множестве и 0 вне его.
LaTeX
$$$\\mathrm{indicatorConstLp}_2\\; hs\\; hμs\\; x = \\big(\\mathrm{ContinuousLinearMap.toSpanSingleton}\\; \\mathbb{R}\\; x\\big).compLp\\big(\\mathrm{indicatorConstLp}_2\\; hs\\; hμs\\; (1 : \\mathbb{R})\\big)$$$
Lean4
theorem indicatorConstLp_eq_toSpanSingleton_compLp {s : Set α} [NormedSpace ℝ E] (hs : MeasurableSet s) (hμs : μ s ≠ ∞)
(x : E) :
indicatorConstLp 2 hs hμs x =
(ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs (1 : ℝ)) :=
by
ext1
refine indicatorConstLp_coeFn.trans ?_
have h_compLp := (ContinuousLinearMap.toSpanSingleton ℝ x).coeFn_compLp (indicatorConstLp 2 hs hμs (1 : ℝ))
rw [← EventuallyEq] at h_compLp
refine EventuallyEq.trans ?_ h_compLp.symm
refine (@indicatorConstLp_coeFn _ _ _ 2 μ _ s hs hμs (1 : ℝ)).mono fun y hy => ?_
dsimp only
rw [hy]
simp_rw [ContinuousLinearMap.toSpanSingleton_apply]
by_cases hy_mem : y ∈ s <;> simp [hy_mem]
