`PFR/Examples.lean`

34 declarations, 0 contain sorry, 0 declared as axioms

Imports (5)

Imported by 1 file

PFR.lean

example (example at line 16) line 16 source

Source documentation

A self-contained version of the PFR conjecture using only Mathlib definitions.

example {A : Set G} {K : ℝ} (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤ K * Nat.card A) :
    ∃ (H : Submodule (ZMod 2) G) (c : Set G),
      Nat.card c < 2 * K ^ 12 ∧ Nat.card H ≤ Nat.card A ∧ A ⊆ c + H := by
…

example (example at line 27) line 27 source

Source documentation

The improved version

example {A : Set G} {K : ℝ} (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤ K * Nat.card A) :
    ∃ (H : Submodule (ZMod 2) G) (c : Set G),
      Nat.card c < 2 * K ^ 11 ∧ Nat.card H ≤ Nat.card A ∧ A ⊆ c + H := by
…

example (example at line 38) line 38 source

Source documentation

The even more improved version

example {A : Set G} {K : ℝ} (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤ K * Nat.card A) :
    ∃ (H : Submodule (ZMod 2) G) (c : Set G),
      Nat.card c < 2 * K ^ 9 ∧ Nat.card H ≤ Nat.card A ∧ A ⊆ c + H := by
…

example (example at line 49) line 49 source

Source documentation

The homomorphism version of PFR.

example (f : G → G') (S : Set G') (hS : ∀ x y : G, f (x + y) - f x - f y ∈ S) :
    ∃ (φ : G →+ G') (T : Set G'), Nat.card T ≤ (Nat.card S)^10 ∧ ∀ x, f x - φ x ∈ T :=
…

example (example at line 54) line 54 source

Source documentation

The approximate homomorphism version of PFR

example (f : G → G') (K : ℝ) (hK : K > 0) [DecidableEq G']
    (hf : Finset.dens {x : G × G | f (x.1 + x.2) = f x.1 + f x.2} ≥ K⁻¹) :
    ∃ (φ : G →+ G') (c : G'),
      Nat.card {x : G | f x = φ x + c} ≥ (Nat.card G) / (2 ^ 144 * K ^ 122) :=
…

example (example at line 69) line 69 source

Source documentation

The bounded torsion version of PFR.

example {m : ℕ} (hm : m ≥ 2)
     (htorsion : ∀ x : G, m • x = 0) {A : Set G} [Finite A] {K : ℝ} (h₀A : A.Nonempty)
     (hA : Nat.card (A + A) ≤ K * A.ncard) :
     ∃ (H : AddSubgroup G) (c : Set G),
      Nat.card c < m * K ^ (256 * m ^ 3 + 1) ∧ (H : Set G).ncard ≤ A.ncard ∧ A ⊆ c + H := by
…

example (example at line 90) line 90 source

Source documentation

Weak PFR over the integers, difference-doubling form.

example (A : Set H) [Finite A] (h'A : A.Nonempty) (K : ℝ)
    (hA : Nat.card (A - A) ≤ K * Nat.card A) :
    ∃ A' : Set H, A' ⊆ A ∧ (Nat.card A') ≥ K ^ (-17 : ℝ) * (Nat.card A) ∧
    AffineSpace.finrank ℤ A' ≤ (40 / log 2) * log K :=
…

Mentions: AffineSpace.finrank

example (example at line 97) line 97 source

Source documentation

Weak PFR over the integers, sumset form as in [GGMT] Theorem 1.3.

example (A : Set H) (hA : A.Finite) (h'A : A.Nonempty) (K : ℝ)
    (hAK : Nat.card (A + A) ≤ K * Nat.card A) :
    ∃ A' ⊆ A, Nat.card A' ≥ K ^ (-34 : ℝ) * Nat.card A ∧
    AffineSpace.finrank ℤ A' ≤ (80 / log 2) * log K :=
…

Mentions: AffineSpace.finrank

example (example at line 117) line 117 source
example (example at line 119) line 119 source
example (example at line 121) line 121 source
example (example at line 124) line 124 source
example (example at line 129) line 129 source
Source documentation
A simple example of applying real-valued subtraction.
```
example (E F : Set Ω) (h : NullMeasurableSet F ℙ) : ℙᵣ (E ∩ F) = ℙᵣ E - ℙᵣ (E \ F) := by
…
```
example (example at line 133) line 133 source

example (example at line 159) line 159 source

Source documentation

$H[X]$ is the Shannon entropy of $X$.

example : H[X] =
    - ∑ x, ((ℙ : Measure Ω).map X).real {x} * Real.log (((ℙ : Measure Ω).map X).real {x}) := by
…

example (example at line 169) line 169 source
Source documentation
$\langle X,Y \rangle$ is the random variable formed by pairing $X$ and $Y$.
```
example (ω : Ω) : (⟨X, Y⟩) ω = (X ω, Y ω) := rfl
```
example (example at line 172) line 172 source
Source documentation
$H[X|Y]$ is the conditional entropy of $X$ relative to $Y$.
```
example : H[X|Y] = H[⟨X,Y⟩] - H[Y] := chain_rule'' ℙ hX hY
```
example (example at line 175) line 175 source
Source documentation
$I[X:Y]$ is the mutual information between $X$ and $Y$.
```
example : I[X:Y] = H[X] + H[Y] - H[⟨X,Y⟩] := rfl
```
example (example at line 178) line 178 source
Source documentation
$I[X:Y|Z]$ is the conditional mutual information between $X$ and $Y$ relative to $Z$.
```
example : I[X:Y|Z] = H[X|Z] + H[Y|Z] - H[⟨X,Y⟩|Z] := condMutualInfo_eq hX hY hZ ℙ
```
example (example at line 181) line 181 source
Source documentation
Submodularity: conditional information is nonnegative.
```
example : 0 ≤ I[X : Y | Z] := condMutualInfo_nonneg hX hY
```
example (example at line 184) line 184 source
Source documentation
Relation between conditional mutual information and conditional independence.
```
example : I[X : Y | Z] = 0 ↔ CondIndepFun X Y Z := condMutualInfo_eq_zero hX hY
…
```
example (example at line 204) line 204 source
Source documentation
d[X # Y] is the Ruzsa distance when X, Y are independent.
```
example (h : IndepFun X Y) : d[X # Y] = H[X-Y] - H[X]/2 - H[Y]/2 := h.rdist_eq hX hY
```
example (example at line 207) line 207 source
Source documentation
d[X # Y] depends only on the distribution of X and Y.
```
example (h1 : IdentDistrib X X') (h2 : IdentDistrib Y Y') : d[X # Y] = d[X' # Y'] :=
…
```
example (example at line 211) line 211 source
Source documentation
The Ruzsa triangle inequality.
```
example : d[X # Z] ≤ d[X # Y] + d[Y # Z] := rdist_triangle hX hY hZ
```
Mentions: rdist_triangle
example (example at line 214) line 214 source
Source documentation
The Kaimanovich-Vershik-Madiman inequality
```
example (h : iIndepFun ![X, Y, Z]) : H[X + Y + Z] - H[X + Y] ≤ H[Y + Z] - H[Y] :=
…
```

example (example at line 218) line 218 source

Source documentation

The entropic Balog--Szemeredi--Gowers inequality

example (h : Z = X + Y) :
    ((ℙ : Measure Ω).map Z)[fun z ↦ d[X ; ℙ[|Z ← z] # Y ; ℙ[|Z ← z]]]
      ≤ 3 * I[X : Y] + 2 * H[Z] - H[X] - H[Y] := by subst h; exact ent_bsg hX hY
…

Mentions: ent_bsg

example (example at line 229) line 229 source
example (example at line 231) line 231 source
example (example at line 233) line 233 source
example (example at line 235) line 235 source
example (example at line 236) line 236 source
example (example at line 238) line 238 source
example (example at line 240) line 240 source
example (example at line 244) line 244 source