Entropy of a kernel with respect to a measure

Main definitions

• kernel.entropy: entropy of a kernel κ with respect to a measure μ, μ[fun t ↦ measureEntropy (κ t)]. We use the notation Hk[κ, μ].

Main statements

• chain_rule: Hk[κ, μ] = Hk[fst κ, μ] + Hk[condKernel κ, μ ⊗ₘ (fst κ)].
• entropy_map_le: data-processing inequality for the kernel entropy

Notations

• Hk[κ, μ] = kernel.entropy κ μ

noncomputable def ProbabilityTheory.kernel.entropy {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] (κ : ↥(ProbabilityTheory.kernel T S)) (μ : MeasureTheory.Measure T) : ℝ

Entropy of a kernel with respect to a measure.

Equations

• Hk[κ , μ] = ∫ (x : T), (fun (y : T) => Hm[κ y]) x ∂μ

def ProbabilityTheory.kernel.«termHk[_,_]» : Lean.ParserDescr

Entropy of a kernel with respect to a measure.

Equations

• One or more equations did not get rendered due to their size.

def ProbabilityTheory.kernel.«termHk[_,_]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ProbabilityTheory.kernel.entropy_zero_measure {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] (κ : ↥(ProbabilityTheory.kernel T S)) : Hk[κ , 0] = 0

@[simp]

theorem ProbabilityTheory.kernel.entropy_zero_kernel {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] (μ : MeasureTheory.Measure T) : Hk[0 , μ] = 0

theorem ProbabilityTheory.kernel.entropy_congr {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] {μ : MeasureTheory.Measure T} {κ : ↥(ProbabilityTheory.kernel T S)} {η : ↥(ProbabilityTheory.kernel T S)} (h : μ.ae.EventuallyEq ⇑κ ⇑η) : Hk[κ , μ] = Hk[η , μ]

theorem ProbabilityTheory.kernel.entropy_nonneg {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] (κ : ↥(ProbabilityTheory.kernel T S)) (μ : MeasureTheory.Measure T) : 0 ≤ Hk[κ , μ]

@[simp]

theorem ProbabilityTheory.kernel.entropy_const {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] (ν : MeasureTheory.Measure S) (μ : MeasureTheory.Measure T) : Hk[ProbabilityTheory.kernel.const T ν , μ] = (μ Set.univ).toReal * Hm[ν]

theorem ProbabilityTheory.kernel.finiteKernelSupport_of_const {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] (ν : MeasureTheory.Measure S) [ProbabilityTheory.FiniteSupport ν] : ProbabilityTheory.kernel.FiniteKernelSupport (ProbabilityTheory.kernel.const T ν)

Constant kernels with finite support, have finite kernel support.

theorem ProbabilityTheory.kernel.finiteSupport_of_compProd' {S : Type u_2} {T : Type u_3} [Countable S] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] {μ : MeasureTheory.Measure T} [MeasureTheory.IsFiniteMeasure μ] {κ : ↥(ProbabilityTheory.kernel T S)} [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.FiniteKernelSupport κ) : ProbabilityTheory.FiniteSupport (μ.compProd κ)

Composing a finitely supported measure with a finitely supported kernel gives a finitely supported kernel.

theorem ProbabilityTheory.kernel.finiteSupport_of_compProd {S : Type u_2} {T : Type u_3} [Countable S] [Nonempty S] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] {μ : MeasureTheory.Measure T} [MeasureTheory.IsFiniteMeasure μ] {κ : ↥(ProbabilityTheory.kernel T S)} [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) : ProbabilityTheory.FiniteSupport (μ.compProd κ)

theorem ProbabilityTheory.kernel.aefiniteKernelSupport_condDistrib {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [Countable S] [Nonempty S] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] (X : Ω → S) (Y : Ω → T) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (hX : Measurable X) (hY : Measurable Y) [FiniteRange X] [FiniteRange Y] : ProbabilityTheory.kernel.AEFiniteKernelSupport (ProbabilityTheory.condDistrib X Y μ) (MeasureTheory.Measure.map Y μ)

theorem ProbabilityTheory.kernel.entropy_le_log_card {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSingletonClass S] [MeasurableSpace T] (κ : ↥(ProbabilityTheory.kernel T S)) (μ : MeasureTheory.Measure T) [Fintype S] [MeasureTheory.IsProbabilityMeasure μ] : Hk[κ , μ] ≤ (↑(Fintype.card S)).log

