Khintchine inequality and empirical sampling

This file was automatically generated by Codex.

The Khintchine upper moment inequality for finite sums in real or complex inner product spaces, two independent sign randomizations, and the empirical sampling estimate for complex functions on arbitrary finite abelian groups. For exponent p at least two and n positive independent uniform samples, the expected pth power of the normalized Lp sampling error is at most (4 sqrt(p/n) times the Lp norm of the function) to the pth power. All statements and supporting definitions use only Mathlib and this module. The sampling theorem is extended to the Croot-Sisask almost-period argument using Markov's inequality, diagonal tuple fibers and translation invariance. Probability-normalized Fourier inversion and Parseval give the general trilinear correlation extraction estimate used by the finite inverse theorem.

Verified source: blueprint/formalization_blueprint.tex, lem:finite-fourier, lines 177-209. The proof uses independent-copy symmetrization, the Khintchine inequality and finite probability-space norm inequalities. The upper-moment proof is adapted from ../lean-variationalsw as attributed below.

noncomputable def TrilinearHT.Auto.finiteAverage {G : Type u_1} [Fintype G] (f : G → ℂ) : ℂ

Probability-counting expectation written as a finite sum.

Equations

• TrilinearHT.Auto.finiteAverage f = (↑(Fintype.card G))⁻¹ * ∑ x : G, f x

noncomputable def TrilinearHT.Auto.finiteConvolution {G : Type u_1} [Fintype G] [AddGroup G] (f g : G → ℂ) (x : G) : ℂ

Probability-normalized convolution, with the source's subtraction convention.

Equations

• TrilinearHT.Auto.finiteConvolution f g x = TrilinearHT.Auto.finiteAverage fun (y : G) => f y * g (x - y)

The following sign-moment helpers are adapted from ../lean-variationalsw/VariationalSW/Auto/KhintchineInequality.lean (Copyright 2026 Joris Roos, Apache 2.0; original author Claude). Only the upper-moment argument is needed here.

def TrilinearHT.Auto.rademacherSum {ι : Type u_1} [DecidableEq ι] {G : Type u_2} [AddCommGroup G] (s u : Finset ι) (v : ι → G) : G

The Rademacher signed sum ∑_{i ∈ s} ε_i v_i attached to the sign pattern u ⊆ s: ε_i = 1 if i ∈ u and ε_i = -1 otherwise.

Equations

• TrilinearHT.Auto.rademacherSum s u v = ∑ i ∈ s, if i ∈ u then v i else -v i

noncomputable def TrilinearHT.Auto.rademacherMean {ι : Type u_1} (s : Finset ι) (F : Finset ι → ℝ) : ℝ

The uniform average 2^{-|s|} ∑_{u ⊆ s} F u over all sign patterns on s.

Equations

• TrilinearHT.Auto.rademacherMean s F = (2 ^ s.card)⁻¹ * ∑ u ∈ s.powerset, F u

theorem TrilinearHT.Auto.rademacherSum_insert_of_subset {ι : Type u_1} [DecidableEq ι] {G : Type u_2} [AddCommGroup G] {s u : Finset ι} {a : ι} (ha : a ∉ s) (hu : u ⊆ s) (v : ι → G) : rademacherSum (insert a s) u v = -v a + rademacherSum s u v

Adding a new index a with sign -1.

theorem TrilinearHT.Auto.rademacherSum_insert_insert {ι : Type u_1} [DecidableEq ι] {G : Type u_2} [AddCommGroup G] {s u : Finset ι} {a : ι} (ha : a ∉ s) (v : ι → G) : rademacherSum (insert a s) (insert a u) v = v a + rademacherSum s u v

Adding a new index a with sign +1.

theorem TrilinearHT.Auto.two_point_pow_aux {P A w c : ℝ} (hP : 0 ≤ P) (hA : 0 ≤ A) (hw : w ^ 2 ≤ 4 * P * A) (hc : 1 ≤ c) (hQ : 0 < P + c * A) (m : ℕ) : 4 * ↑m ≤ c + 3 → (P + A + w) ^ m + (P + A - w) ^ m ≤ 2 * (P + c * A) ^ m ∧ (P + c * A) * (w * ((P + A + w) ^ m - (P + A - w) ^ m)) ≤ 2 * ↑m * w ^ 2 * (P + c * A) ^ m

Real two-point inequality driving the upper moment bound: if w² ≤ 4PA and 4m ≤ c + 3, 1 ≤ c, then (P+A+w)^m + (P+A-w)^m ≤ 2 (P + cA)^m.

