noncomputable def ProbabilityTheory.setRuzsaDist {G : Type u_1} [MeasurableSpace G] [AddCommGroup G] (A B : Set G) : ℝ

The Ruzsa distance between two subsets A, B of a group G is defined to be the Ruzsa distance between their uniform probability distributions. Is only intended for use when A, B are finite and non-empty.

Equations

• dᵤ[A # B] = ProbabilityTheory.Kernel.rdistm (ProbabilityTheory.uniformOn A) (ProbabilityTheory.uniformOn B)

def ProbabilityTheory.«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 ProbabilityTheory.«termDᵤ[_#_]» : Lean.ParserDescr

The Ruzsa distance between two subsets A, B of a group G is defined to be the Ruzsa distance between their uniform probability distributions. Is only intended for use when A, B are finite and non-empty.

Equations

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

theorem ProbabilityTheory.setRuzsaDist_eq_rdist {G : Type u_1} [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] {A B : Set G} [Finite ↑A] [Finite ↑B] {Ω : Type u_2} {Ω' : Type u_3} [mΩ : MeasureTheory.MeasureSpace Ω] [mΩ' : MeasureTheory.MeasureSpace Ω'] {μ : MeasureTheory.Measure Ω} {μ' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] {UA : Ω → G} {UB : Ω' → G} (hUA : ProbabilityTheory.IsUniform A UA μ) (hUB : ProbabilityTheory.IsUniform B UB μ') (hUA_mes : Measurable UA) (hUB_mes : Measurable UB) : dᵤ[A # B] = d[UA ; μ # UB ; μ']

Relating Ruzsa distance between sets to Ruzsa distance between random variables

theorem ProbabilityTheory.setRuzsaDist_nonneg {G : Type u_1} [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] (A B : Set G) [hA : Finite ↑A] [hB : Finite ↑B] [Nonempty ↑A] [Nonempty ↑B] : 0 ≤ dᵤ[A # B]

Ruzsa distance between sets is nonnegative.

theorem ProbabilityTheory.setRuzsaDist_symm {G : Type u_1} [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] (A B : Set G) [hA : Finite ↑A] [hB : Finite ↑B] [Nonempty ↑A] [Nonempty ↑B] : dᵤ[A # B] = dᵤ[B # A]

Ruzsa distance between sets is symmetric.

theorem ProbabilityTheory.setRuzsaDist_triangle {G : Type u_1} [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] (A B C : Set G) [hA : Finite ↑A] [hB : Finite ↑B] [hC : Finite ↑C] [Nonempty ↑A] [Nonempty ↑B] [Nonempty ↑C] : dᵤ[A # C] ≤ dᵤ[A # B] + dᵤ[B # C]

Ruzsa distance between sets obeys the triangle inequality.

theorem ProbabilityTheory.setRuzsaDist_add_const {G : Type u_1} [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] (A B : Set G) [hA : Finite ↑A] [hB : Finite ↑B] [Nonempty ↑A] [Nonempty ↑B] (c c' : G) : dᵤ[A + {c} # B + {c'}] = dᵤ[A # B]

Ruzsa distance between sets is translation invariant.

theorem ProbabilityTheory.setRuzsaDist_of_inj {G : Type u_1} [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] (A B : Set G) [hA : Finite ↑A] [hB : Finite ↑B] [Nonempty ↑A] [Nonempty ↑B] {H : Type u_2} [hH : MeasurableSpace H] [MeasurableSingletonClass H] [AddCommGroup H] [Countable H] {φ : G →+ H} (hφ : Function.Injective ⇑φ) : dᵤ[⇑φ '' A # ⇑φ '' B] = dᵤ[A # B]

Ruzsa distance between sets is preserved by injective homomorphisms.

theorem ProbabilityTheory.setRuzsaDist_le {G : Type u_1} [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] (A B : Set G) [h'A : Finite ↑A] [h'B : Finite ↑B] (hA : A.Nonempty) (hB : B.Nonempty) : dᵤ[A # B] ≤ Real.log ↑(Nat.card ↑(A - B)) - Real.log ↑(Nat.card ↑A) / 2 - Real.log ↑(Nat.card ↑B) / 2

Ruzsa distance between sets is controlled by the doubling constant.