`ProbabilityTheory.IndepFun.hasCondDistrib_const`🔗

Lemma

No docstring.

Types

α : Type u_1mα : MeasurableSpace αA measurable space is a space equipped with a σ-algebra.
β : Type u_2mβ : MeasurableSpace β
Ω : Type u_4mΩ : MeasurableSpace Ω

Given

μ : MeasureTheory.Measure αA measure is defined to be an outer measure that is countably additive on measurable sets, with the additional assumption that the outer measure is the canonical extension of the restricted measure.MeasureTheory.IsFiniteMeasure μA measure μ is called finite if μ univ < ∞.
X : α → β
Y : α → Ω
Q : MeasureTheory.Measure ΩMeasureTheory.SFinite QA measure is called s-finite if it is a countable sum of finite measures.

Assuming

h : IndepFun X Y μTwo functions are independent if the two measurable space structures they generate are independent.
hX : AEMeasurable X μA function is almost everywhere measurable if it coincides almost everywhere with a measurable function.
hY : HasLaw Y Q μThe predicate HasLaw X μ P registers the fact that the random variable X has law μ under the measure P, in other words that P.map X = μ.

Then

HasCondDistrib Y X (Kernel.const β Q) μ

Predicate stating that the conditional distribution of Y given X under the measure P is equal to the kernel κ.

MeasurableSpace : Type u_6 → Type u_6

A measurable space is a space equipped with a σ-algebra.

MeasureTheory.IsFiniteMeasure : {α : Type u_1} → {m0 : MeasurableSpace α} → MeasureTheory.Measure α → Prop

A measure `μ` is called finite if `μ univ < ∞`.

MeasureTheory.Measure : (α : Type u_5) → [MeasurableSpace α] → Type u_5

A measure is defined to be an outer measure that is countably additive on
measurable sets, with the additional assumption that the outer measure is the canonical
extension of the restricted measure.

The measure of a set `s`, denoted `μ s`, is an extended nonnegative real. The real-valued version
is written `μ.real s`.

MeasureTheory.SFinite : {α : Type u_1} → {m0 : MeasurableSpace α} → MeasureTheory.Measure α → Prop

A measure is called s-finite if it is a countable sum of finite measures.

ProbabilityTheory.IndepFun : {Ω : Type u_1} →
  {β : Type u_6} →
    {γ : Type u_7} →
      {_mΩ : MeasurableSpace Ω} →
        [MeasurableSpace β] →
          [MeasurableSpace γ] →
            (Ω → β) → (Ω → γ) → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IndepFun._auto_1 → Prop

Two functions are independent if the two measurable space structures they generate are
independent. For a function `f` with codomain having measurable space structure `m`, the generated
measurable space structure is `MeasurableSpace.comap f m`.
We use the notation `f ⟂ᵢ[μ] g` for `IndepFun f g μ` (scoped in `ProbabilityTheory`).

AEMeasurable : {α : Type u_1} →
  {β : Type u_2} →
    [MeasurableSpace β] →
      {_m : MeasurableSpace α} → (α → β) → autoParam (MeasureTheory.Measure α) AEMeasurable._auto_1 → Prop

A function is almost everywhere measurable if it coincides almost everywhere with a measurable
function.

A similar notion is `MeasureTheory.NullMeasurable`. That notion is equivalent to `AEMeasurable` if
the σ-algebra on the codomain is countably generated, but weaker in general.

ProbabilityTheory.HasLaw : {Ω : Type u_1} →
  {𝓧 : Type u_2} →
    {mΩ : MeasurableSpace Ω} →
      {m𝓧 : MeasurableSpace 𝓧} →
        (Ω → 𝓧) → MeasureTheory.Measure 𝓧 → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.HasLaw._auto_1 → Prop

The predicate `HasLaw X μ P` registers the fact that the random variable `X` has law `μ` under
the measure `P`, in other words that `P.map X = μ`. We also require `X` to be `AEMeasurable`,
to allow for nice interactions with operations on the codomain of `X`. See for instance
`HasLaw.comp`, `IndepFun.hasLaw_mul` and `IndepFun.hasLaw_add`.

ProbabilityTheory.HasCondDistrib : {Ω : Type u_1} →
  {𝓧 : Type u_2} →
    {𝓨 : Type u_3} →
      {mΩ : MeasurableSpace Ω} →
        {m𝓧 : MeasurableSpace 𝓧} →
          {m𝓨 : MeasurableSpace 𝓨} → (Ω → 𝓨) → (Ω → 𝓧) → ProbabilityTheory.Kernel 𝓧 𝓨 → MeasureTheory.Measure Ω → Prop

Predicate stating that the conditional distribution of `Y` given `X` under the measure `P`
is equal to the kernel `κ`.

ProbabilityTheory.Kernel.const : (α : Type u_4) →
  {β : Type u_5} →
    [inst : MeasurableSpace α] → {x : MeasurableSpace β} → MeasureTheory.Measure β → ProbabilityTheory.Kernel α β

Constant kernel, which always returns the same measure.

Code

lemma IndepFun.hasCondDistrib_const [IsFiniteMeasure μ] {Q : Measure Ω} [SFinite Q]
    (h : IndepFun X Y μ) (hX : AEMeasurable X μ) (hY : HasLaw Y Q μ) :
    HasCondDistrib Y X (Kernel.const β Q) μ where
  aemeasurable

Proof

hX.prodMk hY.aemeasurable
  map_eq := by
    rw [(indepFun_iff_map_prod_eq_prod_map_map hX hY.aemeasurable).1 h, hY.map_eq,
      Measure.compProd_const]

Meaning last changed in v4.34.0-rc2-76-g565f652 (2026-09-10).

Self-contained, with its dependencies inlined and proofs replaced by sorry: download the raw file · open it in the Lean web editor.

Dependency graph

Nothing to draw. Its statement rests on no other declaration in this project, and names nothing from a package left unaudited — so the graph is this declaration alone. That is the answer, not a missing picture.

Audit surface: 0 project declarations, 9 external constants

✓ Proved: no sorry anywhere in its closure

This is the tool's own reading of one build's recorded axioms, and it is not robust against an author who wants it to pass. Checking meant to be relied on should go through Comparator, which replays the proof through the kernel from an export against an explicit list of permitted axioms.

ProbabilityTheory.IndepFun.hasCondDistrib_const🔗

`ProbabilityTheory.IndepFun.hasCondDistrib_const`🔗