theorem ProbabilityTheory.kernel.entropy_eq_integral_sum {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] (κ : ↥(ProbabilityTheory.kernel T S)) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) : Hk[κ , μ] = ∫ (x : T), (fun (y : T) => ∑' (x : S), ((κ y) {x}).toReal.negMulLog) x ∂μ

theorem ProbabilityTheory.kernel.entropy_snd_compProd_deterministic_of_injective {S : Type u_2} {T : Type u_3} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSingletonClass U] (κ : ↥(ProbabilityTheory.kernel T S)) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) {f : T × S → U} (hf : ∀ (t : T), Function.Injective fun (x : S) => f (t, x)) (hmes : Measurable f) : Hk[ProbabilityTheory.kernel.snd (ProbabilityTheory.kernel.compProd κ (ProbabilityTheory.kernel.deterministic f hmes)) , μ] = Hk[κ , μ]

theorem ProbabilityTheory.kernel.entropy_map_of_injective {S : Type u_2} {T : Type u_3} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSingletonClass U] (κ : ↥(ProbabilityTheory.kernel T S)) (μ : MeasureTheory.Measure T) {f : S → U} (hf : Function.Injective f) (hmes : Measurable f) : Hk[ProbabilityTheory.kernel.map κ f hmes , μ] = Hk[κ , μ]

theorem ProbabilityTheory.kernel.entropy_map_swap {S : Type u_2} {T : Type u_3} {U : Type u_4} [MeasurableSpace S] [MeasurableSingletonClass S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSingletonClass U] (κ : ↥(ProbabilityTheory.kernel T (S × U))) (μ : MeasureTheory.Measure T) : Hk[ProbabilityTheory.kernel.map κ Prod.swap ⋯ , μ] = Hk[κ , μ]

theorem ProbabilityTheory.kernel.entropy_swapRight {S : Type u_2} {T : Type u_3} {U : Type u_4} [MeasurableSpace S] [MeasurableSingletonClass S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSingletonClass U] (κ : ↥(ProbabilityTheory.kernel T (S × U))) (μ : MeasureTheory.Measure T) : Hk[ProbabilityTheory.kernel.swapRight κ , μ] = Hk[κ , μ]

theorem ProbabilityTheory.kernel.entropy_comap {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass T] {T' : Type u_5} [MeasurableSpace T'] [MeasurableSingletonClass T'] (κ : ↥(ProbabilityTheory.kernel T S)) (μ : MeasureTheory.Measure T) (f : T' → T) (hf : MeasurableEmbedding f) (hf_range : μ.ae.EventuallyEq (Set.range f) Set.univ) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.comap f μ)] (hfμ : ProbabilityTheory.FiniteSupport (MeasureTheory.Measure.comap f μ)) : Hk[ProbabilityTheory.kernel.comap κ f ⋯ , MeasureTheory.Measure.comap f μ] = Hk[κ , μ]

theorem ProbabilityTheory.kernel.FiniteSupport.comap_equiv {T : Type u_3} [MeasurableSpace T] [MeasurableSingletonClass T] {T' : Type u_5} [MeasurableSpace T'] [MeasurableSingletonClass T'] {μ : MeasureTheory.Measure T} (f : T' ≃ᵐ T) [ProbabilityTheory.FiniteSupport μ] : ProbabilityTheory.FiniteSupport (MeasureTheory.Measure.comap (⇑f) μ)

theorem ProbabilityTheory.kernel.entropy_comap_equiv {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass T] {T' : Type u_5} [MeasurableSpace T'] [MeasurableSingletonClass T'] (κ : ↥(ProbabilityTheory.kernel T S)) {μ : MeasureTheory.Measure T} (f : T' ≃ᵐ T) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.FiniteSupport μ] : Hk[ProbabilityTheory.kernel.comap κ ⇑f ⋯ , MeasureTheory.Measure.comap (⇑f) μ] = Hk[κ , μ]

