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

rhoMinusSet_eq_of_identDistrib

PFR.RhoFunctional · PFR/RhoFunctional.lean:76 to 83

Mathematical statement

Exact Lean statement

lemma rhoMinusSet_eq_of_identDistrib {Ω' : Type*} [MeasurableSpace Ω'] {μ' : Measure Ω'}
    {X' : Ω' → G}
    (h : IdentDistrib X X' μ μ') : rhoMinusSet X A μ = rhoMinusSet X' A μ'

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma rhoMinusSet_eq_of_identDistrib {Ω' : Type*} [MeasurableSpace Ω'] {μ' : Measure Ω'}    {X' : Ω' → G}    (h : IdentDistrib X X' μ μ') : rhoMinusSet X A μ = rhoMinusSet X' A μ' := by  have I (μ'' : Measure G) : KL[X ; μ # Prod.fst + Prod.snd ; μ''.prod (uniformOn (A : Set G))] =      KL[X' ; μ' # Prod.fst + Prod.snd ; μ''.prod (uniformOn (A : Set G))] := by    apply ProbabilityTheory.IdentDistrib.KLDiv_eq _ _ h    exact .refl (by fun_prop)  simp only [rhoMinusSet, h.map_eq, I]