MeasureTheory.lintegral_nnnorm_le_of_forall_fin_meas_integral_eq
theorem MeasureTheory.lintegral_nnnorm_le_of_forall_fin_meas_integral_eq :
∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
m ≤ m0 →
∀ {f g : α → ℝ},
MeasureTheory.StronglyMeasurable f →
MeasureTheory.IntegrableOn f s μ →
MeasureTheory.StronglyMeasurable g →
MeasureTheory.IntegrableOn g s μ →
(∀ (t : Set α), MeasurableSet t → ↑↑μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ) →
MeasurableSet s → ↑↑μ s ≠ ⊤ → ∫⁻ (x : α) in s, ↑‖g x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖f x‖₊ ∂μ
The theorem `MeasureTheory.lintegral_nnnorm_le_of_forall_fin_meas_integral_eq` states that for a given sub-σ-algebra `m` of `m0`, and two functions `f` and `g` which are measurable in `m0` and `m` respectively, if their integrals over any `m`-measurable set with finite measure are the same, then the integral over an `m`-measurable set `s` with finite measure of the nonnegative norm of `g` is less than or equal to that of `f`. This condition holds if `f` and `g` are both strongly measurable, and are integrable over the set `s` with respect to measure `μ`.
More concisely: If two measurable functions `f` and `g` have equal integrals over every `m`-measurable set of finite measure in `μ`, and `f` and `g` are strongly measurable and integrable over an `m`-measurable set `s` with finite measure, then the integral of the nonnegative norm of `g` over `s` is less than or equal to that of `f`.
|
MeasureTheory.integral_norm_le_of_forall_fin_meas_integral_eq
theorem MeasureTheory.integral_norm_le_of_forall_fin_meas_integral_eq :
∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
m ≤ m0 →
∀ {f g : α → ℝ},
MeasureTheory.StronglyMeasurable f →
MeasureTheory.IntegrableOn f s μ →
MeasureTheory.StronglyMeasurable g →
MeasureTheory.IntegrableOn g s μ →
(∀ (t : Set α), MeasurableSet t → ↑↑μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ) →
MeasurableSet s → ↑↑μ s ≠ ⊤ → ∫ (x : α) in s, ‖g x‖ ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ∂μ
The theorem states that given a sub-measure space `m` which is a subset of `m0`, a function `f` that is measurable with respect to `m0`, and a function `g` that is measurable with respect to `m`, if the integrals of these two functions coincide on every `m`-measurable set with finite measure, then the integral over any `m`-measurable set `s` with finite measure of the norm of `g` is less than or equal to the integral over the same set of the norm of `f`. This is under the condition that both `f` and `g` are strongly measurable and integrable on `s`.
More concisely: Given measurable and integrable functions `f` and `g` on a sub-measure space `m` of `m0`, if the integrals of their norms coincide on every `m`-measurable set with finite measure, then the integral of `g`'s norm is less than or equal to the integral of `f`'s norm on any `m`-measurable set with finite measure.
|
MeasureTheory.Lp.ae_eq_of_forall_set_integral_eq'
theorem MeasureTheory.Lp.ae_eq_of_forall_set_integral_eq' :
∀ {α : Type u_1} {E' : Type u_2} (𝕜 : Type u_4) {p : ENNReal} {m m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E'] [inst : InnerProductSpace 𝕜 E']
[inst : CompleteSpace E'] [inst : NormedSpace ℝ E'],
m ≤ m0 →
∀ (f g : ↥(MeasureTheory.Lp E' p μ)),
p ≠ 0 →
p ≠ ⊤ →
(∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → MeasureTheory.IntegrableOn (↑↑f) s μ) →
(∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → MeasureTheory.IntegrableOn (↑↑g) s μ) →
(∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ) →
MeasureTheory.AEStronglyMeasurable' m (↑↑f) μ →
MeasureTheory.AEStronglyMeasurable' m (↑↑g) μ → μ.ae.EventuallyEq ↑↑f ↑↑g
This theorem, referred to as the "Uniqueness of the conditional expectation", states that:
Given
- two types `α` and `E'`,
- a type `𝕜`,
- an extended nonnegative real number `p`,
- two measurable spaces `m` and `m0` on `α`,
- a measure `μ` on `α`,
- and assuming `𝕜` is a real-like type, `E'` is a normed additive commutative group, is an inner product space over `𝕜`, is a complete space, and is a normed space over the real numbers,
- and also assuming that the measurable space `m` is less than or equal to `m0`,
for any two functions `f` and `g` from the Lp space on `E'` with parameter `p` and measure `μ`, if
- `p` is non-zero and finite,
- both `f` and `g` are integrable over any measurable set `s` with finite measure `μ`,
- the integral of `f` and `g` over any such set `s` are equal,
- both `f` and `g` are almost everywhere strongly measurable with respect to the measure `μ` (in the sense that they are almost everywhere equal to a strongly measurable function),
then `f` and `g` are equal almost everywhere with respect to the measure `μ`. This theorem thus provides a uniqueness property for functions satisfying these conditions.
More concisely: If two functions from the Lp space over a measurable space with finite measure, are integrable, equal in integral over every measurable set with finite measure, and almost everywhere strongly measurable, then they are equal almost everywhere.
|