Lifting a countable-factor joint law to the carriers

Step 3 of the step-approximation programme: a joint law on a countable pair of factor spaces, whose marginals are the pushed-forward carrier marginals, lifts to a carrier-level joint law with the original carrier marginals and exact pushforward back to the factor law. Built from normalized restrictions to factor cells. Zero-mass cells contribute zero: the factor law's atom over a null cell vanishes by marginal compatibility (proved first, so no 0⁻¹ arithmetic is ever relied on), and the restriction to a null cell is the zero measure.

The countability and measurable-singleton hypotheses are stated explicitly on each factor — nothing relies on a hidden discrete measurable-space instance.

Deliberately not claimed: preservation of either original pair coupling — that would reintroduce arbitrary-carrier disintegration.

noncomputable def MeasureTheory.countableFactorLift {γ₁ : Type u_1} {γ₂ : Type u_2} {ι₁ : Type u_3} {ι₂ : Type u_4} [MeasurableSpace γ₁] [MeasurableSpace γ₂] [MeasurableSpace ι₁] [MeasurableSpace ι₂] (μ₁ : Measure γ₁) (μ₂ : Measure γ₂) (q₁ : γ₁ → ι₁) (q₂ : γ₂ → ι₂) (lam : Measure (ι₁ × ι₂)) : Measure (γ₁ × γ₂)

