Section 16.3: Summing the update levels

This file was automatically generated by Claude.

Formalization of blueprint Section 16, "Normalized absorption and the operator estimate" (sec:completion), subsection 3, "Summing the update levels" (lines 2893-3012) of blueprint/formalization_blueprint.tex.

The operator is the human-written TrilinearHT.T (with truncations TrilinearHT.truncatedTransform) of TrilinearHT/Defs.lean, T(f)(x) = p.v. ∫ Π_i f_i(x + (i+1)t) dt/t. The substitution t ↦ -t turns it into minus the blueprint's p.v. ∫ f₁(x - t) f₂(x - 2t) f₃(x - 3t) dt/t (truncatedTransform_eq_neg, T_eq_neg_integral); the sign is irrelevant for every norm bound.

theorem TrilinearHT.Auto.level_term_le {c θ : ℝ} (hc : 0 < c) (hθ : 0 < θ) {k₁ A : ℕ} (hk : 1 ≤ k₁) (hA : 2 ≤ A) (hx : 2 ≤ ↑k₁ ^ θ) (t : ℕ) : Real.exp (-c * ↑(stagAcc k₁ A t) ^ θ) ≤ Real.exp (-c * ↑k₁ ^ θ / 2) ^ (t + 1)

Blueprint lines 2893-2897: for k_t = k₁^{A^{t-1}} (A ≥ 2), c, θ > 0 and x = k₁^θ ≥ 2, each level weight satisfies (t+1) e^{-c k_t^θ} ≤ (t+1) r^{t+1} with r = e^{-cx/2}.

theorem TrilinearHT.Auto.update_levels_sum {c θ : ℝ} (hc : 0 < c) (hθ : 0 < θ) {A : ℕ} (hA : 2 ≤ A) {ε : ℝ} (hε : 0 < ε) : ∃ (K : ℕ), ∀ (k₁ : ℕ), K ≤ k₁ → (Summable fun (t : ℕ) => (↑t + 1) * Real.exp (-c * ↑(stagAcc k₁ A t) ^ θ)) ∧ ∑' (t : ℕ), (↑t + 1) * Real.exp (-c * ↑(stagAcc k₁ A t) ^ θ) ≤ ε

Blueprint lines 2893-2899 (summing the update levels): for A ≥ 2 and c, θ > 0, the level series Σ_t (t+1) e^{-c k_t^θ} with k_t = k₁^{A^{t-1}} converges, and it is smaller than any prescribed ε > 0 once k₁ is large.

theorem TrilinearHT.Auto.levels_cutoff_sum {X A₀ : ℝ} (E : ℕ → ℝ) (hE : Filter.Tendsto E Filter.atTop (nhds 0)) (Y : ℕ → ℕ → ℝ) (hY0 : ∀ (u t : ℕ), 0 ≤ Y u t) (hX : ∀ (T : ℕ), X ≤ E T + ∑ u ∈ Finset.Icc 1 T, ∑ t ∈ Finset.Ioc u T, Y u t) (hinit : ∀ (u t : ℕ), t < 12 → Y u t ≤ A₀) (b : ℕ → ℝ) (hb0 : ∀ (t : ℕ), 0 ≤ b t) (hb : ∀ (u t : ℕ), 12 ≤ t → u < t → Y u t ≤ b t) (hbs : Summable fun (t : ℕ) => ↑t * b t) : X ≤ 55 * A₀ + ∑' (t : ℕ), ↑t * b t

Blueprint lines 2893-2904 (summing the update levels and the cutoff limit): if for every accuracy cutoff T the quantity X is at most a remainder E_T → 0 plus the sum over update pairs 1 ≤ u < t ≤ T of nonnegative contributions Y_{u,t}, the initial levels t < 12 contribute at most A₀ each and the later levels at most b_t per pair with Σ_t t b_t convergent, then X ≤ 55 A₀ + Σ_t t b_t.

The uniform local estimate (thm:uniform-local, blueprint lines 2906-2932)

theorem TrilinearHT.Auto.uniform_constant_absorption {CN C A c : ℝ} (h : CN ≤ 1 + C * A + C * c * CN) (hc : C * c ≤ 1 / 2) (hCN : 0 ≤ CN) : CN ≤ 2 + 2 * C * A

Blueprint lines 2927-2931 (absorption): from C_N ≤ 1 + C A + C c C_N with C c ≤ 1/2, C_N ≤ 2 + 2 C A.

The main theorem: kernel reconstruction and lattices (blueprint lines 2935-3010)

theorem TrilinearHT.Auto.three_term_telescope {R : Type u_1} [CommRing R] (a₁ a₂ a₃ b₁ b₂ b₃ : R) : a₁ * a₂ * a₃ - b₁ * b₂ * b₃ = (a₁ - b₁) * a₂ * a₃ + b₁ * (a₂ - b₂) * a₃ + b₁ * b₂ * (a₃ - b₃)

Blueprint line 2985: the three-term telescoping product identity.

Pointwise principal value on Schwartz inputs (blueprint lines 2984-2992)

theorem TrilinearHT.Auto.truncatedTransform_eq_neg (f : Fin 3 → ℝ → ℂ) (x ε : ℝ) : truncatedTransform f x ε = -∫ (t : ℝ) in {t : ℝ | ε < |t|}, f 0 (x - t) * f 1 (x - 2 * t) * f 2 (x - 3 * t) / ↑t

The truncation TrilinearHT.truncatedTransform in the blueprint's reflected form -∫_{|t| > ε} f₀(x - t) f₁(x - 2t) f₂(x - 3t) dt/t (substitution t ↦ -t).

theorem TrilinearHT.Auto.progression_product_integrable (f₁ f₂ f₃ : SchwartzMap ℝ ℂ) (x : ℝ) : MeasureTheory.Integrable (fun (t : ℝ) => f₁ (x - t) * f₂ (x - 2 * t) * f₃ (x - 3 * t)) MeasureTheory.volume

The product g(t) = f₁(x - t) f₂(x - 2t) f₃(x - 3t) of three Schwartz functions along the progression is integrable in t.

theorem TrilinearHT.Auto.progression_product_odd_part_le (f₁ f₂ f₃ : SchwartzMap ℝ ℂ) (x : ℝ) : ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, ‖f₁ (x - t) * f₂ (x - 2 * t) * f₃ (x - 3 * t) - f₁ (x - -t) * f₂ (x - 2 * -t) * f₃ (x - 3 * -t)‖ ≤ C * t

Blueprint lines 2984-2989: the symmetric difference g(t) - g(-t) of the progression product is at most C |t| for |t| ≤ 1 (mean value theorem).

theorem TrilinearHT.Auto.progression_truncated_tendsto (f₁ f₂ f₃ : SchwartzMap ℝ ℂ) (x : ℝ) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in {t : ℝ | ε < |t|}, f₁ (x - t) * f₂ (x - 2 * t) * f₃ (x - 3 * t) / ↑t) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (t : ℝ) in Set.Ioi 0, (f₁ (x - t) * f₂ (x - 2 * t) * f₃ (x - 3 * t) - f₁ (x - -t) * f₂ (x - 2 * -t) * f₃ (x - 3 * -t)) / ↑t))

Blueprint thm:main, lines 2989-2992: for Schwartz inputs the symmetric principal value p.v. ∫ f₁(x - t) f₂(x - 2t) f₃(x - 3t) dt/t exists at every real x and equals the absolutely convergent one-sided integral of the odd part ∫_{t > 0} (g(t) - g(-t))/t dt.

theorem TrilinearHT.Auto.truncatedTransform_tendsto_neg_integral (f₁ f₂ f₃ : SchwartzMap ℝ ℂ) (x : ℝ) : Filter.Tendsto (truncatedTransform ![⇑f₁, ⇑f₂, ⇑f₃] x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (-∫ (t : ℝ) in Set.Ioi 0, (f₁ (x - t) * f₂ (x - 2 * t) * f₃ (x - 3 * t) - f₁ (x - -t) * f₂ (x - 2 * -t) * f₃ (x - 3 * -t)) / ↑t))

Blueprint thm:main, lines 2989-2992, for TrilinearHT.truncatedTransform: on Schwartz inputs the truncations converge to minus the odd-part integral of the blueprint's progression product.

theorem TrilinearHT.Auto.T_eq_neg_integral (f₁ f₂ f₃ : SchwartzMap ℝ ℂ) (x : ℝ) : T ![⇑f₁, ⇑f₂, ⇑f₃] x = -∫ (t : ℝ) in Set.Ioi 0, (f₁ (x - t) * f₂ (x - 2 * t) * f₃ (x - 3 * t) - f₁ (x - -t) * f₂ (x - 2 * -t) * f₃ (x - 3 * -t)) / ↑t

On Schwartz inputs TrilinearHT.T is minus the absolutely convergent odd-part integral ∫_{t > 0} (g(t) - g(-t))/t dt of g(t) = f₁(x - t) f₂(x - 2t) f₃(x - 3t).

theorem TrilinearHT.Auto.tendsto_truncatedTransform_three (f₁ f₂ f₃ : SchwartzMap ℝ ℂ) (x : ℝ) : Filter.Tendsto (truncatedTransform ![⇑f₁, ⇑f₂, ⇑f₃] x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (T ![⇑f₁, ⇑f₂, ⇑f₃] x))

Blueprint thm:main, lines 2989-2992: for Schwartz f₁, f₂, f₃ the truncations TrilinearHT.truncatedTransform converge to TrilinearHT.T at every real x.

theorem TrilinearHT.Auto.schwartz_triple_eq_vecCons (f : Fin 3 → SchwartzMap ℝ ℂ) : (fun (i : Fin 3) => ⇑(f i)) = ![⇑(f 0), ⇑(f 1), ⇑(f 2)]

A triple of Schwartz functions, coerced to functions, as a vector literal.

theorem TrilinearHT.Auto.tendsto_truncatedTransform (f : Fin 3 → SchwartzMap ℝ ℂ) (x : ℝ) : Filter.Tendsto (truncatedTransform (fun (i : Fin 3) => ⇑(f i)) x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (T (fun (i : Fin 3) => ⇑(f i)) x))

Blueprint thm:main, lines 2989-2992: for Schwartz functions f the principal value limit defining TrilinearHT.T exists at every real x: truncatedTransform f x ε → T f x as ε → 0⁺.

Unique bounded extension (blueprint lines 2999-3009)

theorem TrilinearHT.Auto.bilinear_dense_extension {𝕜 : Type u_1} {E : Type u_2} {V : Type u_3} {W : Type u_4} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] [CompleteSpace W] (e : E →ₗ[𝕜] V) (hd : DenseRange ⇑e) (B : E →ₗ[𝕜] E →ₗ[𝕜] W) {C : ℝ} (hC : 0 ≤ C) (hB : ∀ (a b : E), ‖(B a) b‖ ≤ C * ‖e a‖ * ‖e b‖) : ∃ (B' : V →L[𝕜] V →L[𝕜] W), (∀ (a b : E), (B' (e a)) (e b) = (B a) b) ∧ ∀ (x : V), ‖B' x‖ ≤ C * ‖x‖

Bilinear step of the extension in blueprint lines 2999-3009: a bilinear map bounded by C ‖e a‖ ‖e b‖ along a dense linear map e extends to a bounded bilinear map with ‖B' x‖ ≤ C ‖x‖.

