Conditional expectation as the best predictor

TheoremOrthogonality of the conditional-expectation residual#✓fully proved

Let \(\mu\) be a finite measure on a measurable space \((\Omega, \mathcal{F})\), let \(\mathcal{G} \subseteq \mathcal{F}\) be a sub-σ-algebra, and let \(Y : \Omega \to \mathbb{R}\) be square-integrable with respect to \(\mu\). Write \(\mathbb{E}[Y \mid \mathcal{G}]\) for the conditional expectation of \(Y\) with respect to \(\mu\) given \(\mathcal{G}\). Then for every strongly \(\mathcal{G}\)-measurable \(h : \Omega \to \mathbb{R}\) that is square-integrable with respect to \(\mu\), the residual \(Y - \mathbb{E}[Y \mid \mathcal{G}]\) is orthogonal to \(h\): \(\int (Y - \mathbb{E}[Y \mid \mathcal{G}]) \, h \, d\mu = 0\).

theorem integral_sub_condExp_mul_eq_zero (hm : m ≤ mΩ) {Y h : Ω → ℝ} (hY : MemLp Y 2 μ)
    (hh : MemLp h 2 μ) (hhm : StronglyMeasurable[m] h) :
    ∫ ω, (Y ω - μ[Y|m] ω) * h ω ∂μ = 0
Used by 2

TheoremPythagorean identity for the conditional mean#✓fully proved

Let \(\mu\) be a finite measure on a measurable space \((\Omega, \mathcal{F})\), let \(\mathcal{G} \subseteq \mathcal{F}\) be a sub-σ-algebra, and let \(Y : \Omega \to \mathbb{R}\) be square-integrable with respect to \(\mu\). Write \(\mathbb{E}[Y \mid \mathcal{G}]\) for the conditional expectation of \(Y\) with respect to \(\mu\) given \(\mathcal{G}\). Then for every strongly \(\mathcal{G}\)-measurable \(g : \Omega \to \mathbb{R}\) that is square-integrable with respect to \(\mu\), \(\int (Y - g)^2 \, d\mu = \int (Y - \mathbb{E}[Y \mid \mathcal{G}])^2 \, d\mu + \int (\mathbb{E}[Y \mid \mathcal{G}] - g)^2 \, d\mu\).

theorem integral_sq_sub_eq_integral_sq_sub_condExp_add (hm : m ≤ mΩ) {Y g : Ω → ℝ}
    (hY : MemLp Y 2 μ) (hg : MemLp g 2 μ) (hgm : StronglyMeasurable[m] g) :
    ∫ ω, (Y ω - g ω) ^ 2 ∂μ =
      ∫ ω, (Y ω - μ[Y|m] ω) ^ 2 ∂μ + ∫ ω, (μ[Y|m] ω - g ω) ^ 2 ∂μ
Uses 1 · Used by 3

TheoremThe conditional mean minimizes the expected squared error#✓fully proved

Let \(\mu\) be a finite measure on a measurable space \((\Omega, \mathcal{F})\), let \(\mathcal{G} \subseteq \mathcal{F}\) be a sub-σ-algebra, and let \(Y : \Omega \to \mathbb{R}\) be square-integrable with respect to \(\mu\). Write \(\mathbb{E}[Y \mid \mathcal{G}]\) for the conditional expectation of \(Y\) with respect to \(\mu\) given \(\mathcal{G}\). Then for every strongly \(\mathcal{G}\)-measurable \(g : \Omega \to \mathbb{R}\) that is square-integrable with respect to \(\mu\), \(\int (Y - \mathbb{E}[Y \mid \mathcal{G}])^2 \, d\mu \le \int (Y - g)^2 \, d\mu\).

theorem integral_sq_sub_condExp_le (hm : m ≤ mΩ) {Y g : Ω → ℝ} (hY : MemLp Y 2 μ)
    (hg : MemLp g 2 μ) (hgm : StronglyMeasurable[m] g) :
    ∫ ω, (Y ω - μ[Y|m] ω) ^ 2 ∂μ ≤ ∫ ω, (Y ω - g ω) ^ 2 ∂μ
Uses 1 · Used by 1

TheoremThe regression function is the Bayes-optimal regressor#✓fully proved

Let \(\mu\) be a finite measure on a measurable space \(\Omega\), let \(X : \Omega \to \mathcal{X}\) be a measurable map into a measurable space \(\mathcal{X}\), and let \(Y : \Omega \to \mathbb{R}\) be square-integrable with respect to \(\mu\). Write \(\mathbb{E}[Y \mid X]\) for the conditional expectation of \(Y\) with respect to \(\mu\) given the σ-algebra generated by \(X\). Then for every measurable \(h : \mathcal{X} \to \mathbb{R}\) such that \(h \circ X\) is square-integrable with respect to \(\mu\), \(\int (Y - \mathbb{E}[Y \mid X])^2 \, d\mu \le \int (Y - h \circ X)^2 \, d\mu\).

theorem integral_sq_sub_condExp_comap_le {𝓧 : Type*} [m𝓧 : MeasurableSpace 𝓧] {X : Ω → 𝓧}
    (hX : Measurable X) {Y : Ω → ℝ} (hY : MemLp Y 2 μ) {h : 𝓧 → ℝ} (hh : Measurable h)
    (hhX : MemLp (h ∘ X) 2 μ) :
    ∫ ω, (Y ω - μ[Y|m𝓧.comap X] ω) ^ 2 ∂μ ≤ ∫ ω, (Y ω - h (X ω)) ^ 2 ∂μ
Uses 1
4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.