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)
:
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.
Instances For
@[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 : ProbabilityTheory.IdentDistrib X X' MeasureTheory.volume MeasureTheory.volume)
:
theorem
sub_mem_symmGroup
{Ω : Type u_1}
{G : Type u_2}
[MeasureTheory.MeasureSpace Ω]
[MeasurableSpace G]
[AddCommGroup G]
[MeasurableAdd₂ G]
{X : Ω → G}
[Fintype G]
[MeasurableSingletonClass G]
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
(hX : Measurable X)
(hdist : d[X # X] = 0)
{x : G}
{y : G}
(hx : MeasureTheory.volume (X ⁻¹' {x}) ≠ 0)
(hy : MeasureTheory.volume (X ⁻¹' {y}) ≠ 0)
:
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}
[Fintype 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}
[Fintype 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}
[Fintype 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.