Ruzsa distance

Here we define Ruzsa distance and establish its basic properties.

Main definitions

• rdist: The Ruzsa distance $d[X ; Y]$ between two random variables
• condRuzsaDist: The conditional Ruzsa distance $d[X | Z ; Y | W]$ (or $d[X ; Y | W]$) between two random variables, conditioned on additional random variables

Main results

• rdist_triangle: The Ruzsa triangle inequality for three random variables.
• kaimanovich_vershik. $$H[X + Y + Z] - H[X + Y] \leq H[Y+ Z] - H[Y]$$
• ent_bsg: If $Z=A+B$, then $$\sum_{z} P[Z=z] d[(A | Z = z) ; (B | Z = z)] \leq 3 I[A :B] + 2 H[Z] - H[A] - H[B]$$

theorem continuous_measureEntropy_probabilityMeasure {Ω : Type u_8} [Fintype Ω] [TopologicalSpace Ω] [DiscreteTopology Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] : Continuous fun (μ : MeasureTheory.ProbabilityMeasure Ω) => Hm[↑μ]

Entropy depends continuously on the measure.

theorem continuous_entropy_restrict_probabilityMeasure {G : Type u_5} [hG : MeasurableSpace G] [Fintype G] [TopologicalSpace G] [DiscreteTopology G] [BorelSpace G] : Continuous fun (μ : MeasureTheory.ProbabilityMeasure G) => H[id ; ↑μ]

noncomputable def rdist {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω'] [hG : MeasurableSpace G] [AddCommGroup G] (X : Ω → G) (Y : Ω' → G) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) (μ' : autoParam (MeasureTheory.Measure Ω') _auto✝) : ℝ

The Ruzsa distance rdist X Y or d[X ; Y] between two random variables is defined as H[X'- Y'] - H[X']/2 - H[Y']/2, where X', Y' are independent copies of X, Y.

Equations