theorem ProbabilityTheory.kernel.entropy_comap_swap {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass T] {T' : Type u_5} [MeasurableSpace T'] [MeasurableSingletonClass T'] [Nonempty T'] (κ : ↥(ProbabilityTheory.kernel (T' × T) S)) {μ : MeasureTheory.Measure (T' × T)} [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.FiniteSupport μ] : Hk[ProbabilityTheory.kernel.comap κ Prod.swap ⋯ , MeasureTheory.Measure.comap Prod.swap μ] = Hk[κ , μ]

def ProbabilityTheory.kernel.prodMKLeft_unit_equiv (T : Type u_5) [MeasurableSpace T] : Unit × T ≃ᵐ T

Measurable equivalence with the product with the one-point space Unit.

Equations

• ProbabilityTheory.kernel.prodMKLeft_unit_equiv T = { toFun := fun (p : Unit × T) => p.2, invFun := Prod.mk (), left_inv := ⋯, right_inv := ⋯, measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem ProbabilityTheory.kernel.entropy_prodMkLeft_unit {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass T] (κ : ↥(ProbabilityTheory.kernel T S)) {μ : MeasureTheory.Measure T} [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] : Hk[ProbabilityTheory.kernel.prodMkLeft Unit κ , MeasureTheory.Measure.map (Prod.mk ()) μ] = Hk[κ , μ]

theorem ProbabilityTheory.kernel.entropy_compProd_aux {S : Type u_2} {T : Type u_3} {U : Type u_4} [MeasurableSpace S] [MeasurableSingletonClass S] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace U] [MeasurableSingletonClass U] {μ : MeasureTheory.Measure T} [MeasureTheory.IsFiniteMeasure μ] {κ : ↥(ProbabilityTheory.kernel T S)} [ProbabilityTheory.IsMarkovKernel κ] {η : ↥(ProbabilityTheory.kernel (T × S) U)} [ProbabilityTheory.IsMarkovKernel η] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.FiniteKernelSupport κ) (hη : ProbabilityTheory.kernel.FiniteKernelSupport η) : Hk[ProbabilityTheory.kernel.compProd κ η , μ] = Hk[κ , μ] + ∫ (x : T), (fun (t : T) => Hk[ProbabilityTheory.kernel.comap η (Prod.mk t) ⋯ , κ t]) x ∂μ

theorem ProbabilityTheory.kernel.entropy_compProd' {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace U] [MeasurableSingletonClass U] {μ : MeasureTheory.Measure T} [MeasureTheory.IsFiniteMeasure μ] {κ : ↥(ProbabilityTheory.kernel T S)} [ProbabilityTheory.IsMarkovKernel κ] {η : ↥(ProbabilityTheory.kernel (T × S) U)} [ProbabilityTheory.IsMarkovKernel η] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.FiniteKernelSupport κ) (hη : ProbabilityTheory.kernel.FiniteKernelSupport η) : Hk[ProbabilityTheory.kernel.compProd κ η , μ] = Hk[κ , μ] + Hk[η , μ.compProd κ]

theorem ProbabilityTheory.kernel.entropy_compProd {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [Nonempty S] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] [Nonempty U] [MeasurableSpace U] [MeasurableSingletonClass U] {μ : MeasureTheory.Measure T} [MeasureTheory.IsFiniteMeasure μ] {κ : ↥(ProbabilityTheory.kernel T S)} [ProbabilityTheory.IsMarkovKernel κ] {η : ↥(ProbabilityTheory.kernel (T × S) U)} [ProbabilityTheory.IsMarkovKernel η] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) (hη : ProbabilityTheory.kernel.AEFiniteKernelSupport η (μ.compProd κ)) : Hk[ProbabilityTheory.kernel.compProd κ η , μ] = Hk[κ , μ] + Hk[η , μ.compProd κ]

@[simp]

theorem ProbabilityTheory.kernel.entropy_deterministic {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] (f : T → S) (μ : MeasureTheory.Measure T) : Hk[ProbabilityTheory.kernel.deterministic f ⋯ , μ] = 0

@[simp]

theorem ProbabilityTheory.kernel.entropy_compProd_deterministic {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [Nonempty S] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] [Nonempty U] [MeasurableSpace U] [MeasurableSingletonClass U] (κ : ↥(ProbabilityTheory.kernel T S)) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsFiniteMeasure μ] (f : T × S → U) [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) : Hk[ProbabilityTheory.kernel.compProd κ (ProbabilityTheory.kernel.deterministic f ⋯) , μ] = Hk[κ , μ]

theorem ProbabilityTheory.kernel.chain_rule {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [Nonempty S] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] [Countable U] [MeasurableSpace U] [MeasurableSingletonClass U] {κ : ↥(ProbabilityTheory.kernel T (S × U))} [ProbabilityTheory.IsMarkovKernel κ] [hU : Nonempty U] {μ : MeasureTheory.Measure T} [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) : Hk[κ , μ] = Hk[ProbabilityTheory.kernel.fst κ , μ] + Hk[ProbabilityTheory.kernel.condKernel κ , μ.compProd (ProbabilityTheory.kernel.fst κ)]

theorem ProbabilityTheory.kernel.chain_rule' {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [Nonempty S] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] [Countable U] [Nonempty U] [MeasurableSpace U] [MeasurableSingletonClass U] {κ : ↥(ProbabilityTheory.kernel T (S × U))} [ProbabilityTheory.IsMarkovKernel κ] {μ : MeasureTheory.Measure T} [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) : Hk[κ , μ] = Hk[ProbabilityTheory.kernel.snd κ , μ] + Hk[ProbabilityTheory.kernel.condKernel (ProbabilityTheory.kernel.swapRight κ) , μ.compProd (ProbabilityTheory.kernel.snd κ)]