The countable-factor lift: the factor law's atoms spread over the normalized products of the corresponding restricted carrier measures.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.map_restrict_preimage_singleton {γ₁ : Type u_1} {ι₁ : Type u_3} [MeasurableSpace γ₁] [MeasurableSpace ι₁] {μ₁ : Measure γ₁} {q₁ : γ₁ → ι₁} (hq : Measurable q₁) (i : ι₁) : Measure.map q₁ (μ₁.restrict (q₁ ⁻¹' {i})) = μ₁ (q₁ ⁻¹' {i}) • Measure.dirac i

Mapping a fiber restriction through its factor map gives a scaled Dirac mass.

theorem MeasureTheory.atom_eq_zero_of_fiber_null_fst {γ₁ : Type u_1} {ι₁ : Type u_3} {ι₂ : Type u_4} [MeasurableSpace γ₁] [MeasurableSpace ι₁] [MeasurableSpace ι₂] [MeasurableSingletonClass ι₁] {μ₁ : Measure γ₁} {q₁ : γ₁ → ι₁} {lam : Measure (ι₁ × ι₂)} (hq₁ : Measurable q₁) (hfst : Measure.map Prod.fst lam = Measure.map q₁ μ₁) {i : ι₁} (h0 : μ₁ (q₁ ⁻¹' {i}) = 0) (j : ι₂) : lam {(i, j)} = 0

The zero-cell guard: marginal compatibility forces the factor law's atom over a null first-coordinate cell to vanish. Proved before any normalization is touched, so the zero-cell summand is eliminated outright rather than by 0⁻¹ arithmetic.

theorem MeasureTheory.atom_eq_zero_of_fiber_null_snd {γ₂ : Type u_2} {ι₁ : Type u_3} {ι₂ : Type u_4} [MeasurableSpace γ₂] [MeasurableSpace ι₁] [MeasurableSpace ι₂] [MeasurableSingletonClass ι₂] {μ₂ : Measure γ₂} {q₂ : γ₂ → ι₂} {lam : Measure (ι₁ × ι₂)} (hq₂ : Measurable q₂) (hsnd : Measure.map Prod.snd lam = Measure.map q₂ μ₂) {j : ι₂} (h0 : μ₂ (q₂ ⁻¹' {j}) = 0) (i : ι₁) : lam {(i, j)} = 0

The symmetric zero-cell guard for the second coordinate.

The carrier marginals — proved first, validating the normalization

theorem MeasureTheory.countableFactorLift_map_fst {γ₁ : Type u_1} {γ₂ : Type u_2} {ι₁ : Type u_3} {ι₂ : Type u_4} [MeasurableSpace γ₁] [MeasurableSpace γ₂] [MeasurableSpace ι₁] [MeasurableSpace ι₂] [Countable ι₁] [MeasurableSingletonClass ι₁] [Countable ι₂] [MeasurableSingletonClass ι₂] {μ₁ : Measure γ₁} {μ₂ : Measure γ₂} {q₁ : γ₁ → ι₁} {q₂ : γ₂ → ι₂} {lam : Measure (ι₁ × ι₂)} [IsFiniteMeasure μ₁] [IsFiniteMeasure μ₂] (hq₁ : Measurable q₁) (hq₂ : Measurable q₂) (hfst : Measure.map Prod.fst lam = Measure.map q₁ μ₁) (hsnd : Measure.map Prod.snd lam = Measure.map q₂ μ₂) : Measure.map Prod.fst (countableFactorLift μ₁ μ₂ q₁ q₂ lam) = μ₁

The first carrier marginal is exact. Per summand the second coordinate integrates out, its normalization cancels (the zero-mass case is eliminated by the guard, not by arithmetic), the factor law's fiber mass recovers each cell restriction by marginal compatibility, and the cell restrictions sum to the carrier measure.

theorem MeasureTheory.countableFactorLift_map_snd {γ₁ : Type u_1} {γ₂ : Type u_2} {ι₁ : Type u_3} {ι₂ : Type u_4} [MeasurableSpace γ₁] [MeasurableSpace γ₂] [MeasurableSpace ι₁] [MeasurableSpace ι₂] [Countable ι₁] [MeasurableSingletonClass ι₁] [Countable ι₂] [MeasurableSingletonClass ι₂] {μ₁ : Measure γ₁} {μ₂ : Measure γ₂} {q₁ : γ₁ → ι₁} {q₂ : γ₂ → ι₂} {lam : Measure (ι₁ × ι₂)} [IsFiniteMeasure μ₁] [IsFiniteMeasure μ₂] (hq₁ : Measurable q₁) (hq₂ : Measurable q₂) (hfst : Measure.map Prod.fst lam = Measure.map q₁ μ₁) (hsnd : Measure.map Prod.snd lam = Measure.map q₂ μ₂) : Measure.map Prod.snd (countableFactorLift μ₁ μ₂ q₁ q₂ lam) = μ₂

The second carrier marginal is exact. Mirror of the first.

theorem MeasureTheory.isProbabilityMeasure_countableFactorLift {γ₁ : Type u_1} {γ₂ : Type u_2} {ι₁ : Type u_3} {ι₂ : Type u_4} [MeasurableSpace γ₁] [MeasurableSpace γ₂] [MeasurableSpace ι₁] [MeasurableSpace ι₂] [Countable ι₁] [MeasurableSingletonClass ι₁] [Countable ι₂] [MeasurableSingletonClass ι₂] {μ₁ : Measure γ₁} {μ₂ : Measure γ₂} {q₁ : γ₁ → ι₁} {q₂ : γ₂ → ι₂} {lam : Measure (ι₁ × ι₂)} [IsFiniteMeasure μ₁] [IsFiniteMeasure μ₂] [IsProbabilityMeasure μ₁] (hq₁ : Measurable q₁) (hq₂ : Measurable q₂) (hfst : Measure.map Prod.fst lam = Measure.map q₁ μ₁) (hsnd : Measure.map Prod.snd lam = Measure.map q₂ μ₂) : IsProbabilityMeasure (countableFactorLift μ₁ μ₂ q₁ q₂ lam)

The lift is a probability measure — derived from the exact first carrier marginal evaluated at univ, independently of the factor-law round-trip.

theorem MeasureTheory.countableFactorLift_map_prodMap {γ₁ : Type u_1} {γ₂ : Type u_2} {ι₁ : Type u_3} {ι₂ : Type u_4} [MeasurableSpace γ₁] [MeasurableSpace γ₂] [MeasurableSpace ι₁] [MeasurableSpace ι₂] [Countable ι₁] [MeasurableSingletonClass ι₁] [Countable ι₂] [MeasurableSingletonClass ι₂] {μ₁ : Measure γ₁} {μ₂ : Measure γ₂} {q₁ : γ₁ → ι₁} {q₂ : γ₂ → ι₂} {lam : Measure (ι₁ × ι₂)} [IsFiniteMeasure μ₁] [IsFiniteMeasure μ₂] (hq₁ : Measurable q₁) (hq₂ : Measurable q₂) (hfst : Measure.map Prod.fst lam = Measure.map q₁ μ₁) (hsnd : Measure.map Prod.snd lam = Measure.map q₂ μ₂) : Measure.map (Prod.map q₁ q₂) (countableFactorLift μ₁ μ₂ q₁ q₂ lam) = lam

The factor-law round-trip is exact: pushing the lift back through the factor maps recovers the input joint law on the nose. This is the acceptance test for the lift, proved atomwise on the countable factor product — never inferred from the marginals. Off-diagonal summands vanish because distinct fibers are disjoint; on the diagonal a null fiber forces the corresponding atom of lam to vanish (the guards), so normalization only ever cancels against a positive cell.