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
Instances For
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 ν
Instances For
Pretty printer defined by notation3 command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
theorem
ProbabilityTheory.kernel.rdist_eq
{T : Type u_1}
{T' : Type u_2}
{G : Type u_4}
[Countable T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Countable T']
[MeasurableSpace T']
[MeasurableSingletonClass T']
[MeasurableSpace G]
[AddCommGroup G]
{κ : ↥(ProbabilityTheory.kernel T G)}
{η : ↥(ProbabilityTheory.kernel T' G)}
{μ : MeasureTheory.Measure T}
{ν : MeasureTheory.Measure T'}
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsProbabilityMeasure ν]
[ProbabilityTheory.FiniteSupport μ]
[ProbabilityTheory.FiniteSupport ν]
:
theorem
ProbabilityTheory.kernel.rdist_eq'
{T : Type u_1}
{T' : Type u_2}
{G : Type u_4}
[Countable T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Countable T']
[MeasurableSpace T']
[MeasurableSingletonClass T']
[MeasurableSpace G]
[AddCommGroup G]
[MeasurableSub₂ 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.map
(ProbabilityTheory.kernel.prod (ProbabilityTheory.kernel.prodMkRight T' κ)
(ProbabilityTheory.kernel.prodMkLeft T η))
(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}
[Countable T]
[Nonempty T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Countable T']
[MeasurableSpace T']
[MeasurableSingletonClass T']
[Countable G]
[MeasurableSpace G]
[MeasurableSingletonClass G]
[AddCommGroup G]
[MeasurableSub₂ 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_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
@[simp]
theorem
ProbabilityTheory.kernel.rdist_zero_kernel_right
{T : Type u_1}
{T' : Type u_2}
{G : Type u_4}
[Countable T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Countable T']
[MeasurableSpace T']
[MeasurableSingletonClass T']
[MeasurableSpace G]
[AddCommGroup G]
[MeasurableSub₂ G]
{κ : ↥(ProbabilityTheory.kernel T G)}
[ProbabilityTheory.IsFiniteKernel κ]
{μ : MeasureTheory.Measure T}
{ν : MeasureTheory.Measure T'}
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsProbabilityMeasure ν]
[ProbabilityTheory.FiniteSupport μ]
[ProbabilityTheory.FiniteSupport ν]
:
@[simp]
theorem
ProbabilityTheory.kernel.rdist_zero_kernel_left
{T : Type u_1}
{T' : Type u_2}
{G : Type u_4}
[Countable T]
[Nonempty T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Countable T']
[MeasurableSpace T']
[MeasurableSingletonClass T']
[Countable G]
[MeasurableSpace G]
[MeasurableSingletonClass G]
[AddCommGroup G]
[MeasurableSub₂ G]
{η : ↥(ProbabilityTheory.kernel T' G)}
[ProbabilityTheory.IsFiniteKernel η]
{μ : MeasureTheory.Measure T}
{ν : MeasureTheory.Measure T'}
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsProbabilityMeasure ν]
[ProbabilityTheory.FiniteSupport μ]
[ProbabilityTheory.FiniteSupport ν]
:
@[simp]
theorem
ProbabilityTheory.kernel.rdist_dirac_zero_right
{T : Type u_1}
{T' : Type u_2}
{G : Type u_4}
[Countable T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Countable T']
[Nonempty T']
[MeasurableSpace T']
[MeasurableSingletonClass T']
[MeasurableSpace G]
[MeasurableSingletonClass G]
[AddCommGroup G]
[MeasurableSub₂ 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}
[Countable T]
[Nonempty T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Countable T']
[MeasurableSpace T']
[MeasurableSingletonClass T']
[Countable G]
[MeasurableSpace G]
[MeasurableSingletonClass G]
[AddCommGroup G]
[MeasurableSub₂ 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
{T : Type u_1}
{G : Type u_4}
[MeasurableSpace T]
[Countable G]
[MeasurableSpace G]
[MeasurableSingletonClass G]
[AddCommGroup G]
(κ : ↥(ProbabilityTheory.kernel T (G × G)))
(η : ↥(ProbabilityTheory.kernel T G))
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
:
ProbabilityTheory.kernel.map (ProbabilityTheory.kernel.prod κ η) (fun (p : (G × G) × G) => p.2 - p.1.2) ⋯ = ProbabilityTheory.kernel.map (ProbabilityTheory.kernel.prod η (ProbabilityTheory.kernel.snd κ))
(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}
[Countable T]
[Nonempty T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Countable T']
[Nonempty T']
[MeasurableSpace T']
[MeasurableSingletonClass T']
[Countable G]
[Nonempty G]
[MeasurableSpace G]
[MeasurableSingletonClass G]
[AddCommGroup G]
[MeasurableSub₂ 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κ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ)
(hη : ProbabilityTheory.kernel.AEFiniteKernelSupport η ν)
:
theorem
ProbabilityTheory.kernel.rdist_nonneg
{T : Type u_1}
{T' : Type u_2}
{G : Type u_4}
[Countable T]
[Nonempty T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Countable T']
[Nonempty T']
[MeasurableSpace T']
[MeasurableSingletonClass T']
[Countable G]
[Nonempty G]
[MeasurableSpace G]
[MeasurableSingletonClass G]
[AddCommGroup G]
[MeasurableSub₂ 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κ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ)
(hη : ProbabilityTheory.kernel.AEFiniteKernelSupport η ν)
:
0 ≤ dk[κ ; μ # η ; ν]
theorem
ProbabilityTheory.kernel.ent_of_diff_le
{T : Type u_1}
{G : Type u_4}
[Countable T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Countable G]
[Nonempty G]
[MeasurableSpace G]
[MeasurableSingletonClass G]
[AddCommGroup G]
[MeasurableSub₂ G]
(κ : ↥(ProbabilityTheory.kernel T (G × G)))
(η : ↥(ProbabilityTheory.kernel T G))
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
(μ : MeasureTheory.Measure T)
[MeasureTheory.IsProbabilityMeasure μ]
[ProbabilityTheory.FiniteSupport μ]
(hκ : ProbabilityTheory.kernel.FiniteKernelSupport κ)
(hη : ProbabilityTheory.kernel.FiniteKernelSupport η)
:
Hk[ProbabilityTheory.kernel.map κ (fun (p : G × G) => p.1 - p.2) ⋯ , μ] ≤ Hk[ProbabilityTheory.kernel.map (ProbabilityTheory.kernel.prod (ProbabilityTheory.kernel.fst κ) η)
(fun (p : G × G) => p.1 - p.2) ⋯ ,
μ] + Hk[ProbabilityTheory.kernel.map (ProbabilityTheory.kernel.prod η (ProbabilityTheory.kernel.snd κ))
(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]
[MeasurableSingletonClass T]
[MeasurableSpace T']
[MeasurableSingletonClass T']
[MeasurableSpace T'']
[MeasurableSingletonClass T'']
[MeasurableSpace G]
[AddCommGroup G]
[MeasurableSub₂ 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.map
(ProbabilityTheory.kernel.prod
(ProbabilityTheory.kernel.prodMkRight T' (ProbabilityTheory.kernel.prodMkRight T'' κ))
(ProbabilityTheory.kernel.prodMkLeft (T × T'') η))
(fun (p : G × G) => p.1 - p.2) ⋯ ,
(μ.prod μ'').prod μ'] = Hk[ProbabilityTheory.kernel.map
(ProbabilityTheory.kernel.prod (ProbabilityTheory.kernel.prodMkRight T' κ)
(ProbabilityTheory.kernel.prodMkLeft T η))
(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]
[MeasurableSingletonClass T]
[MeasurableSpace T']
[MeasurableSingletonClass T']
[MeasurableSpace T'']
[MeasurableSingletonClass T'']
[MeasurableSpace G]
[AddCommGroup G]
[MeasurableSub₂ 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.map
(ProbabilityTheory.kernel.prod (ProbabilityTheory.kernel.prodMkLeft (T × T'') η)
(ProbabilityTheory.kernel.prodMkRight T' (ProbabilityTheory.kernel.prodMkLeft T ξ)))
(fun (p : G × G) => p.1 - p.2) ⋯ ,
(μ.prod μ'').prod μ'] = Hk[ProbabilityTheory.kernel.map
(ProbabilityTheory.kernel.prod (ProbabilityTheory.kernel.prodMkRight T'' η)
(ProbabilityTheory.kernel.prodMkLeft T' ξ))
(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}
[Countable T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
[Countable T']
[Nonempty T']
[MeasurableSpace T']
[MeasurableSingletonClass T']
[Countable T'']
[MeasurableSpace T'']
[MeasurableSingletonClass T'']
[Countable G]
[Nonempty G]
[MeasurableSpace G]
[MeasurableSingletonClass G]
[AddCommGroup G]
[MeasurableSub₂ G]
(κ : ↥(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κ : ProbabilityTheory.kernel.FiniteKernelSupport κ)
(hη : ProbabilityTheory.kernel.FiniteKernelSupport η)
(hξ : ProbabilityTheory.kernel.FiniteKernelSupport ξ)
: