Documentation

theorem TrilinearHT.Auto.unitCircle_norm_representative (x : UnitAddCircle) :

∃ (r : ℝ), ↑r = x ∧ |r| = ‖x‖

Every point of the unit additive circle has a representative realizing its quotient norm.

theorem TrilinearHT.Auto.unitCircle_exists_large_multiple (x : UnitAddCircle) (hx : x ≠ 0) :

∃ (n : ℕ), 1 / 4 ≤ ‖n • x‖

A nonzero point of the circle has an integer multiple at distance at least one quarter.

theorem TrilinearHT.Auto.cyclic_nonzero_character_test_card {q : ℕ} [NeZero q] (χ : ZMod q) (hχ : χ ≠ 0) :

↑(cyclicBohrSet {χ} (1 / 8)).card ≤ ↑q / 2

A nonzero cyclic frequency passes the one-eighth character test on at most half the group.

theorem TrilinearHT.Auto.cyclic_character_test_halving {q : ℕ} [NeZero q] (D : Finset (ZMod q)) (hD : ∀ χ ∈ D, χ ≠ 0) :

∃ (g : ZMod q), 2 * {χ ∈ D | ‖ZMod.toAddCircle (χ * g)‖ < 1 / 8}.card ≤ D.card

One character test eliminates at least half of any finite set of nonzero frequencies.

noncomputable def TrilinearHT.Auto.cyclicTestSurvivors {q d : ℕ} [NeZero q] (D : Finset (ZMod q)) (g : Fin d → ZMod q) :

Finset (ZMod q)

Frequencies surviving all tests in a finite tuple.

Equations

TrilinearHT.Auto.cyclicTestSurvivors D g = {χ ∈ D | ∀ (j : Fin d), ‖ZMod.toAddCircle (χ * g j)‖ < 1 / 8}

Instances For

theorem TrilinearHT.Auto.mem_cyclicTestSurvivors {q d : ℕ} [NeZero q] (D : Finset (ZMod q)) (g : Fin d → ZMod q) (χ : ZMod q) :

χ ∈ cyclicTestSurvivors D g ↔ χ ∈ D ∧ ∀ (j : Fin d), ‖ZMod.toAddCircle (χ * g j)‖ < 1 / 8

theorem TrilinearHT.Auto.cyclic_character_tests_card {q : ℕ} [NeZero q] (D : Finset (ZMod q)) (hD : ∀ χ ∈ D, χ ≠ 0) (d : ℕ) :

∃ (g : Fin d → ZMod q), 2 ^ d * (cyclicTestSurvivors D g).card ≤ D.card

Repeated character tests reduce the surviving cardinality by a factor of two at each step.

theorem TrilinearHT.Auto.cyclic_logarithmic_separating_family {q : ℕ} [NeZero q] (D : Finset (ZMod q)) (hD : D.Nonempty) :

∃ (g : Fin ⌈Real.log (2 * ↑D.card) / Real.log 2⌉₊ → ZMod q), ∀ χ ∈ D, χ ≠ 0 → ∃ (j : Fin ⌈Real.log (2 * ↑D.card) / Real.log 2⌉₊), 1 / 8 ≤ ‖ZMod.toAddCircle (χ * g j)‖

The source logarithmic number of one-eighth tests separates every nonzero frequency in D.

theorem TrilinearHT.Auto.finite_torus_dense_cube {α : Type u_1} {ι : Type u_2} [Fintype ι] (A : Finset α) (hA : A.Nonempty) (phase : α → ι → UnitAddCircle) (N : ℕ) (hN : 0 < N) :

∃ B ⊆ A, B.Nonempty ∧ ↑A.card / ↑N ^ Fintype.card ι ≤ ↑B.card ∧ ∀ x ∈ B, ∀ y ∈ B, ∀ (i : ι), ‖phase x i - phase y i‖ < 1 / ↑N

A finite set of points in a torus has a dense subset in one cube of mesh 1/N.

theorem TrilinearHT.Auto.cyclic_frequency_dense_cube {q d : ℕ} [NeZero q] (H : Finset (ZMod q)) (hH : H.Nonempty) (ξ : ZMod q → ZMod q) (g : Fin d → ZMod q) :

