theorem
lapply_linear_combination
{p : ℕ}
[fpprm : Fact (Nat.Prime p)]
{γ : Type u_1}
{γ₂ : Type u_2}
[Fintype γ]
[Fintype γ₂]
(a : FinPMF γ)
(b : FinPMF γ₂)
(f : γ → FinPMF (ZMod p))
(g : γ₂ → FinPMF (ZMod p × ZMod p × ZMod p))
:
lapply (FinPMF.linear_combination a f) (FinPMF.linear_combination b g) = FinPMF.linear_combination (a * b) fun (x : γ × γ₂) =>
match x with
| (x, y) => lapply (f x) (g y)
theorem
line_point_large_l2_aux
{p : ℕ}
[fpprm : Fact (Nat.Prime p)]
(n : ℕ+)
(β : ℝ)
(hβ : 0 < β)
(hkl : ↑p ^ β ≤ ↑↑n)
(hku : ↑↑n ≤ ↑p ^ (2 - β))
(a' : { x : Finset (ZMod p) // x.Nonempty })
(b' : { x : Finset (ZMod p × ZMod p × ZMod p) // x.Nonempty })
(hD : Set.InjOn Prod.snd ↑↑b')
(hbSz : (↑b').card ≤ ↑n)
:
theorem
line_point_large_l2'
{p : ℕ}
[fpprm : Fact (Nat.Prime p)]
(n : ℕ+)
(β : ℝ)
(hβ : 0 < β)
(hkl : ↑p ^ β ≤ ↑↑n)
(hku : ↑↑n ≤ ↑p ^ (2 - β))
(a : FinPMF (ZMod p))
(b : FinPMF (ZMod p × ZMod p × ZMod p))
(m : ℕ+)
(hm : m ≤ n)
(hD : Set.InjOn Prod.snd (Function.support ⇑b))
(hbSz : max_val b ≤ 1 / ↑↑m)
:
theorem
line_point_large_l2
{p : ℕ}
[fpprm : Fact (Nat.Prime p)]
(n : ℝ)
(β : ℝ)
(hβ : 0 < β)
(hβ2 : β < 1)
(hkl : ↑p ≤ n)
(hku : n ≤ ↑p ^ (2 - β))
(a : FinPMF (ZMod p))
(b : FinPMF (ZMod p × ZMod p × ZMod p))
(m : ℝ)
(hm : m ≤ n)
(hm₂ : 1 ≤ m)
(hD : Set.InjOn Prod.snd (Function.support ⇑b))
(hbSz : max_val b ≤ 1 / m)
:
theorem
bourgain_extractor_aux₃
{p : ℕ}
[fpprm : Fact (Nat.Prime p)]
[pnot2 : Fact (p ≠ 2)]
(b : FinPMF (ZMod p))
(hB : max_val b ≤ ↑p ^ (-1 / 2 + 2 / 11 * bourgainα))
:
close_high_entropy (↑p ^ (1 + 2 / 11 * bourgainα)) (8 * ↑ST_C * ↑p ^ (-2 / 11 * bourgainα))
(FinPMF.apply (lapply b (FinPMF.apply (b * b) lmap)) ⇑decoder)