The rho functional #
Definition of the rho functional and basic facts
noncomputable def
rhoMinusSet
{G : Type uG}
[AddCommGroup G]
[hGm : MeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
(X : Ω → G)
(A : Finset G)
(μ : MeasureTheory.Measure Ω)
:
The set of possible values of $D_{KL}(X \Vert U_A + T)$, where $U_A$ is uniform on $A$ and
$T$ ranges over $G$-valued random variables independent of $U_A$. We also require an absolute
continuity condition so that the KL divergence makes sense in ℝ.
To avoid universe issues, we express this using measures on G, but the equivalence with the
above point of view follows from rhoMinus_le below.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
map_prod_uniformOn_ne_zero
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{A : Finset G}
{y : G}
(hA : A.Nonempty)
{μ : MeasureTheory.Measure G}
[MeasureTheory.IsProbabilityMeasure μ]
(hμ : ∀ (x : G), μ {x} ≠ 0)
:
(MeasureTheory.Measure.map (Prod.fst + Prod.snd) (μ.prod (ProbabilityTheory.uniformOn ↑A))) {y} ≠ 0
theorem
nonempty_rhoMinusSet
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X : Ω → G}
{A : Finset G}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
(hA : A.Nonempty)
:
(rhoMinusSet X A μ).Nonempty
theorem
nonneg_of_mem_rhoMinusSet
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X : Ω → G}
{A : Finset G}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
(hX : Measurable X)
{x : ℝ}
(hx : x ∈ rhoMinusSet X A μ)
:
0 ≤ x
theorem
bddBelow_rhoMinusSet
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X : Ω → G}
{A : Finset G}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
(hX : Measurable X)
:
BddBelow (rhoMinusSet X A μ)
theorem
rhoMinusSet_eq_of_identDistrib
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X : Ω → G}
{A : Finset G}
{Ω' : Type u_2}
[MeasurableSpace Ω']
{μ' : MeasureTheory.Measure Ω'}
{X' : Ω' → G}
(h : ProbabilityTheory.IdentDistrib X X' μ μ')
:
rhoMinusSet X A μ = rhoMinusSet X' A μ'
noncomputable def
rhoMinus
{G : Type uG}
[AddCommGroup G]
[hGm : MeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
(X : Ω → G)
(A : Finset G)
(μ : MeasureTheory.Measure Ω)
:
For any $G$-valued random variable $X$, we define $\rho^-(X)$ to be the infimum of $D_{KL}(X \Vert U_A + T)$, where $U_A$ is uniform on $A$ and $T$ ranges over $G$-valued random variables independent of $U_A$.
Equations
- ρ⁻[X ; μ # A] = sInf (rhoMinusSet X A μ)
Instances For
For any $G$-valued random variable $X$, we define $\rho^-(X)$ to be the infimum of $D_{KL}(X \Vert U_A + T)$, where $U_A$ is uniform on $A$ and $T$ ranges over $G$-valued random variables independent of $U_A$.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pretty printer defined by notation3 command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pretty printer defined by notation3 command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
For any $G$-valued random variable $X$, we define $\rho^-(X)$ to be the infimum of $D_{KL}(X \Vert U_A + T)$, where $U_A$ is uniform on $A$ and $T$ ranges over $G$-valued random variables independent of $U_A$.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
rhoMinus_eq_of_identDistrib
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X : Ω → G}
{A : Finset G}
{Ω' : Type u_2}
[MeasurableSpace Ω']
{X' : Ω' → G}
{μ' : MeasureTheory.Measure Ω'}
(h : ProbabilityTheory.IdentDistrib X X' μ μ')
:
ρ⁻[X ; μ # A] = ρ⁻[X' ; μ' # A]
theorem
rhoMinus_le_def
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X : Ω → G}
{A : Finset G}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
(hX : Measurable X)
{μ' : MeasureTheory.Measure G}
[MeasureTheory.IsProbabilityMeasure μ']
(habs :
∀ (y : G),
(MeasureTheory.Measure.map (Prod.fst + Prod.snd) (μ'.prod (ProbabilityTheory.uniformOn ↑A))) {y} = 0 →
(MeasureTheory.Measure.map X μ) {y} = 0)
:
ρ⁻[X ; μ # A] ≤ KL[X ; μ # Prod.fst + Prod.snd ; μ'.prod (ProbabilityTheory.uniformOn ↑A)]
theorem
rhoMinus_le
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X : Ω → G}
{A : Finset G}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
(hX : Measurable X)
(hA : A.Nonempty)
{Ω' : Type u_2}
[MeasurableSpace Ω']
{T U : Ω' → G}
{μ' : MeasureTheory.Measure Ω'}
[MeasureTheory.IsProbabilityMeasure μ']
(hunif : ProbabilityTheory.IsUniform (↑A) U μ')
(hT : Measurable T)
(hU : Measurable U)
(h_indep : ProbabilityTheory.IndepFun T U μ')
(habs : ∀ (y : G), (MeasureTheory.Measure.map (T + U) μ') {y} = 0 → (MeasureTheory.Measure.map X μ) {y} = 0)
:
theorem
rhoMinus_nonneg
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
{X : Ω → G}
{A : Finset G}
(hX : Measurable X)
:
0 ≤ ρ⁻[X ; μ # A]
We have $\rho^-(X) \geq 0$.
theorem
rhoMinus_zero_measure
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
(hP : μ = 0)
{X : Ω → G}
{A : Finset G}
:
ρ⁻[X ; μ # A] = 0
theorem
rhoMinus_continuous
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{A : Finset G}
[TopologicalSpace G]
[DiscreteTopology G]
(hA : A.Nonempty)
:
Continuous fun (μ : MeasureTheory.ProbabilityMeasure G) => ρ⁻[id ; ↑μ # A]
noncomputable def
rhoPlus
{G : Type uG}
[AddCommGroup G]
[hGm : MeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
(X : Ω → G)
(A : Finset G)
(μ : MeasureTheory.Measure Ω)
:
For any $G$-valued random variable $X$, we define $\rho^+(X) := \rho^-(X) + \bbH(X) - \bbH(U_A)$.
Instances For
For any $G$-valued random variable $X$, we define $\rho^+(X) := \rho^-(X) + \bbH(X) - \bbH(U_A)$.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pretty printer defined by notation3 command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
For any $G$-valued random variable $X$, we define $\rho^+(X) := \rho^-(X) + \bbH(X) - \bbH(U_A)$.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pretty printer defined by notation3 command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
rhoPlus_continuous
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{A : Finset G}
[TopologicalSpace G]
[DiscreteTopology G]
(hA : A.Nonempty)
:
Continuous fun (μ : MeasureTheory.ProbabilityMeasure G) => ρ⁺[id ; ↑μ # A]
theorem
rhoPlus_eq_of_identDistrib
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X : Ω → G}
{A : Finset G}
{Ω' : Type u_2}
[MeasurableSpace Ω']
{X' : Ω' → G}
{μ' : MeasureTheory.Measure Ω'}
(h : ProbabilityTheory.IdentDistrib X X' μ μ')
:
ρ⁺[X ; μ # A] = ρ⁺[X' ; μ' # A]
theorem
exists_mem_card_inter_add
{G : Type uG}
[AddCommGroup G]
[Fintype G]
(H : AddSubgroup G)
{A : Set G}
(hA : A.Nonempty)
:
theorem
rhoMinus_of_subgroup
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{H : AddSubgroup G}
{U : Ω → G}
(hunif : ProbabilityTheory.IsUniform (↑H) U μ)
{A : Finset G}
(hA : A.Nonempty)
(hU : Measurable U)
:
If $H$ is a finite subgroup of $G$, then $\rho^-(U_H) = \log |A| - \log \max_t |A \cap (H+t)|$.
theorem
rhoPlus_of_subgroup
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{H : AddSubgroup G}
{U : Ω → G}
(hunif : ProbabilityTheory.IsUniform (↑H) U μ)
{A : Finset G}
(hA : A.Nonempty)
(hU : Measurable U)
:
If $H$ is a finite subgroup of $G$, then $\rho^+(U_H) = \log |H| - \log \max_t |A \cap (H+t)|$.
noncomputable def
rho
{G : Type uG}
[AddCommGroup G]
[hGm : MeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
(X : Ω → G)
(A : Finset G)
(μ : MeasureTheory.Measure Ω)
:
We define $\rho(X) := (\rho^+(X) + \rho^-(X))/2$.
Instances For
We define $\rho(X) := (\rho^+(X) + \rho^-(X))/2$.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pretty printer defined by notation3 command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
We define $\rho(X) := (\rho^+(X) + \rho^-(X))/2$.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pretty printer defined by notation3 command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
rho_eq_of_identDistrib
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X : Ω → G}
{A : Finset G}
{Ω' : Type u_2}
[MeasurableSpace Ω']
{X' : Ω' → G}
{μ' : MeasureTheory.Measure Ω'}
(h : ProbabilityTheory.IdentDistrib X X' μ μ')
:
ρ[X ; μ # A] = ρ[X' ; μ' # A]
theorem
rho_of_uniform
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{U : Ω → G}
{A : Finset G}
(hunif : ProbabilityTheory.IsUniform (↑A) U μ)
(hU : Measurable U)
(hA : A.Nonempty)
:
ρ[U ; μ # A] = 0
We have $\rho(U_A) = 0$.
theorem
rho_of_subgroup
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{H : AddSubgroup G}
{U : Ω → G}
(hunif : ProbabilityTheory.IsUniform (↑H) U μ)
{A : Finset G}
(hA : A.Nonempty)
(hU : Measurable U)
(r : ℝ)
(hr : ρ[U ; μ # A] ≤ r)
:
If $H$ is a finite subgroup of $G$, and $\rho(U_H) \leq r$, then there exists $t$ such that $|A \cap (H+t)| \geq e^{-r} \sqrt{|A||H|}$, and $|H|/|A| \in [e^{-2r}, e^{2r}]$.
theorem
rho_of_submodule
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
[Module (ZMod 2) G]
{H : Submodule (ZMod 2) G}
{U : Ω → G}
(hunif : ProbabilityTheory.IsUniform (↑H) U μ)
{A : Finset G}
(hA : A.Nonempty)
(hU : Measurable U)
(r : ℝ)
(hr : ρ[U ; μ # A] ≤ r)
:
If $H$ is a finite subgroup of $G$, and $\rho(U_H) \leq r$, then there exists $t$ such that $|A \cap (H+t)| \geq e^{-r} \sqrt{|A||H|}$, and $|H|/|A| \in [e^{-2r}, e^{2r}]$.
theorem
rho_continuous
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
[TopologicalSpace G]
[DiscreteTopology G]
[BorelSpace G]
{A : Finset G}
(hA : A.Nonempty)
:
Continuous fun (μ : MeasureTheory.ProbabilityMeasure G) => ρ[id ; ↑μ # A]
\rho(X)$ depends continuously on the distribution of $X$.
theorem
tendsto_rho_probabilityMeasure
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{A : Finset G}
{α : Type u_2}
{l : Filter α}
[TopologicalSpace Ω]
[BorelSpace Ω]
[TopologicalSpace G]
[BorelSpace G]
[DiscreteTopology G]
{X : Ω → G}
(hX : Continuous X)
(hA : A.Nonempty)
{μ : α → MeasureTheory.ProbabilityMeasure Ω}
{ν : MeasureTheory.ProbabilityMeasure Ω}
(hμ : Filter.Tendsto μ l (nhds ν))
:
Filter.Tendsto (fun (n : α) => ρ[X ; ↑(μ n) # A]) l (nhds ρ[X ; ↑ν # A])
theorem
rhoMinus_of_sum
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X Y : Ω → G}
{A : Finset G}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
(hX : Measurable X)
(hY : Measurable Y)
(hA : A.Nonempty)
(h_indep : ProbabilityTheory.IndepFun X Y μ)
:
If $X,Y$ are independent, one has $$ \rho^-(X+Y) \leq \rho^-(X)$$
theorem
rhoPlus_of_sum
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X Y : Ω → G}
{A : Finset G}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
(hX : Measurable X)
(hY : Measurable Y)
(hA : A.Nonempty)
(h_indep : ProbabilityTheory.IndepFun X Y μ)
:
If $X,Y$ are independent, one has $$ \rho^+(X+Y) \leq \rho^+(X) + \bbH[X+Y] - \bbH[X]$$
theorem
rho_of_sum
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X Y : Ω → G}
{A : Finset G}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
(hX : Measurable X)
(hY : Measurable Y)
(hA : A.Nonempty)
(h_indep : ProbabilityTheory.IndepFun X Y μ)
:
If $X,Y$ are independent, one has $$ \rho(X+Y) \leq \rho(X) + \frac{1}{2}( \bbH[X+Y] - \bbH[X] ).$$
theorem
rho_of_translate
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X : Ω → G}
{A : Finset G}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
(hX : Measurable X)
(hA : A.Nonempty)
(s : G)
:
noncomputable def
condRho
{G : Type uG}
[AddCommGroup G]
[hGm : MeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{S : Type u_2}
(X : Ω → G)
(Y : Ω → S)
(A : Finset G)
(μ : MeasureTheory.Measure Ω)
:
We define $\rho(X|Y) := \sum_y {\bf P}(Y=y) \rho(X|Y=y)$.
Equations
- ρ[X | Y ; μ # A] = ∑' (s : S), (μ (Y ⁻¹' {s})).toReal * ρ[X ; ProbabilityTheory.cond μ (Y ⁻¹' {s}) # A]
Instances For
noncomputable def
condRhoMinus
{G : Type uG}
[AddCommGroup G]
[hGm : MeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{S : Type u_2}
(X : Ω → G)
(Y : Ω → S)
(A : Finset G)
(μ : MeasureTheory.Measure Ω)
:
Average of rhoMinus along the fibers
Equations
- ρ⁻[X | Y ; μ # A] = ∑' (s : S), (μ (Y ⁻¹' {s})).toReal * ρ⁻[X ; ProbabilityTheory.cond μ (Y ⁻¹' {s}) # A]
Instances For
noncomputable def
condRhoPlus
{G : Type uG}
[AddCommGroup G]
[hGm : MeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{S : Type u_2}
(X : Ω → G)
(Y : Ω → S)
(A : Finset G)
(μ : MeasureTheory.Measure Ω)
:
Average of rhoPlus along the fibers
Equations
- ρ⁺[X | Y ; μ # A] = ∑' (s : S), (μ (Y ⁻¹' {s})).toReal * ρ⁺[X ; ProbabilityTheory.cond μ (Y ⁻¹' {s}) # A]
Instances For
Pretty printer defined by notation3 command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
We define $\rho(X|Y) := \sum_y {\bf P}(Y=y) \rho(X|Y=y)$.
Equations
- One or more equations did not get rendered due to their size.
Instances For
We define $\rho(X|Y) := \sum_y {\bf P}(Y=y) \rho(X|Y=y)$.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pretty printer defined by notation3 command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Average of rhoMinus along the fibers
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pretty printer defined by notation3 command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pretty printer defined by notation3 command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Average of rhoPlus along the fibers
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
condRho_of_translate
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X : Ω → G}
{A : Finset G}
{S : Type u_2}
{Y : Ω → S}
(hX : Measurable X)
(hA : A.Nonempty)
(s : G)
:
For any $s\in G$, $\rho(X+s|Y)=\rho(X|Y)$.
theorem
condRho_of_injective
{G : Type uG}
[AddCommGroup G]
[hGm : MeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
(X : Ω → G)
{S : Type u_2}
{T : Type u_3}
(Y : Ω → S)
{A : Finset G}
{f : S → T}
(hf : Function.Injective f)
:
If $f$ is injective, then $\rho(X|f(Y))=\rho(X|Y)$.
theorem
condRho_eq_of_identDistrib
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{A : Finset G}
{S : Type u_2}
[MeasurableSpace S]
[MeasurableSingletonClass S]
{Y : Ω → G}
{W : Ω → S}
{Ω' : Type u_3}
[MeasurableSpace Ω']
{μ' : MeasureTheory.Measure Ω'}
{Y' : Ω' → G}
{W' : Ω' → S}
(hY : Measurable Y)
(hW : Measurable W)
(hY' : Measurable Y')
(hW' : Measurable W')
(h : ProbabilityTheory.IdentDistrib (⟨Y, W⟩) (⟨Y', W'⟩) μ μ')
:
ρ[Y | W ; μ # A] = ρ[Y' | W' ; μ' # A]
theorem
condRhoMinus_le
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X : Ω → G}
{A : Finset G}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
{S : Type u_2}
[MeasurableSpace S]
[Fintype S]
[MeasurableSingletonClass S]
{Z : Ω → S}
(hX : Measurable X)
(hZ : Measurable Z)
(hA : A.Nonempty)
:
$$ \rho^-(X|Z) \leq \rho^-(X) + \bbH[X] - \bbH[X|Z]$$
theorem
condRhoPlus_le
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X : Ω → G}
{A : Finset G}
[MeasureTheory.IsProbabilityMeasure μ]
{S : Type u_2}
[MeasurableSpace S]
[Fintype S]
[MeasurableSingletonClass S]
{Z : Ω → S}
(hX : Measurable X)
(hZ : Measurable Z)
(hA : A.Nonempty)
:
ρ⁺[X | Z ; μ # A] ≤ ρ⁺[X ; μ # A]
$$ \rho^+(X|Z) \leq \rho^+(X)$$
theorem
condRho_eq
{G : Type uG}
[AddCommGroup G]
[hGm : MeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X : Ω → G}
{A : Finset G}
{S : Type u_2}
[Fintype S]
{Z : Ω → S}
:
theorem
condRho_le
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X : Ω → G}
{A : Finset G}
[MeasureTheory.IsProbabilityMeasure μ]
{S : Type u_2}
[MeasurableSpace S]
[Fintype S]
[MeasurableSingletonClass S]
{Z : Ω → S}
(hX : Measurable X)
(hZ : Measurable Z)
(hA : A.Nonempty)
:
$$ \rho(X|Z) \leq \rho(X) + \frac{1}{2}( \bbH[X] - \bbH[X|Z] )$$
theorem
condRho_prod_eq_sum
{G : Type uG}
[AddCommGroup G]
[hGm : MeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X : Ω → G}
{A : Finset G}
[MeasureTheory.IsProbabilityMeasure μ]
{S : Type u_2}
[MeasurableSpace S]
[Fintype S]
[MeasurableSingletonClass S]
{Z T : Ω → S}
(hZ : Measurable Z)
(hT : Measurable T)
:
ρ[X | ⟨Z, T⟩ ; μ # A] = ∑ g : S, (μ (T ⁻¹' {g})).toReal * ρ[X | Z ; ProbabilityTheory.cond μ (T ⁻¹' {g}) # A]
theorem
condRho_prod_le
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X : Ω → G}
{A : Finset G}
[MeasureTheory.IsProbabilityMeasure μ]
{S : Type u_2}
[MeasurableSpace S]
[Fintype S]
[MeasurableSingletonClass S]
{Z T : Ω → S}
(hX : Measurable X)
(hZ : Measurable Z)
(hT : Measurable T)
(hA : A.Nonempty)
:
$$ \rho(X|Z) \leq \rho(X) + \frac{1}{2}( \bbH[X] - \bbH[X|Z] )$$, conditional version
theorem
condRho_prod_eq_of_indepFun
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{A : Finset G}
[MeasureTheory.IsProbabilityMeasure μ]
{X : Ω → G}
{S : Type u_2}
[Fintype S]
[MeasurableSpace S]
[MeasurableSingletonClass S]
{W W' : Ω → S}
(hX : Measurable X)
(hW : Measurable W)
(hW' : Measurable W')
(h : ProbabilityTheory.IndepFun (⟨X, W⟩) W' μ)
:
ρ[X | ⟨W, W'⟩ ; μ # A] = ρ[X | W ; μ # A]
theorem
rho_of_sum_le
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X Y : Ω → G}
{A : Finset G}
[Module (ZMod 2) G]
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
(hX : Measurable X)
(hY : Measurable Y)
(hA : A.Nonempty)
(h_indep : ProbabilityTheory.IndepFun X Y μ)
:
If $X,Y$ are independent, then $$ \rho(X+Y) \leq \frac{1}{2}(\rho(X)+\rho(Y) + d[X;Y]).$$
theorem
condRho_of_sum_le
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{X Y : Ω → G}
{A : Finset G}
[Module (ZMod 2) G]
[MeasureTheory.IsProbabilityMeasure μ]
(hX : Measurable X)
(hY : Measurable Y)
(hA : A.Nonempty)
(h_indep : ProbabilityTheory.IndepFun X Y μ)
:
If $X,Y$ are independent, then $$ \rho(X | X+Y) \leq \frac{1}{2}(\rho(X)+\rho(Y) + d[X;Y]).$$
noncomputable def
phi
{G : Type uG}
[AddCommGroup G]
[hGm : MeasurableSpace G]
{Ω : Type u_2}
[MeasurableSpace Ω]
(X Y : Ω → G)
(η : ℝ)
(A : Finset G)
(μ : MeasureTheory.Measure Ω)
:
Given $G$-valued random variables $X,Y$, define $$ \phi[X;Y] := d[X;Y] + \eta(\rho(X) + \rho(Y))$$.
Instances For
def
phiMinimizes
{G : Type uG}
[AddCommGroup G]
[hGm : MeasurableSpace G]
{Ω : Type u_2}
[MeasurableSpace Ω]
(X Y : Ω → G)
(η : ℝ)
(A : Finset G)
(μ : MeasureTheory.Measure Ω)
:
Given $G$-valued random variables $X,Y$, define $$ \phi[X;Y] := d[X;Y] + \eta(\rho(X) + \rho(Y))$$ and define a \emph{$\phi$-minimizer} to be a pair of random variables $X,Y$ which minimizes $\phi[X;Y]$.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
phiMinimizes_of_identDistrib
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{Ω' : Type u_2}
[MeasureTheory.MeasureSpace Ω']
{X Y : Ω → G}
{X' Y' : Ω' → G}
{η : ℝ}
{A : Finset G}
(h_min : phiMinimizes X Y η A MeasureTheory.volume)
(h₁ : ProbabilityTheory.IdentDistrib X X' MeasureTheory.volume MeasureTheory.volume)
(h₂ : ProbabilityTheory.IdentDistrib Y Y' MeasureTheory.volume MeasureTheory.volume)
:
phiMinimizes X' Y' η A MeasureTheory.volume
theorem
phiMinimizes_comm
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
{X Y : Ω → G}
{η : ℝ}
{A : Finset G}
(h_min : phiMinimizes X Y η A MeasureTheory.volume)
:
phiMinimizes Y X η A MeasureTheory.volume
theorem
phi_min_exists
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{A : Finset G}
{η : ℝ}
(hA : A.Nonempty)
:
∃ (μ : MeasureTheory.Measure (G × G)), MeasureTheory.IsProbabilityMeasure μ ∧ phiMinimizes Prod.fst Prod.snd η A μ
There exists a $\phi$-minimizer.
theorem
le_rdist_of_phiMinimizes
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{A : Finset G}
{η : ℝ}
{X₁ X₂ : Ω → G}
(h_min : phiMinimizes X₁ X₂ η A MeasureTheory.volume)
{Ω₁ : Type u_2}
{Ω₂ : Type u_3}
[MeasurableSpace Ω₁]
[MeasurableSpace Ω₂]
{μ₁ : MeasureTheory.Measure Ω₁}
{μ₂ : MeasureTheory.Measure Ω₂}
[MeasureTheory.IsProbabilityMeasure μ₁]
[MeasureTheory.IsProbabilityMeasure μ₂]
{X₁' : Ω₁ → G}
{X₂' : Ω₂ → G}
(hX₁' : Measurable X₁')
(hX₂' : Measurable X₂')
:
theorem
le_rdist_of_phiMinimizes'
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{A : Finset G}
{η : ℝ}
{X₁ X₂ : Ω → G}
(h_min : phiMinimizes X₁ X₂ η A MeasureTheory.volume)
{Ω₁ : Type u_2}
{Ω₂ : Type u_3}
[MeasurableSpace Ω₁]
[MeasurableSpace Ω₂]
{μ₁ : MeasureTheory.Measure Ω₁}
{μ₂ : MeasureTheory.Measure Ω₂}
[MeasureTheory.IsProbabilityMeasure μ₁]
[MeasureTheory.IsProbabilityMeasure μ₂]
{X₁' : Ω₁ → G}
{X₂' : Ω₂ → G}
(hX₁' : Measurable X₁')
(hX₂' : Measurable X₂')
:
theorem
condRho_le_condRuzsaDist_of_phiMinimizes
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{A : Finset G}
{η : ℝ}
{X₁ X₂ X₁' X₂' : Ω → G}
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
{S : Type u_2}
{T : Type u_3}
[Fintype S]
[MeasurableSpace S]
[MeasurableSingletonClass S]
[Fintype T]
[MeasurableSpace T]
[MeasurableSingletonClass T]
(h : phiMinimizes X₁ X₂ η A MeasureTheory.volume)
(h1 : Measurable X₁')
(h2 : Measurable X₂')
{Z : Ω → S}
{W : Ω → T}
(hZ : Measurable Z)
(hW : Measurable W)
:
theorem
I_one_le
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{A : Finset G}
{η : ℝ}
(hη : 0 < η)
{X₁ X₂ X₁' X₂' : Ω → G}
(h_min : phiMinimizes X₁ X₂ η A MeasureTheory.volume)
(h₁ : ProbabilityTheory.IdentDistrib X₁ X₁' MeasureTheory.volume MeasureTheory.volume)
(h₂ : ProbabilityTheory.IdentDistrib X₂ X₂' MeasureTheory.volume MeasureTheory.volume)
(h_indep :
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hGm) ![X₁, X₂, X₁', X₂']
MeasureTheory.volume)
(hX₁ : Measurable X₁)
(hX₂ : Measurable X₂)
(hX₁' : Measurable X₁')
(hX₂' : Measurable X₂')
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
[Module (ZMod 2) G]
(hA : A.Nonempty)
:
$I_1\le 2\eta d[X_1;X_2]$
theorem
I_two_aux
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{X₁ X₂ X₁' X₂' : Ω → G}
(h₁ : ProbabilityTheory.IdentDistrib X₁ X₁' MeasureTheory.volume MeasureTheory.volume)
(h₂ : ProbabilityTheory.IdentDistrib X₂ X₂' MeasureTheory.volume MeasureTheory.volume)
(h_indep :
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hGm) ![X₁, X₂, X₁', X₂']
MeasureTheory.volume)
(hX₁ : Measurable X₁)
(hX₂ : Measurable X₂)
(hX₁' : Measurable X₁')
(hX₂' : Measurable X₂')
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
[Module (ZMod 2) G]
:
theorem
rdist_add_rdist_eq
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{X₁ X₂ X₁' X₂' : Ω → G}
(h₁ : ProbabilityTheory.IdentDistrib X₁ X₁' MeasureTheory.volume MeasureTheory.volume)
(h₂ : ProbabilityTheory.IdentDistrib X₂ X₂' MeasureTheory.volume MeasureTheory.volume)
(h_indep :
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hGm) ![X₁, X₂, X₁', X₂']
MeasureTheory.volume)
(hX₁ : Measurable X₁)
(hX₂ : Measurable X₂)
(hX₁' : Measurable X₁')
(hX₂' : Measurable X₂')
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
[Module (ZMod 2) G]
:
$d[X_1;X_1]+d[X_2;X_2]= 2d[X_1;X_2]+(I_2-I_1)$.
theorem
I_two_aux'
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{X₁ X₂ X₁' X₂' : Ω → G}
(h₁ : ProbabilityTheory.IdentDistrib X₁ X₁' MeasureTheory.volume MeasureTheory.volume)
(h₂ : ProbabilityTheory.IdentDistrib X₂ X₂' MeasureTheory.volume MeasureTheory.volume)
(h_indep :
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hGm) ![X₁, X₂, X₁', X₂']
MeasureTheory.volume)
(hX₁ : Measurable X₁)
(hX₂ : Measurable X₂)
(hX₁' : Measurable X₁')
(hX₂' : Measurable X₂')
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
[Module (ZMod 2) G]
:
theorem
I_two_le
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{A : Finset G}
{η : ℝ}
(hη : 0 < η)
{X₁ X₂ X₁' X₂' : Ω → G}
(h_min : phiMinimizes X₁ X₂ η A MeasureTheory.volume)
(h₁ : ProbabilityTheory.IdentDistrib X₁ X₁' MeasureTheory.volume MeasureTheory.volume)
(h₂ : ProbabilityTheory.IdentDistrib X₂ X₂' MeasureTheory.volume MeasureTheory.volume)
(h_indep :
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hGm) ![X₁, X₂, X₁', X₂']
MeasureTheory.volume)
(hX₁ : Measurable X₁)
(hX₂ : Measurable X₂)
(hX₁' : Measurable X₁')
(hX₂' : Measurable X₂')
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
[Module (ZMod 2) G]
(hA : A.Nonempty)
(h'η : η < 1)
:
$I_2\le 2\eta d[X_1;X_2] + \frac{\eta}{1-\eta}(2\eta d[X_1;X_2]-I_1)$.
theorem
dist_le_of_sum_zero
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{A : Finset G}
{η : ℝ}
{X₁ X₂ : Ω → G}
(h_min : phiMinimizes X₁ X₂ η A MeasureTheory.volume)
[Module (ZMod 2) G]
{Ω' : Type u_2}
[MeasurableSpace Ω']
{μ : MeasureTheory.Measure Ω'}
[MeasureTheory.IsProbabilityMeasure μ]
{T₁ T₂ T₃ : Ω' → G}
(hsum : T₁ + T₂ + T₃ = 0)
(hT₁ : Measurable T₁)
(hT₂ : Measurable T₂)
(hT₃ : Measurable T₃)
:
If $G$-valued random variables $T_1,T_2,T_3$ satisfy $T_1+T_2+T_3=0$, then $$d[X_1;X_2]\le 3\bbI[T_1:T_2\mid T_3] + (2\bbH[T_3]-\bbH[T_1]-\bbH[T_2])+ \eta(\rho(T_1|T_3)+\rho(T_2|T_3)-\rho(X_1)-\rho(X_2)).$$
theorem
dist_le_of_sum_zero_cond
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{A : Finset G}
{η : ℝ}
{X₁ X₂ : Ω → G}
(h_min : phiMinimizes X₁ X₂ η A MeasureTheory.volume)
[Module (ZMod 2) G]
{Ω' : Type u_2}
[MeasureTheory.MeasureSpace Ω']
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
{T₁ T₂ T₃ S : Ω' → G}
(hsum : T₁ + T₂ + T₃ = 0)
(hT₁ : Measurable T₁)
(hT₂ : Measurable T₂)
(hT₃ : Measurable T₃)
(hS : Measurable S)
:
If $G$-valued random variables $T_1,T_2,T_3$ satisfy $T_1+T_2+T_3=0$, then $$d[X_1;X_2]\le 3\bbI[T_1:T_2\mid T_3] + (2\bbH[T_3]-\bbH[T_1]-\bbH[T_2])+ \eta(\rho(T_1|T_3)+\rho(T_2|T_3)-\rho(X_1)-\rho(X_2)).$$
theorem
dist_le_of_sum_zero'
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{A : Finset G}
{η : ℝ}
{X₁ X₂ : Ω → G}
(h_min : phiMinimizes X₁ X₂ η A MeasureTheory.volume)
[Module (ZMod 2) G]
{Ω' : Type u_2}
[MeasureTheory.MeasureSpace Ω']
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
{T₁ T₂ T₃ : Ω' → G}
(hsum : T₁ + T₂ + T₃ = 0)
(hT₁ : Measurable T₁)
(hT₂ : Measurable T₂)
(hT₃ : Measurable T₃)
:
If $G$-valued random variables $T_1,T_2,T_3$ satisfy $T_1+T_2+T_3=0$, then $$d[X_1;X_2] \leq \sum_{1 \leq i < j \leq 3} \bbI[T_i:T_j]
- \frac{\eta}{3} \sum_{1 \leq i < j \leq 3} (\rho(T_i|T_j) + \rho(T_j|T_i) -\rho(X_1)-\rho(X_2))$$
theorem
dist_le_of_sum_zero_cond'
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{A : Finset G}
{η : ℝ}
{X₁ X₂ : Ω → G}
(h_min : phiMinimizes X₁ X₂ η A MeasureTheory.volume)
[Module (ZMod 2) G]
{Ω' : Type u_2}
[MeasureTheory.MeasureSpace Ω']
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
{T₁ T₂ T₃ : Ω' → G}
(S : Ω' → G)
(hsum : T₁ + T₂ + T₃ = 0)
(hT₁ : Measurable T₁)
(hT₂ : Measurable T₂)
(hT₃ : Measurable T₃)
(hS : Measurable S)
:
If $G$-valued random variables $T_1,T_2,T_3$ satisfy $T_1+T_2+T_3=0$, then $$d[X_1;X_2] \leq \sum_{1 \leq i < j \leq 3} \bbI[T_i:T_j]
- \frac{\eta}{3} \sum_{1 \leq i < j \leq 3} (\rho(T_i|T_j) + \rho(T_j|T_i) -\rho(X_1)-\rho(X_2))$$
theorem
new_gen_ineq_aux1
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{A : Finset G}
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
[Module (ZMod 2) G]
{Y₁ Y₂ Y₃ Y₄ : Ω → G}
(hY₁ : Measurable Y₁)
(hY₂ : Measurable Y₂)
(hY₃ : Measurable Y₃)
(hY₄ : Measurable Y₄)
(h_indep :
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hGm) ![Y₁, Y₂, Y₃, Y₄] MeasureTheory.volume)
(hA : A.Nonempty)
:
theorem
new_gen_ineq_aux2
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{A : Finset G}
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
[Module (ZMod 2) G]
{Y₁ Y₂ Y₃ Y₄ : Ω → G}
(hY₁ : Measurable Y₁)
(hY₂ : Measurable Y₂)
(hY₃ : Measurable Y₃)
(hY₄ : Measurable Y₄)
(h_indep :
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hGm) ![Y₁, Y₂, Y₃, Y₄] MeasureTheory.volume)
(hA : A.Nonempty)
:
theorem
new_gen_ineq
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{A : Finset G}
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
[Module (ZMod 2) G]
{Y₁ Y₂ Y₃ Y₄ : Ω → G}
(hY₁ : Measurable Y₁)
(hY₂ : Measurable Y₂)
(hY₃ : Measurable Y₃)
(hY₄ : Measurable Y₄)
(h_indep :
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hGm) ![Y₁, Y₂, Y₃, Y₄] MeasureTheory.volume)
(hA : A.Nonempty)
:
theorem
condRho_sum_le
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{A : Finset G}
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
[Module (ZMod 2) G]
{Y₁ Y₂ Y₃ Y₄ : Ω → G}
(hY₁ : Measurable Y₁)
(hY₂ : Measurable Y₂)
(hY₃ : Measurable Y₃)
(hY₄ : Measurable Y₄)
(h_indep :
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hGm) ![Y₁, Y₂, Y₃, Y₄] MeasureTheory.volume)
(hA : A.Nonempty)
:
For independent random variables $Y_1,Y_2,Y_3,Y_4$ over $G$, define $S:=Y_1+Y_2+Y_3+Y_4$, $T_1:=Y_1+Y_2$, $T_2:=Y_1+Y_3$. Then $$\rho(T_1|T_2,S)+\rho(T_2|T_1,S) - \frac{1}{2}\sum_{i} \rho(Y_i) \le \frac{1}{2}(d[Y_1;Y_2]+d[Y_3;Y_4]+d[Y_1;Y_3]+d[Y_2;Y_4]).$$
theorem
condRho_sum_le'
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{A : Finset G}
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
[Module (ZMod 2) G]
{Y₁ Y₂ Y₃ Y₄ : Ω → G}
(hY₁ : Measurable Y₁)
(hY₂ : Measurable Y₂)
(hY₃ : Measurable Y₃)
(hY₄ : Measurable Y₄)
(h_indep :
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hGm) ![Y₁, Y₂, Y₃, Y₄] MeasureTheory.volume)
(hA : A.Nonempty)
:
let S := Y₁ + Y₂ + Y₃ + Y₄;
let T₁ := Y₁ + Y₂;
let T₂ := Y₁ + Y₃;
let T₃ := Y₂ + Y₃;
ρ[T₁ | ⟨T₂, S⟩ # A] + ρ[T₂ | ⟨T₁, S⟩ # A] + ρ[T₁ | ⟨T₃, S⟩ # A] + ρ[T₃ | ⟨T₁, S⟩ # A] + ρ[T₂ | ⟨T₃, S⟩ # A] + ρ[T₃ | ⟨T₂, S⟩ # A] - 3 * (ρ[Y₁ # A] + ρ[Y₂ # A] + ρ[Y₃ # A] + ρ[Y₄ # A]) / 2 ≤ d[Y₁ # Y₂] + d[Y₁ # Y₃] + d[Y₁ # Y₄] + d[Y₂ # Y₃] + d[Y₂ # Y₄] + d[Y₃ # Y₄]
For independent random variables $Y_1,Y_2,Y_3,Y_4$ over $G$, define $T_1:=Y_1+Y_2, T_2:=Y_1+Y_3, T_3:=Y_2+Y_3$ and $S:=Y_1+Y_2+Y_3+Y_4$. Then $$\sum_{1 \leq i < j \leq 3} (\rho(T_i|T_j,S) + \rho(T_j|T_i,S) - \frac{1}{2}\sum_{i} \rho(Y_i))\le \sum_{1\leq i < j \leq 4}d[Y_i;Y_j]$$
theorem
dist_of_min_eq_zero'
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{A : Finset G}
{η : ℝ}
(hη : 0 < η)
{X₁ X₂ X₁' X₂' : Ω → G}
(h_min : phiMinimizes X₁ X₂ η A MeasureTheory.volume)
(h₁ : ProbabilityTheory.IdentDistrib X₁ X₁' MeasureTheory.volume MeasureTheory.volume)
(h₂ : ProbabilityTheory.IdentDistrib X₂ X₂' MeasureTheory.volume MeasureTheory.volume)
(h_indep :
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hGm) ![X₁, X₂, X₁', X₂']
MeasureTheory.volume)
(hX₁ : Measurable X₁)
(hX₂ : Measurable X₂)
(hX₁' : Measurable X₁')
(hX₂' : Measurable X₂')
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
[Module (ZMod 2) G]
(hA : A.Nonempty)
(hη' : η < 1 / 8)
:
d[X₁ # X₂] = 0
If $X_1, X_2$ is a $\phi$-minimizer, then $d[X_1;X_2] = 0$.
theorem
dist_of_min_eq_zero
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{A : Finset G}
{η : ℝ}
(hη : 0 < η)
{X₁ X₂ : Ω → G}
(h_min : phiMinimizes X₁ X₂ η A MeasureTheory.volume)
(hX₁ : Measurable X₁)
(hX₂ : Measurable X₂)
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
[Module (ZMod 2) G]
(hA : A.Nonempty)
(hη' : η < 1 / 8)
:
d[X₁ # X₂] = 0
theorem
phiMinimizer_exists_rdist_eq_zero
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[hGm : MeasurableSpace G]
[DiscreteMeasurableSpace G]
{A : Finset G}
[Module (ZMod 2) G]
(hA : A.Nonempty)
:
∃ (Ω : Type uG) (x : MeasureTheory.MeasureSpace Ω) (X₁ : Ω → G) (X₂ : Ω → G),
Measurable X₁ ∧ Measurable X₂ ∧ MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧ phiMinimizes X₁ X₂ (1 / 8) A MeasureTheory.volume ∧ d[X₁ # X₂] = 0
For η ≤ 1/8, there exist phi-minimizers X₁, X₂ at zero Rusza distance. For η < 1/8,
all minimizers are fine, by dist_of_min_eq_zero. For η = 1/8, we use a limit of
minimizers for η < 1/8, which exists by compactness.
theorem
rho_PFR_conjecture
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[Module (ZMod 2) G]
{Ω : Type uG}
[MeasureTheory.MeasureSpace Ω]
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
[MeasurableSpace G]
[DiscreteMeasurableSpace G]
(Y₁ Y₂ : Ω → G)
(hY₁ : Measurable Y₁)
(hY₂ : Measurable Y₂)
(A : Finset G)
(hA : A.Nonempty)
:
∃ (H : Submodule (ZMod 2) G) (Ω' : Type uG) (mΩ' : MeasureTheory.MeasureSpace Ω') (U : Ω' → G),
MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧ Measurable U ∧ ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume ∧ 2 * ρ[U # A] ≤ ρ[Y₁ # A] + ρ[Y₂ # A] + 8 * d[Y₁ # Y₂]
For any random variables $Y_1,Y_2$, there exist a subgroup $H$ such that $$ 2\rho(U_H) \leq \rho(Y_1) + \rho(Y_2) + 8 d[Y_1;Y_2].$$
theorem
better_PFR_conjecture_aux0
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[Module (ZMod 2) G]
{A : Set G}
(h₀A : A.Nonempty)
{K : ℝ}
(hA : ↑(Nat.card ↑(A + A)) ≤ K * ↑(Nat.card ↑A))
:
If $|A+A| \leq K|A|$, then there exists a subgroup $H$ and $t\in G$ such that $|A \cap (H+t)| \geq K^{-4} \sqrt{|A||V|}$, and $|H|/|A|\in[K^{-8},K^8]$.
theorem
better_PFR_conjecture_aux
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[Module (ZMod 2) G]
{A : Set G}
(h₀A : A.Nonempty)
{K : ℝ}
(hA : ↑(Nat.card ↑(A + A)) ≤ K * ↑(Nat.card ↑A))
:
Auxiliary statement towards the polynomial Freiman-Ruzsa (PFR) conjecture: if $A$ is a subset of an elementary abelian 2-group of doubling constant at most $K$, then there exists a subgroup $H$ such that $A$ can be covered by at most $K^5 |A|^{1/2} / |H|^{1/2}$ cosets of $H$, and $H$ has the same cardinality as $A$ up to a multiplicative factor $K^8$.
theorem
better_PFR_conjecture
{G : Type uG}
[AddCommGroup G]
[Fintype G]
[Module (ZMod 2) G]
{A : Set G}
(h₀A : A.Nonempty)
{K : ℝ}
(hA : ↑(Nat.card ↑(A + A)) ≤ K * ↑(Nat.card ↑A))
:
If $A \subset {\bf F}_2^n$ is finite non-empty with $|A+A| \leq K|A|$, then there exists a subgroup $H$ of ${\bf F}_2^n$ with $|H| \leq |A|$ such that $A$ can be covered by at most $2K^9$ translates of $H$.
theorem
better_PFR_conjecture'
{G : Type u_1}
[AddCommGroup G]
[Module (ZMod 2) G]
{A : Set G}
{K : ℝ}
(h₀A : A.Nonempty)
(Afin : A.Finite)
(hA : ↑(Nat.card ↑(A + A)) ≤ K * ↑(Nat.card ↑A))
:
Corollary of better_PFR_conjecture in which the ambient group is not required to be finite
(but) then $H$ and $c$ are finite.