theorem TrilinearHT.Auto.trilinear_dense_extension {𝕜 : Type u_1} {E : Type u_2} {V : Type u_3} {W : Type u_4} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] [CompleteSpace W] (e : E →ₗ[𝕜] V) (hd : DenseRange ⇑e) (T : E →ₗ[𝕜] E →ₗ[𝕜] E →ₗ[𝕜] W) {C : ℝ} (hC : 0 ≤ C) (hT : ∀ (a b c : E), ‖((T a) b) c‖ ≤ C * ‖e a‖ * ‖e b‖ * ‖e c‖) : ∃ (T' : V →L[𝕜] V →L[𝕜] V →L[𝕜] W), (∀ (a b c : E), ((T' (e a)) (e b)) (e c) = ((T a) b) c) ∧ (∀ (x y z : V), ‖((T' x) y) z‖ ≤ C * ‖x‖ * ‖y‖ * ‖z‖) ∧ ∀ (S : V →L[𝕜] V →L[𝕜] V →L[𝕜] W), (∀ (a b c : E), ((S (e a)) (e b)) (e c) = ((T a) b) c) → S = T'

Blueprint thm:main, lines 2999-3009: a trilinear map on a space E with a dense linear map e : E → V (Schwartz functions in L³), bounded by C ‖e a‖ ‖e b‖ ‖e c‖ with values in a complete space (L¹), has a unique bounded trilinear extension to V, with the same bound.

instance TrilinearHT.Auto.fact_one_le_three_ennreal : Fact (1 ≤ 3)

L³ is a normed space: 1 ≤ 3.

theorem TrilinearHT.Auto.schwartz_L3_unique_extension (T : SchwartzMap ℝ ℂ →ₗ[ℂ] SchwartzMap ℝ ℂ →ₗ[ℂ] SchwartzMap ℝ ℂ →ₗ[ℂ] ↥(MeasureTheory.Lp ℂ 1 MeasureTheory.volume)) {C : ℝ} (hC : 0 ≤ C) (hT : ∀ (f₁ f₂ f₃ : SchwartzMap ℝ ℂ), ‖((T f₁) f₂) f₃‖ ≤ C * ‖f₁.toLp 3 MeasureTheory.volume‖ * ‖f₂.toLp 3 MeasureTheory.volume‖ * ‖f₃.toLp 3 MeasureTheory.volume‖) : ∃ (T' : ↥(MeasureTheory.Lp ℂ 3 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 3 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 3 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 1 MeasureTheory.volume)), (∀ (f₁ f₂ f₃ : SchwartzMap ℝ ℂ), ((T' (f₁.toLp 3 MeasureTheory.volume)) (f₂.toLp 3 MeasureTheory.volume)) (f₃.toLp 3 MeasureTheory.volume) = ((T f₁) f₂) f₃) ∧ (∀ (x y z : ↥(MeasureTheory.Lp ℂ 3 MeasureTheory.volume)), ‖((T' x) y) z‖ ≤ C * ‖x‖ * ‖y‖ * ‖z‖) ∧ ∀ (S : ↥(MeasureTheory.Lp ℂ 3 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 3 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 3 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 1 MeasureTheory.volume)), (∀ (f₁ f₂ f₃ : SchwartzMap ℝ ℂ), ((S (f₁.toLp 3 MeasureTheory.volume)) (f₂.toLp 3 MeasureTheory.volume)) (f₃.toLp 3 MeasureTheory.volume) = ((T f₁) f₂) f₃) → S = T'

Blueprint thm:main, lines 2999-3009, specialized: a trilinear operator on Schwartz triples with values in L¹(ℝ) and the bound ‖T(f₁, f₂, f₃)‖₁ ≤ C Π ‖f_j‖₃ has a unique bounded trilinear extension to L³(ℝ)³ (Schwartz functions are dense in L³, SchwartzMap.denseRange_toLpCLM).

The uniform local estimate from normalized absorption (thm:uniform-local)

def TrilinearHT.Auto.dyadicHullCells (G : RealDyadicGrid) (cells : Finset (ℤ × ℤ)) (root : ℤ × ℤ) : Set (ℤ × ℤ)

The cells of the rooted subtree spanned by a finite cell collection under a root: dyadic cells inside the root that contain some used cell (blueprint prop:normalized, line 2831).

Equations

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

noncomputable def TrilinearHT.Auto.cellLqNorm (G : RealDyadicGrid) (q : ℝ) (f : ℝ → ℂ) (K : ℤ × ℤ) : ENNReal

The normalized local L^q norm ‖f‖_{q,I} on the dyadic cell (s, m).

Equations

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

def TrilinearHT.Auto.NormalizedAbsorption (κ : LocalKernelClass) (q : ℝ) (N : ℕ) (A c : ℝ) : Prop

Blueprint prop:normalized, eq:normalized (lines 2827-2833), for fixed constants A, c: on every finite rooted dyadic subtree with root I_* whose used cells lie in at most N consecutive depths and with ‖f_j‖_{q,I} ≤ 1 on all its cells, Σ_{I used} |I| |H_I(f)| ≤ (A + c C_N) |I_*|.

Equations

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

theorem TrilinearHT.Auto.exists_firstStop_above {α : Type u_1} {C : Finset α} {cell : α → Set ℝ} {bad : α → α → Prop} [(J K : α) → Decidable (bad J K)] {J K : α} (hK : K ∈ C) (hKJ : cell K ⊂ cell J) (hb : bad J K) : ∃ L ∈ firstStops C cell bad J, cell K ⊆ cell L

Every violating cell lies in a first stop (finite maximality).

theorem TrilinearHT.Auto.stopGen_parent {α : Type u_1} [DecidableEq α] {C : Finset α} {cell : α → Set ℝ} {bad : α → α → Prop} [(J K : α) → Decidable (bad J K)] {roots : Finset α} {k : ℕ} {K : α} (hK : K ∈ stopGen C cell bad roots (k + 1)) : ∃ P ∈ stopGen C cell bad roots k, K ∈ firstStops C cell bad P

theorem TrilinearHT.Auto.stopGen_disjoint {α : Type u_1} [DecidableEq α] {C : Finset α} {cell : α → Set ℝ} {bad : α → α → Prop} [(J K : α) → Decidable (bad J K)] {roots : Finset α} (hr : roots ⊆ C) (hlam : ∀ K ∈ C, ∀ L ∈ C, cell K ⊆ cell L ∨ cell L ⊆ cell K ∨ Disjoint (cell K) (cell L)) (hinj : ∀ K ∈ C, ∀ L ∈ C, cell K = cell L → K = L) (hroots : ∀ R ∈ roots, ∀ R' ∈ roots, R ≠ R' → Disjoint (cell R) (cell R')) (k : ℕ) (J : α) : J ∈ stopGen C cell bad roots k → ∀ J' ∈ stopGen C cell bad roots k, J ≠ J' → Disjoint (cell J) (cell J')

Each stopping generation consists of pairwise disjoint cells.

theorem TrilinearHT.Auto.stopGen_ancestor {α : Type u_1} [DecidableEq α] {C : Finset α} {cell : α → Set ℝ} {bad : α → α → Prop} [(J K : α) → Decidable (bad J K)] {roots : Finset α} (k d : ℕ) (K : α) : K ∈ stopGen C cell bad roots (k + d) → ∃ A ∈ stopGen C cell bad roots k, cell K ⊆ cell A

Ancestors in earlier generations.

theorem TrilinearHT.Auto.stopGen_ancestor_stop {α : Type u_1} [DecidableEq α] {C : Finset α} {cell : α → Set ℝ} {bad : α → α → Prop} [(J K : α) → Decidable (bad J K)] {roots : Finset α} (k d : ℕ) {K : α} (hK : K ∈ stopGen C cell bad roots (k + 1 + d)) : ∃ A ∈ stopGen C cell bad roots k, ∃ B ∈ firstStops C cell bad A, cell K ⊆ cell B

A later-generation cell lies in a first stop of its ancestor.

theorem TrilinearHT.Auto.stop_inside_firstStop {α : Type u_1} [DecidableEq α] {C : Finset α} {cell : α → Set ℝ} {bad : α → α → Prop} [(J K : α) → Decidable (bad J K)] {roots : Finset α} (hr : roots ⊆ C) (hlam : ∀ K ∈ C, ∀ L ∈ C, cell K ⊆ cell L ∨ cell L ⊆ cell K ∨ Disjoint (cell K) (cell L)) (hinj : ∀ K ∈ C, ∀ L ∈ C, cell K = cell L → K = L) (hroots : ∀ R ∈ roots, ∀ R' ∈ roots, R ≠ R' → Disjoint (cell R) (cell R')) (hne : ∀ (K : α), (cell K).Nonempty) {k k' : ℕ} {J J' : α} (hJ : J ∈ stopGen C cell bad roots k) (hJ' : J' ∈ stopGen C cell bad roots k') (hss : cell J' ⊂ cell J) : ∃ B ∈ firstStops C cell bad J, cell J' ⊆ cell B

Blueprint lines 2919-2921: every stopping cell strictly inside a stopping cell J lies inside a first stop of J.

noncomputable def TrilinearHT.Auto.stopCells {α : Type u_1} [DecidableEq α] (C : Finset α) (cell : α → Set ℝ) (bad : α → α → Prop) [(J K : α) → Decidable (bad J K)] (roots : Finset α) : Finset α

The stopping cells: members of some generation.

Equations

• TrilinearHT.Auto.stopCells C cell bad roots = {J ∈ C | ∃ (k : ℕ), J ∈ TrilinearHT.Auto.stopGen C cell bad roots k}

def TrilinearHT.Auto.stopRemainder {α : Type u_1} (C : Finset α) (cell : α → Set ℝ) (bad : α → α → Prop) [(J K : α) → Decidable (bad J K)] (J : α) : Set ℝ

The sparse remainder E_J = J ∖ ⋃ first stops.

Equations

• TrilinearHT.Auto.stopRemainder C cell bad J = cell J \ ⋃ B ∈ TrilinearHT.Auto.firstStops C cell bad J, cell B

theorem TrilinearHT.Auto.stopRemainder_disjoint {α : Type u_1} [DecidableEq α] {C : Finset α} {cell : α → Set ℝ} {bad : α → α → Prop} [(J K : α) → Decidable (bad J K)] {roots : Finset α} (hr : roots ⊆ C) (hlam : ∀ K ∈ C, ∀ L ∈ C, cell K ⊆ cell L ∨ cell L ⊆ cell K ∨ Disjoint (cell K) (cell L)) (hinj : ∀ K ∈ C, ∀ L ∈ C, cell K = cell L → K = L) (hroots : ∀ R ∈ roots, ∀ R' ∈ roots, R ≠ R' → Disjoint (cell R) (cell R')) (hne : ∀ (K : α), (cell K).Nonempty) : (↑(stopCells C cell bad roots)).PairwiseDisjoint (stopRemainder C cell bad)

Blueprint lines 2919-2921: the remainders of distinct stopping cells are disjoint.

theorem TrilinearHT.Auto.stop_sparse_bound {α : Type u_1} [DecidableEq α] {C : Finset α} {cell : α → Set ℝ} {bad : α → α → Prop} [(J K : α) → Decidable (bad J K)] {roots : Finset α} (hr : roots ⊆ C) (hlam : ∀ K ∈ C, ∀ L ∈ C, cell K ⊆ cell L ∨ cell L ⊆ cell K ∨ Disjoint (cell K) (cell L)) (hinj : ∀ K ∈ C, ∀ L ∈ C, cell K = cell L → K = L) (hroots : ∀ R ∈ roots, ∀ R' ∈ roots, R ≠ R' → Disjoint (cell R) (cell R')) (hne : ∀ (K : α), (cell K).Nonempty) (hmeas : ∀ (K : α), MeasurableSet (cell K)) (hfin : ∀ (K : α), MeasureTheory.volume (cell K) ≠ ⊤) (hquarter : ∀ J ∈ stopCells C cell bad roots, 4 * MeasureTheory.volume (⋃ B ∈ firstStops C cell bad J, cell B) ≤ MeasureTheory.volume (cell J)) (F : ℝ → ENNReal) (v : α → ENNReal) (hv : ∀ J ∈ stopCells C cell bad roots, ∀ x ∈ cell J, v J ≤ F x) : ∑ J ∈ stopCells C cell bad roots, MeasureTheory.volume (cell J) * v J ≤ 4 / 3 * ∫⁻ (x : ℝ), F x

Blueprint lines 2919-2924 (sparse bound): if the first stops of every stopping cell cover at most a quarter of it, and v_J ≤ F on J, then Σ_J |J| v_J ≤ (4/3) ∫ F.

theorem TrilinearHT.Auto.stops_measure_le {ι : Type u_1} (J : Set ℝ) (s : Finset ι) (B : ι → Set ℝ) (hBJ : ∀ i ∈ s, B i ⊆ J) (hdisj : (↑s).PairwiseDisjoint B) (hmeas : ∀ i ∈ s, MeasurableSet (B i)) (g : ℝ → ENNReal) (hJ0 : MeasureTheory.volume J ≠ 0) (hJfin : MeasureTheory.volume J ≠ ⊤) (hint : ∫⁻ (x : ℝ) in J, g x ≠ ⊤) (hBfin : ∀ i ∈ s, MeasureTheory.volume (B i) ≠ ⊤) (hbad : ∀ i ∈ s, 16 * ((MeasureTheory.volume J)⁻¹ * ∫⁻ (x : ℝ) in J, g x) < (MeasureTheory.volume (B i))⁻¹ * ∫⁻ (x : ℝ) in B i, g x) : 16 * ∑ i ∈ s, MeasureTheory.volume (B i) ≤ MeasureTheory.volume J

Blueprint lines 2911-2915: disjoint subcells B ⊆ J on which the average of g = |f|^q exceeds 16 times its average on J have total length at most |J|/16: 16 a_J^q Σ |B| < Σ ∫_B |f|^q ≤ a_J^q |J|.

noncomputable def TrilinearHT.Auto.dyadicAncestorIndex (G : RealDyadicGrid) (I : ℤ × ℤ) (s : ℤ) : ℤ

The index of the depth-s ancestor of the cell I (junk when s > I.1).

Equations

• TrilinearHT.Auto.dyadicAncestorIndex G I s = if h : s ≤ I.1 then Classical.choose ⋯ else I.2

theorem TrilinearHT.Auto.dyadicAncestorIndex_spec (G : RealDyadicGrid) (I : ℤ × ℤ) {s : ℤ} (h : s ≤ I.1) : dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G s (dyadicAncestorIndex G I s)

theorem TrilinearHT.Auto.dyadicAncestorIndex_eq (G : RealDyadicGrid) {K I : ℤ × ℤ} (h : dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G K.1 K.2) : K.2 = dyadicAncestorIndex G I K.1

A cell containing I at depth s is the ancestor of I at depth s.

noncomputable def TrilinearHT.Auto.dyadicHullFamily (G : RealDyadicGrid) (cells : Finset (ℤ × ℤ)) (s₀ : ℤ) : Finset (ℤ × ℤ)

The candidate cells: dyadic cells of depth at least s₀ containing a used cell.

Equations

• TrilinearHT.Auto.dyadicHullFamily G cells s₀ = cells.biUnion fun (I : ℤ × ℤ) => Finset.image (fun (s : ℤ) => (s, TrilinearHT.Auto.dyadicAncestorIndex G I s)) (Finset.Icc s₀ I.1)

theorem TrilinearHT.Auto.mem_dyadicHullFamily (G : RealDyadicGrid) (cells : Finset (ℤ × ℤ)) (s₀ : ℤ) (K : ℤ × ℤ) : K ∈ dyadicHullFamily G cells s₀ ↔ s₀ ≤ K.1 ∧ ∃ I ∈ cells, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G K.1 K.2

noncomputable def TrilinearHT.Auto.cellPowAverage (G : RealDyadicGrid) (q : ℝ) (f : ℝ → ℂ) (K : ℤ × ℤ) : ENNReal

The average of |f|^q over the dyadic cell K.

Equations

• TrilinearHT.Auto.cellPowAverage G q f K = (MeasureTheory.volume (TrilinearHT.Auto.dyadicGridCell G K.1 K.2))⁻¹ * ∫⁻ (x : ℝ) in TrilinearHT.Auto.dyadicGridCell G K.1 K.2, ‖f x‖ₑ ^ q

theorem TrilinearHT.Auto.cellLqNorm_eq (G : RealDyadicGrid) {q : ℝ} (hq : 0 < q) (f : ℝ → ℂ) (hf : Measurable f) (K : ℤ × ℤ) : cellLqNorm G q f K = cellPowAverage G q f K ^ (1 / q)

‖f‖_{q,K} = (avg_K |f|^q)^{1/q}.

noncomputable def TrilinearHT.Auto.FiniteDepthLocalData.restrictScale {κ : LocalKernelClass} {q : ℝ} {N : ℕ} (D : FiniteDepthLocalData κ q N) (S : Finset (ℤ × ℤ)) (hS : S ⊆ D.cells) (c : Fin 4 → ℂ) : FiniteDepthLocalData κ q N

Finite data restricted to a subset of its cells, with rescaled inputs.

Equations

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

theorem TrilinearHT.Auto.FiniteDepthLocalData.restrictScale_numerator {κ : LocalKernelClass} {q : ℝ} {N : ℕ} (D : FiniteDepthLocalData κ q N) (S : Finset (ℤ × ℤ)) (hS : S ⊆ D.cells) (c : Fin 4 → ℂ) : finiteDepthNumerator (D.restrictScale S hS c) = ‖∏ j : Fin 4, c j‖ * ∑ I ∈ S, dyadicGridLength D.grid I.1 * ‖localProgressionForm (dyadicGridLength D.grid I.1) (D.kernel I) D.input‖

theorem TrilinearHT.Auto.piece_bound_of_normalized {κ : LocalKernelClass} {q : ℝ} {N : ℕ} {A c : ℝ} (hnorm : NormalizedAbsorption κ q N A c) (D : FiniteDepthLocalData κ q N) (S : Finset (ℤ × ℤ)) (hS : S ⊆ D.cells) (J : ℤ × ℤ) (hSJ : ∀ I ∈ S, dyadicGridCell D.grid I.1 I.2 ⊆ dyadicGridCell D.grid J.1 J.2) (b : Fin 4 → ℝ) (hb : ∀ (j : Fin 4), 0 ≤ b j) (hloc : ∀ K ∈ dyadicHullCells D.grid S J, ∀ (j : Fin 4), cellLqNorm D.grid q (D.input j) K ≤ ENNReal.ofReal (b j)) : ∑ I ∈ S, dyadicGridLength D.grid I.1 * ‖localProgressionForm (dyadicGridLength D.grid I.1) (D.kernel I) D.input‖ ≤ (∏ j : Fin 4, b j) * (A + c * finiteDepthConstant κ q N) * dyadicGridLength D.grid J.1

Blueprint lines 2916-2918 (piece bound): if every cell of the subtree spanned by S under J has ‖f_j‖_{q,K} ≤ b_j, then normalized absorption applied to f_j/(b_j + ε) gives Σ_{I ∈ S} |I| |H_I(f)| ≤ (Π b_j) (A + c C_N) |J|.

theorem TrilinearHT.Auto.firstStops_pairwiseDisjoint {α : Type u_1} {C : Finset α} {cell : α → Set ℝ} {bad : α → α → Prop} [(J K : α) → Decidable (bad J K)] (hlam : ∀ K ∈ C, ∀ L ∈ C, cell K ⊆ cell L ∨ cell L ⊆ cell K ∨ Disjoint (cell K) (cell L)) (hinj : ∀ K ∈ C, ∀ L ∈ C, cell K = cell L → K = L) (J : α) : (↑(firstStops C cell bad J)).PairwiseDisjoint cell

The first stops of a cell are pairwise disjoint.

theorem TrilinearHT.Auto.finiteDepth_input_lintegral_ne_top {κ : LocalKernelClass} {q : ℝ} {N : ℕ} (hq : 0 < q) (D : FiniteDepthLocalData κ q N) (j : Fin 4) (s : Set ℝ) : ∫⁻ (x : ℝ) in s, ‖D.input j x‖ₑ ^ q ≠ ⊤

The q-th power integral of a finite-depth input is finite.

theorem TrilinearHT.Auto.cellPowAverage_ne_top {κ : LocalKernelClass} {q : ℝ} {N : ℕ} (hq : 0 < q) (D : FiniteDepthLocalData κ q N) (j : Fin 4) (K : ℤ × ℤ) : cellPowAverage D.grid q (D.input j) K ≠ ⊤

theorem TrilinearHT.Auto.cellLqNorm_ne_top {κ : LocalKernelClass} {q : ℝ} {N : ℕ} (hq : 0 < q) (D : FiniteDepthLocalData κ q N) (j : Fin 4) (K : ℤ × ℤ) : cellLqNorm D.grid q (D.input j) K ≠ ⊤

theorem TrilinearHT.Auto.numerator_le_of_normalized {κ : LocalKernelClass} {q : ℝ} {N : ℕ} {A c : ℝ} (hq : 2 ≤ q) (hnorm : NormalizedAbsorption κ q N A c) (hX : 0 ≤ A + c * finiteDepthConstant κ q N) (D : FiniteDepthLocalData κ q N) : ENNReal.ofReal (finiteDepthNumerator D) ≤ ENNReal.ofReal (4 / 3 * 16 ^ (4 / q) * (A + c * finiteDepthConstant κ q N)) * finiteDepthDenominator D

Blueprint thm:uniform-local, lines 2910-2925: normalized absorption implies, for every finite-depth datum, Σ_I |I| |H_I(f)| ≤ (4/3) 16^{4/q} (A + c C_N) ∫ Π_j M_q f_j.

theorem TrilinearHT.Auto.uniform_local_of_normalized (κ : LocalKernelClass) {q : ℝ} (hq : 2 ≤ q) {A c : ℝ} (hA : 0 ≤ A) (hc : 0 ≤ c) (hsmall : 4 / 3 * 16 ^ (4 / q) * c ≤ 1 / 2) (hnorm : ∀ (N : ℕ), NormalizedAbsorption κ q N A c) (N : ℕ) : finiteDepthConstant κ q N ≤ 2 + 2 * (4 / 3 * 16 ^ (4 / q)) * A

Blueprint thm:uniform-local (lines 2906-2932), from prop:normalized: if normalized absorption holds at every depth N with constants A, c independent of N and C c ≤ 1/2 for C = (4/3) 16^{4/q}, then C_N(q) ≤ 2 + 2 C A for every N.

The kernel with four zero marginals (thm:main, blueprint lines 2944-2950)

noncomputable def TrilinearHT.Auto.progDeriv (j : ℝ) (g : ℝ × ℝ → ℂ) (p : ℝ × ℝ) : ℂ

The derivative (∂_S - j ∂_X) g, i.e. along the direction (-j, 1).

Equations

• TrilinearHT.Auto.progDeriv j g p = (fderiv ℝ g p) (-j, 1)

theorem TrilinearHT.Auto.progDeriv_contDiff {j : ℝ} {g : ℝ × ℝ → ℂ} (hg : ContDiff ℝ (↑⊤) g) : ContDiff ℝ (↑⊤) (progDeriv j g)

theorem TrilinearHT.Auto.progDeriv_hasCompactSupport {j : ℝ} {g : ℝ × ℝ → ℂ} (hg : HasCompactSupport g) : HasCompactSupport (progDeriv j g)

theorem TrilinearHT.Auto.progDeriv_comm (a b : ℝ) {g : ℝ × ℝ → ℂ} (hg : ContDiff ℝ (↑⊤) g) : progDeriv a (progDeriv b g) = progDeriv b (progDeriv a g)

The directional derivatives commute on smooth functions (symmetric second derivative).

theorem TrilinearHT.Auto.integral_progDeriv_eq_zero (j u : ℝ) {g : ℝ × ℝ → ℂ} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) : ∫ (S : ℝ), progDeriv j g (u - j * S, S) = 0

Blueprint line 2947: ∫ ((∂_S - j ∂_X) g)(u - jS, S) dS = 0 for compactly supported C¹ functions, since the integrand is the derivative of S ↦ g(u - jS, S).

noncomputable def TrilinearHT.Auto.fourMarginalKernel (g : ℝ × ℝ → ℂ) : ℝ × ℝ → ℂ

Blueprint line 2944: W = Π_{j=0}^3 (∂_S - j ∂_X) g.

Equations

• TrilinearHT.Auto.fourMarginalKernel g = TrilinearHT.Auto.progDeriv 0 (TrilinearHT.Auto.progDeriv 1 (TrilinearHT.Auto.progDeriv 2 (TrilinearHT.Auto.progDeriv 3 g)))

theorem TrilinearHT.Auto.fourMarginalKernel_marginal {g : ℝ × ℝ → ℂ} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (u : ℝ) (j : Fin 4) : ∫ (S : ℝ), fourMarginalKernel g (u - ↑↑j * S, S) = 0

Blueprint lines 2945-2950: for a smooth compactly supported g, the kernel W = Π_j (∂_S - j ∂_X) g has the four zero marginals ∫ W(u - jS, S) dS = 0, j = 0, 1, 2, 3 (the constant-coefficient derivatives commute, so each factor can be taken outermost).

The partition sum of the kernel (thm:main, blueprint lines 2951-2955)

theorem TrilinearHT.Auto.progDeriv_eventuallyEq {j : ℝ} {f g : ℝ × ℝ → ℂ} {p : ℝ × ℝ} (h : f =ᶠ[nhds p] g) : progDeriv j f =ᶠ[nhds p] progDeriv j g

theorem TrilinearHT.Auto.fourMarginalKernel_eventuallyEq {f g : ℝ × ℝ → ℂ} {p : ℝ × ℝ} (h : f =ᶠ[nhds p] g) : fourMarginalKernel f p = fourMarginalKernel g p

theorem TrilinearHT.Auto.progDeriv_sum {ι : Type u_1} (s : Finset ι) (g : ι → ℝ × ℝ → ℂ) (j : ℝ) (hg : ∀ i ∈ s, Differentiable ℝ (g i)) : (progDeriv j fun (p : ℝ × ℝ) => ∑ i ∈ s, g i p) = fun (p : ℝ × ℝ) => ∑ i ∈ s, progDeriv j (g i) p

theorem TrilinearHT.Auto.fourMarginalKernel_sum {ι : Type u_1} (s : Finset ι) (g : ι → ℝ × ℝ → ℂ) (hg : ∀ i ∈ s, ContDiff ℝ (↑⊤) (g i)) : (fourMarginalKernel fun (p : ℝ × ℝ) => ∑ i ∈ s, g i p) = fun (p : ℝ × ℝ) => ∑ i ∈ s, fourMarginalKernel (g i) p

theorem TrilinearHT.Auto.progDeriv_snd {j : ℝ} {φ : ℝ → ℂ} (hφ : Differentiable ℝ φ) : (progDeriv j fun (p : ℝ × ℝ) => φ p.2) = fun (p : ℝ × ℝ) => deriv φ p.2

On functions of S alone, ∂_S - j ∂_X is d/dS.

theorem TrilinearHT.Auto.fourMarginalKernel_snd {φ : ℝ → ℂ} (hφ : ContDiff ℝ (↑⊤) φ) : (fourMarginalKernel fun (p : ℝ × ℝ) => φ p.2) = fun (p : ℝ × ℝ) => iteratedDeriv 4 φ p.2

theorem TrilinearHT.Auto.fourMarginalKernel_zero : (fourMarginalKernel fun (x : ℝ × ℝ) => 0) = 0

theorem TrilinearHT.Auto.fourMarginalKernel_partition_sum {ω : ℝ → ℝ} (hω : ContDiff ℝ (↑⊤) ω) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → ω x = 0) (hsum : ∀ (x : ℝ), ∑' (k : ℤ), ω (x - ↑k) = 1) {φ : ℝ → ℂ} (hφ : ContDiff ℝ (↑⊤) φ) (x s : ℝ) : ∑' (m : ℤ), fourMarginalKernel (fun (p : ℝ × ℝ) => ↑(ω (p.1 - ↑m)) * φ p.2) (x, s) = iteratedDeriv 4 φ s

Blueprint lines 2951-2955: for a smooth integer partition of unity ω supported in (-1, 1) and smooth φ, the translates of W = Π_j (∂_S - j∂_X)[ω(X) φ(S)] sum to Σ_m W(x - m, s) = φ⁽⁴⁾(s) (a locally finite sum).

Three interlacing lattices (thm:main, blueprint lines 2963-2967)

theorem TrilinearHT.Auto.interlacing_boundaries {r α L : ℝ} (hr : 0 < r) (hL : L < r / 3) (σ : ℤ) (hσ : σ = 1 ∨ σ = -1) {j j' n n' : ℤ} (hj : j ∈ Set.Icc (-1) 1) (hj' : j' ∈ Set.Icc (-1) 1) (h : r * (↑n + ↑σ * ↑j / 3) ∈ Set.Icc α (α + L)) (h' : r * (↑n' + ↑σ * ↑j' / 3) ∈ Set.Icc α (α + L)) : j = j'

Blueprint lines 2963-2967: at one depth the boundaries r(ℤ + σ j/3), j ∈ {-1, 0, 1}, σ = ±1, of the three lattices interlace with spacing r/3, so an interval of length less than r/3 contains boundary points of at most one lattice.

The kernel of a product (thm:main, blueprint line 2944)

def TrilinearHT.Auto.tensorKernel (A B : ℝ → ℂ) : ℝ × ℝ → ℂ

The tensor product (X, S) ↦ A(X) B(S).

Equations

• TrilinearHT.Auto.tensorKernel A B p = A p.1 * B p.2

theorem TrilinearHT.Auto.tensorKernel_differentiable {A B : ℝ → ℂ} (hA : Differentiable ℝ A) (hB : Differentiable ℝ B) : Differentiable ℝ (tensorKernel A B)

theorem TrilinearHT.Auto.progDeriv_tensor (j : ℝ) {A B : ℝ → ℂ} (hA : Differentiable ℝ A) (hB : Differentiable ℝ B) : progDeriv j (tensorKernel A B) = fun (p : ℝ × ℝ) => tensorKernel A (deriv B) p - ↑j * tensorKernel (deriv A) B p

(∂_S - j ∂_X)(A ⊗ B) = A ⊗ B' - j A' ⊗ B.

theorem TrilinearHT.Auto.progDeriv_comb (j : ℝ) {ι : Type u_1} (s : Finset ι) (c : ι → ℂ) (f : ι → ℝ × ℝ → ℂ) (hf : ∀ (i : ι), Differentiable ℝ (f i)) : (progDeriv j fun (p : ℝ × ℝ) => ∑ i ∈ s, c i * f i p) = fun (p : ℝ × ℝ) => ∑ i ∈ s, c i * progDeriv j (f i) p

Linearity of ∂_S - j ∂_X on finite combinations.

theorem TrilinearHT.Auto.fourMarginalKernel_tensor {ω φ : ℝ → ℂ} (hω : ContDiff ℝ (↑⊤) ω) (hφ : ContDiff ℝ (↑⊤) φ) : fourMarginalKernel (tensorKernel ω φ) = fun (p : ℝ × ℝ) => tensorKernel ω (iteratedDeriv 4 φ) p - 6 * tensorKernel (iteratedDeriv 1 ω) (iteratedDeriv 3 φ) p + 11 * tensorKernel (iteratedDeriv 2 ω) (iteratedDeriv 2 φ) p - 6 * tensorKernel (iteratedDeriv 3 ω) (iteratedDeriv 1 φ) p

Blueprint line 2944 for a product: with a = ∂_S, b = ∂_X, a(a - b)(a - 2b)(a - 3b) = a⁴ - 6a³b + 11a²b² - 6ab³, so W = ω φFourth - 6 ω' φ''' + 11 ω'' φ'' - 6 ω''' φ'.

Derivatives of rescaled kernels (thm:main, blueprint lines 2970-2974)

theorem TrilinearHT.Auto.localKernelPartial_tensorSum {ι : Type u_1} (s : Finset ι) (c : ι → ℂ) (A B : ι → ℝ → ℂ) (hA : ∀ (k : ι), ContDiff ℝ (↑⊤) (A k)) (hB : ∀ (k : ι), ContDiff ℝ (↑⊤) (B k)) (m n : ℕ) (z : ℝ × ℝ) : localKernelPartial m n (fun (p : ℝ × ℝ) => ∑ k ∈ s, c k * A k p.1 * B k p.2) z = ∑ k ∈ s, c k * iteratedDeriv m (A k) z.1 * iteratedDeriv n (B k) z.2

Partial derivatives of a finite sum of tensors Σ_k c_k A_k(x) B_k(t).

theorem TrilinearHT.Auto.iteratedDeriv_affine_complex (n : ℕ) {f : ℝ → ℂ} (hf : ContDiff ℝ (↑⊤) f) (c a : ℝ) : (iteratedDeriv n fun (x : ℝ) => f (c * x + a)) = fun (x : ℝ) => ↑c ^ n * iteratedDeriv n f (c * x + a)

Affine rescaling for complex-valued functions: (f(c x + a))⁽ⁿ⁾ = cⁿ f⁽ⁿ⁾(c x + a).

theorem TrilinearHT.Auto.iteratedDeriv_ofReal (n : ℕ) {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) : (iteratedDeriv n fun (x : ℝ) => ↑(f x)) = fun (x : ℝ) => ↑(iteratedDeriv n f x)

Derivatives commute with the real-to-complex cast.

noncomputable def TrilinearHT.Auto.rescaledKernel (W : ℝ × ℝ → ℂ) (a r m₀ : ℝ) : ℝ × ℝ → ℂ

The rescaled kernel w(x, t) = (r/a) W(x/a - m₀, t/a).

Equations

• TrilinearHT.Auto.rescaledKernel W a r m₀ p = ↑(r / a) * W (p.1 / a - m₀, p.2 / a)

theorem TrilinearHT.Auto.rescaledKernel_partial_le {ι : Type u_1} (s : Finset ι) (c : ι → ℂ) (A B : ι → ℝ → ℂ) (hA : ∀ (k : ι), ContDiff ℝ (↑⊤) (A k)) (hB : ∀ (k : ι), ContDiff ℝ (↑⊤) (B k)) (GA GB : ι → ℕ → ℝ) (hGA : ∀ (k : ι) (i : ℕ) (x : ℝ), ‖iteratedDeriv i (A k) x‖ ≤ GA k i) (hGB : ∀ (k : ι) (i : ℕ) (x : ℝ), ‖iteratedDeriv i (B k) x‖ ≤ GB k i) {a r : ℝ} (ha : 0 < a) (hr : 0 ≤ r) (m₀ : ℝ) (m n : ℕ) (z : ℝ × ℝ) : ‖localKernelPartial m n (rescaledKernel (fun (p : ℝ × ℝ) => ∑ k ∈ s, c k * A k p.1 * B k p.2) a r m₀) z‖ ≤ r / a * a⁻¹ ^ (m + n) * ∑ k ∈ s, ‖c k‖ * GA k m * GB k n

Blueprint lines 2970-2974: if W = Σ_k c_k A_k(X) B_k(S) with smooth factors whose derivatives are bounded by GA k i, GB k i, then the rescaled kernel has |∂_x^m ∂_t^n w| ≤ (r/a) a^{-(m+n)} Σ_k |c_k| GA k m GB k n.

theorem TrilinearHT.Auto.gevrey_kernel_absorb {C₀ D : ℕ} (hC₀ : 1 ≤ C₀) (hD : 1 ≤ D) (m n k : ℕ) (hk : k ≤ 4) : ↑D ^ (m + n + 1) * 34 * ((↑C₀ * (↑(k + m) + 1)) ^ (C₀ * (k + m + 1)) * (↑C₀ * (↑(4 - k + n) + 1)) ^ (C₀ * (4 - k + n + 1))) ≤ (↑(3 * C₀ + 34 + D) * (↑(m + n) + 2)) ^ ((3 * C₀ + 34 + D) * (m + n + 2))

Blueprint line 2974: the products of Gevrey bounds G(j) = (C₀(j+1))^{C₀(j+1)} occurring in W, together with the factor 34 D^{u+1}, are absorbed by (C(u+2))^{C(u+2)} for C = 3C₀ + 34 + D.

theorem TrilinearHT.Auto.iteratedDeriv_iteratedDeriv_add (i k : ℕ) (f : ℝ → ℂ) : iteratedDeriv i (iteratedDeriv k f) = iteratedDeriv (i + k) f

theorem TrilinearHT.Auto.rescaledW_derivative_bound {ω φ : ℝ → ℂ} (hω : ContDiff ℝ (↑⊤) ω) (hφ : ContDiff ℝ (↑⊤) φ) {C₀ D : ℕ} (hC₀ : 1 ≤ C₀) (hD : 1 ≤ D) (hωG : ∀ (j : ℕ) (x : ℝ), ‖iteratedDeriv j ω x‖ ≤ (↑C₀ * (↑j + 1)) ^ (C₀ * (j + 1))) (hφG : ∀ (j : ℕ) (x : ℝ), ‖iteratedDeriv j φ x‖ ≤ (↑C₀ * (↑j + 1)) ^ (C₀ * (j + 1))) {a : ℝ} (ha : 0 < a) (m₀ : ℝ) (m n : ℕ) (z : ℝ × ℝ) : ‖localKernelPartial m n (rescaledKernel (fourMarginalKernel (tensorKernel ω φ)) a (↑D * a) m₀) z‖ ≤ (↑D * a)⁻¹ ^ (m + n) * (↑(3 * C₀ + 34 + D) * (↑(m + n) + 2)) ^ ((3 * C₀ + 34 + D) * (m + n + 2))

Blueprint lines 2970-2974: for ω, φ with Gevrey bounds ‖g⁽ʲ⁾‖ ≤ (C₀(j+1))^{C₀(j+1)} and r = D a, the rescaled kernel w(x,t) = (r/a) W(x/a - m₀, t/a) of W = Π_j (∂_S - j∂_X)[ω φ] satisfies |∂_x^m ∂_t^n w| ≤ r^{-u} (C(u+2))^{C(u+2)}, u = m + n, with C = 3C₀ + 34 + D independent of a, m₀ and the point.

Gevrey bound for φ(S) = S³ χ(S) (thm:main, blueprint line 2935)

theorem TrilinearHT.Auto.iteratedDeriv_eq_zero_of_notMem_tsupport {f : ℝ → ℝ} {x : ℝ} (hx : x ∉ tsupport f) (n : ℕ) : iteratedDeriv n f x = 0

theorem TrilinearHT.Auto.cubic_cutoff_gevrey {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) {R : ℝ} (hR : 0 ≤ R) (hsupp : tsupport χ ⊆ Set.Icc (-R) R) {Cχ : ℕ} (hCχ : 1 ≤ Cχ) (hG : ∀ (k : ℕ) (x : ℝ), |iteratedDeriv k χ x| ≤ (↑Cχ * (↑k + 1)) ^ (Cχ * (k + 1))) : ∃ (C₀ : ℕ), 1 ≤ C₀ ∧ ∀ (n : ℕ) (x : ℝ), |iteratedDeriv n (fun (S : ℝ) => S ^ 3 * χ S) x| ≤ (↑C₀ * (↑n + 1)) ^ (C₀ * (n + 1))

Blueprint line 2935: if χ is a smooth cutoff supported in [-R, R] with Gevrey bounds |χ⁽ᵏ⁾| ≤ (C(k+1))^{C(k+1)}, then φ(S) = S³ χ(S) has Gevrey bounds with a larger constant.

Support and marginals of the rescaled kernel (thm:main, lines 2966-2970)

theorem TrilinearHT.Auto.tsupport_progDeriv_subset (j : ℝ) (g : ℝ × ℝ → ℂ) : tsupport (progDeriv j g) ⊆ tsupport g

theorem TrilinearHT.Auto.support_fourMarginalKernel_subset (g : ℝ × ℝ → ℂ) : Function.support (fourMarginalKernel g) ⊆ tsupport g

theorem TrilinearHT.Auto.tsupport_tensorKernel_subset (A B : ℝ → ℂ) : tsupport (tensorKernel A B) ⊆ tsupport A ×ˢ tsupport B

theorem TrilinearHT.Auto.rescaledW_support {ω φ : ℝ → ℂ} {R : ℝ} (hR : 0 ≤ R) (hω : tsupport ω ⊆ Set.Icc (-1) 1) (hφ : tsupport φ ⊆ Set.Icc (-R) R) {a r m₀ : ℝ} (ha : 0 < a) (z : ℝ × ℝ) (hz : rescaledKernel (fourMarginalKernel (tensorKernel ω φ)) a r m₀ z ≠ 0) (j : Fin 4) : realProgressionCoordinate j z ∈ Set.Icc (a * (m₀ - 1 - 3 * R)) (a * (m₀ + 1 + 3 * R))

Blueprint lines 2966-2968: if ω is supported in [-1, 1] and φ in [-R, R], the progression coordinates x + j t on the support of the rescaled kernel (r/a) W(x/a - m₀, t/a) lie in [a(m₀ - 1 - 3R), a(m₀ + 1 + 3R)].

theorem TrilinearHT.Auto.rescaledW_marginal {g : ℝ × ℝ → ℂ} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) {a r m₀ : ℝ} (ha : 0 < a) (u : ℝ) (j : Fin 4) : ∫ (t : ℝ), rescaledKernel (fourMarginalKernel g) a r m₀ (u - ↑↑j * t, t) = 0

Blueprint line 2970: rescaling preserves the four zero marginals: ∫ w(u - j t, t) dt = 0 for w(x, t) = (r/a) W(x/a - m₀, t/a).

noncomputable def TrilinearHT.Auto.kernelClassOf (μ : ℝ) (hμ : 0 < μ) (C : ℕ) (hC : 1 ≤ C) : LocalKernelClass

The admissible kernel class with margin μ and derivative constant C.

Equations

• TrilinearHT.Auto.kernelClassOf μ hμ C hC = { margin := μ, margin_pos := hμ, derivativeConstant := ↑C, one_le_derivativeConstant := ⋯ }

theorem TrilinearHT.Auto.rescaledW_admissible {ω φ : ℝ → ℂ} (hω : ContDiff ℝ (↑⊤) ω) (hφ : ContDiff ℝ (↑⊤) φ) {R : ℝ} (hR : 0 ≤ R) (hωs : tsupport ω ⊆ Set.Icc (-1) 1) (hφs : tsupport φ ⊆ Set.Icc (-R) R) {C₀ D : ℕ} (hC₀ : 1 ≤ C₀) (hD : 1 ≤ D) (hωG : ∀ (j : ℕ) (x : ℝ), ‖iteratedDeriv j ω x‖ ≤ (↑C₀ * (↑j + 1)) ^ (C₀ * (j + 1))) (hφG : ∀ (j : ℕ) (x : ℝ), ‖iteratedDeriv j φ x‖ ≤ (↑C₀ * (↑j + 1)) ^ (C₀ * (j + 1))) {μ : ℝ} (hμ : 0 < μ) {a m₀ c : ℝ} (ha : 0 < a) (hcell : c + μ * (↑D * a) ≤ a * (m₀ - 1 - 3 * R) ∧ a * (m₀ + 1 + 3 * R) ≤ c + ↑D * a - μ * (↑D * a)) : IsAdmissibleLocalKernel (kernelClassOf μ hμ (3 * C₀ + 34 + D) ⋯) c (↑D * a) (rescaledKernel (fourMarginalKernel (tensorKernel ω φ)) a (↑D * a) m₀)

Blueprint lines 2966-2974: the rescaled translate w(x,t) = (r/a) W(x/a - m₀, t/a), r = D a, of the kernel W built from Gevrey ω (support [-1,1]) and φ (support [-R,R]), is an admissible local kernel on any cell [c, c + r] whose margin μ r interior contains [a(m₀ - 1 - 3R), a(m₀ + 1 + 3R)], with derivative constant 3C₀ + 34 + D.

theorem TrilinearHT.Auto.interval_in_cell_of_no_boundary {r θ α β : ℝ} (hr : 0 < r) (hno : ∀ (n : ℤ), r * (↑n + θ) ∉ Set.Icc α β) : ∃ (n : ℤ), r * (↑n + θ) ≤ α ∧ β < r * (↑n + θ) + r

A closed interval avoiding the boundaries r(ℤ + θ) lies inside one cell [c, c + r).

theorem TrilinearHT.Auto.exists_lattice_cell_with_margin {r α β : ℝ} (hr : 0 < r) (hlen : β - α + r / 12 < r / 3) (σ : ℤ) (hσ : σ = 1 ∨ σ = -1) : ∃ j ∈ Set.Icc (-1) 1, ∃ (n : ℤ), r * (↑n + ↑σ * ↑j / 3) + r / 24 ≤ α ∧ β ≤ r * (↑n + ↑σ * ↑j / 3) + r - r / 24

Blueprint lines 2966-2968: if β - α + r/12 < r/3, then in one of the lattices with boundaries r(ℤ + σ j/3), j ∈ {0, 1}, the interval [α, β] lies in a single cell with margin r/24.

The three lattices as dyadic grids (thm:main, blueprint lines 2962-2965)

theorem TrilinearHT.Auto.neg_one_pow_natAbs_succ (s : ℤ) : (-1) ^ (s + 1).natAbs = -(-1) ^ s.natAbs

noncomputable def TrilinearHT.Auto.interlacedGrid (r₀ : ℝ) (hr₀ : 0 < r₀) (j : ℤ) : RealDyadicGrid

Blueprint lines 2962-2965: the lattice with boundaries r_s(ℤ + (-1)^s j/3), r_s = r_* 2^{-s}, j ∈ {-1, 0, 1}, is a real dyadic grid: consecutive boundaries are nested since 2(-1)^s j/3 - (-1)^{s+1} j/3 = (-1)^s j is an integer.

Equations

• TrilinearHT.Auto.interlacedGrid r₀ hr₀ j = { baseLength := r₀, baseLength_pos := hr₀, origin := fun (s : ℤ) => r₀ * 2 ^ (-s) * ((-1) ^ s.natAbs * ↑j / 3), alignment := ⋯ }

theorem TrilinearHT.Auto.interlacedGrid_left (r₀ : ℝ) (hr₀ : 0 < r₀) (j s m : ℤ) : dyadicGridLeft (interlacedGrid r₀ hr₀ j) s m = dyadicGridLength (interlacedGrid r₀ hr₀ j) s * (↑m + (-1) ^ s.natAbs * ↑j / 3)

theorem TrilinearHT.Auto.card_int_le_of_interval (S : Finset ℤ) {α L : ℝ} (hL : 0 ≤ L) (h : ∀ m ∈ S, α ≤ ↑m ∧ ↑m ≤ α + L) : ↑S.card ≤ L + 1

Blueprint lines 2968-2969: integers in an interval of length L number at most L + 1; hence a cell of length r = D a receives at most D + 1 translates m a.

Families of local kernels on one grid (thm:main, blueprint lines 2971-2976)

noncomputable def TrilinearHT.Auto.familyLocalSum {ι : Type u_1} (G : RealDyadicGrid) (R : Finset ι) (cell : ι → ℤ × ℤ) (w : ι → ℝ × ℝ → ℂ) (f : Fin 4 → ℝ → ℂ) : ℝ

The local sum Σ_p |I_p| |H_{I_p}(f)| of a family of kernels placed on grid cells.

Equations

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

theorem TrilinearHT.Auto.familyLocalSum_le_of_injective {κ : LocalKernelClass} {q : ℝ} (hq : 2 ≤ q) {N : ℕ} {ι : Type u_1} (G : RealDyadicGrid) (R : Finset ι) (cell : ι → ℤ × ℤ) (w : ι → ℝ × ℝ → ℂ) (s₀ : ℤ) (hdepth : ∀ p ∈ R, s₀ ≤ (cell p).1 ∧ (cell p).1 < s₀ + ↑N) (hadm : ∀ p ∈ R, IsAdmissibleLocalKernel κ (dyadicGridLeft G (cell p).1 (cell p).2) (dyadicGridLength G (cell p).1) (w p)) (hinj : Set.InjOn cell ↑R) (f : Fin 4 → ℝ → ℂ) (hfm : ∀ (i : Fin 4), Measurable (f i)) (hfL : ∀ (i : Fin 4), MeasureTheory.MemLp (f i) (ENNReal.ofReal q) MeasureTheory.volume) (hfc : ∀ (i : Fin 4), HasCompactSupport (f i)) : ENNReal.ofReal (familyLocalSum G R cell w f) ≤ ENNReal.ofReal (finiteDepthConstant κ q N) * ∫⁻ (x : ℝ), ∏ i : Fin 4, scalarMaximalQ q (f i) x

A family of admissible kernels with distinct cells in N consecutive depths of one grid is a finite-depth datum, so its local sum is at most C_N ∫ Π M_q f_j.

theorem TrilinearHT.Auto.familyLocalSum_nonneg {ι : Type u_1} (G : RealDyadicGrid) (R : Finset ι) (cell : ι → ℤ × ℤ) (w : ι → ℝ × ℝ → ℂ) (f : Fin 4 → ℝ → ℂ) : 0 ≤ familyLocalSum G R cell w f

theorem TrilinearHT.Auto.familyLocalSum_le_of_multiplicity {κ : LocalKernelClass} {q : ℝ} (hq : 2 ≤ q) {N : ℕ} {ι : Type u_1} (G : RealDyadicGrid) (cell : ι → ℤ × ℤ) (w : ι → ℝ × ℝ → ℂ) (s₀ : ℤ) (f : Fin 4 → ℝ → ℂ) (hfm : ∀ (i : Fin 4), Measurable (f i)) (hfL : ∀ (i : Fin 4), MeasureTheory.MemLp (f i) (ENNReal.ofReal q) MeasureTheory.volume) (hfc : ∀ (i : Fin 4), HasCompactSupport (f i)) (M : ℕ) (R : Finset ι) : (∀ (c : ℤ × ℤ), {p ∈ R | cell p = c}.card ≤ M) → (∀ p ∈ R, s₀ ≤ (cell p).1 ∧ (cell p).1 < s₀ + ↑N) → (∀ p ∈ R, IsAdmissibleLocalKernel κ (dyadicGridLeft G (cell p).1 (cell p).2) (dyadicGridLength G (cell p).1) (w p)) → ENNReal.ofReal (familyLocalSum G R cell w f) ≤ ↑M * (ENNReal.ofReal (finiteDepthConstant κ q N) * ∫⁻ (x : ℝ), ∏ i : Fin 4, scalarMaximalQ q (f i) x)

Blueprint lines 2968-2976: if at most M kernels of the family share a cell, the family splits into M subfamilies with distinct cells, so its local sum is at most M C_N ∫ Π M_q f_j.

noncomputable def TrilinearHT.Auto.scaleTranslateTerm (W : ℝ × ℝ → ℂ) (a m : ℝ) (f : Fin 4 → ℝ → ℂ) : ℂ

The scale-a translate-m term ∫ a⁻¹ W(x/a - m, t/a) Π_j f_j(x + jt) dx dt of the integrated kernel (blueprint lines 2957-2960).

Equations

• TrilinearHT.Auto.scaleTranslateTerm W a m f = ∫ (z : ℝ × ℝ), ↑a⁻¹ * W (z.1 / a - m, z.2 / a) * ∏ j : Fin 4, f j (TrilinearHT.Auto.realProgressionCoordinate j z)

theorem TrilinearHT.Auto.scaleTranslateTerm_eq (W : ℝ × ℝ → ℂ) {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (m : ℝ) (f : Fin 4 → ℝ → ℂ) : scaleTranslateTerm W a m f = ↑r * localProgressionForm r (rescaledKernel W a r m) f

Blueprint lines 2957-2960: the term equals |I| H_I(f) for the rescaled kernel on a cell of length r = D a.

theorem TrilinearHT.Auto.interlacedGrid_length (r₀ : ℝ) (hr₀ : 0 < r₀) (j n : ℤ) : dyadicGridLength (interlacedGrid r₀ hr₀ j) (-n) = r₀ * 2 ^ n

theorem TrilinearHT.Auto.truncated_scale_sum_bound {ω φ : ℝ → ℂ} (hω : ContDiff ℝ (↑⊤) ω) (hφ : ContDiff ℝ (↑⊤) φ) {R : ℝ} (hR : 0 ≤ R) (hωs : tsupport ω ⊆ Set.Icc (-1) 1) (hφs : tsupport φ ⊆ Set.Icc (-R) R) {C₀ D : ℕ} (hC₀ : 1 ≤ C₀) (hD : 1 ≤ D) (hDR : 8 + 24 * R < ↑D) (hωG : ∀ (j : ℕ) (x : ℝ), ‖iteratedDeriv j ω x‖ ≤ (↑C₀ * (↑j + 1)) ^ (C₀ * (j + 1))) (hφG : ∀ (j : ℕ) (x : ℝ), ‖iteratedDeriv j φ x‖ ≤ (↑C₀ * (↑j + 1)) ^ (C₀ * (j + 1))) {q : ℝ} (hq : 2 ≤ q) (N : ℕ) {b : ℝ} (hb : 0 < b) (n₁ : ℤ) (P : Finset (ℤ × ℤ)) (hP : ∀ p ∈ P, n₁ ≤ p.1 ∧ p.1 < n₁ + ↑N) (f : Fin 4 → ℝ → ℂ) (hfm : ∀ (i : Fin 4), Measurable (f i)) (hfL : ∀ (i : Fin 4), MeasureTheory.MemLp (f i) (ENNReal.ofReal q) MeasureTheory.volume) (hfc : ∀ (i : Fin 4), HasCompactSupport (f i)) : ENNReal.ofReal (∑ p ∈ P, ‖scaleTranslateTerm (fourMarginalKernel (tensorKernel ω φ)) (b * 2 ^ p.1) (↑p.2) f‖) ≤ 3 * (↑(D + 1) * (ENNReal.ofReal (finiteDepthConstant (kernelClassOf (1 / 24) truncated_scale_sum_bound._proof_1 (3 * C₀ + 34 + D) ⋯) q N) * ∫⁻ (x : ℝ), ∏ i : Fin 4, scalarMaximalQ q (f i) x))

Blueprint lines 2957-2976, for one value of b: for any finite set P of scales n (in N consecutive values) and translates m, with a = b 2ⁿ and D > 8 + 24R, Σ_{(n,m) ∈ P} |∫ a⁻¹ W(x/a - m, t/a) Π f_j| ≤ 3 (D + 1) C_N ∫ Π M_q f_j, where C_N is the finite-depth constant of the fixed admissible class.

The maximal-function bound (thm:main, blueprint lines 2976-2980)

theorem TrilinearHT.Auto.scalarMaximalQ_le_hl {q : ℝ} (hq : 0 < q) (f : ℝ → ℂ) (x : ℝ) : scalarMaximalQ q f x ≤ 2 ^ (1 / q) * ClassicalMaximal.hlMaximal MeasureTheory.volume (fun (y : ℝ) => ‖f y‖ ^ q) x ^ (1 / q)

The uncentered powered maximal function is at most 2^{1/q} times the centered one.

theorem TrilinearHT.Auto.scalarMaximalQ_le_of_bound {q : ℝ} (hq : 0 < q) {f : ℝ → ℂ} {B : ℝ} (hB : 0 ≤ B) (hf : ∀ (y : ℝ), ‖f y‖ ≤ B) (x : ℝ) : scalarMaximalQ q f x ≤ ENNReal.ofReal B

theorem TrilinearHT.Auto.eLpNorm_hlMaximal_le_real {p : ℝ} (hp : 1 < p) {h : ℝ → ℝ} (hh : MeasureTheory.AEStronglyMeasurable h MeasureTheory.volume) : MeasureTheory.eLpNorm (ClassicalMaximal.hlMaximal MeasureTheory.volume h) (ENNReal.ofReal p) MeasureTheory.volume ≤ ClassicalMaximal.hlMaximalConst 3 p * MeasureTheory.eLpNorm h (ENNReal.ofReal p) MeasureTheory.volume

The Hardy–Littlewood maximal theorem on ℝ (doubling constant 3).

theorem TrilinearHT.Auto.lintegral_hlMaximal_pow_le {q : ℝ} (hq : 0 < q) (hq3 : q < 3) {f : ℝ → ℂ} (hf : Measurable f) : ∫⁻ (x : ℝ), ClassicalMaximal.hlMaximal MeasureTheory.volume (fun (y : ℝ) => ‖f y‖ ^ q) x ^ (3 / q) ≤ ClassicalMaximal.hlMaximalConst 3 (3 / q) ^ (3 / q) * ∫⁻ (x : ℝ), ‖f x‖ₑ ^ 3

The L³ norm of the centered powered maximal function, for q < 3: ∫ (M (|f|^q))^{3/q} ≤ K^{3/q} ∫ |f|³ with K = hlMaximalConst 3 (3/q).

theorem TrilinearHT.Auto.maximal_product_bound {q : ℝ} (hq : 0 < q) (hq3 : q < 3) (f : Fin 4 → ℝ → ℂ) (hf : ∀ (i : Fin 4), Measurable (f i)) {B : ℝ} (hB : 0 ≤ B) (h0 : ∀ (y : ℝ), ‖f 0 y‖ ≤ B) : ∫⁻ (x : ℝ), ∏ i : Fin 4, scalarMaximalQ q (f i) x ≤ ENNReal.ofReal B * ∏ j : Fin 3, 2 ^ (1 / q) * ClassicalMaximal.hlMaximalConst 3 (3 / q) ^ (1 / q) * (∫⁻ (x : ℝ), ‖f j.succ x‖ₑ ^ 3) ^ (1 / 3)

Blueprint lines 2976-2980: for 0 < q < 3, |f₀| ≤ B and measurable f₁, f₂, f₃, ∫ Π_j M_q f_j ≤ B Π_{j=1}^3 2^{1/q} K^{1/q} ‖f_j‖_3, by Hölder in three L³ factors and the Hardy–Littlewood maximal theorem in L^{3/q}.

The scale-truncated kernel (thm:main, blueprint lines 2955-2958 and 2982-2995)

theorem TrilinearHT.Auto.scale_kernel_integral {ψ ψ' : ℝ → ℂ} (hd : ∀ (x : ℝ), HasDerivAt ψ (ψ' x) x) (hψ' : Continuous ψ') {t A B : ℝ} (ht : t ≠ 0) (hA : 0 < A) (hAB : A ≤ B) : ∫ (a : ℝ) in A..B, ψ' (t / a) * ↑(a ^ 2)⁻¹ = (ψ (t / A) - ψ (t / B)) / ↑t

Blueprint eq:kernel-reconstruction, truncated in scale: for ψ = φ''' with continuous derivative ψ' = φ⁽⁴⁾, t ≠ 0 and 0 < A ≤ B, ∫_A^B ψ'(t/a) a⁻² da = (ψ(t/A) - ψ(t/B))/t.

theorem TrilinearHT.Auto.fourMarginalKernel_translate {ω φ : ℝ → ℂ} (hω : ContDiff ℝ (↑⊤) ω) (hφ : ContDiff ℝ (↑⊤) φ) (m : ℝ) (p : ℝ × ℝ) : fourMarginalKernel (fun (p : ℝ × ℝ) => ω (p.1 - m) * φ p.2) p = fourMarginalKernel (tensorKernel ω φ) (p.1 - m, p.2)

The kernel of a translated product is the translated kernel.

theorem TrilinearHT.Auto.partition_sum_finite {ω φ : ℝ → ℝ} (hω : ContDiff ℝ (↑⊤) ω) (hsupp : ∀ (x : ℝ), 3 / 4 ≤ |x| → ω x = 0) (hsum : ∀ (x : ℝ), ∑' (k : ℤ), ω (x - ↑k) = 1) (hφ : ContDiff ℝ (↑⊤) φ) (X S : ℝ) (F : Finset ℤ) (hF : ∀ (m : ℤ), |X - ↑m| < 1 → m ∈ F) : ∑ m ∈ F, fourMarginalKernel (tensorKernel (fun (y : ℝ) => ↑(ω y)) fun (y : ℝ) => ↑(φ y)) (X - ↑m, S) = iteratedDeriv 4 (fun (y : ℝ) => ↑(φ y)) S

Blueprint line 2952 at scale a: if ω is a smooth partition of unity supported in [-3/4, 3/4], then for every x, t and every finite set F ⊇ {m : |x/a - m| < 1}, Σ_{m ∈ F} W(x/a - m, t/a) = φ⁽⁴⁾(t/a).

theorem TrilinearHT.Auto.integrable_rescaled_kernel {W : ℝ × ℝ → ℂ} (hW : Continuous W) (hWc : HasCompactSupport W) {a : ℝ} (ha : 0 < a) (m : ℝ) : MeasureTheory.Integrable (fun (z : ℝ × ℝ) => W (z.1 / a - m, z.2 / a)) MeasureTheory.volume

A continuous compactly supported kernel composed with the affine map z ↦ (z.1/a - m, z.2/a) is integrable.

theorem TrilinearHT.Auto.sum_scaleTranslateTerm {ω φ : ℝ → ℝ} (hω : ContDiff ℝ (↑⊤) ω) (hsupp : ∀ (x : ℝ), 3 / 4 ≤ |x| → ω x = 0) (hsum : ∀ (x : ℝ), ∑' (k : ℤ), ω (x - ↑k) = 1) (hωc : HasCompactSupport ω) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) {a T : ℝ} (ha : 0 < a) (f : Fin 4 → ℝ → ℂ) (hfm : ∀ (i : Fin 4), Measurable (f i)) {Bf : ℝ} (hfb : ∀ (i : Fin 4) (x : ℝ), ‖f i x‖ ≤ Bf) (hf0 : ∀ (x : ℝ), T < |x| → f 0 x = 0) (F : Finset ℤ) (hF : ∀ (m : ℤ), |↑m| ≤ T / a + 1 → m ∈ F) : ∑ m ∈ F, scaleTranslateTerm (fourMarginalKernel (tensorKernel (fun (y : ℝ) => ↑(ω y)) fun (y : ℝ) => ↑(φ y))) a (↑m) f = ∫ (z : ℝ × ℝ), ↑a⁻¹ * iteratedDeriv 4 (fun (y : ℝ) => ↑(φ y)) (z.2 / a) * ∏ j : Fin 4, f j (realProgressionCoordinate j z)

Blueprint lines 2951-2958 at scale a: if f₀ vanishes outside [-T, T] and F contains all m with |m| ≤ T/a + 1, then Σ_{m ∈ F} ∫ a⁻¹ W(x/a - m, t/a) Π f_j = ∫ a⁻¹ φ⁽⁴⁾(t/a) Π f_j.

theorem TrilinearHT.Auto.scale_fubini {ψ' : ℝ → ℂ} (hψ' : Continuous ψ') {R Bψ : ℝ} (hψb : ∀ (s : ℝ), ‖ψ' s‖ ≤ Bψ) (hψs : ∀ (s : ℝ), R < |s| → ψ' s = 0) (f : Fin 4 → ℝ → ℂ) (hfm : ∀ (i : Fin 4), Measurable (f i)) {Bf T : ℝ} (hfb : ∀ (i : Fin 4) (x : ℝ), ‖f i x‖ ≤ Bf) (hf0 : ∀ (x : ℝ), T < |x| → f 0 x = 0) {A B : ℝ} (hA : 0 < A) (hAB : A ≤ B) : ∫ (a : ℝ) in A..B, (∫ (z : ℝ × ℝ), ↑a⁻¹ * ψ' (z.2 / a) * ∏ j : Fin 4, f j (realProgressionCoordinate j z)) * ↑a⁻¹ = ∫ (z : ℝ × ℝ), (∫ (a : ℝ) in A..B, ψ' (z.2 / a) * ↑(a ^ 2)⁻¹) * ∏ j : Fin 4, f j (realProgressionCoordinate j z)

Blueprint lines 2955-2958 (Fubini in the scale): for 0 < A ≤ B, inputs bounded by Bf with f₀ supported in [-T, T], and ψ' = φ⁽⁴⁾ bounded by Bψ and supported in [-R, R], ∫_A^B (∫ a⁻¹ ψ'(t/a) Π f) a⁻¹ da = ∫ (∫_A^B ψ'(t/a) a⁻² da) Π f.

theorem TrilinearHT.Auto.setLIntegral_Ico_scale (H : ℝ → ENNReal) {c : ℝ} (hc : 0 < c) : ∫⁻ (a : ℝ) in Set.Ico c (2 * c), H a = ENNReal.ofReal c * ∫⁻ (b : ℝ) in Set.Ico 1 2, H (c * b)

Rescaling a dyadic scale block: for c > 0, ∫⁻_{[c, 2c)} H = c ∫⁻_{[1, 2)} H(c b) db (no measurability of H is needed).

theorem TrilinearHT.Auto.lintegral_dyadic_blocks_le (H : ℝ → ENNReal) (n₁ n₂ : ℤ) : n₁ ≤ n₂ → ∫⁻ (a : ℝ) in Set.Ico (2 ^ n₁) (2 ^ n₂), H a ≤ ∫⁻ (b : ℝ) in Set.Ico 1 2, ∑ n ∈ Finset.Ico n₁ n₂, ENNReal.ofReal (2 ^ n) * H (2 ^ n * b)

Blueprint lines 2955-2957 (a = b 2ⁿ): the scale integral over [2^{n₁}, 2^{n₂}) is at most ∫⁻_{[1,2)} Σ_{n₁ ≤ n < n₂} 2ⁿ H(2ⁿ b) db.

theorem TrilinearHT.Auto.integrated_scale_form_bound {ω φ : ℝ → ℝ} (hω : ContDiff ℝ (↑⊤) ω) (hsupp : ∀ (x : ℝ), 3 / 4 ≤ |x| → ω x = 0) (hsum : ∀ (x : ℝ), ∑' (k : ℤ), ω (x - ↑k) = 1) (hωc : HasCompactSupport ω) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) {R : ℝ} (hR : 0 ≤ R) (hωs : (tsupport fun (y : ℝ) => ↑(ω y)) ⊆ Set.Icc (-1) 1) (hφs : (tsupport fun (y : ℝ) => ↑(φ y)) ⊆ Set.Icc (-R) R) {C₀ D : ℕ} (hC₀ : 1 ≤ C₀) (hD : 1 ≤ D) (hDR : 8 + 24 * R < ↑D) (hωG : ∀ (j : ℕ) (x : ℝ), ‖iteratedDeriv j (fun (y : ℝ) => ↑(ω y)) x‖ ≤ (↑C₀ * (↑j + 1)) ^ (C₀ * (j + 1))) (hφG : ∀ (j : ℕ) (x : ℝ), ‖iteratedDeriv j (fun (y : ℝ) => ↑(φ y)) x‖ ≤ (↑C₀ * (↑j + 1)) ^ (C₀ * (j + 1))) {q : ℝ} (hq : 2 ≤ q) {Cst : ℝ} (hCst : ∀ (N : ℕ), finiteDepthConstant (kernelClassOf (1 / 24) truncated_scale_sum_bound._proof_1 (3 * C₀ + 34 + D) ⋯) q N ≤ Cst) (f : Fin 4 → ℝ → ℂ) (hfm : ∀ (i : Fin 4), Measurable (f i)) {Bf T : ℝ} (hfb : ∀ (i : Fin 4) (x : ℝ), ‖f i x‖ ≤ Bf) (hT : 0 ≤ T) (hf0 : ∀ (x : ℝ), T < |x| → f 0 x = 0) (hfL : ∀ (i : Fin 4), MeasureTheory.MemLp (f i) (ENNReal.ofReal q) MeasureTheory.volume) (hfc : ∀ (i : Fin 4), HasCompactSupport (f i)) {A B : ℝ} (hA : 0 < A) (hAB : A ≤ B) : ‖∫ (z : ℝ × ℝ), (∫ (a : ℝ) in A..B, iteratedDeriv 4 (fun (y : ℝ) => ↑(φ y)) (z.2 / a) * ↑(a ^ 2)⁻¹) * ∏ j : Fin 4, f j (realProgressionCoordinate j z)‖ₑ ≤ 3 * (↑(D + 1) * (ENNReal.ofReal Cst * ∫⁻ (x : ℝ), ∏ i : Fin 4, scalarMaximalQ q (f i) x))

Blueprint lines 2955-2980, before the scale limit: the four-linear form with the integrated scale kernel K_{A,B}(t) = ∫_A^B φ⁽⁴⁾(t/a) a⁻² da is bounded by 3 (D + 1) C ∫ Π M_q f_j, uniformly in 0 < A ≤ B, whenever all finite-depth constants of the fixed admissible class are at most C.

The scale limit (thm:main, blueprint lines 2982-2995)

theorem TrilinearHT.Auto.explicit_kernel_bound {ψ ψd : ℝ → ℂ} (hd : ∀ (x : ℝ), HasDerivAt ψ (ψd x) x) {Bψ Bd : ℝ} (hψb : ∀ (s : ℝ), ‖ψ s‖ ≤ Bψ) (hdb : ∀ (s : ℝ), ‖ψd s‖ ≤ Bd) {n : ℝ} (hn : 1 ≤ n) (t : ℝ) : ‖(ψ (t * n) - ψ (t / n)) / ↑t‖ ≤ 2 * Bψ + Bd * n

The explicit truncated kernel (ψ(nt) - ψ(t/n))/t is bounded by 2 B_ψ + B' n when ψ is bounded by B_ψ with derivative bounded by B'.

theorem TrilinearHT.Auto.explicit_kernel_tendsto {ψ ψd : ℝ → ℂ} (hd : ∀ (x : ℝ), HasDerivAt ψ (ψd x) x) {Bψ Bd R : ℝ} (hψb : ∀ (s : ℝ), ‖ψ s‖ ≤ Bψ) (hdb : ∀ (s : ℝ), ‖ψd s‖ ≤ Bd) (hψs : ∀ (s : ℝ), R < |s| → ψ s = 0) (heven : ∀ (s : ℝ), ψ (-s) = ψ s) {P : ℝ × ℝ → ℂ} (hPi : MeasureTheory.Integrable P MeasureTheory.volume) (hQi : MeasureTheory.Integrable (fun (z : ℝ × ℝ) => (P z - P (z.1, -z.2)) / ↑z.2) MeasureTheory.volume) : Filter.Tendsto (fun (n : ℕ) => ∫ (z : ℝ × ℝ), (ψ (z.2 * ↑n) - ψ (z.2 / ↑n)) / ↑z.2 * P z) Filter.atTop (nhds (-ψ 0 / 2 * ∫ (z : ℝ × ℝ), (P z - P (z.1, -z.2)) / ↑z.2))

Blueprint lines 2982-2995 (dominated convergence in the scale range [1/n, n]): for an even C¹ profile ψ = φ''' supported in [-R, R] and an integrable P whose odd quotient Q(x,t) = (P(x,t) - P(x,-t))/t is integrable, ∫ (ψ(nt) - ψ(t/n))/t · P → -ψ(0)/2 · ∫ Q.

theorem TrilinearHT.Auto.integrable_strip_shift {u : ℝ → ℂ} (hu : MeasureTheory.Integrable u MeasureTheory.volume) (huc : Continuous u) (T : ℝ) {c : ℝ} (hc : c ≠ 0) : MeasureTheory.Integrable (fun (z : ℝ × ℝ) => (Set.Icc (-T) T).indicator (fun (x : ℝ) => 1) z.1 * ‖u (z.1 + c * z.2)‖) MeasureTheory.volume

A strip-cut shifted integrable function: (x, t) ↦ 1_{[-T,T]}(x) ‖u(x + c t)‖ is integrable on ℝ² for c ≠ 0.

theorem TrilinearHT.Auto.progression_odd_quotient_integrable (f : Fin 4 → ℝ → ℂ) (hf0m : Measurable (f 0)) {M T : ℝ} (hfb : ∀ (i : Fin 4) (x : ℝ), ‖f i x‖ ≤ M) (hf0 : ∀ (x : ℝ), T < |x| → f 0 x = 0) (hfd : ∀ (j : Fin 3), Differentiable ℝ (f j.succ)) (hfd' : ∀ (j : Fin 3) (x : ℝ), ‖deriv (f j.succ) x‖ ≤ M) (hf1 : MeasureTheory.Integrable (f 1) MeasureTheory.volume) : MeasureTheory.Integrable (fun (z : ℝ × ℝ) => ∏ j : Fin 4, f j (realProgressionCoordinate j z)) MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (z : ℝ × ℝ) => (∏ j : Fin 4, f j (realProgressionCoordinate j z) - ∏ j : Fin 4, f j (realProgressionCoordinate j (z.1, -z.2))) / ↑z.2) MeasureTheory.volume

Blueprint lines 2984-2992, integrated in x: for f₀ bounded measurable supported in [-T, T] and C¹ inputs f₁, f₂, f₃ with values and derivatives bounded by M and f₁ integrable, the progression product P(x,t) = Π_j f_j(x + jt) and its odd quotient (P(x,t) - P(x,-t))/t are integrable on ℝ².

theorem TrilinearHT.Auto.odd_quotient_integral_eq (f : Fin 4 → ℝ → ℂ) (hQi : MeasureTheory.Integrable (fun (z : ℝ × ℝ) => (∏ j : Fin 4, f j (realProgressionCoordinate j z) - ∏ j : Fin 4, f j (realProgressionCoordinate j (z.1, -z.2))) / ↑z.2) MeasureTheory.volume) : ∫ (z : ℝ × ℝ), (∏ j : Fin 4, f j (realProgressionCoordinate j z) - ∏ j : Fin 4, f j (realProgressionCoordinate j (z.1, -z.2))) / ↑z.2 = -2 * ∫ (x : ℝ), f 0 x * ∫ (t : ℝ) in Set.Ioi 0, (f 1 (x - t) * f 2 (x - 2 * t) * f 3 (x - 3 * t) - f 1 (x - -t) * f 2 (x - 2 * -t) * f 3 (x - 3 * -t)) / ↑t

Blueprint lines 2990-2995 (pairing t with -t and reflecting): if the odd quotient Q(x,t) = (P(x,t) - P(x,-t))/t of the progression product P(x,t) = Π_j f_j(x + jt) is integrable, then ∫ Q = -2 ∫ f₀(x) I(x) dx, where I(x) = ∫_{t > 0} (g(t) - g(-t))/t dt for g(t) = f₁(x - t) f₂(x - 2t) f₃(x - 3t) is the odd-part integral (T = -I on Schwartz inputs, T_eq_neg_integral).

theorem TrilinearHT.Auto.ae_snd_ne_zero : ∀ᵐ (z : ℝ × ℝ), z.2 ≠ 0

The set {t = 0} is null in ℝ².

theorem TrilinearHT.Auto.integrated_kernel_form_eq {ψ ψ' : ℝ → ℂ} (hd : ∀ (x : ℝ), HasDerivAt ψ (ψ' x) x) (hψ' : Continuous ψ') {A B : ℝ} (hA : 0 < A) (hAB : A ≤ B) (P : ℝ × ℝ → ℂ) : ∫ (z : ℝ × ℝ), (∫ (a : ℝ) in A..B, ψ' (z.2 / a) * ↑(a ^ 2)⁻¹) * P z = ∫ (z : ℝ × ℝ), (ψ (z.2 / A) - ψ (z.2 / B)) / ↑z.2 * P z

Blueprint eq:kernel-reconstruction inside the four-linear form: for 0 < A ≤ B, the integrated kernel ∫_A^B ψ'(t/a) a⁻² da may be replaced by (ψ(t/A) - ψ(t/B))/t.

theorem TrilinearHT.Auto.iteratedDeriv_bound_support {φ : ℝ → ℂ} (hφ : ContDiff ℝ (↑⊤) φ) {R : ℝ} (hφs : tsupport φ ⊆ Set.Icc (-R) R) (k : ℕ) : (∀ (s : ℝ), R < |s| → iteratedDeriv k φ s = 0) ∧ ∃ (B : ℝ), ∀ (s : ℝ), ‖iteratedDeriv k φ s‖ ≤ B

The k-th derivative of a smooth function supported in [-R, R] is bounded and vanishes outside [-R, R].

theorem TrilinearHT.Auto.pv_form_bound {ω φ : ℝ → ℝ} (hω : ContDiff ℝ (↑⊤) ω) (hsupp : ∀ (x : ℝ), 3 / 4 ≤ |x| → ω x = 0) (hsum : ∀ (x : ℝ), ∑' (k : ℤ), ω (x - ↑k) = 1) (hωc : HasCompactSupport ω) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (hφodd : ∀ (s : ℝ), φ (-s) = -φ s) {R : ℝ} (hR : 0 ≤ R) (hωs : (tsupport fun (y : ℝ) => ↑(ω y)) ⊆ Set.Icc (-1) 1) (hφs : (tsupport fun (y : ℝ) => ↑(φ y)) ⊆ Set.Icc (-R) R) {C₀ D : ℕ} (hC₀ : 1 ≤ C₀) (hD : 1 ≤ D) (hDR : 8 + 24 * R < ↑D) (hωG : ∀ (j : ℕ) (x : ℝ), ‖iteratedDeriv j (fun (y : ℝ) => ↑(ω y)) x‖ ≤ (↑C₀ * (↑j + 1)) ^ (C₀ * (j + 1))) (hφG : ∀ (j : ℕ) (x : ℝ), ‖iteratedDeriv j (fun (y : ℝ) => ↑(φ y)) x‖ ≤ (↑C₀ * (↑j + 1)) ^ (C₀ * (j + 1))) {q : ℝ} (hq : 2 ≤ q) (hq3 : q < 3) {Cst : ℝ} (hCst : ∀ (N : ℕ), finiteDepthConstant (kernelClassOf (1 / 24) truncated_scale_sum_bound._proof_1 (3 * C₀ + 34 + D) ⋯) q N ≤ Cst) {f₀ : ℝ → ℂ} (hf₀m : Measurable f₀) {B₀ T : ℝ} (hB₀ : 0 ≤ B₀) (hf₀b : ∀ (x : ℝ), ‖f₀ x‖ ≤ B₀) (hT : 0 ≤ T) (hf₀T : ∀ (x : ℝ), T < |x| → f₀ x = 0) (f₁ f₂ f₃ : SchwartzMap ℝ ℂ) : ‖iteratedDeriv 3 (fun (y : ℝ) => ↑(φ y)) 0 * ∫ (x : ℝ), f₀ x * TrilinearHT.T ![⇑f₁, ⇑f₂, ⇑f₃] x‖ₑ ≤ 3 * (↑(D + 1) * (ENNReal.ofReal Cst * (ENNReal.ofReal B₀ * ∏ j : Fin 3, 2 ^ (1 / q) * ClassicalMaximal.hlMaximalConst 3 (3 / q) ^ (1 / q) * (∫⁻ (x : ℝ), ‖![f₀, ⇑f₁, ⇑f₂, ⇑f₃] j.succ x‖ₑ ^ 3) ^ (1 / 3))))

Blueprint lines 2955-2995: for f₀ bounded by B₀, measurable and supported in [-T, T], and Schwartz f₁, f₂, f₃, the principal-value form satisfies |φ'''(0)| |∫ f₀ T(f₁, f₂, f₃)| ≤ 3 (D + 1) C B₀ Π_j 2^{1/q} K^{1/q} ‖f_j‖₃, whenever all finite-depth constants of the fixed admissible class are at most C.

The L¹ bound by duality (thm:main, blueprint lines 2996-2999)

theorem TrilinearHT.Auto.lintegral_enorm_le_of_duality {g : ℝ → ℂ} (hg : Measurable g) {Mg : ℝ} (hgb : ∀ (x : ℝ), ‖g x‖ ≤ Mg) {Y : ENNReal} (h : ∀ (f₀ : ℝ → ℂ) (T : ℝ), Measurable f₀ → (∀ (x : ℝ), ‖f₀ x‖ ≤ 1) → 0 ≤ T → (∀ (x : ℝ), T < |x| → f₀ x = 0) → ‖∫ (x : ℝ), f₀ x * g x‖ₑ ≤ Y) : ∫⁻ (x : ℝ), ‖g x‖ₑ ≤ Y

Blueprint lines 2996-2999 (duality): a bounded measurable g whose pairings with all measurable tests |f₀| ≤ 1 supported in compact intervals are bounded by Y satisfies ∫ |g| ≤ Y. The test f₀ = 1_{[-R,R]} conj(g)/|g| gives ∫_{[-R,R]} |g|, and monotone convergence lets R → ∞.

theorem TrilinearHT.Auto.progression_odd_diff_le {f₁ f₂ f₃ : ℝ → ℂ} {M : ℝ} (hd : ∀ i ∈ [f₁, f₂, f₃], Differentiable ℝ i) (hb : ∀ i ∈ [f₁, f₂, f₃], ∀ (x : ℝ), ‖i x‖ ≤ M) (hb' : ∀ i ∈ [f₁, f₂, f₃], ∀ (x : ℝ), ‖deriv i x‖ ≤ M) (x t : ℝ) : ‖f₁ (x - t) * f₂ (x - 2 * t) * f₃ (x - 3 * t) - f₁ (x - -t) * f₂ (x - 2 * -t) * f₃ (x - 3 * -t)‖ ≤ 12 * M ^ 3 * |t|

Blueprint lines 2984-2989, uniformly in x: the odd part of the progression product along x - jt is at most 12 M³ |t| when the inputs and their derivatives are bounded by M.

noncomputable def TrilinearHT.Auto.oddIntegrandMajorant (f₁ : ℝ → ℂ) (M x t : ℝ) : ℝ

The integrable majorant 12 M³ 1_{(0,1]}(t) + M² (|f₁(x - t)| + |f₁(x + t)|) of the odd part (g(t) - g(-t))/t of the progression product.

Equations

• TrilinearHT.Auto.oddIntegrandMajorant f₁ M x t = (Set.Ioc 0 1).indicator (fun (x : ℝ) => 12 * M ^ 3) t + M ^ 2 * (‖f₁ (x - t)‖ + ‖f₁ (x + t)‖)

theorem TrilinearHT.Auto.oddIntegrandMajorant_integrable {f₁ : ℝ → ℂ} (hi : MeasureTheory.Integrable f₁ MeasureTheory.volume) (M x : ℝ) : MeasureTheory.Integrable (oddIntegrandMajorant f₁ M x) MeasureTheory.volume

theorem TrilinearHT.Auto.oddIntegrand_le {f₁ f₂ f₃ : ℝ → ℂ} {M : ℝ} (hd : ∀ i ∈ [f₁, f₂, f₃], Differentiable ℝ i) (hb : ∀ i ∈ [f₁, f₂, f₃], ∀ (x : ℝ), ‖i x‖ ≤ M) (hb' : ∀ i ∈ [f₁, f₂, f₃], ∀ (x : ℝ), ‖deriv i x‖ ≤ M) (x : ℝ) {t : ℝ} (htp : 0 < t) : ‖(f₁ (x - t) * f₂ (x - 2 * t) * f₃ (x - 3 * t) - f₁ (x - -t) * f₂ (x - 2 * -t) * f₃ (x - 3 * -t)) / ↑t‖ ≤ oddIntegrandMajorant f₁ M x t

Blueprint lines 2984-2992, uniformly in x: for t > 0 the odd part of the progression product divided by t is dominated by oddIntegrandMajorant.

theorem TrilinearHT.Auto.oddIntegrand_integrableOn {f₁ f₂ f₃ : ℝ → ℂ} {M : ℝ} (hd : ∀ i ∈ [f₁, f₂, f₃], Differentiable ℝ i) (hb : ∀ i ∈ [f₁, f₂, f₃], ∀ (x : ℝ), ‖i x‖ ≤ M) (hb' : ∀ i ∈ [f₁, f₂, f₃], ∀ (x : ℝ), ‖deriv i x‖ ≤ M) (hi : MeasureTheory.Integrable f₁ MeasureTheory.volume) (x : ℝ) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (f₁ (x - t) * f₂ (x - 2 * t) * f₃ (x - 3 * t) - f₁ (x - -t) * f₂ (x - 2 * -t) * f₃ (x - 3 * -t)) / ↑t) (Set.Ioi 0) MeasureTheory.volume

The odd-part integrand (g(t) - g(-t))/t of the progression product is integrable on (0, ∞).

theorem TrilinearHT.Auto.oddIntegral_bound {f₁ f₂ f₃ : ℝ → ℂ} {M : ℝ} (hd : ∀ i ∈ [f₁, f₂, f₃], Differentiable ℝ i) (hb : ∀ i ∈ [f₁, f₂, f₃], ∀ (x : ℝ), ‖i x‖ ≤ M) (hb' : ∀ i ∈ [f₁, f₂, f₃], ∀ (x : ℝ), ‖deriv i x‖ ≤ M) (hi : MeasureTheory.Integrable f₁ MeasureTheory.volume) (x : ℝ) : ‖∫ (t : ℝ) in Set.Ioi 0, (f₁ (x - t) * f₂ (x - 2 * t) * f₃ (x - 3 * t) - f₁ (x - -t) * f₂ (x - 2 * -t) * f₃ (x - 3 * -t)) / ↑t‖ ≤ 12 * M ^ 3 + 2 * (M ^ 2 * ∫ (y : ℝ), ‖f₁ y‖)

The odd-part integral is uniformly bounded: |∫_{t > 0} (g(t) - g(-t))/t dt| ≤ 12 M³ + 2 M² ‖f₁‖₁.

theorem TrilinearHT.Auto.oddIntegral_measurable {f₁ f₂ f₃ : ℝ → ℂ} (h₁ : Continuous f₁) (h₂ : Continuous f₂) (h₃ : Continuous f₃) : Measurable fun (x : ℝ) => ∫ (t : ℝ) in Set.Ioi 0, (f₁ (x - t) * f₂ (x - 2 * t) * f₃ (x - 3 * t) - f₁ (x - -t) * f₂ (x - 2 * -t) * f₃ (x - 3 * -t)) / ↑t

The odd-part integral of continuous inputs is measurable in x.

theorem TrilinearHT.Auto.T_eq_neg_integral_fun (f₁ f₂ f₃ : SchwartzMap ℝ ℂ) : T ![⇑f₁, ⇑f₂, ⇑f₃] = fun (x : ℝ) => -∫ (t : ℝ) in Set.Ioi 0, (f₁ (x - t) * f₂ (x - 2 * t) * f₃ (x - 3 * t) - f₁ (x - -t) * f₂ (x - 2 * -t) * f₃ (x - 3 * -t)) / ↑t

TrilinearHT.T of Schwartz inputs as a function: minus the odd-part integral.

theorem TrilinearHT.Auto.T_measurable (f₁ f₂ f₃ : SchwartzMap ℝ ℂ) : Measurable (T ![⇑f₁, ⇑f₂, ⇑f₃])

TrilinearHT.T of Schwartz inputs is measurable.

theorem TrilinearHT.Auto.T_bound {f₁ f₂ f₃ : SchwartzMap ℝ ℂ} {M : ℝ} (hd : ∀ i ∈ [⇑f₁, ⇑f₂, ⇑f₃], Differentiable ℝ i) (hb : ∀ i ∈ [⇑f₁, ⇑f₂, ⇑f₃], ∀ (x : ℝ), ‖i x‖ ≤ M) (hb' : ∀ i ∈ [⇑f₁, ⇑f₂, ⇑f₃], ∀ (x : ℝ), ‖deriv i x‖ ≤ M) (x : ℝ) : ‖T ![⇑f₁, ⇑f₂, ⇑f₃] x‖ ≤ 12 * M ^ 3 + 2 * (M ^ 2 * ∫ (y : ℝ), ‖f₁ y‖)

TrilinearHT.T of Schwartz inputs is uniformly bounded: |T(f₁, f₂, f₃)(x)| ≤ 12 M³ + 2 M² ‖f₁‖₁.

theorem TrilinearHT.Auto.T_lintegral_le {ω φ : ℝ → ℝ} (hω : ContDiff ℝ (↑⊤) ω) (hsupp : ∀ (x : ℝ), 3 / 4 ≤ |x| → ω x = 0) (hsum : ∀ (x : ℝ), ∑' (k : ℤ), ω (x - ↑k) = 1) (hωc : HasCompactSupport ω) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (hφodd : ∀ (s : ℝ), φ (-s) = -φ s) (hφ0 : iteratedDeriv 3 (fun (y : ℝ) => ↑(φ y)) 0 ≠ 0) {R : ℝ} (hR : 0 ≤ R) (hωs : (tsupport fun (y : ℝ) => ↑(ω y)) ⊆ Set.Icc (-1) 1) (hφs : (tsupport fun (y : ℝ) => ↑(φ y)) ⊆ Set.Icc (-R) R) {C₀ D : ℕ} (hC₀ : 1 ≤ C₀) (hD : 1 ≤ D) (hDR : 8 + 24 * R < ↑D) (hωG : ∀ (j : ℕ) (x : ℝ), ‖iteratedDeriv j (fun (y : ℝ) => ↑(ω y)) x‖ ≤ (↑C₀ * (↑j + 1)) ^ (C₀ * (j + 1))) (hφG : ∀ (j : ℕ) (x : ℝ), ‖iteratedDeriv j (fun (y : ℝ) => ↑(φ y)) x‖ ≤ (↑C₀ * (↑j + 1)) ^ (C₀ * (j + 1))) {q : ℝ} (hq : 2 ≤ q) (hq3 : q < 3) {Cst : ℝ} (hCst : ∀ (N : ℕ), finiteDepthConstant (kernelClassOf (1 / 24) truncated_scale_sum_bound._proof_1 (3 * C₀ + 34 + D) ⋯) q N ≤ Cst) (f₁ f₂ f₃ : SchwartzMap ℝ ℂ) : ∫⁻ (x : ℝ), ‖T ![⇑f₁, ⇑f₂, ⇑f₃] x‖ₑ ≤ 3 * (↑(D + 1) * (ENNReal.ofReal Cst * ∏ j : Fin 3, 2 ^ (1 / q) * ClassicalMaximal.hlMaximalConst 3 (3 / q) ^ (1 / q) * MeasureTheory.eLpNorm (![⇑f₁, ⇑f₂, ⇑f₃] j) 3 MeasureTheory.volume)) / ‖iteratedDeriv 3 (fun (y : ℝ) => ↑(φ y)) 0‖ₑ

Blueprint thm:main, lines 2955-2999: for Schwartz f₁, f₂, f₃, ‖T(f₁, f₂, f₃)‖₁ ≤ |φ'''(0)|⁻¹ 3 (D + 1) C Π_j 2^{1/q} K^{1/q} ‖f_j‖₃, whenever all finite-depth constants of the fixed admissible class built from ω, φ are at most C.

The concrete kernel and the L¹ bound (thm:main, blueprint lines 2934-2947)

theorem TrilinearHT.Auto.gevrey_bound_mono {C C' : ℕ} (hC : 1 ≤ C) (hCC' : C ≤ C') (j : ℕ) : (↑C * (↑j + 1)) ^ (C * (j + 1)) ≤ (↑C' * (↑j + 1)) ^ (C' * (j + 1))

Gevrey bounds are monotone in the constant.

theorem TrilinearHT.Auto.gevreyIntervalCutoff_even (x : ℝ) : gevreyIntervalCutoff (-2) (-1) 1 2 (-x) = gevreyIntervalCutoff (-2) (-1) 1 2 x

The even cutoff χ = 1 on [-1, 1], supported in (-2, 2).

theorem TrilinearHT.Auto.cubic_profile_exists : ∃ (φ : ℝ → ℝ), ContDiff ℝ (↑⊤) φ ∧ HasCompactSupport φ ∧ (∀ (s : ℝ), φ (-s) = -φ s) ∧ iteratedDeriv 3 (fun (y : ℝ) => ↑(φ y)) 0 = 6 ∧ (tsupport fun (y : ℝ) => ↑(φ y)) ⊆ Set.Icc (-2) 2 ∧ ∃ (C : ℕ), 1 ≤ C ∧ ∀ (j : ℕ) (x : ℝ), ‖iteratedDeriv j (fun (y : ℝ) => ↑(φ y)) x‖ ≤ (↑C * (↑j + 1)) ^ (C * (j + 1))

Blueprint lines 2934-2936: the profile φ(S) = S³ χ(S), with χ an even Gevrey cutoff equal to one near zero, is smooth, odd, supported in [-2, 2], Gevrey, and φ'''(0) = 6.

theorem TrilinearHT.Auto.gevreyPartition_complex : (tsupport fun (y : ℝ) => ↑(gevreyPartition y)) ⊆ Set.Icc (-1) 1 ∧ ∃ (C : ℕ), 1 ≤ C ∧ ∀ (j : ℕ) (x : ℝ), ‖iteratedDeriv j (fun (y : ℝ) => ↑(gevreyPartition y)) x‖ ≤ (↑C * (↑j + 1)) ^ (C * (j + 1))

The Gevrey partition ω in complex form: smooth, supported in [-1, 1], Gevrey.

theorem TrilinearHT.Auto.T_L1_bound_of_uniform (huni : ∀ (κ : LocalKernelClass), ∃ (q : ℝ), 2 ≤ q ∧ q < 3 ∧ ∃ (Cst : ℝ), ∀ (N : ℕ), finiteDepthConstant κ q N ≤ Cst) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (f₁ f₂ f₃ : SchwartzMap ℝ ℂ), ∫⁻ (x : ℝ), ‖T ![⇑f₁, ⇑f₂, ⇑f₃] x‖ₑ ≤ ENNReal.ofReal C * (MeasureTheory.eLpNorm (⇑f₁) 3 MeasureTheory.volume * MeasureTheory.eLpNorm (⇑f₂) 3 MeasureTheory.volume * MeasureTheory.eLpNorm (⇑f₃) 3 MeasureTheory.volume)

Blueprint thm:main, lines 2934-2999, given thm:uniform-local: if every admissible class has uniformly bounded finite-depth constants for some q ∈ [2, 3), then ‖T(f₁, f₂, f₃)‖₁ ≤ C Π_j ‖f_j‖₃ for Schwartz inputs, with one finite C.

theorem TrilinearHT.Auto.schwartz_triple_bounds (f₁ f₂ f₃ : SchwartzMap ℝ ℂ) : ∃ (M : ℝ), (∀ i ∈ [⇑f₁, ⇑f₂, ⇑f₃], Differentiable ℝ i) ∧ (∀ i ∈ [⇑f₁, ⇑f₂, ⇑f₃], ∀ (x : ℝ), ‖i x‖ ≤ M) ∧ ∀ i ∈ [⇑f₁, ⇑f₂, ⇑f₃], ∀ (x : ℝ), ‖deriv i x‖ ≤ M

The bounds needed for TrilinearHT.T on Schwartz inputs: differentiability and uniform bounds on the functions and their derivatives.

theorem TrilinearHT.Auto.oddIntegrand_schwartz_integrableOn (f₁ f₂ f₃ : SchwartzMap ℝ ℂ) (x : ℝ) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (f₁ (x - t) * f₂ (x - 2 * t) * f₃ (x - 3 * t) - f₁ (x - -t) * f₂ (x - 2 * -t) * f₃ (x - 3 * -t)) / ↑t) (Set.Ioi 0) MeasureTheory.volume

theorem TrilinearHT.Auto.T_add (f₁ g₁ f₂ g₂ f₃ g₃ : SchwartzMap ℝ ℂ) (x : ℝ) : T ![⇑(f₁ + g₁), ⇑f₂, ⇑f₃] x = T ![⇑f₁, ⇑f₂, ⇑f₃] x + T ![⇑g₁, ⇑f₂, ⇑f₃] x ∧ T ![⇑f₁, ⇑(f₂ + g₂), ⇑f₃] x = T ![⇑f₁, ⇑f₂, ⇑f₃] x + T ![⇑f₁, ⇑g₂, ⇑f₃] x ∧ T ![⇑f₁, ⇑f₂, ⇑(f₃ + g₃)] x = T ![⇑f₁, ⇑f₂, ⇑f₃] x + T ![⇑f₁, ⇑f₂, ⇑g₃] x

TrilinearHT.T is additive in each Schwartz argument.

theorem TrilinearHT.Auto.T_smul (c : ℂ) (f₁ f₂ f₃ : SchwartzMap ℝ ℂ) (x : ℝ) : T ![⇑(c • f₁), ⇑f₂, ⇑f₃] x = c • T ![⇑f₁, ⇑f₂, ⇑f₃] x ∧ T ![⇑f₁, ⇑(c • f₂), ⇑f₃] x = c • T ![⇑f₁, ⇑f₂, ⇑f₃] x ∧ T ![⇑f₁, ⇑f₂, ⇑(c • f₃)] x = c • T ![⇑f₁, ⇑f₂, ⇑f₃] x

TrilinearHT.T is homogeneous in each Schwartz argument.

theorem TrilinearHT.Auto.tht_main_of_uniform (huni : ∀ (κ : LocalKernelClass), ∃ (q : ℝ), 2 ≤ q ∧ q < 3 ∧ ∃ (Cst : ℝ), ∀ (N : ℕ), finiteDepthConstant κ q N ≤ Cst) : ∃ (C : ℝ), 0 ≤ C ∧ (∀ (f₁ f₂ f₃ : SchwartzMap ℝ ℂ), (∀ (x : ℝ), Filter.Tendsto (truncatedTransform ![⇑f₁, ⇑f₂, ⇑f₃] x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (T ![⇑f₁, ⇑f₂, ⇑f₃] x))) ∧ MeasureTheory.MemLp (T ![⇑f₁, ⇑f₂, ⇑f₃]) 1 MeasureTheory.volume ∧ ∫⁻ (x : ℝ), ‖T ![⇑f₁, ⇑f₂, ⇑f₃] x‖ₑ ≤ ENNReal.ofReal C * (MeasureTheory.eLpNorm (⇑f₁) 3 MeasureTheory.volume * MeasureTheory.eLpNorm (⇑f₂) 3 MeasureTheory.volume * MeasureTheory.eLpNorm (⇑f₃) 3 MeasureTheory.volume)) ∧ ∃ (T' : ↥(MeasureTheory.Lp ℂ 3 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 3 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 3 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 1 MeasureTheory.volume)), (∀ (f₁ f₂ f₃ : SchwartzMap ℝ ℂ), ↑↑(((T' (f₁.toLp 3 MeasureTheory.volume)) (f₂.toLp 3 MeasureTheory.volume)) (f₃.toLp 3 MeasureTheory.volume)) =ᵐ[MeasureTheory.volume] T ![⇑f₁, ⇑f₂, ⇑f₃]) ∧ (∀ (x y z : ↥(MeasureTheory.Lp ℂ 3 MeasureTheory.volume)), ‖((T' x) y) z‖ ≤ C * ‖x‖ * ‖y‖ * ‖z‖) ∧ ∀ (S : ↥(MeasureTheory.Lp ℂ 3 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 3 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 3 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 1 MeasureTheory.volume)), (∀ (f₁ f₂ f₃ : SchwartzMap ℝ ℂ), ↑↑(((S (f₁.toLp 3 MeasureTheory.volume)) (f₂.toLp 3 MeasureTheory.volume)) (f₃.toLp 3 MeasureTheory.volume)) =ᵐ[MeasureTheory.volume] T ![⇑f₁, ⇑f₂, ⇑f₃]) → S = T'

Blueprint thm:main (lines 2934-3009), given thm:uniform-local in the form of uniformly bounded finite-depth constants for every admissible class: for Schwartz inputs the principal value T(f₁, f₂, f₃)(x) = p.v. ∫ f₁(x - t) f₂(x - 2t) f₃(x - 3t) dt/t exists at every x, lies in L¹ with ‖T(f₁, f₂, f₃)‖₁ ≤ C Π_j ‖f_j‖₃, and T has a unique bounded trilinear extension L³ × L³ × L³ → L¹.

theorem TrilinearHT.Auto.uniform_of_normalized (hnorm : ∀ (κ : LocalKernelClass), ∃ (q : ℝ), 2 ≤ q ∧ q < 3 ∧ ∃ (A : ℝ) (c : ℝ), 0 ≤ A ∧ 0 ≤ c ∧ 4 / 3 * 16 ^ (4 / q) * c ≤ 1 / 2 ∧ ∀ (N : ℕ), NormalizedAbsorption κ q N A c) (κ : LocalKernelClass) : ∃ (q : ℝ), 2 ≤ q ∧ q < 3 ∧ ∃ (Cst : ℝ), ∀ (N : ℕ), finiteDepthConstant κ q N ≤ Cst

thm:uniform-local from prop:normalized for every admissible class.

theorem TrilinearHT.Auto.isAdmissibleLocalKernel_zero (κ : LocalKernelClass) (a : ℝ) {r : ℝ} (hr : 0 < r) : IsAdmissibleLocalKernel κ a r 0

The zero kernel is admissible (it carries the unused cells of a finite tree).

theorem TrilinearHT.Auto.tree_expansion_bound {κ : LocalKernelClass} {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {w : ℤ × ℤ → ℝ × ℝ → ℂ} {f : Fin 4 → ℝ → ℂ} {g : ℕ → ℤ × ℤ → ℝ → ℂ} {kk : ℕ → ℕ} (hcells : ∀ I ∈ dyadicFiniteTree G J N, kernelHull G J N w I → ∃ (D : StaggerCell κ), D.r = dyadicGridLength G I.1 ∧ D.w = w I ∧ D.f = f ∧ (∀ (t : ℕ), D.g t = g t I) ∧ (∀ (T : ℕ), D.H D.f = D.H (D.tail T) + ∑ u ∈ Finset.Icc 1 T, (D.H (Function.update (D.tail T) (stagPos u) (D.incr u)) + ∑ t ∈ Finset.Ioc u T, if stagPos t ≠ stagPos u then D.H (D.tuple u t) else 0)) ∧ ∀ (T : ℕ), 4 ≤ T → ‖D.H (D.tail T)‖ ≤ 32 * Real.exp (-↑(kk (T - 3))) ∧ ∀ (u : ℕ), ‖D.H (Function.update (D.tail T) (stagPos u) (D.incr u))‖ ≤ 32 * Real.exp (-↑(kk (T - 3)))) (T : ℕ) (hT : 4 ≤ T) : ∑ I ∈ dyadicFiniteTree G J N, dyadicGridLength G I.1 * ‖localProgressionForm (dyadicGridLength G I.1) (w I) f‖ ≤ (↑T + 1) * (32 * Real.exp (-↑(kk (T - 3)))) * ∑ I ∈ dyadicFiniteTree G J N, dyadicGridLength G I.1 + ∑ u ∈ Finset.Icc 1 T, ∑ t ∈ Finset.Ioc u T, if stagPos t ≠ stagPos u then ∑ I ∈ dyadicFiniteTree G J N, dyadicGridLength G I.1 * ‖localProgressionForm (dyadicGridLength G I.1) (w I) (stagTuple f g u t I)‖ else 0

Blueprint lines 2893-2904 (the expansion at a finite cutoff T): on a finite tree whose kernel-hull cells carry stagger cells, the length-weighted sum of |H_I(f)| is at most the remainders (T+1) 32 e^{-k_{T-3}} per unit length plus the tuple sums over the update pairs 1 ≤ u < t ≤ T in distinct positions.

def TrilinearHT.Auto.ActiveSetup.LevelProps {κ : LocalKernelClass} {c₀ : ℕ} (B : ActiveSetup κ c₀) (k Cb : ℕ) (η₀ : ℝ) : Prop

The properties of the active setups of a noninitial level produced by activeCellReduction, at accuracy k, complexity exponent C_b and pair bound η₀, including the sub-root properties used by restarts.

Equations

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

def TrilinearHT.Auto.ActiveFinal (κ : LocalKernelClass) : Prop

Blueprint eq:active-final (prop:normalized, lines 2885-2888) as a statement about the active setups of the base reduction: for every complexity order c', exponent C_b and pair exponent θ₀, there are q ∈ (2, 3), c_* > 0 and C such that, at every large accuracy k, every active setup with the level properties at η₀ = e^{-2 k^{θ₀}} whose nonzero kernels lie in N consecutive depths satisfies Σ_I |I| |H_I(Y)| ≤ (C η₀^{c_*} (1 + C_N(q)) + e^{-k}) |R|.

Equations

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

theorem TrilinearHT.Auto.StaggerCell.tuple_measurable {κ : LocalKernelClass} (C : StaggerCell κ) (u t : ℕ) (l : Fin 4) : Measurable (C.tuple u t l)

theorem TrilinearHT.Auto.tendsto_cutoff_remainder {kk : ℕ → ℕ} (hkk : ∀ (t : ℕ), 1 ≤ t → ↑t ≤ ↑(kk t)) (S : ℝ) : Filter.Tendsto (fun (T : ℕ) => (↑T + 1) * (32 * Real.exp (-↑(kk (T - 3)))) * S) Filter.atTop (nhds 0)

The cutoff remainders vanish: if k_t ≥ t for t ≥ 1, then (T+1) e^{-k_{T-3}} → 0.

noncomputable def TrilinearHT.Auto.levelSum (G : RealDyadicGrid) (J : ℤ × ℤ) (N : ℕ) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (f : Fin 4 → ℝ → ℂ) (g : ℕ → ℤ × ℤ → ℝ → ℂ) (u t : ℕ) : ℝ

The length-weighted sum of the forms of one level, over a finite tree with kernels w.

Equations

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

theorem TrilinearHT.Auto.levelSum_nonneg (G : RealDyadicGrid) (J : ℤ × ℤ) (N : ℕ) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (f : Fin 4 → ℝ → ℂ) (g : ℕ → ℤ × ℤ → ℝ → ℂ) (u t : ℕ) : 0 ≤ levelSum G J N w f g u t

theorem TrilinearHT.Auto.sum_levelSum (G : RealDyadicGrid) (J : ℤ × ℤ) (N : ℕ) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (f : Fin 4 → ℝ → ℂ) (g : ℕ → ℤ × ℤ → ℝ → ℂ) (T : ℕ) : (∑ u ∈ Finset.Icc 1 T, ∑ t ∈ Finset.Ioc u T, if stagPos t ≠ stagPos u then ∑ I ∈ dyadicFiniteTree G J N, dyadicGridLength G I.1 * ‖localProgressionForm (dyadicGridLength G I.1) (w I) (stagTuple f g u t I)‖ else 0) = ∑ u ∈ Finset.Icc 1 T, ∑ t ∈ Finset.Ioc u T, levelSum G J N w f g u t

Over the update pairs of a cutoff, the tuple sums are the level sums.