theorem L1_le_card_rpow_mul_dft_norm {α : Type u_1} [αnonempty : Nonempty α] [Fintype α] [AddCommGroup α] (a : α → ℝ) : ‖a‖_[1] ≤ ↑(Fintype.card α) ^ (3 / 2) * ‖cft fun (x : α) => ↑(a x)‖_[⊤]

theorem lemma43 {α : Type u_1} [αnonempty : Nonempty α] [Fintype α] [AddCommGroup α] {β : Type u_2} [Nonempty β] [Fintype β] [AddCommGroup β] (a : α → ℝ) [DecidableEq β] (t : NNReal) (ε : NNReal) (h : ∀ (χ : AddChar α ℂ), AddChar.IsNontrivial χ → ‖cft (fun (x : α) => ↑(a x)) χ‖ ≤ ↑ε / ↑(Fintype.card α)) (σ : α → β) (h₂ : ∀ (χ : AddChar β ℂ), ‖cft (⇑χ ∘ σ)‖_[1] ≤ ↑t) : ‖σ # a - σ # Function.const α (Finset.expect Finset.univ fun (x : α) => a x)‖_[1] ≤ ↑t * ↑ε * √↑(Fintype.card β)

theorem range_eq_zmod_image (n : ℕ+) : Finset.range ↑n = Finset.image (fun (t : ZMod ↑n) => ZMod.val t) Finset.univ

theorem le_add_div_add_of_le_of_le (a : ℝ) (b : ℝ) (n : ℝ) (hb : 0 < b) (hn : 0 < n) (h : a / b ≤ n) : a / b ≤ (a + 1) / (b + 1 / n)

theorem circle_lower_bound (x : ℝ) : 2 - |4 * x - 2| ≤ ‖↑(Circle.e x) - 1‖

theorem bound_on_apply_uniform (n : ℕ+) (m : ℕ+) : ‖(fun (x : ZMod ↑n) => ↑(ZMod.val x)) # ⇑(Uniform { val := Finset.univ, property := ⋯ }) - ⇑(Uniform { val := Finset.univ, property := ⋯ })‖_[1] ≤ ↑↑m / ↑↑n

theorem lemma44 (n : ℕ+) (m : ℕ+) (χ : AddChar (ZMod ↑m) ℂ) : ‖cft (⇑χ ∘ fun (x : ZMod ↑n) => ↑(ZMod.val x))‖_[1] ≤ 6 * Real.log ↑↑n + 6

theorem generalized_XOR_lemma (n : ℕ+) (m : ℕ+) (ε : NNReal) (a : FinPMF (ZMod ↑n)) (h : ∀ (χ : AddChar (ZMod ↑n) ℂ), AddChar.IsNontrivial χ → ‖cft (fun (x : ZMod ↑n) => ↑(a x)) χ‖ ≤ ↑ε / ↑(Fintype.card (ZMod ↑n))) : SD (FinPMF.apply a fun (x : ZMod ↑n) => ↑(ZMod.val x)) (Uniform { val := Finset.univ, property := ⋯ }) ≤ ↑ε * √↑↑m * (3 * Real.log ↑↑n + 3) + ↑↑m / (2 * ↑↑n)