MeasureTheory.condexpIndL1.proof_2
theorem MeasureTheory.condexpIndL1.proof_2 :
∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α),
MeasurableSet s ∧ ↑↑μ s ≠ ⊤ → MeasurableSet s
This theorem, `MeasureTheory.condexpIndL1.proof_2`, states that for any type `α` with an associated measurable space `m0`, a measure `μ` on `α`, and a set `s` of type `α`, if `s` is a measurable set and the measure of `s` is not infinite, then `s` is a measurable set. The theorem is basically asserting the property of a measurable set under certain conditions. More specifically, it assures that if a set is measurable and its measure is finite then it remains to be measurable.
More concisely: If `α` is a type with measurable space `m0`, `μ` is a measure on `α`, and `s` is a measurable, finite-measure subset of `α`, then `s` is measurable.
|
MeasureTheory.set_integral_condexpL1
theorem MeasureTheory.set_integral_condexpL1 :
∀ {α : Type u_1} {F' : Type u_4} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F']
[inst_2 : CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m ≤ m0}
[inst_3 : MeasureTheory.SigmaFinite (μ.trim hm)] {f : α → F'} {s : Set α},
MeasureTheory.Integrable f μ →
MeasurableSet s → ∫ (x : α) in s, ↑↑(MeasureTheory.condexpL1 hm μ f) x ∂μ = ∫ (x : α) in s, f x ∂μ
This theorem, known as an alias of `MeasureTheory.setIntegral_condexpL1`, states that for a given set `s` in a measure space `α`, if the function `f : α → F'` is integrable and the set `s` is measurable, then the integral of the conditional expectation `condexpL1` of `f` over the set `s` is equal to the integral of `f` over the same set. The conditional expectation `condexpL1` is computed with respect to a measure `μ` and a measurable space `m` that is a sub-space of `m0`, assuming `m` is sigma-finite under the trimmed measure `μ.trim hm`. Here, `F'` is a normed add commutative group and a complete normed space over the reals.
More concisely: For a measurable set `s` in a sigma-finite measure space `(α, Σ, μ)` and integrable function `f : α → F'`, the integral of the conditional expectation `condexpL1 f μ s` over `s` equals the integral of `f` over `s`.
|
MeasureTheory.dominatedFinMeasAdditive_condexpInd
theorem MeasureTheory.dominatedFinMeasAdditive_condexpInd :
∀ {α : Type u_1} (G : Type u_5) [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} [inst_1 : NormedSpace ℝ G]
(hm : m ≤ m0) (μ : MeasureTheory.Measure α) [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)],
MeasureTheory.DominatedFinMeasAdditive μ (MeasureTheory.condexpInd G hm μ) 1
This theorem states that for any types `α` and `G`, with `G` being a normed additive commutative group, any two measurable spaces `m` and `m0` on `α` with `m` being a sub-measure of `m0`, a measure `μ` on `α` that is sigma-finite when trimmed by `m`, the function `MeasureTheory.condexpInd G hm μ` is a dominated finite measure additive function. In other words, the function is finite measure additive and its norm on any measurable set is less than or equal to the measure of the set. The domination constant in this case is `1`.
More concisely: For any sigma-finite measure `μ` on a measurable space `(α, G)` that is a sub-measure of a finite measure `m0`, the function `MeasureTheory.condexpInd G m μ` is a dominated finite measure additive function with domination constant 1.
|
MeasureTheory.condexpIndL1.proof_3
theorem MeasureTheory.condexpIndL1.proof_3 :
∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α),
MeasurableSet s ∧ ↑↑μ s ≠ ⊤ → ↑↑μ s ≠ ⊤
This theorem states that for any type `α` with a measurable space `m0`, a measure `μ` on `α`, and a set `s` of `α`, if the set `s` is a measurable set and the measure of `s` is different from infinity, then the measure of `s` remains different from infinity. In other words, the theorem assures that the condition of being a measurable set and having a measure different from infinity is preserved under the given conditions.
More concisely: If `α` is a type with measurable space `m0`, `μ` is a measure on `α`, `s` is a measurable subset of `α` with finite measure, then the measure of `s` remains finite.
|
Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1._auxLemma.1
theorem Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1._auxLemma.1 : (¬False) = True
This theorem, `Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1._auxLemma.1`, simply states that the negation of "false" is "true". In logical terms, it's expressing that if something is not false, then it must be true. This is a fundamental concept in boolean logic.
More concisely: The negation of a false statement is true.
|