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

condRho_prod_le

PFR.RhoFunctional · PFR/RhoFunctional.lean:1020 to 1038

Source documentation

$\rho(X|Z) \leq \rho(X) + \frac{1}{2}( \bbH[X] - \bbH[X|Z])$ , conditional version

Exact Lean statement

lemma condRho_prod_le [IsProbabilityMeasure μ] {S : Type*} [MeasurableSpace S]
    [Finite S] [MeasurableSingletonClass S]
    {Z T : Ω → S} (hX : Measurable X) (hZ : Measurable Z) (hT : Measurable T) (hA : A.Nonempty) :
    ρ[X | ⟨Z, T⟩ ; μ # A] ≤ ρ[X | T ; μ # A] + (H[X | T ; μ] - H[X | ⟨Z, T⟩ ; μ]) / 2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma condRho_prod_le [IsProbabilityMeasure μ] {S : Type*} [MeasurableSpace S]    [Finite S] [MeasurableSingletonClass S]    {Z T : Ω → S} (hX : Measurable X) (hZ : Measurable Z) (hT : Measurable T) (hA : A.Nonempty) :    ρ[X | ⟨Z, T⟩ ; μ # A] ≤ ρ[X | T ; μ # A] + (H[X | T ; μ] - H[X | ⟨Z, T⟩ ; μ]) / 2 := by  cases nonempty_fintype S  rw [condRho_prod_eq_sum hZ hT]  have : ∑ g : S, μ.real (T ⁻¹' {g}) * ρ[ X | Z ; μ[|T ⁻¹' {g}] # A] ≤    ∑ g : S, μ.real (T ⁻¹' {g}) *      (ρ[X ; μ[|T ⁻¹' {g}] # A] + (H[X ; μ[|T ⁻¹' {g}]] - H[X | Z ; μ[|T ⁻¹' {g}]]) / 2) := by    apply Finset.sum_le_sum (fun g hg ↦ ?_)    rcases eq_or_ne (μ.real (T ⁻¹' {g})) 0 with hpg | hpg    · simp [hpg]    gcongr    have hμ : IsProbabilityMeasure (μ[|T ⁻¹' {g}]) := cond_isProbabilityMeasure_of_real hpg    exact condRho_le hX hZ hA  apply this.trans_eq  simp_rw [mul_add, mul_div, mul_sub, Finset.sum_add_distrib, ← Finset.sum_div,    Finset.sum_sub_distrib, condRho, tsum_fintype, condEntropy_eq_sum_fintype X T μ hT,    condEntropy_prod_eq_sum μ hZ hT]