Ruzsa distance between kernels

Notations

• dk[κ ; μ # η ; ν] =

noncomputable def ProbabilityTheory.Kernel.rdistm {G : Type u_4} [MeasurableSpace G] [AddCommGroup G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) : ℝ

The Rusza distance between two measures, defined as H[X - Y] - H[X]/2 - H[Y]/2 where X and Y are independent variables distributed according to the two measures.

Equations

• ProbabilityTheory.Kernel.rdistm μ ν = Hm[MeasureTheory.Measure.map (fun (x : G × G) => x.1 - x.2) (μ.prod ν)] - Hm[μ] / 2 - Hm[ν] / 2

noncomputable def ProbabilityTheory.Kernel.rdist {T : Type u_1} {T' : Type u_2} {G : Type u_4} [MeasurableSpace T] [MeasurableSpace T'] [MeasurableSpace G] [AddCommGroup G] (κ : ProbabilityTheory.Kernel T G) (η : ProbabilityTheory.Kernel T' G) (μ : MeasureTheory.Measure T) (ν : MeasureTheory.Measure T') : ℝ

The Rusza distance between two kernels taking values in the same space, defined as the average Rusza distance between the image measures.

Equations

• dk[κ ; μ # η ; ν] = ∫ (x : T × T'), (fun (p : T × T') => ProbabilityTheory.Kernel.rdistm (κ p.1) (η p.2)) x ∂μ.prod ν

def ProbabilityTheory.Kernel.«termDk[_;_#_;_]» : Lean.ParserDescr

The Rusza distance between two kernels taking values in the same space, defined as the average Rusza distance between the image measures.

Equations

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

def ProbabilityTheory.Kernel.«termDk[_;_#_;_]».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.rdist_zero_right {T : Type u_1} {T' : Type u_2} {G : Type u_4} [MeasurableSpace T] [MeasurableSpace T'] [MeasurableSpace G] [AddCommGroup G] (κ : ProbabilityTheory.Kernel T G) (η : ProbabilityTheory.Kernel T' G) (μ : MeasureTheory.Measure T) : dk[κ ; μ # η ; 0] = 0

@[simp]

theorem ProbabilityTheory.Kernel.rdist_zero_left {T : Type u_1} {T' : Type u_2} {G : Type u_4} [MeasurableSpace T] [MeasurableSpace T'] [MeasurableSpace G] [AddCommGroup G] (κ : ProbabilityTheory.Kernel T G) (η : ProbabilityTheory.Kernel T' G) (ν' : MeasureTheory.Measure T') : dk[κ ; 0 # η ; ν'] = 0

theorem ProbabilityTheory.Kernel.rdist_eq {T : Type u_1} {T' : Type u_2} {G : Type u_4} [MeasurableSpace T] [MeasurableSpace T'] [MeasurableSpace G] [AddCommGroup G] [Countable T] [MeasurableSingletonClass T] [Countable T'] [MeasurableSingletonClass T'] {κ : ProbabilityTheory.Kernel T G} {η : ProbabilityTheory.Kernel T' G} {μ : MeasureTheory.Measure T} {ν : MeasureTheory.Measure T'} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] [ProbabilityTheory.FiniteSupport μ] [ProbabilityTheory.FiniteSupport ν] : dk[κ ; μ # η ; ν] = ∫ (x : T × T'), (fun (p : T × T') => Hm[MeasureTheory.Measure.map (fun (x : G × G) => x.1 - x.2) ((κ p.1).prod (η p.2))]) x ∂μ.prod ν - Hk[κ , μ] / 2 - Hk[η , ν] / 2

theorem ProbabilityTheory.Kernel.rdist_eq' {T : Type u_1} {T' : Type u_2} {G : Type u_4} [MeasurableSpace T] [MeasurableSpace T'] [MeasurableSpace G] [AddCommGroup G] [Countable T] [MeasurableSingletonClass T] [Countable T'] [MeasurableSingletonClass T'] [MeasurableSingletonClass G] [Countable G] {κ : ProbabilityTheory.Kernel T G} {η : ProbabilityTheory.Kernel T' G} [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] {μ : MeasureTheory.Measure T} {ν : MeasureTheory.Measure T'} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] [ProbabilityTheory.FiniteSupport μ] [ProbabilityTheory.FiniteSupport ν] : dk[κ ; μ # η ; ν] = Hk[((ProbabilityTheory.Kernel.prodMkRight T' κ).prod (ProbabilityTheory.Kernel.prodMkLeft T η)).map fun (x : G × G) => x.1 - x.2 , μ.prod ν] - Hk[κ , μ] / 2 - Hk[η , ν] / 2

theorem ProbabilityTheory.Kernel.rdist_symm {T : Type u_1} {T' : Type u_2} {G : Type u_4} [MeasurableSpace T] [MeasurableSpace T'] [MeasurableSpace G] [AddCommGroup G] [Countable T] [MeasurableSingletonClass T] [Countable T'] [MeasurableSingletonClass T'] [MeasurableSingletonClass G] [Countable G] {κ : ProbabilityTheory.Kernel T G} {η : ProbabilityTheory.Kernel T' G} [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] {μ : MeasureTheory.Measure T} {ν : MeasureTheory.Measure T'} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] [ProbabilityTheory.FiniteSupport μ] [ProbabilityTheory.FiniteSupport ν] : dk[κ ; μ # η ; ν] = dk[η ; ν # κ ; μ]

@[simp]

theorem ProbabilityTheory.Kernel.rdist_zero_kernel_right {T : Type u_1} {T' : Type u_2} {G : Type u_4} [MeasurableSpace T] [MeasurableSpace T'] [MeasurableSpace G] [AddCommGroup G] [Countable T] [MeasurableSingletonClass T] [Countable T'] [MeasurableSingletonClass T'] [MeasurableSingletonClass G] [Countable G] {κ : ProbabilityTheory.Kernel T G} [ProbabilityTheory.IsFiniteKernel κ] {μ : MeasureTheory.Measure T} {ν : MeasureTheory.Measure T'} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] [ProbabilityTheory.FiniteSupport μ] [ProbabilityTheory.FiniteSupport ν] : dk[κ ; μ # 0 ; ν] = -Hk[κ , μ] / 2

@[simp]

theorem ProbabilityTheory.Kernel.rdist_zero_kernel_left {T : Type u_1} {T' : Type u_2} {G : Type u_4} [MeasurableSpace T] [MeasurableSpace T'] [MeasurableSpace G] [AddCommGroup G] [Countable T] [MeasurableSingletonClass T] [Countable T'] [MeasurableSingletonClass T'] [MeasurableSingletonClass G] [Countable G] {η : ProbabilityTheory.Kernel T' G} [ProbabilityTheory.IsFiniteKernel η] {μ : MeasureTheory.Measure T} {ν : MeasureTheory.Measure T'} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] [ProbabilityTheory.FiniteSupport μ] [ProbabilityTheory.FiniteSupport ν] : dk[0 ; μ # η ; ν] = -Hk[η , ν] / 2

@[simp]

theorem ProbabilityTheory.Kernel.rdist_dirac_zero_right {T : Type u_1} {T' : Type u_2} {G : Type u_4} [MeasurableSpace T] [MeasurableSpace T'] [MeasurableSpace G] [AddCommGroup G] [Countable T] [MeasurableSingletonClass T] [Countable T'] [MeasurableSingletonClass T'] [MeasurableSingletonClass G] [Countable G] {κ : ProbabilityTheory.Kernel T G} [ProbabilityTheory.IsFiniteKernel κ] {μ : MeasureTheory.Measure T} {ν : MeasureTheory.Measure T'} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] [ProbabilityTheory.FiniteSupport μ] [ProbabilityTheory.FiniteSupport ν] : dk[κ ; μ # ProbabilityTheory.Kernel.const T' (MeasureTheory.Measure.dirac 0) ; ν] = Hk[κ , μ] / 2

@[simp]

theorem ProbabilityTheory.Kernel.rdist_dirac_zero_left {T : Type u_1} {T' : Type u_2} {G : Type u_4} [MeasurableSpace T] [MeasurableSpace T'] [MeasurableSpace G] [AddCommGroup G] [Countable T] [MeasurableSingletonClass T] [Countable T'] [MeasurableSingletonClass T'] [MeasurableSingletonClass G] [Countable G] {η : ProbabilityTheory.Kernel T' G} [ProbabilityTheory.IsFiniteKernel η] {μ : MeasureTheory.Measure T} {ν : MeasureTheory.Measure T'} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] [ProbabilityTheory.FiniteSupport μ] [ProbabilityTheory.FiniteSupport ν] : dk[ProbabilityTheory.Kernel.const T (MeasureTheory.Measure.dirac 0) ; μ # η ; ν] = Hk[η , ν] / 2

theorem ProbabilityTheory.Kernel.ruzsa_triangle_aux {G : Type u_4} [MeasurableSpace G] [AddCommGroup G] [MeasurableSingletonClass G] [Countable G] {T : Type u_5} [MeasurableSpace T] (κ : ProbabilityTheory.Kernel T (G × G)) (η : ProbabilityTheory.Kernel T G) [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η] : ((κ.prod η).map fun (p : (G × G) × G) => p.2 - p.1.2) = (η.prod κ.snd).map fun (p : G × G) => p.1 - p.2

theorem ProbabilityTheory.Kernel.abs_sub_entropy_le_rdist {T : Type u_1} {T' : Type u_2} {G : Type u_4} [MeasurableSpace T] [MeasurableSpace T'] [MeasurableSpace G] [AddCommGroup G] [Countable T] [MeasurableSingletonClass T] [Countable T'] [MeasurableSingletonClass T'] [MeasurableSingletonClass G] [Countable G] {κ : ProbabilityTheory.Kernel T G} {η : ProbabilityTheory.Kernel T' G} [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η] {μ : MeasureTheory.Measure T} {ν : MeasureTheory.Measure T'} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] [ProbabilityTheory.FiniteSupport μ] [ProbabilityTheory.FiniteSupport ν] (hκ : κ.AEFiniteKernelSupport μ) (hη : η.AEFiniteKernelSupport ν) : |Hk[κ , μ] - Hk[η , ν]| ≤ 2 * dk[κ ; μ # η ; ν]

theorem ProbabilityTheory.Kernel.rdist_nonneg {T : Type u_1} {T' : Type u_2} {G : Type u_4} [MeasurableSpace T] [MeasurableSpace T'] [MeasurableSpace G] [AddCommGroup G] [Countable T] [MeasurableSingletonClass T] [Countable T'] [MeasurableSingletonClass T'] [MeasurableSingletonClass G] [Countable G] {κ : ProbabilityTheory.Kernel T G} {η : ProbabilityTheory.Kernel T' G} [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η] {μ : MeasureTheory.Measure T} {ν : MeasureTheory.Measure T'} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] [ProbabilityTheory.FiniteSupport μ] [ProbabilityTheory.FiniteSupport ν] (hκ : κ.AEFiniteKernelSupport μ) (hη : η.AEFiniteKernelSupport ν) : 0 ≤ dk[κ ; μ # η ; ν]

theorem ProbabilityTheory.Kernel.ent_of_diff_le {T : Type u_1} {G : Type u_4} [MeasurableSpace T] [MeasurableSpace G] [AddCommGroup G] [Countable T] [MeasurableSingletonClass T] [MeasurableSingletonClass G] [Countable G] (κ : ProbabilityTheory.Kernel T (G × G)) (η : ProbabilityTheory.Kernel T G) [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η] (μ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.FiniteSupport μ] (hκ : κ.FiniteKernelSupport) (hη : η.FiniteKernelSupport) : Hk[κ.map fun (p : G × G) => p.1 - p.2 , μ] ≤ Hk[(κ.fst.prod η).map fun (p : G × G) => p.1 - p.2 , μ] + Hk[(η.prod κ.snd).map fun (p : G × G) => p.1 - p.2 , μ] - Hk[η , μ]

The improved entropic Ruzsa triangle inequality.

theorem ProbabilityTheory.Kernel.rdist_triangle_aux1 {T : Type u_1} {T' : Type u_2} {T'' : Type u_3} {G : Type u_4} [MeasurableSpace T] [MeasurableSpace T'] [MeasurableSpace T''] [MeasurableSpace G] [AddCommGroup G] [MeasurableSingletonClass T] [MeasurableSingletonClass T'] [MeasurableSingletonClass T''] [MeasurableSingletonClass G] [Countable G] (κ : ProbabilityTheory.Kernel T G) (η : ProbabilityTheory.Kernel T' G) [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η] (μ : MeasureTheory.Measure T) (μ' : MeasureTheory.Measure T') (μ'' : MeasureTheory.Measure T'') [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] [MeasureTheory.IsProbabilityMeasure μ''] [ProbabilityTheory.FiniteSupport μ] [ProbabilityTheory.FiniteSupport μ'] [ProbabilityTheory.FiniteSupport μ''] : Hk[((ProbabilityTheory.Kernel.prodMkRight T' (ProbabilityTheory.Kernel.prodMkRight T'' κ)).prod (ProbabilityTheory.Kernel.prodMkLeft (T × T'') η)).map fun (p : G × G) => p.1 - p.2 , (μ.prod μ'').prod μ'] = Hk[((ProbabilityTheory.Kernel.prodMkRight T' κ).prod (ProbabilityTheory.Kernel.prodMkLeft T η)).map fun (x : G × G) => x.1 - x.2 , μ.prod μ']

