Measure theory lemmas to be upstreamed to Mathlib

theorem AEMeasurable.eval {X : Type u_1} {ι : Type u_2} {Y : ι → Type u_3} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} [(i : ι) → MeasurableSpace (Y i)] {i : ι} {f : X → (i : ι) → Y i} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : X) => f x i) μ

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 MeasureTheory.MemLp.aemeasurable {X : Type u_1} {Y : Type u_2} {mX : MeasurableSpace X} {μ : Measure X} [MeasurableSpace Y] [ENorm Y] [TopologicalSpace Y] [TopologicalSpace.PseudoMetrizableSpace Y] [BorelSpace Y] {f : X → Y} {p : ENNReal} (hf : MemLp f p μ) : AEMeasurable f μ

theorem ProbabilityTheory.charFun_pi {ι : Type u_1} [Fintype ι] {E : ι → Type u_2} {mE : (i : ι) → MeasurableSpace (E i)} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] (μ : (i : ι) → MeasureTheory.Measure (E i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (t : PiLp 2 E) : MeasureTheory.charFun (MeasureTheory.Measure.pi μ) t = ∏ i : ι, MeasureTheory.charFun (μ i) (t i)

@[simp]

theorem ProbabilityTheory.charFun_toDual_symm_eq_charFunDual {E : Type u_1} [NormedAddCommGroup E] [CompleteSpace E] [InnerProductSpace ℝ E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} (L : NormedSpace.Dual ℝ E) : MeasureTheory.charFun μ ((InnerProductSpace.toDual ℝ E).symm L) = MeasureTheory.charFunDual μ L

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

theorem MeasureTheory.Measure.pi_map_eval {ι : Type u_1} [Fintype ι] {Ω : ι → Type u_2} {mΩ : (i : ι) → MeasurableSpace (Ω i)} {μ : (i : ι) → Measure (Ω i)} [∀ (i : ι), IsFiniteMeasure (μ i)] [DecidableEq ι] (i : ι) : map (Function.eval i) (Measure.pi μ) = (∏ j ∈ Finset.univ.erase i, (μ j) Set.univ) • μ i

theorem ProbabilityTheory.measurePreserving_eval {ι : Type u_1} [Fintype ι] {Ω : ι → Type u_2} {mΩ : (i : ι) → MeasurableSpace (Ω i)} {μ : (i : ι) → MeasureTheory.Measure (Ω i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (i : ι) : MeasureTheory.MeasurePreserving (Function.eval i) (MeasureTheory.Measure.pi μ) (μ i)

theorem ProbabilityTheory.iIndepFun_pi {ι : Type u_1} [Fintype ι] {Ω : ι → Type u_2} {mΩ : (i : ι) → MeasurableSpace (Ω i)} {μ : (i : ι) → MeasureTheory.Measure (Ω i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {𝒳 : ι → Type u_3} [(i : ι) → MeasurableSpace (𝒳 i)] {X : (i : ι) → Ω i → 𝒳 i} (mX : ∀ (i : ι), Measurable (X i)) : iIndepFun (fun (i : ι) (ω : (i : ι) → Ω i) => X i (ω i)) (MeasureTheory.Measure.pi μ)

theorem ProbabilityTheory.iIndepFun_pi₀ {ι : Type u_1} [Fintype ι] {Ω : ι → Type u_2} {mΩ : (i : ι) → MeasurableSpace (Ω i)} {μ : (i : ι) → MeasureTheory.Measure (Ω i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {𝒳 : ι → Type u_3} [(i : ι) → MeasurableSpace (𝒳 i)] {X : (i : ι) → Ω i → 𝒳 i} (mX : ∀ (i : ι), AEMeasurable (X i) (μ i)) : iIndepFun (fun (i : ι) (ω : (i : ι) → Ω i) => X i (ω i)) (MeasureTheory.Measure.pi μ)

theorem ProbabilityTheory.variance_pi {ι : Type u_1} [Fintype ι] {Ω : ι → Type u_2} {mΩ : (i : ι) → MeasurableSpace (Ω i)} {μ : (i : ι) → MeasureTheory.Measure (Ω i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {X : (i : ι) → Ω i → ℝ} (h : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 (μ i)) : variance (∑ i : ι, fun (ω : (i : ι) → Ω i) => X i (ω i)) (MeasureTheory.Measure.pi μ) = ∑ i : ι, variance (X i) (μ i)

theorem ProbabilityTheory.variance_sub {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.MemLp X 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) : variance (X - Y) μ = variance X μ - 2 * covariance X Y μ + variance Y μ

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

theorem ProbabilityTheory.covariance_mul_left {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} (c : ℝ) : covariance (fun (ω : Ω) => c * X ω) Y μ = c * covariance X Y μ

theorem ProbabilityTheory.covariance_mul_right {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} (c : ℝ) : covariance X (fun (ω : Ω) => c * Y ω) μ = c * covariance X Y μ

theorem ProbabilityTheory.covariance_sum_left' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {Y : Ω → ℝ} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} [MeasureTheory.IsFiniteMeasure μ] (hX : ∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) : covariance (∑ i ∈ s, X i) Y μ = ∑ i ∈ s, covariance (X i) Y μ

theorem ProbabilityTheory.covariance_sum_left {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {Y : Ω → ℝ} {ι : Type u_2} {X : ι → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] [Fintype ι] (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) : covariance (∑ i : ι, X i) Y μ = ∑ i : ι, covariance (X i) Y μ

theorem ProbabilityTheory.covariance_fun_sum_left' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {Y : Ω → ℝ} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} [MeasureTheory.IsFiniteMeasure μ] (hX : ∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) : covariance (fun (ω : Ω) => ∑ i ∈ s, X i ω) Y μ = ∑ i ∈ s, covariance (fun (ω : Ω) => X i ω) Y μ

theorem ProbabilityTheory.covariance_fun_sum_left {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {Y : Ω → ℝ} {ι : Type u_2} {X : ι → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] [Fintype ι] (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) : covariance (fun (ω : Ω) => ∑ i : ι, X i ω) Y μ = ∑ i : ι, covariance (fun (ω : Ω) => X i ω) Y μ

theorem ProbabilityTheory.covariance_sum_right' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {Y : Ω → ℝ} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} [MeasureTheory.IsFiniteMeasure μ] (hX : ∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) : covariance Y (∑ i ∈ s, X i) μ = ∑ i ∈ s, covariance Y (X i) μ

theorem ProbabilityTheory.covariance_sum_right {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {Y : Ω → ℝ} {ι : Type u_2} {X : ι → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] [Fintype ι] (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) : covariance Y (∑ i : ι, X i) μ = ∑ i : ι, covariance Y (X i) μ

theorem ProbabilityTheory.covariance_fun_sum_right' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {Y : Ω → ℝ} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} [MeasureTheory.IsFiniteMeasure μ] (hX : ∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) : covariance Y (fun (ω : Ω) => ∑ i ∈ s, X i ω) μ = ∑ i ∈ s, covariance Y (fun (ω : Ω) => X i ω) μ

theorem ProbabilityTheory.covariance_fun_sum_right {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {Y : Ω → ℝ} {ι : Type u_2} {X : ι → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] [Fintype ι] (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) : covariance Y (fun (ω : Ω) => ∑ i : ι, X i ω) μ = ∑ i : ι, covariance Y (fun (ω : Ω) => X i ω) μ

theorem ProbabilityTheory.covariance_sum_sum' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} [MeasureTheory.IsFiniteMeasure μ] {ι' : Type u_3} {Y : ι' → Ω → ℝ} {t : Finset ι'} (hX : ∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) (hY : ∀ i ∈ t, MeasureTheory.MemLp (Y i) 2 μ) : covariance (∑ i ∈ s, X i) (∑ j ∈ t, Y j) μ = ∑ i ∈ s, ∑ j ∈ t, covariance (X i) (Y j) μ

theorem ProbabilityTheory.covariance_sum_sum {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] [Fintype ι] {ι' : Type u_3} [Fintype ι'] {Y : ι' → Ω → ℝ} (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) (hY : ∀ (i : ι'), MeasureTheory.MemLp (Y i) 2 μ) : covariance (∑ i : ι, X i) (∑ j : ι', Y j) μ = ∑ i : ι, ∑ j : ι', covariance (X i) (Y j) μ

theorem ProbabilityTheory.covariance_fun_sum_fun_sum' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} [MeasureTheory.IsFiniteMeasure μ] {ι' : Type u_3} {Y : ι' → Ω → ℝ} {t : Finset ι'} (hX : ∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) (hY : ∀ i ∈ t, MeasureTheory.MemLp (Y i) 2 μ) : covariance (fun (ω : Ω) => ∑ i ∈ s, X i ω) (fun (ω : Ω) => ∑ j ∈ t, Y j ω) μ = ∑ i ∈ s, ∑ j ∈ t, covariance (fun (ω : Ω) => X i ω) (fun (ω : Ω) => Y j ω) μ

theorem ProbabilityTheory.covariance_fun_sum_fun_sum {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] [Fintype ι] {ι' : Type u_3} [Fintype ι'] {Y : ι' → Ω → ℝ} (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) (hY : ∀ (i : ι'), MeasureTheory.MemLp (Y i) 2 μ) : covariance (fun (ω : Ω) => ∑ i : ι, X i ω) (fun (ω : Ω) => ∑ j : ι', Y j ω) μ = ∑ i : ι, ∑ j : ι', covariance (fun (ω : Ω) => X i ω) (fun (ω : Ω) => Y j ω) μ

theorem ProbabilityTheory.variance_sum' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} [MeasureTheory.IsFiniteMeasure μ] (hX : ∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) : variance (∑ i ∈ s, X i) μ = ∑ i ∈ s, ∑ j ∈ s, covariance (X i) (X j) μ

theorem ProbabilityTheory.variance_sum {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] [Fintype ι] (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) : variance (∑ i : ι, X i) μ = ∑ i : ι, ∑ j : ι, covariance (X i) (X j) μ

theorem ProbabilityTheory.variance_fun_sum' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} [MeasureTheory.IsFiniteMeasure μ] (hX : ∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) : variance (fun (ω : Ω) => ∑ i ∈ s, X i ω) μ = ∑ i ∈ s, ∑ j ∈ s, covariance (fun (ω : Ω) => X i ω) (fun (ω : Ω) => X j ω) μ

theorem ProbabilityTheory.variance_fun_sum {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] [Fintype ι] (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) : variance (fun (ω : Ω) => ∑ i : ι, X i ω) μ = ∑ i : ι, ∑ j : ι, covariance (fun (ω : Ω) => X i ω) (fun (ω : Ω) => X j ω) μ

theorem ProbabilityTheory.covariance_map_equiv {Ω : Type u_3} {Ω' : Type u_4} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω'} (X Y : Ω → ℝ) (Z : Ω' ≃ᵐ Ω) : covariance X Y (MeasureTheory.Measure.map (⇑Z) μ) = covariance (X ∘ ⇑Z) (Y ∘ ⇑Z) μ

theorem ProbabilityTheory.covariance_map {Ω : Type u_3} {Ω' : Type u_4} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω'} {X Y : Ω → ℝ} {Z : Ω' → Ω} (hX : MeasureTheory.AEStronglyMeasurable X (MeasureTheory.Measure.map Z μ)) (hY : MeasureTheory.AEStronglyMeasurable Y (MeasureTheory.Measure.map Z μ)) (hZ : AEMeasurable Z μ) : covariance X Y (MeasureTheory.Measure.map Z μ) = covariance (X ∘ Z) (Y ∘ Z) μ

theorem ProbabilityTheory.covariance_map_fun {Ω : Type u_3} {Ω' : Type u_4} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω'} {X Y : Ω → ℝ} {Z : Ω' → Ω} (hX : MeasureTheory.AEStronglyMeasurable X (MeasureTheory.Measure.map Z μ)) (hY : MeasureTheory.AEStronglyMeasurable Y (MeasureTheory.Measure.map Z μ)) (hZ : AEMeasurable Z μ) : covariance X Y (MeasureTheory.Measure.map Z μ) = covariance (fun (ω : Ω') => X (Z ω)) (fun (ω : Ω') => Y (Z ω)) μ

theorem ProbabilityTheory.variance_map_equiv {Ω : Type u_3} {Ω' : Type u_4} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω'} (X : Ω → ℝ) (Y : Ω' ≃ᵐ Ω) : variance X (MeasureTheory.Measure.map (⇑Y) μ) = variance (X ∘ ⇑Y) μ

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

theorem ContinuousLinearMap.integral_comp_id_comm' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [CompleteSpace E] [CompleteSpace F] [MeasurableSpace E] {μ : MeasureTheory.Measure E} (h : MeasureTheory.Integrable _root_.id μ) (L : E →L[𝕜] F) : ∫ (x : E), L x ∂μ = L (∫ (x : E), _root_.id x ∂μ)

theorem ContinuousLinearMap.integral_comp_id_comm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [CompleteSpace E] [CompleteSpace F] [MeasurableSpace E] {μ : MeasureTheory.Measure E} (h : MeasureTheory.Integrable _root_.id μ) (L : E →L[𝕜] F) : ∫ (x : E), L x ∂μ = L (∫ (x : E), x ∂μ)

theorem ContinuousLinearMap.integral_id_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [CompleteSpace E] [CompleteSpace F] [MeasurableSpace E] {μ : MeasureTheory.Measure E} [OpensMeasurableSpace E] [MeasurableSpace F] [BorelSpace F] [SecondCountableTopology F] (h : MeasureTheory.Integrable _root_.id μ) (L : E →L[𝕜] F) : ∫ (x : F), x ∂MeasureTheory.Measure.map (⇑L) μ = L (∫ (x : E), x ∂μ)

theorem EuclideanSpace.coe_measurableEquiv' {ι : Type u_1} : ⇑(EuclideanSpace.measurableEquiv ι) = ⇑(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) : μ (EMetric.ball a r) = μ (EMetric.ball 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) : μ (EMetric.ball a r) = μ (EMetric.ball 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) : μ (EMetric.ball a r) = μ (EMetric.ball 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) : μ (EMetric.ball a r) = μ (EMetric.ball 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) : μ (EMetric.closedBall a r) = μ (EMetric.closedBall 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) : μ (EMetric.closedBall a r) = μ (EMetric.closedBall 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) : μ (EMetric.closedBall a r) = μ (EMetric.closedBall 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) : μ (EMetric.closedBall a r) = μ (EMetric.closedBall 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 (EMetric.closedBall x r) / MeasureTheory.volume (EMetric.closedBall y s) = (r / s) ^ Module.finrank ℝ E

theorem MeasureTheory.Isometry.single {ι : Type u_1} [Fintype ι] [DecidableEq ι] {E : ι → Type u_4} [(i : ι) → PseudoEMetricSpace (E i)] [(i : ι) → Zero (E i)] (i : ι) : Isometry (Pi.single i)

theorem MeasureTheory.memLp_pi_iff {ι : Type u_1} {Ω : Type u_2} {E : ι → Type u_3} [Fintype ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} [(i : ι) → NormedAddCommGroup (E i)] {p : ENNReal} {X : (i : ι) → Ω → E i} : MemLp (fun (ω : Ω) (x : ι) => X x ω) p P ↔ ∀ (i : ι), MemLp (X i) p P

theorem MeasureTheory.MemLp.of_eval {ι : Type u_1} {Ω : Type u_2} {E : ι → Type u_3} [Fintype ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} [(i : ι) → NormedAddCommGroup (E i)] {p : ENNReal} {X : (i : ι) → Ω → E i} : (∀ (i : ι), MemLp (X i) p P) → MemLp (fun (ω : Ω) (x : ι) => X x ω) p P

Alias of the reverse direction of MeasureTheory.memLp_pi_iff.

theorem MeasureTheory.MemLp.eval {ι : Type u_1} {Ω : Type u_2} {E : ι → Type u_3} [Fintype ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} [(i : ι) → NormedAddCommGroup (E i)] {p : ENNReal} {X : (i : ι) → Ω → E i} : MemLp (fun (ω : Ω) (x : ι) => X x ω) p P → ∀ (i : ι), MemLp (X i) p P

Alias of the forward direction of MeasureTheory.memLp_pi_iff.

theorem MeasureTheory.integrable_pi_iff {ι : Type u_1} {Ω : Type u_2} {E : ι → Type u_3} [Fintype ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} [(i : ι) → NormedAddCommGroup (E i)] {X : (i : ι) → Ω → E i} : Integrable (fun (ω : Ω) (x : ι) => X x ω) P ↔ ∀ (i : ι), Integrable (X i) P

theorem MeasureTheory.Integrable.eval {ι : Type u_1} {Ω : Type u_2} {E : ι → Type u_3} [Fintype ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} [(i : ι) → NormedAddCommGroup (E i)] {X : (i : ι) → Ω → E i} : Integrable (fun (ω : Ω) (x : ι) => X x ω) P → ∀ (i : ι), Integrable (X i) P

Alias of the forward direction of MeasureTheory.integrable_pi_iff.

theorem MeasureTheory.Integrable.of_eval {ι : Type u_1} {Ω : Type u_2} {E : ι → Type u_3} [Fintype ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} [(i : ι) → NormedAddCommGroup (E i)] {X : (i : ι) → Ω → E i} : (∀ (i : ι), Integrable (X i) P) → Integrable (fun (ω : Ω) (x : ι) => X x ω) P

Alias of the reverse direction of MeasureTheory.integrable_pi_iff.

theorem MeasureTheory.integral_eval {ι : Type u_1} {Ω : Type u_2} {E : ι → Type u_3} [Fintype ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} [(i : ι) → NormedAddCommGroup (E i)] {X : (i : ι) → Ω → E i} [(i : ι) → NormedSpace ℝ (E i)] [∀ (i : ι), CompleteSpace (E i)] (hX : ∀ (i : ι), Integrable (X i) P) (i : ι) : (∫ (ω : Ω) (x : ι), X x ω ∂P) i = ∫ (ω : Ω), X i ω ∂P

theorem MeasureTheory.memLp_piLp_iff {ι : Type u_1} {Ω : Type u_2} {E : ι → Type u_3} [Fintype ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} [(i : ι) → NormedAddCommGroup (E i)] {p q : ENNReal} [Fact (1 ≤ q)] {X : Ω → PiLp q E} : MemLp X p P ↔ ∀ (i : ι), MemLp (fun (x : Ω) => X x i) p P

theorem MeasureTheory.MemLp.eval_piLp {ι : Type u_1} {Ω : Type u_2} {E : ι → Type u_3} [Fintype ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} [(i : ι) → NormedAddCommGroup (E i)] {p q : ENNReal} [Fact (1 ≤ q)] {X : Ω → PiLp q E} : MemLp X p P → ∀ (i : ι), MemLp (fun (x : Ω) => X x i) p P

Alias of the forward direction of MeasureTheory.memLp_piLp_iff.

theorem MeasureTheory.MemLp.of_eval_piLp {ι : Type u_1} {Ω : Type u_2} {E : ι → Type u_3} [Fintype ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} [(i : ι) → NormedAddCommGroup (E i)] {p q : ENNReal} [Fact (1 ≤ q)] {X : Ω → PiLp q E} : (∀ (i : ι), MemLp (fun (x : Ω) => X x i) p P) → MemLp X p P

Alias of the reverse direction of MeasureTheory.memLp_piLp_iff.

theorem MeasureTheory.integrable_piLp_iff {ι : Type u_1} {Ω : Type u_2} {E : ι → Type u_3} [Fintype ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} [(i : ι) → NormedAddCommGroup (E i)] {q : ENNReal} [Fact (1 ≤ q)] {X : Ω → PiLp q E} : Integrable X P ↔ ∀ (i : ι), Integrable (fun (x : Ω) => X x i) P

theorem MeasureTheory.Integrable.of_eval_piLp {ι : Type u_1} {Ω : Type u_2} {E : ι → Type u_3} [Fintype ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} [(i : ι) → NormedAddCommGroup (E i)] {q : ENNReal} [Fact (1 ≤ q)] {X : Ω → PiLp q E} : (∀ (i : ι), Integrable (fun (x : Ω) => X x i) P) → Integrable X P

Alias of the reverse direction of MeasureTheory.integrable_piLp_iff.

theorem MeasureTheory.Integrable.eval_piLp {ι : Type u_1} {Ω : Type u_2} {E : ι → Type u_3} [Fintype ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} [(i : ι) → NormedAddCommGroup (E i)] {q : ENNReal} [Fact (1 ≤ q)] {X : Ω → PiLp q E} : Integrable X P → ∀ (i : ι), Integrable (fun (x : Ω) => X x i) P

Alias of the forward direction of MeasureTheory.integrable_piLp_iff.

theorem PiLp.integral_eval {ι : Type u_1} {Ω : Type u_2} {E : ι → Type u_3} [Fintype ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [(i : ι) → NormedAddCommGroup (E i)] {q : ENNReal} [Fact (1 ≤ q)] {X : Ω → PiLp q E} [(i : ι) → NormedSpace ℝ (E i)] [∀ (i : ι), CompleteSpace (E i)] (hX : ∀ (i : ι), MeasureTheory.Integrable (fun (x : Ω) => X x i) P) (i : ι) : (∫ (ω : Ω), X ω ∂P) i = ∫ (ω : Ω), X ω i ∂P