# Probability density function #

This file defines the probability density function of random variables, by which we mean measurable functions taking values in a Borel space. The probability density function is defined as the Radon–Nikodym derivative of the law of `X`. In particular, a measurable function `f` is said to the probability density function of a random variable `X` if for all measurable sets `S`, `ℙ(X ∈ S) = ∫ x in S, f x dx`. Probability density functions are one way of describing the distribution of a random variable, and are useful for calculating probabilities and finding moments (although the latter is better achieved with moment-generating functions).

This file also defines the continuous uniform distribution and proves some properties about random variables with this distribution.

## Main definitions #

- `MeasureTheory.HasPDF` : A random variable `X : Ω → E` is said to `HasPDF` with respect to the measure `ℙ` on `Ω` and `μ` on `E` if the push-forward measure of `ℙ` along `X` is absolutely continuous with respect to `μ` and they `HaveLebesgueDecomposition`.
- `MeasureTheory.pdf` : If `X` is a random variable that `HasPDF X ℙ μ`, then `pdf X` is the Radon–Nikodym derivative of the push-forward measure of `ℙ` along `X` with respect to `μ`.
- `MeasureTheory.pdf.IsUniform` : A random variable `X` is said to follow the uniform distribution if it has a constant probability density function with a compact, non-null support.

## Main results #

- `MeasureTheory.pdf.integral_pdf_smul` : Law of the unconscious statistician, i.e. if a random variable `X : Ω → E` has pdf `f`, then `𝔼(g(X)) = ∫ x, f x • g x dx` for all measurable `g : E → F`.
- `MeasureTheory.pdf.integral_mul_eq_integral` : A real-valued random variable `X` with pdf `f` has expectation `∫ x, x * f x dx`.
- `MeasureTheory.pdf.IsUniform.integral_eq` : If `X` follows the uniform distribution with its pdf having support `s`, then `X` has expectation `(λ s)⁻¹ * ∫ x in s, x dx` where `λ` is the Lebesgue measure.

## TODO #

Ultimately, we would also like to define characteristic functions to describe distributions as it exists for all random variables. However, to define this, we will need Fourier transforms which we currently do not have.

source
class MeasureTheory.HasPDF {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω) (μ : Measure E := by volume_tac) :
Prop

A random variable `X : Ω → E` is said to have a probability density function (`HasPDF`) with respect to the measure `ℙ` on `Ω` and `μ` on `E` if the push-forward measure of `ℙ` along `X` is absolutely continuous with respect to `μ` and they have a Lebesgue decomposition (`HaveLebesgueDecomposition`).

- aemeasurable' : AEMeasurable X ℙ
- haveLebesgueDecomposition' : (Measure.map X ℙ).HaveLebesgueDecomposition μ
- absolutelyContinuous' : (Measure.map X ℙ).AbsolutelyContinuous μ

Instances

