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

condRhoPlus_le

PFR.RhoFunctional · PFR/RhoFunctional.lean:960 to 975

Source documentation

$\rho^+(X|Z) \leq \rho^+(X)$

Exact Lean statement

lemma condRhoPlus_le [IsProbabilityMeasure μ] {S : Type*} [MeasurableSpace S]
    [Finite S] [MeasurableSingletonClass S]
    {Z : Ω → S} (hX : Measurable X) (hZ : Measurable Z) (hA : A.Nonempty) :
    ρ⁺[X | Z ; μ # A] ≤ ρ⁺[X ; μ # A]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma condRhoPlus_le [IsProbabilityMeasure μ] {S : Type*} [MeasurableSpace S]    [Finite S] [MeasurableSingletonClass S]    {Z : Ω → S} (hX : Measurable X) (hZ : Measurable Z) (hA : A.Nonempty) :    ρ⁺[X | Z ; μ # A] ≤ ρ⁺[X ; μ # A] := by  cases nonempty_fintype S  have : IsProbabilityMeasure (Measure.map Z μ) := isProbabilityMeasure_map hZ.aemeasurable  have I₁ := condRhoMinus_le hX hZ hA (μ := μ)  simp_rw [condRhoPlus, rhoPlus, tsum_fintype]  simp only [Nat.card_eq_fintype_card, Fintype.card_coe, mul_sub, mul_add, Finset.sum_sub_distrib,    Finset.sum_add_distrib, tsub_le_iff_right]  rw [← Finset.sum_mul, ← tsum_fintype (L := SummationFilter.unconditional _),    ← condRhoMinus, ← condEntropy_eq_sum_fintype _ _ _ hZ]  simp_rw [← map_measureReal_apply hZ (measurableSet_singleton _)]  simp only [sum_measureReal_singleton, Finset.coe_univ, probReal_univ, one_mul,    sub_add_cancel, ge_iff_le]  linarith