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 variableX : Ω → Eis said toHasPDFwith respect to the measureℙonΩandμonEif the push-forward measure ofℙalongXis absolutely continuous with respect toμand theyHaveLebesgueDecomposition.MeasureTheory.pdf: IfXis a random variable thatHasPDF X ℙ μ, thenpdf Xis the Radon–Nikodym derivative of the push-forward measure ofℙalongXwith respect toμ.MeasureTheory.pdf.IsUniform: A random variableXis 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 variableX : Ω → Ehas pdff, then𝔼(g(X)) = ∫ x, f x • g x dxfor all measurableg : E → F.MeasureTheory.pdf.integral_mul_eq_integral: A real-valued random variableXwith pdffhas expectation∫ x, x * f x dx.MeasureTheory.pdf.IsUniform.integral_eq: IfXfollows the uniform distribution with its pdf having supports, thenXhas expectation(λ s)⁻¹ * ∫ x in s, x dxwhereλis the Lebesgue measure.
class
MeasureTheory.HasPDF
{Ω : Type u_1}
{E : Type u_2}
[MeasurableSpace E]
{m : MeasurableSpace Ω}
(X : Ω → E)
(ℙ : Measure Ω)
(μ : Measure E := by volume_tac)
:
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
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 μ
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 μ
theorem
MeasureTheory.HasPDF.aemeasurable
{Ω : Type u_1}
{E : Type u_2}
[MeasurableSpace E]
{x✝ : MeasurableSpace Ω}
(X : Ω → E)
(ℙ : Measure Ω)
(μ : Measure E)
[HasPDF X ℙ μ]
:
AEMeasurable X ℙ
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 μ
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 μ
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)
:
A random variable that HasPDF is quasi-measure-preserving.
theorem
MeasureTheory.HasPDF.congr
{Ω : Type u_1}
{E : Type u_2}
[MeasurableSpace E]
{x✝ : MeasurableSpace Ω}
{X Y : Ω → E}
{ℙ : Measure Ω}
{μ : Measure E}
(hXY : X =ᵐ[ℙ] Y)
[hX : HasPDF X ℙ μ]
:
HasPDF Y ℙ μ
theorem
MeasureTheory.HasPDF.congr_iff
{Ω : Type u_1}
{E : Type u_2}
[MeasurableSpace E]
{x✝ : MeasurableSpace Ω}
{X Y : Ω → E}
{ℙ : Measure Ω}
{μ : Measure E}
(hXY : X =ᵐ[ℙ] Y)
:
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.
noncomputable 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
theorem
MeasureTheory.pdf_def
{Ω : Type u_1}
{E : Type u_2}
[MeasurableSpace E]
{x✝ : MeasurableSpace Ω}
{ℙ : Measure Ω}
{μ : Measure E}
{X : Ω → E}
:
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 ℙ)
:
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 μ)
:
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 ℙ μ =ᵐ[μ] 0)
:
AEMeasurable X ℙ
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 ℙ μ =ᵐ[μ] 0)
:
HasPDF X ℙ μ
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 ℙ μ)
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)
:
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)
:
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 ℙ μ]
:
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)
:
theorem
MeasureTheory.pdf.congr
{Ω : Type u_1}
{E : Type u_2}
[MeasurableSpace E]
{m : MeasurableSpace Ω}
{ℙ : Measure Ω}
{μ : Measure E}
{X Y : Ω → E}
(hXY : X =ᵐ[ℙ] Y)
:
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 ℙ μ]
:
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 μ)
:
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 μ)
:
theorem
MeasureTheory.pdf.ae_lt_top
{Ω : Type u_1}
{E : Type u_2}
[MeasurableSpace E]
{m : MeasurableSpace Ω}
{ℙ : Measure Ω}
[IsFiniteMeasure ℙ]
{μ : Measure E}
{X : Ω → E}
:
theorem
MeasureTheory.pdf.ofReal_toReal_ae_eq
{Ω : Type u_1}
{E : Type u_2}
[MeasurableSpace E]
{m : MeasurableSpace Ω}
{ℙ : Measure Ω}
{μ : Measure E}
[IsFiniteMeasure ℙ]
{X : Ω → E}
:
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 μ)
:
The Law of the Unconscious Statistician for nonnegative random variables.
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 μ)
:
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 μ)
:
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.
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 ν)
:
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.
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 μ ν)
:
theorem
Real.hasPDF_iff
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{ℙ : MeasureTheory.Measure Ω}
{X : Ω → ℝ}
[MeasureTheory.SFinite ℙ]
:
theorem
Real.hasPDF_iff_of_aemeasurable
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{ℙ : MeasureTheory.Measure Ω}
{X : Ω → ℝ}
[MeasureTheory.SFinite ℙ]
(hX : AEMeasurable X ℙ)
:
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 λ.
theorem
MeasureTheory.pdf.integral_mul_eq_integral
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{ℙ : Measure Ω}
{X : Ω → ℝ}
[IsFiniteMeasure ℙ]
[HasPDF X ℙ volume]
:
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.
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 ν)]
:
Random variables are independent iff their joint density is a product of marginal densities.
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) ℙ μ
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) ℙ μ
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) ℙ μ
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) ℙ μ
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 ℙ μ) μ
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 ℙ μ) μ
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 ℙ μ) μ
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 ℙ μ) μ