theorem TrilinearHT.Auto.two_point_norm_pow (𝕜 : Type u_2) {H : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (x a : H) {μ c : ℝ} (hμ : 0 ≤ μ) (hc : 1 ≤ c) (n : ℕ) (hn : 4 * ↑n ≤ c + 3) : (‖x + a‖ ^ 2 + μ) ^ n + (‖x - a‖ ^ 2 + μ) ^ n ≤ 2 * (‖x‖ ^ 2 + μ + c * ‖a‖ ^ 2) ^ n

Two-point inequality in an inner product space: (‖x+a‖²+μ)^n + (‖x-a‖²+μ)^n ≤ 2 (‖x‖²+μ+c‖a‖²)^n whenever 1 ≤ c and 4n ≤ c+3.

theorem TrilinearHT.Auto.sum_powerset_norm_sq_add_pow_le {ι : Type u_1} [DecidableEq ι] (𝕜 : Type u_2) {H : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (s : Finset ι) (v : ι → H) {c : ℝ} (hc : 1 ≤ c) (n : ℕ) (hn : 4 * ↑n ≤ c + 3) (x : H) (μ : ℝ) : 0 ≤ μ → ∑ u ∈ s.powerset, (‖x + rademacherSum s u v‖ ^ 2 + μ) ^ n ≤ 2 ^ s.card * (‖x‖ ^ 2 + μ + c * ∑ i ∈ s, ‖v i‖ ^ 2) ^ n

Even-moment bound with a free base point: for 1 ≤ c, 4n ≤ c+3, μ ≥ 0, ∑_{u ⊆ s} (‖x + ∑ ε_i v_i‖² + μ)^n ≤ 2^{|s|} (‖x‖² + μ + c ∑ ‖v_i‖²)^n.

theorem TrilinearHT.Auto.sum_powerset_norm_rademacherSum_pow_le {ι : Type u_1} [DecidableEq ι] (𝕜 : Type u_2) {H : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (s : Finset ι) (v : ι → H) {c : ℝ} (hc : 1 ≤ c) (n : ℕ) (hn : 4 * ↑n ≤ c + 3) : ∑ u ∈ s.powerset, ‖rademacherSum s u v‖ ^ (2 * n) ≤ 2 ^ s.card * (c * ∑ i ∈ s, ‖v i‖ ^ 2) ^ n

Even moments: ∑_{u ⊆ s} ‖∑ ε_i v_i‖^{2n} ≤ 2^{|s|} (c ∑ ‖v_i‖²)^n for 1 ≤ c, 4n ≤ c+3.

noncomputable def TrilinearHT.Auto.khintchineUpperConst (p : ℝ) : ℝ

The explicit upper Khintchine constant C_p = √(4 ⌈p/2⌉).

Equations

• TrilinearHT.Auto.khintchineUpperConst p = √(4 * ↑⌈p / 2⌉₊)

theorem TrilinearHT.Auto.khintchineUpperConst_pos {p : ℝ} (hp : 0 < p) : 0 < khintchineUpperConst p

Positivity of the upper Khintchine constant.

theorem TrilinearHT.Auto.khintchine_upper_rpow {ι : Type u_1} [DecidableEq ι] (𝕜 : Type u_2) {H : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (s : Finset ι) (v : ι → H) {p : ℝ} (hp : 0 < p) : (rademacherMean s fun (u : Finset ι) => ‖rademacherSum s u v‖ ^ p) ≤ (khintchineUpperConst p * √(∑ i ∈ s, ‖v i‖ ^ 2)) ^ p

Upper Khintchine inequality, p-th power form: 2^{-|s|} ∑_{u ⊆ s} ‖∑ ε_i v_i‖^p ≤ (C_p (∑ ‖v_i‖²)^{1/2})^p for 0 < p.

theorem TrilinearHT.Auto.khintchine_upper {ι : Type u_1} [DecidableEq ι] (𝕜 : Type u_2) {H : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (s : Finset ι) (v : ι → H) {p : ℝ} (hp : 0 < p) : (rademacherMean s fun (u : Finset ι) => ‖rademacherSum s u v‖ ^ p) ^ (1 / p) ≤ khintchineUpperConst p * √(∑ i ∈ s, ‖v i‖ ^ 2)

Upper Khintchine inequality (Blueprint Lemma 2.6 (lem:khintchine), upper bound): for vectors v_i in a real or complex inner product space and 0 < p < ∞, (𝔼_ε ‖∑_{i ∈ s} ε_i v_i‖^p)^{1/p} ≤ C_p (∑_{i ∈ s} ‖v_i‖²)^{1/2}, where the expectation is the uniform average over the 2^{|s|} sign patterns and C_p = khintchineUpperConst p depends only on p.

theorem TrilinearHT.Auto.khintchineUpperConst_le {p : ℝ} (hp : 2 ≤ p) : khintchineUpperConst p ≤ 2 * √p

theorem TrilinearHT.Auto.signs_moment_bound {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (a : ι → ℂ) {p : ℝ} (hp : 2 ≤ p) : (rademacherMean s fun (u : Finset ι) => ‖rademacherSum s u a‖ ^ p) ^ (1 / p) ≤ 2 * √p * √(∑ i ∈ s, ‖a i‖ ^ 2)

The source's dimension-free sign estimate, with the absolute constant 2.

theorem TrilinearHT.Auto.rademacherMean_mono {ι : Type u_1} (s : Finset ι) {f g : Finset ι → ℝ} (h : ∀ u ∈ s.powerset, f u ≤ g u) : rademacherMean s f ≤ rademacherMean s g

Finite uniform expectations used in sampling symmetrization.

noncomputable def TrilinearHT.Auto.uniformMean {A : Type u_1} {E : Type u_2} [Fintype A] [AddCommMonoid E] [Module ℝ E] (f : A → E) : E

Uniform average of a function on a finite type.

Equations

• TrilinearHT.Auto.uniformMean f = (↑(Fintype.card A))⁻¹ • ∑ a : A, f a

theorem TrilinearHT.Auto.uniformMean_const {A : Type u_1} {E : Type u_2} [Fintype A] [Nonempty A] [AddCommMonoid E] [Module ℝ E] (c : E) : (uniformMean fun (x : A) => c) = c

theorem TrilinearHT.Auto.uniformMean_add {A : Type u_1} {E : Type u_2} [Fintype A] [AddCommMonoid E] [Module ℝ E] (f g : A → E) : (uniformMean fun (a : A) => f a + g a) = uniformMean f + uniformMean g

theorem TrilinearHT.Auto.uniformMean_sub {A : Type u_1} {E : Type u_2} [Fintype A] [AddCommGroup E] [Module ℝ E] (f g : A → E) : (uniformMean fun (a : A) => f a - g a) = uniformMean f - uniformMean g

theorem TrilinearHT.Auto.uniformMean_sum {A : Type u_1} {I : Type u_2} {E : Type u_3} [Fintype A] [AddCommMonoid E] [Module ℝ E] (s : Finset I) (f : I → A → E) : (uniformMean fun (a : A) => ∑ i ∈ s, f i a) = ∑ i ∈ s, uniformMean (f i)

theorem TrilinearHT.Auto.uniformMean_smul {A : Type u_1} {E : Type u_2} [Fintype A] [AddCommMonoid E] [Module ℝ E] (c : ℝ) (f : A → E) : (uniformMean fun (a : A) => c • f a) = c • uniformMean f

theorem TrilinearHT.Auto.uniformMean_mono {A : Type u_1} [Fintype A] {f g : A → ℝ} (h : ∀ (a : A), f a ≤ g a) : uniformMean f ≤ uniformMean g

theorem TrilinearHT.Auto.uniformMean_nonneg {A : Type u_1} [Fintype A] {f : A → ℝ} (h : ∀ (a : A), 0 ≤ f a) : 0 ≤ uniformMean f

theorem TrilinearHT.Auto.uniformMean_equiv {A : Type u_1} {B : Type u_2} {E : Type u_3} [Fintype A] [Fintype B] [AddCommMonoid E] [Module ℝ E] (e : A ≃ B) (f : B → E) : (uniformMean fun (a : A) => f (e a)) = uniformMean f

theorem TrilinearHT.Auto.uniformMean_prod {A : Type u_1} {B : Type u_2} {E : Type u_3} [Fintype A] [Fintype B] [AddCommMonoid E] [Module ℝ E] (f : A × B → E) : uniformMean f = uniformMean fun (a : A) => uniformMean fun (b : B) => f (a, b)

theorem TrilinearHT.Auto.uniformMean_norm_rpow_le {A : Type u_1} [Fintype A] [Nonempty A] (f : A → ℂ) {p : ℝ} (hp : 1 ≤ p) : ‖uniformMean f‖ ^ p ≤ uniformMean fun (a : A) => ‖f a‖ ^ p

theorem TrilinearHT.Auto.uniformMean_eval {I : Type u_1} {A : Type u_2} {E : Type u_3} [Fintype I] [DecidableEq I] [Fintype A] [Nonempty A] [AddCommMonoid E] [Module ℝ E] (i : I) (f : A → E) : (uniformMean fun (a : I → A) => f (a i)) = uniformMean f

theorem TrilinearHT.Auto.sampling_ghost_bound {I : Type u_1} {A : Type u_2} [Fintype I] [DecidableEq I] [Fintype A] [Nonempty A] (f : A → ℂ) {p : ℝ} (hp : 1 ≤ p) : (uniformMean fun (a : I → A) => ‖∑ i : I, (f (a i) - uniformMean f)‖ ^ p) ≤ uniformMean fun (a : I → A) => uniformMean fun (b : I → A) => ‖∑ i : I, (f (a i) - f (b i))‖ ^ p

Jensen's introduction of an independent copy of the entire sample.

def TrilinearHT.Auto.samplePairSwap {I : Type u_1} {A : Type u_2} [DecidableEq I] (u : Finset I) : (I → A) × (I → A) ≃ (I → A) × (I → A)

Swapping sample pairs at selected coordinates preserves the uniform distribution.

Equations

• One or more equations did not get rendered due to their size.

theorem TrilinearHT.Auto.samplePairSwap_difference {I : Type u_1} {A : Type u_2} [Fintype I] [DecidableEq I] (u : Finset I) (f : A → ℂ) (ab : (I → A) × (I → A)) : ∑ i : I, (f (((samplePairSwap u) ab).1 i) - f (((samplePairSwap u) ab).2 i)) = rademacherSum Finset.univ u fun (i : I) => f (ab.1 i) - f (ab.2 i)

theorem TrilinearHT.Auto.uniformMean_rademacherMean_comm {A : Type u_1} {I : Type u_2} [Fintype A] (s : Finset I) (f : A → Finset I → ℝ) : (uniformMean fun (a : A) => rademacherMean s (f a)) = rademacherMean s fun (u : Finset I) => uniformMean fun (a : A) => f a u

theorem TrilinearHT.Auto.rademacherMean_const {I : Type u_1} (s : Finset I) (c : ℝ) : (rademacherMean s fun (x : Finset I) => c) = c

theorem TrilinearHT.Auto.sampling_sign_symmetrization {I : Type u_1} {A : Type u_2} [Fintype I] [DecidableEq I] [Fintype A] (f : A → ℂ) (p : ℝ) : (uniformMean fun (a : I → A) => uniformMean fun (b : I → A) => ‖∑ i : I, (f (a i) - f (b i))‖ ^ p) = uniformMean fun (ab : (I → A) × (I → A)) => rademacherMean Finset.univ fun (u : Finset I) => ‖rademacherSum Finset.univ u fun (i : I) => f (ab.1 i) - f (ab.2 i)‖ ^ p

theorem TrilinearHT.Auto.signs_moment_le_sum_rpow {I : Type u_1} [Fintype I] [DecidableEq I] (a : I → ℂ) {p : ℝ} (hp : 2 ≤ p) : (rademacherMean Finset.univ fun (u : Finset I) => ‖rademacherSum Finset.univ u a‖ ^ p) ≤ khintchineUpperConst p ^ p * ↑(Fintype.card I) ^ (p / 2 - 1) * ∑ i : I, ‖a i‖ ^ p

theorem TrilinearHT.Auto.norm_sub_rpow_le (a b : ℂ) {p : ℝ} (hp : 1 ≤ p) : ‖a - b‖ ^ p ≤ 2 ^ (p - 1) * (‖a‖ ^ p + ‖b‖ ^ p)

theorem TrilinearHT.Auto.uniformMean_comm {A : Type u_1} {B : Type u_2} {E : Type u_3} [Fintype A] [Fintype B] [AddCommMonoid E] [Module ℝ E] (f : A → B → E) : (uniformMean fun (a : A) => uniformMean (f a)) = uniformMean fun (b : B) => uniformMean fun (a : A) => f a b

theorem TrilinearHT.Auto.sample_difference_moment {I : Type u_1} {A : Type u_2} [Fintype I] [DecidableEq I] [Fintype A] [Nonempty A] (f : A → ℂ) (i : I) {p : ℝ} (hp : 1 ≤ p) : (uniformMean fun (ab : (I → A) × (I → A)) => ‖f (ab.1 i) - f (ab.2 i)‖ ^ p) ≤ 2 ^ p * uniformMean fun (a : A) => ‖f a‖ ^ p

theorem TrilinearHT.Auto.sampling_sum_moment_bound {I : Type u_1} {A : Type u_2} [Fintype I] [DecidableEq I] [Nonempty I] [Fintype A] [Nonempty A] (f : A → ℂ) {p : ℝ} (hp : 2 ≤ p) : (uniformMean fun (a : I → A) => ‖∑ i : I, (f (a i) - uniformMean f)‖ ^ p) ≤ (2 * khintchineUpperConst p * √↑(Fintype.card I)) ^ p * uniformMean fun (a : A) => ‖f a‖ ^ p

Centered sums of independent uniform samples have square-root sample-size growth.

theorem TrilinearHT.Auto.sampling_mean_moment_bound {I : Type u_1} {A : Type u_2} [Fintype I] [DecidableEq I] [Nonempty I] [Fintype A] [Nonempty A] (f : A → ℂ) {p : ℝ} (hp : 2 ≤ p) : (uniformMean fun (a : I → A) => ‖(uniformMean fun (i : I) => f (a i)) - uniformMean f‖ ^ p) ≤ (4 * √(p / ↑(Fintype.card I))) ^ p * uniformMean fun (a : A) => ‖f a‖ ^ p

noncomputable def TrilinearHT.Auto.finiteLpNorm {G : Type u_1} [Fintype G] (p : ℝ) (f : G → ℂ) : ℝ

Finite Lᵖ norm with probability counting measure.

Equations

• TrilinearHT.Auto.finiteLpNorm p f = (TrilinearHT.Auto.uniformMean fun (x : G) => ‖f x‖ ^ p) ^ (1 / p)

theorem TrilinearHT.Auto.finiteLpNorm_rpow {G : Type u_1} [Fintype G] (f : G → ℂ) {p : ℝ} (hp : 0 < p) : finiteLpNorm p f ^ p = uniformMean fun (x : G) => ‖f x‖ ^ p

theorem TrilinearHT.Auto.uniformMean_translate {G : Type u_1} {E : Type u_2} [AddGroup G] [Fintype G] [AddCommMonoid E] [Module ℝ E] (f : G → E) (a : G) : (uniformMean fun (x : G) => f (x - a)) = uniformMean f

theorem TrilinearHT.Auto.sampling_translate_moment_bound {G : Type u_1} {A : Type u_2} {I : Type u_3} [AddCommGroup G] [Fintype G] [Fintype A] [Nonempty A] [Fintype I] [DecidableEq I] [Nonempty I] (z : A → G) (f : G → ℂ) {p : ℝ} (hp : 2 ≤ p) : (uniformMean fun (a : I → A) => (finiteLpNorm p fun (x : G) => (uniformMean fun (i : I) => f (x - z (a i))) - uniformMean fun (b : A) => f (x - z b)) ^ p) ≤ (4 * √(p / ↑(Fintype.card I)) * finiteLpNorm p f) ^ p

Sampling estimate for translates; samples may be drawn uniformly from any finite type.

theorem TrilinearHT.Auto.uniformMean_complex_eq {G : Type u_1} [Fintype G] (f : G → ℂ) : uniformMean f = finiteAverage f

noncomputable def TrilinearHT.Auto.finiteSetDensity {G : Type u_1} [Fintype G] [DecidableEq G] (A : Finset G) (x : G) : ℂ

The probability-density normalization 1_A / (|A| / |G|).

Equations

• TrilinearHT.Auto.finiteSetDensity A x = if x ∈ A then ↑(Fintype.card G) / ↑A.card else 0

theorem TrilinearHT.Auto.finiteConvolution_comm {G : Type u_1} [AddCommGroup G] [Fintype G] (f g : G → ℂ) (x : G) : finiteConvolution f g x = finiteConvolution g f x

theorem TrilinearHT.Auto.finiteConvolution_setDensity {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (A : Finset G) (f : G → ℂ) (x : G) : finiteConvolution f (finiteSetDensity A) x = uniformMean fun (a : ↥A) => f (x - ↑a)

theorem TrilinearHT.Auto.sampling_convolution_bound {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (A : Finset G) (hA : A.Nonempty) (n : ℕ) (hn : 0 < n) (f : G → ℂ) {p : ℝ} (hp : 2 ≤ p) : (uniformMean fun (a : Fin n → ↥A) => (finiteLpNorm p fun (x : G) => (uniformMean fun (i : Fin n) => f (x - ↑(a i))) - finiteConvolution f (finiteSetDensity A) x) ^ p) ≤ (4 * √(p / ↑n) * finiteLpNorm p f) ^ p

Blueprint lem:finite-fourier: the sampling inequality with probability counting norms and convolution, with the absolute constant 4.

Finite probability Lp norm laws for almost periods

theorem TrilinearHT.Auto.finiteLpNorm_nonneg {G : Type u_1} [Fintype G] (p : ℝ) (f : G → ℂ) : 0 ≤ finiteLpNorm p f

theorem TrilinearHT.Auto.finiteLpNorm_eq_scaled_sum {G : Type u_1} [Fintype G] (p : ℝ) (f : G → ℂ) : finiteLpNorm p f = (↑(Fintype.card G))⁻¹ ^ (1 / p) * (∑ x : G, ‖f x‖ ^ p) ^ (1 / p)

theorem TrilinearHT.Auto.finiteLpNorm_zero {G : Type u_1} [Fintype G] {p : ℝ} (hp : 0 < p) : (finiteLpNorm p fun (x : G) => 0) = 0

theorem TrilinearHT.Auto.finiteLpNorm_neg {G : Type u_1} [Fintype G] (p : ℝ) (f : G → ℂ) : (finiteLpNorm p fun (x : G) => -f x) = finiteLpNorm p f

theorem TrilinearHT.Auto.finiteLpNorm_add_le {G : Type u_1} [Fintype G] {p : ℝ} (hp : 1 ≤ p) (f g : G → ℂ) : (finiteLpNorm p fun (x : G) => f x + g x) ≤ finiteLpNorm p f + finiteLpNorm p g

Minkowski for the actual probability-counting norm used by the sampling theorem.

theorem TrilinearHT.Auto.finiteLpNorm_translate {G : Type u_1} [AddGroup G] [Fintype G] (p : ℝ) (f : G → ℂ) (a : G) : (finiteLpNorm p fun (x : G) => f (x - a)) = finiteLpNorm p f

theorem TrilinearHT.Auto.finiteLpNorm_translate_add {G : Type u_1} [AddGroup G] [Fintype G] (p : ℝ) (f : G → ℂ) (a : G) : (finiteLpNorm p fun (x : G) => f (x + a)) = finiteLpNorm p f

Markov counting and the source sample size

theorem TrilinearHT.Auto.uniformMean_half_good {A : Type u_1} [Fintype A] [Nonempty A] (u : A → ℝ) (hu : ∀ (a : A), 0 ≤ u a) {R : ℝ} (hR : 0 ≤ R) (hmean : uniformMean u ≤ R / 2) : ↑(Fintype.card A) / 2 ≤ ↑{a : A | u a ≤ R}.card

A nonnegative finite random variable of mean at most half a threshold is below that threshold on at least half the sample space. The threshold may be zero.

noncomputable def TrilinearHT.Auto.almostPeriodSampleSize (p ε : ℝ) : ℕ

An explicit universal sample size for the almost-period theorem.

Equations

• TrilinearHT.Auto.almostPeriodSampleSize p ε = ⌈64 * p / ε ^ 2⌉₊

theorem TrilinearHT.Auto.almostPeriodSampleSize_pos {p ε : ℝ} (hp : 0 < p) (hε : 0 < ε) : 0 < almostPeriodSampleSize p ε

theorem TrilinearHT.Auto.almostPeriodSampleSize_factor {p ε : ℝ} (hp : 0 < p) (hε : 0 < ε) : 4 * √(p / ↑(almostPeriodSampleSize p ε)) ≤ ε / 2

At the chosen sample size, the sampling constant is at most epsilon/2.

noncomputable def TrilinearHT.Auto.goodSampleTuples {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (A : Finset G) (n : ℕ) (f : G → ℂ) (p ε : ℝ) : Finset (Fin n → ↥A)

The actual sample tuples giving the required Lp approximation.

Equations

• One or more equations did not get rendered due to their size.

theorem TrilinearHT.Auto.mem_goodSampleTuples {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (A : Finset G) (n : ℕ) (f : G → ℂ) (p ε : ℝ) (a : Fin n → ↥A) : a ∈ goodSampleTuples A n f p ε ↔ (finiteLpNorm p fun (x : G) => (uniformMean fun (i : Fin n) => f (x - ↑(a i))) - finiteConvolution f (finiteSetDensity A) x) ≤ ε * finiteLpNorm p f

theorem TrilinearHT.Auto.goodSampleTuples_card_lower {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (A : Finset G) (hA : A.Nonempty) (f : G → ℂ) {p ε : ℝ} (hp : 2 ≤ p) (hε : 0 < ε) : ↑A.card ^ almostPeriodSampleSize p ε / 2 ≤ ↑(goodSampleTuples A (almostPeriodSampleSize p ε) f p ε).card

Blueprint lem:almostperiods, lines 777-781: at least half of all tuples of ceil(64*p/epsilon^2) samples are good.

Diagonal tuple fibers

def TrilinearHT.Auto.diagonalTupleEquiv {G : Type u_1} [AddCommGroup G] (n : ℕ) : (Fin (n + 1) → G) ≃ (Fin n → G) × G

A tuple consists of its differences from the first coordinate and its first coordinate. This explicitly parametrizes diagonal-subgroup cosets.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TrilinearHT.Auto.diagonalTupleFiber {G : Type u_1} [AddCommGroup G] [Fintype G] {n : ℕ} (S : Finset (Fin (n + 1) → G)) (z : Fin n → G) : Finset G

The translation parameters whose reconstructed tuples belong to S.

Equations

• TrilinearHT.Auto.diagonalTupleFiber S z = {t : G | (Fin.cons t fun (i : Fin n) => z i + t) ∈ S}

theorem TrilinearHT.Auto.mem_diagonalTupleFiber {G : Type u_1} [AddCommGroup G] [Fintype G] {n : ℕ} (S : Finset (Fin (n + 1) → G)) (z : Fin n → G) (t : G) : t ∈ diagonalTupleFiber S z ↔ (Fin.cons t fun (i : Fin n) => z i + t) ∈ S

theorem TrilinearHT.Auto.sum_diagonalTupleFiber_card {G : Type u_1} [AddCommGroup G] [Fintype G] {n : ℕ} (S : Finset (Fin (n + 1) → G)) : ∑ z : Fin n → G, (diagonalTupleFiber S z).card = S.card

Counting all diagonal fibers counts each tuple exactly once.

theorem TrilinearHT.Auto.exists_large_diagonalTupleFiber {G : Type u_1} [AddCommGroup G] [Fintype G] {n : ℕ} (S : Finset (Fin (n + 1) → G)) : ∃ (z : Fin n → G), ↑S.card / ↑(Fintype.card G) ^ n ≤ ↑(diagonalTupleFiber S z).card

Among the |G|^n diagonal fibers of (n+1)-tuples, one has at least the average number of members of S.

noncomputable def TrilinearHT.Auto.goodGroupSampleTuples {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (A : Finset G) (n : ℕ) (f : G → ℂ) (p ε : ℝ) : Finset (Fin n → G)

Good tuples regarded as actual group-valued tuples, forgetting membership proofs.

Equations

• TrilinearHT.Auto.goodGroupSampleTuples A n f p ε = Finset.image (fun (a : Fin n → ↥A) (i : Fin n) => ↑(a i)) (TrilinearHT.Auto.goodSampleTuples A n f p ε)

theorem TrilinearHT.Auto.goodGroupSampleTuples_card {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (A : Finset G) (n : ℕ) (f : G → ℂ) (p ε : ℝ) : (goodGroupSampleTuples A n f p ε).card = (goodSampleTuples A n f p ε).card

theorem TrilinearHT.Auto.mem_goodGroupSampleTuples {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (A : Finset G) (n : ℕ) (f : G → ℂ) (p ε : ℝ) (a : Fin n → G) : a ∈ goodGroupSampleTuples A n f p ε ↔ (∀ (i : Fin n), a i ∈ A) ∧ (finiteLpNorm p fun (x : G) => (uniformMean fun (i : Fin n) => f (x - a i)) - finiteConvolution f (finiteSetDensity A) x) ≤ ε * finiteLpNorm p f

theorem TrilinearHT.Auto.good_diagonal_fiber_density {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (A : Finset G) (f : G → ℂ) (p ε : ℝ) {n : ℕ} (hgood : ↑A.card ^ (n + 1) / 2 ≤ ↑(goodSampleTuples A (n + 1) f p ε).card) : ∃ (z : Fin n → G), (↑A.card / ↑(Fintype.card G)) ^ (n + 1) / 2 ≤ ↑(diagonalTupleFiber (goodGroupSampleTuples A (n + 1) f p ε) z).card / ↑(Fintype.card G)

Blueprint lem:almostperiods, lines 781-783: a diagonal fiber of good tuples has the required parameter-set density alpha^(n+1)/2.

Translation differences of good samples

theorem TrilinearHT.Auto.diagonal_empirical_translate {G : Type u_1} [AddCommGroup G] {n : ℕ} (z : Fin n → G) (t t' : G) (f : G → ℂ) (x : G) : (uniformMean fun (i : Fin (n + 1)) => f (x + t - t' - Fin.cons t (fun (j : Fin n) => z j + t) i)) = uniformMean fun (i : Fin (n + 1)) => f (x - Fin.cons t' (fun (j : Fin n) => z j + t') i)

Empirical averages in one diagonal fiber are exact translates of each other.

theorem TrilinearHT.Auto.diagonal_good_samples_almost_period {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (A : Finset G) (f : G → ℂ) {p ε : ℝ} (hp : 1 ≤ p) {n : ℕ} (z : Fin n → G) {t t' : G} (ht : t ∈ diagonalTupleFiber (goodGroupSampleTuples A (n + 1) f p ε) z) (ht' : t' ∈ diagonalTupleFiber (goodGroupSampleTuples A (n + 1) f p ε) z) : (finiteLpNorm p fun (x : G) => finiteConvolution f (finiteSetDensity A) (x + t - t') - finiteConvolution f (finiteSetDensity A) x) ≤ 2 * ε * finiteLpNorm p f

Two good tuples in a common diagonal fiber give the source translation error.

theorem TrilinearHT.Auto.sampling_almost_periods {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (A : Finset G) (hA : A.Nonempty) (f : G → ℂ) {p ε : ℝ} (hp : 2 ≤ p) (hε : 0 < ε) : ∃ (X : Finset G), X.Nonempty ∧ (↑A.card / ↑(Fintype.card G)) ^ almostPeriodSampleSize p ε / 2 ≤ ↑X.card / ↑(Fintype.card G) ∧ ∀ t ∈ X, ∀ t' ∈ X, (finiteLpNorm p fun (x : G) => finiteConvolution f (finiteSetDensity A) (x + t - t') - finiteConvolution f (finiteSetDensity A) x) ≤ 2 * ε * finiteLpNorm p f

Blueprint lem:almostperiods, lines 766-783: for every real p >= 2 there is a nonempty set of density at least alpha^n/2, where n = ceil(64*p/epsilon^2), whose pairwise differences are 2*epsilon almost periods of the actual convolution f * mu_A.

Telescoping over iterated sumsets

theorem TrilinearHT.Auto.finiteLpNorm_translation_add_le {G : Type u_1} [AddCommGroup G] [Fintype G] {p : ℝ} (hp : 1 ≤ p) (f : G → ℂ) (u v : G) : (finiteLpNorm p fun (x : G) => f (x + (u + v)) - f x) ≤ (finiteLpNorm p fun (x : G) => f (x + u) - f x) + finiteLpNorm p fun (x : G) => f (x + v) - f x

The translation error is subadditive in its translation parameter.

theorem TrilinearHT.Auto.finiteLpNorm_sumset_difference_bound {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {p : ℝ} (hp : 1 ≤ p) (f : G → ℂ) (X : Finset G) (C : ℝ) (hpair : ∀ t ∈ X, ∀ t' ∈ X, (finiteLpNorm p fun (x : G) => f (x + (t - t')) - f x) ≤ C) (k : ℕ) (u : G) : u ∈ k • X - k • X → (finiteLpNorm p fun (x : G) => f (x + u) - f x) ≤ ↑k * C

A bound on pairwise differences telescopes to every iterated sum-difference set.

theorem TrilinearHT.Auto.sampling_almost_periods_iterated {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (A : Finset G) (hA : A.Nonempty) (f : G → ℂ) {p ε : ℝ} (hp : 2 ≤ p) (hε : 0 < ε) : ∃ (X : Finset G), X.Nonempty ∧ (↑A.card / ↑(Fintype.card G)) ^ almostPeriodSampleSize p ε / 2 ≤ ↑X.card / ↑(Fintype.card G) ∧ ∀ (k : ℕ), ∀ u ∈ k • X - k • X, (finiteLpNorm p fun (x : G) => finiteConvolution f (finiteSetDensity A) (x + u) - finiteConvolution f (finiteSetDensity A) x) ≤ 2 * ↑k * ε * finiteLpNorm p f

Blueprint lem:almostperiods, lines 766-784, including its final kX-kX conclusion. The universal sampling constant is 64, the density is at least alpha^ceil(64*p/epsilon^2)/2, and the error is 2*k*epsilon.

Probability-normalized Fourier analysis on finite cyclic groups.

noncomputable def TrilinearHT.Auto.finiteFourier {q : ℕ} [NeZero q] (f : ZMod q → ℂ) (ξ : ZMod q) : ℂ

Probability-normalized discrete Fourier transform on a cyclic group.

Equations

• TrilinearHT.Auto.finiteFourier f ξ = (↑q)⁻¹ * ZMod.dft f ξ

theorem TrilinearHT.Auto.finiteFourier_eq_average {q : ℕ} [NeZero q] (f : ZMod q → ℂ) (ξ : ZMod q) : finiteFourier f ξ = finiteAverage fun (x : ZMod q) => f x * ZMod.stdAddChar (-(ξ * x))

theorem TrilinearHT.Auto.finiteFourier_inversion {q : ℕ} [NeZero q] (f : ZMod q → ℂ) (x : ZMod q) : f x = ∑ ξ : ZMod q, finiteFourier f ξ * ZMod.stdAddChar (ξ * x)

theorem TrilinearHT.Auto.stdAddChar_conj {q : ℕ} [NeZero q] (x : ZMod q) : (starRingEnd ℂ) (ZMod.stdAddChar x) = ZMod.stdAddChar (-x)

theorem TrilinearHT.Auto.finiteAverage_sum {G : Type u_1} {I : Type u_2} [Fintype G] (s : Finset I) (f : I → G → ℂ) : (finiteAverage fun (x : G) => ∑ i ∈ s, f i x) = ∑ i ∈ s, finiteAverage (f i)

theorem TrilinearHT.Auto.finiteAverage_mul_const {G : Type u_1} [Fintype G] (f : G → ℂ) (c : ℂ) : (finiteAverage fun (x : G) => f x * c) = finiteAverage f * c

theorem TrilinearHT.Auto.finiteAverage_const_mul {G : Type u_1} [Fintype G] (c : ℂ) (f : G → ℂ) : (finiteAverage fun (x : G) => c * f x) = c * finiteAverage f

theorem TrilinearHT.Auto.finiteAverage_re {G : Type u_1} [Fintype G] (f : G → ℂ) : (finiteAverage f).re = uniformMean fun (x : G) => (f x).re

theorem TrilinearHT.Auto.finiteFourier_pairing {q : ℕ} [NeZero q] (f g : ZMod q → ℂ) : (finiteAverage fun (x : ZMod q) => f x * (starRingEnd ℂ) (g x)) = ∑ ξ : ZMod q, finiteFourier f ξ * (starRingEnd ℂ) (finiteFourier g ξ)

theorem TrilinearHT.Auto.finiteFourier_parseval {q : ℕ} [NeZero q] (f : ZMod q → ℂ) : (uniformMean fun (x : ZMod q) => ‖f x‖ ^ 2) = ∑ ξ : ZMod q, ‖finiteFourier f ξ‖ ^ 2

theorem TrilinearHT.Auto.finiteAverage_comm {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (f : A → B → ℂ) : (finiteAverage fun (a : A) => finiteAverage (f a)) = finiteAverage fun (b : B) => finiteAverage fun (a : A) => f a b

theorem TrilinearHT.Auto.finiteAverage_equiv {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (e : A ≃ B) (f : B → ℂ) : (finiteAverage fun (a : A) => f (e a)) = finiteAverage f

theorem TrilinearHT.Auto.finiteFourier_translate {q : ℕ} [NeZero q] (f : ZMod q → ℂ) (a ξ : ZMod q) : finiteFourier (fun (x : ZMod q) => f (x - a)) ξ = ZMod.stdAddChar (-(ξ * a)) * finiteFourier f ξ

theorem TrilinearHT.Auto.finiteFourier_convolution {q : ℕ} [NeZero q] (f g : ZMod q → ℂ) (ξ : ZMod q) : finiteFourier (finiteConvolution f g) ξ = finiteFourier f ξ * finiteFourier g ξ