Section 1: Foundations, conventions, and proof interfaces

This file was automatically generated by Claude.

Formalization of blueprint Section 1, "Foundations, conventions, and proof interfaces" (sec:foundations, lines 53-253) of blueprint/formalization_blueprint.tex.

instance TrilinearHT.Auto.fact_zero_lt_sixteen : Fact (0 < 16)

The period 16 of the Gowers-norm circle is positive.

noncomputable def TrilinearHT.Auto.logarithmicSize (t : ℝ) : ℝ

The logarithmic size parameter in blueprint Lemma lem:budget-rules.

Equations

• TrilinearHT.Auto.logarithmicSize t = 1 + Real.log t

def TrilinearHT.Auto.QuasipolynomialBound (f : ℝ → ℝ) : Prop

Blueprint Lemma lem:budget-rules: an explicit quasipolynomial majorant. The coefficient and degree are chosen before the universally quantified parameter.

Equations

• TrilinearHT.Auto.QuasipolynomialBound f = ∃ (C : ℝ), 1 ≤ C ∧ ∃ (d : ℕ), 1 ≤ d ∧ ∀ (t : ℝ), 2 ≤ t → 0 ≤ f t ∧ f t ≤ Real.exp (C * TrilinearHT.Auto.logarithmicSize t ^ d)

theorem TrilinearHT.Auto.one_le_logarithmicSize {t : ℝ} (ht : 2 ≤ t) : 1 ≤ logarithmicSize t

theorem TrilinearHT.Auto.logarithmicSize_pow_mono {t : ℝ} (ht : 2 ≤ t) {d e : ℕ} (hde : d ≤ e) : logarithmicSize t ^ d ≤ logarithmicSize t ^ e

Increasing the degree of a logarithmic majorant on the source domain.

theorem TrilinearHT.Auto.quasipolynomialBound_mul {f g : ℝ → ℝ} (hf : QuasipolynomialBound f) (hg : QuasipolynomialBound g) : QuasipolynomialBound fun (t : ℝ) => f t * g t

Blueprint Lemma lem:budget-rules, closure under products.

theorem TrilinearHT.Auto.quasipolynomialBound_add {f g : ℝ → ℝ} (hf : QuasipolynomialBound f) (hg : QuasipolynomialBound g) : QuasipolynomialBound fun (t : ℝ) => f t + g t

Blueprint Lemma lem:budget-rules, closure under sums.

theorem TrilinearHT.Auto.quasipolynomialBound_const {c : ℝ} (hc : 0 ≤ c) : QuasipolynomialBound fun (x : ℝ) => c

A nonnegative constant has a quasipolynomial bound (including the empty-sum case).

theorem TrilinearHT.Auto.quasipolynomialBound_rpow {f : ℝ → ℝ} (hf : QuasipolynomialBound f) {p : ℝ} (hp : 0 ≤ p) : QuasipolynomialBound fun (t : ℝ) => f t ^ p

Blueprint Lemma lem:budget-rules, closure under nonnegative fixed real powers.

Separated-frequency rows

The quadratic-envelope integral calculations are adapted from ../lean-spherical/LeanSpherical/Auto/Spherical/MSS/Kakeya/TTStarSchur.lean, copyright 2026 Joris Roos, Apache 2.0.

noncomputable def TrilinearHT.Auto.fourierWave (ξ x : ℝ) : ℂ

The convention e(ξ x) = exp(2π i ξ x) used in the blueprint.

Equations

• TrilinearHT.Auto.fourierWave ξ x = ↑(Real.fourierChar (ξ * x))

theorem TrilinearHT.Auto.fourierWave_continuous (ξ : ℝ) : Continuous (fourierWave ξ)

theorem TrilinearHT.Auto.norm_fourierWave (ξ x : ℝ) : ‖fourierWave ξ x‖ = 1

theorem TrilinearHT.Auto.integral_abs_derivative_le_endpoints {a b : ℝ} {u u' : ℝ → ℝ} (hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hsign : (∀ x ∈ Set.uIcc a b, 0 ≤ u' x) ∨ ∀ x ∈ Set.uIcc a b, u' x ≤ 0) : ∫ (x : ℝ) in a..b, |u' x| ≤ |u a| + |u b|

A derivative with one sign has variation bounded by its endpoint sizes.

theorem TrilinearHT.Auto.hasDerivAt_fourierWave_comp {p : ℝ → ℝ} {q x : ℝ} (hp : HasDerivAt p q x) : HasDerivAt (fun (t : ℝ) => fourierWave 1 (p t)) (fourierWave 1 (p x) * (↑(2 * Real.pi * q) * Complex.I)) x

Differentiating the blueprint's oscillatory wave along a real phase.

theorem TrilinearHT.Auto.norm_integral_fourierWave_of_reciprocal {a b : ℝ} (hab : a ≤ b) (p q u u' : ℝ → ℝ) (hpcont : Continuous p) (hp : ∀ x ∈ Set.uIcc a b, HasDerivAt p (q x) x) (hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x) (hu'cont : ContinuousOn u' (Set.uIcc a b)) (hcancel : ∀ x ∈ Set.uIcc a b, u x * q x = 1) (hsign : (∀ x ∈ Set.uIcc a b, 0 ≤ u' x) ∨ ∀ x ∈ Set.uIcc a b, u' x ≤ 0) : ‖∫ (x : ℝ) in a..b, fourierWave 1 (p x)‖ ≤ 2 * (|u a| + |u b|)

