noncomputable def BKTProof.l2NormSqHighFreq {α : Type u_1} (S : Finset α) (f : α → ℂ) : ℝ

The squared $L^2$-norm of the high-frequency part of f on a finite set S, i.e. ∑_{x ∈ S} |f(x) − μ_S(f)|², where μ_S(f) = (1/|S|) ∑_{y ∈ S} f(y) is the average of f over S. This is ‖f_h‖_{L^2(S)}² in the notation of BKT.

theorem BKTProof.l2NormSqHighFreq_mono_of_subset {α : Type u_1} [DecidableEq α] {S T : Finset α} (hST : S ⊆ T) (hS : S.Nonempty) (f : α → ℂ) : l2NormSqHighFreq S f ≤ l2NormSqHighFreq T f

Monotonicity of the high-frequency squared norm under enlarging the domain: if S ⊆ T and S is nonempty, then ‖f_h‖²_{L^2(S)} ≤ ‖f_h‖²_{L^2(T)}. The proof expands the mean of f on T versus the mean on S and uses that the cross-term vanishes because ∑_{x ∈ S} (f(x) − μ_S) = 0.

noncomputable def BKTProof.l2NormHighFreq {α : Type u_1} (S : Finset α) (f : α → ℂ) : ℝ

The high-frequency $L^2$-norm of f on a finite set S, namely ‖f_h‖_{L^2(S)} = √(∑_{x ∈ S} |f(x) − μ_S(f)|²).

theorem BKTProof.l2NormHighFreq_mono_of_subset {α : Type u_1} [DecidableEq α] {S T : Finset α} (hST : S ⊆ T) (hS : S.Nonempty) (f : α → ℂ) : l2NormHighFreq S f ≤ l2NormHighFreq T f

Square-root version of monotonicity: ‖f_h‖_{L^2(S)} ≤ ‖f_h‖_{L^2(T)} whenever S ⊆ T and S is nonempty.

theorem BKTProof.bkt_lemma3 (q : ℕ) [NeZero q] (f : ZMod q → ℂ) : l2NormHighFreq {x : ZMod q | IsUnit x} f ≤ l2NormHighFreq Finset.univ f

BKT Lemma 3 (Subsection 7.3 of BKT): the high-frequency $L^2$-norm of f restricted to the units ℤ_q^* is at most its high-frequency $L^2$-norm on all of ℤ_q, i.e. ‖f_h^*‖_{L^2(ℤ_q^*)} ≤ ‖f_h‖_{L^2(ℤ_q)}.