Source indexedlemma · leanprover/lean4:v4.33.0-rc1

condRuzsaDist_nonneg

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:573 to 584

Mathematical statement

Exact Lean statement

lemma condRuzsaDist_nonneg [Countable T] {X : Ω → G} (hX : Measurable X) [FiniteRange X]
    {Z : Ω → S} (hZ : Measurable Z) [FiniteRange Z]
    {Y : Ω' → G} (hY : Measurable Y) [FiniteRange Y]
    {W : Ω' → T} (hW : Measurable W) [FiniteRange W]
    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] :
    0 ≤ d[X | Z ; μ # Y | W ; μ']

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma condRuzsaDist_nonneg [Countable T] {X : Ω → G} (hX : Measurable X) [FiniteRange X]    {Z : Ω → S} (hZ : Measurable Z) [FiniteRange Z]    {Y : Ω' → G} (hY : Measurable Y) [FiniteRange Y]    {W : Ω' → T} (hW : Measurable W) [FiniteRange W]    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] :    0 ≤ d[X | Z ; μ # Y | W ; μ'] := by  rw [condRuzsaDist_def]  have : IsProbabilityMeasure (μ.map Z) := isProbabilityMeasure_map hZ.aemeasurable  have : IsProbabilityMeasure (μ'.map W) := isProbabilityMeasure_map hW.aemeasurable  refine Kernel.rdist_nonneg ?_ ?_  · exact Kernel.aefiniteKernelSupport_condDistrib _ _ _ hX hZ  · exact Kernel.aefiniteKernelSupport_condDistrib _ _ _ hY hW