Kernel entropy and mutual information in a commutative group

Main definitions

Main results

@[simp]

theorem measureEntropy_inv {G : Type u_5} [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [Countable G] (μ : MeasureTheory.Measure G) : Hm[MeasureTheory.Measure.map (fun (x : G) => x⁻¹) μ] = Hm[μ]

@[simp]

theorem measureEntropy_neg {G : Type u_5} [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [Countable G] (μ : MeasureTheory.Measure G) : Hm[MeasureTheory.Measure.map (fun (x : G) => -x) μ] = Hm[μ]

theorem measureEntropy_div_comm {G : Type u_5} [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [Countable G] (μ : MeasureTheory.Measure (G × G)) : Hm[MeasureTheory.Measure.map (fun (p : G × G) => p.1 / p.2) μ] = Hm[MeasureTheory.Measure.map (fun (p : G × G) => p.2 / p.1) μ]

theorem measureEntropy_sub_comm {G : Type u_5} [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [Countable G] (μ : MeasureTheory.Measure (G × G)) : Hm[MeasureTheory.Measure.map (fun (p : G × G) => p.1 - p.2) μ] = Hm[MeasureTheory.Measure.map (fun (p : G × G) => p.2 - p.1) μ]

theorem ProbabilityTheory.Kernel.entropy_inv {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [Countable G] (κ : ProbabilityTheory.Kernel T G) (μ : MeasureTheory.Measure T) : Hk[κ.map fun (x : G) => x⁻¹ , μ] = Hk[κ , μ]

theorem ProbabilityTheory.Kernel.entropy_neg {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [Countable G] (κ : ProbabilityTheory.Kernel T G) (μ : MeasureTheory.Measure T) : Hk[κ.map fun (x : G) => -x , μ] = Hk[κ , μ]

theorem ProbabilityTheory.Kernel.entropy_div_comm {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [Countable G] (κ : ProbabilityTheory.Kernel T (G × G)) (μ : MeasureTheory.Measure T) : Hk[κ.map fun (p : G × G) => p.1 / p.2 , μ] = Hk[κ.map fun (p : G × G) => p.2 / p.1 , μ]

theorem ProbabilityTheory.Kernel.entropy_sub_comm {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [Countable G] (κ : ProbabilityTheory.Kernel T (G × G)) (μ : MeasureTheory.Measure T) : Hk[κ.map fun (p : G × G) => p.1 - p.2 , μ] = Hk[κ.map fun (p : G × G) => p.2 - p.1 , μ]

theorem ProbabilityTheory.Kernel.entropy_snd_sub_mutualInfo_le_entropy_map_mul {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [Countable G] [Countable T] [MeasurableSingletonClass T] (κ : ProbabilityTheory.Kernel T (G × G)) [ProbabilityTheory.IsZeroOrMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) : Hk[κ.snd , μ] - Ik[κ , μ] ≤ Hk[κ.map fun (p : G × G) => p.1 * p.2 , μ]

theorem ProbabilityTheory.Kernel.entropy_snd_sub_mutualInfo_le_entropy_map_add {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [Countable G] [Countable T] [MeasurableSingletonClass T] (κ : ProbabilityTheory.Kernel T (G × G)) [ProbabilityTheory.IsZeroOrMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) : Hk[κ.snd , μ] - Ik[κ , μ] ≤ Hk[κ.map fun (p : G × G) => p.1 + p.2 , μ]

theorem ProbabilityTheory.Kernel.entropy_snd_sub_mutualInfo_le_entropy_map_mul' {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [Countable G] [Countable T] [MeasurableSingletonClass T] (κ : ProbabilityTheory.Kernel T (G × G)) [ProbabilityTheory.IsZeroOrMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) : Hk[κ.snd , μ] - Ik[κ , μ] ≤ Hk[κ.map fun (p : G × G) => p.2 * p.1 , μ]

theorem ProbabilityTheory.Kernel.entropy_snd_sub_mutualInfo_le_entropy_map_add' {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [Countable G] [Countable T] [MeasurableSingletonClass T] (κ : ProbabilityTheory.Kernel T (G × G)) [ProbabilityTheory.IsZeroOrMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) : Hk[κ.snd , μ] - Ik[κ , μ] ≤ Hk[κ.map fun (p : G × G) => p.2 + p.1 , μ]

theorem ProbabilityTheory.Kernel.entropy_fst_sub_mutualInfo_le_entropy_map_mul {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [Countable G] [Countable T] [MeasurableSingletonClass T] (κ : ProbabilityTheory.Kernel T (G × G)) [ProbabilityTheory.IsZeroOrMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) : Hk[κ.fst , μ] - Ik[κ , μ] ≤ Hk[κ.map fun (p : G × G) => p.1 * p.2 , μ]

theorem ProbabilityTheory.Kernel.entropy_fst_sub_mutualInfo_le_entropy_map_add {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [Countable G] [Countable T] [MeasurableSingletonClass T] (κ : ProbabilityTheory.Kernel T (G × G)) [ProbabilityTheory.IsZeroOrMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) : Hk[κ.fst , μ] - Ik[κ , μ] ≤ Hk[κ.map fun (p : G × G) => p.1 + p.2 , μ]

theorem ProbabilityTheory.Kernel.entropy_fst_sub_mutualInfo_le_entropy_map_mul' {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [Countable G] [Countable T] [MeasurableSingletonClass T] (κ : ProbabilityTheory.Kernel T (G × G)) [ProbabilityTheory.IsZeroOrMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) : Hk[κ.fst , μ] - Ik[κ , μ] ≤ Hk[κ.map fun (p : G × G) => p.2 * p.1 , μ]

theorem ProbabilityTheory.Kernel.entropy_fst_sub_mutualInfo_le_entropy_map_add' {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [Countable G] [Countable T] [MeasurableSingletonClass T] (κ : ProbabilityTheory.Kernel T (G × G)) [ProbabilityTheory.IsZeroOrMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) : Hk[κ.fst , μ] - Ik[κ , μ] ≤ Hk[κ.map fun (p : G × G) => p.2 + p.1 , μ]

theorem ProbabilityTheory.Kernel.entropy_snd_sub_mutualInfo_le_entropy_map_div {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [Countable G] [Countable T] [MeasurableSingletonClass T] (κ : ProbabilityTheory.Kernel T (G × G)) [ProbabilityTheory.IsZeroOrMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) : Hk[κ.snd , μ] - Ik[κ , μ] ≤ Hk[κ.map fun (p : G × G) => p.1 / p.2 , μ]

theorem ProbabilityTheory.Kernel.entropy_snd_sub_mutualInfo_le_entropy_map_sub {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [Countable G] [Countable T] [MeasurableSingletonClass T] (κ : ProbabilityTheory.Kernel T (G × G)) [ProbabilityTheory.IsZeroOrMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) : Hk[κ.snd , μ] - Ik[κ , μ] ≤ Hk[κ.map fun (p : G × G) => p.1 - p.2 , μ]

theorem ProbabilityTheory.Kernel.entropy_fst_sub_mutualInfo_le_entropy_map_div {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [Countable G] [Countable T] [MeasurableSingletonClass T] (κ : ProbabilityTheory.Kernel T (G × G)) [ProbabilityTheory.IsZeroOrMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) : Hk[κ.fst , μ] - Ik[κ , μ] ≤ Hk[κ.map fun (p : G × G) => p.1 / p.2 , μ]

theorem ProbabilityTheory.Kernel.entropy_fst_sub_mutualInfo_le_entropy_map_sub {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [Countable G] [Countable T] [MeasurableSingletonClass T] (κ : ProbabilityTheory.Kernel T (G × G)) [ProbabilityTheory.IsZeroOrMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) : Hk[κ.fst , μ] - Ik[κ , μ] ≤ Hk[κ.map fun (p : G × G) => p.1 - p.2 , μ]

theorem ProbabilityTheory.Kernel.max_entropy_sub_mutualInfo_le_entropy_mul {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [Countable G] [Countable T] [MeasurableSingletonClass T] (κ : ProbabilityTheory.Kernel T (G × G)) [ProbabilityTheory.IsZeroOrMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) : Hk[κ.fst , μ] ⊔ Hk[κ.snd , μ] - Ik[κ , μ] ≤ Hk[κ.map fun (p : G × G) => p.1 * p.2 , μ]

theorem ProbabilityTheory.Kernel.max_entropy_sub_mutualInfo_le_entropy_add {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [Countable G] [Countable T] [MeasurableSingletonClass T] (κ : ProbabilityTheory.Kernel T (G × G)) [ProbabilityTheory.IsZeroOrMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) : Hk[κ.fst , μ] ⊔ Hk[κ.snd , μ] - Ik[κ , μ] ≤ Hk[κ.map fun (p : G × G) => p.1 + p.2 , μ]

theorem ProbabilityTheory.Kernel.max_entropy_sub_mutualInfo_le_entropy_mul' {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [Countable G] [Countable T] [MeasurableSingletonClass T] (κ : ProbabilityTheory.Kernel T (G × G)) [ProbabilityTheory.IsZeroOrMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) : Hk[κ.fst , μ] ⊔ Hk[κ.snd , μ] - Ik[κ , μ] ≤ Hk[κ.map fun (p : G × G) => p.2 * p.1 , μ]

theorem ProbabilityTheory.Kernel.max_entropy_sub_mutualInfo_le_entropy_add' {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [Countable G] [Countable T] [MeasurableSingletonClass T] (κ : ProbabilityTheory.Kernel T (G × G)) [ProbabilityTheory.IsZeroOrMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) : Hk[κ.fst , μ] ⊔ Hk[κ.snd , μ] - Ik[κ , μ] ≤ Hk[κ.map fun (p : G × G) => p.2 + p.1 , μ]

theorem ProbabilityTheory.Kernel.max_entropy_sub_mutualInfo_le_entropy_div {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [Countable G] [Countable T] [MeasurableSingletonClass T] (κ : ProbabilityTheory.Kernel T (G × G)) [ProbabilityTheory.IsZeroOrMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) : Hk[κ.fst , μ] ⊔ Hk[κ.snd , μ] - Ik[κ , μ] ≤ Hk[κ.map fun (p : G × G) => p.1 / p.2 , μ]

theorem ProbabilityTheory.Kernel.max_entropy_sub_mutualInfo_le_entropy_sub {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [Countable G] [Countable T] [MeasurableSingletonClass T] (κ : ProbabilityTheory.Kernel T (G × G)) [ProbabilityTheory.IsZeroOrMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) : Hk[κ.fst , μ] ⊔ Hk[κ.snd , μ] - Ik[κ , μ] ≤ Hk[κ.map fun (p : G × G) => p.1 - p.2 , μ]

theorem ProbabilityTheory.Kernel.max_entropy_le_entropy_mul_prod {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [Countable G] [Countable T] [MeasurableSingletonClass T] (κ : ProbabilityTheory.Kernel T G) [ProbabilityTheory.IsMarkovKernel κ] (η : ProbabilityTheory.Kernel T G) [ProbabilityTheory.IsMarkovKernel η] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) (hη : η.AEFiniteKernelSupport μ) : Hk[κ , μ] ⊔ Hk[η , μ] ≤ Hk[(κ.prod η).map fun (p : G × G) => p.1 * p.2 , μ]

theorem ProbabilityTheory.Kernel.max_entropy_le_entropy_add_sum {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [Countable G] [Countable T] [MeasurableSingletonClass T] (κ : ProbabilityTheory.Kernel T G) [ProbabilityTheory.IsMarkovKernel κ] (η : ProbabilityTheory.Kernel T G) [ProbabilityTheory.IsMarkovKernel η] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) (hη : η.AEFiniteKernelSupport μ) : Hk[κ , μ] ⊔ Hk[η , μ] ≤ Hk[(κ.prod η).map fun (p : G × G) => p.1 + p.2 , μ]

theorem ProbabilityTheory.Kernel.max_entropy_le_entropy_div_prod {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [Countable G] [Countable T] [MeasurableSingletonClass T] (κ : ProbabilityTheory.Kernel T G) [ProbabilityTheory.IsMarkovKernel κ] (η : ProbabilityTheory.Kernel T G) [ProbabilityTheory.IsMarkovKernel η] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) (hη : η.AEFiniteKernelSupport μ) : Hk[κ , μ] ⊔ Hk[η , μ] ≤ Hk[(κ.prod η).map fun (p : G × G) => p.1 / p.2 , μ]

theorem ProbabilityTheory.Kernel.max_entropy_le_entropy_sub_prod {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [Countable G] [Countable T] [MeasurableSingletonClass T] (κ : ProbabilityTheory.Kernel T G) [ProbabilityTheory.IsMarkovKernel κ] (η : ProbabilityTheory.Kernel T G) [ProbabilityTheory.IsMarkovKernel η] (μ : MeasureTheory.Measure T) [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) (hη : η.AEFiniteKernelSupport μ) : Hk[κ , μ] ⊔ Hk[η , μ] ≤ Hk[(κ.prod η).map fun (p : G × G) => p.1 - p.2 , μ]