theorem ProbabilityTheory.Kernel.rdist_triangle_aux2 {T : Type u_1} {T' : Type u_2} {T'' : Type u_3} {G : Type u_4} [MeasurableSpace T] [MeasurableSpace T'] [MeasurableSpace T''] [MeasurableSpace G] [AddCommGroup G] [MeasurableSingletonClass T] [MeasurableSingletonClass T'] [MeasurableSingletonClass T''] [MeasurableSingletonClass G] [Countable G] (η : ProbabilityTheory.Kernel T' G) (ξ : ProbabilityTheory.Kernel T'' G) [ProbabilityTheory.IsMarkovKernel η] [ProbabilityTheory.IsMarkovKernel ξ] (μ : MeasureTheory.Measure T) (μ' : MeasureTheory.Measure T') (μ'' : MeasureTheory.Measure T'') [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] [MeasureTheory.IsProbabilityMeasure μ''] [ProbabilityTheory.FiniteSupport μ] [ProbabilityTheory.FiniteSupport μ'] [ProbabilityTheory.FiniteSupport μ''] : Hk[((ProbabilityTheory.Kernel.prodMkLeft (T × T'') η).prod (ProbabilityTheory.Kernel.prodMkRight T' (ProbabilityTheory.Kernel.prodMkLeft T ξ))).map fun (p : G × G) => p.1 - p.2 , (μ.prod μ'').prod μ'] = Hk[((ProbabilityTheory.Kernel.prodMkRight T'' η).prod (ProbabilityTheory.Kernel.prodMkLeft T' ξ)).map fun (x : G × G) => x.1 - x.2 , μ'.prod μ'']

