The 100% version of entropic PFR

Here we show entropic PFR in the case of doubling constant zero.

Main results

• exists_isUniform_of_rdist_eq_zero : If $d[X_1;X_2]=0$, then there exists a subgroup $H \leq G$ such that $d[X_1;U_H] = d[X_2;U_H] = 0$.

def symmGroup {Ω : Type u_1} {G : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasurableSpace G] [AddCommGroup G] [MeasurableAdd₂ G] (X : Ω → G) (hX : Measurable X) : AddSubgroup G

The symmetry group Sym of $X$: the set of all $h ∈ G$ such that $X + h$ has an identical distribution to $X$.

Equations

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

@[simp]

theorem mem_symmGroup {Ω : Type u_1} {G : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasurableSpace G] [AddCommGroup G] [MeasurableAdd₂ G] {X : Ω → G} (hX : Measurable X) {x : G} : x ∈ symmGroup X hX ↔ ProbabilityTheory.IdentDistrib X (fun (ω : Ω) => X ω + x) MeasureTheory.volume MeasureTheory.volume

theorem ProbabilityTheory.IdentDistrib.symmGroup_eq {Ω : Type u_1} {G : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasurableSpace G] [AddCommGroup G] [MeasurableAdd₂ G] {X : Ω → G} {Ω' : Type u_3} [MeasureTheory.MeasureSpace Ω'] {X' : Ω' → G} (hX : Measurable X) (hX' : Measurable X') (h : IdentDistrib X X' MeasureTheory.volume MeasureTheory.volume) : symmGroup X hX = symmGroup X' hX'

theorem sub_mem_symmGroup {Ω : Type u_1} {G : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasurableSpace G] [AddCommGroup G] [MeasurableAdd₂ G] {X : Ω → G} [Finite G] [MeasurableSingletonClass G] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (hX : Measurable X) (hdist : d[X # X] = 0) {x y : G} (hx : MeasureTheory.volume (X ⁻¹' {x}) ≠ 0) (hy : MeasureTheory.volume (X ⁻¹' {y}) ≠ 0) : x - y ∈ symmGroup X hX

If $d[X ;X]=0$, and $x,y \in G$ are such that $P[X=x], P[X=y]>0$, then $x-y \in \mathrm{Sym}[X]$.

theorem isUniform_sub_const_of_rdist_eq_zero {Ω : Type u_1} {G : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasurableSpace G] [AddCommGroup G] [MeasurableAdd₂ G] {X : Ω → G} [Finite G] [MeasurableSingletonClass G] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (hX : Measurable X) (hdist : d[X # X] = 0) {x₀ : G} (hx₀ : MeasureTheory.volume (X ⁻¹' {x₀}) ≠ 0) : ProbabilityTheory.IsUniform (↑(symmGroup X hX)) (fun (ω : Ω) => X ω - x₀) MeasureTheory.volume

If d[X # X] = 0, then X - x₀ is the uniform distribution on the subgroup of G stabilizing the distribution of X, for any x₀ of positive probability.

theorem exists_isUniform_of_rdist_self_eq_zero {Ω : Type u_1} {G : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasurableSpace G] [AddCommGroup G] [MeasurableAdd₂ G] {X : Ω → G} [Finite G] [MeasurableSingletonClass G] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (hX : Measurable X) (hdist : d[X # X] = 0) : ∃ (H : AddSubgroup G) (U : Ω → G), Measurable U ∧ ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume ∧ d[X # U] = 0

If $d[X ;X]=0$, then there exists a subgroup $H \leq G$ such that $d[X ;U_H] = 0$.

theorem exists_isUniform_of_rdist_eq_zero {Ω : Type u_1} {G : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasurableSpace G] [AddCommGroup G] [MeasurableAdd₂ G] {X : Ω → G} [Finite G] [MeasurableSingletonClass G] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {Ω' : Type u_3} [MeasureTheory.MeasureSpace Ω'] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X' : Ω' → G} (hX : Measurable X) (hX' : Measurable X') (hdist : d[X # X'] = 0) : ∃ (H : AddSubgroup G) (U : Ω → G), Measurable U ∧ ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume ∧ d[X # U] = 0 ∧ d[X' # U] = 0

If $d[X_1;X_2]=0$, then there exists a subgroup $H \leq G$ such that $d[X_1;U_H] = d[X_2;U_H] = 0$. Follows from the preceding claim by the triangle inequality.