Conditional cumulative distribution function #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Given ρ : measure (α × ℝ), we define the conditional cumulative distribution function
(conditional cdf) of ρ. It is a function cond_cdf ρ : α → ℝ → ℝ such that if ρ is a finite
measure, then for all a : α cond_cdf ρ a is monotone and right-continuous with limit 0 at -∞
and limit 1 at +∞, and such that for all x : ℝ, a ↦ cond_cdf ρ a x is measurable. For all
x : ℝ and measurable set s, that function satisfies
∫⁻ a in s, ennreal.of_real (cond_cdf ρ a x) ∂ρ.fst = ρ (s ×ˢ Iic x).
Main definitions #
probability_theory.cond_cdf ρ : α → stieltjes_function: the conditional cdf ofρ : measure (α × ℝ). Astieltjes_functionis a functionℝ → ℝwhich is monotone and right-continuous.
Main statements #
probability_theory.set_lintegral_cond_cdf: for alla : αandx : ℝ, all measurable sets,∫⁻ a in s, ennreal.of_real (cond_cdf ρ a x) ∂ρ.fst = ρ (s ×ˢ Iic x).
References #
The construction of the conditional cdf in this file follows the proof of Theorem 3.4 in O. Kallenberg, Foundations of modern probability.
TODO #
theorem
directed.sequence_le
{α : Type u_1}
{β : Type u_2}
[encodable α]
[inhabited α]
[preorder β]
{f : α → β}
(hf : directed ge f)
(a : α) :
f (directed.sequence f hf (encodable.encode a + 1)) ≤ f a
theorem
at_bot_le_nhds_bot
{α : Type u_1}
[topological_space α]
[linear_order α]
[order_bot α]
[order_topology α] :
theorem
at_top_le_nhds_top
{α : Type u_1}
[topological_space α]
[linear_order α]
[order_top α]
[order_topology α] :
theorem
tendsto_of_antitone
{ι : Type u_1}
{α : Type u_2}
[preorder ι]
[topological_space α]
[conditionally_complete_linear_order α]
[order_topology α]
{f : ι → α}
(h_mono : antitone f) :
filter.tendsto f filter.at_top filter.at_bot ∨ ∃ (l : α), filter.tendsto f filter.at_top (nhds l)
theorem
ennreal.of_real_cinfi
{α : Type u_1}
(f : α → ℝ)
[nonempty α] :
ennreal.of_real (⨅ (i : α), f i) = ⨅ (i : α), ennreal.of_real (f i)
theorem
lintegral_infi_directed_of_measurable
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
[countable β]
{f : β → α → ennreal}
{μ : measure_theory.measure α}
(hμ : μ ≠ 0)
(hf : ∀ (b : β), measurable (f b))
(hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ⊤)
(h_directed : directed ge f) :
Monotone convergence for an infimum over a directed family and indexed by a countable type
noncomputable
def
measure_theory.measure.Iic_snd
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(r : ℝ) :
Measure on α such that for a measurable set s, ρ.Iic_snd r s = ρ (s ×ˢ Iic r).
theorem
measure_theory.measure.Iic_snd_apply
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(r : ℝ)
{s : set α}
(hs : measurable_set s) :
theorem
measure_theory.measure.Iic_snd_mono
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
{r r' : ℝ}
(h_le : r ≤ r') :
theorem
measure_theory.measure.Iic_snd_le_fst
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(r : ℝ) :
theorem
measure_theory.measure.Iic_snd_ac_fst
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(r : ℝ) :
(ρ.Iic_snd r).absolutely_continuous ρ.fst
theorem
measure_theory.measure.is_finite_measure.Iic_snd
{α : Type u_1}
{mα : measurable_space α}
{ρ : measure_theory.measure (α × ℝ)}
[measure_theory.is_finite_measure ρ]
(r : ℝ) :
theorem
measure_theory.measure.infi_Iic_snd_gt
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(t : ℚ)
{s : set α}
(hs : measurable_set s)
[measure_theory.is_finite_measure ρ] :
theorem
measure_theory.measure.tendsto_Iic_snd_at_top
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
{s : set α}
(hs : measurable_set s) :
filter.tendsto (λ (r : ℚ), ⇑(ρ.Iic_snd ↑r) s) filter.at_top (nhds (⇑(ρ.fst) s))
theorem
measure_theory.measure.tendsto_Iic_snd_at_bot
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ]
{s : set α}
(hs : measurable_set s) :
filter.tendsto (λ (r : ℚ), ⇑(ρ.Iic_snd ↑r) s) filter.at_bot (nhds 0)
Auxiliary definitions #
We build towards the definition of probability_theory.cond_cdf. We first define
probability_theory.pre_cdf, a function defined on α × ℚ with the properties of a cdf almost
everywhere. We then introduce probability_theory.cond_cdf_rat, a function on α × ℚ which has
the properties of a cdf for all a : α. We finally extend to ℝ.
noncomputable
def
probability_theory.pre_cdf
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(r : ℚ) :
pre_cdf is the Radon-Nikodym derivative of ρ.Iic_snd with respect to ρ.fst at each
r : ℚ. This function ℚ → α → ℝ≥0∞ is such that for almost all a : α, the function ℚ → ℝ≥0∞
satisfies the properties of a cdf (monotone with limit 0 at -∞ and 1 at +∞, right-continuous).
We define this function on ℚ and not ℝ because ℚ is countable, which allows us to prove
properties of the form ∀ᵐ a ∂ρ.fst, ∀ q, P (pre_cdf q a), instead of the weaker
∀ q, ∀ᵐ a ∂ρ.fst, P (pre_cdf q a).
theorem
probability_theory.measurable_pre_cdf
{α : Type u_1}
{mα : measurable_space α}
{ρ : measure_theory.measure (α × ℝ)}
{r : ℚ} :
theorem
probability_theory.with_density_pre_cdf
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(r : ℚ)
[measure_theory.is_finite_measure ρ] :
ρ.fst.with_density (probability_theory.pre_cdf ρ r) = ρ.Iic_snd ↑r
theorem
probability_theory.set_lintegral_pre_cdf_fst
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(r : ℚ)
{s : set α}
(hs : measurable_set s)
[measure_theory.is_finite_measure ρ] :
theorem
probability_theory.monotone_pre_cdf
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ] :
theorem
probability_theory.set_lintegral_infi_gt_pre_cdf
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ]
(t : ℚ)
{s : set α}
(hs : measurable_set s) :
theorem
probability_theory.pre_cdf_le_one
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ] :
theorem
probability_theory.tendsto_lintegral_pre_cdf_at_top
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ] :
filter.tendsto (λ (r : ℚ), ∫⁻ (a : α), probability_theory.pre_cdf ρ r a ∂ρ.fst) filter.at_top (nhds (⇑ρ set.univ))
theorem
probability_theory.tendsto_lintegral_pre_cdf_at_bot
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ] :
filter.tendsto (λ (r : ℚ), ∫⁻ (a : α), probability_theory.pre_cdf ρ r a ∂ρ.fst) filter.at_bot (nhds 0)
theorem
probability_theory.tendsto_pre_cdf_at_top_one
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ] :
∀ᵐ (a : α) ∂ρ.fst, filter.tendsto (λ (r : ℚ), probability_theory.pre_cdf ρ r a) filter.at_top (nhds 1)
theorem
probability_theory.tendsto_pre_cdf_at_bot_zero
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ] :
∀ᵐ (a : α) ∂ρ.fst, filter.tendsto (λ (r : ℚ), probability_theory.pre_cdf ρ r a) filter.at_bot (nhds 0)
theorem
probability_theory.inf_gt_pre_cdf
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ] :
structure
probability_theory.has_cond_cdf
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α) :
Prop
- mono : monotone (λ (r : ℚ), probability_theory.pre_cdf ρ r a)
- le_one : ∀ (r : ℚ), probability_theory.pre_cdf ρ r a ≤ 1
- tendsto_at_top_one : filter.tendsto (λ (r : ℚ), probability_theory.pre_cdf ρ r a) filter.at_top (nhds 1)
- tendsto_at_bot_zero : filter.tendsto (λ (r : ℚ), probability_theory.pre_cdf ρ r a) filter.at_bot (nhds 0)
- infi_rat_gt_eq : ∀ (t : ℚ), (⨅ (r : ↥(set.Ioi t)), probability_theory.pre_cdf ρ ↑r a) = probability_theory.pre_cdf ρ t a
A product measure on α × ℝ is said to have a conditional cdf at a : α if pre_cdf is
monotone with limit 0 at -∞ and 1 at +∞, and is right continuous.
This property holds almost everywhere (see has_cond_cdf_ae).
theorem
probability_theory.has_cond_cdf_ae
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ] :
∀ᵐ (a : α) ∂ρ.fst, probability_theory.has_cond_cdf ρ a
def
probability_theory.cond_cdf_set
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ)) :
set α
A measurable set of elements of α such that ρ has a conditional cdf at all
a ∈ cond_cdf_set.
Equations
- probability_theory.cond_cdf_set ρ = (measure_theory.to_measurable ρ.fst {b : α | ¬probability_theory.has_cond_cdf ρ b})ᶜ
theorem
probability_theory.measurable_set_cond_cdf_set
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ)) :
theorem
probability_theory.has_cond_cdf_of_mem_cond_cdf_set
{α : Type u_1}
{mα : measurable_space α}
{ρ : measure_theory.measure (α × ℝ)}
{a : α}
(h : a ∈ probability_theory.cond_cdf_set ρ) :
theorem
probability_theory.mem_cond_cdf_set_ae
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ] :
noncomputable
def
probability_theory.cond_cdf_rat
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ)) :
Conditional cdf of the measure given the value on α, restricted to the rationals.
It is defined to be pre_cdf if a ∈ cond_cdf_set, and a default cdf-like function
otherwise. This is an auxiliary definition used to define cond_cdf.
Equations
- probability_theory.cond_cdf_rat ρ = λ (a : α), ite (a ∈ probability_theory.cond_cdf_set ρ) (λ (r : ℚ), (probability_theory.pre_cdf ρ r a).to_real) (λ (r : ℚ), ite (r < 0) 0 1)
theorem
probability_theory.cond_cdf_rat_of_not_mem
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α)
(h : a ∉ probability_theory.cond_cdf_set ρ)
{r : ℚ} :
probability_theory.cond_cdf_rat ρ a r = ite (r < 0) 0 1
theorem
probability_theory.cond_cdf_rat_of_mem
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α)
(h : a ∈ probability_theory.cond_cdf_set ρ)
(r : ℚ) :
probability_theory.cond_cdf_rat ρ a r = (probability_theory.pre_cdf ρ r a).to_real
theorem
probability_theory.monotone_cond_cdf_rat
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α) :
theorem
probability_theory.measurable_cond_cdf_rat
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(q : ℚ) :
measurable (λ (a : α), probability_theory.cond_cdf_rat ρ a q)
theorem
probability_theory.cond_cdf_rat_nonneg
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α)
(r : ℚ) :
0 ≤ probability_theory.cond_cdf_rat ρ a r
theorem
probability_theory.cond_cdf_rat_le_one
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α)
(r : ℚ) :
probability_theory.cond_cdf_rat ρ a r ≤ 1
theorem
probability_theory.tendsto_cond_cdf_rat_at_bot
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α) :
theorem
probability_theory.tendsto_cond_cdf_rat_at_top
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α) :
theorem
probability_theory.cond_cdf_rat_ae_eq
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ]
(r : ℚ) :
(λ (a : α), probability_theory.cond_cdf_rat ρ a r) =ᵐ[ρ.fst] λ (a : α), (probability_theory.pre_cdf ρ r a).to_real
theorem
probability_theory.of_real_cond_cdf_rat_ae_eq
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ]
(r : ℚ) :
(λ (a : α), ennreal.of_real (probability_theory.cond_cdf_rat ρ a r)) =ᵐ[ρ.fst] probability_theory.pre_cdf ρ r
theorem
probability_theory.inf_gt_cond_cdf_rat
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α)
(t : ℚ) :
(⨅ (r : ↥(set.Ioi t)), probability_theory.cond_cdf_rat ρ a ↑r) = probability_theory.cond_cdf_rat ρ a t
@[irreducible]
noncomputable
def
probability_theory.cond_cdf'
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ)) :
Conditional cdf of the measure given the value on α, as a plain function. This is an auxiliary
definition used to define cond_cdf.
Equations
- probability_theory.cond_cdf' ρ = λ (a : α) (t : ℝ), ⨅ (r : {r' // t < ↑r'}), probability_theory.cond_cdf_rat ρ a ↑r
theorem
probability_theory.cond_cdf'_def
{α : Type u_1}
{mα : measurable_space α}
{ρ : measure_theory.measure (α × ℝ)}
{a : α}
{x : ℝ} :
probability_theory.cond_cdf' ρ a x = ⨅ (r : {r // x < ↑r}), probability_theory.cond_cdf_rat ρ a ↑r
theorem
probability_theory.cond_cdf'_eq_cond_cdf_rat
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α)
(r : ℚ) :
theorem
probability_theory.cond_cdf'_nonneg
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α)
(r : ℝ) :
0 ≤ probability_theory.cond_cdf' ρ a r
theorem
probability_theory.bdd_below_range_cond_cdf_rat_gt
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α)
(x : ℝ) :
theorem
probability_theory.monotone_cond_cdf'
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α) :
theorem
probability_theory.continuous_within_at_cond_cdf'_Ici
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α)
(x : ℝ) :
continuous_within_at (probability_theory.cond_cdf' ρ a) (set.Ici x) x
Conditional cdf #
noncomputable
def
probability_theory.cond_cdf
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α) :
Conditional cdf of the measure given the value on α, as a Stieltjes function.
Equations
- probability_theory.cond_cdf ρ a = {to_fun := probability_theory.cond_cdf' ρ a, mono' := _, right_continuous' := _}
theorem
probability_theory.cond_cdf_eq_cond_cdf_rat
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α)
(r : ℚ) :
⇑(probability_theory.cond_cdf ρ a) ↑r = probability_theory.cond_cdf_rat ρ a r
theorem
probability_theory.cond_cdf_nonneg
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α)
(r : ℝ) :
0 ≤ ⇑(probability_theory.cond_cdf ρ a) r
The conditional cdf is non-negative for all a : α.
theorem
probability_theory.cond_cdf_le_one
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α)
(x : ℝ) :
⇑(probability_theory.cond_cdf ρ a) x ≤ 1
The conditional cdf is lower or equal to 1 for all a : α.
theorem
probability_theory.tendsto_cond_cdf_at_bot
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α) :
The conditional cdf tends to 0 at -∞ for all a : α.
theorem
probability_theory.tendsto_cond_cdf_at_top
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α) :
The conditional cdf tends to 1 at +∞ for all a : α.
theorem
probability_theory.cond_cdf_ae_eq
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ]
(r : ℚ) :
(λ (a : α), ⇑(probability_theory.cond_cdf ρ a) ↑r) =ᵐ[ρ.fst] λ (a : α), (probability_theory.pre_cdf ρ r a).to_real
theorem
probability_theory.of_real_cond_cdf_ae_eq
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ]
(r : ℚ) :
(λ (a : α), ennreal.of_real (⇑(probability_theory.cond_cdf ρ a) ↑r)) =ᵐ[ρ.fst] probability_theory.pre_cdf ρ r
theorem
probability_theory.measurable_cond_cdf
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(x : ℝ) :
measurable (λ (a : α), ⇑(probability_theory.cond_cdf ρ a) x)
The conditional cdf is a measurable function of a : α for all x : ℝ.
theorem
probability_theory.set_lintegral_cond_cdf_rat
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ]
(r : ℚ)
{s : set α}
(hs : measurable_set s) :
Auxiliary lemma for set_lintegral_cond_cdf.
theorem
probability_theory.set_lintegral_cond_cdf
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ]
(x : ℝ)
{s : set α}
(hs : measurable_set s) :
theorem
probability_theory.lintegral_cond_cdf
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ]
(x : ℝ) :
theorem
probability_theory.strongly_measurable_cond_cdf
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(x : ℝ) :
measure_theory.strongly_measurable (λ (a : α), ⇑(probability_theory.cond_cdf ρ a) x)
The conditional cdf is a strongly measurable function of a : α for all x : ℝ.
theorem
probability_theory.integrable_cond_cdf
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ]
(x : ℝ) :
measure_theory.integrable (λ (a : α), ⇑(probability_theory.cond_cdf ρ a) x) ρ.fst
theorem
probability_theory.set_integral_cond_cdf
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ]
(x : ℝ)
{s : set α}
(hs : measurable_set s) :
theorem
probability_theory.integral_cond_cdf
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ]
(x : ℝ) :
theorem
probability_theory.measure_cond_cdf_Iic
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α)
(x : ℝ) :
⇑((probability_theory.cond_cdf ρ a).measure) (set.Iic x) = ennreal.of_real (⇑(probability_theory.cond_cdf ρ a) x)
theorem
probability_theory.measure_cond_cdf_univ
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α) :
⇑((probability_theory.cond_cdf ρ a).measure) set.univ = 1
@[protected, instance]
def
probability_theory.measure.measure_theory.is_probability_measure
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α) :
theorem
probability_theory.measurable_measure_cond_cdf
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ)) :
measurable (λ (a : α), (probability_theory.cond_cdf ρ a).measure)
The function a ↦ (cond_cdf ρ a).measure is measurable.