theorem ProbabilityTheory.Kernel.rdist_triangle {T : Type u_1} {T' : Type u_2} {T'' : Type u_3} {G : Type u_4} [MeasurableSpace T] [MeasurableSpace T'] [MeasurableSpace T''] [MeasurableSpace G] [AddCommGroup G] [MeasurableSingletonClass T] [MeasurableSingletonClass T'] [MeasurableSingletonClass T''] [MeasurableSingletonClass G] [Countable G] [Countable T] [Countable T'] [Countable T''] (κ : ProbabilityTheory.Kernel T G) (η : ProbabilityTheory.Kernel T' G) (ξ : ProbabilityTheory.Kernel T'' G) [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η] [ProbabilityTheory.IsMarkovKernel ξ] (μ : MeasureTheory.Measure T) (μ' : MeasureTheory.Measure T') (μ'' : MeasureTheory.Measure T'') [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] [MeasureTheory.IsProbabilityMeasure μ''] [ProbabilityTheory.FiniteSupport μ] [ProbabilityTheory.FiniteSupport μ'] [ProbabilityTheory.FiniteSupport μ''] (hκ : κ.FiniteKernelSupport) (hη : η.FiniteKernelSupport) (hξ : ξ.FiniteKernelSupport) : dk[κ ; μ # ξ ; μ''] ≤ dk[κ ; μ # η ; μ'] + dk[η ; μ' # ξ ; μ'']