One nonstationary integration by parts, with a real reciprocal amplitude. The sign condition controls its total variation by the endpoint values.

theorem TrilinearHT.Auto.quadratic_oscillatory_integral_bound (α β γ : ℝ) {a b A : ℝ} (hab : a ≤ b) (hA : 0 < A) (hlower : ∀ x ∈ Set.Icc a b, A ≤ |2 * α * x + β|) : ‖∫ (x : ℝ) in Set.Icc a b, fourierWave 1 (α * x ^ 2 + β * x + γ)‖ ≤ 4 / A

Blueprint Lemma lem:fourier-foundation, lines 143 and 158: a real quadratic phase whose derivative has modulus at least A has oscillatory integral at most 4/A. This includes linear phases and degenerate intervals.

theorem TrilinearHT.Auto.integral_finiteHaar_uniform {G : Type u_1} {E : Type u_2} [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f : G → E) : ∫ (x : G), f x ∂finiteHaar G = uniformMean f

theorem TrilinearHT.Auto.finite_cubeAverage_eq {G : Type u_1} [AddCommGroup G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] (j : ℕ) (f : (Fin j → Bool) → G → ℂ) : cubeAverage (finiteHaar G) j f = uniformMean fun (h : Fin j → G) => uniformMean (cubeIntegrand f h)

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

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

theorem TrilinearHT.Auto.finite_cubeAverage_conj {G : Type u_1} [AddCommGroup G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] (j : ℕ) (f : G → ℂ) : (cubeAverage (finiteHaar G) j fun (x : Fin j → Bool) (x_1 : G) => (starRingEnd ℂ) (f x_1)) = (starRingEnd ℂ) (cubeAverage (finiteHaar G) j fun (x : Fin j → Bool) => f)

noncomputable def TrilinearHT.Auto.realLineEquiv : EuclideanSpace ℝ (Fin 1) ≃ₗᵢ[ℝ] ℝ

The measure-preserving isometry identifying the one-coordinate Euclidean space with the blueprint's real variable.

Equations

