@[simp]

theorem ProbabilityTheory.entropy_mul_const {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} (hX : Measurable X) (c : G) : H[X * fun (x : Ω) => c ; μ] = H[X ; μ]

@[simp]

theorem ProbabilityTheory.entropy_add_const {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} (hX : Measurable X) (c : G) : H[X + fun (x : Ω) => c ; μ] = H[X ; μ]

theorem ProbabilityTheory.entropy_mul_right {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : H[⟨X, X * Y⟩ ; μ] = H[⟨X, Y⟩ ; μ]

H[X, X * Y] = H[X, Y].

theorem ProbabilityTheory.entropy_add_right {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : H[⟨X, X + Y⟩ ; μ] = H[⟨X, Y⟩ ; μ]

H[X, X + Y] = H[X, Y]

theorem ProbabilityTheory.entropy_mul_right' {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : H[⟨X, Y * X⟩ ; μ] = H[⟨X, Y⟩ ; μ]

H[X, Y * X] = H[X, Y]

theorem ProbabilityTheory.entropy_add_right' {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : H[⟨X, Y + X⟩ ; μ] = H[⟨X, Y⟩ ; μ]

H[X, Y + X] = H[X, Y]

theorem ProbabilityTheory.entropy_mul_left {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : H[⟨Y * X, Y⟩ ; μ] = H[⟨X, Y⟩ ; μ]

H[Y * X, Y] = H[X, Y]

theorem ProbabilityTheory.entropy_add_left {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : H[⟨Y + X, Y⟩ ; μ] = H[⟨X, Y⟩ ; μ]

H[Y + X, Y] = H[X, Y]

theorem ProbabilityTheory.entropy_mul_left' {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : H[⟨X * Y, Y⟩ ; μ] = H[⟨X, Y⟩ ; μ]

H[X * Y, Y] = H[X, Y]

theorem ProbabilityTheory.entropy_add_left' {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : H[⟨X + Y, Y⟩ ; μ] = H[⟨X, Y⟩ ; μ]

H[X + Y, Y] = H[X, Y]

theorem ProbabilityTheory.entropy_inv_right {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : H[⟨X, Y⁻¹⟩ ; μ] = H[⟨X, Y⟩ ; μ]

H[X, Y⁻¹] = H[X, Y]

theorem ProbabilityTheory.entropy_neg_right {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : H[⟨X, -Y⟩ ; μ] = H[⟨X, Y⟩ ; μ]

H[X, -Y] = H[X, Y]

theorem ProbabilityTheory.entropy_inv_left {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : H[⟨X⁻¹, Y⟩ ; μ] = H[⟨X, Y⟩ ; μ]

H[X⁻¹, Y] = H[X, Y]

theorem ProbabilityTheory.entropy_neg_left {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : H[⟨-X, Y⟩ ; μ] = H[⟨X, Y⟩ ; μ]

H[-X, Y] = H[X, Y]

theorem ProbabilityTheory.entropy_div_right {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : H[⟨X, X / Y⟩ ; μ] = H[⟨X, Y⟩ ; μ]

H[X, X / Y] = H[X, Y]

theorem ProbabilityTheory.entropy_sub_right {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : H[⟨X, X - Y⟩ ; μ] = H[⟨X, Y⟩ ; μ]

H[X, X - Y] = H[X, Y]

theorem ProbabilityTheory.entropy_div_right' {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : H[⟨X, Y / X⟩ ; μ] = H[⟨X, Y⟩ ; μ]

H[X, Y / X] = H[X, Y]

theorem ProbabilityTheory.entropy_sub_right' {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : H[⟨X, Y - X⟩ ; μ] = H[⟨X, Y⟩ ; μ]

H[X, Y - X] = H[X, Y]

theorem ProbabilityTheory.entropy_div_left {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : H[⟨Y / X, Y⟩ ; μ] = H[⟨X, Y⟩ ; μ]

H[Y / X, Y] = H[X, Y]

theorem ProbabilityTheory.entropy_sub_left {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : H[⟨Y - X, Y⟩ ; μ] = H[⟨X, Y⟩ ; μ]

H[Y - X, Y] = H[X, Y]

theorem ProbabilityTheory.entropy_div_left' {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : H[⟨X / Y, Y⟩ ; μ] = H[⟨X, Y⟩ ; μ]

H[X / Y, Y] = H[X, Y]

theorem ProbabilityTheory.entropy_sub_left' {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : H[⟨X - Y, Y⟩ ; μ] = H[⟨X, Y⟩ ; μ]

H[X - Y, Y] = H[X, Y]

theorem ProbabilityTheory.entropy_inv {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} (hX : Measurable X) : H[X⁻¹ ; μ] = H[X ; μ]

If X is G-valued, then H[X⁻¹]=H[X].

theorem ProbabilityTheory.entropy_neg {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} (hX : Measurable X) : H[-X ; μ] = H[X ; μ]

If X is G-valued, then H[-X]=H[X].

theorem ProbabilityTheory.entropy_div_comm {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} {Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) : H[X / Y ; μ] = H[Y / X ; μ]

H[X / Y] = H[Y / X]

theorem ProbabilityTheory.entropy_sub_comm {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} {Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) : H[X - Y ; μ] = H[Y - X ; μ]

H[X - Y] = H[Y - X]

theorem ProbabilityTheory.max_condEntropy_sub_condMutualInfo_le_condEntropy_div {Ω : Type uΩ} {G : Type uS} {T : Type uT} [mΩ : MeasurableSpace Ω] [Countable G] [Countable T] [hG : MeasurableSpace G] [MeasurableSpace T] [MeasurableSingletonClass G] [MeasurableSingletonClass T] [Group G] {X Y : Ω → G} {μ : MeasureTheory.Measure Ω} [FiniteRange X] [FiniteRange Y] {Z : Ω → T} (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) [MeasureTheory.IsProbabilityMeasure μ] [FiniteRange Z] : max H[X | Z ; μ] H[Y | Z ; μ] - I[X : Y|Z;μ] ≤ H[X / Y | Z ; μ]

max(H[X | Z], H[Y | Z]) - I[X : Y | Z] ≤ H[X / Y | Z]

theorem ProbabilityTheory.max_condEntropy_sub_condMutualInfo_le_condEntropy_sub {Ω : Type uΩ} {G : Type uS} {T : Type uT} [mΩ : MeasurableSpace Ω] [Countable G] [Countable T] [hG : MeasurableSpace G] [MeasurableSpace T] [MeasurableSingletonClass G] [MeasurableSingletonClass T] [AddGroup G] {X Y : Ω → G} {μ : MeasureTheory.Measure Ω} [FiniteRange X] [FiniteRange Y] {Z : Ω → T} (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) [MeasureTheory.IsProbabilityMeasure μ] [FiniteRange Z] : max H[X | Z ; μ] H[Y | Z ; μ] - I[X : Y|Z;μ] ≤ H[X - Y | Z ; μ]

max(H[X | Z], H[Y | Z]) - I[X : Y | Z] ≤ H[X - Y | Z]

theorem ProbabilityTheory.condEntropy_mul_left {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X Y : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) : H[Y * X | Y ; μ] = H[X | Y ; μ]

H[Y * X | Y] = H[X | Y]

theorem ProbabilityTheory.condEntropy_add_left {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X Y : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) : H[Y + X | Y ; μ] = H[X | Y ; μ]

H[Y + X | Y] = H[X | Y]

theorem ProbabilityTheory.condEntropy_mul_right {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X Y : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) : H[X * Y | Y ; μ] = H[X | Y ; μ]

H[X * Y | Y] = H[X | Y]

theorem ProbabilityTheory.condEntropy_add_right {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X Y : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) : H[X + Y | Y ; μ] = H[X | Y ; μ]

H[X + Y | Y] = H[X | Y]

theorem ProbabilityTheory.condEntropy_div_left {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X Y : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) : H[Y / X | Y ; μ] = H[X | Y ; μ]

H[Y / X | Y] = H[X | Y]

theorem ProbabilityTheory.condEntropy_sub_left {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X Y : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) : H[Y - X | Y ; μ] = H[X | Y ; μ]

H[Y - X | Y] = H[X | Y]

theorem ProbabilityTheory.condEntropy_div_right {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X Y : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) : H[X / Y | Y ; μ] = H[X | Y ; μ]

H[X / Y | Y] = H[X | Y]

theorem ProbabilityTheory.condEntropy_sub_right {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X Y : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) : H[X - Y | Y ; μ] = H[X | Y ; μ]

H[X - Y | Y] = H[X | Y]

theorem ProbabilityTheory.mutualInfo_mul_right {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X Y : Ω → G} [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (h : IndepFun X Y μ) : I[X : X * Y ; μ] = H[X * Y ; μ] - H[Y ; μ]

I[X : X * Y] = H[X * Y] - H[Y] iff X, Y are independent.

theorem ProbabilityTheory.mutualInfo_add_right {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X Y : Ω → G} [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (h : IndepFun X Y μ) : I[X : X + Y ; μ] = H[X + Y ; μ] - H[Y ; μ]

I[X : X + Y] = H[X + Y] - H[Y] iff X, Y are independent.

theorem ProbabilityTheory.entropy_sub_mutualInfo_le_entropy_mul {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → G} [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) : H[X ; μ] - I[X : Y ; μ] ≤ H[X * Y ; μ]

H[X] - I[X : Y] ≤ H[X * Y]

theorem ProbabilityTheory.entropy_sub_mutualInfo_le_entropy_add {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → G} [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) : H[X ; μ] - I[X : Y ; μ] ≤ H[X + Y ; μ]

H[X] - I[X : Y] ≤ H[X + Y]

theorem ProbabilityTheory.entropy_sub_mutualInfo_le_entropy_mul' {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → G} [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) : H[Y ; μ] - I[X : Y ; μ] ≤ H[X * Y ; μ]

H[Y] - I[X : Y] ≤ H[X * Y]

theorem ProbabilityTheory.entropy_sub_mutualInfo_le_entropy_add' {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → G} [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) : H[Y ; μ] - I[X : Y ; μ] ≤ H[X + Y ; μ]

H[Y] - I[X : Y] ≤ H[X + Y]

theorem ProbabilityTheory.entropy_sub_mutualInfo_le_entropy_div {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → G} [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) : H[X ; μ] - I[X : Y ; μ] ≤ H[X / Y ; μ]

H[X] - I[X : Y] ≤ H[X / Y]

theorem ProbabilityTheory.entropy_sub_mutualInfo_le_entropy_sub {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → G} [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) : H[X ; μ] - I[X : Y ; μ] ≤ H[X - Y ; μ]

H[X] - I[X : Y] ≤ H[X - Y]

theorem ProbabilityTheory.entropy_sub_mutualInfo_le_entropy_div' {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → G} [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) : H[Y ; μ] - I[X : Y ; μ] ≤ H[X / Y ; μ]

H[Y] - I[X : Y] ≤ H[X / Y]

theorem ProbabilityTheory.entropy_sub_mutualInfo_le_entropy_sub' {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → G} [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) : H[Y ; μ] - I[X : Y ; μ] ≤ H[X - Y ; μ]

H[Y] - I[X : Y] ≤ H[X - Y]

theorem ProbabilityTheory.max_entropy_sub_mutualInfo_le_entropy_mul {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → G} [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) : max H[X ; μ] H[Y ; μ] - I[X : Y ; μ] ≤ H[X * Y ; μ]

max(H[X], H[Y]) - I[X : Y] ≤ H[X * Y]

theorem ProbabilityTheory.max_entropy_sub_mutualInfo_le_entropy_add {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → G} [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) : max H[X ; μ] H[Y ; μ] - I[X : Y ; μ] ≤ H[X + Y ; μ]

max(H[X], H[Y]) - I[X : Y] ≤ H[X + Y]

theorem ProbabilityTheory.max_entropy_sub_mutualInfo_le_entropy_div {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → G} [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) : max H[X ; μ] H[Y ; μ] - I[X : Y ; μ] ≤ H[X / Y ; μ]

max(H[X], H[Y]) - I[X : Y] ≤ H[X / Y]

theorem ProbabilityTheory.max_entropy_sub_mutualInfo_le_entropy_sub {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → G} [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) : max H[X ; μ] H[Y ; μ] - I[X : Y ; μ] ≤ H[X - Y ; μ]

max(H[X], H[Y]) - I[X : Y] ≤ H[X - Y]

theorem ProbabilityTheory.max_condEntropy_sub_condMutualInfo_le_condEntropy_mul {Ω : Type uΩ} {G : Type uS} {T : Type uT} [mΩ : MeasurableSpace Ω] [Countable G] [Countable T] [hG : MeasurableSpace G] [MeasurableSpace T] [MeasurableSingletonClass G] [MeasurableSingletonClass T] [Group G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → G} [FiniteRange X] [FiniteRange Y] {Z : Ω → T} [FiniteRange Z] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) : max H[X | Z ; μ] H[Y | Z ; μ] - I[X : Y|Z;μ] ≤ H[X * Y | Z ; μ]

max(H[X | Z], H[Y | Z]) - I[X : Y | Z] ≤ H[X * Y | Z]

theorem ProbabilityTheory.max_condEntropy_sub_condMutualInfo_le_condEntropy_add {Ω : Type uΩ} {G : Type uS} {T : Type uT} [mΩ : MeasurableSpace Ω] [Countable G] [Countable T] [hG : MeasurableSpace G] [MeasurableSpace T] [MeasurableSingletonClass G] [MeasurableSingletonClass T] [AddGroup G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → G} [FiniteRange X] [FiniteRange Y] {Z : Ω → T} [FiniteRange Z] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) : max H[X | Z ; μ] H[Y | Z ; μ] - I[X : Y|Z;μ] ≤ H[X + Y | Z ; μ]

max(H[X | Z], H[Y | Z]) - I[X : Y | Z] ≤ H[X + Y | Z]

theorem ProbabilityTheory.max_entropy_le_entropy_mul {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → G} [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) (h : IndepFun X Y μ) : max H[X ; μ] H[Y ; μ] ≤ H[X * Y ; μ]

If X, Y are independent, then max(H[X], H[Y]) ≤ H[X * Y].

theorem ProbabilityTheory.max_entropy_le_entropy_add {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → G} [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) (h : IndepFun X Y μ) : max H[X ; μ] H[Y ; μ] ≤ H[X + Y ; μ]

If X, Y are independent, then max(H[X], H[Y]) ≤ H[X + Y]

theorem ProbabilityTheory.max_entropy_le_entropy_div {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Group G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → G} [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) (h : IndepFun X Y μ) : max H[X ; μ] H[Y ; μ] ≤ H[X / Y ; μ]

If X, Y are independent, then max(H[X], H[Y]) ≤ H[X / Y].

theorem ProbabilityTheory.max_entropy_le_entropy_sub {Ω : Type uΩ} {G : Type uS} [mΩ : MeasurableSpace Ω] [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] {X : Ω → G} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → G} [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) (h : IndepFun X Y μ) : max H[X ; μ] H[Y ; μ] ≤ H[X - Y ; μ]

If X, Y are independent, then max(H[X], H[Y]) ≤ H[X - Y].

theorem ProbabilityTheory.max_entropy_le_entropy_prod {Ω : Type uΩ} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {G : Type u_1} [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [CommGroup G] [MeasurableMul₂ G] {I : Type u_2} {s : Finset I} {i₀ : I} (hi₀ : i₀ ∈ s) {X : I → Ω → G} [∀ (i : I), FiniteRange (X i)] (hX : ∀ (i : I), Measurable (X i)) (h_indep : iIndepFun X μ) : H[X i₀ ; μ] ≤ H[∏ i ∈ s, X i ; μ]

If X₁, ..., Xₙ are independent and s ⊆ {1, ..., n}, then for all i ∈ s, H[Xᵢ] ≤ H[∏ j ∈ s, Xⱼ].

theorem ProbabilityTheory.max_entropy_le_entropy_sum {Ω : Type uΩ} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {G : Type u_1} [Countable G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] [MeasurableAdd₂ G] {I : Type u_2} {s : Finset I} {i₀ : I} (hi₀ : i₀ ∈ s) {X : I → Ω → G} [∀ (i : I), FiniteRange (X i)] (hX : ∀ (i : I), Measurable (X i)) (h_indep : iIndepFun X μ) : H[X i₀ ; μ] ≤ H[∑ i ∈ s, X i ; μ]

If X₁, ..., Xₙ are independent and s ⊆ {1, ..., n}, then for all i ∈ s, H[Xᵢ] ≤ H[∑ j ∈ s, Xⱼ].