ConditionalProduct.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Product structure from equal normalized real conditionals

This is the finite-rectangle step of Einsiedler--Katok (2003), Lemma 8.2. A common conditional measure, even if initially specified only up to a scalar on each fiber, forces a genuine product measure after normalization.

theorem OAI.DukePrimeDegree.eq_prod_of_constant_real_conditionals line 21

Source documentation

Equal normalized conditionals on the real factor force a product.

theorem eq_prod_of_constant_real_conditionals {B : Type*} [MeasurableSpace B]
    (μ : Measure (B × ℝ)) [IsFiniteMeasure μ]
    (ν : Measure ℝ) [IsFiniteMeasure ν]
    (h : ∀ᵐ x ∂μ.fst, μ.condKernel x = ν) :
    μ = μ.fst.prod ν := by
…

theorem OAI.DukePrimeDegree.eq_prod_of_projective_real_conditionals line 34

Source documentation

Projectively equal conditional measures become exactly equal after normalizing their common model. The only scalar left is the marginal.

theorem eq_prod_of_projective_real_conditionals {B : Type*} [MeasurableSpace B]
    (μ : Measure (B × ℝ)) [IsFiniteMeasure μ]
    (ν : Measure ℝ) [IsFiniteMeasure ν] (hν : ν univ ≠ 0)
    (h : ∀ᵐ x ∂μ.fst, ∃ c : ℝ≥0∞, μ.condKernel x = c • ν) :
    μ = μ.fst.prod (anchorNormalize ν univ) := by
…