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] (κ : 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_app.ProbabilityTheory.Kernel.entropy» : 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] (κ : 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} {κ η : Kernel T S} (h : ⇑κ =ᵐ[μ] ⇑η) : Hk[κ , μ] = Hk[η , μ]

theorem ProbabilityTheory.Kernel.entropy_nonneg {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] (κ : 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[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) [FiniteSupport ν] : (const T ν).FiniteKernelSupport

Constant kernels with finite support, have finite kernel support.

theorem ProbabilityTheory.Kernel.finiteSupport_of_compProd' {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] {μ : MeasureTheory.Measure T} [MeasureTheory.IsFiniteMeasure μ] {κ : Kernel T S} [IsZeroOrMarkovKernel κ] [FiniteSupport μ] (hκ : κ.FiniteKernelSupport) : 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} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass S] [Countable T] [MeasurableSingletonClass T] {μ : MeasureTheory.Measure T} [MeasureTheory.IsFiniteMeasure μ] {κ : Kernel T S} [IsZeroOrMarkovKernel κ] [FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) : FiniteSupport (μ.compProd κ)

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

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

theorem ProbabilityTheory.Kernel.entropy_eq_integral_sum {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] (κ : Kernel T S) [IsZeroOrMarkovKernel κ] (μ : 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] (κ : Kernel T S) [IsMarkovKernel κ] (μ : MeasureTheory.Measure T) {f : T × S → U} (hf : ∀ (t : T), Function.Injective fun (x : S) => f (t, x)) (hmes : Measurable f) : Hk[(κ.compProd (deterministic f hmes)).snd , μ] = 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] (κ : Kernel T S) (μ : MeasureTheory.Measure T) {f : S → U} (hf : Function.Injective f) (hmes : Measurable f) : Hk[κ.map f , μ] = Hk[κ , μ]

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

theorem ProbabilityTheory.Kernel.entropy_swapRight {S : Type u_2} {T : Type u_3} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSingletonClass S] [MeasurableSingletonClass U] (κ : Kernel T (S × U)) (μ : MeasureTheory.Measure T) : Hk[κ.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'] (κ : Kernel T S) (μ : MeasureTheory.Measure T) (f : T' → T) (hf : MeasurableEmbedding f) (hf_range : Set.range f =ᵐ[μ] Set.univ) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.comap f μ)] (hfμ : FiniteSupport (MeasureTheory.Measure.comap f μ)) : Hk[κ.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'] {μ : MeasureTheory.Measure T} (f : T' ≃ᵐ T) [FiniteSupport μ] : 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'] (κ : Kernel T S) {μ : MeasureTheory.Measure T} (f : T' ≃ᵐ T) [MeasureTheory.IsFiniteMeasure μ] [FiniteSupport μ] : Hk[κ.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'] (κ : Kernel (T' × T) S) {μ : MeasureTheory.Measure (T' × T)} [MeasureTheory.IsFiniteMeasure μ] [FiniteSupport μ] : Hk[κ.comap Prod.swap ⋯ , MeasureTheory.Measure.comap Prod.swap μ] = Hk[κ , μ]

theorem ProbabilityTheory.Kernel.entropy_prodMkLeft_unit {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass T] (κ : Kernel T S) {μ : MeasureTheory.Measure T} [MeasureTheory.IsZeroOrProbabilityMeasure μ] [FiniteSupport μ] : Hk[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] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [MeasurableSingletonClass U] {μ : MeasureTheory.Measure T} [MeasureTheory.IsFiniteMeasure μ] {κ : Kernel T S} [IsZeroOrMarkovKernel κ] {η : Kernel (T × S) U} [IsMarkovKernel η] [FiniteSupport μ] (hκ : κ.FiniteKernelSupport) (hη : η.FiniteKernelSupport) : Hk[κ.compProd η , μ] = Hk[κ , μ] + ∫ (x : T), (fun (t : T) => Hk[η.comap (Prod.mk t) ⋯ , κ t]) x ∂μ

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

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

@[simp]

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

@[simp]

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

theorem ProbabilityTheory.Kernel.nonempty_of_isMarkovKernel {α : Type u_5} {β : Type u_6} [MeasurableSpace α] [MeasurableSpace β] (κ : Kernel α β) [IsMarkovKernel κ] [Nonempty α] : Nonempty β

theorem ProbabilityTheory.Kernel.nonempty_of_isProbabilityMeasure_of_isMarkovKernel {α : Type u_5} {β : Type u_6} [MeasurableSpace α] [MeasurableSpace β] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] (κ : Kernel α β) [IsMarkovKernel κ] : Nonempty β

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

theorem ProbabilityTheory.Kernel.entropy_map_le {S : Type u_2} {T : Type u_3} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [Countable S] [MeasurableSingletonClass S] [Countable T] [MeasurableSingletonClass T] [Countable U] [MeasurableSingletonClass U] {κ : Kernel T S} [IsZeroOrMarkovKernel κ] {μ : MeasureTheory.Measure T} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (f : S → U) [FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) : Hk[κ.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} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [Countable S] [MeasurableSingletonClass S] [Countable T] [MeasurableSingletonClass T] [Countable U] [MeasurableSingletonClass U] {κ : Kernel T S} {η : Kernel T U} [IsZeroOrMarkovKernel κ] [IsZeroOrMarkovKernel η] {μ : MeasureTheory.Measure T} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (f : S → U) (g : U → S) (h1 : η = κ.map f) (h2 : κ = η.map g) [FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) (hη : η.AEFiniteKernelSupport μ) : Hk[κ , μ] = Hk[η , μ]

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

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