The quasipolynomial dense Bogolyubov theorem

This file was automatically generated by Codex.

For a nonempty subset of a finite cyclic group of density alpha, its double difference set contains a Bohr set of rank O(log^4(1/alpha)), reciprocal radius O(alpha^(-1) log^4(1/alpha)), and density exp(-O(log^5(1/alpha))). The proof combines sampling almost periods, Chang's spectrum theorem and finite Fourier analysis. Statements and local definitions use Mathlib and local vocabulary; proofs reuse the previously verified sampling and spectrum prerequisites. Reference: blueprint lem:dense-Bohr, lines 786-820.

noncomputable def TrilinearHT.Auto.bogolyubovBaseFunction {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) (x : G) : ℝ

The positive source witness mu_A * mu_A * 1_{-(A+A)}, expressed using probability averages on A so the normalization is explicit.

Equations

• TrilinearHT.Auto.bogolyubovBaseFunction A x = A.expect fun (a : G) => A.expect fun (b : G) => if x - a - b ∈ -(A + A) then 1 else 0

theorem TrilinearHT.Auto.bogolyubovBaseFunction_zero {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) (hA : A.Nonempty) : bogolyubovBaseFunction A 0 = 1

The witness is exactly one at the identity, not merely bounded below.

theorem TrilinearHT.Auto.bogolyubov_pair_mem_difference {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) {x a b : G} (ha : a ∈ A) (hb : b ∈ A) (h : x - a - b ∈ -(A + A)) : x ∈ 2 • A - 2 • A

Every contributing pair in the witness certifies membership in the double difference set.

theorem TrilinearHT.Auto.bogolyubovBaseFunction_eq_zero_of_notMem {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) {x : G} (hx : x ∉ 2 • A - 2 • A) : bogolyubovBaseFunction A x = 0

The witness vanishes outside the actual sum-difference set.

theorem TrilinearHT.Auto.bogolyubovBaseFunction_pos_mem {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) {x : G} (hx : 0 < bogolyubovBaseFunction A x) : x ∈ 2 • A - 2 • A

Positivity of the witness is sufficient for the desired containment.

theorem TrilinearHT.Auto.bogolyubov_expect_norm_rpow_le {G : Type u_1} (A : Finset G) (hA : A.Nonempty) (f : G → ℂ) {p : ℝ} (hp : 1 ≤ p) : ‖A.expect fun (a : G) => f a‖ ^ p ≤ A.expect fun (a : G) => ‖f a‖ ^ p

Jensen's inequality for the probability average on a nonempty finite set.

theorem TrilinearHT.Auto.bogolyubov_expect_subset_le {G : Type u_1} [Fintype G] (A : Finset G) (f : G → ℝ) (hf : ∀ (x : G), 0 ≤ f x) : (A.expect fun (a : G) => f a) ≤ ↑(Fintype.card G) / ↑A.card * Finset.univ.expect fun (x : G) => f x

Restricting a nonnegative probability average costs the reciprocal density.

theorem TrilinearHT.Auto.bogolyubov_expect_norm_le {G : Type u_1} [Fintype G] (A : Finset G) (hA : A.Nonempty) (f : G → ℂ) {p : ℝ} (hp : 1 ≤ p) : ‖A.expect fun (a : G) => f a‖ ≤ (↑(Fintype.card G) / ↑A.card) ^ (1 / p) * (Finset.univ.expect fun (x : G) => ‖f x‖ ^ p) ^ (1 / p)

The finite probability-measure Holder estimate used to amplify almost periods.

noncomputable def TrilinearHT.Auto.bogolyubovAverage {G : Type u_1} [AddCommGroup G] (A : Finset G) (f : G → ℂ) (x : G) : ℂ

Convolution with the uniform probability measure on a finite set.

Equations

• TrilinearHT.Auto.bogolyubovAverage A f x = A.expect fun (a : G) => f (x - a)

theorem TrilinearHT.Auto.bogolyubovAverage_norm_le {G : Type u_1} [AddCommGroup G] [Fintype G] (A : Finset G) (hA : A.Nonempty) (f : G → ℂ) {p : ℝ} (hp : 1 ≤ p) (x : G) : ‖bogolyubovAverage A f x‖ ≤ (↑(Fintype.card G) / ↑A.card) ^ (1 / p) * (Finset.univ.expect fun (y : G) => ‖f y‖ ^ p) ^ (1 / p)

