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

ProbabilityTheory.Kernel.rdist_symm

PFR.ForMathlib.Entropy.Kernel.RuzsaDist · PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean:76 to 84

Mathematical statement

Exact Lean statement

lemma rdist_symm {κ : Kernel T G} {η : Kernel T' G} [IsFiniteKernel κ] [IsFiniteKernel η]
    {μ : Measure T} {ν : Measure T'} [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    [FiniteSupport μ] [FiniteSupport ν] :
    dk[κ ; μ # η ; ν] = dk[η ; ν # κ ; μ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma rdist_symm {κ : Kernel T G} {η : Kernel T' G} [IsFiniteKernel κ] [IsFiniteKernel η]    {μ : Measure T} {ν : Measure T'} [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]    [FiniteSupport μ] [FiniteSupport ν] :    dk[κ ; μ # η ; ν] = dk[η ; ν # κ ; μ] := by  rw [rdist_eq', rdist_eq', sub_sub, sub_sub, add_comm]  congr 1  rw [← entropy_comap_swap, comap_map_comm _ _ (by fun_prop), entropy_sub_comm, Measure.comap_swap,    Measure.prod_swap, comap_prod_swap, map_map _ (by fun_prop) (by fun_prop)]  congr