Documentation

PFR.ForMathlib.Entropy.Kernel.Group

Kernel entropy and mutual information in a commutative group #

Main definitions #

Main results #

source
@[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[μ]
source
@[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[μ]
source
theorem measureEntropy_sub_comm {G : Type u_5} [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [MeasurableSub₂ 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) μ]
source
theorem measureEntropy_div_comm {G : Type u_5} [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [MeasurableDiv₂ 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) μ]
source
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[ProbabilityTheory.kernel.map κ (fun (x : G) => -x) ⋯ , μ] = Hk[κ , μ]
source
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[ProbabilityTheory.kernel.map κ (fun (x : G) => x⁻¹) ⋯ , μ] = Hk[κ , μ]
source
theorem ProbabilityTheory.kernel.entropy_sub_comm {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [MeasurableSub₂ G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T (G × G))) (μ : MeasureTheory.Measure T) :
Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.1 - p.2) ⋯ , μ] = Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.2 - p.1) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.entropy_div_comm {G : Type u_5} {T : Type u_6} [MeasurableSpace T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [MeasurableDiv₂ G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T (G × G))) (μ : MeasureTheory.Measure T) :
Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.1 / p.2) ⋯ , μ] = Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.2 / p.1) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.entropy_snd_sub_mutualInfo_le_entropy_map_add {G : Type u_5} {T : Type u_6} [Countable T] [Nonempty T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [MeasurableAdd₂ G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T (G × G))) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) :
Hk[ProbabilityTheory.kernel.snd κ , μ] - Ik[κ , μ] ≤ Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.1 + p.2) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.entropy_snd_sub_mutualInfo_le_entropy_map_mul {G : Type u_5} {T : Type u_6} [Countable T] [Nonempty T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [MeasurableMul₂ G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T (G × G))) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) :
Hk[ProbabilityTheory.kernel.snd κ , μ] - Ik[κ , μ] ≤ Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.1 * p.2) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.entropy_snd_sub_mutualInfo_le_entropy_map_add' {G : Type u_5} {T : Type u_6} [Countable T] [Nonempty T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T (G × G))) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) :
Hk[ProbabilityTheory.kernel.snd κ , μ] - Ik[κ , μ] ≤ Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.2 + p.1) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.entropy_snd_sub_mutualInfo_le_entropy_map_mul' {G : Type u_5} {T : Type u_6} [Countable T] [Nonempty T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T (G × G))) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) :
Hk[ProbabilityTheory.kernel.snd κ , μ] - Ik[κ , μ] ≤ Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.2 * p.1) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.entropy_fst_sub_mutualInfo_le_entropy_map_add {G : Type u_5} {T : Type u_6} [Countable T] [Nonempty T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [MeasurableAdd₂ G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T (G × G))) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) :
Hk[ProbabilityTheory.kernel.fst κ , μ] - Ik[κ , μ] ≤ Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.1 + p.2) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.entropy_fst_sub_mutualInfo_le_entropy_map_mul {G : Type u_5} {T : Type u_6} [Countable T] [Nonempty T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [MeasurableMul₂ G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T (G × G))) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) :
Hk[ProbabilityTheory.kernel.fst κ , μ] - Ik[κ , μ] ≤ Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.1 * p.2) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.entropy_fst_sub_mutualInfo_le_entropy_map_add' {G : Type u_5} {T : Type u_6} [Countable T] [Nonempty T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [MeasurableAdd₂ G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T (G × G))) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) :
Hk[ProbabilityTheory.kernel.fst κ , μ] - Ik[κ , μ] ≤ Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.2 + p.1) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.entropy_fst_sub_mutualInfo_le_entropy_map_mul' {G : Type u_5} {T : Type u_6} [Countable T] [Nonempty T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [MeasurableMul₂ G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T (G × G))) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) :
Hk[ProbabilityTheory.kernel.fst κ , μ] - Ik[κ , μ] ≤ Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.2 * p.1) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.entropy_snd_sub_mutualInfo_le_entropy_map_sub {G : Type u_5} {T : Type u_6} [Countable T] [Nonempty T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [MeasurableSub₂ G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T (G × G))) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) :
Hk[ProbabilityTheory.kernel.snd κ , μ] - Ik[κ , μ] ≤ Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.1 - p.2) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.entropy_snd_sub_mutualInfo_le_entropy_map_div {G : Type u_5} {T : Type u_6} [Countable T] [Nonempty T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [MeasurableDiv₂ G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T (G × G))) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) :
Hk[ProbabilityTheory.kernel.snd κ , μ] - Ik[κ , μ] ≤ Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.1 / p.2) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.entropy_fst_sub_mutualInfo_le_entropy_map_sub {G : Type u_5} {T : Type u_6} [Countable T] [Nonempty T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [MeasurableSub₂ G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T (G × G))) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) :
Hk[ProbabilityTheory.kernel.fst κ , μ] - Ik[κ , μ] ≤ Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.1 - p.2) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.entropy_fst_sub_mutualInfo_le_entropy_map_div {G : Type u_5} {T : Type u_6} [Countable T] [Nonempty T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [MeasurableDiv₂ G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T (G × G))) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) :
Hk[ProbabilityTheory.kernel.fst κ , μ] - Ik[κ , μ] ≤ Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.1 / p.2) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.max_entropy_sub_mutualInfo_le_entropy_add {G : Type u_5} {T : Type u_6} [Countable T] [Nonempty T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [MeasurableAdd₂ G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T (G × G))) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) :
max (Hk[ProbabilityTheory.kernel.fst κ , μ]) (Hk[ProbabilityTheory.kernel.snd κ , μ]) - Ik[κ , μ] ≤ Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.1 + p.2) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.max_entropy_sub_mutualInfo_le_entropy_mul {G : Type u_5} {T : Type u_6} [Countable T] [Nonempty T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [MeasurableMul₂ G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T (G × G))) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) :
max (Hk[ProbabilityTheory.kernel.fst κ , μ]) (Hk[ProbabilityTheory.kernel.snd κ , μ]) - Ik[κ , μ] ≤ Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.1 * p.2) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.max_entropy_sub_mutualInfo_le_entropy_add' {G : Type u_5} {T : Type u_6} [Countable T] [Nonempty T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [MeasurableAdd₂ G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T (G × G))) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) :
max (Hk[ProbabilityTheory.kernel.fst κ , μ]) (Hk[ProbabilityTheory.kernel.snd κ , μ]) - Ik[κ , μ] ≤ Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.2 + p.1) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.max_entropy_sub_mutualInfo_le_entropy_mul' {G : Type u_5} {T : Type u_6} [Countable T] [Nonempty T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [MeasurableMul₂ G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T (G × G))) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) :
max (Hk[ProbabilityTheory.kernel.fst κ , μ]) (Hk[ProbabilityTheory.kernel.snd κ , μ]) - Ik[κ , μ] ≤ Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.2 * p.1) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.max_entropy_sub_mutualInfo_le_entropy_sub {G : Type u_5} {T : Type u_6} [Countable T] [Nonempty T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [MeasurableSub₂ G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T (G × G))) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) :
max (Hk[ProbabilityTheory.kernel.fst κ , μ]) (Hk[ProbabilityTheory.kernel.snd κ , μ]) - Ik[κ , μ] ≤ Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.1 - p.2) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.max_entropy_sub_mutualInfo_le_entropy_div {G : Type u_5} {T : Type u_6} [Countable T] [Nonempty T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [MeasurableDiv₂ G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T (G × G))) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) :
max (Hk[ProbabilityTheory.kernel.fst κ , μ]) (Hk[ProbabilityTheory.kernel.snd κ , μ]) - Ik[κ , μ] ≤ Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.1 / p.2) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.max_entropy_le_entropy_add_sum {G : Type u_5} {T : Type u_6} [Countable T] [Nonempty T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [MeasurableAdd₂ G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T G)) [ProbabilityTheory.IsMarkovKernel κ] (η : ↥(ProbabilityTheory.kernel T G)) [ProbabilityTheory.IsMarkovKernel η] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) (hη : ProbabilityTheory.kernel.AEFiniteKernelSupport η μ) :
max (Hk[κ , μ]) (Hk[η , μ]) ≤ Hk[ProbabilityTheory.kernel.map (ProbabilityTheory.kernel.prod κ η) (fun (p : G × G) => p.1 + p.2) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.max_entropy_le_entropy_mul_prod {G : Type u_5} {T : Type u_6} [Countable T] [Nonempty T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [MeasurableMul₂ G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T G)) [ProbabilityTheory.IsMarkovKernel κ] (η : ↥(ProbabilityTheory.kernel T G)) [ProbabilityTheory.IsMarkovKernel η] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) (hη : ProbabilityTheory.kernel.AEFiniteKernelSupport η μ) :
max (Hk[κ , μ]) (Hk[η , μ]) ≤ Hk[ProbabilityTheory.kernel.map (ProbabilityTheory.kernel.prod κ η) (fun (p : G × G) => p.1 * p.2) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.max_entropy_le_entropy_sub_prod {G : Type u_5} {T : Type u_6} [Countable T] [Nonempty T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace G] [MeasurableSingletonClass G] [AddGroup G] [MeasurableSub₂ G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T G)) [ProbabilityTheory.IsMarkovKernel κ] (η : ↥(ProbabilityTheory.kernel T G)) [ProbabilityTheory.IsMarkovKernel η] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) (hη : ProbabilityTheory.kernel.AEFiniteKernelSupport η μ) :
max (Hk[κ , μ]) (Hk[η , μ]) ≤ Hk[ProbabilityTheory.kernel.map (ProbabilityTheory.kernel.prod κ η) (fun (p : G × G) => p.1 - p.2) ⋯ , μ]
source
theorem ProbabilityTheory.kernel.max_entropy_le_entropy_div_prod {G : Type u_5} {T : Type u_6} [Countable T] [Nonempty T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace G] [MeasurableSingletonClass G] [Group G] [MeasurableDiv₂ G] [Countable G] (κ : ↥(ProbabilityTheory.kernel T G)) [ProbabilityTheory.IsMarkovKernel κ] (η : ↥(ProbabilityTheory.kernel T G)) [ProbabilityTheory.IsMarkovKernel η] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) (hη : ProbabilityTheory.kernel.AEFiniteKernelSupport η μ) :
max (Hk[κ , μ]) (Hk[η , μ]) ≤ Hk[ProbabilityTheory.kernel.map (ProbabilityTheory.kernel.prod κ η) (fun (p : G × G) => p.1 / p.2) ⋯ , μ]