Ruzsa distance for finite sets

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ᵤ[_#_]» : 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 : IsUniform A UA μ) (hUB : 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_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.