Documentation

PFR.ForMathlib.Entropy.Kernel.Basic

Entropy of a kernel with respect to a measure #

Main definitions #

Main statements #

Notations #

Entropy of a kernel with respect to a measure.

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

    Pretty printer defined by notation3 command.

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

      Entropy of a kernel with respect to a measure.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem ProbabilityTheory.Kernel.entropy_congr {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] {μ : MeasureTheory.Measure T} {κ η : ProbabilityTheory.Kernel T S} (h : κ =ᵐ[μ] η) :
        Hk[κ , μ] = Hk[η , μ]
        @[simp]

        Constant kernels with finite support, have finite kernel support.

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

        theorem ProbabilityTheory.Kernel.entropy_eq_integral_sum {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] (κ : ProbabilityTheory.Kernel T S) [ProbabilityTheory.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] (κ : ProbabilityTheory.Kernel T S) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) {f : T × SU} (hf : ∀ (t : T), Function.Injective fun (x : S) => f (t, x)) (hmes : Measurable f) :
        Hk[(κ.compProd (ProbabilityTheory.Kernel.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] (κ : ProbabilityTheory.Kernel T S) (μ : MeasureTheory.Measure T) {f : SU} (hf : Function.Injective f) (hmes : Measurable f) :
        Hk[κ.map f , μ] = 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 μ] {κ : ProbabilityTheory.Kernel T S} [ProbabilityTheory.IsZeroOrMarkovKernel κ] {η : ProbabilityTheory.Kernel (T × S) U} [ProbabilityTheory.IsMarkovKernel η] [ProbabilityTheory.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 μ] {κ : ProbabilityTheory.Kernel T S} [ProbabilityTheory.IsZeroOrMarkovKernel κ] {η : ProbabilityTheory.Kernel (T × S) U} [ProbabilityTheory.IsMarkovKernel η] [ProbabilityTheory.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 μ] {κ : ProbabilityTheory.Kernel T S} [ProbabilityTheory.IsZeroOrMarkovKernel κ] {η : ProbabilityTheory.Kernel (T × S) U} [ProbabilityTheory.IsMarkovKernel η] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) (hη : η.AEFiniteKernelSupport (μ.compProd κ)) :
        Hk[κ.compProd η , μ] = Hk[κ , μ] + Hk[η , μ.compProd κ]
        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] {κ : ProbabilityTheory.Kernel T (S × U)} [ProbabilityTheory.IsZeroOrMarkovKernel κ] [hU : Nonempty U] {μ : MeasureTheory.Measure T} [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.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] {κ : ProbabilityTheory.Kernel T (S × U)} [ProbabilityTheory.IsZeroOrMarkovKernel κ] {μ : MeasureTheory.Measure T} [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) :
        Hk[κ , μ] = Hk[κ.snd , μ] + Hk[κ.swapRight.condKernel , μ.compProd κ.snd]
        @[simp]

        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] {κ : ProbabilityTheory.Kernel T S} {η : ProbabilityTheory.Kernel T U} [ProbabilityTheory.IsZeroOrMarkovKernel κ] [ProbabilityTheory.IsZeroOrMarkovKernel η] {μ : MeasureTheory.Measure T} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (f : SU) (g : US) (h1 : η = κ.map f) (h2 : κ = η.map g) [ProbabilityTheory.FiniteSupport μ] (hκ : κ.AEFiniteKernelSupport μ) (hη : η.AEFiniteKernelSupport μ) :
        Hk[κ , μ] = Hk[η , μ]