noncomputable def
MeasureTheory.lcondExp
{α : Type u_1}
(m : MeasurableSpace α)
{m₀ : MeasurableSpace α}
(μ : Measure α)
[SigmaFinite μ]
(f : α → ENNReal)
:
α → ENNReal
Lebesgue conditional expectation of an ℝ≥0∞-valued function. It is defined as 0 if any of
the following conditions holds:
mis not a sub-σ-algebra ofm₀,μis not σ-finite with respect tom,fis notμ-integrable.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Lebesgue conditional expectation of an ℝ≥0∞-valued function. It is defined as 0 if any of
the following conditions holds:
mis not a sub-σ-algebra ofm₀,μis not σ-finite with respect tom.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MeasureTheory.lcondExp_of_not_le
{α : Type u_1}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
{f : α → ENNReal}
(hm_not : ¬m ≤ m₀)
:
theorem
MeasureTheory.lcondExp_of_not_sigmaFinite
{α : Type u_1}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
{f : α → ENNReal}
(hm : m ≤ m₀)
(hμm_not : ¬SigmaFinite (μ.trim hm))
:
theorem
MeasureTheory.lcondExp_of_sigmaFinite
{α : Type u_1}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
{f : α → ENNReal}
(hm : m ≤ m₀)
[hμm : SigmaFinite (μ.trim hm)]
:
lcondExp m μ f = if Measurable f then f
else if hf : Measurable f then ENNReal.ofReal ∘ ⨆ (n : ℕ), μ[ENNReal.toReal ∘ ⇑(⋯.approx n)|m] else 0
theorem
MeasureTheory.lcondExp_of_measurable
{α : Type u_1}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
(hm : m ≤ m₀)
[hμm : SigmaFinite (μ.trim hm)]
{f : α → ENNReal}
(hf : Measurable f)
:
theorem
MeasureTheory.lcondExp_const
{α : Type u_1}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
(hm : m ≤ m₀)
(c : ENNReal)
[IsFiniteMeasure μ]
:
@[simp]
theorem
MeasureTheory.lcondExp_zero
{α : Type u_1}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
:
theorem
MeasureTheory.measurable_lcondExp
{α : Type u_1}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
{f : α → ENNReal}
:
Measurable (lcondExp m μ f)
theorem
MeasureTheory.lcondExp_congr_ae
{α : Type u_1}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
{f g : α → ENNReal}
(h : f =ᶠ[ae μ] g)
:
theorem
MeasureTheory.lcondExp_of_aemeasurable
{α : Type u_1}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
(hm : m ≤ m₀)
[hμm : SigmaFinite (μ.trim hm)]
{f : α → ENNReal}
(hf : AEMeasurable f μ)
:
theorem
MeasureTheory.setLIntegral_lcondExp
{α : Type u_1}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
{f : α → ENNReal}
{s : Set α}
(hm : m ≤ m₀)
[SigmaFinite (μ.trim hm)]
(hs : MeasurableSet s)
:
The lintegral of the conditional expectation μ⁻[f|hm] over an m-measurable set is equal to
the lintegral of f on that set.
theorem
MeasureTheory.lintegral_lcondExp
{α : Type u_1}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
{f : α → ENNReal}
(hm : m ≤ m₀)
[hμm : SigmaFinite (μ.trim hm)]
:
theorem
MeasureTheory.lintegral_lcondExp_indicator
{α : Type u_1}
{m₀ : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
{Y : α → ENNReal}
(hY : Measurable Y)
[SigmaFinite (μ.trim ⋯)]
{A : Set α}
(hA : MeasurableSet A)
:
∫⁻ (x : α), lcondExp (MeasurableSpace.comap Y inferInstance) μ (A.indicator fun (x : α) => 1) x ∂μ = μ A
Total probability law using lcondExp as conditional probability.
theorem
MeasureTheory.ae_eq_lcondExp_of_forall_setLIntegral_eq
{α : Type u_1}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
(hm : m ≤ m₀)
[SigmaFinite (μ.trim hm)]
{f g : α → ENNReal}
(hg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, g x ∂μ = ∫⁻ (x : α) in s, f x ∂μ)
(hgm : AEStronglyMeasurable g μ)
:
Uniqueness of the conditional expectation
If a function is a.e. m-measurable, verifies an integrability condition and has same lintegral
as f on all m-measurable sets, then it is a.e. equal to μ⁻[f|hm].
theorem
MeasureTheory.lcondExp_bot
{α : Type u_1}
{m₀ : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
[IsProbabilityMeasure μ]
(f : α → ENNReal)
:
theorem
MeasureTheory.lcondExp_add
{α : Type u_1}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
{f g : α → ENNReal}
:
theorem
MeasureTheory.lcondExp_finset_sum
{α : Type u_1}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
{ι : Type u_2}
{s : Finset ι}
{f : ι → α → ENNReal}
:
theorem
MeasureTheory.lcondExp_smul
{α : Type u_1}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
(c : NNReal)
(f : α → ENNReal)
:
theorem
MeasureTheory.lcondExp_sub
{α : Type u_1}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
{f g : α → ENNReal}
:
theorem
MeasureTheory.lcondExp_lcondExp_of_le
{α : Type u_1}
{f : α → ENNReal}
{m₁ m₂ m₀ : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
(hm₁₂ : m₁ ≤ m₂)
(hm₂ : m₂ ≤ m₀)
[SigmaFinite (μ.trim hm₂)]
:
theorem
MeasureTheory.lcondExp_mono
{α : Type u_1}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
(f g : α → ENNReal)
: