theorem AddChar.eq_iff {α : Type u_1} {R : Type u_3} (a : α) (b : α) [AddGroup α] [GroupWithZero R] (χ : AddChar α R) : χ a = χ b ↔ χ (a - b) = 1

def IP {α : Type u_1} [CommSemiring α] : LinearMap.BilinForm α (α × α)

Equations

• IP = LinearMap.mk₂ α (fun (x y : α × α) => x.1 * y.1 + x.2 * y.2) ⋯ ⋯ ⋯ ⋯

theorem IP_comm {α : Type u_1} [CommSemiring α] (a : α × α) (b : α × α) : (IP a) b = (IP b) a

theorem apply_inner_product_injective {α : Type u_1} [Field α] (χ : AddChar α ℂ) (h : AddChar.IsNontrivial χ) : Function.Injective fun (x : α × α) => { toFun := fun (y : α × α) => χ ((IP x) y), map_zero_one' := ⋯, map_add_mul' := ⋯ }

theorem apply_inner_product_bijective {α : Type u_1} [Fintype α] [Field α] (χ : AddChar α ℂ) (h : AddChar.IsNontrivial χ) : Function.Bijective fun (x : α × α) => { toFun := fun (y : α × α) => χ ((IP x) y), map_zero_one' := ⋯, map_add_mul' := ⋯ }

noncomputable def AddChar.inner_product_equiv {α : Type u_1} [Fintype α] [Field α] (χ : AddChar α ℂ) (h : AddChar.IsNontrivial χ) : α × α ≃ AddChar (α × α) ℂ

Equations

• AddChar.inner_product_equiv χ h = Equiv.ofBijective (fun (x : α × α) => { toFun := fun (y : α × α) => χ ((IP x) y), map_zero_one' := ⋯, map_add_mul' := ⋯ }) ⋯

theorem bourgain_extractor_aux_inner {α : Type u_1} [Fintype α] [Field α] (a : α × α → ℝ) (b : α × α → ℝ) (χ : AddChar α ℂ) (h : AddChar.IsNontrivial χ) : (Finset.sum Finset.univ fun (x : α × α) => ↑(a x) * Finset.sum Finset.univ fun (y : α × α) => ↑(b y) * χ ((IP x) y)) = l2Inner (⇑Complex.ofReal ∘ a) fun (x : α × α) => dft (fun (x : α × α) => ↑(b x)) ((AddChar.inner_product_equiv χ h) x)⁻¹

theorem bourgain_extractor_aux₀ {α : Type u_1} [Fintype α] [Field α] (a : α × α → ℝ) (b : α × α → ℝ) (χ : AddChar α ℂ) (h : AddChar.IsNontrivial χ) : ‖Finset.sum Finset.univ fun (x : α × α) => ↑(a x) * Finset.sum Finset.univ fun (y : α × α) => ↑(b y) * χ ((IP x) y)‖ ^ 2 ≤ ↑(Fintype.card α) ^ 2 * ‖a‖_[2] ^ 2 * ‖b‖_[2] ^ 2

theorem bourgain_extractor_aux₀' {α : Type u_1} [Fintype α] [Field α] (a : α × α → ℝ) (b : α × α → ℝ) (χ : AddChar α ℂ) (h : AddChar.IsNontrivial χ) : ‖Finset.sum Finset.univ fun (x : α × α) => ↑(a x) * Finset.sum Finset.univ fun (y : α × α) => ↑(b y) * χ ((IP x) y)‖ ≤ ↑(Fintype.card α) * ‖a‖_[2] * ‖b‖_[2]

theorem bourgain_extractor_aux₁ {α : Type u_1} {β : Type u_2} [Fintype α] [Field α] [Fintype β] [AddCommGroup β] [Module α β] [DecidableEq β] (a : FinPMF β) (b : FinPMF β) (χ : AddChar α ℂ) (F : LinearMap.BilinForm α β) : ‖Finset.sum Finset.univ fun (x : β) => ↑(a x) * Finset.sum Finset.univ fun (y : β) => ↑(b y) * χ ((F x) y)‖ ^ 2 ≤ ‖Finset.sum Finset.univ fun (x : β) => ↑(a x) * Finset.sum Finset.univ fun (y : β) => ↑((b - b) y) * χ ((F x) y)‖

theorem bourgain_extractor_aux₁' {α : Type u_1} {β : Type u_2} [Fintype α] [Field α] [Fintype β] [AddCommGroup β] [Module α β] [DecidableEq β] (a : FinPMF β) (b : FinPMF β) (χ : AddChar α ℂ) (F : LinearMap.BilinForm α β) : ‖Finset.sum Finset.univ fun (x : β) => ↑(a x) * Finset.sum Finset.univ fun (y : β) => ↑(b y) * χ ((F x) y)‖ ≤ ‖Finset.sum Finset.univ fun (x : β) => ↑(a x) * Finset.sum Finset.univ fun (y : β) => ↑((b - b) y) * χ ((F x) y)‖ ^ 2⁻¹

theorem bourgain_extractor_aux₂ {α : Type u_1} (ε : ℝ) (hε : 0 < ε) (n : ℝ) (hn : 0 < n) [Fintype α] [Field α] [DecidableEq α] (a : FinPMF (α × α)) (b : FinPMF (α × α)) (χ : AddChar α ℂ) (h : AddChar.IsNontrivial χ) (hA : close_high_entropy n ε a) (hB : close_high_entropy n ε b) : ‖Finset.sum Finset.univ fun (x : α × α) => ↑(a x) * Finset.sum Finset.univ fun (y : α × α) => ↑(b y) * χ ((IP x) y)‖ ≤ ↑(Fintype.card α) / n + 2 * ε