source
theorem MeasureTheory.hasPDF_iff {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {x✝ : MeasurableSpace Ω} {X : Ω → E} {ℙ : Measure Ω} {μ : Measure E} :
HasPDF X ℙ μ ↔ AEMeasurable X ℙ ∧ (Measure.map X ℙ).HaveLebesgueDecomposition μ ∧ (Measure.map X ℙ).AbsolutelyContinuous μ
source
theorem MeasureTheory.hasPDF_iff_of_aemeasurable {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {x✝ : MeasurableSpace Ω} {X : Ω → E} {ℙ : Measure Ω} {μ : Measure E} (hX : AEMeasurable X ℙ) :
HasPDF X ℙ μ ↔ (Measure.map X ℙ).HaveLebesgueDecomposition μ ∧ (Measure.map X ℙ).AbsolutelyContinuous μ
source
theorem MeasureTheory.HasPDF.aemeasurable {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {x✝ : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω) (μ : Measure E) [HasPDF X ℙ μ] :
AEMeasurable X ℙ
source
instance MeasureTheory.HasPDF.haveLebesgueDecomposition {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {x✝ : MeasurableSpace Ω} {X : Ω → E} {ℙ : Measure Ω} {μ : Measure E} [HasPDF X ℙ μ] :
(Measure.map X ℙ).HaveLebesgueDecomposition μ
source
theorem MeasureTheory.HasPDF.absolutelyContinuous {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {x✝ : MeasurableSpace Ω} {X : Ω → E} {ℙ : Measure Ω} {μ : Measure E} [HasPDF X ℙ μ] :
(Measure.map X ℙ).AbsolutelyContinuous μ
source
theorem MeasureTheory.HasPDF.quasiMeasurePreserving_of_measurable {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {x✝ : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω) (μ : Measure E) [HasPDF X ℙ μ] (h : Measurable X) :
Measure.QuasiMeasurePreserving X ℙ μ

A random variable that `HasPDF` is quasi-measure-preserving.

source
theorem MeasureTheory.HasPDF.congr {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {x✝ : MeasurableSpace Ω} {X Y : Ω → E} {ℙ : Measure Ω} {μ : Measure E} (hXY : X =ᶠ[ae ℙ] Y) [hX : HasPDF X ℙ μ] :
HasPDF Y ℙ μ
source
theorem MeasureTheory.HasPDF.congr_iff {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {x✝ : MeasurableSpace Ω} {X Y : Ω → E} {ℙ : Measure Ω} {μ : Measure E} (hXY : X =ᶠ[ae ℙ] Y) :
HasPDF X ℙ μ ↔ HasPDF Y ℙ μ
source
theorem MeasureTheory.hasPDF_of_map_eq_withDensity {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {x✝ : MeasurableSpace Ω} {X : Ω → E} {ℙ : Measure Ω} {μ : Measure E} (hX : AEMeasurable X ℙ) (f : E → ENNReal) (hf : AEMeasurable f μ) (h : Measure.map X ℙ = μ.withDensity f) :
HasPDF X ℙ μ

X `HasPDF` if there is a pdf `f` such that `map X ℙ = μ.withDensity f`.

source
def MeasureTheory.pdf {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {x✝ : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω) (μ : Measure E := by volume_tac) :
E → ENNReal

If `X` is a random variable, then `pdf X ℙ μ` is the Radon–Nikodym derivative of the push-forward measure of `ℙ` along `X` with respect to `μ`.

Equations

- MeasureTheory.pdf X ℙ μ = (MeasureTheory.Measure.map X ℙ).rnDeriv μ

Instances For

source
theorem MeasureTheory.pdf_def {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {x✝ : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {X : Ω → E} :
pdf X ℙ μ = (Measure.map X ℙ).rnDeriv μ
source
theorem MeasureTheory.pdf_of_not_aemeasurable {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {x✝ : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {X : Ω → E} (hX : ¬AEMeasurable X ℙ) :
pdf X ℙ μ =ᶠ[ae μ] 0
source
theorem MeasureTheory.pdf_of_not_haveLebesgueDecomposition {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {x✝ : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {X : Ω → E} (h : ¬(Measure.map X ℙ).HaveLebesgueDecomposition μ) :
pdf X ℙ μ = 0
source
theorem MeasureTheory.aemeasurable_of_pdf_ne_zero {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} (X : Ω → E) (h : ¬pdf X ℙ μ =ᶠ[ae μ] 0) :
AEMeasurable X ℙ
source
theorem MeasureTheory.hasPDF_of_pdf_ne_zero {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {X : Ω → E} (hac : (Measure.map X ℙ).AbsolutelyContinuous μ) (hpdf : ¬pdf X ℙ μ =ᶠ[ae μ] 0) :
HasPDF X ℙ μ
source
theorem MeasureTheory.measurable_pdf {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω) (μ : Measure E := by volume_tac) :
Measurable (pdf X ℙ μ)
source
theorem MeasureTheory.withDensity_pdf_le_map {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {x✝ : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω) (μ : Measure E := by volume_tac) :
μ.withDensity (pdf X ℙ μ) ≤ Measure.map X ℙ
source
theorem MeasureTheory.setLIntegral_pdf_le_map {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω) (μ : Measure E := by volume_tac) (s : Set E) :
∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ ≤ (Measure.map X ℙ) s
source
theorem MeasureTheory.map_eq_withDensity_pdf {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω) (μ : Measure E := by volume_tac) [hX : HasPDF X ℙ μ] :
Measure.map X ℙ = μ.withDensity (pdf X ℙ μ)
source
theorem MeasureTheory.map_eq_setLIntegral_pdf {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω) (μ : Measure E := by volume_tac) [hX : HasPDF X ℙ μ] {s : Set E} (hs : MeasurableSet s) :
(Measure.map X ℙ) s = ∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ
source
theorem MeasureTheory.pdf.congr {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {X Y : Ω → E} (hXY : X =ᶠ[ae ℙ] Y) :
pdf X ℙ μ = pdf Y ℙ μ
source
theorem MeasureTheory.pdf.lintegral_eq_measure_univ {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {X : Ω → E} [HasPDF X ℙ μ] :
∫⁻ (x : E), pdf X ℙ μ x ∂μ = ℙ Set.univ
source
theorem MeasureTheory.pdf.eq_of_map_eq_withDensity {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} [IsFiniteMeasure ℙ] {X : Ω → E} [HasPDF X ℙ μ] (f : E → ENNReal) (hmf : AEMeasurable f μ) :
Measure.map X ℙ = μ.withDensity f ↔ pdf X ℙ μ =ᶠ[ae μ] f
source
theorem MeasureTheory.pdf.eq_of_map_eq_withDensity' {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} [SigmaFinite μ] {X : Ω → E} [HasPDF X ℙ μ] (f : E → ENNReal) (hmf : AEMeasurable f μ) :
Measure.map X ℙ = μ.withDensity f ↔ pdf X ℙ μ =ᶠ[ae μ] f
source
theorem MeasureTheory.pdf.ae_lt_top {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : Measure Ω} [IsFiniteMeasure ℙ] {μ : Measure E} {X : Ω → E} :
∀ᵐ (x : E) ∂μ, pdf X ℙ μ x < ⊤
source
theorem MeasureTheory.pdf.ofReal_toReal_ae_eq {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} [IsFiniteMeasure ℙ] {X : Ω → E} :
(fun (x : E) => ENNReal.ofReal (pdf X ℙ μ x).toReal) =ᶠ[ae μ] pdf X ℙ μ
source
theorem MeasureTheory.pdf.lintegral_pdf_mul {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {X : Ω → E} [HasPDF X ℙ μ] {f : E → ENNReal} (hf : AEMeasurable f μ) :
∫⁻ (x : E), pdf X ℙ μ x * f x ∂μ = ∫⁻ (x : Ω), f (X x) ∂ℙ

The Law of the Unconscious Statistician for nonnegative random variables.

source
theorem MeasureTheory.pdf.integrable_pdf_smul_iff {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsFiniteMeasure ℙ] {X : Ω → E} [HasPDF X ℙ μ] {f : E → F} (hf : AEStronglyMeasurable f μ) :
Integrable (fun (x : E) => (pdf X ℙ μ x).toReal • f x) μ ↔ Integrable (fun (x : Ω) => f (X x)) ℙ
source
theorem MeasureTheory.pdf.integral_pdf_smul {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsFiniteMeasure ℙ] {X : Ω → E} [HasPDF X ℙ μ] {f : E → F} (hf : AEStronglyMeasurable f μ) :
∫ (x : E), (pdf X ℙ μ x).toReal • f x ∂μ = ∫ (x : Ω), f (X x) ∂ℙ

The Law of the Unconscious Statistician: Given a random variable `X` and a measurable function `f`, `f ∘ X` is a random variable with expectation `∫ x, pdf X x • f x ∂μ` where `μ` is a measure on the codomain of `X`.

source
theorem MeasureTheory.pdf.quasiMeasurePreserving_hasPDF {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {F : Type u_3} [MeasurableSpace F] {ν : Measure F} (X : Ω → E) [HasPDF X ℙ μ] {g : E → F} (hg : Measure.QuasiMeasurePreserving g μ ν) (hmap : (Measure.map g (Measure.map X ℙ)).HaveLebesgueDecomposition ν) :
HasPDF (g ∘ X) ℙ ν

A random variable that `HasPDF` transformed under a `QuasiMeasurePreserving` map also `HasPDF` if `(map g (map X ℙ)).HaveLebesgueDecomposition μ`.

`quasiMeasurePreserving_hasPDF` is more useful in the case we are working with a probability measure and a real-valued random variable.

source
theorem MeasureTheory.pdf.quasiMeasurePreserving_hasPDF' {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {F : Type u_3} [MeasurableSpace F] {ν : Measure F} (X : Ω → E) [HasPDF X ℙ μ] {g : E → F} [SFinite ℙ] [SigmaFinite ν] (hg : Measure.QuasiMeasurePreserving g μ ν) :
HasPDF (g ∘ X) ℙ ν
source
theorem Real.hasPDF_iff {Ω : Type u_1} {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.SFinite ℙ] :
MeasureTheory.HasPDF X ℙ MeasureTheory.volume ↔ AEMeasurable X ℙ ∧ (MeasureTheory.Measure.map X ℙ).AbsolutelyContinuous MeasureTheory.volume
source
theorem Real.hasPDF_iff_of_aemeasurable {Ω : Type u_1} {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.SFinite ℙ] (hX : AEMeasurable X ℙ) :
MeasureTheory.HasPDF X ℙ MeasureTheory.volume ↔ (MeasureTheory.Measure.map X ℙ).AbsolutelyContinuous MeasureTheory.volume

A real-valued random variable `X` `HasPDF X ℙ λ` (where `λ` is the Lebesgue measure) if and only if the push-forward measure of `ℙ` along `X` is absolutely continuous with respect to `λ`.

source
theorem MeasureTheory.pdf.integral_mul_eq_integral {Ω : Type u_1} {m : MeasurableSpace Ω} {ℙ : Measure Ω} {X : Ω → ℝ} [IsFiniteMeasure ℙ] [HasPDF X ℙ volume] :
∫ (x : ℝ), x * (pdf X ℙ volume x).toReal = ∫ (x : Ω), X x ∂ℙ

If `X` is a real-valued random variable that has pdf `f`, then the expectation of `X` equals `∫ x, x * f x ∂λ` where `λ` is the Lebesgue measure.

source
theorem MeasureTheory.pdf.hasFiniteIntegral_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {ℙ : Measure Ω} {X : Ω → ℝ} [IsFiniteMeasure ℙ] {f : ℝ → ℝ} {g : ℝ → ENNReal} (hg : pdf X ℙ volume =ᶠ[ae volume] g) (hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ⊤) :
HasFiniteIntegral (fun (x : ℝ) => f x * (pdf X ℙ volume x).toReal) volume
source
theorem MeasureTheory.pdf.indepFun_iff_pdf_prod_eq_pdf_mul_pdf {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {F : Type u_3} [MeasurableSpace F] {ν : Measure F} {X : Ω → E} {Y : Ω → F} [IsFiniteMeasure ℙ] [SigmaFinite μ] [SigmaFinite ν] [HasPDF (fun (ω : Ω) => (X ω, Y ω)) ℙ (μ.prod ν)] :
ProbabilityTheory.IndepFun X Y ℙ ↔ pdf (fun (ω : Ω) => (X ω, Y ω)) ℙ (μ.prod ν) =ᶠ[ae (μ.prod ν)] fun (z : E × F) => pdf X ℙ μ z.1 * pdf Y ℙ ν z.2

Random variables are independent iff their joint density is a product of marginal densities.

source
theorem ProbabilityTheory.IndepFun.mul_hasPDF' {Ω : Type u_1} {G : Type u_2} {mΩ : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [Group G] {mG : MeasurableSpace G} [MeasurableMul₂ G] [MeasurableInv G] {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] {X Y : Ω → G} [MeasureTheory.SFinite μ] [MeasureTheory.HasPDF X ℙ μ] [MeasureTheory.HasPDF Y ℙ μ] (σX : MeasureTheory.SigmaFinite (MeasureTheory.Measure.map X ℙ)) (σY : MeasureTheory.SigmaFinite (MeasureTheory.Measure.map Y ℙ)) (hXY : IndepFun X Y ℙ) :
MeasureTheory.HasPDF (X * Y) ℙ μ
source
theorem ProbabilityTheory.IndepFun.add_hasPDF' {Ω : Type u_1} {G : Type u_2} {mΩ : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [AddGroup G] {mG : MeasurableSpace G} [MeasurableAdd₂ G] [MeasurableNeg G] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] {X Y : Ω → G} [MeasureTheory.SFinite μ] [MeasureTheory.HasPDF X ℙ μ] [MeasureTheory.HasPDF Y ℙ μ] (σX : MeasureTheory.SigmaFinite (MeasureTheory.Measure.map X ℙ)) (σY : MeasureTheory.SigmaFinite (MeasureTheory.Measure.map Y ℙ)) (hXY : IndepFun X Y ℙ) :
MeasureTheory.HasPDF (X + Y) ℙ μ
source
theorem ProbabilityTheory.IndepFun.mul_hasPDF {Ω : Type u_1} {G : Type u_2} {mΩ : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [Group G] {mG : MeasurableSpace G} [MeasurableMul₂ G] [MeasurableInv G] {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] {X Y : Ω → G} [MeasureTheory.SFinite μ] [MeasureTheory.HasPDF X ℙ μ] [MeasureTheory.HasPDF Y ℙ μ] [MeasureTheory.IsFiniteMeasure ℙ] (hXY : IndepFun X Y ℙ) :
MeasureTheory.HasPDF (X * Y) ℙ μ
source
theorem ProbabilityTheory.IndepFun.add_hasPDF {Ω : Type u_1} {G : Type u_2} {mΩ : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [AddGroup G] {mG : MeasurableSpace G} [MeasurableAdd₂ G] [MeasurableNeg G] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] {X Y : Ω → G} [MeasureTheory.SFinite μ] [MeasureTheory.HasPDF X ℙ μ] [MeasureTheory.HasPDF Y ℙ μ] [MeasureTheory.IsFiniteMeasure ℙ] (hXY : IndepFun X Y ℙ) :
MeasureTheory.HasPDF (X + Y) ℙ μ
source
theorem ProbabilityTheory.IndepFun.pdf_mul_eq_mlconvolution_pdf' {Ω : Type u_1} {G : Type u_2} {mΩ : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [Group G] {mG : MeasurableSpace G} [MeasurableMul₂ G] [MeasurableInv G] {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] {X Y : Ω → G} [MeasureTheory.SigmaFinite μ] [MeasureTheory.HasPDF X ℙ μ] [MeasureTheory.HasPDF Y ℙ μ] (σX : MeasureTheory.SigmaFinite (MeasureTheory.Measure.map X ℙ)) (σY : MeasureTheory.SigmaFinite (MeasureTheory.Measure.map Y ℙ)) (hXY : IndepFun X Y ℙ) :
MeasureTheory.pdf (X * Y) ℙ μ =ᵐ[μ] MeasureTheory.mlconvolution (MeasureTheory.pdf X ℙ μ) (MeasureTheory.pdf Y ℙ μ) μ
source
theorem ProbabilityTheory.IndepFun.pdf_add_eq_lconvolution_pdf' {Ω : Type u_1} {G : Type u_2} {mΩ : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [AddGroup G] {mG : MeasurableSpace G} [MeasurableAdd₂ G] [MeasurableNeg G] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] {X Y : Ω → G} [MeasureTheory.SigmaFinite μ] [MeasureTheory.HasPDF X ℙ μ] [MeasureTheory.HasPDF Y ℙ μ] (σX : MeasureTheory.SigmaFinite (MeasureTheory.Measure.map X ℙ)) (σY : MeasureTheory.SigmaFinite (MeasureTheory.Measure.map Y ℙ)) (hXY : IndepFun X Y ℙ) :
MeasureTheory.pdf (X + Y) ℙ μ =ᵐ[μ] MeasureTheory.lconvolution (MeasureTheory.pdf X ℙ μ) (MeasureTheory.pdf Y ℙ μ) μ
source
theorem ProbabilityTheory.IndepFun.pdf_mul_eq_mlconvolution_pdf {Ω : Type u_1} {G : Type u_2} {mΩ : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [Group G] {mG : MeasurableSpace G} [MeasurableMul₂ G] [MeasurableInv G] {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] {X Y : Ω → G} [MeasureTheory.SFinite μ] [MeasureTheory.HasPDF X ℙ μ] [MeasureTheory.HasPDF Y ℙ μ] [MeasureTheory.IsFiniteMeasure ℙ] (hXY : IndepFun X Y ℙ) :
MeasureTheory.pdf (X * Y) ℙ μ =ᵐ[μ] MeasureTheory.mlconvolution (MeasureTheory.pdf X ℙ μ) (MeasureTheory.pdf Y ℙ μ) μ
source
theorem ProbabilityTheory.IndepFun.pdf_add_eq_lconvolution_pdf {Ω : Type u_1} {G : Type u_2} {mΩ : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [AddGroup G] {mG : MeasurableSpace G} [MeasurableAdd₂ G] [MeasurableNeg G] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] {X Y : Ω → G} [MeasureTheory.SFinite μ] [MeasureTheory.HasPDF X ℙ μ] [MeasureTheory.HasPDF Y ℙ μ] [MeasureTheory.IsFiniteMeasure ℙ] (hXY : IndepFun X Y ℙ) :
MeasureTheory.pdf (X + Y) ℙ μ =ᵐ[μ] MeasureTheory.lconvolution (MeasureTheory.pdf X ℙ μ) (MeasureTheory.pdf Y ℙ μ) μ