A pointwise estimate for averaging an arbitrary function on a translate of A.

theorem TrilinearHT.Auto.bogolyubovAverage_translation_le {G : Type u_1} [AddCommGroup G] [Fintype G] (A : Finset G) (hA : A.Nonempty) (f : G → ℂ) {p : ℝ} (hp : 1 ≤ p) (u x : G) : ‖bogolyubovAverage A f (x + u) - bogolyubovAverage A f x‖ ≤ (↑(Fintype.card G) / ↑A.card) ^ (1 / p) * (Finset.univ.expect fun (y : G) => ‖f (y + u) - f y‖ ^ p) ^ (1 / p)

Convolution turns an L^p translation bound into a uniform bound.

theorem TrilinearHT.Auto.bogolyubov_density_loss_le {α : ℝ} (hα : 0 < α) : (1 / α) ^ (1 / max 2 (Real.log (1 / α))) ≤ Real.exp 1

The density loss is at most e for the source's choice of the real exponent.

theorem TrilinearHT.Auto.bogolyubov_double_average_almost_periods {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (A : Finset G) (hA : A.Nonempty) (f : G → ℂ) (hf : ∀ (x : G), ‖f x‖ ≤ 1) {p ε : ℝ} (hp : 2 ≤ p) (hε : 0 < ε) : ∃ (X : Finset G), X.Nonempty ∧ (↑A.card / ↑(Fintype.card G)) ^ ⌈64 * p / ε ^ 2⌉₊ / 2 ≤ ↑X.card / ↑(Fintype.card G) ∧ ∀ (k : ℕ), ∀ u ∈ k • X - k • X, ∀ (x : G), ‖bogolyubovAverage A (bogolyubovAverage A f) (x + u) - bogolyubovAverage A (bogolyubovAverage A f) x‖ ≤ (↑(Fintype.card G) / ↑A.card) ^ (1 / p) * (2 * ↑k * ε)

Sampling almost periods after the second convolution, for any bounded input.

theorem TrilinearHT.Auto.bogolyubovBaseFunction_eq_double_average {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) (x : G) : ↑(bogolyubovBaseFunction A x) = bogolyubovAverage A (bogolyubovAverage A fun (y : G) => if y ∈ -(A + A) then 1 else 0) x

The real positive witness is the actual double convolution of the indicator.

noncomputable def TrilinearHT.Auto.bogolyubovExponent (α : ℝ) : ℝ

The source's real exponent, logarithmic number of iterations and tolerance.

Equations

• TrilinearHT.Auto.bogolyubovExponent α = max 2 (Real.log (1 / α))

noncomputable def TrilinearHT.Auto.bogolyubovIterations (α : ℝ) : ℕ

Number of density-increment steps allowed at density α.

Equations

• TrilinearHT.Auto.bogolyubovIterations α = ⌈10 + Real.log (1 / α) / Real.log 2⌉₊

noncomputable def TrilinearHT.Auto.bogolyubovTolerance (α : ℝ) : ℝ

Accuracy used in each Bogolyubov sampling step.

Equations

• TrilinearHT.Auto.bogolyubovTolerance α = (1000 * Real.exp 1 * ↑(TrilinearHT.Auto.bogolyubovIterations α))⁻¹

noncomputable def TrilinearHT.Auto.bogolyubovSampleSize (α : ℝ) : ℕ

Sample size required by the Bogolyubov accuracy and exponent budgets.

Equations

• TrilinearHT.Auto.bogolyubovSampleSize α = ⌈64 * TrilinearHT.Auto.bogolyubovExponent α / TrilinearHT.Auto.bogolyubovTolerance α ^ 2⌉₊

theorem TrilinearHT.Auto.bogolyubovIterations_pos {α : ℝ} (hα : 0 < α) (hα1 : α ≤ 1) : 0 < bogolyubovIterations α

theorem TrilinearHT.Auto.bogolyubovTolerance_pos {α : ℝ} (hα : 0 < α) (hα1 : α ≤ 1) : 0 < bogolyubovTolerance α

theorem TrilinearHT.Auto.bogolyubov_parameter_error {α : ℝ} (hα : 0 < α) (hα1 : α ≤ 1) : (1 / α) ^ (1 / bogolyubovExponent α) * (2 * ↑(bogolyubovIterations α) * bogolyubovTolerance α) ≤ 1 / 100

The parameters give the advertised uniform error, with room in the constant.

theorem TrilinearHT.Auto.bogolyubov_witness_almost_periods {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (A : Finset G) (hA : A.Nonempty) : have α := ↑A.card / ↑(Fintype.card G); ∃ (X : Finset G), X.Nonempty ∧ α ^ bogolyubovSampleSize α / 2 ≤ ↑X.card / ↑(Fintype.card G) ∧ ∀ u ∈ bogolyubovIterations α • X - bogolyubovIterations α • X, ∀ (x : G), |bogolyubovBaseFunction A (x + u) - bogolyubovBaseFunction A x| ≤ 1 / 100

The positive witness has uniform almost periods on the required iterated difference set. This is the displayed estimate in blueprint lem:dense-Bohr, lines 801-805.

theorem TrilinearHT.Auto.bogolyubovSampleSize_le {α : ℝ} (hα : 0 < α) (hα1 : α ≤ 1) : ↑(bogolyubovSampleSize α) ≤ 65 * bogolyubovExponent α / bogolyubovTolerance α ^ 2

The chosen sampling length has the source's O(p epsilon^(-2)) bound.

noncomputable def TrilinearHT.Auto.bogolyubovSmooth {G : Type u_1} [AddCommGroup G] (X : Finset G) : ℕ → (G → ℂ) → G → ℂ

Repeated averaging against the probability law of a difference of two points of X.

Equations

• TrilinearHT.Auto.bogolyubovSmooth X 0 x✝¹ x✝ = x✝¹ x✝
• TrilinearHT.Auto.bogolyubovSmooth X k.succ x✝¹ x✝ = X.expect fun (a : G) => X.expect fun (b : G) => TrilinearHT.Auto.bogolyubovSmooth X k x✝¹ (x✝ + a - b)

theorem TrilinearHT.Auto.bogolyubovSmooth_sub_const {G : Type u_1} [AddCommGroup G] (X : Finset G) (hX : X.Nonempty) (k : ℕ) (f : G → ℂ) (c : ℂ) (x : G) : bogolyubovSmooth X k (fun (y : G) => f y - c) x = bogolyubovSmooth X k f x - c

theorem TrilinearHT.Auto.bogolyubovSmooth_norm_le {G : Type u_1} [AddCommGroup G] [DecidableEq G] (X : Finset G) (hX : X.Nonempty) (k : ℕ) (f : G → ℂ) (x : G) (C : ℝ) (h : ∀ u ∈ k • X - k • X, ‖f (x + u)‖ ≤ C) : ‖bogolyubovSmooth X k f x‖ ≤ C

The averaging law is supported on the actual iterated difference set.

theorem TrilinearHT.Auto.bogolyubovSmooth_error_le {G : Type u_1} [AddCommGroup G] [DecidableEq G] (X : Finset G) (hX : X.Nonempty) (k : ℕ) (f : G → ℂ) (δ : ℝ) (h : ∀ u ∈ k • X - k • X, ∀ (x : G), ‖f (x + u) - f x‖ ≤ δ) (x : G) : ‖bogolyubovSmooth X k f x - f x‖ ≤ δ

Smoothing changes an almost-invariant function by at most its uniform translation error.

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

Probability-normalized cyclic Fourier transform, with the negative-character convention.

Equations

• TrilinearHT.Auto.bogolyubovFourier f ξ = Finset.univ.expect fun (x : ZMod q) => f x * ZMod.stdAddChar (-(ξ * x))

theorem TrilinearHT.Auto.bogolyubovFourier_eq_dft {q : ℕ} [NeZero q] (f : ZMod q → ℂ) (ξ : ZMod q) : bogolyubovFourier f ξ = (↑q)⁻¹ * ZMod.dft f ξ

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

theorem TrilinearHT.Auto.bogolyubovFourier_expect {q : ℕ} [NeZero q] {I : Type u_1} (S : Finset I) (f : I → ZMod q → ℂ) (ξ : ZMod q) : bogolyubovFourier (fun (x : ZMod q) => S.expect fun (a : I) => f a x) ξ = S.expect fun (a : I) => bogolyubovFourier (f a) ξ

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

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

theorem TrilinearHT.Auto.bogolyubovFourier_average {q : ℕ} [NeZero q] (A : Finset (ZMod q)) (f : ZMod q → ℂ) (ξ : ZMod q) : bogolyubovFourier (bogolyubovAverage A f) ξ = (A.expect fun (a : ZMod q) => ZMod.stdAddChar (-(ξ * a))) * bogolyubovFourier f ξ

theorem TrilinearHT.Auto.bogolyubovFourier_smooth_step {q : ℕ} [NeZero q] (X : Finset (ZMod q)) (f : ZMod q → ℂ) (ξ : ZMod q) : bogolyubovFourier (fun (x : ZMod q) => X.expect fun (a : ZMod q) => X.expect fun (b : ZMod q) => f (x + a - b)) ξ = ↑(‖X.expect fun (a : ZMod q) => ZMod.stdAddChar (-(ξ * a))‖ ^ 2) * bogolyubovFourier f ξ

One smoothing step multiplies each Fourier coefficient by the squared character mean.

theorem TrilinearHT.Auto.bogolyubovFourier_smooth {q : ℕ} [NeZero q] (X : Finset (ZMod q)) (k : ℕ) (f : ZMod q → ℂ) (ξ : ZMod q) : bogolyubovFourier (bogolyubovSmooth X k f) ξ = ↑(‖X.expect fun (a : ZMod q) => ZMod.stdAddChar (-(ξ * a))‖ ^ (2 * k)) * bogolyubovFourier f ξ

The iterated averaging multiplier in blueprint lem:dense-Bohr, line 810.

theorem TrilinearHT.Auto.bogolyubovFourier_pairing {q : ℕ} [NeZero q] (f g : ZMod q → ℂ) : (Finset.univ.expect fun (x : ZMod q) => f x * (starRingEnd ℂ) (g x)) = ∑ ξ : ZMod q, bogolyubovFourier f ξ * (starRingEnd ℂ) (bogolyubovFourier g ξ)

theorem TrilinearHT.Auto.bogolyubovFourier_parseval {q : ℕ} [NeZero q] (f : ZMod q → ℂ) : (Finset.univ.expect fun (x : ZMod q) => ‖f x‖ ^ 2) = ∑ ξ : ZMod q, ‖bogolyubovFourier f ξ‖ ^ 2

@[reducible, inline]

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

The probability density of a finite subset, relative to normalized counting measure.

Equations

• TrilinearHT.Auto.bogolyubovDensity A x = TrilinearHT.Auto.finiteSetDensity A x

theorem TrilinearHT.Auto.bogolyubovFourier_density {q : ℕ} [NeZero q] (A : Finset (ZMod q)) (ξ : ZMod q) : bogolyubovFourier (bogolyubovDensity A) ξ = A.expect fun (a : ZMod q) => ZMod.stdAddChar (-(ξ * a))

theorem TrilinearHT.Auto.bogolyubov_character_mass {q : ℕ} [NeZero q] (A : Finset (ZMod q)) (hA : A.Nonempty) : ∑ ξ : ZMod q, ‖A.expect fun (a : ZMod q) => ZMod.stdAddChar (-(ξ * a))‖ ^ 2 = ↑q / ↑A.card

The squared Fourier mass of a probability density is exactly its reciprocal density.

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

theorem TrilinearHT.Auto.bogolyubov_witness_fourier_mass {q : ℕ} [NeZero q] (A : Finset (ZMod q)) (hA : A.Nonempty) : ∑ ξ : ZMod q, ‖bogolyubovFourier (fun (x : ZMod q) => ↑(bogolyubovBaseFunction A x)) ξ‖ ≤ ↑q / ↑A.card

The positive witness has Fourier l1 mass at most the reciprocal density of A.

theorem TrilinearHT.Auto.bogolyubov_circle_distance (x : UnitAddCircle) : ‖↑(AddCircle.toCircle x) - 1‖ ≤ 2 * Real.pi * ‖x‖

The circle exponential is Lipschitz for the quotient-circle distance.

theorem TrilinearHT.Auto.bogolyubov_stdChar_distance {q : ℕ} [NeZero q] (x : ZMod q) : ‖ZMod.stdAddChar x - 1‖ ≤ 2 * Real.pi * ‖ZMod.toAddCircle x‖

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

A Bohr set, using the quotient norm on the additive circle.

Equations

• TrilinearHT.Auto.bogolyubovBohrSet S ρ = {u : ZMod q | ∀ s ∈ S, ‖ZMod.toAddCircle (s * u)‖ < ρ}

theorem TrilinearHT.Auto.mem_bogolyubovBohrSet {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (ρ : ℝ) (u : ZMod q) : u ∈ bogolyubovBohrSet S ρ ↔ ∀ s ∈ S, ‖ZMod.toAddCircle (s * u)‖ < ρ

theorem TrilinearHT.Auto.bogolyubov_span_phase {q : ℕ} [NeZero q] (S : Finset (ZMod q)) {ρ : ℝ} (hρ : 0 ≤ ρ) {u ξ : ZMod q} (hu : u ∈ bogolyubovBohrSet S ρ) (hξ : ξ ∈ S.addSpan) : ‖ZMod.stdAddChar (ξ * u) - 1‖ ≤ 2 * Real.pi * ↑S.card * ρ

Every frequency in the signed span has controlled phase on the Bohr set.

theorem TrilinearHT.Auto.bogolyubov_spectrum_generators {q : ℕ} [NeZero q] (X : Finset (ZMod q)) (hX : X.Nonempty) : ∃ (S : Finset (ZMod q)), ↑S.card ≤ 16 * Real.log (↑q / ↑X.card) ∧ ∀ (ξ : ZMod q), 1 / 2 ≤ ‖X.expect fun (a : ZMod q) => ZMod.stdAddChar (-(ξ * a))‖ → ξ ∈ S.addSpan

Chang's theorem at threshold one half, in the exact cyclic character convention.

theorem TrilinearHT.Auto.bogolyubov_character_mean_norm_le {q : ℕ} [NeZero q] (X : Finset (ZMod q)) (hX : X.Nonempty) (ξ : ZMod q) : ‖X.expect fun (a : ZMod q) => ZMod.stdAddChar (-(ξ * a))‖ ≤ 1

theorem TrilinearHT.Auto.bogolyubov_spectrum_split {q : ℕ} [NeZero q] (X : Finset (ZMod q)) (hX : X.Nonempty) (S : Finset (ZMod q)) (hS : ∀ (ξ : ZMod q), 1 / 2 ≤ ‖X.expect fun (a : ZMod q) => ZMod.stdAddChar (-(ξ * a))‖ → ξ ∈ S.addSpan) (k : ℕ) (f : ZMod q → ℂ) {M ρ : ℝ} (hρ : 0 ≤ ρ) (hM : ∑ ξ : ZMod q, ‖bogolyubovFourier f ξ‖ ≤ M) {u : ZMod q} (hu : u ∈ bogolyubovBohrSet S ρ) : ‖bogolyubovSmooth X k f u - bogolyubovSmooth X k f 0‖ ≤ M * (2 * Real.pi * ↑S.card * ρ + 2 * (1 / 2) ^ (2 * k))

Splitting at spectral threshold one half gives the uniform Fourier translation estimate.

theorem TrilinearHT.Auto.bogolyubov_small_spectrum_error {α : ℝ} (hα : 0 < α) (hα1 : α ≤ 1) : 1 / α * (2 * (1 / 2) ^ (2 * bogolyubovIterations α)) ≤ 1 / 100

The logarithmic iteration count suppresses the small spectrum by the required constant.

noncomputable def TrilinearHT.Auto.bogolyubovRadius (α : ℝ) (d : ℕ) : ℝ

The source radius balances the large spectrum against reciprocal density.

Equations

• TrilinearHT.Auto.bogolyubovRadius α d = α / (1000 * (↑d + 1))

theorem TrilinearHT.Auto.bogolyubov_large_spectrum_error {α : ℝ} (hα : 0 < α) (d : ℕ) : 1 / α * (2 * Real.pi * ↑d * bogolyubovRadius α d) ≤ 1 / 100

theorem TrilinearHT.Auto.bogolyubov_smoothing_structure {q : ℕ} [NeZero q] (A : Finset (ZMod q)) (hA : A.Nonempty) : have α := ↑A.card / ↑q; have F := fun (x : ZMod q) => ↑(bogolyubovBaseFunction A x); ∃ (X : Finset (ZMod q)) (S : Finset (ZMod q)), X.Nonempty ∧ α ^ bogolyubovSampleSize α / 2 ≤ ↑X.card / ↑q ∧ ↑S.card ≤ 16 * Real.log (↑q / ↑X.card) ∧ (∀ (x : ZMod q), ‖bogolyubovSmooth X (bogolyubovIterations α) F x - F x‖ ≤ 1 / 100) ∧ ∀ u ∈ bogolyubovBohrSet S (bogolyubovRadius α S.card), ‖bogolyubovSmooth X (bogolyubovIterations α) F u - bogolyubovSmooth X (bogolyubovIterations α) F 0‖ ≤ 1 / 50

Sampling and Chang produce a smoothing that is close to the positive witness and nearly constant on a Bohr set. This completes the spectral estimate of lem:dense-Bohr.

noncomputable def TrilinearHT.Auto.bogolyubovLog (α : ℝ) : ℝ

The logarithmic parameter used in the quasipolynomial estimates.

Equations

• TrilinearHT.Auto.bogolyubovLog α = 1 + Real.log (1 / α)

theorem TrilinearHT.Auto.bogolyubovLog_one_le {α : ℝ} (hα : 0 < α) (hα1 : α ≤ 1) : 1 ≤ bogolyubovLog α

theorem TrilinearHT.Auto.bogolyubov_parameters_polynomial {α : ℝ} (hα : 0 < α) (hα1 : α ≤ 1) : bogolyubovExponent α ≤ 2 * bogolyubovLog α ∧ ↑(bogolyubovIterations α) ≤ 16 * bogolyubovLog α ∧ (bogolyubovTolerance α)⁻¹ ≤ 48000 * bogolyubovLog α ∧ ↑(bogolyubovSampleSize α) ≤ 10 ^ 12 * bogolyubovLog α ^ 3

Explicit polynomial logarithmic bounds for the source parameters.

theorem TrilinearHT.Auto.bogolyubov_log_density_bound {α β : ℝ} (hα : 0 < α) (hα1 : α ≤ 1) (_hβ : 0 < β) (hd : α ^ bogolyubovSampleSize α / 2 ≤ β) : Real.log (1 / β) ≤ 2 * 10 ^ 12 * bogolyubovLog α ^ 4

The sampling density costs at most four powers of the logarithmic parameter.

theorem TrilinearHT.Auto.bogolyubov_bohr_containment {q : ℕ} [NeZero q] (A : Finset (ZMod q)) (hA : A.Nonempty) : have α := ↑A.card / ↑q; ∃ (S : Finset (ZMod q)), ↑S.card ≤ 10 ^ 14 * bogolyubovLog α ^ 4 ∧ bogolyubovBohrSet S (bogolyubovRadius α S.card) ⊆ 2 • A - 2 • A

The quantitative Bohr containment obtained from the positive witness.

theorem TrilinearHT.Auto.bogolyubov_radius_bounds {α : ℝ} (hα : 0 < α) (hα1 : α ≤ 1) (d : ℕ) (hd : ↑d ≤ 10 ^ 14 * bogolyubovLog α ^ 4) : 0 < bogolyubovRadius α d ∧ bogolyubovRadius α d < 1 / 2 ∧ (bogolyubovRadius α d)⁻¹ ≤ 10 ^ 18 * α⁻¹ * bogolyubovLog α ^ 4

The source radius is positive, small, and has a polynomial logarithmic reciprocal.

theorem TrilinearHT.Auto.bogolyubov_radius_log_bound {α : ℝ} (hα : 0 < α) (hα1 : α ≤ 1) (d : ℕ) (hd : ↑d ≤ 10 ^ 14 * bogolyubovLog α ^ 4) : Real.log (3 / bogolyubovRadius α d) ≤ 4 * 10 ^ 18 * bogolyubovLog α

The logarithm of the inverse radius costs only one more logarithmic factor.