Moments of a convolution [UPSTREAM]

The convolution μ ∗ ν of two probability measures on ℝ is the law of the sum of independent draws from μ and ν, so its mean is the sum of the means and its variance the sum of the variances. The second moment of a law about any point is its variance plus the squared distance of its mean from the point.

Main statements

• ProbabilityTheory.integral_id_conv: the mean of a convolution.
• ProbabilityTheory.variance_id_conv: the variance of a convolution.
• ProbabilityTheory.integral_sub_sq: the second moment about a point.

theorem ProbabilityTheory.memLp_id_conv {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {p : ENNReal} (hμ : MeasureTheory.MemLp id p μ) (hν : MeasureTheory.MemLp id p ν) : MeasureTheory.MemLp id p (μ.conv ν)

theorem ProbabilityTheory.integral_id_conv {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hμ : MeasureTheory.Integrable id μ) (hν : MeasureTheory.Integrable id ν) : ∫ (x : ℝ), x ∂μ.conv ν = ∫ (x : ℝ), x ∂μ + ∫ (x : ℝ), x ∂ν

theorem ProbabilityTheory.variance_id_conv {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hμ : MeasureTheory.MemLp id 2 μ) (hν : MeasureTheory.MemLp id 2 ν) : variance id (μ.conv ν) = variance id μ + variance id ν

theorem ProbabilityTheory.integral_sub_sq {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hμ : MeasureTheory.MemLp id 2 μ) (c : ℝ) : ∫ (x : ℝ), (x - c) ^ 2 ∂μ = variance id μ + (∫ (x : ℝ), x ∂μ - c) ^ 2