noncomputable def MeasureTheory.Measure.discreteUniform {S : Type u_1} [MeasurableSpace S] (H : Set S) : MeasureTheory.Measure S

In practice one would also impose the conditions MeasurableSingletonClass S, Finite H and Nonempty H before attempting to use this definition.

Equations

• MeasureTheory.Measure.discreteUniform H = (↑H.encard)⁻¹ • MeasureTheory.Measure.count.restrict H

theorem MeasureTheory.Measure.discreteUniform_of_infinite {S : Type u_1} [MeasurableSpace S] (H : Set S) (h : H.Infinite) : MeasureTheory.Measure.discreteUniform H = 0

The uniform distribution on an infinite set vanishes by definition.

theorem MeasureTheory.Measure.discreteUniform_apply {S : Type u_1} [MeasurableSpace S] (H : Set S) [MeasurableSingletonClass S] [Finite ↑H] (A : Set S) : (MeasureTheory.Measure.discreteUniform H) A = ↑(Nat.card ↑(A ∩ H)) / ↑(Nat.card ↑H)

The usual formula for the discrete uniform measure applied to an arbitrary set.

theorem MeasureTheory.Measure.discreteUniform_apply' {S : Type u_1} [MeasurableSpace S] (H : Set S) [MeasurableSingletonClass S] [Finite ↑H] (A : Set S) : (MeasureTheory.Measure.discreteUniform H).real A = ↑(Nat.card ↑(A ∩ H)) / ↑(Nat.card ↑H)

Variant of `discreteUniform_apply' using real-valued measures.

instance MeasureTheory.Measure.discreteUniform.isProbabilityMeasure {S : Type u_1} [MeasurableSpace S] (H : Set S) [MeasurableSingletonClass S] [Finite ↑H] [Nonempty ↑H] : MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.discreteUniform H)

Equations

• ⋯ = ⋯

theorem MeasureTheory.Measure.map_discreteUniform_of_inj {S : Type u_1} [MeasurableSpace S] (H : Set S) [MeasurableSingletonClass S] [Finite ↑H] {T : Type u_2} [MeasurableSpace T] [MeasurableSingletonClass T] {f : S → T} (hmes : Measurable f) (hf : Function.Injective f) : MeasureTheory.Measure.map f (MeasureTheory.Measure.discreteUniform H) = MeasureTheory.Measure.discreteUniform (f '' H)

injective map of discrete uniform is discrete uniform

theorem MeasureTheory.Measure.isUniform_iff_uniform_dist {S : Type u_1} [MeasurableSpace S] (H : Set S) [MeasurableSingletonClass S] [Finite ↑H] [Nonempty ↑H] {Ω : Type u_2} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [Countable S] (hμ : MeasureTheory.IsProbabilityMeasure μ) {U : Ω → S} (hU : Measurable U) : ProbabilityTheory.IsUniform H U μ ↔ MeasureTheory.Measure.map U μ = MeasureTheory.Measure.discreteUniform H

A random variable is uniform iff its distribution is.

theorem ProbabilityTheory.entropy_of_discreteUniform {S : Type u_1} [MeasurableSpace S] (H : Set S) [MeasurableSingletonClass S] [Finite ↑H] [Nonempty ↑H] : Hm[MeasureTheory.Measure.discreteUniform H] = (↑(Nat.card ↑H)).log

The entropy of a uniform measure is the log of the cardinality of its support.

noncomputable def ProbabilityTheory.rdist_set {G : Type u_1} [MeasurableSpace G] [AddCommGroup G] (A : Set G) (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 (MeasureTheory.Measure.discreteUniform A) (MeasureTheory.Measure.discreteUniform B)

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

Equations

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

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.

theorem ProbabilityTheory.rdist_set_eq_rdist {G : Type u_1} [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] {A : Set G} {B : Set G} [Finite ↑A] [Finite ↑B] [Nonempty ↑A] [Nonempty ↑B] {Ω : Type u_2} {Ω' : Type u_3} [mΩ : MeasureTheory.MeasureSpace Ω] [mΩ' : MeasureTheory.MeasureSpace Ω'] {μ : MeasureTheory.Measure Ω} {μ' : MeasureTheory.Measure Ω'} (hμ : MeasureTheory.IsProbabilityMeasure μ) (hμ' : 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.rdist_set_nonneg {G : Type u_1} [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] (A : Set G) (B : Set G) [Finite ↑A] [Finite ↑B] [Nonempty ↑A] [Nonempty ↑B] : 0 ≤ dᵤ[A # B]

Ruzsa distance between sets is nonnegative.

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

Ruzsa distance between sets is symmetric.

theorem ProbabilityTheory.rdist_set_triangle {G : Type u_1} [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] (A : Set G) (B : Set G) (C : Set G) [Finite ↑A] [Finite ↑B] [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.rdist_set_add_const {G : Type u_1} [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] (A : Set G) (B : Set G) [Finite ↑A] [Finite ↑B] [Nonempty ↑A] [Nonempty ↑B] (c : G) (c' : G) : dᵤ[A + {c} # B + {c'}] = dᵤ[A # B]

Ruzsa distance between sets is translation invariant.

theorem ProbabilityTheory.rdist_set_of_inj {G : Type u_1} [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] (A : Set G) (B : Set G) [Finite ↑A] [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.rdist_set_le {G : Type u_1} [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] (A : Set G) (B : Set G) [Finite ↑A] [Finite ↑B] (hA : A.Nonempty) (hB : B.Nonempty) : dᵤ[A # B] ≤ (↑(Nat.card ↑(A - B))).log - (↑(Nat.card ↑A)).log / 2 - (↑(Nat.card ↑B)).log / 2

Ruzsa distance between sets is controlled by the doubling constant.