• d[X ; μ # Y ; μ'] = H[fun (x : G × G) => x.1 - x.2 ; (MeasureTheory.Measure.map X μ).prod (MeasureTheory.Measure.map Y μ')] - H[X ; μ] / 2 - H[Y ; μ'] / 2

def «termD[_;_#_;_]» : Lean.ParserDescr

The Ruzsa distance rdist X Y or d[X ; Y] between two random variables is defined as H[X'- Y'] - H[X']/2 - H[Y']/2, where X', Y' are independent copies of X, Y.

Equations

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

def «termD[_;_#_;_]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

def «termD[_#_]» : Lean.ParserDescr

The Ruzsa distance rdist X Y or d[X ; Y] between two random variables is defined as H[X'- Y'] - H[X']/2 - H[Y']/2, where X', Y' are independent copies of X, Y.

Equations

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

def «termD[_#_]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

theorem rdist_def {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω'] [hG : MeasurableSpace G] [AddCommGroup G] (X : Ω → G) (Y : Ω' → G) (μ : MeasureTheory.Measure Ω) (μ' : MeasureTheory.Measure Ω') : d[X ; μ # Y ; μ'] = H[fun (x : G × G) => x.1 - x.2 ; (MeasureTheory.Measure.map X μ).prod (MeasureTheory.Measure.map Y μ')] - H[X ; μ] / 2 - H[Y ; μ'] / 2

Explicit formula for the Ruzsa distance.

theorem rdist_eq_rdistm {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [hG : MeasurableSpace G] [AddCommGroup G] {X : Ω → G} {Y : Ω' → G} : d[X ; μ # Y ; μ'] = ProbabilityTheory.Kernel.rdistm (MeasureTheory.Measure.map X μ) (MeasureTheory.Measure.map Y μ')

Ruzsa distance of random variables equals Ruzsa distance of the kernels.

theorem continuous_rdist_restrict_probabilityMeasure {G : Type u_5} [hG : MeasurableSpace G] [AddCommGroup G] [Fintype G] [TopologicalSpace G] [DiscreteTopology G] [BorelSpace G] : Continuous fun (μ : MeasureTheory.ProbabilityMeasure G × MeasureTheory.ProbabilityMeasure G) => d[id ; ↑μ.1 # id ; ↑μ.2]

Ruzsa distance depends continuously on the measure.

theorem continuous_rdist_restrict_probabilityMeasure₁ {Ω : Type u_1} {G : Type u_5} [mΩ : MeasurableSpace Ω] [hG : MeasurableSpace G] [AddCommGroup G] [Fintype G] [TopologicalSpace G] [DiscreteTopology G] [BorelSpace G] (X : Ω → G) (P : autoParam (MeasureTheory.Measure Ω) _auto✝) [MeasureTheory.IsProbabilityMeasure P] (X_mble : Measurable X) : Continuous fun (μ : MeasureTheory.ProbabilityMeasure G) => d[id ; MeasureTheory.Measure.map X P # id ; ↑μ]

theorem rdist_eq_rdist_id_map {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [hG : MeasurableSpace G] [AddCommGroup G] {X : Ω → G} {Y : Ω' → G} : d[X ; μ # Y ; μ'] = d[id ; MeasureTheory.Measure.map X μ # id ; MeasureTheory.Measure.map Y μ']

Ruzsa distance between random variables equals Ruzsa distance between their distributions.

theorem continuous_rdist_restrict_probabilityMeasure₁' {Ω : Type u_1} {G : Type u_5} [mΩ : MeasurableSpace Ω] [hG : MeasurableSpace G] [AddCommGroup G] [Fintype G] [TopologicalSpace G] [DiscreteTopology G] [BorelSpace G] (X : Ω → G) (P : autoParam (MeasureTheory.Measure Ω) _auto✝) [MeasureTheory.IsProbabilityMeasure P] (X_mble : Measurable X) : Continuous fun (μ : MeasureTheory.ProbabilityMeasure G) => d[X ; P # id ; ↑μ]

Ruzsa distance depends continuously on the second measure.

theorem ProbabilityTheory.IdentDistrib.rdist_eq {Ω : Type u_1} {Ω' : Type u_2} {Ω'' : Type u_3} {Ω''' : Type u_4} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [mΩ'' : MeasurableSpace Ω''] {μ'' : MeasureTheory.Measure Ω''} [mΩ''' : MeasurableSpace Ω'''] {μ''' : MeasureTheory.Measure Ω'''} [hG : MeasurableSpace G] [AddCommGroup G] {X : Ω → G} {Y : Ω' → G} {X' : Ω'' → G} {Y' : Ω''' → G} (hX : ProbabilityTheory.IdentDistrib X X' μ μ'') (hY : ProbabilityTheory.IdentDistrib Y Y' μ' μ''') : d[X ; μ # Y ; μ'] = d[X' ; μ'' # Y' ; μ''']

If X', Y' are copies of X, Y respectively then d[X' ; Y'] = d[X ; Y].

theorem tendsto_rdist_probabilityMeasure {Ω : Type u_1} {G : Type u_5} [mΩ : MeasurableSpace Ω] [hG : MeasurableSpace G] [AddCommGroup G] {α : Type u_8} {l : Filter α} [TopologicalSpace Ω] [BorelSpace Ω] [TopologicalSpace G] [BorelSpace G] [Fintype G] [DiscreteTopology G] {X : Ω → G} {Y : Ω → G} (hX : Continuous X) (hY : Continuous Y) {μ : α → MeasureTheory.ProbabilityMeasure Ω} {ν : MeasureTheory.ProbabilityMeasure Ω} (hμ : Filter.Tendsto μ l (nhds ν)) : Filter.Tendsto (fun (n : α) => d[X ; ↑(μ n) # Y ; ↑(μ n)]) l (nhds d[X ; ↑ν # Y ; ↑ν])

theorem ProbabilityTheory.IndepFun.rdist_eq {Ω : Type u_1} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [hG : MeasurableSpace G] [AddCommGroup G] {X : Ω → G} [Countable G] [MeasurableSingletonClass G] [MeasureTheory.IsFiniteMeasure μ] {Y : Ω → G} (h : ProbabilityTheory.IndepFun X Y μ) (hX : Measurable X) (hY : Measurable Y) : d[X ; μ # Y ; μ] = H[X - Y ; μ] - H[X ; μ] / 2 - H[Y ; μ] / 2

If X, Y are independent G-random variables then d[X ; Y] = H[X - Y] - H[X]/2 - H[Y]/2.

theorem rdist_le_avg_ent {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω'] [hG : MeasurableSpace G] [AddCommGroup G] [Countable G] [MeasurableSingletonClass G] {X : Ω → G} {Y : Ω' → G} [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) (μ' : autoParam (MeasureTheory.Measure Ω') _auto✝) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] : d[X ; μ # Y ; μ'] ≤ (H[X ; μ] + H[Y ; μ']) / 2

d[X ; Y] ≤ H[X]/2 + H[Y]/2.

theorem rdist_of_inj {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [hG : MeasurableSpace G] [AddCommGroup G] {X : Ω → G} {Y : Ω' → G} [Countable G] [MeasurableSingletonClass G] {H : Type u_8} [hH : MeasurableSpace H] [MeasurableSingletonClass H] [AddCommGroup H] [Countable H] (hX : Measurable X) (hY : Measurable Y) (φ : G →+ H) (hφ : Function.Injective ⇑φ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] : d[⇑φ ∘ X ; μ # ⇑φ ∘ Y ; μ'] = d[X ; μ # Y ; μ']

Applying an injective homomorphism does not affect Ruzsa distance.

theorem rdist_zero_eq_half_ent {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [hG : MeasurableSpace G] [AddCommGroup G] {X : Ω → G} [Countable G] [MeasurableSingletonClass G] [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] : d[X ; μ # fun (x : Ω') => 0 ; μ'] = H[X ; μ] / 2

d[X ; 0] = H[X] / 2.

theorem rdist_symm {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [hG : MeasurableSpace G] [AddCommGroup G] {X : Ω → G} {Y : Ω' → G} [Countable G] [MeasurableSingletonClass G] [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure μ'] : d[X ; μ # Y ; μ'] = d[Y ; μ' # X ; μ]

d[X ; Y] = d[Y ; X]

theorem diff_ent_le_rdist {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [hG : MeasurableSpace G] [AddCommGroup G] {X : Ω → G} {Y : Ω' → G} [Countable G] [MeasurableSingletonClass G] [FiniteRange X] [FiniteRange Y] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] (hX : Measurable X) (hY : Measurable Y) : |H[X ; μ] - H[Y ; μ']| ≤ 2 * d[X ; μ # Y ; μ']

|H[X] - H[Y]| ≤ 2 d[X ; Y].

theorem diff_ent_le_rdist' {Ω : Type u_1} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [hG : MeasurableSpace G] [AddCommGroup G] {X : Ω → G} [Countable G] [MeasurableSingletonClass G] [FiniteRange X] [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) (h : ProbabilityTheory.IndepFun X Y μ) [FiniteRange Y] : H[X - Y ; μ] - H[X ; μ] ≤ 2 * d[X ; μ # Y ; μ]

H[X - Y] - H[X] ≤ 2d[X ; Y].

theorem diff_ent_le_rdist'' {Ω : Type u_1} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [hG : MeasurableSpace G] [AddCommGroup G] {X : Ω → G} [Countable G] [MeasurableSingletonClass G] [FiniteRange X] [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) (h : ProbabilityTheory.IndepFun X Y μ) [FiniteRange Y] : H[X - Y ; μ] - H[Y ; μ] ≤ 2 * d[X ; μ # Y ; μ]

H[X - Y] - H[Y] ≤ 2d[X ; Y].

theorem rdist_nonneg {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [hG : MeasurableSpace G] [AddCommGroup G] {X : Ω → G} {Y : Ω' → G} [Countable G] [MeasurableSingletonClass G] [FiniteRange X] [FiniteRange Y] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] (hX : Measurable X) (hY : Measurable Y) : 0 ≤ d[X ; μ # Y ; μ']

d[X ; Y] ≥ 0.

theorem ent_of_proj_le {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [hG : MeasurableSpace G] [AddCommGroup G] {X : Ω → G} [Countable G] [MeasurableSingletonClass G] [FiniteRange X] {UH : Ω' → G} [FiniteRange UH] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] (hX : Measurable X) (hU : Measurable UH) {H : AddSubgroup G} (hH : (↑H).Finite) (hunif : ProbabilityTheory.IsUniform (↑H) UH μ') : H[⇑(QuotientAddGroup.mk' H) ∘ X ; μ] ≤ 2 * d[X ; μ # UH ; μ']

If $G$ is an additive group and $X$ is a $G$-valued random variable and $H\leq G$ is a finite subgroup then, with $\pi:G\to G/H$ the natural homomorphism we have (where $U_H$ is uniform on $H$) $\mathbb{H}(\pi(X))\leq 2d[X;U_H].$

theorem rdist_add_const {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [hG : MeasurableSpace G] [AddCommGroup G] {X : Ω → G} {Y : Ω' → G} [Countable G] [MeasurableSingletonClass G] [FiniteRange X] [FiniteRange Y] [MeasureTheory.IsZeroOrProbabilityMeasure μ] [MeasureTheory.IsZeroOrProbabilityMeasure μ'] (hX : Measurable X) (hY : Measurable Y) {c : G} : d[X ; μ # Y + fun (x : Ω') => c ; μ'] = d[X ; μ # Y ; μ']

Adding a constant to a random variable does not change the Rusza distance.

theorem rdist_add_const' {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [hG : MeasurableSpace G] [AddCommGroup G] {X : Ω → G} {Y : Ω' → G} [Countable G] [MeasurableSingletonClass G] [FiniteRange X] [FiniteRange Y] [MeasureTheory.IsZeroOrProbabilityMeasure μ] [MeasureTheory.IsZeroOrProbabilityMeasure μ'] (c : G) (c' : G) (hX : Measurable X) (hY : Measurable Y) : d[X + fun (x : Ω) => c ; μ # Y + fun (x : Ω') => c' ; μ'] = d[X ; μ # Y ; μ']

A variant of rdist_add_const where one adds constants to both variables.

theorem ent_of_diff_le {Ω : Type u_1} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [hG : MeasurableSpace G] [AddCommGroup G] [Countable G] [MeasurableSingletonClass G] (X : Ω → G) (Y : Ω → G) (Z : Ω → G) (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (h : ProbabilityTheory.IndepFun (⟨X, Y⟩) Z μ) [MeasureTheory.IsProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] [FiniteRange Z] : H[X - Y ; μ] ≤ H[X - Z ; μ] + H[Z - Y ; μ] - H[Z ; μ]

The improved entropic Ruzsa triangle inequality.

theorem rdist_triangle {Ω : Type u_1} {Ω' : Type u_2} {Ω'' : Type u_3} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [mΩ'' : MeasurableSpace Ω''] {μ'' : MeasureTheory.Measure Ω''} [hG : MeasurableSpace G] [AddCommGroup G] [Countable G] [MeasurableSingletonClass G] {X : Ω → G} {Y : Ω' → G} {Z : Ω'' → G} (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) [hμ : MeasureTheory.IsProbabilityMeasure μ] [hμ' : MeasureTheory.IsProbabilityMeasure μ'] [hμ'' : MeasureTheory.IsProbabilityMeasure μ''] [FiniteRange X] [FiniteRange Y] [FiniteRange Z] : d[X ; μ # Z ; μ''] ≤ d[X ; μ # Y ; μ'] + d[Y ; μ' # Z ; μ'']

The entropic Ruzsa triangle inequality

noncomputable def condRuzsaDist {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} {S : Type u_6} {T : Type u_7} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω'] [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace S] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] (X : Ω → G) (Z : Ω → S) (Y : Ω' → G) (W : Ω' → T) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) [MeasureTheory.IsFiniteMeasure μ] (μ' : autoParam (MeasureTheory.Measure Ω') _auto✝) [MeasureTheory.IsFiniteMeasure μ'] : ℝ

The conditional Ruzsa distance d[X|Z ; Y|W].

Equations

• d[X | Z ; μ # Y | W ; μ'] = dk[ProbabilityTheory.condDistrib X Z μ ; MeasureTheory.Measure.map Z μ # ProbabilityTheory.condDistrib Y W μ' ; MeasureTheory.Measure.map W μ']

def «termD[_|_;_#_|_;_]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

def «termD[_|_;_#_|_;_]» : Lean.ParserDescr

The conditional Ruzsa distance d[X|Z ; Y|W].

Equations

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

def «termD[_|_#_|_]» : Lean.ParserDescr

The conditional Ruzsa distance d[X|Z ; Y|W].

Equations

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

def «termD[_|_#_|_]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

theorem condRuzsaDist_def {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} {S : Type u_6} {T : Type u_7} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω'] [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace S] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] (X : Ω → G) (Z : Ω → S) (Y : Ω' → G) (W : Ω' → T) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (μ' : MeasureTheory.Measure Ω') [MeasureTheory.IsFiniteMeasure μ'] : d[X | Z ; μ # Y | W ; μ'] = dk[ProbabilityTheory.condDistrib X Z μ ; MeasureTheory.Measure.map Z μ # ProbabilityTheory.condDistrib Y W μ' ; MeasureTheory.Measure.map W μ']

@[simp]

theorem condRuszaDist_zero_right {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} {S : Type u_6} {T : Type u_7} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω'] [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace S] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] (X : Ω → G) (Z : Ω → S) (Y : Ω' → G) (W : Ω' → T) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : d[X | Z ; μ # Y | W ; 0] = 0

@[simp]

theorem condRuszaDist_zero_left {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} {S : Type u_6} {T : Type u_7} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω'] [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace S] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] (X : Ω → G) (Z : Ω → S) (Y : Ω' → G) (W : Ω' → T) (μ' : MeasureTheory.Measure Ω') [MeasureTheory.IsFiniteMeasure μ'] : d[X | Z ; 0 # Y | W ; μ'] = 0

theorem condRuzsaDist_eq_sum' {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} {S : Type u_6} {T : Type u_7} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω'] [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace S] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] [MeasurableSingletonClass S] [MeasurableSingletonClass T] {X : Ω → G} {Z : Ω → S} {Y : Ω' → G} {W : Ω' → T} (hX : Measurable X) (hZ : Measurable Z) (hY : Measurable Y) (hW : Measurable W) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (μ' : MeasureTheory.Measure Ω') [MeasureTheory.IsFiniteMeasure μ'] [Fintype S] [Fintype T] : d[X | Z ; μ # Y | W ; μ'] = ∑ z : S, ∑ w : T, (μ (Z ⁻¹' {z})).toReal * (μ' (W ⁻¹' {w})).toReal * d[X ; ProbabilityTheory.cond μ (Z ⁻¹' {z}) # Y ; ProbabilityTheory.cond μ' (W ⁻¹' {w})]

Explicit formula for conditional Ruzsa distance $d[X|Z; Y|W]$ in a fintype.

theorem condRuzsaDist_eq_sum {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} {S : Type u_6} {T : Type u_7} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω'] [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace S] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] [MeasurableSingletonClass S] [MeasurableSingletonClass T] {X : Ω → G} {Z : Ω → S} {Y : Ω' → G} {W : Ω' → T} (hX : Measurable X) (hZ : Measurable Z) (hY : Measurable Y) (hW : Measurable W) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (μ' : MeasureTheory.Measure Ω') [MeasureTheory.IsFiniteMeasure μ'] [FiniteRange Z] [FiniteRange W] : d[X | Z ; μ # Y | W ; μ'] = ∑ z ∈ FiniteRange.toFinset Z, ∑ w ∈ FiniteRange.toFinset W, (μ (Z ⁻¹' {z})).toReal * (μ' (W ⁻¹' {w})).toReal * d[X ; ProbabilityTheory.cond μ (Z ⁻¹' {z}) # Y ; ProbabilityTheory.cond μ' (W ⁻¹' {w})]

Explicit formula for conditional Ruzsa distance $d[X|Z; Y|W]$.

theorem condRuzsaDist_symm {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} {S : Type u_6} {T : Type u_7} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace S] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable S] [Countable T] {X : Ω → G} {Z : Ω → S} {Y : Ω' → G} {W : Ω' → T} (hZ : Measurable Z) (hW : Measurable W) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] [FiniteRange Z] [FiniteRange W] : d[X | Z ; μ # Y | W ; μ'] = d[Y | W ; μ' # X | Z ; μ]

$$ d[X|Z; Y|W] = d[Y|W; X|Z]$$

theorem condRuzsaDist_nonneg {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} {S : Type u_6} {T : Type u_7} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace S] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable S] [Countable T] {X : Ω → G} (hX : Measurable X) [FiniteRange X] {Z : Ω → S} (hZ : Measurable Z) [FiniteRange Z] {Y : Ω' → G} (hY : Measurable Y) [FiniteRange Y] {W : Ω' → T} (hW : Measurable W) [FiniteRange W] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] : 0 ≤ d[X | Z ; μ # Y | W ; μ']

noncomputable def condRuzsaDist' {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} {T : Type u_7} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω'] [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] (X : Ω → G) (Y : Ω' → G) (W : Ω' → T) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) (μ' : autoParam (MeasureTheory.Measure Ω') _auto✝) [MeasureTheory.IsFiniteMeasure μ'] : ℝ

The conditional Ruzsa distance d[X ; Y|W].

Equations

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

def «termD[_;_#_|_;_]» : Lean.ParserDescr

The conditional Ruzsa distance d[X ; Y|W].

Equations

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

def «termD[_;_#_|_;_]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

def «termD[_#_|_]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

def «termD[_#_|_]» : Lean.ParserDescr

The conditional Ruzsa distance d[X ; Y|W].

Equations

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

theorem condRuzsaDist'_def {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω'] [hG : MeasurableSpace G] [AddCommGroup G] [Countable G] [MeasurableSingletonClass G] {T : Type u_8} [MeasurableSpace T] (X : Ω → G) (Y : Ω' → G) (W : Ω' → T) (μ : MeasureTheory.Measure Ω) (μ' : MeasureTheory.Measure Ω') [MeasureTheory.IsFiniteMeasure μ'] : d[X ; μ # Y | W ; μ'] = dk[ProbabilityTheory.Kernel.const Unit (MeasureTheory.Measure.map X μ) ; MeasureTheory.Measure.dirac () # ProbabilityTheory.condDistrib Y W μ' ; MeasureTheory.Measure.map W μ']

Conditional Ruzsa distance equals Ruzsa distance of associated kernels.

@[simp]

theorem condRuzsaDist'_zero_right {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω'] [hG : MeasurableSpace G] [AddCommGroup G] [Countable G] [MeasurableSingletonClass G] {T : Type u_8} [MeasurableSpace T] (X : Ω → G) (Y : Ω' → G) (W : Ω' → T) (μ : MeasureTheory.Measure Ω) : d[X ; μ # Y | W ; 0] = 0

theorem condRuzsaDist'_eq_sum {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} {T : Type u_7} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω'] [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] [MeasurableSingletonClass T] {X : Ω → G} {Y : Ω' → G} {W : Ω' → T} (hY : Measurable Y) (hW : Measurable W) (μ : MeasureTheory.Measure Ω) (μ' : MeasureTheory.Measure Ω') [MeasureTheory.IsFiniteMeasure μ'] [FiniteRange W] : d[X ; μ # Y | W ; μ'] = ∑ w ∈ FiniteRange.toFinset W, (μ' (W ⁻¹' {w})).toReal * d[X ; μ # Y ; ProbabilityTheory.cond μ' (W ⁻¹' {w})]

Explicit formula for conditional Ruzsa distance d[X ; Y | W].

theorem condRuzsaDist'_eq_sum' {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} {T : Type u_7} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω'] [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] [MeasurableSingletonClass T] {X : Ω → G} {Y : Ω' → G} {W : Ω' → T} (hY : Measurable Y) (hW : Measurable W) (μ : MeasureTheory.Measure Ω) (μ' : MeasureTheory.Measure Ω') [MeasureTheory.IsFiniteMeasure μ'] [Fintype T] : d[X ; μ # Y | W ; μ'] = ∑ w : T, (μ' (W ⁻¹' {w})).toReal * d[X ; μ # Y ; ProbabilityTheory.cond μ' (W ⁻¹' {w})]

Alternate formula for conditional Ruzsa distance d[X ; Y | W] when T is a Fintype.

theorem condRuzsaDist'_prod_eq_sum {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} {T : Type u_7} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω'] [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] [MeasurableSingletonClass T] {X : Ω → G} {Y : Ω' → G} {W : Ω' → T} {W' : Ω' → T} (μ : MeasureTheory.Measure Ω) (μ' : MeasureTheory.Measure Ω') (hY : Measurable Y) (hW' : Measurable W') (hW : Measurable W) [MeasureTheory.IsFiniteMeasure μ'] [FiniteRange W] [FiniteRange W'] : d[X ; μ # Y | ⟨W', W⟩ ; μ'] = ∑ w ∈ FiniteRange.toFinset W, (μ' (W ⁻¹' {w})).toReal * d[X ; μ # Y | W' ; ProbabilityTheory.cond μ' (W ⁻¹' {w})]

theorem condRuzsaDist'_prod_eq_sum' {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} {T : Type u_7} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω'] [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] [MeasurableSingletonClass T] {X : Ω → G} {Y : Ω' → G} {W : Ω' → T} {W' : Ω' → T} (μ : MeasureTheory.Measure Ω) (μ' : MeasureTheory.Measure Ω') (hY : Measurable Y) (hW' : Measurable W') (hW : Measurable W) [MeasureTheory.IsFiniteMeasure μ'] [Fintype T] : d[X ; μ # Y | ⟨W', W⟩ ; μ'] = ∑ w : T, (μ' (W ⁻¹' {w})).toReal * d[X ; μ # Y | W' ; ProbabilityTheory.cond μ' (W ⁻¹' {w})]

Version of condRuzsaDist'_prod_eq_sum when W has finite codomain.

theorem condRuzsaDist'_eq_integral {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} {T : Type u_7} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω'] [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] [MeasurableSingletonClass T] (X : Ω → G) {Y : Ω' → G} {W : Ω' → T} (hY : Measurable Y) (hW : Measurable W) (μ : MeasureTheory.Measure Ω) (μ' : MeasureTheory.Measure Ω') [MeasureTheory.IsFiniteMeasure μ'] [FiniteRange W] : d[X ; μ # Y | W ; μ'] = ∫ (x : T), (fun (w : T) => d[X ; μ # Y ; ProbabilityTheory.cond μ' (W ⁻¹' {w})]) x ∂MeasureTheory.Measure.map W μ'

Explicit formula for conditional Ruzsa distance d[X ; Y | W], in integral form.

theorem condRuzsaDist_of_const {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} {S : Type u_6} {T : Type u_7} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace S] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable S] [Countable T] {X : Ω → G} (hX : Measurable X) (Y : Ω' → G) (W : Ω' → T) (c : S) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] [FiniteRange W] : d[X | fun (x : Ω) => c ; μ # Y | W ; μ'] = d[X ; μ # Y | W ; μ']

Conditioning by a constant does not affect Ruzsa distance.

theorem condRuzsaDist_of_indep {Ω : Type u_1} {G : Type u_5} {S : Type u_6} {T : Type u_7} [mΩ : MeasurableSpace Ω] [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace S] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable S] [Countable T] {X : Ω → G} {Z : Ω → S} {Y : Ω → G} {W : Ω → T} (hX : Measurable X) (hZ : Measurable Z) (hY : Measurable Y) (hW : Measurable W) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (h : ProbabilityTheory.IndepFun (⟨X, Z⟩) (⟨Y, W⟩) μ) [FiniteRange Z] [FiniteRange W] : d[X | Z ; μ # Y | W ; μ] = H[X - Y | ⟨Z, W⟩ ; μ] - H[X | Z ; μ] / 2 - H[Y | W ; μ] / 2

If $(X,Z)$ and $(Y,W)$ are independent, then d[X | Z ; Y | W] = H[X'- Y' | Z', W'] - H[X'|Z']/2 - H[Y'|W']/2.

theorem condRuzsaDist'_of_indep {Ω : Type u_1} {G : Type u_5} {T : Type u_7} [mΩ : MeasurableSpace Ω] [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] [MeasurableSingletonClass T] [Countable T] {X : Ω → G} {Y : Ω → G} {W : Ω → T} (hX : Measurable X) (hY : Measurable Y) (hW : Measurable W) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (h : ProbabilityTheory.IndepFun X (⟨Y, W⟩) μ) [FiniteRange W] : d[X ; μ # Y | W ; μ] = H[X - Y | W ; μ] - H[X ; μ] / 2 - H[Y | W ; μ] / 2

Formula for conditional Ruzsa distance for independent sets of variables.

theorem condRuzsaDist_of_copy {Ω : Type u_1} {Ω' : Type u_2} {Ω'' : Type u_3} {Ω''' : Type u_4} {G : Type u_5} {S : Type u_6} {T : Type u_7} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [mΩ'' : MeasurableSpace Ω''] {μ'' : MeasureTheory.Measure Ω''} [mΩ''' : MeasurableSpace Ω'''] {μ''' : MeasureTheory.Measure Ω'''} [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace S] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] [MeasurableSingletonClass S] [MeasurableSingletonClass T] {X : Ω → G} (hX : Measurable X) {Z : Ω → S} (hZ : Measurable Z) {Y : Ω' → G} (hY : Measurable Y) {W : Ω' → T} (hW : Measurable W) {X' : Ω'' → G} (hX' : Measurable X') {Z' : Ω'' → S} (hZ' : Measurable Z') {Y' : Ω''' → G} (hY' : Measurable Y') {W' : Ω''' → T} (hW' : Measurable W') [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure μ'] [MeasureTheory.IsFiniteMeasure μ''] [MeasureTheory.IsFiniteMeasure μ'''] (h1 : ProbabilityTheory.IdentDistrib (⟨X, Z⟩) (⟨X', Z'⟩) μ μ'') (h2 : ProbabilityTheory.IdentDistrib (⟨Y, W⟩) (⟨Y', W'⟩) μ' μ''') [FiniteRange Z] [FiniteRange W] [FiniteRange Z'] [FiniteRange W'] : d[X | Z ; μ # Y | W ; μ'] = d[X' | Z' ; μ'' # Y' | W' ; μ''']

The conditional Ruzsa distance is unchanged if the sets of random variables are replaced with copies.

theorem condRuzsaDist'_of_copy {Ω : Type u_1} {Ω' : Type u_2} {Ω'' : Type u_3} {Ω''' : Type u_4} {G : Type u_5} {T : Type u_7} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [mΩ'' : MeasurableSpace Ω''] {μ'' : MeasureTheory.Measure Ω''} [mΩ''' : MeasurableSpace Ω'''] {μ''' : MeasureTheory.Measure Ω'''} [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] [MeasurableSingletonClass T] (X : Ω → G) {Y : Ω' → G} (hY : Measurable Y) {W : Ω' → T} (hW : Measurable W) (X' : Ω'' → G) {Y' : Ω''' → G} (hY' : Measurable Y') {W' : Ω''' → T} (hW' : Measurable W') [MeasureTheory.IsFiniteMeasure μ'] [MeasureTheory.IsFiniteMeasure μ'''] (h1 : ProbabilityTheory.IdentDistrib X X' μ μ'') (h2 : ProbabilityTheory.IdentDistrib (⟨Y, W⟩) (⟨Y', W'⟩) μ' μ''') [FiniteRange W] [FiniteRange W'] : d[X ; μ # Y | W ; μ'] = d[X' ; μ'' # Y' | W' ; μ''']

theorem condRuszaDist_prod_eq_of_indepFun {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} {T : Type u_7} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω'] [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] [MeasurableSingletonClass T] {μ : MeasureTheory.Measure Ω} {μ' : MeasureTheory.Measure Ω'} {X : Ω → G} {Y : Ω' → G} {W : Ω' → T} {W' : Ω' → T} (hX : Measurable X) (hY : Measurable Y) (hW : Measurable W) (hW' : Measurable W') (h : ProbabilityTheory.IndepFun (⟨Y, W⟩) W' μ') [MeasureTheory.IsProbabilityMeasure μ'] [Fintype T] : d[X ; μ # Y | ⟨W, W'⟩ ; μ'] = d[X ; μ # Y | W ; μ']

theorem condRuzsaDist_comp_right {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} {T : Type u_7} [mΩ : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [mΩ' : MeasurableSpace Ω'] (μ' : MeasureTheory.Measure Ω') [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] [MeasurableSingletonClass T] {T' : Type u_8} [Fintype T] [Fintype T'] [MeasurableSpace T'] [MeasurableSingletonClass T'] [MeasureTheory.IsFiniteMeasure μ'] (X : Ω → G) (Y : Ω' → G) (W : Ω' → T) (e : T → T') (hY : Measurable Y) (hW : Measurable W) (he : Measurable e) (h'e : Function.Injective e) : d[X ; μ # Y | e ∘ W ; μ'] = d[X ; μ # Y | W ; μ']

theorem condRuzsaDist_of_inj_map {Ω : Type u_1} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [hG : MeasurableSpace G] [AddCommGroup G] [Countable G] [MeasurableSingletonClass G] {G' : Type u_8} [Countable G'] [AddCommGroup G'] [MeasurableSpace G'] [MeasurableSingletonClass G'] [MeasureTheory.IsProbabilityMeasure μ] (Y : Fin 4 → Ω → G) (h_indep : ProbabilityTheory.IndepFun (⟨Y 0, Y 2⟩) (⟨Y 1, Y 3⟩) μ) (h_meas : ∀ (i : Fin 4), Measurable (Y i)) (π : G × G →+ G') (hπ : ∀ (h : G), Function.Injective fun (g : G) => π (g, h)) [FiniteRange (Y 2)] [FiniteRange (Y 3)] : d[⇑π ∘ ⟨Y 0, Y 2⟩ | Y 2 ; μ # ⇑π ∘ ⟨Y 1, Y 3⟩ | Y 3 ; μ] = d[Y 0 | Y 2 ; μ # Y 1 | Y 3 ; μ]

theorem condRuzsaDist'_of_inj_map {Ω : Type u_1} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [hG : MeasurableSpace G] [AddCommGroup G] [Countable G] [MeasurableSingletonClass G] [MeasureTheory.IsProbabilityMeasure μ] [Module (ZMod 2) G] {X : Ω → G} {B : Ω → G} {C : Ω → G} (hX : Measurable X) (hB : Measurable B) (hC : Measurable C) (h_indep : ProbabilityTheory.IndepFun X (⟨B, C⟩) μ) [FiniteRange X] [FiniteRange B] [FiniteRange C] : d[X ; μ # B | B + C ; μ] = d[X ; μ # C | B + C ; μ]

theorem condRuzsaDist'_of_inj_map' {Ω : Type u_1} {Ω'' : Type u_3} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [mΩ'' : MeasurableSpace Ω''] {μ'' : MeasureTheory.Measure Ω''} [hG : MeasurableSpace G] [AddCommGroup G] [Countable G] [MeasurableSingletonClass G] [Module (ZMod 2) G] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ''] {A : Ω'' → G} {B : Ω → G} {C : Ω → G} (hA : Measurable A) (hB : Measurable B) (hC : Measurable C) [FiniteRange A] [FiniteRange B] [FiniteRange C] : d[A ; μ'' # B | B + C ; μ] = d[A ; μ'' # C | B + C ; μ]

theorem kaimanovich_vershik {Ω : Type u_1} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [hG : MeasurableSpace G] [AddCommGroup G] [Countable G] [MeasurableSingletonClass G] {X : Ω → G} {Y : Ω → G} {Z : Ω → G} (h : ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![X, Y, Z] μ) (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) [FiniteRange X] [FiniteRange Z] [FiniteRange Y] : H[X + Y + Z ; μ] - H[X + Y ; μ] ≤ H[Y + Z ; μ] - H[Y ; μ]

The Kaimanovich-Vershik inequality. H[X + Y + Z] - H[X + Y] ≤ H[Y + Z] - H[Y].

theorem kaimanovich_vershik' {Ω : Type u_1} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [hG : MeasurableSpace G] [AddCommGroup G] [Countable G] [MeasurableSingletonClass G] {X : Ω → G} {Y : Ω → G} {Z : Ω → G} (h : ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![X, Y, Z] μ) (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) [FiniteRange X] [FiniteRange Z] [FiniteRange Y] : H[X - (Y + Z) ; μ] - H[X - Y ; μ] ≤ H[Y + Z ; μ] - H[Y ; μ]

A version of the Kaimanovich-Vershik inequality with some variables negated.

theorem ent_bsg {Ω : Type u_1} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [hG : MeasurableSpace G] [AddCommGroup G] [Countable G] [MeasurableSingletonClass G] [MeasureTheory.IsProbabilityMeasure μ] {A : Ω → G} {B : Ω → G} (hA : Measurable A) (hB : Measurable B) [Fintype G] : ∫ (x : G), (fun (z : G) => d[A ; ProbabilityTheory.cond μ ((A + B) ⁻¹' {z}) # B ; ProbabilityTheory.cond μ ((A + B) ⁻¹' {z})]) x ∂MeasureTheory.Measure.map (A + B) μ ≤ 3 * I[A : B ; μ] + 2 * H[A + B ; μ] - H[A ; μ] - H[B ; μ]

The entropic Balog-Szemerédi-Gowers inequality. Let $A, B$ be $G$-valued random variables on $\Omega$, and set $Z := A+B$. Then $$\sum_{z} P[Z=z] d[(A | Z = z) ; (B | Z = z)] \leq 3 I[A :B] + 2 H[Z] - H[A] - H[B]. $$ TODO: remove the hypothesis of Fintype G from here and from condIndep_copies'

theorem condRuzsaDist_le {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} {S : Type u_6} {T : Type u_7} [mΩ : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [mΩ' : MeasurableSpace Ω'] (μ' : MeasureTheory.Measure Ω') [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace S] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [Countable S] [Countable T] {X : Ω → G} {Z : Ω → S} {Y : Ω' → G} {W : Ω' → T} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] (hX : Measurable X) (hZ : Measurable Z) (hY : Measurable Y) (hW : Measurable W) [FiniteRange X] [FiniteRange Z] [FiniteRange Y] [FiniteRange W] : d[X | Z ; μ # Y | W ; μ'] ≤ d[X ; μ # Y ; μ'] + I[X : Z ; μ] / 2 + I[Y : W ; μ'] / 2

Suppose that $(X, Z)$ and $(Y, W)$ are random variables, where $X, Y$ take values in an abelian group. Then $$d[X | Z ; Y | W] \leq d[X ; Y] + \tfrac{1}{2} I[X : Z] + \tfrac{1}{2} I[Y : W]$$

theorem condRuzsaDist_le' {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} {T : Type u_7} [mΩ : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [mΩ' : MeasurableSpace Ω'] (μ' : MeasureTheory.Measure Ω') [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] [MeasurableSingletonClass T] [Countable T] {X : Ω → G} {Y : Ω' → G} {W : Ω' → T} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] (hX : Measurable X) (hY : Measurable Y) (hW : Measurable W) [FiniteRange X] [FiniteRange Y] [FiniteRange W] : d[X ; μ # Y | W ; μ'] ≤ d[X ; μ # Y ; μ'] + I[Y : W ; μ'] / 2

theorem condRuzsaDist_le'_prod {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} {T : Type u_7} [mΩ : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [mΩ' : MeasurableSpace Ω'] (μ' : MeasureTheory.Measure Ω') [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSpace T] [Countable G] [MeasurableSingletonClass G] [MeasurableSingletonClass T] [Countable T] {X : Ω → G} {Y : Ω' → G} {W : Ω' → T} {Z : Ω' → T} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] (hX : Measurable X) (hY : Measurable Y) (hW : Measurable W) (hZ : Measurable Z) [FiniteRange X] [FiniteRange Y] [FiniteRange W] [FiniteRange Z] : d[X ; μ # Y | ⟨W, Z⟩ ; μ'] ≤ d[X ; μ # Y | Z ; μ'] + I[Y : W|Z;μ'] / 2

theorem comparison_of_ruzsa_distances {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [hG : MeasurableSpace G] [AddCommGroup G] [Countable G] [MeasurableSingletonClass G] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] {X : Ω → G} {Y : Ω' → G} {Z : Ω' → G} (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (h : ProbabilityTheory.IndepFun Y Z μ') [FiniteRange X] [FiniteRange Z] [FiniteRange Y] : d[X ; μ # Y + Z ; μ'] - d[X ; μ # Y ; μ'] ≤ (H[Y + Z ; μ'] - H[Y ; μ']) / 2 ∧ (Module (ZMod 2) G → H[Y + Z ; μ'] - H[Y ; μ'] = d[Y ; μ' # Z ; μ'] + H[Z ; μ'] / 2 - H[Y ; μ'] / 2)

theorem condRuzsaDist_diff_le {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [hG : MeasurableSpace G] [AddCommGroup G] [Countable G] [MeasurableSingletonClass G] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] {X : Ω → G} {Y : Ω' → G} {Z : Ω' → G} (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (h : ProbabilityTheory.IndepFun Y Z μ') [FiniteRange X] [FiniteRange Z] [FiniteRange Y] : d[X ; μ # Y + Z ; μ'] - d[X ; μ # Y ; μ'] ≤ (H[Y + Z ; μ'] - H[Y ; μ']) / 2

Let $X, Y, Z$ be random variables taking values in some abelian group, and with $Y, Z$ independent. Then we have $$d[X ; Y + Z] -d[X ; Y] \leq \tfrac{1}{2} (H[Y+ Z] - H[Y])$$ $$= \tfrac{1}{2} d[Y ; Z] + \tfrac{1}{4} H[Z] - \tfrac{1}{4} H[Y]$$ and $$d[X ; Y|Y+ Z] - d[X ; Y] \leq \tfrac{1}{2} \bigl(H[Y+ Z] - H[Z]\bigr)$$ $$= \tfrac{1}{2} d[Y ; Z] + \tfrac{1}{4} H[Y] - \tfrac{1}{4} H[Z]$$

theorem entropy_sub_entropy_eq_condRuzsaDist_add {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [hG : MeasurableSpace G] [AddCommGroup G] [Countable G] [MeasurableSingletonClass G] [Module (ZMod 2) G] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] {X : Ω → G} {Y : Ω' → G} {Z : Ω' → G} (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (h : ProbabilityTheory.IndepFun Y Z μ') [FiniteRange X] [FiniteRange Z] [FiniteRange Y] : H[Y + Z ; μ'] - H[Y ; μ'] = d[Y ; μ' # Z ; μ'] + H[Z ; μ'] / 2 - H[Y ; μ'] / 2

theorem condRuzsaDist_diff_le' {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [hG : MeasurableSpace G] [AddCommGroup G] [Countable G] [MeasurableSingletonClass G] [Module (ZMod 2) G] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] {X : Ω → G} {Y : Ω' → G} {Z : Ω' → G} (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (h : ProbabilityTheory.IndepFun Y Z μ') [FiniteRange X] [FiniteRange Z] [FiniteRange Y] : d[X ; μ # Y + Z ; μ'] - d[X ; μ # Y ; μ'] ≤ d[Y ; μ' # Z ; μ'] / 2 + H[Z ; μ'] / 4 - H[Y ; μ'] / 4

theorem condRuzsaDist_diff_le'' {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [hG : MeasurableSpace G] [AddCommGroup G] [Countable G] [MeasurableSingletonClass G] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] {X : Ω → G} {Y : Ω' → G} {Z : Ω' → G} (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (h : ProbabilityTheory.IndepFun Y Z μ') [FiniteRange X] [FiniteRange Z] [FiniteRange Y] : d[X ; μ # Y | Y + Z ; μ'] - d[X ; μ # Y ; μ'] ≤ (H[Y + Z ; μ'] - H[Z ; μ']) / 2

theorem condRuzsaDist_diff_le''' {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [hG : MeasurableSpace G] [AddCommGroup G] [Countable G] [MeasurableSingletonClass G] [Module (ZMod 2) G] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] {X : Ω → G} {Y : Ω' → G} {Z : Ω' → G} (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (h : ProbabilityTheory.IndepFun Y Z μ') [FiniteRange X] [FiniteRange Z] [FiniteRange Y] : d[X ; μ # Y | Y + Z ; μ'] - d[X ; μ # Y ; μ'] ≤ d[Y ; μ' # Z ; μ'] / 2 + H[Y ; μ'] / 4 - H[Z ; μ'] / 4

theorem condRuzsaDist_diff_ofsum_le {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [hG : MeasurableSpace G] [AddCommGroup G] [Countable G] [MeasurableSingletonClass G] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] {X : Ω → G} {Y : Ω' → G} {Z : Ω' → G} {Z' : Ω' → G} (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (hZ' : Measurable Z') (h : ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![Y, Z, Z'] μ') [FiniteRange X] [FiniteRange Z] [FiniteRange Y] [FiniteRange Z'] : d[X ; μ # Y + Z | Y + Z + Z' ; μ'] - d[X ; μ # Y ; μ'] ≤ (H[Y + Z + Z' ; μ'] + H[Y + Z ; μ'] - H[Y ; μ'] - H[Z' ; μ']) / 2