OAI/NumberTheory/DukePrimeDegree/Entropy/NestedRealConditionals.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compatibility of nested real conditional measures

Conditioning first on a transverse coordinate and then on all but one leaf coordinate gives the same real conditional as conditioning on both coordinates at once. This is the finite-chart form of Einsiedler--Katok (2003), Lemma 8.1.

  1. theorem OAI.DukePrimeDegree.ae_nested_real_conditionals line 23
  2. theorem OAI.DukePrimeDegree.ae_nested_eq_prod_of_projective_conditionals line 48

    Source documentation

    Constant projective real conditionals in a full chart force each larger conditional leaf measure to split as a product.

    theorem ae_nested_eq_prod_of_projective_conditionals
    (μ : Measure (T × (B × ℝ))) [IsFiniteMeasure μ]
    (ν : T → Measure ℝ) (hνfinite : ∀ a, IsFiniteMeasure (ν a))
    (hν : ∀ a, ν a Set.univ ≠ 0)
    (h : ∀ᵐ a ∂μ.fst, ∀ᵐ b ∂(μ.condKernel a).fst, ∃ c : ℝ≥0∞,
      (μ.map MeasurableEquiv.prodAssoc.symm).condKernel (a, b) = c • ν a) :
    ∀ᵐ a ∂μ.fst,
      μ.condKernel a = (μ.condKernel a).fst.prod
        (PrimeDegreePackets.anchorNormalize (ν a) Set.univ) := by
…

    Mentions: OAI.PrimeDegreePackets.anchorNormalize