MeasureTheory.L2.inner_indicatorConstLp_eq_set_integral_inner
theorem MeasureTheory.L2.inner_indicatorConstLp_eq_set_integral_inner :
∀ {α : Type u_1} {E : Type u_2} (𝕜 : Type u_4) [inst : RCLike 𝕜] [inst_1 : MeasurableSpace α]
{μ : MeasureTheory.Measure α} [inst_2 : NormedAddCommGroup E] [inst_3 : InnerProductSpace 𝕜 E] {s : Set α}
(f : ↥(MeasureTheory.Lp E 2 μ)) (hs : MeasurableSet s) (c : E) (hμs : ↑↑μ s ≠ ⊤),
⟪MeasureTheory.indicatorConstLp 2 hs hμs c, f⟫_𝕜 = ∫ (x : α) in s, ⟪c, ↑↑f x⟫_𝕜 ∂μ
This theorem, known as **Alias of `MeasureTheory.L2.inner_indicatorConstLp_eq_setIntegral_inner`** states that for any measurable set `s` in a measure space `α` with measure `μ`, any element `f` of the `Lp` space with `p=2` and `E` as the normed commutative addition group, and any element `c` of `E`, the inner product in `L2` space between the indicator function of set `s` and `f` is equal to the integral of the inner product over `s`, given that the measure of the set `s` is not infinite. In mathematical terms, ⟪MeasureTheory.indicatorConstLp 2 hs hμs c, f⟫_𝕜 = ∫ (x : α) in s, ⟪c, ↑↑f x⟫_𝕜 ∂μ.
More concisely: For any measurable set `s` with finite measure `μ` in a measure space `α`, the inner product of the indicator function of `s` and an `L2` function `f` equals the integral over `s` of the pointwise inner product between the indicator function and `f`.
|
MeasureTheory.L2.inner_indicatorConstLp_one
theorem MeasureTheory.L2.inner_indicatorConstLp_one :
∀ {α : Type u_1} {𝕜 : Type u_4} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace α] {μ : MeasureTheory.Measure α}
{s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (f : ↥(MeasureTheory.Lp 𝕜 2 μ)),
⟪MeasureTheory.indicatorConstLp 2 hs hμs 1, f⟫_𝕜 = ∫ (x : α) in s, ↑↑f x ∂μ
This theorem, `MeasureTheory.L2.inner_indicatorConstLp_one`, states that for any measurable space `α`, a field `𝕜` which is either the real or complex number system, a measure `μ` on `α`, a set `s` in `α` that is measurable and has measure not equal to infinity, and a function `f` in the L2 space (square-integrable functions) with respect to measure `μ`, the inner product in the L2 space of the indicator function of the set `s` (with constant value 1) and the function `f` is equal to the integral of `f` over the set `s`.
In other words, the inner product of the indicator function of a set and a function in the L2 space corresponds to integrating that function over the set.
More concisely: For any measurable space, measure, measurable set of finite measure, and square-integrable function, the inner product of the indicator function of the set and the function equals the integral of the function over the set.
|
MeasureTheory.L2.inner_indicatorConstLp_eq_inner_set_integral
theorem MeasureTheory.L2.inner_indicatorConstLp_eq_inner_set_integral :
∀ {α : Type u_1} {E : Type u_2} (𝕜 : Type u_4) [inst : RCLike 𝕜] [inst_1 : MeasurableSpace α]
{μ : MeasureTheory.Measure α} [inst_2 : NormedAddCommGroup E] [inst_3 : InnerProductSpace 𝕜 E] {s : Set α}
[inst_4 : CompleteSpace E] [inst_5 : NormedSpace ℝ E] (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (c : E)
(f : ↥(MeasureTheory.Lp E 2 μ)),
⟪MeasureTheory.indicatorConstLp 2 hs hμs c, f⟫_𝕜 = ⟪c, ∫ (x : α) in s, ↑↑f x ∂μ⟫_𝕜
The theorem `MeasureTheory.L2.inner_indicatorConstLp_eq_inner_set_integral` states that for a given measurable set `s` with finite measure, a constant `c`, and a function `f` in the `L2` space, the inner product in `L2` between the indicator function of the set `s` scaled by `c` (`indicatorConstLp 2 hs hμs c`) and the function `f` is equal to the inner product of the constant `c` and the integral of the function `f` over the set `s`.
Formally, this is expressed as:
For any measurable set `s` of finite measure, any constant `c`, and any function `f` in the `L2` space, the inner product ⟪`indicatorConstLp 2 hs hμs c`, `f`⟫ in the field 𝕜 equals the inner product ⟪`c`, ∫`f` over `s` dμ⟫ in the field 𝕜.
More concisely: For any measurable set `s` of finite measure, constant `c`, and `L2` function `f`, the inner product of `c` times the indicator function of `s` and `f` equals the inner product of `c` with the integral of `f` over `s`.
|