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

rho_of_uniform

PFR.RhoFunctional · PFR/RhoFunctional.lean:665 to 675

Source documentation

We have $\rho(U_A) = 0$ .

Exact Lean statement

lemma rho_of_uniform [IsProbabilityMeasure μ]
    {U : Ω → G} {A : Finset G} (hunif : IsUniform A U μ) (hU : Measurable U)
    (hA : A.Nonempty) : ρ[U ; μ # A] = 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma rho_of_uniform [IsProbabilityMeasure μ]    {U : Ω → G} {A : Finset G} (hunif : IsUniform A U μ) (hU : Measurable U)    (hA : A.Nonempty) : ρ[U ; μ # A] = 0 := by  have : H[U ; μ] = log (Nat.card A) := hunif.entropy_eq' (toFinite _) hU  simp only [rho, rhoPlus, this, Nat.card_eq_fintype_card, Fintype.card_coe, add_sub_cancel_right,    add_self_div_two]  apply le_antisymm _ (rhoMinus_nonneg hU)  have Z := rhoMinus_le hU hA (T := fun _ ↦ 0) hunif measurable_const hU    (indepFun_const 0).symm (μ := μ)  have : (fun x ↦ 0) + U = U := by ext y; simp  simpa [this] using Z