Documentation

PFR.WeakPFR

Weak PFR over the integers #

Here we use the entropic form of PFR to deduce a weak form of PFR over the integers.

Main statement #

def IsShift {G : Type u_1} [AddCommGroup G] (A : Set G) (B : Set G) :

A set A is a shift of a set B if it can be written as x + B.

Equations
Instances For
    theorem IsShift.sub_self_congr {G : Type u_1} [AddCommGroup G] {A : Set G} {B : Set G} :
    IsShift A BA - A = B - B
    theorem IsShift.card_congr {G : Type u_1} [AddCommGroup G] {A : Set G} {B : Set G} :
    IsShift A BNat.card A = Nat.card B
    def NotInCoset {G : Type u_1} [AddCommGroup G] (A : Set G) (B : Set G) :

    The property of two sets A, B of a group G not being contained in cosets of the same proper subgroup

    Equations
    Instances For
      theorem wlog_notInCoset {G : Type u_1} [AddCommGroup G] {A : Set G} {B : Set G} (hA : A.Nonempty) (hB : B.Nonempty) :
      ∃ (G' : AddSubgroup G) (A' : Set G') (B' : Set G'), IsShift A (Subtype.val '' A') IsShift B (Subtype.val '' B') NotInCoset A' B'

      Without loss of generality, one can move (up to translation and embedding) any pair A, B of non-empty sets into a subgroup where they are not in a coset.

      theorem torsion_free_doubling {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableSingletonClass G] [Countable G] {Ω : Type u_2} {Ω' : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Ω'] (X : ΩG) (Y : Ω'G) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) (μ' : autoParam (MeasureTheory.Measure Ω') _auto✝) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) (hG : AddMonoid.IsTorsionFree G) :
      d[X ; μ # Y + Y ; μ'] 5 * d[X ; μ # Y ; μ']

      If G is torsion-free and X, Y are G-valued random variables then d[X ; 2Y] ≤ 5d[X ; Y].

      theorem torsion_dist_shrinking {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableSingletonClass G] [Countable G] {Ω : Type u_2} {Ω' : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Ω'] (X : ΩG) (Y : Ω'G) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) (μ' : autoParam (MeasureTheory.Measure Ω') _auto✝) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] {H : Type u_4} [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) [AddCommGroup H] [Module (ZMod 2) H] [MeasurableSpace H] [MeasurableSingletonClass H] [Countable H] (hG : AddMonoid.IsTorsionFree G) (φ : G →+ H) :
      H[φ X ; μ] 10 * d[X ; μ # Y ; μ']

      If G is a torsion-free group and X, Y are G-valued random variables and φ : G → 𝔽₂^d is a homomorphism then H[φ ∘ X ; μ] ≤ 10 * d[X ; μ # Y ; μ'].

      theorem app_ent_PFR' {G : Type u_1} [AddCommGroup G] [Module (ZMod 2) G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] {Ω : Type u_2} {Ω' : Type u_3} [mΩ : MeasureTheory.MeasureSpace Ω] [mΩ' : MeasureTheory.MeasureSpace Ω'] (X : ΩG) (Y : Ω'G) [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {α : } (hent : 20 * d[X # Y] < α * (H[X] + H[Y])) (hX : Measurable X) (hY : Measurable Y) :
      ∃ (H : Submodule (ZMod 2) G), Real.log (Nat.card H) < (1 + α) / 2 * (H[X] + H[Y]) H[H.mkQ X] + H[H.mkQ Y] < α * (H[X] + H[Y])

      Let $G=\mathbb{F}_2^n$ and X, Y be G-valued random variables such that [\mathbb{H}(X)+\mathbb{H}(Y)> (20/\alpha) d[X ;Y],] for some $\alpha > 0$. There is a non-trivial subgroup $H\leq G$ such that [\log \lvert H\rvert <(1+\alpha)/2 (\mathbb{H}(X)+\mathbb{H}(Y))] and [\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))< \alpha (\mathbb{H}(X)+\mathbb{H}(Y))] where $\psi:G\to G/H$ is the natural projection homomorphism.

      theorem app_ent_PFR {G : Type u_1} [AddCommGroup G] [Module (ZMod 2) G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] {Ω : Type u_2} {Ω' : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Ω'] (X : ΩG) (Y : Ω'G) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) (μ' : autoParam (MeasureTheory.Measure Ω') _auto✝) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] (α : ) (hent : 20 * d[X ; μ # Y ; μ'] < α * (H[X ; μ] + H[Y ; μ'])) (hX : Measurable X) (hY : Measurable Y) :
      ∃ (H : Submodule (ZMod 2) G), Real.log (Nat.card H) < (1 + α) / 2 * (H[X ; μ] + H[Y ; μ']) H[H.mkQ X ; μ] + H[H.mkQ Y ; μ'] < α * (H[X ; μ] + H[Y ; μ'])
      theorem PFR_projection' {G : Type u_1} [AddCommGroup G] [Module (ZMod 2) G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] {Ω : Type u_2} {Ω' : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Ω'] (X : ΩG) (Y : Ω'G) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) (μ' : autoParam (MeasureTheory.Measure Ω') _auto✝) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] (α : ) (hX : Measurable X) (hY : Measurable Y) (αpos : 0 < α) (αone : α < 1) :
      ∃ (H : Submodule (ZMod 2) G), Real.log (Nat.card H) (1 + α) / (2 * (1 - α)) * (H[X ; μ] + H[Y ; μ']) α * (H[H.mkQ X ; μ] + H[H.mkQ Y ; μ']) 20 * d[H.mkQ X ; μ # H.mkQ Y ; μ']

      If $G=\mathbb{F}_2^d$ and X, Y are G-valued random variables and $\alpha < 1$ then there is a subgroup $H\leq \mathbb{F}_2^d$ such that [\log \lvert H\rvert \leq (1 + α) / (2 * (1 - α)) * (\mathbb{H}(X)+\mathbb{H}(Y))] and if $\psi:G \to G/H$ is the natural projection then [\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))\leq 20/\alpha * d[\psi(X);\psi(Y)].]

      theorem PFR_projection {G : Type u_1} [AddCommGroup G] [Module (ZMod 2) G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] {Ω : Type u_2} {Ω' : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Ω'] (X : ΩG) (Y : Ω'G) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) (μ' : autoParam (MeasureTheory.Measure Ω') _auto✝) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] (hX : Measurable X) (hY : Measurable Y) :
      ∃ (H : Submodule (ZMod 2) G), Real.log (Nat.card H) 2 * (H[X ; μ] + H[Y ; μ']) H[H.mkQ X ; μ] + H[H.mkQ Y ; μ'] 34 * d[H.mkQ X ; μ # H.mkQ Y ; μ']

      If $G=\mathbb{F}_2^d$ and X, Y are G-valued random variables then there is a subgroup $H\leq \mathbb{F}_2^d$ such that [\log \lvert H\rvert \leq 2 * (\mathbb{H}(X)+\mathbb{H}(Y))] and if $\psi:G \to G/H$ is the natural projection then [\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))\leq 34 * d[\psi(X);\psi(Y)].]

      theorem four_logs {a : } {b : } {c : } {d : } (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hd : 0 < d) :
      theorem sum_prob_preimage {G : Type u_1} {H : Type u_2} {X : Finset H} {A : Set G} [Finite A] {φ : A{ x : H // x X }} {A_ : HSet G} (hA : A.Nonempty) (hφ : ∀ (x : { x : H // x X }), A_ x = Subtype.val '' (φ ⁻¹' {x})) :
      xX, (Nat.card (A_ x)) / (Nat.card A) = 1
      theorem single_fibres {G : Type u_1} {H : Type u_2} {Ω : Type u_3} {Ω' : Type u_4} [AddCommGroup G] [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup H] [Countable H] [MeasurableSpace H] [MeasurableSingletonClass H] [MeasureTheory.MeasureSpace Ω] [MeasureTheory.MeasureSpace Ω'] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (φ : G →+ H) {A : Set G} {B : Set G} [Finite A] [Finite B] {UA : ΩG} {UB : Ω'G} (hA : A.Nonempty) (hB : B.Nonempty) (hUA' : Measurable UA) (hUB' : Measurable UB) (hUA : ProbabilityTheory.IsUniform A UA MeasureTheory.volume) (hUB : ProbabilityTheory.IsUniform B UB MeasureTheory.volume) (hUA_mem : ∀ (ω : Ω), UA ω A) (hUB_mem : ∀ (ω : Ω'), UB ω B) :
      ∃ (x : H) (y : H) (Ax : Set G) (By : Set G), Ax = A (↑φ).toFun ⁻¹' {x} By = B (↑φ).toFun ⁻¹' {y} Ax.Nonempty By.Nonempty d[(↑φ).toFun UA # (↑φ).toFun UB] * Real.log ((Nat.card A) * (Nat.card B) / ((Nat.card Ax) * (Nat.card By))) (H[(↑φ).toFun UA] + H[(↑φ).toFun UB]) * (d[UA # UB] - dᵤ[Ax # By])

      Let $\phi : G\to H$ be a homomorphism and $A,B\subseteq G$ be finite subsets. If $x,y\in H$ then let $A_x=A\cap \phi^{-1}(x)$ and $B_y=B\cap \phi^{-1}(y)$. There exist $x,y\in H$ such that $A_x,B_y$ are both non-empty and [d[\phi(U_A);\phi(U_B)]\log \frac{\lvert A\rvert\lvert B\rvert}{\lvert A_x\rvert\lvert B_y\rvert} \leq (\mathbb{H}(\phi(U_A))+\mathbb{H}(\phi(U_B)))(d(U_A,U_B)-d(U_{A_x},U_{B_y}).]

      theorem third_iso {G : Type u_2} [AddCommGroup G] {G₂ : AddSubgroup G} (H' : AddSubgroup (G G₂)) :
      let H := G G₂; let φ := QuotientAddGroup.mk' G₂; let N := AddSubgroup.comap φ H'; ∃ (e : H H' ≃+ G N), ∀ (x : G), e ((QuotientAddGroup.mk' H') (φ x)) = (QuotientAddGroup.mk' N) x

      A version of the third isomorphism theorem: if G₂ ≤ G and H' is a subgroup of G⧸G₂, then there is a canonical isomorphism between H⧸H' and G⧸N, where N is the preimage of H' in G. A bit clunky; may be a better way to do this

      theorem single {Ω : Type u_2} [MeasurableSpace Ω] [DiscreteMeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {A : Set Ω} {z : Ω} (hA : μ.real A = 1) (hz : 0 < μ.real {z}) :
      z A
      theorem weak_PFR_asymm_prelim {G : Type u_1} [AddCommGroup G] [Module.Free G] [Module.Finite G] [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] (A : Set G) (B : Set G) [A_fin : Finite A] [B_fin : Finite B] (hnA : A.Nonempty) (hnB : B.Nonempty) :
      ∃ (N : AddSubgroup G) (x : G N) (y : G N) (Ax : Set G) (By : Set G), Ax.Nonempty By.Nonempty Ax.Finite By.Finite Ax = {z : G | z A (QuotientAddGroup.mk' N) z = x} By = {z : G | z B (QuotientAddGroup.mk' N) z = y} Real.log 2 * (Module.finrank G) Real.log (Nat.card (G N)) + 40 * dᵤ[A # B] Real.log (Nat.card A) + Real.log (Nat.card B) - Real.log (Nat.card Ax) - Real.log (Nat.card By) 34 * (dᵤ[A # B] - dᵤ[Ax # By])

      Given two non-empty finite subsets A, B of a rank n free Z-module G, there exists a subgroup N and points x, y in G/N such that the fibers Ax, By of A, B over x, y respectively are non-empty, one has the inequality $$\log\frac{|A| |B|}{|A_x| |B_y|} ≤ 34 (d[U_A; U_B] - d[U_{A_x}; U_{B_y}])$$ and one has the dimension bound $$n \log 2 ≤ \log |G/N| + 40 d[U_A; U_B]$$.

      def WeakPFRAsymmConclusion {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] (A : Set G) (B : Set G) :

      Separating out the conclusion of weak_PFR_asymm for convenience of induction arguments.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def not_in_coset {G : Type u_2} [AddCommGroup G] (A : Set G) (B : Set G) :

        The property of two sets A,B of a group G not being contained in cosets of the same proper subgroup

        Equations
        Instances For
          theorem dimension_of_shift {G : Type u_2} [AddCommGroup G] {H : AddSubgroup G} (A : Set H) (x : G) :
          AffineSpace.finrank ((fun (a : H) => a + x) '' A) = AffineSpace.finrank A

          In fact one has equality here, but this is trickier to prove and not needed for the argument.

          theorem conclusion_transfers {G : Type u_1} [AddCommGroup G] [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] {A : Set G} {B : Set G} (G' : AddSubgroup G) (A' : Set G') (B' : Set G') (hA : IsShift A (Subtype.val '' A')) (hB : IsShift B (Subtype.val '' B')) [Finite A'] [Finite B'] (hA' : A'.Nonempty) (hB' : B'.Nonempty) (h : WeakPFRAsymmConclusion A' B') :
          theorem weak_PFR_asymm {G : Type u_1} [AddCommGroup G] [Module.Free G] [Module.Finite G] [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] (A : Set G) (B : Set G) [Finite A] [Finite B] (hA : A.Nonempty) (hB : B.Nonempty) :

          If $A,B\subseteq \mathbb{Z}^d$ are finite non-empty sets then there exist non-empty $A'\subseteq A$ and $B'\subseteq B$ such that [\log\frac{\lvert A\rvert\lvert B\rvert}{\lvert A'\rvert\lvert B'\rvert}\leq 34 d[U_A;U_B]] such that $\max(\dim A',\dim B')\leq \frac{40}{\log 2} d[U_A;U_B]$.

          theorem weak_PFR {G : Type u_1} [AddCommGroup G] [Module.Free G] [Module.Finite G] [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] {A : Set G} [Finite A] {K : } (hA : A.Nonempty) (hK : 0 < K) (hdist : dᵤ[A # A] Real.log K) :
          A'A, K ^ (-17) * (Nat.card A) (Nat.card A') (AffineSpace.finrank A') 40 / Real.log 2 * Real.log K

          If $A\subseteq \mathbb{Z}^d$ is a finite non-empty set with $d[U_A;U_A]\leq \log K$ then there exists a non-empty $A'\subseteq A$ such that $\lvert A'\rvert\geq K^{-17}\lvert A\rvert$ and $\dim A'\leq \frac{40}{\log 2} \log K$.

          theorem weak_PFR_int {G : Type u_2} [AddCommGroup G] [Module.Free G] [Module.Finite G] {A : Set G} [A_fin : Finite A] (hnA : A.Nonempty) {K : } (hA : (Nat.card (A - A)) K * (Nat.card A)) :
          A'A, (Nat.card A') K ^ (-17) * (Nat.card A) (AffineSpace.finrank A') 40 / Real.log 2 * Real.log K

          Let $A\subseteq \mathbb{Z}^d$ and $\lvert A-A\rvert\leq K\lvert A\rvert$. There exists $A'\subseteq A$ such that $\lvert A'\rvert \geq K^{-17}\lvert A\rvert$ and $\dim A' \leq \frac{40}{\log 2} \log K$.