English
The inner product of an indicator function on a measurable set with a function equals the integral over the set of the inner product with the constant vector.
Русский
Внутреннее произведение индикатора на множество и функции равно интегралу по этому множеству от скалярного произведения с константой.
LaTeX
$$$⟪\\mathrm{indicator}_{s}, f⟫ = \\int_{s} ⟪c, f(x)⟫ \\, dμ(x)$$$
Lean4
/-- The inner product in `L2` of the indicator of a set `indicatorConstLp 2 hs hμs c` and `f` is
equal to the integral of the inner product over `s`: `∫ x in s, ⟪c, f x⟫ ∂μ`. -/
theorem inner_indicatorConstLp_eq_setIntegral_inner (f : Lp E 2 μ) (hs : MeasurableSet s) (c : E) (hμs : μ s ≠ ∞) :
(⟪indicatorConstLp 2 hs hμs c, f⟫ : 𝕜) = ∫ x in s, ⟪c, f x⟫ ∂μ :=
by
rw [inner_def, ← integral_add_compl hs (L2.integrable_inner _ f)]
have h_left : (∫ x in s, ⟪(indicatorConstLp 2 hs hμs c) x, f x⟫ ∂μ) = ∫ x in s, ⟪c, f x⟫ ∂μ :=
by
suffices h_ae_eq : ∀ᵐ x ∂μ, x ∈ s → ⟪indicatorConstLp 2 hs hμs c x, f x⟫ = ⟪c, f x⟫ from
setIntegral_congr_ae hs h_ae_eq
have h_indicator : ∀ᵐ x : α ∂μ, x ∈ s → indicatorConstLp 2 hs hμs c x = c := indicatorConstLp_coeFn_mem
refine h_indicator.mono fun x hx hxs => ?_
congr
exact hx hxs
have h_right : (∫ x in sᶜ, ⟪(indicatorConstLp 2 hs hμs c) x, f x⟫ ∂μ) = 0 :=
by
suffices h_ae_eq : ∀ᵐ x ∂μ, x ∉ s → ⟪indicatorConstLp 2 hs hμs c x, f x⟫ = 0
by
simp_rw [← Set.mem_compl_iff] at h_ae_eq
suffices h_int_zero : (∫ x in sᶜ, ⟪indicatorConstLp 2 hs hμs c x, f x⟫ ∂μ) = ∫ _ in sᶜ, 0 ∂μ
by
rw [h_int_zero]
simp
exact setIntegral_congr_ae hs.compl h_ae_eq
have h_indicator : ∀ᵐ x : α ∂μ, x ∉ s → indicatorConstLp 2 hs hμs c x = 0 := indicatorConstLp_coeFn_notMem
refine h_indicator.mono fun x hx hxs => ?_
rw [hx hxs]
exact inner_zero_left _
rw [h_left, h_right, add_zero]