@[simp]

theorem ProbabilityTheory.kernel.entropy_prodMkRight {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [Nonempty S] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace U] {κ : ↥(ProbabilityTheory.kernel T S)} {η : ↥(ProbabilityTheory.kernel T U)} [ProbabilityTheory.IsMarkovKernel κ] {μ : MeasureTheory.Measure T} [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) : Hk[ProbabilityTheory.kernel.prodMkRight S η , μ.compProd κ] = Hk[η , μ]

theorem ProbabilityTheory.kernel.entropy_prodMkRight' {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [Nonempty S] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace U] {η : ↥(ProbabilityTheory.kernel T U)} {μ : MeasureTheory.Measure T} [MeasureTheory.IsProbabilityMeasure μ] {ν : MeasureTheory.Measure S} [MeasureTheory.IsProbabilityMeasure ν] [ProbabilityTheory.FiniteSupport μ] [ProbabilityTheory.FiniteSupport ν] : Hk[ProbabilityTheory.kernel.prodMkRight S η , μ.prod ν] = Hk[η , μ]

@[simp]

theorem ProbabilityTheory.kernel.entropy_prodMkLeft {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace U] {η : ↥(ProbabilityTheory.kernel T U)} {ν : MeasureTheory.Measure S} [MeasureTheory.IsProbabilityMeasure ν] {μ : MeasureTheory.Measure T} [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] [ProbabilityTheory.FiniteSupport ν] : Hk[ProbabilityTheory.kernel.prodMkLeft S η , ν.prod μ] = Hk[η , μ]

@[simp]

theorem ProbabilityTheory.kernel.entropy_prod {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [Nonempty S] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] [Countable U] [Nonempty U] [MeasurableSpace U] [MeasurableSingletonClass U] {κ : ↥(ProbabilityTheory.kernel T S)} {η : ↥(ProbabilityTheory.kernel T U)} [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η] {μ : MeasureTheory.Measure T} [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) (hη : ProbabilityTheory.kernel.AEFiniteKernelSupport η μ) : Hk[ProbabilityTheory.kernel.prod κ η , μ] = Hk[κ , μ] + Hk[η , μ]

theorem ProbabilityTheory.kernel.entropy_map_le {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [Nonempty S] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] [Countable U] [Nonempty U] [MeasurableSpace U] [MeasurableSingletonClass U] {κ : ↥(ProbabilityTheory.kernel T S)} [ProbabilityTheory.IsMarkovKernel κ] {μ : MeasureTheory.Measure T} [MeasureTheory.IsProbabilityMeasure μ] (f : S → U) [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) : Hk[ProbabilityTheory.kernel.map κ f ⋯ , μ] ≤ Hk[κ , μ]

Data-processing inequality for the kernel entropy.

theorem ProbabilityTheory.kernel.entropy_of_map_eq_of_map {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [Nonempty S] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] [Countable U] [Nonempty U] [MeasurableSpace U] [MeasurableSingletonClass U] {κ : ↥(ProbabilityTheory.kernel T S)} {η : ↥(ProbabilityTheory.kernel T U)} [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η] {μ : MeasureTheory.Measure T} [MeasureTheory.IsProbabilityMeasure μ] (f : S → U) (g : U → S) (h1 : η = ProbabilityTheory.kernel.map κ f ⋯) (h2 : κ = ProbabilityTheory.kernel.map η g ⋯) [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) (hη : ProbabilityTheory.kernel.AEFiniteKernelSupport η μ) : Hk[κ , μ] = Hk[η , μ]

theorem ProbabilityTheory.kernel.entropy_snd_le {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [Nonempty S] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] [Countable U] [Nonempty U] [MeasurableSpace U] [MeasurableSingletonClass U] {κ : ↥(ProbabilityTheory.kernel T (S × U))} [ProbabilityTheory.IsMarkovKernel κ] {μ : MeasureTheory.Measure T} [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) : Hk[ProbabilityTheory.kernel.snd κ , μ] ≤ Hk[κ , μ]

theorem ProbabilityTheory.kernel.entropy_fst_le {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [Nonempty S] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] [Countable U] [Nonempty U] [MeasurableSpace U] [MeasurableSingletonClass U] (κ : ↥(ProbabilityTheory.kernel T (S × U))) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) : Hk[ProbabilityTheory.kernel.fst κ , μ] ≤ Hk[κ , μ]