• TrilinearHT.Auto.realLineEquiv = { toLinearEquiv := ↑(PiLp.equivOfUnique 2 ℝ fun (x : Fin 1) => ℝ), norm_map' := TrilinearHT.Auto.realLineEquiv._proof_1 }

theorem TrilinearHT.Auto.hlMaximal_realLine_comp {E : Type u_1} [NormedAddCommGroup E] (f : ℝ → E) (x : EuclideanSpace ℝ (Fin 1)) : ClassicalMaximal.hlMaximal MeasureTheory.volume (fun (y : EuclideanSpace ℝ (Fin 1)) => f (realLineEquiv y)) x = ClassicalMaximal.hlMaximal MeasureTheory.volume f (realLineEquiv x)

theorem TrilinearHT.Auto.mixedENorm_realLine_comp {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.Measure Ω) (p s : ℝ) (u : ℝ × Ω → ENNReal) : (ClassicalMaximal.mixedENorm MeasureTheory.volume ν p s fun (z : EuclideanSpace ℝ (Fin 1) × Ω) => u (realLineEquiv z.1, z.2)) = ClassicalMaximal.mixedENorm MeasureTheory.volume ν p s u

noncomputable def TrilinearHT.Auto.realMixedMaximal {Ω : Type u_1} {E : Type u_2} [NormedAddCommGroup E] (f : ℝ × Ω → E) (z : ℝ × Ω) : ENNReal

Hardy–Littlewood maximal function in the real coordinate of a mixed-space input.

Equations

• TrilinearHT.Auto.realMixedMaximal f z = TrilinearHT.Auto.ClassicalMaximal.hlMaximal MeasureTheory.volume (fun (y : ℝ) => f (y, z.2)) z.1

theorem TrilinearHT.Auto.feffermanStein_real {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (ν : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure ν] {p s : ℝ} (hp : 1 < p) (hs : 1 < s) {f : ℝ × Ω → E} (hf : Measurable f) : ClassicalMaximal.mixedENorm MeasureTheory.volume ν p s (realMixedMaximal f) ≤ ClassicalMaximal.fsMixedConst 1 p s * ClassicalMaximal.mixedENorm MeasureTheory.volume ν p s fun (z : ℝ × Ω) => ‖f z‖ₑ

noncomputable def TrilinearHT.Auto.centeredMaximalQ {Ω : Type u_1} (q : ℝ) (f : ℝ × Ω → ℂ) (z : ℝ × Ω) : ENNReal

The centered powered maximal function, used to prove the uncentered source estimate.

Equations

• TrilinearHT.Auto.centeredMaximalQ q f z = TrilinearHT.Auto.realMixedMaximal (fun (z : ℝ × Ω) => ‖f z‖ ^ q) z ^ (1 / q)

theorem TrilinearHT.Auto.centeredMaximalQ_mixedNorm {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure ν] {p q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) (hpq : q < p) (f : ℝ × Ω → ℂ) (hf : Measurable f) : ClassicalMaximal.mixedENorm MeasureTheory.volume ν p 4 (centeredMaximalQ q f) ≤ ClassicalMaximal.fsMixedConst 1 (p / q) (4 / q) ^ (1 / q) * ClassicalMaximal.mixedENorm MeasureTheory.volume ν p 4 fun (z : ℝ × Ω) => ‖f z‖ₑ

theorem TrilinearHT.Auto.centeredOneMixedNorm (p q : ℝ) (hq2 : 2 < q) (hq3 : q < 3) (hpq : q < p) : ∃ (C : NNReal), ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (ν : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure ν] (f : ℝ × Ω → ℂ), Measurable f → ClassicalMaximal.mixedENorm MeasureTheory.volume ν p 4 (centeredMaximalQ q f) ≤ ↑C * ClassicalMaximal.mixedENorm MeasureTheory.volume ν p 4 fun (z : ℝ × Ω) => ‖f z‖ₑ

Centered prerequisite for blueprint lem:vector-maximal: for 2 < q < 3 and p > q, M_q is bounded on L^p(ℝ; L^4(Ω)), uniformly over finite inner measure spaces.

noncomputable def TrilinearHT.Auto.uncenteredRealMaximal {E : Type u_1} [NormedAddCommGroup E] (f : ℝ → E) (x : ℝ) : ENNReal

The uncentered Hardy–Littlewood maximal operator specified at blueprint line 67, using nondegenerate intervals containing the evaluation point.

Equations

• TrilinearHT.Auto.uncenteredRealMaximal f x = ⨆ (a : ℝ), ⨆ (b : ℝ), ⨆ (_ : a < b), ⨆ (_ : x ∈ Set.Icc a b), (ENNReal.ofReal (b - a))⁻¹ * ∫⁻ (y : ℝ) in Set.Icc a b, ‖f y‖ₑ

theorem TrilinearHT.Auto.real_intervalAverage_le_two_centered {E : Type u_1} [NormedAddCommGroup E] (f : ℝ → E) {a b x : ℝ} (hab : a < b) (hx : x ∈ Set.Icc a b) : (ENNReal.ofReal (b - a))⁻¹ * ∫⁻ (y : ℝ) in Set.Icc a b, ‖f y‖ₑ ≤ 2 * ClassicalMaximal.hlMaximal MeasureTheory.volume f x

theorem TrilinearHT.Auto.uncenteredRealMaximal_le_two_centered {E : Type u_1} [NormedAddCommGroup E] (f : ℝ → E) (x : ℝ) : uncenteredRealMaximal f x ≤ 2 * ClassicalMaximal.hlMaximal MeasureTheory.volume f x

The uncentered maximal operator is at most twice the centered one.

theorem TrilinearHT.Auto.mixedENorm_const_mul {X : Type u_1} {Ω : Type u_2} [MeasurableSpace X] [MeasurableSpace Ω] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Ω) {p s : ℝ} (hp : 0 < p) (hs : 0 < s) (c : ENNReal) (hc : c ≠ ⊤) (f : X × Ω → ENNReal) : (ClassicalMaximal.mixedENorm μ ν p s fun (z : X × Ω) => c * f z) = c * ClassicalMaximal.mixedENorm μ ν p s f

noncomputable def TrilinearHT.Auto.maximalQ {Ω : Type u_1} (q : ℝ) (f : ℝ × Ω → ℂ) (z : ℝ × Ω) : ENNReal

The blueprint's powered uncentered maximal function, with the convention specified at source line 67 and used in lem:vector-maximal and eq:CN.

Equations

• TrilinearHT.Auto.maximalQ q f z = TrilinearHT.Auto.uncenteredRealMaximal (fun (y : ℝ) => ‖f (y, z.2)‖ ^ q) z.1 ^ (1 / q)

theorem TrilinearHT.Auto.maximalQ_le_centered {Ω : Type u_1} {q : ℝ} (hq : 0 < q) (f : ℝ × Ω → ℂ) (z : ℝ × Ω) : maximalQ q f z ≤ 2 ^ (1 / q) * centeredMaximalQ q f z

theorem TrilinearHT.Auto.oneMixedNorm (p q : ℝ) (hq2 : 2 < q) (hq3 : q < 3) (hpq : q < p) : ∃ (C : NNReal), ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (ν : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure ν] (f : ℝ × Ω → ℂ), Measurable f → ClassicalMaximal.mixedENorm MeasureTheory.volume ν p 4 (maximalQ q f) ≤ ↑C * ClassicalMaximal.mixedENorm MeasureTheory.volume ν p 4 fun (z : ℝ × Ω) => ‖f z‖ₑ

Blueprint lem:vector-maximal, lines 240–251: the source's uncentered M_q is bounded on L^p(ℝ; L^4(Ω)), uniformly over all finite inner measure spaces.