∃ H' ⊆ H, H'.Nonempty ∧ ↑H.card / 256 ^ d ≤ ↑H'.card ∧ ∀ h ∈ H', ∀ h' ∈ H', ∀ (j : Fin d), ‖ZMod.toAddCircle ((ξ h - ξ h') * g j)‖ < 1 / 256

A common cube retains the source fraction of a graph's domain and controls all frequency differences.

Smooth finite Bohr weights #

noncomputable def TrilinearHT.Auto.unitCircleCentered (x : UnitAddCircle) :

The source centered representative in [-1/2,1/2).

Equations

TrilinearHT.Auto.unitCircleCentered x = ↑((AddCircle.equivIco 1 (-(1 / 2))) x)

Instances For

theorem TrilinearHT.Auto.unitCircleCentered_mem (x : UnitAddCircle) :

-(1 / 2) ≤ unitCircleCentered x ∧ unitCircleCentered x < 1 / 2

theorem TrilinearHT.Auto.unitCircleCentered_coe (x : UnitAddCircle) :

↑(unitCircleCentered x) = x

theorem TrilinearHT.Auto.unitCircleCentered_abs (x : UnitAddCircle) :

|unitCircleCentered x| = ‖x‖

noncomputable def TrilinearHT.Auto.circleCutoff (b : ℝ → ℝ) (r : ℝ) (x : UnitAddCircle) :

Periodic extension of the cutoff in the centered coordinate.

Equations

TrilinearHT.Auto.circleCutoff b r x = b (TrilinearHT.Auto.unitCircleCentered x / r)

Instances For

noncomputable def TrilinearHT.Auto.cyclicBohrWeight {q : ℕ} [NeZero q] (b : ℝ → ℝ) (S : Finset (ZMod q)) (r : ℝ) (x : ZMod q) :

The source periodic product weight.

Equations

TrilinearHT.Auto.cyclicBohrWeight b S r x = ∏ s ∈ S, TrilinearHT.Auto.circleCutoff b r (ZMod.toAddCircle (s * x))

Instances For

noncomputable def TrilinearHT.Auto.cyclicBohrMass {q : ℕ} [NeZero q] (b : ℝ → ℝ) (S : Finset (ZMod q)) (r : ℝ) :

Uniform mass of the smooth weight.

Equations

TrilinearHT.Auto.cyclicBohrMass b S r = Finset.univ.expect fun (x : ZMod q) => TrilinearHT.Auto.cyclicBohrWeight b S r x

Instances For

noncomputable def TrilinearHT.Auto.cyclicBohrMeasure {q : ℕ} [NeZero q] (b : ℝ → ℝ) (S : Finset (ZMod q)) (r : ℝ) (x : ZMod q) :

The weight normalized to have uniform mean one.

Equations

TrilinearHT.Auto.cyclicBohrMeasure b S r x = TrilinearHT.Auto.cyclicBohrWeight b S r x / TrilinearHT.Auto.cyclicBohrMass b S r

Instances For

theorem TrilinearHT.Auto.cyclicBohrWeight_nonneg {q : ℕ} [NeZero q] (b : ℝ → ℝ) (hb : ∀ (x : ℝ), 0 ≤ b x) (S : Finset (ZMod q)) (r : ℝ) (x : ZMod q) :

0 ≤ cyclicBohrWeight b S r x

theorem TrilinearHT.Auto.cyclicBohrWeight_le_one {q : ℕ} [NeZero q] (b : ℝ → ℝ) (hb : ∀ (x : ℝ), 0 ≤ b x) (hb1 : ∀ (x : ℝ), b x ≤ 1) (S : Finset (ZMod q)) (r : ℝ) (x : ZMod q) :

cyclicBohrWeight b S r x ≤ 1

theorem TrilinearHT.Auto.cyclicBohrWeight_eq_one {q : ℕ} [NeZero q] (b : ℝ → ℝ) (hb : ∀ (x : ℝ), |x| ≤ 1 / 2 → b x = 1) (S : Finset (ZMod q)) {r : ℝ} (hr : 0 < r) (x : ZMod q) (hx : x ∈ cyclicBohrSet S (r / 2)) :

cyclicBohrWeight b S r x = 1

theorem TrilinearHT.Auto.cyclicBohrWeight_eq_zero_of_notMem {q : ℕ} [NeZero q] (b : ℝ → ℝ) (hb : ∀ (x : ℝ), 1 ≤ |x| → b x = 0) (S : Finset (ZMod q)) {r : ℝ} (hr : 0 < r) (x : ZMod q) (hx : x ∉ cyclicBohrSet S r) :

cyclicBohrWeight b S r x = 0

theorem TrilinearHT.Auto.cyclicBohrMass_bounds {q : ℕ} [NeZero q] (b : ℝ → ℝ) (hb : ∀ (x : ℝ), 0 ≤ b x) (hb1 : ∀ (x : ℝ), b x ≤ 1) (hbone : ∀ (x : ℝ), |x| ≤ 1 / 2 → b x = 1) (S : Finset (ZMod q)) {r : ℝ} (hr : 0 < r) (hrsmall : r < 1 / 8) :

(r / 6) ^ S.card ≤ cyclicBohrMass b S r ∧ cyclicBohrMass b S r ≤ 1

The smooth weight has at least the source Bohr-volume mass and at most unit mass.

theorem TrilinearHT.Auto.cyclicBohrMass_pos {q : ℕ} [NeZero q] (b : ℝ → ℝ) (hb : ∀ (x : ℝ), 0 ≤ b x) (hb1 : ∀ (x : ℝ), b x ≤ 1) (hbone : ∀ (x : ℝ), |x| ≤ 1 / 2 → b x = 1) (S : Finset (ZMod q)) {r : ℝ} (hr : 0 < r) (hrsmall : r < 1 / 8) :

0 < cyclicBohrMass b S r

theorem TrilinearHT.Auto.unitCircleCentered_coe_of_mem {a : ℝ} (ha : -(1 / 2) ≤ a ∧ a < 1 / 2) :

unitCircleCentered ↑a = a

theorem TrilinearHT.Auto.circleCutoff_local_difference (b : ℝ → ℝ) {L : NNReal} (hLip : LipschitzWith L b) (hsupp : ∀ (a : ℝ), 1 ≤ |a| → b a = 0) {r : ℝ} (hr : 0 < r) (hrsmall : r < 1 / 8) (x y : UnitAddCircle) (hx : circleCutoff b r x ≠ 0) (hxy : ‖x - y‖ < r) :

|circleCutoff b r x - circleCutoff b r y| ≤ ↑L / r * ‖x - y‖

A nearby point can be lifted in the same centered coordinate whenever a cutoff is active.

theorem TrilinearHT.Auto.circleCutoff_difference (b : ℝ → ℝ) {L : NNReal} (hLip : LipschitzWith L b) (hb : ∀ (a : ℝ), 0 ≤ b a) (hb1 : ∀ (a : ℝ), b a ≤ 1) (hsupp : ∀ (a : ℝ), 1 ≤ |a| → b a = 0) {r : ℝ} (hr : 0 < r) (hrsmall : r < 1 / 8) (x y : UnitAddCircle) :

|circleCutoff b r x - circleCutoff b r y| ≤ max (↑L) 1 / r * ‖x - y‖

The periodically extended cutoff is globally Lipschitz, including across the coordinate cut.

theorem TrilinearHT.Auto.real_product_difference_bound {ι : Type u_1} (s : Finset ι) (f g : ι → ℝ) (hf : ∀ i ∈ s, |f i| ≤ 1) (hg : ∀ i ∈ s, |g i| ≤ 1) :

|∏ i ∈ s, f i - ∏ i ∈ s, g i| ≤ ∑ i ∈ s, |f i - g i|

A telescoping product estimate for factors in the real unit ball.

noncomputable def TrilinearHT.Auto.cyclicBohrNorm {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (x : ZMod q) :

The maximum quotient-circle norm of the selected cyclic coordinates.

Equations

TrilinearHT.Auto.cyclicBohrNorm S x = ↑(S.sup fun (s : ZMod q) => ‖ZMod.toAddCircle (s * x)‖₊)

Instances For

theorem TrilinearHT.Auto.norm_le_cyclicBohrNorm {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (x s : ZMod q) (hs : s ∈ S) :

‖ZMod.toAddCircle (s * x)‖ ≤ cyclicBohrNorm S x

theorem TrilinearHT.Auto.cyclicBohrWeight_translation {q : ℕ} [NeZero q] (b : ℝ → ℝ) {L : NNReal} (hLip : LipschitzWith L b) (hb : ∀ (a : ℝ), 0 ≤ b a) (hb1 : ∀ (a : ℝ), b a ≤ 1) (hsupp : ∀ (a : ℝ), 1 ≤ |a| → b a = 0) (S : Finset (ZMod q)) {r : ℝ} (hr : 0 < r) (hrsmall : r < 1 / 8) (x t : ZMod q) :

|cyclicBohrWeight b S r (x + t) - cyclicBohrWeight b S r x| ≤ max (↑L) 1 * ↑S.card * cyclicBohrNorm S t / r

The source uniform translation bound for smooth Bohr weights.

theorem TrilinearHT.Auto.unitCircle_chord_lower (x : UnitAddCircle) :

4 * ‖x‖ ≤ ‖↑(AddCircle.toCircle x) - 1‖

The unit-circle chord controls four times the quotient-circle distance.

noncomputable def TrilinearHT.Auto.weightedCircleAverage {G : Type u_1} [Fintype G] (w : G → ℝ) (φ : G → UnitAddCircle) :

Weighted uniform average of a circle-valued phase.

Equations

TrilinearHT.Auto.weightedCircleAverage w φ = Finset.univ.expect fun (x : G) => ↑(w x) * ↑(AddCircle.toCircle (φ x))

Instances For

theorem TrilinearHT.Auto.weightedCircleAverage_sub {G : Type u_1} [Fintype G] (w v : G → ℝ) (φ : G → UnitAddCircle) :

weightedCircleAverage (fun (x : G) => w x - v x) φ = weightedCircleAverage w φ - weightedCircleAverage v φ

theorem TrilinearHT.Auto.weightedCircleAverage_div {G : Type u_1} [Fintype G] (w : G → ℝ) (φ : G → UnitAddCircle) (c : ℝ) :

weightedCircleAverage (fun (x : G) => w x / c) φ = weightedCircleAverage w φ / ↑c

theorem TrilinearHT.Auto.weightedCircleAverage_norm_le {G : Type u_1} [Fintype G] (w : G → ℝ) (φ : G → UnitAddCircle) :

‖weightedCircleAverage w φ‖ ≤ Finset.univ.expect fun (x : G) => |w x|

theorem TrilinearHT.Auto.weightedCircleAverage_translate {G : Type u_1} [Fintype G] [AddCommGroup G] (w : G → ℝ) (φ : G → UnitAddCircle) (t : G) (hadd : ∀ (x : G), w x ≠ 0 → φ (x + t) = φ x + φ t) :

weightedCircleAverage (fun (x : G) => w (x - t)) φ = ↑(AddCircle.toCircle (φ t)) * weightedCircleAverage w φ

Weighted translation uses phase additivity only at points carrying nonzero weight.

theorem TrilinearHT.Auto.weighted_local_character_decay {G : Type u_1} [Fintype G] [AddCommGroup G] (w : G → ℝ) (φ : G → UnitAddCircle) (t : G) {β τ A : ℝ} (hβ : 0 < β) (hτ : 0 < τ) (hcorr : τ ≤ ‖weightedCircleAverage (fun (x : G) => w x / β) φ‖) (hadd : ∀ (x : G), w x ≠ 0 → φ (x + t) = φ x + φ t) (htrans : ∀ (x : G), |w (x - t) - w x| ≤ A) :

‖φ t‖ ≤ A / (β * τ)

Local Fourier decay for any weight whose translated difference is uniformly small.

theorem TrilinearHT.Auto.cyclicBohrWeight_local_fourier_decay {q : ℕ} [NeZero q] (b : ℝ → ℝ) {L : NNReal} (hLip : LipschitzWith L b) (hb : ∀ (a : ℝ), 0 ≤ b a) (hb1 : ∀ (a : ℝ), b a ≤ 1) (hbone : ∀ (a : ℝ), |a| ≤ 1 / 2 → b a = 1) (hsupp : ∀ (a : ℝ), 1 ≤ |a| → b a = 0) (S : Finset (ZMod q)) {r : ℝ} (hr : 0 < r) (hrsmall : r < 1 / 8) (φ : ZMod q → UnitAddCircle) (hadd : ∀ x ∈ cyclicBohrSet S (3 * r), ∀ y ∈ cyclicBohrSet S (3 * r), x + y ∈ cyclicBohrSet S (3 * r) → φ (x + y) = φ x + φ y) {τ : ℝ} (hτ : 0 < τ) (hcorr : τ ≤ ‖weightedCircleAverage (cyclicBohrMeasure b S r) φ‖) (t : ZMod q) (ht : t ∈ cyclicBohrSet S r) :

‖φ t‖ ≤ max (↑L) 1 * ↑S.card * cyclicBohrNorm S t / (r * cyclicBohrMass b S r * τ)

The source local Fourier decay bound, requiring additivity only on the larger Bohr domain.

theorem TrilinearHT.Auto.unit_cutoff_hasCompactSupport (b : ℝ → ℝ) (hsupp : ∀ (a : ℝ), 1 ≤ |a| → b a = 0) :

HasCompactSupport b

A cutoff vanishing outside the unit interval has compact topological support.

Finite shift correlations and repeated Cauchy-Schwarz #

The general finite-average argument below is the two-stage Cauchy-Schwarz step in blueprint lem:derivative-graph, lines 842-855. All statements and local definitions use Mathlib finite averages. The proof of finite Jensen reuses the previously verified general sampling prerequisite.

theorem TrilinearHT.Auto.finite_expect_norm_sq_le {I : Type u_1} [Fintype I] [Nonempty I] (f : I → ℂ) :

‖Finset.univ.expect fun (i : I) => f i‖ ^ 2 ≤ Finset.univ.expect fun (i : I) => ‖f i‖ ^ 2

Jensen's inequality for the square norm of a finite probability average.

theorem TrilinearHT.Auto.finite_expect_weighted_sq_le {I : Type u_1} [Fintype I] [Nonempty I] (a b : I → ℂ) (ha : ∀ (i : I), ‖a i‖ ≤ 1) :

‖Finset.univ.expect fun (i : I) => a i * b i‖ ^ 2 ≤ Finset.univ.expect fun (i : I) => ‖b i‖ ^ 2

A unit-bounded weight can be removed from the finite Cauchy-Schwarz estimate.

noncomputable def TrilinearHT.Auto.finiteShiftCorrelation {G : Type u_1} {K : Type u_2} [AddCommGroup G] [Fintype G] [Fintype K] (A v : G → K → ℂ) :

Shift correlation of a bounded kernel with a finite family of functions.

Equations

TrilinearHT.Auto.finiteShiftCorrelation A v = Finset.univ.expect fun (k : K) => Finset.univ.expect fun (x : G) => A x k * Finset.univ.expect fun (h : G) => (starRingEnd ℂ) (A (x + h) k) * v h k

Instances For

noncomputable def TrilinearHT.Auto.finiteShiftCorrelationSquare {G : Type u_1} {K : Type u_2} [AddCommGroup G] [Fintype G] [Fintype K] (A v : G → K → ℂ) :

The nonnegative square average arising after the first Cauchy-Schwarz step.

Equations

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

Instances For

theorem TrilinearHT.Auto.finiteShiftCorrelation_first_cs {G : Type u_1} {K : Type u_2} [AddCommGroup G] [Fintype G] [Fintype K] [Nonempty K] (A v : G → K → ℂ) (hA : ∀ (x : G) (k : K), ‖A x k‖ ≤ 1) :

‖finiteShiftCorrelation A v‖ ^ 2 ≤ finiteShiftCorrelationSquare A v

First Cauchy-Schwarz step, valid for an arbitrary unit-bounded finite kernel.

theorem TrilinearHT.Auto.finite_expect_norm_sq_eq {I : Type u_1} [Fintype I] (f : I → ℂ) :

↑(‖Finset.univ.expect fun (i : I) => f i‖ ^ 2) = Finset.univ.expect fun (i : I) => Finset.univ.expect fun (j : I) => f i * (starRingEnd ℂ) (f j)

Expansion of the square of a finite complex average.

theorem TrilinearHT.Auto.finiteShiftCorrelationSquare_inner {G : Type u_1} {K : Type u_2} [AddCommGroup G] [Fintype G] (A v : G → K → ℂ) (x : G) (k : K) :

↑(‖Finset.univ.expect fun (h : G) => (starRingEnd ℂ) (A (x + h) k) * v h k‖ ^ 2) = Finset.univ.expect fun (h : G) => Finset.univ.expect fun (u : G) => (starRingEnd ℂ) (A (x + h) k) * A (x + h + u) k * (v h k * (starRingEnd ℂ) (v (h + u) k))

Expansion of the inner square after writing the second shift as h + u.

theorem TrilinearHT.Auto.finite_expect_reverse_three {I : Type u_1} {J : Type u_2} {K : Type u_3} [Fintype I] [Fintype J] [Fintype K] (f : I → J → K → ℂ) :

(Finset.univ.expect fun (i : I) => Finset.univ.expect fun (j : J) => Finset.univ.expect fun (k : K) => f i j k) = Finset.univ.expect fun (k : K) => Finset.univ.expect fun (j : J) => Finset.univ.expect fun (i : I) => f i j k

theorem TrilinearHT.Auto.finite_expect_ofReal {I : Type u_1} [Fintype I] (f : I → ℝ) :

↑(Finset.univ.expect fun (i : I) => f i) = Finset.univ.expect fun (i : I) => ↑(f i)

theorem TrilinearHT.Auto.finiteShiftCorrelationSquare_eq {G : Type u_1} {K : Type u_2} [AddCommGroup G] [Fintype G] [Fintype K] (A v : G → K → ℂ) :

↑(finiteShiftCorrelationSquare A v) = Finset.univ.expect fun (k : K) => Finset.univ.expect fun (u : G) => Finset.univ.expect fun (y : G) => (starRingEnd ℂ) (A y k) * A (y + u) k * Finset.univ.expect fun (h : G) => v h k * (starRingEnd ℂ) (v (h + u) k)

Reindexing the first square average isolates the differenced v factors.

noncomputable def TrilinearHT.Auto.finiteShiftEnergy {G : Type u_1} {K : Type u_2} [AddCommGroup G] [Fintype G] [Fintype K] (v : G → K → ℂ) :

The averaged squared correlation of the differences of a finite family.

Equations

TrilinearHT.Auto.finiteShiftEnergy v = Finset.univ.expect fun (k : K) => Finset.univ.expect fun (u : G) => ‖Finset.univ.expect fun (h : G) => v h k * (starRingEnd ℂ) (v (h + u) k)‖ ^ 2

Instances For

theorem TrilinearHT.Auto.finiteShiftCorrelation_second_cs {G : Type u_1} {K : Type u_2} [AddCommGroup G] [Fintype G] [Fintype K] [Nonempty K] (A v : G → K → ℂ) (hA : ∀ (x : G) (k : K), ‖A x k‖ ≤ 1) :

finiteShiftCorrelationSquare A v ^ 2 ≤ finiteShiftEnergy v

Second Cauchy-Schwarz step: the remaining bounded kernel factors disappear.

theorem TrilinearHT.Auto.finiteShiftCorrelation_fourth_le {G : Type u_1} {K : Type u_2} [AddCommGroup G] [Fintype G] [Fintype K] [Nonempty K] (A v : G → K → ℂ) (hA : ∀ (x : G) (k : K), ‖A x k‖ ≤ 1) :

‖finiteShiftCorrelation A v‖ ^ 4 ≤ finiteShiftEnergy v

Two Cauchy-Schwarz steps control the fourth power of the shift correlation by energy.

theorem TrilinearHT.Auto.gowersNorm_le_one {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] {j : ℕ} (hj : 1 ≤ j) (f : G → ℂ) (hf : Measurable f) (hbound : ∀ (x : G), ‖f x‖ ≤ 1) :

gowersNorm μ j f ≤ 1

A unit-bounded measurable function has Gowers norm at most one on a Haar probability group.

Function graphs and character energy #

These general counting identities supply the exact orthogonality step of blueprint lem:derivative-graph, lines 856-861. Their statements use only Mathlib and the local graph definitions. Proofs reuse finite-average identities from the independently verified Gowers-Cauchy-Schwarz module.

def TrilinearHT.Auto.finiteFunctionGraph {G : Type u_1} {F : Type u_2} [DecidableEq G] [DecidableEq F] (H : Finset G) (ξ : G → F) :

Finset (G × F)

The graph of a function restricted to a finite set.

Equations

TrilinearHT.Auto.finiteFunctionGraph H ξ = Finset.image (fun (h : G) => (h, ξ h)) H

Instances For

theorem TrilinearHT.Auto.mem_finiteFunctionGraph {G : Type u_1} {F : Type u_2} [DecidableEq G] [DecidableEq F] (H : Finset G) (ξ : G → F) (x : G) (y : F) :

(x, y) ∈ finiteFunctionGraph H ξ ↔ x ∈ H ∧ ξ x = y

def TrilinearHT.Auto.graphEnergyTriples {G : Type u_1} {F : Type u_2} [AddCommGroup G] [Fintype G] [DecidableEq G] [AddCommGroup F] [DecidableEq F] (H : Finset G) (ξ : G → F) :

Finset (G × G × G)

Shift triples that describe additive parallelograms in a function graph.

Equations

TrilinearHT.Auto.graphEnergyTriples H ξ = {p : G × G × G | p.1 ∈ H ∧ p.1 + p.2.1 ∈ H ∧ p.2.2 ∈ H ∧ p.2.2 + p.2.1 ∈ H ∧ ξ p.1 - ξ (p.1 + p.2.1) - ξ p.2.2 + ξ (p.2.2 + p.2.1) = 0}

Instances For

def TrilinearHT.Auto.graphEnergyQuad {G : Type u_1} {F : Type u_2} [AddCommGroup G] (ξ : G → F) (p : G × G × G) :

((G × F) × G × F) × (G × F) × G × F

Four graph points forming the additive-energy parallelogram parametrized by p.

Equations

TrilinearHT.Auto.graphEnergyQuad ξ p = (((p.1, ξ p.1), p.1 + p.2.1, ξ (p.1 + p.2.1)), (p.2.2 + p.2.1, ξ (p.2.2 + p.2.1)), p.2.2, ξ p.2.2)

Instances For

theorem TrilinearHT.Auto.graphEnergyTriples_card {G : Type u_1} {F : Type u_2} [AddCommGroup G] [Fintype G] [DecidableEq G] [AddCommGroup F] [DecidableEq F] (H : Finset G) (ξ : G → F) :

(graphEnergyTriples H ξ).card = (finiteFunctionGraph H ξ).addEnergy (finiteFunctionGraph H ξ)

The shift-triple count is exactly the standard additive energy of the graph.

noncomputable def TrilinearHT.Auto.graphPhase {q : ℕ} [NeZero q] (H : Finset (ZMod q)) (ξ : ZMod q → ZMod q) (h k : ZMod q) :

The character associated with a graph point, zero outside the graph's domain.

Equations

TrilinearHT.Auto.graphPhase H ξ h k = if h ∈ H then ZMod.stdAddChar (ξ h * k) else 0

Instances For

theorem TrilinearHT.Auto.graph_character_orthogonality {q : ℕ} [NeZero q] (ζ : ZMod q) :

(Finset.univ.expect fun (k : ZMod q) => ZMod.stdAddChar (ζ * k)) = if ζ = 0 then 1 else 0

theorem TrilinearHT.Auto.graph_stdChar_conj {q : ℕ} [NeZero q] (x : ZMod q) :

(starRingEnd ℂ) (ZMod.stdAddChar x) = ZMod.stdAddChar (-x)

theorem TrilinearHT.Auto.graphPhase_orthogonality {q : ℕ} [NeZero q] (H : Finset (ZMod q)) (ξ : ZMod q → ZMod q) (h u t : ZMod q) :

(Finset.univ.expect fun (k : ZMod q) => graphPhase H ξ h k * (starRingEnd ℂ) (graphPhase H ξ (h + u) k) * (starRingEnd ℂ) (graphPhase H ξ t k * (starRingEnd ℂ) (graphPhase H ξ (t + u) k))) = if (h, u, t) ∈ graphEnergyTriples H ξ then 1 else 0

Character orthogonality detects exactly the graph parallelogram relation.

theorem TrilinearHT.Auto.finite_expect_rotate_four {I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} [Fintype I] [Fintype J] [Fintype K] [Fintype L] (f : I → J → K → L → ℂ) :

(Finset.univ.expect fun (i : I) => Finset.univ.expect fun (j : J) => Finset.univ.expect fun (k : K) => Finset.univ.expect fun (l : L) => f i j k l) = Finset.univ.expect fun (j : J) => Finset.univ.expect fun (k : K) => Finset.univ.expect fun (l : L) => Finset.univ.expect fun (i : I) => f i j k l

theorem TrilinearHT.Auto.finiteTripleIndicator_average {G : Type u_1} [Fintype G] [DecidableEq G] (T : Finset (G × G × G)) :

(Finset.univ.expect fun (a : G) => Finset.univ.expect fun (b : G) => Finset.univ.expect fun (c : G) => if (a, b, c) ∈ T then 1 else 0) = ↑T.card / ↑(Fintype.card G) ^ 3

A triple indicator average is its exact count divided by the cube of the ambient size.

theorem TrilinearHT.Auto.graphPhase_energy {q : ℕ} [NeZero q] (H : Finset (ZMod q)) (ξ : ZMod q → ZMod q) :

(Finset.univ.expect fun (k : ZMod q) => Finset.univ.expect fun (u : ZMod q) => ‖Finset.univ.expect fun (h : ZMod q) => graphPhase H ξ h k * (starRingEnd ℂ) (graphPhase H ξ (h + u) k)‖ ^ 2) = ↑((finiteFunctionGraph H ξ).addEnergy (finiteFunctionGraph H ξ)) / ↑q ^ 3

The differenced graph characters have exactly normalized additive energy. This is the character-orthogonality count in lem:derivative-graph, lines 856-861.

theorem TrilinearHT.Auto.finiteFunctionGraph_card {G : Type u_1} {F : Type u_2} [DecidableEq G] [DecidableEq F] (H : Finset G) (ξ : G → F) :

(finiteFunctionGraph H ξ).card = H.card

theorem TrilinearHT.Auto.finiteFunctionGraph_subset {G : Type u_1} {F : Type u_2} [DecidableEq G] [DecidableEq F] (H : Finset G) (ξ : G → F) (T : Finset (G × F)) (hT : T ⊆ finiteFunctionGraph H ξ) :

∃ H' ⊆ H, T = finiteFunctionGraph H' ξ ∧ H'.card = T.card

Every subset of a function graph is the same function restricted to its projected domain.

theorem TrilinearHT.Auto.graph_balog_szemeredi_gowers {G : Type u_1} {F : Type u_2} [AddCommGroup G] [DecidableEq G] [AddCommGroup F] [DecidableEq F] (H : Finset G) (hH : H.Nonempty) (ξ : G → F) {K : ℝ} (hK : 1 ≤ K) (henergy : ↑H.card ^ 3 / K ≤ ↑((finiteFunctionGraph H ξ).addEnergy (finiteFunctionGraph H ξ))) :

∃ H' ⊆ H, ↑H.card / (80000000000 * K) ≤ ↑H'.card ∧ ↑(finiteFunctionGraph H' ξ - finiteFunctionGraph H' ξ).card ≤ 10 ^ 25 * K ^ 10 * ↑H'.card

BSG preserves the graph structure and the original frequency function on a large domain.

def TrilinearHT.Auto.graphVerticalDifferences {G : Type u_1} {F : Type u_2} [AddCommGroup G] [DecidableEq G] [AddCommGroup F] [DecidableEq F] (Γ : Finset (G × F)) (m n : ℕ) :

Finset F

The vertical fiber of an iterated difference of a finite subset of a product group.

Equations

TrilinearHT.Auto.graphVerticalDifferences Γ m n = Finset.image Prod.snd ({p ∈ m • Γ - n • Γ | p.1 = 0})

Instances For

theorem TrilinearHT.Auto.mem_graphVerticalDifferences {G : Type u_1} {F : Type u_2} [AddCommGroup G] [DecidableEq G] [AddCommGroup F] [DecidableEq F] (Γ : Finset (G × F)) (m n : ℕ) (χ : F) :

χ ∈ graphVerticalDifferences Γ m n ↔ (0, χ) ∈ m • Γ - n • Γ

theorem TrilinearHT.Auto.graphVerticalDifferences_card_mul_le {G : Type u_1} {F : Type u_2} [AddCommGroup G] [DecidableEq G] [AddCommGroup F] [DecidableEq F] (H : Finset G) (ξ : G → F) (m n : ℕ) :

(finiteFunctionGraph H ξ).card * (graphVerticalDifferences (finiteFunctionGraph H ξ) m n).card ≤ ((m + 1) • finiteFunctionGraph H ξ - n • finiteFunctionGraph H ξ).card

Translating graph points by vertical differences is injective.

theorem TrilinearHT.Auto.graphVerticalDifferences_card_le {G : Type u_1} {F : Type u_2} [AddCommGroup G] [DecidableEq G] [AddCommGroup F] [DecidableEq F] (H : Finset G) (hH : H.Nonempty) (ξ : G → F) {K : ℝ} (_hK : 1 ≤ K) (hsmall : ↑(finiteFunctionGraph H ξ - finiteFunctionGraph H ξ).card ≤ K * ↑H.card) (m n : ℕ) :

↑(graphVerticalDifferences (finiteFunctionGraph H ξ) m n).card ≤ K ^ (m + 1 + n)

Pluennecke-Ruzsa bounds the vertical fiber of every iterated graph difference.

theorem TrilinearHT.Auto.graphVerticalDifferences_eight_card_le {G : Type u_1} {F : Type u_2} [AddCommGroup G] [DecidableEq G] [AddCommGroup F] [DecidableEq F] (H : Finset G) (hH : H.Nonempty) (ξ : G → F) {K : ℝ} (hK : 1 ≤ K) (hsmall : ↑(finiteFunctionGraph H ξ - finiteFunctionGraph H ξ).card ≤ K * ↑H.card) :

↑(graphVerticalDifferences (finiteFunctionGraph H ξ) 8 8).card ≤ K ^ 17

Blueprint lem:local-frequency, lines 883-885: the vertical obstruction set has size K^17.

theorem TrilinearHT.Auto.iterated_difference_phase_bound {G : Type u_1} {E : Type u_2} [AddCommGroup G] [DecidableEq G] [SeminormedAddCommGroup E] (φ : G →+ E) (A : Finset G) (ε : ℝ) (hA : ∀ a ∈ A, ∀ b ∈ A, ‖φ (a - b)‖ ≤ ε) (m : ℕ) (z : G) (hz : z ∈ m • A - m • A) :

‖φ z‖ ≤ ↑m * ε

A uniform phase bound on pairwise differences extends linearly to iterated differences.

theorem TrilinearHT.Auto.iterated_graph_of_no_vertical {G : Type u_1} {F : Type u_2} [AddCommGroup G] [DecidableEq G] [AddCommGroup F] [DecidableEq F] (Γ : Finset (G × F)) (m : ℕ) (hzero : ∀ (χ : F), (0, χ) ∈ (m + m) • Γ - (m + m) • Γ → χ = 0) :

Set.InjOn Prod.fst ↑(m • Γ - m • Γ)

Absence of vertical differences in the doubled difference set implies a graph property.

theorem TrilinearHT.Auto.cyclic_graph_cube_no_vertical {G : Type u_1} [AddCommGroup G] [DecidableEq G] {q d : ℕ} [NeZero q] (H H' : Finset G) (ξ : G → ZMod q) (hsub : H' ⊆ H) (g : Fin d → ZMod q) (hsep : ∀ χ ∈ graphVerticalDifferences (finiteFunctionGraph H ξ) 8 8, χ ≠ 0 → ∃ (j : Fin d), 1 / 8 ≤ ‖ZMod.toAddCircle (χ * g j)‖) (hcube : ∀ h ∈ H', ∀ h' ∈ H', ∀ (j : Fin d), ‖ZMod.toAddCircle ((ξ h - ξ h') * g j)‖ < 1 / 256) (χ : ZMod q) :

(0, χ) ∈ 8 • finiteFunctionGraph H' ξ - 8 • finiteFunctionGraph H' ξ → χ = 0

Character separation and one common cube eliminate all vertical eightfold differences.

theorem TrilinearHT.Auto.graphVerticalDifferences_nonempty {G : Type u_1} {F : Type u_2} [AddCommGroup G] [DecidableEq G] [AddCommGroup F] [DecidableEq F] (H : Finset G) (hH : H.Nonempty) (ξ : G → F) (m : ℕ) :

(graphVerticalDifferences (finiteFunctionGraph H ξ) m m).Nonempty

A nonempty graph has zero in every equal-order vertical difference set.

theorem TrilinearHT.Auto.cyclic_graph_refinement {q : ℕ} [NeZero q] (H : Finset (ZMod q)) (hH : H.Nonempty) (ξ : ZMod q → ZMod q) :

∃ H' ⊆ H, H'.Nonempty ∧ ↑H.card / 256 ^ ⌈Real.log (2 * ↑(graphVerticalDifferences (finiteFunctionGraph H ξ) 8 8).card) / Real.log 2⌉₊ ≤ ↑H'.card ∧ Set.InjOn Prod.fst ↑(4 • finiteFunctionGraph H' ξ - 4 • finiteFunctionGraph H' ξ)

The source logarithmic cube refinement makes the fourfold difference set a graph.

@[reducible, inline]

noncomputable abbrev TrilinearHT.Auto.graphBohrSet {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (ρ : ℝ) :

Finset (ZMod q)

The cyclic Bohr domain used for the local graph model.

Equations

TrilinearHT.Auto.graphBohrSet S ρ = TrilinearHT.Auto.cyclicBohrSet S ρ

Instances For

theorem TrilinearHT.Auto.mem_graphBohrSet {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (ρ : ℝ) (u : ZMod q) :

u ∈ graphBohrSet S ρ ↔ ∀ s ∈ S, ‖ZMod.toAddCircle (s * u)‖ < ρ

theorem TrilinearHT.Auto.zero_mem_graphBohrSet {q : ℕ} [NeZero q] (S : Finset (ZMod q)) {ρ : ℝ} (hρ : 0 < ρ) :

0 ∈ graphBohrSet S ρ

theorem TrilinearHT.Auto.cyclic_small_bohr_domain {q : ℕ} [NeZero q] (H : Finset (ZMod q)) (hH : H.Nonempty) :

∃ (S : Finset (ZMod q)) (ρ : ℝ), 1 ∈ S ∧ 0 < ρ ∧ ρ < 1 / 100 ∧ ↑S.card + Real.log (1 / ρ) ≤ 10 ^ 20 * (1 + Real.log (1 / (↑H.card / ↑q))) ^ 4 ∧ graphBohrSet S ρ ⊆ 2 • H - 2 • H

Dense Bogolyubov with the unit frequency, the source small radius, and a single polynomial bound for rank plus logarithmic reciprocal radius.

theorem TrilinearHT.Auto.finiteFunctionGraph_image_fst {G : Type u_1} {F : Type u_2} [DecidableEq G] [DecidableEq F] (H : Finset G) (ξ : G → F) :

Finset.image Prod.fst (finiteFunctionGraph H ξ) = H

The first projection of a finite function graph is its domain.

theorem TrilinearHT.Auto.graph_difference_lift {G : Type u_1} {F : Type u_2} [AddCommGroup G] [DecidableEq G] [AddCommGroup F] [DecidableEq F] (H : Finset G) (ξ : G → F) (m : ℕ) (u : G) (hu : u ∈ m • H - m • H) :

∃ (v : F), (u, v) ∈ m • finiteFunctionGraph H ξ - m • finiteFunctionGraph H ξ

Every point of an iterated domain difference has a frequency lift in the graph difference.

theorem TrilinearHT.Auto.zero_mem_iterated_difference {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) (hA : A.Nonempty) (m : ℕ) :

0 ∈ m • A - m • A

Zero belongs to every equal-order difference of a nonempty set.

theorem TrilinearHT.Auto.add_mem_doubled_difference {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) (m : ℕ) {x y : G} (hx : x ∈ m • A - m • A) (hy : y ∈ m • A - m • A) :

x + y ∈ (m + m) • A - (m + m) • A

Adding two equal-order differences doubles their order.

theorem TrilinearHT.Auto.difference_subset_double_difference {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) (hA : A.Nonempty) :

A - A ⊆ 2 • A - 2 • A

Padding both sides by the same point embeds a difference set into its double.

theorem TrilinearHT.Auto.local_graph_frequency_lift {G : Type u_1} {F : Type u_2} [AddCommGroup G] [DecidableEq G] [AddCommGroup F] [DecidableEq F] (H : Finset G) (hH : H.Nonempty) (ξ : G → F) (B : Finset G) (hBzero : 0 ∈ B) (hB : B ⊆ 2 • H - 2 • H) (hgraph : Set.InjOn Prod.fst ↑(4 • finiteFunctionGraph H ξ - 4 • finiteFunctionGraph H ξ)) :

∃ (f : G → F), f 0 = 0 ∧ (∀ u ∈ B, (u, f u) ∈ 2 • finiteFunctionGraph H ξ - 2 • finiteFunctionGraph H ξ) ∧ (∀ a ∈ B, ∀ b ∈ B, ∀ c ∈ B, ∀ d ∈ B, a + b = c + d → f a + f b = f c + f d) ∧ ∀ h ∈ H, ∀ h' ∈ H, h - h' ∈ B → f (h - h') = ξ h - ξ h'

A domain inside a double difference set has a unique frequency lift; injectivity on the fourfold graph gives the full order-two Freiman identity.

theorem TrilinearHT.Auto.cyclic_local_frequency_map {q : ℕ} (hq : Odd q) (H : Finset (ZMod q)) (hH : H.Nonempty) (ξ : ZMod q → ZMod q) (B : Finset (ZMod q)) (hBzero : 0 ∈ B) (hB : B ⊆ 2 • H - 2 • H) (hgraph : Set.InjOn Prod.fst ↑(4 • finiteFunctionGraph H ξ - 4 • finiteFunctionGraph H ξ)) :

∃ (M : ZMod q → ZMod q), M 0 = 0 ∧ (∀ a ∈ B, ∀ b ∈ B, ∀ c ∈ B, ∀ d ∈ B, a + b = c + d → 2 * M a + 2 * M b = 2 * M c + 2 * M d) ∧ (∀ u ∈ B, ∀ v ∈ B, u + v ∈ B → M (u + v) = M u + M v) ∧ ∀ h ∈ H, ∀ h' ∈ H, h - h' ∈ B → ξ h - ξ h' = 2 * M (h - h')

In odd cyclic groups the unique graph frequency lift can be halved, retaining Freiman order two, local additivity, and all original graph differences.

theorem TrilinearHT.Auto.logarithmic_cube_partition_cost {x : ℝ} (hx : 1 ≤ x) :

256 ^ ⌈Real.log (2 * x) / Real.log 2⌉₊ ≤ 65536 * x ^ 8

The exact logarithmic test count gives a polynomial cube-partition cost.

theorem TrilinearHT.Auto.cyclic_graph_refinement_polynomial {q : ℕ} [NeZero q] (H : Finset (ZMod q)) (hH : H.Nonempty) (ξ : ZMod q → ZMod q) {K : ℝ} (hK : 1 ≤ K) (hsmall : ↑(finiteFunctionGraph H ξ - finiteFunctionGraph H ξ).card ≤ K * ↑H.card) :

∃ H' ⊆ H, H'.Nonempty ∧ ↑H.card / ↑q / (65536 * K ^ 136) ≤ ↑H'.card / ↑q ∧ Set.InjOn Prod.fst ↑(4 • finiteFunctionGraph H' ξ - 4 • finiteFunctionGraph H' ξ)

Graph refinement loses only a fixed polynomial of the difference-set constant.

theorem TrilinearHT.Auto.polynomial_density_after_loss {δ α β C D K : ℝ} (hδ : 0 < δ) (hC : 0 < C) (hD : 0 < D) (hK : 0 < K) (a b n : ℕ) (hα : δ ^ a / C ≤ α) (hβ : α / (D * (K / δ ^ b) ^ n) ≤ β) :

δ ^ (a + b * n) / (C * D * K ^ n) ≤ β

Composition of polynomial density with a polynomial loss, with exact exponents.

theorem TrilinearHT.Auto.log_inverse_le_of_power_density {α δ C : ℝ} (hα : 0 < α) (hδ : 0 < δ) (hC : 0 < C) (n : ℕ) (h : δ ^ n / C ≤ α) :

Real.log (1 / α) ≤ Real.log C + ↑n * Real.log (1 / δ)

A polynomial density lower bound gives the corresponding logarithmic upper bound.

noncomputable def TrilinearHT.Auto.localSymmetryInnerRadius (C : ℝ) (d : ℕ) (r ζ : ℝ) :

An explicit inner radius with room for every local-symmetry substitution.

Equations

TrilinearHT.Auto.localSymmetryInnerRadius C d r ζ = r * min 1 (ζ ^ 2) / (1000 * (C + 1) * (↑d + 1))

Instances For

theorem TrilinearHT.Auto.finite_gowersNorm_pow {G : Type u_1} [AddCommGroup G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] [MeasurableAdd₂ G] {j : ℕ} (hj : 1 ≤ j) (f : G → ℂ) :

gowersNorm (finiteHaar G) j f ^ 2 ^ j = (cubeAverage (finiteHaar G) j fun (x : Fin j → Bool) => f).re

theorem TrilinearHT.Auto.finiteFourier_reflect_conj {q : ℕ} [NeZero q] (f : ZMod q → ℂ) (ξ : ZMod q) :

finiteFourier (fun (x : ZMod q) => (starRingEnd ℂ) (f (-x))) ξ = (starRingEnd ℂ) (finiteFourier f ξ)

theorem TrilinearHT.Auto.finite_cubeAverage_sq {G : Type u_1} [AddCommGroup G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] [MeasurableAdd₂ G] (j : ℕ) (f : G → ℂ) :

(cubeAverage (finiteHaar G) (j + 1) fun (x : Fin (j + 1) → Bool) => f) = ↑(uniformMean fun (h : Fin j → G) => ‖uniformMean (diagonalCubeIntegrand j f h)‖ ^ 2)

theorem TrilinearHT.Auto.diagonalCubeIntegrand_one {G : Type u_1} [AddCommGroup G] (f : G → ℂ) (h : Fin 1 → G) (x : G) :

diagonalCubeIntegrand 1 f h x = f x * (starRingEnd ℂ) (f (x + h 0))

theorem TrilinearHT.Auto.finiteFourier_gowers_two {q : ℕ} [NeZero q] (f : ZMod q → ℂ) :

gowersNorm (finiteHaar (ZMod q)) 2 f ^ 4 = ∑ ξ : ZMod q, ‖finiteFourier f ξ‖ ^ 4

theorem TrilinearHT.Auto.uniformMean_fin_cons {G : Type u_1} {E : Type u_2} [Fintype G] [AddCommMonoid E] [Module ℝ E] (j : ℕ) (f : (Fin (j + 1) → G) → E) :

uniformMean f = uniformMean fun (t : G) => uniformMean fun (h : Fin j → G) => f (Fin.cons t h)

theorem TrilinearHT.Auto.finite_cubeAverage_recursion {G : Type u_1} [AddCommGroup G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] (j : ℕ) (f : G → ℂ) :

(cubeAverage (finiteHaar G) (j + 1) fun (x : Fin (j + 1) → Bool) => f) = uniformMean fun (t : G) => cubeAverage (finiteHaar G) j fun (x : Fin j → Bool) (x_1 : G) => f x_1 * (starRingEnd ℂ) (f (x_1 + t))

theorem TrilinearHT.Auto.uniformMean_re {G : Type u_1} [Fintype G] (f : G → ℂ) :

(uniformMean f).re = uniformMean fun (x : G) => (f x).re

theorem TrilinearHT.Auto.finite_gowers_three_recursion {G : Type u_1} [AddCommGroup G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] [MeasurableAdd₂ G] (f : G → ℂ) :

gowersNorm (finiteHaar G) 3 f ^ 8 = uniformMean fun (t : G) => (gowersNorm (finiteHaar G) 2 fun (x : G) => f (x + t) * (starRingEnd ℂ) (f x)) ^ 4

The source's U³ recursion, with its stated multiplicative-difference convention.

Difference-set growth from minimal growth #

Chang's theorem with the source Fourier normalization #

Derivative graph frequency selection #

theorem TrilinearHT.Auto.uniformMean_upper_level_density {G : Type u_1} [Fintype G] [Nonempty G] (u : G → ℝ) {a : ℝ} (ha : 0 ≤ a) (hu : ∀ (x : G), u x ≤ 1) (hm : a ≤ uniformMean u) :

a / 2 ≤ ↑{x : G | a / 2 ≤ u x}.card / ↑(Fintype.card G)

A bounded function with large mean has a dense upper level set.

theorem TrilinearHT.Auto.finiteFourier_norm_le_one {q : ℕ} [NeZero q] (f : ZMod q → ℂ) (hf : ∀ (x : ZMod q), ‖f x‖ ≤ 1) (ξ : ZMod q) :

‖finiteFourier f ξ‖ ≤ 1

theorem TrilinearHT.Auto.derivative_frequency_selection {q : ℕ} [NeZero q] (f : ZMod q → ℂ) (hf : ∀ (x : ZMod q), ‖f x‖ ≤ 1) {δ : ℝ} (hδ : 0 < δ) (hU : δ ≤ gowersNorm (finiteHaar (ZMod q)) 3 f) :

∃ (H : Finset (ZMod q)) (ξ : ZMod q → ZMod q), δ ^ 8 / 2 ≤ ↑H.card / ↑q ∧ ∀ h ∈ H, δ ^ 4 / √2 ≤ ‖finiteFourier (fun (x : ZMod q) => f (x + h) * (starRingEnd ℂ) (f x)) (ξ h)‖

Blueprint lem:derivative-graph, lines 829-835: a large U³ norm supplies a dense set of derivatives with a selected Fourier coefficient of size at least delta^4/sqrt(2).

Squared derivative correlation #

theorem TrilinearHT.Auto.finiteFourier_correlation_square {q : ℕ} [NeZero q] (g : ZMod q → ℂ) (ξ : ZMod q) :

(finiteAverage fun (x : ZMod q) => finiteAverage fun (k : ZMod q) => g x * (starRingEnd ℂ) (g (x + k)) * ZMod.stdAddChar (ξ * k)) = ↑(‖finiteFourier g ξ‖ ^ 2)

Fourier correlation squared, expressed by a translated autocorrelation average.

theorem TrilinearHT.Auto.derivative_correlation_square {q : ℕ} [NeZero q] (f : ZMod q → ℂ) (h ξ : ZMod q) :

(finiteAverage fun (x : ZMod q) => finiteAverage fun (k : ZMod q) => f (x + k) * (starRingEnd ℂ) (f x) * (starRingEnd ℂ) (f (x + h + k) * (starRingEnd ℂ) (f (x + h))) * ZMod.stdAddChar (ξ * k)) = ↑(‖finiteFourier (fun (x : ZMod q) => f (x + h) * (starRingEnd ℂ) (f x)) ξ‖ ^ 2)

The two derivative factors in the source give the square of a derivative Fourier coefficient.

noncomputable def TrilinearHT.Auto.derivativeGraphKernel {q : ℕ} (f : ZMod q → ℂ) (x k : ZMod q) :

The bounded two-variable derivative kernel in the derivative-graph argument.

Equations

TrilinearHT.Auto.derivativeGraphKernel f x k = f (x + k) * (starRingEnd ℂ) (f x)

Instances For

@[reducible, inline]

noncomputable abbrev TrilinearHT.Auto.derivativeGraphCharacter {q : ℕ} [NeZero q] (H : Finset (ZMod q)) (ξ : ZMod q → ZMod q) (h k : ZMod q) :

The selected character, extended by zero outside the selected derivative set.

Equations

TrilinearHT.Auto.derivativeGraphCharacter H ξ h k = TrilinearHT.Auto.graphPhase H ξ h k

Instances For

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

The source's positive trilinear correlation quantity.

Equations

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

Instances For

theorem TrilinearHT.Auto.derivativeGraphCorrelation_eq {q : ℕ} [NeZero q] (f : ZMod q → ℂ) (H : Finset (ZMod q)) (ξ : ZMod q → ZMod q) :

derivativeGraphCorrelation f H ξ = ↑(uniformMean fun (h : ZMod q) => if h ∈ H then ‖finiteFourier (fun (x : ZMod q) => f (x + h) * (starRingEnd ℂ) (f x)) (ξ h)‖ ^ 2 else 0)

Blueprint lem:derivative-graph, lines 836-841: the trilinear correlation is a nonnegative real average of squared derivative Fourier coefficients.

theorem TrilinearHT.Auto.derivativeGraphCorrelation_re_nonneg {q : ℕ} [NeZero q] (f : ZMod q → ℂ) (H : Finset (ZMod q)) (ξ : ZMod q → ZMod q) :

0 ≤ (derivativeGraphCorrelation f H ξ).re

theorem TrilinearHT.Auto.derivativeGraphCorrelation_lower {q : ℕ} [NeZero q] (f : ZMod q → ℂ) (H : Finset (ZMod q)) (ξ : ZMod q → ZMod q) {δ : ℝ} (hδ : 0 < δ) (hH : δ ^ 8 / 2 ≤ ↑H.card / ↑q) (hc : ∀ h ∈ H, δ ^ 4 / √2 ≤ ‖finiteFourier (fun (x : ZMod q) => f (x + h) * (starRingEnd ℂ) (f x)) (ξ h)‖) :

δ ^ 16 / 4 ≤ (derivativeGraphCorrelation f H ξ).re

The source density and derivative correlation bounds give T >= delta^16/4.

theorem TrilinearHT.Auto.derivativeGraphCorrelation_norm_eq_re {q : ℕ} [NeZero q] (f : ZMod q → ℂ) (H : Finset (ZMod q)) (ξ : ZMod q → ZMod q) :

‖derivativeGraphCorrelation f H ξ‖ = (derivativeGraphCorrelation f H ξ).re

First derivative-graph Cauchy-Schwarz step #

theorem TrilinearHT.Auto.derivativeGraphKernel_norm_le {q : ℕ} (f : ZMod q → ℂ) (hf : ∀ (x : ZMod q), ‖f x‖ ≤ 1) (x k : ZMod q) :

‖derivativeGraphKernel f x k‖ ≤ 1

theorem TrilinearHT.Auto.derivativeGraphCorrelation_eq_shift {q : ℕ} [NeZero q] (f : ZMod q → ℂ) (H : Finset (ZMod q)) (ξ : ZMod q → ZMod q) :

derivativeGraphCorrelation f H ξ = finiteShiftCorrelation (derivativeGraphKernel f) (derivativeGraphCharacter H ξ)

theorem TrilinearHT.Auto.derivativeGraphCorrelation_fourth_le {q : ℕ} [NeZero q] (f : ZMod q → ℂ) (hf : ∀ (x : ZMod q), ‖f x‖ ≤ 1) (H : Finset (ZMod q)) (ξ : ZMod q → ZMod q) :

‖derivativeGraphCorrelation f H ξ‖ ^ 4 ≤ finiteShiftEnergy (derivativeGraphCharacter H ξ)

Blueprint lem:derivative-graph, lines 849-855: two Cauchy-Schwarz steps leave only the squared averages of differenced selected characters.

theorem TrilinearHT.Auto.derivativeGraphCharacter_energy {q : ℕ} [NeZero q] (H : Finset (ZMod q)) (ξ : ZMod q → ZMod q) :

finiteShiftEnergy (derivativeGraphCharacter H ξ) = ↑((Finset.image (fun (h : ZMod q) => (h, ξ h)) H).addEnergy (Finset.image (fun (h : ZMod q) => (h, ξ h)) H)) / ↑q ^ 3

Blueprint lem:derivative-graph, lines 856-861: the character average is exactly the additive energy of the selected graph, divided by the cube of the ambient group size.

theorem TrilinearHT.Auto.derivative_graph_energy {q : ℕ} [NeZero q] (f : ZMod q → ℂ) (hf : ∀ (x : ZMod q), ‖f x‖ ≤ 1) {δ : ℝ} (hδ : 0 < δ) (hU : δ ≤ gowersNorm (finiteHaar (ZMod q)) 3 f) :

∃ (H : Finset (ZMod q)) (ξ : ZMod q → ZMod q), δ ^ 8 / 2 ≤ ↑H.card / ↑q ∧ (∀ h ∈ H, δ ^ 4 / √2 ≤ ‖finiteFourier (fun (x : ZMod q) => f (x + h) * (starRingEnd ℂ) (f x)) (ξ h)‖) ∧ δ ^ 64 / 256 * ↑q ^ 3 ≤ ↑((Finset.image (fun (h : ZMod q) => (h, ξ h)) H).addEnergy (Finset.image (fun (h : ZMod q) => (h, ξ h)) H))

Blueprint lem:derivative-graph, lines 822-863: a bounded function with U³ >= delta has a dense derivative-frequency graph retaining correlations delta^4/sqrt(2) and additive energy at least delta^64 |G|^3 / 256. All frequencies and graph points are actual cyclic group elements, and energy is Mathlib's unnormalized additive-energy count.

Small-difference derivative subgraph #

theorem TrilinearHT.Auto.derivative_graph_small_difference {q : ℕ} [NeZero q] (f : ZMod q → ℂ) (hf : ∀ (x : ZMod q), ‖f x‖ ≤ 1) {δ : ℝ} (hδ : 0 < δ) (hU : δ ≤ gowersNorm (finiteHaar (ZMod q)) 3 f) :

∃ (H : Finset (ZMod q)) (ξ : ZMod q → ZMod q), δ ^ 72 / 10 ^ 14 ≤ ↑H.card / ↑q ∧ (∀ h ∈ H, δ ^ 4 / √2 ≤ ‖finiteFourier (fun (x : ZMod q) => f (x + h) * (starRingEnd ℂ) (f x)) (ξ h)‖) ∧ ↑(finiteFunctionGraph H ξ - finiteFunctionGraph H ξ).card ≤ 10 ^ 50 / δ ^ 640 * ↑H.card

Blueprint lem:local-frequency, line 881: BSG retains derivative correlations on a polynomial-density subgraph with a polynomial difference-set constant.

Quantitative locally additive derivative frequency #

noncomputable def TrilinearHT.Auto.localFrequencyDensityCost :

Explicit universal loss in the local derivative-frequency estimate.

Equations

TrilinearHT.Auto.localFrequencyDensityCost = 10 ^ 14 * 65536 * (10 ^ 50) ^ 136

Instances For