Measure theory lemmas to be upstreamed to Mathlib

theorem integrable_inner {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {f g : Ω → E} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (hf : MeasureTheory.MemLp f 2 P) (hg : MeasureTheory.MemLp g 2 P) : MeasureTheory.Integrable (fun (ω : Ω) => inner ℝ (f ω) (g ω)) P

theorem condExp_inner_of_aestronglyMeasurable_left {Ω : Type u_1} {E : Type u_2} {m mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {f g : Ω → E} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (hf : MeasureTheory.AEStronglyMeasurable f P) (hfg : MeasureTheory.Integrable (fun (ω : Ω) => inner ℝ (f ω) (g ω)) P) (hg : MeasureTheory.Integrable g P) : P[fun (ω : Ω) => inner ℝ (f ω) (g ω) | m] =ᵐ[P] fun (ω : Ω) => inner ℝ (f ω) (P[g | m] ω)

theorem condExp_inner_of_aestronglyMeasurable_right {Ω : Type u_1} {E : Type u_2} {m mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {f g : Ω → E} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (hg : MeasureTheory.AEStronglyMeasurable g P) (hfg : MeasureTheory.Integrable (fun (ω : Ω) => inner ℝ (f ω) (g ω)) P) (hf : MeasureTheory.Integrable f P) : P[fun (ω : Ω) => inner ℝ (f ω) (g ω) | m] =ᵐ[P] fun (ω : Ω) => inner ℝ (P[f | m] ω) (g ω)

theorem Filter.EventuallyEq.div' {α : Type u_1} {β : Type u_2} [Div β] {f f' g g' : α → β} {l : Filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') : f / f' =ᶠ[l] g / g'

theorem Filter.EventuallyEq.sub' {α : Type u_1} {β : Type u_2} [Sub β] {f f' g g' : α → β} {l : Filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') : f - f' =ᶠ[l] g - g'

theorem ProbabilityTheory.eq_gaussianReal_integral_variance {μ : MeasureTheory.Measure ℝ} {m : ℝ} {v : NNReal} (h : μ = gaussianReal m v) : μ = gaussianReal (∫ (x : ℝ), id x ∂μ) (variance id μ).toNNReal

theorem ProbabilityTheory.centralMoment_of_integral_id_eq_zero {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (p : ℕ) (hX : ∫ (x : Ω), X x ∂μ = 0) : centralMoment X p μ = ∫ (ω : Ω), X ω ^ p ∂μ

theorem MeasurableEquiv.coe_toLp_symm_eq {ι : Type u_1} : ⇑(MeasurableEquiv.toLp 2 (ι → ℝ)).symm = ⇑(EuclideanSpace.equiv ι ℝ)

@[simp]

theorem zero_mem_parallelepiped {ι : Type u_1} {E : Type u_2} [Fintype ι] [AddCommGroup E] [Module ℝ E] {v : ι → E} : 0 ∈ parallelepiped v

@[simp]

theorem nonempty_parallelepiped {ι : Type u_1} {E : Type u_2} [Fintype ι] [AddCommGroup E] [Module ℝ E] {v : ι → E} : (parallelepiped v).Nonempty

@[simp]

theorem volume_of_nonempty_of_subsingleton {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [Subsingleton E] {s : Set E} (hs : s.Nonempty) : MeasureTheory.volume s = 1

theorem MeasureTheory.Measure.IsMulLeftInvariant.measure_ball_const {G : Type u_1} [Group G] [PseudoMetricSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] (μ : Measure G) [μ.IsMulLeftInvariant] [IsIsometricSMul G G] [MeasurableMul G] (a b : G) (r : ℝ) : μ (Metric.ball a r) = μ (Metric.ball b r)

theorem MeasureTheory.Measure.IsAddLeftInvariant.measure_ball_const {G : Type u_1} [AddGroup G] [PseudoMetricSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] (μ : Measure G) [μ.IsAddLeftInvariant] [IsIsometricVAdd G G] [MeasurableAdd G] (a b : G) (r : ℝ) : μ (Metric.ball a r) = μ (Metric.ball b r)

theorem MeasureTheory.Measure.IsMulRightInvariant.measure_ball_const {G : Type u_1} [CommGroup G] [PseudoMetricSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] (μ : Measure G) [μ.IsMulRightInvariant] [IsIsometricSMul Gᵐᵒᵖ G] [MeasurableMul G] (a b : G) (r : ℝ) : μ (Metric.ball a r) = μ (Metric.ball b r)

theorem MeasureTheory.Measure.IsAddRightInvariant.measure_ball_const {G : Type u_1} [AddCommGroup G] [PseudoMetricSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] (μ : Measure G) [μ.IsAddRightInvariant] [IsIsometricVAdd Gᵃᵒᵖ G] [MeasurableAdd G] (a b : G) (r : ℝ) : μ (Metric.ball a r) = μ (Metric.ball b r)

theorem MeasureTheory.Measure.IsMulLeftInvariant.measure_closedBall_const {G : Type u_1} [Group G] [PseudoMetricSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] (μ : Measure G) [μ.IsMulLeftInvariant] [IsIsometricSMul G G] [MeasurableMul G] (a b : G) (r : ℝ) : μ (Metric.closedBall a r) = μ (Metric.closedBall b r)

theorem MeasureTheory.Measure.IsAddLeftInvariant.measure_closedBall_const {G : Type u_1} [AddGroup G] [PseudoMetricSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] (μ : Measure G) [μ.IsAddLeftInvariant] [IsIsometricVAdd G G] [MeasurableAdd G] (a b : G) (r : ℝ) : μ (Metric.closedBall a r) = μ (Metric.closedBall b r)

theorem MeasureTheory.Measure.IsMulRightInvariant.measure_closeBall_const {G : Type u_1} [CommGroup G] [PseudoMetricSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] (μ : Measure G) [μ.IsMulRightInvariant] [IsIsometricSMul Gᵐᵒᵖ G] [MeasurableMul G] (a b : G) (r : ℝ) : μ (Metric.closedBall a r) = μ (Metric.closedBall b r)

theorem MeasureTheory.Measure.IsAddRightInvariant.measure_closeBall_const {G : Type u_1} [AddCommGroup G] [PseudoMetricSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] (μ : Measure G) [μ.IsAddRightInvariant] [IsIsometricVAdd Gᵃᵒᵖ G] [MeasurableAdd G] (a b : G) (r : ℝ) : μ (Metric.closedBall a r) = μ (Metric.closedBall b r)

theorem MeasureTheory.Measure.IsMulLeftInvariant.measure_ball_const' {G : Type u_1} [Group G] [PseudoEMetricSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] (μ : Measure G) [μ.IsMulLeftInvariant] [IsIsometricSMul G G] [MeasurableMul G] (a b : G) (r : ENNReal) : μ (Metric.eball a r) = μ (Metric.eball b r)

theorem MeasureTheory.Measure.IsAddLeftInvariant.measure_ball_const' {G : Type u_1} [AddGroup G] [PseudoEMetricSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] (μ : Measure G) [μ.IsAddLeftInvariant] [IsIsometricVAdd G G] [MeasurableAdd G] (a b : G) (r : ENNReal) : μ (Metric.eball a r) = μ (Metric.eball b r)

theorem MeasureTheory.Measure.IsMulRightInvariant.measure_ball_const' {G : Type u_1} [CommGroup G] [PseudoEMetricSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] (μ : Measure G) [μ.IsMulRightInvariant] [IsIsometricSMul Gᵐᵒᵖ G] [MeasurableMul G] (a b : G) (r : ENNReal) : μ (Metric.eball a r) = μ (Metric.eball b r)

theorem MeasureTheory.Measure.IsAddRightInvariant.measure_ball_const' {G : Type u_1} [AddCommGroup G] [PseudoEMetricSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] (μ : Measure G) [μ.IsAddRightInvariant] [IsIsometricVAdd Gᵃᵒᵖ G] [MeasurableAdd G] (a b : G) (r : ENNReal) : μ (Metric.eball a r) = μ (Metric.eball b r)

theorem MeasureTheory.Measure.IsMulLeftInvariant.measure_closedBall_const' {G : Type u_1} [Group G] [PseudoEMetricSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] (μ : Measure G) [μ.IsMulLeftInvariant] [IsIsometricSMul G G] [MeasurableMul G] (a b : G) (r : ENNReal) : μ (Metric.closedEBall a r) = μ (Metric.closedEBall b r)

theorem MeasureTheory.Measure.IsAddLeftInvariant.measure_closedBall_const' {G : Type u_1} [AddGroup G] [PseudoEMetricSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] (μ : Measure G) [μ.IsAddLeftInvariant] [IsIsometricVAdd G G] [MeasurableAdd G] (a b : G) (r : ENNReal) : μ (Metric.closedEBall a r) = μ (Metric.closedEBall b r)

theorem MeasureTheory.Measure.IsMulRightInvariant.measure_closeBall_const' {G : Type u_1} [CommGroup G] [PseudoEMetricSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] (μ : Measure G) [μ.IsMulRightInvariant] [IsIsometricSMul Gᵐᵒᵖ G] [MeasurableMul G] (a b : G) (r : ENNReal) : μ (Metric.closedEBall a r) = μ (Metric.closedEBall b r)

theorem MeasureTheory.Measure.IsAddRightInvariant.measure_closeBall_const' {G : Type u_1} [AddCommGroup G] [PseudoEMetricSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] (μ : Measure G) [μ.IsAddRightInvariant] [IsIsometricVAdd Gᵃᵒᵖ G] [MeasurableAdd G] (a b : G) (r : ENNReal) : μ (Metric.closedEBall a r) = μ (Metric.closedEBall b r)

theorem InnerProductSpace.volume_closedBall_div {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (x y : E) {r s : ℝ} (hr : 0 < r) (hs : 0 < s) : MeasureTheory.volume (Metric.closedBall x r) / MeasureTheory.volume (Metric.closedBall y s) = ENNReal.ofReal (r / s) ^ Module.finrank ℝ E

theorem InnerProductSpace.volume_closedBall_div' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (x y : E) (r s : ENNReal) : MeasureTheory.volume (Metric.closedEBall x r) / MeasureTheory.volume (Metric.closedEBall y s) = (r / s) ^ Module.finrank ℝ E

theorem MeasureTheory.Measure.addHaar_closedEBall_center {E : Type u_1} [SeminormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddLeftInvariant] (x : E) (r : ENNReal) : μ (Metric.closedEBall x r) = μ (Metric.closedEBall 0 r)

The measure of a closed ball for a left-invariant measure does not depend on its center.

theorem MeasureTheory.Measure.addHaar_closedEBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (x : E) (r : ENNReal) : μ (Metric.closedEBall x r) = r ^ Module.finrank ℝ E * μ (Metric.ball 0 1)

The measure of a closed ball of radius r for an additive Haar measure in dimension d is r ^ d times the measure of the unit ball.

theorem MeasureTheory.Measure.addHaar_closedEBall_div {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (x y : E) (r s : ENNReal) : μ (Metric.closedEBall x r) / μ (Metric.closedEBall y s) = (r / s) ^ Module.finrank ℝ E

For an additive Haar measure in dimension d, the ratio of the measures of two closed balls of radii r and s is (r / s) ^ d.

theorem ProbabilityTheory.covariance_fun_add_left {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y Z : Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.MemLp X 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) (hZ : MeasureTheory.MemLp Z 2 μ) : covariance (fun (ω : Ω) => X ω + Y ω) Z μ = covariance (fun (ω : Ω) => X ω) Z μ + covariance (fun (ω : Ω) => Y ω) Z μ

theorem ProbabilityTheory.covariance_fun_add_right {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y Z : Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.MemLp X 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) (hZ : MeasureTheory.MemLp Z 2 μ) : covariance X (fun (ω : Ω) => Y ω + Z ω) μ = covariance X (fun (ω : Ω) => Y ω) μ + covariance X (fun (ω : Ω) => Z ω) μ

theorem ProbabilityTheory.variance_fun_div {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (c : ℝ) (hX : AEMeasurable X μ) : variance (fun (ω : Ω) => X ω / c) μ = variance X μ / c ^ 2

theorem MeasurableSpace.comap_process {Ω : Type u_1} {T : Type u_2} {𝓧 : T → Type u_3} [(t : T) → MeasurableSpace (𝓧 t)] (X : (t : T) → Ω → 𝓧 t) : MeasurableSpace.comap (fun (ω : Ω) (t : T) => X t ω) pi = ⨆ (t : T), MeasurableSpace.comap (X t) inferInstance

theorem MeasurableSpace.comap_le_comap {Ω : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} [m𝓧 : MeasurableSpace 𝓧] [m𝓨 : MeasurableSpace 𝓨] {X : Ω → 𝓧} {Y : Ω → 𝓨} (f : 𝓧 → 𝓨) (hf : Measurable f) (h : Y = f ∘ X) : MeasurableSpace.comap Y m𝓨 ≤ MeasurableSpace.comap X m𝓧

theorem MeasurableSpace.generateFrom_singleton_eq_comap_indicator_one {Ω : Type u_1} {A : Set Ω} : generateFrom {A} = MeasurableSpace.comap (A.indicator 1) inferInstance

theorem ProbabilityTheory.singleton_indepSets_comap_iff {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsZeroOrProbabilityMeasure P] {𝓧 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {A : Set Ω} {X : Ω → 𝓧} (hX : Measurable X) (hA : MeasurableSet A) : IndepSets {A} {s : Set Ω | MeasurableSet s} P ↔ IndepFun (A.indicator 1) X P

theorem IndepSets.setIntegral_eq_mul {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧} [MeasureTheory.IsZeroOrProbabilityMeasure μ] {f : 𝓧 → ℝ} {A : Set Ω} (hA1 : ProbabilityTheory.IndepSets {A} {s : Set Ω | MeasurableSet s} μ) (hX : Measurable X) (hA2 : MeasurableSet A) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map X μ)) : ∫ (ω : Ω) in A, f (X ω) ∂μ = μ.real A * ∫ (ω : Ω), f (X ω) ∂μ

theorem Indep.singleton_indepSets {Ω : Type u_1} {m1 m2 mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} (h : ProbabilityTheory.Indep m1 m2 P) {A : Set Ω} (hA : MeasurableSet A) : ProbabilityTheory.IndepSets {A} {s : Set Ω | MeasurableSet s} P

theorem measurableSpace_le_iff {Ω : Type u_1} {m1 m2 : MeasurableSpace Ω} : m1 ≤ m2 ↔ ∀ (s : Set Ω), MeasurableSet s → MeasurableSet s