WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Conditional expectation

Revision #1108 → #2474 · back to history

modifiedDice rolling example50b41e35d75e
FieldFrom #1108To #2474
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Illustrative example; no such worked example lives in Mathlib.
status—not_formalized
modifiedRainfall data example6e422ad44672
FieldFrom #1108To #2474
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Illustrative example; not present as a formalized instance in Mathlib.
status—not_formalized
modifiedConditional expectation given an event64a35941e200
FieldFrom #1108To #2474
mathlib.decl—ProbabilityTheory.cond
mathlib.match_kind—invocation
mathlib.module—Mathlib.Probability.ProbabilityTheory.ConditionalProbability
note—E[X|A] itself is not a named Mathlib definition; it is expressible as an integral against the conditioned measure `ProbabilityTheory.cond`.
status—partial
modifiedConditional expectation for discrete random variables51fed9e8054a
FieldFrom #1108To #2474
mathlib.decl—MeasureTheory.condExp
mathlib.match_kind—generalization
mathlib.module—Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
note—Mathlib has no per-value E[X|Y=y] discrete formula; it defines the σ-algebra-valued `condExp` from which the discrete formula is a special case.
status—partial
modifiedConditional expectation for continuous random variablesb2d8982db826
FieldFrom #1108To #2474
mathlib.decl—ProbabilityTheory.condDistrib
mathlib.match_kind—generalization
mathlib.module—Mathlib.Probability.Kernel.CondDistrib
note—The density-based E[X|Y=y] formula is not defined directly; Mathlib provides the regular conditional distribution `condDistrib` from which it derives.
status—partial
modifiedConditional expectation of L^2 random variablesf9f5ab93738f
FieldFrom #1108To #2474
mathlib.decl—MeasureTheory.condExpL2
mathlib.match_kind—exact
mathlib.module—Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
note—`condExpL2` is the orthogonal-projection L² conditional expectation.
status—formalized
modifiedNon-uniqueness with constant Yf7e433412604
FieldFrom #1108To #2474
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Motivating example for non-uniqueness; not a Mathlib declaration.
status—not_formalized
modifiedNon-uniqueness with 2-dimensional Y0d9c112a760d
FieldFrom #1108To #2474
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Motivating example only; no Mathlib formalization.
status—not_formalized
modifiedUniqueness of conditional expectation up to measure zero02541be891df
FieldFrom #1108To #2474
mathlib.decl—MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq
mathlib.match_kind—exact
mathlib.module—Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
note—Characterizes a.e. uniqueness of `condExp` from the defining set-integral property.
status—formalized
modifiedExistence via Hilbert projection13e0ecd8dc87
FieldFrom #1108To #2474
mathlib.decl—MeasureTheory.condExpL2
mathlib.match_kind—exact
mathlib.module—Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
note—`condExpL2` is literally defined as `orthogonalProjectionOnto` the `lpMeas` subspace via the Hilbert projection theorem.
status—formalized
modifiedConditional expectation equals linear regression for jointly normal variables4bd798867f69
FieldFrom #1108To #2474
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no multivariate Gaussian and hence no formalization of the jointly-normal linear-regression identity.
status—not_formalized
modifiedConditional expectation given a sub-sigma-algebra22461ea4ad18
FieldFrom #1108To #2474
mathlib.decl—MeasureTheory.condExp
mathlib.match_kind—exact
mathlib.module—Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
note—`condExp m μ f` is exactly the conditional expectation of `f` w.r.t. the sub-σ-algebra `m`.
status—formalized
modifiedExistence via Radon–Nikodymfeac083eaf6e
FieldFrom #1108To #2474
mathlib.decl—MeasureTheory.rnDeriv_ae_eq_condExp
mathlib.match_kind—exact
mathlib.module—Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
note—Identifies `condExp` a.e. with the Radon–Nikodym derivative of `μ.withDensity f` restricted to the sub-σ-algebra.
status—formalized
modifiedConditional expectation given a random variable4eb0bef5515f
FieldFrom #1108To #2474
mathlib.decl—MeasureTheory.condExp
mathlib.match_kind—invocation
mathlib.module—Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
note—Mathlib expresses E[X|Y] via `condExp (MeasurableSpace.comap Y ‹_›) μ X`; there is no dedicated `condExp Y` abbreviation.
status—partial
modifiedDoob–Dynkin lemma representationfeeb44f6a2bb
FieldFrom #1108To #2474
mathlib.decl—Measurable.exists_eq_measurable_comp
mathlib.match_kind—exact
mathlib.module—Mathlib.MeasureTheory.Function.FactorsThrough
note—Factorization of a σ(Y)-measurable function as a measurable function of Y — the Doob–Dynkin lemma.
status—formalized
addedAlmost-sure uniqueness of conditional expectation9e2f8f23d5ad
modifiedMarkov kernel property of conditional probability10a1c6b0d26e
FieldFrom #1108To #2474
mathlib.decl—ProbabilityTheory.condExpKernel
mathlib.match_kind—exact
mathlib.module—Mathlib.Probability.Kernel.Condexp
note—`condExpKernel` is defined and carries an `IsMarkovKernel` instance.
status—formalized
modifiedLaw of the unconscious statisticiandde19fbdc321
FieldFrom #1108To #2474
mathlib.decl—ProbabilityTheory.condExp_ae_eq_integral_condExpKernel
mathlib.match_kind—exact
mathlib.module—Mathlib.Probability.Kernel.Condexp
note—Expresses `μ[f | m]` a.e. as an integral against the conditional-expectation kernel.
status—formalized
modifiedGeneral definition of conditional expectation in Banach space9a9f358cb7e5
FieldFrom #1108To #2474
mathlib.decl—MeasureTheory.condExp
mathlib.match_kind—exact
mathlib.module—Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
note—`condExp` is defined for functions into any Banach space `E` (`NormedAddCommGroup E`, `NormedSpace ℝ E`).
status—formalized
modifiedPulling out independent factorsc2592fc79fe3
FieldFrom #1108To #2474
mathlib.decl—MeasureTheory.condExp_indep_eq
mathlib.match_kind—exact
mathlib.module—Mathlib.Probability.ConditionalExpectation
note—For `m₁`-measurable `f` with `m₁, m₂` independent, `μ[f | m₂] = μ[f]` a.e.
status—formalized
modifiedStability under measurability8b77b78775b6
FieldFrom #1108To #2474
mathlib.decl—MeasureTheory.condExp_of_stronglyMeasurable
mathlib.match_kind—exact
mathlib.module—Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
note—If `f` is already `m`-strongly measurable and integrable, `μ[f | m] = f` a.e.
status—formalized
modifiedPulling out known factorsc202706fe200
FieldFrom #1108To #2474
mathlib.decl—MeasureTheory.condExp_mul_of_stronglyMeasurable_left
mathlib.match_kind—exact
mathlib.module—Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
note—`m`-measurable factor `f` can be pulled out: `μ[f*g | m] = f * μ[g | m]` a.e.; there is also a bilinear form.
status—formalized
modifiedLaw of total expectation40b15532d30f
FieldFrom #1108To #2474
mathlib.decl—MeasureTheory.integral_condExp
mathlib.match_kind—exact
mathlib.module—Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
note—∫ μ[f|m] dμ = ∫ f dμ.
status—formalized
modifiedTower property14e891696040
FieldFrom #1108To #2474
mathlib.decl—MeasureTheory.condExp_condExp_of_le
mathlib.match_kind—exact
mathlib.module—Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
note—For `m₁ ≤ m₂`, `μ[μ[f|m₂]|m₁] = μ[f|m₁]` a.e.
status—formalized
modifiedDoob martingale property13a606cc00e9
FieldFrom #1108To #2474
mathlib.decl—MeasureTheory.martingale_condExp
mathlib.match_kind—exact
mathlib.module—Mathlib.Probability.Martingale.Basic
note—`fun i => μ[f | ℱ i]` is a martingale — the Doob (Lévy) martingale.
status—formalized
modifiedLinearity of conditional expectation5f447ef12b0b
FieldFrom #1108To #2474
mathlib.decl—MeasureTheory.condExp_add
mathlib.match_kind—exact
mathlib.module—Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
note—`condExp_add` plus `condExp_smul`/`condExp_sub` give linearity.
status—formalized
modifiedPositivity4c162f1fd09b
FieldFrom #1108To #2474
mathlib.decl—MeasureTheory.condExp_nonneg
mathlib.match_kind—exact
mathlib.module—Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
note—`0 ≤ᵐ f → 0 ≤ᵐ μ[f | m]`.
status—formalized
modifiedMonotonicitya53b3ba3ea96
FieldFrom #1108To #2474
mathlib.decl—MeasureTheory.condExp_mono
mathlib.match_kind—exact
mathlib.module—Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
note—`f ≤ᵐ g → μ[f|m] ≤ᵐ μ[g|m]` for integrable `f, g`.
status—formalized
modifiedConditional monotone convergence77d1aac653ac
FieldFrom #1108To #2474
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No conditional monotone convergence theorem for `condExp` was found in Mathlib.
status—not_formalized
modifiedConditional dominated convergenced586718d3768
FieldFrom #1108To #2474
mathlib.decl—MeasureTheory.tendsto_condExpL1_of_dominated_convergence
mathlib.match_kind—special_case
mathlib.module—Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
note—Mathlib has an L¹-convergence version of dominated convergence for `condExpL1`, but not the pointwise-a.e. conditional DCT statement of the article.
status—partial
modifiedConditional Fatou's lemma49d22b66b791
FieldFrom #1108To #2474
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No conditional Fatou lemma was located in Mathlib.
status—not_formalized
modifiedConditional Jensen's inequality728c82b12e56
FieldFrom #1108To #2474
mathlib.decl—ConvexOn.map_condExp_le
mathlib.match_kind—exact
mathlib.module—Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
note—`φ(μ[f|m]) ≤ᵐ μ[φ ∘ f | m]` for convex `φ`.
status—formalized
modifiedConditional variance54df37ec3d27
FieldFrom #1108To #2474
mathlib.decl—ProbabilityTheory.condVar
mathlib.match_kind—exact
mathlib.module—Mathlib.Probability.CondVar
note—`condVar` is the conditional variance `Var[X; μ | m]`.
status—formalized
modifiedAlgebraic formula for the variance9c21dd49e49f
FieldFrom #1108To #2474
mathlib.decl—ProbabilityTheory.condVar_ae_eq_condExp_sq_sub_sq_condExp
mathlib.match_kind—exact
mathlib.module—Mathlib.Probability.CondVar
note—`Var[X|m] =ᵐ μ[X²|m] − (μ[X|m])²`.
status—formalized
modifiedLaw of total variance3c72bc16b7be
FieldFrom #1108To #2474
mathlib.decl—ProbabilityTheory.integral_condVar_add_variance_condExp
mathlib.match_kind—exact
mathlib.module—Mathlib.Probability.CondVar
note—`E[Var[X|m]] + Var[E[X|m]] = Var[X]`.
status—formalized
modifiedMartingale convergence18fdd696536f
FieldFrom #1108To #2474
mathlib.decl—MeasureTheory.Integrable.tendsto_ae_condExp
mathlib.match_kind—exact
mathlib.module—Mathlib.Probability.Martingale.Convergence
note—L¹ (Lévy-type) martingale convergence: `μ[g | ℱ n]` converges a.e. to `μ[g | ⨆ n, ℱ n]`; `Submartingale.ae_tendsto_limitProcess` is the underlying submartingale form.
status—formalized
modifiedConditional expectation as L^2-projectionf1afe312d116
FieldFrom #1108To #2474
mathlib.decl—MeasureTheory.condExpL2
mathlib.match_kind—exact
mathlib.module—Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
note—`condExpL2` is defined as the orthogonal projection onto `lpMeas E 𝕜 m 2 μ`.
status—formalized
modifiedSelf-adjointness of conditional expectationed71ad06423b
FieldFrom #1108To #2474
mathlib.decl—MeasureTheory.inner_condExpL2_left_eq_right
mathlib.match_kind—exact
mathlib.module—Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
note—⟨E[f|m], g⟩ = ⟨f, E[g|m]⟩ in L², the self-adjointness identity.
status—formalized
modifiedContractive projection on L^p2ced8ccb4782
FieldFrom #1108To #2474
mathlib.decl—MeasureTheory.norm_condExpL2_le_one
mathlib.match_kind—special_case
mathlib.module—Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
note—Mathlib has contractivity for p=1 (`eLpNorm_one_condExp_le_eLpNorm`) and p=2 (`norm_condExpL2_le_one`), but not a uniform L^p (1 ≤ p ≤ ∞) statement.
status—partial
modifiedDoob's conditional independence property6d7d9906a530
FieldFrom #1108To #2474
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib defines `CondIndep`/`iCondIndep` but no theorem stating Doob's conditional-independence characterization of the conditional expectation was found.
status—not_formalized