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

nonempty_rhoMinusSet

PFR.RhoFunctional · PFR/RhoFunctional.lean:56 to 65

Mathematical statement

Exact Lean statement

lemma nonempty_rhoMinusSet [IsZeroOrProbabilityMeasure μ] (hA : A.Nonempty) :
    Set.Nonempty (rhoMinusSet X A μ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma nonempty_rhoMinusSet [IsZeroOrProbabilityMeasure μ] (hA : A.Nonempty) :    Set.Nonempty (rhoMinusSet X A μ) := by  rcases eq_zero_or_isProbabilityMeasure μ with hμ | hμ  · refine ⟨0, ⟨uniformOn (A : Set G), isProbabilityMeasure_uniformOn A.finite_toSet hA,      by simp [hμ], by simp [hμ, KLDiv]⟩⟩  set μ' := uniformOn (univ : Set G) with hμ'  have : IsProbabilityMeasure μ' := isProbabilityMeasure_uniformOn finite_univ univ_nonempty  refine ⟨_, ⟨μ', this, fun y hy ↦ (map_prod_uniformOn_ne_zero hA ?_ hy).elim, rfl⟩⟩  intro x  simp [hμ', uniformOn_apply_singleton_of_mem (mem_univ _) finite_univ]