Section 11.1: Two structured inputs and delayed moments (part 1a: lem:predictors)

This file was automatically generated by Claude.

Formalization of blueprint Section 11, "The base reduction" (sec:base), subsection 1, "Two structured inputs and delayed moments", part 1a: lem:predictors (lines 1480-1535) of blueprint/formalization_blueprint.tex.

theorem TrilinearHT.Auto.integral_conj_mul_eq_fourier {τ : ℝ → ℂ} (hτ1 : MeasureTheory.Integrable τ MeasureTheory.volume) (hτ2 : MeasureTheory.MemLp τ 2 MeasureTheory.volume) (F : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ∫ (y : ℝ), (starRingEnd ℂ) (τ y) * ↑↑F y = ∫ (ξ : ℝ), (starRingEnd ℂ) (FourierTransform.fourier τ ξ) * ↑↑(FourierTransform.fourier F) ξ

Parseval for a test function in L¹ ∩ L² against an L² class.

theorem TrilinearHT.Auto.memLp_two_mul_bounded {m : ℝ → ℂ} (hm : Measurable m) {M : ℝ} (hM : ∀ (ξ : ℝ), ‖m ξ‖ ≤ M) (G : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : MeasureTheory.MemLp (fun (ξ : ℝ) => m ξ * ↑↑G ξ) 2 MeasureTheory.volume

A bounded measurable multiplier of an L² class.

theorem TrilinearHT.Auto.norm_sq_toLp_mul {m : ℝ → ℂ} (hm : Measurable m) {M : ℝ} (hM : ∀ (ξ : ℝ), ‖m ξ‖ ≤ M) (G : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ‖MeasureTheory.MemLp.toLp (fun (ξ : ℝ) => m ξ * ↑↑G ξ) ⋯‖ ^ 2 = ∫ (ξ : ℝ), ‖m ξ‖ ^ 2 * ‖↑↑G ξ‖ ^ 2

The squared norm of a multiplier class.

theorem TrilinearHT.Auto.fourier_modulation_real (f : ℝ → ℂ) (c ξ : ℝ) : FourierTransform.fourier (fun (y : ℝ) => ↑(Real.fourierChar (c * y)) * f y) ξ = FourierTransform.fourier f (ξ - c)

Modulation by e(c y) translates the Fourier transform on the line.

theorem TrilinearHT.Auto.norm_integral_cell_test_le {g : ℝ → ℂ} {a r B : ℝ} (hr : 0 < r) (hB : 0 ≤ B) (hgm : Measurable g) (hgb : ∀ (y : ℝ), ‖g y‖ ≤ B) (hgs : ∀ y ∉ Set.Ico a (a + r), g y = 0) (K : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ‖∫ (y : ℝ), (starRingEnd ℂ) (g y) * ↑↑K y‖ ≤ B * √r * √(∫ (y : ℝ) in Set.Ico a (a + r), ‖↑↑K y‖ ^ 2)

A bounded test function on a cell of length r, paired against an L² class.

noncomputable def TrilinearHT.Auto.bumpMultiplier (η : ℝ) : ℝ

The frequency weight of the single-scale square function: quadratic vanishing at the center and fourth-power decay away from it.

Equations

• TrilinearHT.Auto.bumpMultiplier η = if |η| ≤ 1 then (2 * Real.pi * η) ^ 2 else ((2 * Real.pi * η) ^ 2)⁻¹ ^ 2

theorem TrilinearHT.Auto.bumpMultiplier_nonneg (η : ℝ) : 0 ≤ bumpMultiplier η

theorem TrilinearHT.Auto.measurable_bumpMultiplier : Measurable bumpMultiplier

theorem TrilinearHT.Auto.sum_setIntegral_disjoint_le {ι : Type u_1} (S : Finset ι) (s : ι → Set ℝ) (hs : ∀ (i : ι), MeasurableSet (s i)) (hdisj : (↑S).PairwiseDisjoint s) {g : ℝ → ℝ} (hg0 : ∀ (y : ℝ), 0 ≤ g y) (hgi : MeasureTheory.Integrable g MeasureTheory.volume) : ∑ i ∈ S, ∫ (y : ℝ) in s i, g y ≤ ∫ (y : ℝ), g y

Sums of set integrals over pairwise disjoint cells are at most the whole integral.

theorem TrilinearHT.Auto.fourier_deriv_compact {Θ : ℝ → ℂ} (hΘ : ContDiff ℝ 1 Θ) (hΘc : HasCompactSupport Θ) (η : ℝ) : FourierTransform.fourier (deriv Θ) η = 2 * ↑Real.pi * Complex.I * ↑η * FourierTransform.fourier Θ η

Fourier transform of a compactly supported C¹ derivative.

theorem TrilinearHT.Auto.Lp_norm_sq_eq_integral (u : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ‖u‖ ^ 2 = ∫ (y : ℝ), ‖↑↑u y‖ ^ 2

theorem TrilinearHT.Auto.integrable_conj_mul_of_memLp {f g : ℝ → ℂ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : MeasureTheory.Integrable (fun (x : ℝ) => (starRingEnd ℂ) (f x) * g x) MeasureTheory.volume

The product of two square-integrable functions, one conjugated, is integrable.

theorem TrilinearHT.Auto.hasCompactSupport_of_zero_outside_Ico {f : ℝ → ℂ} {a r : ℝ} (hf : ∀ y ∉ Set.Ico a (a + r), f y = 0) : HasCompactSupport f

theorem TrilinearHT.Auto.cell_bump_square_function {ι : Type u_1} (S : Finset ι) (a : ι → ℝ) {r A c : ℝ} (hr : 0 < r) (hA : 0 ≤ A) (hdisj : (↑S).PairwiseDisjoint fun (i : ι) => Set.Ico (a i) (a i + r)) (θ Θ : ι → ℝ → ℂ) (hΘ : ∀ (i : ι), ContDiff ℝ 1 (Θ i)) (hθ : ∀ (i : ι), ContDiff ℝ 2 (θ i)) (hΘd : ∀ (i : ι), deriv (Θ i) = θ i) (hΘs : ∀ (i : ι), ∀ y ∉ Set.Ico (a i) (a i + r), Θ i y = 0) (hθ2s : ∀ (i : ι), ∀ y ∉ Set.Ico (a i) (a i + r), deriv (deriv (θ i)) y = 0) (hΘb : ∀ (i : ι) (y : ℝ), ‖Θ i y‖ ≤ A * r) (hθ2b : ∀ (i : ι) (y : ℝ), ‖deriv (deriv (θ i)) y‖ ≤ A / r ^ 2) (F : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ∑ i ∈ S, r⁻¹ * ‖∫ (y : ℝ), (starRingEnd ℂ) (↑(Real.fourierChar (c * y)) * θ i y) * ↑↑F y‖ ^ 2 ≤ 2 * A ^ 2 * ∫ (ξ : ℝ), bumpMultiplier (r * (ξ - c)) * ‖↑↑(FourierTransform.fourier F) ξ‖ ^ 2

Blueprint lem:predictors, proof line 1531 (single-scale part): modulated mean-zero bumps on disjoint cells of length r are jointly Bessel, with a frequency weight vanishing quadratically at the modulation frequency and decaying to fourth order away from it.

noncomputable def TrilinearHT.Auto.bumpBandBound (ℓ : ℤ) : ℝ

The dyadic band envelope of bumpMultiplier.

Equations

• TrilinearHT.Auto.bumpBandBound ℓ = if ℓ ≤ 0 then (2 * Real.pi) ^ 2 * 4 ^ (ℓ + 1) else ((2 * Real.pi) ^ 4)⁻¹ * 16 ^ (-ℓ)

theorem TrilinearHT.Auto.bumpBandBound_nonneg (ℓ : ℤ) : 0 ≤ bumpBandBound ℓ

theorem TrilinearHT.Auto.bumpMultiplier_le_band {η : ℝ} {ℓ : ℤ} (h1 : 2 ^ ℓ ≤ |η|) (h2 : |η| < 2 ^ (ℓ + 1)) : bumpMultiplier η ≤ bumpBandBound ℓ

theorem TrilinearHT.Auto.bumpMultiplier_le (η : ℝ) : bumpMultiplier η ≤ (2 * Real.pi) ^ 2

theorem TrilinearHT.Auto.hasSum_half_pow_natAbs : HasSum (fun (ℓ : ℤ) => (1 / 2) ^ ℓ.natAbs) 3

theorem TrilinearHT.Auto.band_term_le (ℓ : ℤ) : (1 + 2 ^ ℓ) * bumpBandBound ℓ ≤ 8 * (2 * Real.pi) ^ 2 * (1 / 2) ^ ℓ.natAbs

theorem TrilinearHT.Auto.sum_bumpMultiplier_le {ι : Type u_1} (T : Finset ι) (η : ι → ℝ) {N : ℝ} (hN : 0 ≤ N) (hband : ∀ (ℓ : ℤ), ↑{p ∈ T | 2 ^ ℓ ≤ |η p| ∧ |η p| < 2 ^ (ℓ + 1)}.card ≤ N * (1 + 2 ^ ℓ)) : ∑ p ∈ T, bumpMultiplier (η p) ≤ 24 * (2 * Real.pi) ^ 2 * N

Blueprint lem:predictors, proof line 1531: if every dyadic band 2^ℓ ≤ |η| < 2^(ℓ+1) contains at most N (1 + 2^ℓ) of the normalized frequency offsets, then the summed square-function weight is at most a fixed multiple of N.

theorem TrilinearHT.Auto.multiscale_bump_bessel {κ : Type u_1} {ι : Type u_2} (T : Finset κ) (r c : κ → ℝ) (hr : ∀ (p : κ), 0 < r p) (S : κ → Finset ι) (a : κ → ι → ℝ) {A : ℝ} (hA : 0 ≤ A) (hdisj : ∀ (p : κ), (↑(S p)).PairwiseDisjoint fun (i : ι) => Set.Ico (a p i) (a p i + r p)) (θ Θ : κ → ι → ℝ → ℂ) (hΘ : ∀ (p : κ) (i : ι), ContDiff ℝ 1 (Θ p i)) (hθ : ∀ (p : κ) (i : ι), ContDiff ℝ 2 (θ p i)) (hΘd : ∀ (p : κ) (i : ι), deriv (Θ p i) = θ p i) (hΘs : ∀ (p : κ) (i : ι), ∀ y ∉ Set.Ico (a p i) (a p i + r p), Θ p i y = 0) (hθ2s : ∀ (p : κ) (i : ι), ∀ y ∉ Set.Ico (a p i) (a p i + r p), deriv (deriv (θ p i)) y = 0) (hΘb : ∀ (p : κ) (i : ι) (y : ℝ), ‖Θ p i y‖ ≤ A * r p) (hθ2b : ∀ (p : κ) (i : ι) (y : ℝ), ‖deriv (deriv (θ p i)) y‖ ≤ A / r p ^ 2) {M : ℝ} (hM : ∀ (ξ : ℝ), ∑ p ∈ T, bumpMultiplier (r p * (ξ - c p)) ≤ M) (F : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ∑ p ∈ T, ∑ i ∈ S p, (r p)⁻¹ * ‖∫ (y : ℝ), (starRingEnd ℂ) (↑(Real.fourierChar (c p * y)) * θ p i y) * ↑↑F y‖ ^ 2 ≤ 2 * A ^ 2 * M * ‖F‖ ^ 2

Blueprint lem:predictors, proof line 1531: the multi-scale square-function bound. If the weights of all scale-frequency pairs sum to at most M at every frequency, the modulated mean-zero bump rows over all pairs and cells are jointly Bessel.

theorem TrilinearHT.Auto.meanZero_bump_primitive {θ : ℝ → ℂ} (hθ : Continuous θ) {a r : ℝ} (hr : 0 < r) (hs : ∀ y ∉ Set.Ico a (a + r), θ y = 0) (hmean : ∫ (y : ℝ), θ y = 0) {B : ℝ} (hB : ∀ (y : ℝ), ‖θ y‖ ≤ B) : (ContDiff ℝ 1 fun (y : ℝ) => ∫ (s : ℝ) in a..y, θ s) ∧ (deriv fun (y : ℝ) => ∫ (s : ℝ) in a..y, θ s) = θ ∧ (∀ y ∉ Set.Ico a (a + r), ∫ (s : ℝ) in a..y, θ s = 0) ∧ ∀ (y : ℝ), ‖∫ (s : ℝ) in a..y, θ s‖ ≤ B * r

The primitive of a continuous mean-zero bump supported in a cell is a C¹ function supported in the same cell.

theorem TrilinearHT.Auto.multiscale_meanZero_bessel {κ : Type u_1} {ι : Type u_2} (T : Finset κ) (r c : κ → ℝ) (hr : ∀ (p : κ), 0 < r p) (S : κ → Finset ι) (a : κ → ι → ℝ) {A : ℝ} (hA : 0 ≤ A) (hdisj : ∀ (p : κ), (↑(S p)).PairwiseDisjoint fun (i : ι) => Set.Ico (a p i) (a p i + r p)) (θ : κ → ι → ℝ → ℂ) (hθ : ∀ (p : κ) (i : ι), ContDiff ℝ 2 (θ p i)) (hθs : ∀ (p : κ) (i : ι), ∀ y ∉ Set.Ico (a p i) (a p i + r p), θ p i y = 0) (hmean : ∀ (p : κ) (i : ι), ∫ (y : ℝ), θ p i y = 0) (hθb : ∀ (p : κ) (i : ι) (y : ℝ), ‖θ p i y‖ ≤ A) (hθ2b : ∀ (p : κ) (i : ι) (y : ℝ), ‖deriv (deriv (θ p i)) y‖ ≤ A / r p ^ 2) {M : ℝ} (hM : ∀ (ξ : ℝ), ∑ p ∈ T, bumpMultiplier (r p * (ξ - c p)) ≤ M) (F : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ∑ p ∈ T, ∑ i ∈ S p, (r p)⁻¹ * ‖∫ (y : ℝ), (starRingEnd ℂ) (↑(Real.fourierChar (c p * y)) * θ p i y) * ↑↑F y‖ ^ 2 ≤ 2 * A ^ 2 * M * ‖F‖ ^ 2

Blueprint lem:predictors, proof line 1531: the multi-scale square function for smooth mean-zero bumps supported in disjoint cells, with ‖θ‖ ≤ A and ‖θ''‖ ≤ A r⁻².

noncomputable def TrilinearHT.Auto.kernelUnitEnvelope (κ : LocalKernelClass) (m : ℕ) : ℝ

The derivative envelope of the unit-rescaled admissible kernel at order m.

Equations

• TrilinearHT.Auto.kernelUnitEnvelope κ m = 4 ^ 2 * (16 ^ m * TrilinearHT.Auto.kernelDerivBound κ m)

theorem TrilinearHT.Auto.exists_unit_plateau {m : ℝ} (hm : 0 < m) (hm4 : m ≤ 1 / 4) : ∃ (η₁ : ℝ → ℝ) (K : ℝ) (I : ℝ), ContDiff ℝ (↑⊤) η₁ ∧ (∀ (u : ℝ), 0 ≤ η₁ u ∧ η₁ u ≤ 1) ∧ (∀ (u : ℝ), |u| ≤ 1 / 2 - m → η₁ u = 1) ∧ (∀ (u : ℝ), 1 / 2 - m / 2 ≤ |u| → η₁ u = 0) ∧ 0 < I ∧ ∫ (u : ℝ), η₁ u = I ∧ 0 ≤ K ∧ ∀ (u : ℝ), ∀ i ≤ 2, ‖iteratedFDeriv ℝ i η₁ u‖ ≤ K

A fixed unit-scale plateau bump: equal to one on |u| ≤ 1/2 - m, supported in |u| < 1/2 - m/2, with bounded derivatives up to order two and positive integral.

noncomputable def TrilinearHT.Auto.plateauAt (η₁ : ℝ → ℝ) (a₀ r y : ℝ) : ℂ

The unit plateau transported to the cell [a₀, a₀ + r).

Equations

• TrilinearHT.Auto.plateauAt η₁ a₀ r y = ↑(η₁ ((y - (a₀ + r / 2)) / r))

noncomputable def TrilinearHT.Auto.meanZeroWave (η₁ : ℝ → ℝ) (I a₀ r α y : ℝ) : ℂ

The mean-zero projection Π(η e(α ·)) = η e(α ·) - (∫ η e(α ·)) η / ∫ η.

Equations

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

theorem TrilinearHT.Auto.plateauAt_eq_zero {η₁ : ℝ → ℝ} {m : ℝ} (hm : 0 < m) (hη0 : ∀ (u : ℝ), 1 / 2 - m / 2 ≤ |u| → η₁ u = 0) {a₀ r : ℝ} (hr : 0 < r) {y : ℝ} (hy : y ∉ Set.Ico a₀ (a₀ + r)) : plateauAt η₁ a₀ r y = 0

theorem TrilinearHT.Auto.plateauAt_contDiff {η₁ : ℝ → ℝ} (hη : ContDiff ℝ (↑⊤) η₁) (a₀ r : ℝ) : ContDiff ℝ (↑⊤) (plateauAt η₁ a₀ r)

theorem TrilinearHT.Auto.integral_plateauAt {η₁ : ℝ → ℝ} {I : ℝ} (hIη : ∫ (u : ℝ), η₁ u = I) {a₀ r : ℝ} (hr : 0 < r) : ∫ (y : ℝ), plateauAt η₁ a₀ r y = ↑(r * I)

theorem TrilinearHT.Auto.plateauAt_geomBound {η₁ : ℝ → ℝ} {K : ℝ} (hη : ContDiff ℝ (↑⊤) η₁) (hKb : ∀ (u : ℝ), ∀ i ≤ 2, ‖iteratedFDeriv ℝ i η₁ u‖ ≤ K) {a₀ r : ℝ} (hr : 0 < r) (y : ℝ) : GeomBound (plateauAt η₁ a₀ r) y K (1 / r) 2

Geometric derivative bounds of the transported plateau.

theorem TrilinearHT.Auto.meanZeroWave_props {η₁ : ℝ → ℝ} {m K I : ℝ} (hm : 0 < m) (hη : ContDiff ℝ (↑⊤) η₁) (hη01 : ∀ (u : ℝ), 0 ≤ η₁ u ∧ η₁ u ≤ 1) (hη0 : ∀ (u : ℝ), 1 / 2 - m / 2 ≤ |u| → η₁ u = 0) (hI : 0 < I) (hIη : ∫ (u : ℝ), η₁ u = I) (hK : 0 ≤ K) (hKb : ∀ (u : ℝ), ∀ i ≤ 2, ‖iteratedFDeriv ℝ i η₁ u‖ ≤ K) {a₀ r : ℝ} (hr : 0 < r) (α : ℝ) : ContDiff ℝ (↑⊤) (meanZeroWave η₁ I a₀ r α) ∧ (∀ y ∉ Set.Ico a₀ (a₀ + r), meanZeroWave η₁ I a₀ r α y = 0) ∧ ∫ (y : ℝ), meanZeroWave η₁ I a₀ r α y = 0 ∧ (∀ (y : ℝ), ‖meanZeroWave η₁ I a₀ r α y‖ ≤ 2) ∧ ∀ (y : ℝ), ‖deriv (deriv (meanZeroWave η₁ I a₀ r α)) y‖ ≤ 2 * K * (1 / r + 6 * Real.pi * |α|) ^ 2

The mean-zero wave Π(η e(α ·)) is a smooth mean-zero bump in the cell with ‖θ‖ ≤ 2 and ‖θ''‖ ≤ 2K (1/r + 6π|α|)².

noncomputable def TrilinearHT.Auto.slotPairKernel (w : ℝ × ℝ → ℂ) (a b : Fin 4) (ya yb : ℝ) : ℂ

The local kernel in the coordinates (y_a, y_b) = (x + a t, x + b t) of two distinct slots: t = (y_b - y_a)/(b - a) and x = y_a - a t.

Equations

• TrilinearHT.Auto.slotPairKernel w a b ya yb = w (ya - ↑↑a * ((yb - ya) / (↑↑b - ↑↑a)), (yb - ya) / (↑↑b - ↑↑a))

theorem TrilinearHT.Auto.fin_cast_sub_ne {a b : Fin 4} (hab : a ≠ b) : ↑↑b - ↑↑a ≠ 0

theorem TrilinearHT.Auto.slotPairKernel_progression (w : ℝ × ℝ → ℂ) {a b : Fin 4} (hab : a ≠ b) (z : ℝ × ℝ) : slotPairKernel w a b (realProgressionCoordinate a z) (realProgressionCoordinate b z) = w z

theorem TrilinearHT.Auto.slotPairKernel_marginal {κ : LocalKernelClass} {a₀ r : ℝ} {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {a b : Fin 4} (hab : a ≠ b) (u : ℝ) : ∫ (s : ℝ), slotPairKernel w a b s u = 0 ∧ ∫ (s : ℝ), slotPairKernel w a b u s = 0

eq:marginals in the coordinates (y_a, y_b): integration in either variable vanishes.

noncomputable def TrilinearHT.Auto.slotPairFreqA (a b : Fin 4) (r : ℝ) (v : Fin 2 → ℤ) : ℝ

The y_a frequency of the v-th kernel character in slot coordinates.

Equations

• TrilinearHT.Auto.slotPairFreqA a b r v = (↑(v 0) * ↑↑b - ↑(v 1)) / (16 * r * (↑↑b - ↑↑a))

noncomputable def TrilinearHT.Auto.slotPairFreqB (a b : Fin 4) (r : ℝ) (v : Fin 2 → ℤ) : ℝ

The y_b frequency of the v-th kernel character in slot coordinates.

Equations

• TrilinearHT.Auto.slotPairFreqB a b r v = (↑(v 1) - ↑(v 0) * ↑↑a) / (16 * r * (↑↑b - ↑↑a))

noncomputable def TrilinearHT.Auto.slotPairPhase (a₀ r : ℝ) (v : Fin 2 → ℤ) : ℝ

The constant phase of the v-th kernel character.

Equations

• TrilinearHT.Auto.slotPairPhase a₀ r v = -(↑(v 0) * (a₀ + r / 2)) / (16 * r)

theorem TrilinearHT.Auto.slotPairKernel_support {κ : LocalKernelClass} {a₀ r : ℝ} {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {a b : Fin 4} (hab : a ≠ b) {ya yb : ℝ} (h : slotPairKernel w a b ya yb ≠ 0) : a₀ + κ.margin * r ≤ ya ∧ ya ≤ a₀ + r - κ.margin * r ∧ a₀ + κ.margin * r ≤ yb ∧ yb ≤ a₀ + r - κ.margin * r

theorem TrilinearHT.Auto.slotPairKernel_plateau_expansion {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {a b : Fin 4} (hab : a ≠ b) {η₁ : ℝ → ℝ} {m : ℝ} (hm : 0 < m) (hmκ : m ≤ κ.margin) (hη1 : ∀ (u : ℝ), |u| ≤ 1 / 2 - m → η₁ u = 1) (hη0 : ∀ (u : ℝ), 1 / 2 - m / 2 ≤ |u| → η₁ u = 0) : have c := periodicFourierCoeff (cubePeriodization (kernelUnitRescale a₀ r w) 16); ∀ (ya yb : ℝ), HasSum (fun (v : Fin 2 → ℤ) => c v * ↑(Real.fourierChar (slotPairPhase a₀ r v)) * (plateauAt η₁ a₀ r ya * ↑(Real.fourierChar (slotPairFreqA a b r v * ya))) * (plateauAt η₁ a₀ r yb * ↑(Real.fourierChar (slotPairFreqB a b r v * yb)))) (slotPairKernel w a b ya yb)

Blueprint lem:predictors, proof line 1529: the kernel in slot coordinates is an absolutely convergent sum of plateau-cut characters η(y_a) e(α y_a) η(y_b) e(β y_b), valid on the whole plane.

theorem TrilinearHT.Auto.hasSum_integral_of_dominated {ι : Type u_1} [Countable ι] {f : ι → ℝ → ℂ} {g : ℝ → ℂ} (hf : ∀ (i : ι), MeasureTheory.Integrable (f i) MeasureTheory.volume) {a : ι → ℝ} (ha : Summable a) (hfa : ∀ (i : ι), ∫ (s : ℝ), ‖f i s‖ ≤ a i) (hg : ∀ (s : ℝ), HasSum (fun (i : ι) => f i s) (g s)) : HasSum (fun (i : ι) => ∫ (s : ℝ), f i s) (∫ (s : ℝ), g s)

Integrating an absolutely convergent expansion term by term.

theorem TrilinearHT.Auto.slotPairKernel_meanZero_tensor {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {a b : Fin 4} (hab : a ≠ b) {η₁ : ℝ → ℝ} {m I : ℝ} (hm : 0 < m) (hmκ : m ≤ κ.margin) (hη : ContDiff ℝ (↑⊤) η₁) (hη01 : ∀ (u : ℝ), 0 ≤ η₁ u ∧ η₁ u ≤ 1) (hη1 : ∀ (u : ℝ), |u| ≤ 1 / 2 - m → η₁ u = 1) (hη0 : ∀ (u : ℝ), 1 / 2 - m / 2 ≤ |u| → η₁ u = 0) (hI : 0 < I) (hIη : ∫ (u : ℝ), η₁ u = I) : have c := periodicFourierCoeff (cubePeriodization (kernelUnitRescale a₀ r w) 16); ∀ (ya yb : ℝ), HasSum (fun (v : Fin 2 → ℤ) => c v * ↑(Real.fourierChar (slotPairPhase a₀ r v)) * meanZeroWave η₁ I a₀ r (slotPairFreqA a b r v) ya * meanZeroWave η₁ I a₀ r (slotPairFreqB a b r v) yb) (slotPairKernel w a b ya yb)

Blueprint lem:predictors, proof line 1529: the kernel in slot coordinates is an absolutely convergent sum of tensor products of smooth mean-zero bumps Π(η e(α ·)) ⊗ Π(η e(β ·)), with the same coefficient magnitudes as the kernel.

structure TrilinearHT.Auto.UnitPlateau (m : ℝ) : Type

Unit-scale plateau data with margin m.

• η : ℝ → ℝ

  Smooth plateau function on the unit-scale interval.

• K : ℝ

  Uniform Lipschitz bound for the plateau function.

• I : ℝ

  Integral used to normalize the plateau function.

• smooth : ContDiff ℝ (↑⊤) self.η
• bounds (u : ℝ) : 0 ≤ self.η u ∧ self.η u ≤ 1
• one (u : ℝ) : |u| ≤ 1 / 2 - m → self.η u = 1
• zero (u : ℝ) : 1 / 2 - m / 2 ≤ |u| → self.η u = 0
• I_pos : 0 < self.I
• integral : ∫ (u : ℝ), self.η u = self.I
• K_nonneg : 0 ≤ self.K
• deriv_bound (u : ℝ) (i : ℕ) : i ≤ 2 → ‖iteratedFDeriv ℝ i self.η u‖ ≤ self.K

noncomputable def TrilinearHT.Auto.kernelPlateauMargin (κ : LocalKernelClass) : ℝ

The plateau margin of a kernel class.

Equations

• TrilinearHT.Auto.kernelPlateauMargin κ = min κ.margin (1 / 4)

theorem TrilinearHT.Auto.kernelPlateauMargin_pos (κ : LocalKernelClass) : 0 < kernelPlateauMargin κ

theorem TrilinearHT.Auto.kernelPlateauMargin_le (κ : LocalKernelClass) : kernelPlateauMargin κ ≤ κ.margin

noncomputable def TrilinearHT.Auto.kernelPlateau (κ : LocalKernelClass) : UnitPlateau (kernelPlateauMargin κ)

A fixed plateau for each kernel class.

Equations

• TrilinearHT.Auto.kernelPlateau κ = Classical.choice ⋯

noncomputable def TrilinearHT.Auto.classWave (κ : LocalKernelClass) (a₀ r α y : ℝ) : ℂ

The mean-zero wave of the kernel class at a cell.

Equations

• TrilinearHT.Auto.classWave κ a₀ r α y = TrilinearHT.Auto.meanZeroWave (TrilinearHT.Auto.kernelPlateau κ).η (TrilinearHT.Auto.kernelPlateau κ).I a₀ r α y

theorem TrilinearHT.Auto.classWave_props (κ : LocalKernelClass) {a₀ r : ℝ} (hr : 0 < r) (α : ℝ) : ContDiff ℝ (↑⊤) (classWave κ a₀ r α) ∧ (∀ y ∉ Set.Ico a₀ (a₀ + r), classWave κ a₀ r α y = 0) ∧ ∫ (y : ℝ), classWave κ a₀ r α y = 0 ∧ (∀ (y : ℝ), ‖classWave κ a₀ r α y‖ ≤ 2) ∧ ∀ (y : ℝ), ‖deriv (deriv (classWave κ a₀ r α)) y‖ ≤ 2 * (kernelPlateau κ).K * (1 / r + 6 * Real.pi * |α|) ^ 2

theorem TrilinearHT.Auto.slotPairKernel_classTensor {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {a b : Fin 4} (hab : a ≠ b) : have c := periodicFourierCoeff (cubePeriodization (kernelUnitRescale a₀ r w) 16); ∀ (ya yb : ℝ), HasSum (fun (v : Fin 2 → ℤ) => c v * ↑(Real.fourierChar (slotPairPhase a₀ r v)) * classWave κ a₀ r (slotPairFreqA a b r v) ya * classWave κ a₀ r (slotPairFreqB a b r v) yb) (slotPairKernel w a b ya yb)

theorem TrilinearHT.Auto.hasSum_integral_of_dominated' {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [Countable ι] {f : ι → α → ℂ} {g : α → ℂ} (hf : ∀ (i : ι), MeasureTheory.Integrable (f i) μ) {a : ι → ℝ} (ha : Summable a) (hfa : ∀ (i : ι), ∫ (s : α), ‖f i s‖ ∂μ ≤ a i) (hg : ∀ (s : α), HasSum (fun (i : ι) => f i s) (g s)) : HasSum (fun (i : ι) => ∫ (s : α), f i s ∂μ) (∫ (s : α), g s ∂μ)

Integrating an absolutely convergent expansion term by term (general measure space).

theorem TrilinearHT.Auto.separated_linear_cell_tensor {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {a b : Fin 4} (hab : a ≠ b) (γ : ℝ) {Ga Gb : ℝ → ℂ} (hGam : Measurable Ga) (hGbm : Measurable Gb) (hGa : MeasureTheory.Integrable Ga MeasureTheory.volume) (hGb : MeasureTheory.Integrable Gb MeasureTheory.volume) : have c := periodicFourierCoeff (cubePeriodization (kernelUnitRescale a₀ r w) 16); have ν := γ / (↑↑b - ↑↑a); have X := fun (v : Fin 2 → ℤ) => ∫ (y : ℝ), classWave κ a₀ r (slotPairFreqA a b r v) y * ↑(Real.fourierChar (-ν * y)) * Ga y; have Y := fun (v : Fin 2 → ℤ) => ∫ (y : ℝ), classWave κ a₀ r (slotPairFreqB a b r v) y * ↑(Real.fourierChar (ν * y)) * Gb y; (Summable fun (v : Fin 2 → ℤ) => ‖c v‖ * (√r⁻¹ * ‖X v‖) * (√r⁻¹ * ‖Y v‖)) ∧ r * ‖separatedLocalForm r w (fun (t : ℝ) => ↑(Real.fourierChar (γ * t))) a b Ga Gb‖ ≤ |(↑↑b - ↑↑a)⁻¹| * ∑' (v : Fin 2 → ℤ), ‖c v‖ * (√r⁻¹ * ‖X v‖) * (√r⁻¹ * ‖Y v‖)

Blueprint lem:predictors, proof line 1531: for a linear phase e(γ t) the separated form at one cell is a sum over the kernel characters of products of two mean-zero rows, |I| |H_I| ≤ |b-a|⁻¹ Σ_v |c_v| |W^a_v| |W^b_v|, with centers ∓γ/(b-a).

structure TrilinearHT.Auto.CellRowFamily (G : RealDyadicGrid) (ι : Type) : Type

A finite family of local rows g ↦ ∫ conj(τ_i) g over dyadic cells of a grid, each supported in its decision cell, with a joint Bessel bound on L²(ℝ).

• index : Finset ι

  Finite set of row indices used in the cell family.

• cell : ι → ℤ × ℤ

  Dyadic support cell assigned to each row.

• test : ι → ℝ → ℂ

  Measurable scalar test function assigned to each row.

• measurable (i : ι) : Measurable (self.test i)
• bounded (i : ι) : ∃ (C : ℝ), ∀ (y : ℝ), ‖self.test i y‖ ≤ C
• local_support (i : ι) (y : ℝ) : y ∉ dyadicGridCell G (self.cell i).1 (self.cell i).2 → self.test i y = 0
• bound : ℝ

  Bessel bound controlling the square sum of the row coefficients.

• bound_nonneg : 0 ≤ self.bound
• bessel (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ∑ i ∈ self.index, ‖∫ (y : ℝ), (starRingEnd ℂ) (self.test i y) * ↑↑g y‖ ^ 2 ≤ self.bound ^ 2 * ‖g‖ ^ 2

def TrilinearHT.Auto.IsAdmissibleOpponent (G : RealDyadicGrid) (J : ℤ × ℤ) (F : ℝ → ℂ) (z : ℤ × ℤ → ℝ → ℂ) (K : ℝ) : Prop

Blueprint sec:base, lines 1482–1485: a cell-dependent opponent z_I for the input F on the subtree rooted at J is admissible with transfer constant K if every local Bessel row family over cells of J applied to the inputs z_I is controlled by K times its bound times ‖1_J F‖₂.

Equations

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

theorem TrilinearHT.Auto.Lp_norm_sq_toLp_indicator {s : Set ℝ} (hs : MeasurableSet s) {F : ℝ → ℂ} (hF : MeasureTheory.MemLp (s.indicator F) 2 MeasureTheory.volume) : ‖MeasureTheory.MemLp.toLp (s.indicator F) hF‖ ^ 2 = ∫ (y : ℝ) in s, ‖F y‖ ^ 2

theorem TrilinearHT.Auto.integral_conj_test_eq_indicator {G : RealDyadicGrid} {ι : Type} (R : CellRowFamily G ι) {s : Set ℝ} (i : ι) (hsub : dyadicGridCell G (R.cell i).1 (R.cell i).2 ⊆ s) (F : ℝ → ℂ) : ∫ (y : ℝ), (starRingEnd ℂ) (R.test i y) * F y = ∫ (y : ℝ), (starRingEnd ℂ) (R.test i y) * s.indicator F y

theorem TrilinearHT.Auto.isAdmissibleOpponent_fixed (G : RealDyadicGrid) (J : ℤ × ℤ) {F : ℝ → ℂ} (hF : MeasureTheory.MemLp ((dyadicGridCell G J.1 J.2).indicator F) 2 MeasureTheory.volume) : IsAdmissibleOpponent G J F (fun (x : ℤ × ℤ) => F) 1

Blueprint sec:base, line 1482: a fixed square-integrable input is an admissible opponent with transfer constant one.

theorem TrilinearHT.Auto.isAdmissibleOpponent_squareEnergy (G : RealDyadicGrid) (J : ℤ × ℤ) {F : ℝ → ℂ} (Z : ℤ × ℤ → ℝ → ℂ) {L : ℝ} (hZ : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp ((dyadicGridCell G I.1 I.2).indicator (Z I)) 2 MeasureTheory.volume) (henergy : ∀ (S : Finset (ℤ × ℤ)), (∀ I ∈ S, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G J.1 J.2) → ∑ I ∈ S, ∫ (y : ℝ) in dyadicGridCell G I.1 I.2, ‖Z I y‖ ^ 2 ≤ L ^ 2 * ∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖F y‖ ^ 2) : IsAdmissibleOpponent G J F Z L

Blueprint sec:base, lines 1482–1484: a sequence Z_I with square energy Σ_I ∫_I |Z_I|² ≤ L² ‖1_J F‖² over every finite collection of cells of J is an admissible opponent with transfer constant L.

theorem TrilinearHT.Auto.separatedLocalForm_indicator {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) (Q : ℝ → ℂ) (a b : Fin 4) (Fa Fb : ℝ → ℂ) : separatedLocalForm r w Q a b Fa Fb = separatedLocalForm r w Q a b ((Set.Ico a₀ (a₀ + r)).indicator Fa) ((Set.Ico a₀ (a₀ + r)).indicator Fb)

The separated form only sees its inputs on the cell.

noncomputable def TrilinearHT.Auto.kernelPointEnvelope (κ : LocalKernelClass) (p : ℕ) : ℝ

The pointwise weighted envelope of admissible-kernel Fourier coefficients.

Equations

• TrilinearHT.Auto.kernelPointEnvelope κ p = max (TrilinearHT.Auto.kernelUnitEnvelope κ 0) (TrilinearHT.Auto.kernelUnitEnvelope κ (p + 2 + 1) * √↑2 ^ (p + 2 + 1) * 2 ^ p)

theorem TrilinearHT.Auto.admissibleKernel_coeff_envelope {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) (p : ℕ) (v : Fin 2 → ℤ) : ‖periodicFourierCoeff (cubePeriodization (kernelUnitRescale a₀ r w) 16) v‖ * (1 + frequencyLength v) ^ p ≤ kernelPointEnvelope κ p

theorem TrilinearHT.Auto.summable_frequency_weight_three : Summable fun (v : Fin 2 → ℤ) => ((1 + frequencyLength v) ^ 3)⁻¹

Absolute summability of the frequency weight (1 + |v|)⁻³ on ℤ².

noncomputable def TrilinearHT.Auto.waveRowTest (G : RealDyadicGrid) (κ : LocalKernelClass) {ι : Type u_1} (cell : ι → ℤ × ℤ) (α ν : ι → ℝ) (ψ : ℝ → ℂ) (I : ι) (y : ℝ) : ℂ

The normalized mean-zero wave rows g ↦ |I|^{-1/2} ∫_I ω_I e(ν_I y) ψ g of blueprint lem:predictors, proof lines 1534–1538, written as ∫ conj(test) g.

Equations

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

theorem TrilinearHT.Auto.integral_conj_waveRowTest (G : RealDyadicGrid) (κ : LocalKernelClass) {ι : Type u_1} (cell : ι → ℤ × ℤ) (α ν : ι → ℝ) (ψ : ℝ → ℂ) (I : ι) (g : ℝ → ℂ) : ∫ (y : ℝ), (starRingEnd ℂ) (waveRowTest G κ cell α ν ψ I y) * g y = ↑√(dyadicGridLength G (cell I).1)⁻¹ * ∫ (y : ℝ), classWave κ (dyadicGridLeft G (cell I).1 (cell I).2) (dyadicGridLength G (cell I).1) (α I) y * ↑(Real.fourierChar (ν I * y)) * ψ y * g y

theorem TrilinearHT.Auto.classWave_deriv2_le (κ : LocalKernelClass) {a₀ r : ℝ} (hr : 0 < r) (α : ℝ) {A : ℝ} (hA : 2 * (kernelPlateau κ).K * (1 + 6 * Real.pi * (r * |α|)) ^ 2 ≤ A) (y : ℝ) : ‖deriv (deriv (classWave κ a₀ r α)) y‖ ≤ A / r ^ 2

The bound for the second derivative of a class wave in the normalized form A / r².

theorem TrilinearHT.Auto.waveRow_bessel (G : RealDyadicGrid) (κ : LocalKernelClass) {ι : Type u_1} (cell : ι → ℤ × ℤ) (S : Finset ι) (α ν : ι → ℝ) (hinj : Set.InjOn (fun (I : ι) => (cell I, ν I)) ↑S) {ψ : ℝ → ℂ} (hψm : Measurable ψ) {B : ℝ} (hψ : ∀ (y : ℝ), ‖ψ y‖ ≤ B) {A : ℝ} (hA2 : 2 ≤ A) (hA : ∀ I ∈ S, 2 * (kernelPlateau κ).K * (1 + 6 * Real.pi * (dyadicGridLength G (cell I).1 * |α I|)) ^ 2 ≤ A) {M : ℝ} (hM : ∀ (ξ : ℝ), ∑ p ∈ Finset.image (fun (I : ι) => ((cell I).1, ν I)) S, bumpMultiplier (dyadicGridLength G p.1 * (ξ - p.2)) ≤ M) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ∑ I ∈ S, ‖∫ (y : ℝ), (starRingEnd ℂ) (waveRowTest G κ cell α ν ψ I y) * ↑↑g y‖ ^ 2 ≤ 2 * A ^ 2 * M * B ^ 2 * ‖g‖ ^ 2

Blueprint lem:predictors, proof lines 1538–1541: the mean-zero wave rows over a finite set of grid cells are jointly Bessel, with squared bound 2 A² M B², where M bounds the frequency multiplicity of the (scale, center) pairs, A the wave derivative constant and B the multiplier ψ.

theorem TrilinearHT.Auto.measurable_waveRowTest (G : RealDyadicGrid) (κ : LocalKernelClass) {ι : Type u_1} (cell : ι → ℤ × ℤ) (α ν : ι → ℝ) {ψ : ℝ → ℂ} (hψm : Measurable ψ) (I : ι) : Measurable (waveRowTest G κ cell α ν ψ I)

theorem TrilinearHT.Auto.norm_waveRowTest_le (G : RealDyadicGrid) (κ : LocalKernelClass) {ι : Type u_1} (cell : ι → ℤ × ℤ) (α ν : ι → ℝ) {ψ : ℝ → ℂ} {B : ℝ} (hψ : ∀ (y : ℝ), ‖ψ y‖ ≤ B) (I : ι) (y : ℝ) : ‖waveRowTest G κ cell α ν ψ I y‖ ≤ √(dyadicGridLength G (cell I).1)⁻¹ * (2 * B)

theorem TrilinearHT.Auto.waveRowTest_local (G : RealDyadicGrid) (κ : LocalKernelClass) {ι : Type u_1} (cell : ι → ℤ × ℤ) (α ν : ι → ℝ) (ψ : ℝ → ℂ) (I : ι) (y : ℝ) (hy : y ∉ dyadicGridCell G (cell I).1 (cell I).2) : waveRowTest G κ cell α ν ψ I y = 0

noncomputable def TrilinearHT.Auto.waveRowFamily (G : RealDyadicGrid) (κ : LocalKernelClass) {ι : Type} (cell : ι → ℤ × ℤ) (S : Finset ι) (α ν : ι → ℝ) (hinj : Set.InjOn (fun (I : ι) => (cell I, ν I)) ↑S) {ψ : ℝ → ℂ} (hψm : Measurable ψ) {B : ℝ} (hψ : ∀ (y : ℝ), ‖ψ y‖ ≤ B) {A : ℝ} (hA2 : 2 ≤ A) (hA : ∀ I ∈ S, 2 * (kernelPlateau κ).K * (1 + 6 * Real.pi * (dyadicGridLength G (cell I).1 * |α I|)) ^ 2 ≤ A) {M : ℝ} (hM : ∀ (ξ : ℝ), ∑ p ∈ Finset.image (fun (I : ι) => ((cell I).1, ν I)) S, bumpMultiplier (dyadicGridLength G p.1 * (ξ - p.2)) ≤ M) : CellRowFamily G ι

The mean-zero wave rows as a local Bessel row family.

Equations

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

theorem TrilinearHT.Auto.slotPairFreqA_le {a b : Fin 4} (hab : a ≠ b) {r : ℝ} (hr : 0 < r) (v : Fin 2 → ℤ) : r * |slotPairFreqA a b r v| ≤ frequencyLength v / 4

The slot frequencies of a kernel character are at most |v|/4 at unit scale.

theorem TrilinearHT.Auto.slotPairFreqB_le {a b : Fin 4} (hab : a ≠ b) {r : ℝ} (hr : 0 < r) (v : Fin 2 → ℤ) : r * |slotPairFreqB a b r v| ≤ frequencyLength v / 4

noncomputable def TrilinearHT.Auto.charWaveConst (κ : LocalKernelClass) (L : ℝ) : ℝ

The wave derivative constant for a kernel character of length L.

Equations

• TrilinearHT.Auto.charWaveConst κ L = (2 + 2 * (TrilinearHT.Auto.kernelPlateau κ).K) * 25 * (1 + L) ^ 2

theorem TrilinearHT.Auto.two_le_charWaveConst (κ : LocalKernelClass) {L : ℝ} (hL : 0 ≤ L) : 2 ≤ charWaveConst κ L

theorem TrilinearHT.Auto.charWaveConst_ge (κ : LocalKernelClass) {L β : ℝ} (hβ : 0 ≤ β) (hβL : β ≤ L / 4) : 2 * (kernelPlateau κ).K * (1 + 6 * Real.pi * β) ^ 2 ≤ charWaveConst κ L

theorem TrilinearHT.Auto.bumpMultiplier_neg (η : ℝ) : bumpMultiplier (-η) = bumpMultiplier η

theorem TrilinearHT.Auto.multiplicity_neg (G : RealDyadicGrid) {ι : Type u_1} (cell : ι → ℤ × ℤ) (S : Finset ι) (ν : ι → ℝ) {M : ℝ} (hM : ∀ (ξ : ℝ), ∑ p ∈ Finset.image (fun (I : ι) => ((cell I).1, ν I)) S, bumpMultiplier (dyadicGridLength G p.1 * (ξ - p.2)) ≤ M) (ξ : ℝ) : ∑ p ∈ Finset.image (fun (I : ι) => ((cell I).1, -ν I)) S, bumpMultiplier (dyadicGridLength G p.1 * (ξ - p.2)) ≤ M

Negating all centers preserves the frequency multiplicity bound.

theorem TrilinearHT.Auto.integral_classWave_indicator (κ : LocalKernelClass) {a₀ r : ℝ} (hr : 0 < r) (α : ℝ) (E g : ℝ → ℂ) : ∫ (y : ℝ), classWave κ a₀ r α y * E y * (Set.Ico a₀ (a₀ + r)).indicator g y = ∫ (y : ℝ), classWave κ a₀ r α y * E y * g y

A mean-zero wave annihilates the outside of its cell, so a cell indicator on the input may be dropped.

noncomputable def TrilinearHT.Auto.linearScaleConst (κ : LocalKernelClass) : ℝ

The constant of the linear-phase scale sum.

Equations

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

theorem TrilinearHT.Auto.integrable_cell_mul {s : Set ℝ} (hs : MeasurableSet s) {ψ z : ℝ → ℂ} (hψm : Measurable ψ) (hψ : ∀ (y : ℝ), ‖ψ y‖ ≤ 1) (hzm : Measurable z) (hz : MeasureTheory.IntegrableOn z s MeasureTheory.volume) : MeasureTheory.Integrable (s.indicator fun (y : ℝ) => ψ y * z y) MeasureTheory.volume

theorem TrilinearHT.Auto.linear_phase_scale_sum_rows (G : RealDyadicGrid) (κ : LocalKernelClass) {ι : Type} (cell : ι → ℤ × ℤ) (S : Finset ι) (w : ι → ℝ × ℝ → ℂ) (hw : ∀ I ∈ S, IsAdmissibleLocalKernel κ (dyadicGridLeft G (cell I).1 (cell I).2) (dyadicGridLength G (cell I).1) (w I)) {a b : Fin 4} (hab : a ≠ b) (γ : ι → ℝ) {ψa ψb : ℝ → ℂ} (hψam : Measurable ψa) (hψbm : Measurable ψb) (hψa : ∀ (y : ℝ), ‖ψa y‖ ≤ 1) (hψb : ∀ (y : ℝ), ‖ψb y‖ ≤ 1) {za zb : ℤ × ℤ → ℝ → ℂ} {Ka Kb Na Nb : ℝ} (hKa : 0 ≤ Ka) (hKb : 0 ≤ Kb) (hNa0 : 0 ≤ Na) (hNb0 : 0 ≤ Nb) (hzam : ∀ (I : ℤ × ℤ), Measurable (za I)) (hzbm : ∀ (I : ℤ × ℤ), Measurable (zb I)) (hzai : ∀ I ∈ S, MeasureTheory.IntegrableOn (za (cell I)) (dyadicGridCell G (cell I).1 (cell I).2) MeasureTheory.volume) (hzbi : ∀ I ∈ S, MeasureTheory.IntegrableOn (zb (cell I)) (dyadicGridCell G (cell I).1 (cell I).2) MeasureTheory.volume) {M : ℝ} (hM : ∀ (ξ : ℝ), ∑ p ∈ Finset.image (fun (I : ι) => ((cell I).1, γ I / (↑↑b - ↑↑a))) S, bumpMultiplier (dyadicGridLength G p.1 * (ξ - p.2)) ≤ M) (hxrow : ∀ (v : Fin 2 → ℤ), ∑ I ∈ S, ‖∫ (y : ℝ), (starRingEnd ℂ) (waveRowTest G κ cell (fun (I : ι) => slotPairFreqA a b (dyadicGridLength G (cell I).1) v) (fun (I : ι) => -(γ I / (↑↑b - ↑↑a))) ψa I y) * za (cell I) y‖ ^ 2 ≤ Ka ^ 2 * (charWaveConst κ (frequencyLength v) * 1 * √(2 * M)) ^ 2 * Na ^ 2) (hyrow : ∀ (v : Fin 2 → ℤ), ∑ I ∈ S, ‖∫ (y : ℝ), (starRingEnd ℂ) (waveRowTest G κ cell (fun (I : ι) => slotPairFreqB a b (dyadicGridLength G (cell I).1) v) (fun (I : ι) => γ I / (↑↑b - ↑↑a)) ψb I y) * zb (cell I) y‖ ^ 2 ≤ Kb ^ 2 * (charWaveConst κ (frequencyLength v) * 1 * √(2 * M)) ^ 2 * Nb ^ 2) : ∑ I ∈ S, dyadicGridLength G (cell I).1 * ‖separatedLocalForm (dyadicGridLength G (cell I).1) (w I) (fun (t : ℝ) => ↑(Real.fourierChar (γ I * t))) a b (fun (y : ℝ) => ψa y * za (cell I) y) fun (y : ℝ) => ψb y * zb (cell I) y‖ ≤ linearScaleConst κ * M * Ka * Kb * Na * Nb

The row form of linear_phase_scale_sum: the same bound holds whenever the two families of mean-zero wave rows of the inputs obey the square-sum bounds that admissibility would give, with arbitrary input sizes Na, Nb (blueprint lem:delay, line 1559, pairs delayed rows with the opposing Bessel rows).

theorem TrilinearHT.Auto.linear_phase_scale_sum (G : RealDyadicGrid) (κ : LocalKernelClass) (J : ℤ × ℤ) {ι : Type} (cell : ι → ℤ × ℤ) (S : Finset ι) (hSJ : ∀ I ∈ S, dyadicGridCell G (cell I).1 (cell I).2 ⊆ dyadicGridCell G J.1 J.2) (w : ι → ℝ × ℝ → ℂ) (hw : ∀ I ∈ S, IsAdmissibleLocalKernel κ (dyadicGridLeft G (cell I).1 (cell I).2) (dyadicGridLength G (cell I).1) (w I)) {a b : Fin 4} (hab : a ≠ b) (γ : ι → ℝ) (hinj : Set.InjOn (fun (I : ι) => (cell I, γ I / (↑↑b - ↑↑a))) ↑S) {ψa ψb : ℝ → ℂ} (hψam : Measurable ψa) (hψbm : Measurable ψb) (hψa : ∀ (y : ℝ), ‖ψa y‖ ≤ 1) (hψb : ∀ (y : ℝ), ‖ψb y‖ ≤ 1) {Fa Fb : ℝ → ℂ} {za zb : ℤ × ℤ → ℝ → ℂ} {Ka Kb : ℝ} (hKa : 0 ≤ Ka) (hKb : 0 ≤ Kb) (hza : IsAdmissibleOpponent G J Fa za Ka) (hzb : IsAdmissibleOpponent G J Fb zb Kb) (hzam : ∀ (I : ℤ × ℤ), Measurable (za I)) (hzbm : ∀ (I : ℤ × ℤ), Measurable (zb I)) (hzai : ∀ I ∈ S, MeasureTheory.IntegrableOn (za (cell I)) (dyadicGridCell G (cell I).1 (cell I).2) MeasureTheory.volume) (hzbi : ∀ I ∈ S, MeasureTheory.IntegrableOn (zb (cell I)) (dyadicGridCell G (cell I).1 (cell I).2) MeasureTheory.volume) {M : ℝ} (hM : ∀ (ξ : ℝ), ∑ p ∈ Finset.image (fun (I : ι) => ((cell I).1, γ I / (↑↑b - ↑↑a))) S, bumpMultiplier (dyadicGridLength G p.1 * (ξ - p.2)) ≤ M) : ∑ I ∈ S, dyadicGridLength G (cell I).1 * ‖separatedLocalForm (dyadicGridLength G (cell I).1) (w I) (fun (t : ℝ) => ↑(Real.fourierChar (γ I * t))) a b (fun (y : ℝ) => ψa y * za (cell I) y) fun (y : ℝ) => ψb y * zb (cell I) y‖ ≤ linearScaleConst κ * M * Ka * Kb * √(∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖Fa y‖ ^ 2) * √(∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖Fb y‖ ^ 2)

Blueprint lem:predictors, proof lines 1534–1542: for linear phases e(γ_I t) the length-weighted scale sum of the separated forms against admissible opponents is bounded by the frequency multiplicity M of the (scale, center) pairs times the transfer constants and the input norms on J.

theorem TrilinearHT.Auto.card_le_of_one_separated {ι : Type u_1} (s : Finset ι) (t : ι → ℝ) {β : ℝ} (hβ : 0 ≤ β) (hs : ∀ i ∈ s, |t i| ≤ β) (hsep : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → 1 ≤ |t i - t j|) : ↑s.card ≤ 2 * β + 2

A 1-separated finite set of real numbers in [-β, β] has at most 2β + 2 points.

noncomputable def TrilinearHT.Auto.heightBandConst (d : ℕ) (B : ℝ) : ℝ

The scale-count constant of lem:height for one dyadic band of an extended parameter vector of dimension d + 1.

Equations

• TrilinearHT.Auto.heightBandConst d B = 32 * (↑(d + 1) + 1) ^ 4 * (Real.log (2 * B) + Real.log 4)

theorem TrilinearHT.Auto.rational_center_multiplicity {d : ℕ} (G : RealDyadicGrid) (χ : Fin d → ℝ) {B : ℝ} (hB : 2 ≤ B) (T : Finset (ℤ × ℝ)) (hrat : ∀ p ∈ T, ∃ (a : Fin d → ℚ), (∀ (j : Fin d), ↑(rationalHeight (a j)) ≤ B) ∧ p.2 = ∑ j : Fin d, ↑(a j) * χ j) (hsep : ∀ p ∈ T, ∀ q ∈ T, p.1 = q.1 → p ≠ q → 1 ≤ dyadicGridLength G p.1 * |p.2 - q.2|) (ξ : ℝ) : ∑ p ∈ T, bumpMultiplier (dyadicGridLength G p.1 * (ξ - p.2)) ≤ 24 * (2 * Real.pi) ^ 2 * (4 * heightBandConst d B)

Blueprint lem:predictors, proof lines 1539–1541: frequency multiplicity of bounded-height rational centers. If every center ν at scale s is a rational evaluation a · χ of height at most B of a fixed vector and the centers at one scale are 1/|I|-separated, then for every ξ the bump weights sum to at most a constant times the lem:height band count.

theorem TrilinearHT.Auto.setIntegral_norm_le_sqrt {s : Set ℝ} (hsv : MeasureTheory.volume s < ⊤) {f : ℝ → ℂ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict s)) : ∫ (y : ℝ) in s, ‖f y‖ ≤ √(MeasureTheory.volume.real s) * √(∫ (y : ℝ) in s, ‖f y‖ ^ 2)

Cauchy–Schwarz on a set of finite measure: ∫_s |f| ≤ |s|^{1/2} (∫_s |f|²)^{1/2}.

theorem TrilinearHT.Auto.admissibleKernel_time_le {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {z : ℝ × ℝ} (hz : w z ≠ 0) : |z.2| ≤ r

The cell of an admissible kernel bounds the time variable: |t| ≤ r on its support.

theorem TrilinearHT.Auto.separatedLocalForm_sup_le {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {a b : Fin 4} (hab : a ≠ b) {K : ℝ → ℂ} {η : ℝ} (hη : 0 ≤ η) (hK : ∀ (t : ℝ), |t| ≤ r → ‖K t‖ ≤ η) {Fa Fb : ℝ → ℂ} (hFam : Measurable Fa) (hFbm : Measurable Fb) (hFa : MeasureTheory.MemLp Fa 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) (hFb : MeasureTheory.MemLp Fb 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) : ‖separatedLocalForm r w K a b Fa Fb‖ ≤ localKernelSupBound κ * η * √(r⁻¹ * ∫ (y : ℝ) in Set.Ico a₀ (a₀ + r), ‖Fa y‖ ^ 2) * √(r⁻¹ * ∫ (y : ℝ) in Set.Ico a₀ (a₀ + r), ‖Fb y‖ ^ 2)

Blueprint lem:predictors, proof lines 1521–1523: an elementary bound for the separated form with a time modifier bounded by η on the allowed range, by the kernel supremum and the normalized L² norms of the two inputs on the cell.

def TrilinearHT.Auto.HasDepthEnergy (G : RealDyadicGrid) (J : ℤ × ℤ) (F : ℝ → ℂ) (z : ℤ × ℤ → ℝ → ℂ) (K : ℝ) : Prop

Blueprint sec:base, lines 1482–1485, the depth form of admissibility: on every family of cells of one depth inside J the opponent has square energy at most K² ‖1_J F‖² (contraction for fixed inputs and projections, the assumed energy for square-energy sequences).

Equations

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

theorem TrilinearHT.Auto.hasDepthEnergy_fixed (G : RealDyadicGrid) (J : ℤ × ℤ) {F : ℝ → ℂ} (hF : MeasureTheory.IntegrableOn (fun (y : ℝ) => ‖F y‖ ^ 2) (dyadicGridCell G J.1 J.2) MeasureTheory.volume) : HasDepthEnergy G J F (fun (x : ℤ × ℤ) => F) 1

A fixed input has depth energy with constant one, cells of one depth being disjoint.

theorem TrilinearHT.Auto.depth_weighted_energy_sum (G : RealDyadicGrid) (J : ℤ × ℤ) (S : Finset (ℤ × ℤ)) (hSJ : ∀ I ∈ S, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G J.1 J.2) (c : ℤ → ℝ) (hc : ∀ (s : ℤ), 0 ≤ c s) {Fa Fb : ℝ → ℂ} {za zb : ℤ × ℤ → ℝ → ℂ} {Ka Kb : ℝ} (hKa : 0 ≤ Ka) (hKb : 0 ≤ Kb) (hEa : HasDepthEnergy G J Fa za Ka) (hEb : HasDepthEnergy G J Fb zb Kb) : ∑ I ∈ S, c I.1 * (√(∫ (y : ℝ) in dyadicGridCell G I.1 I.2, ‖za I y‖ ^ 2) * √(∫ (y : ℝ) in dyadicGridCell G I.1 I.2, ‖zb I y‖ ^ 2)) ≤ (∑ s ∈ Finset.image Prod.fst S, c s) * Ka * Kb * √(∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖Fa y‖ ^ 2) * √(∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖Fb y‖ ^ 2)

Blueprint lem:predictors, proof line 1523 ("at each depth use contractions and Cauchy–Schwarz"): a depth-weighted sum of products of cell energies is bounded by the total depth weight times the opponent constants and input norms.

theorem TrilinearHT.Auto.cell_normalized_product {r X Y : ℝ} (hr : 0 < r) : r * (√(r⁻¹ * X) * √(r⁻¹ * Y)) = √X * √Y

The cell-normalized product of two L² norms at the cell length.

theorem TrilinearHT.Auto.separatedLocalForm_add {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {a b : Fin 4} (hab : a ≠ b) {Q₁ Q₂ : ℝ → ℂ} (hQ₁ : Measurable Q₁) (hQ₂ : Measurable Q₂) {C : ℝ} (hQ₁b : ∀ (t : ℝ), ‖Q₁ t‖ ≤ C) (hQ₂b : ∀ (t : ℝ), ‖Q₂ t‖ ≤ C) {Fa Fb : ℝ → ℂ} (hFam : Measurable Fa) (hFbm : Measurable Fb) (hFa : MeasureTheory.MemLp Fa 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) (hFb : MeasureTheory.MemLp Fb 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) : separatedLocalForm r w (fun (t : ℝ) => Q₁ t + Q₂ t) a b Fa Fb = separatedLocalForm r w Q₁ a b Fa Fb + separatedLocalForm r w Q₂ a b Fa Fb

The separated form is additive in the time factor for bounded measurable factors and cell-local L² inputs.

theorem TrilinearHT.Auto.integrableOn_cell_of_memLp (G : RealDyadicGrid) (I : ℤ × ℤ) {z : ℝ → ℂ} (h : MeasureTheory.MemLp z 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) : MeasureTheory.IntegrableOn z (dyadicGridCell G I.1 I.2) MeasureTheory.volume

theorem TrilinearHT.Auto.memLp_mul_bounded_restrict {s : Set ℝ} {ψ z : ℝ → ℂ} (hψm : Measurable ψ) (hψ : ∀ (y : ℝ), ‖ψ y‖ ≤ 1) (hz : MeasureTheory.MemLp z 2 (MeasureTheory.volume.restrict s)) : MeasureTheory.MemLp (fun (y : ℝ) => ψ y * z y) 2 (MeasureTheory.volume.restrict s)

theorem TrilinearHT.Auto.setIntegral_mul_bounded_le {s : Set ℝ} {ψ z : ℝ → ℂ} (hψ : ∀ (y : ℝ), ‖ψ y‖ ≤ 1) (hz : MeasureTheory.MemLp z 2 (MeasureTheory.volume.restrict s)) : ∫ (y : ℝ) in s, ‖ψ y * z y‖ ^ 2 ≤ ∫ (y : ℝ) in s, ‖z y‖ ^ 2

noncomputable def TrilinearHT.Auto.quadPhase (lam γ t : ℝ) : ℂ

The phase e(λ t² + γ t).

Equations

• TrilinearHT.Auto.quadPhase lam γ t = ↑(Real.fourierChar (lam * t ^ 2 + γ * t))

theorem TrilinearHT.Auto.quadPhase_split (lam γ t : ℝ) : quadPhase lam γ t = ↑(Real.fourierChar (γ * t)) + (↑(Real.fourierChar (lam * t ^ 2)) - 1) * ↑(Real.fourierChar (γ * t))

theorem TrilinearHT.Auto.single_phase_scale_sum (G : RealDyadicGrid) (κ : LocalKernelClass) (J : ℤ × ℤ) (S : Finset (ℤ × ℤ)) (hSJ : ∀ I ∈ S, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G J.1 J.2) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (hw : ∀ I ∈ S, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) {a b : Fin 4} (hab : a ≠ b) (lam γ : ℤ → ℝ) {ψa ψb : ℝ → ℂ} (hψam : Measurable ψa) (hψbm : Measurable ψb) (hψa : ∀ (y : ℝ), ‖ψa y‖ ≤ 1) (hψb : ∀ (y : ℝ), ‖ψb y‖ ≤ 1) {Fa Fb : ℝ → ℂ} {za zb : ℤ × ℤ → ℝ → ℂ} {Ka Kb : ℝ} (hKa : 0 ≤ Ka) (hKb : 0 ≤ Kb) (hza : IsAdmissibleOpponent G J Fa za Ka) (hzb : IsAdmissibleOpponent G J Fb zb Kb) (hEa : HasDepthEnergy G J Fa za Ka) (hEb : HasDepthEnergy G J Fb zb Kb) (hzam : ∀ (I : ℤ × ℤ), Measurable (za I)) (hzbm : ∀ (I : ℤ × ℤ), Measurable (zb I)) (hza2 : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (za I) 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) (hzb2 : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (zb I) 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) {M : ℝ} (hM : ∀ (ξ : ℝ), ∑ p ∈ Finset.image (fun (I : ℤ × ℤ) => (I.1, γ I.1 / (↑↑b - ↑↑a))) S, bumpMultiplier (dyadicGridLength G p.1 * (ξ - p.2)) ≤ M) {Λ : ℝ} (hΛ : ∑ s ∈ Finset.image Prod.fst S, 2 * Real.pi * |lam s| * dyadicGridLength G s ^ 2 ≤ Λ) : ∑ I ∈ S, dyadicGridLength G I.1 * ‖separatedLocalForm (dyadicGridLength G I.1) (w I) (quadPhase (lam I.1) (γ I.1)) a b (fun (y : ℝ) => ψa y * za I y) fun (y : ℝ) => ψb y * zb I y‖ ≤ (linearScaleConst κ * M + localKernelSupBound κ * Λ) * Ka * Kb * √(∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖Fa y‖ ^ 2) * √(∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖Fb y‖ ^ 2)

Blueprint lem:predictors, proof lines 1521–1523 and 1534–1542: the absolute scale sum of one phase family e(λ_s t² + γ_s t) (one phase per depth) against admissible opponents. The linear part costs the frequency multiplicity M of the centers γ_s/(b-a), the quadratic part the total size Λ ≥ Σ_s 2π |λ_s| r_s².

noncomputable def TrilinearHT.Auto.bandCutoff (u : ℝ) : ℝ

The fixed plateau used for the Fourier-supremum bands: the square of the Gevrey plateau of exists_plateau_cutoff, so it is nonnegative, equal to one on [-1, 1] and supported in [-2, 2] (blueprint lem:separation, line 1387).

Equations

• TrilinearHT.Auto.bandCutoff u = Classical.choose TrilinearHT.Auto.exists_plateau_cutoff u ^ 2

theorem TrilinearHT.Auto.bandCutoff_spec : ContDiff ℝ (↑⊤) bandCutoff ∧ (∀ (u : ℝ), 0 ≤ bandCutoff u) ∧ (∀ (u : ℝ), bandCutoff u ≤ 1) ∧ (∀ (u : ℝ), |u| ≤ 1 → bandCutoff u = 1) ∧ ∀ (u : ℝ), 2 ≤ |u| → bandCutoff u = 0

theorem TrilinearHT.Auto.bandCutoff_hasCompactSupport : HasCompactSupport bandCutoff

theorem TrilinearHT.Auto.bandCutoff_integrable : MeasureTheory.Integrable bandCutoff MeasureTheory.volume

theorem TrilinearHT.Auto.bandCutoff_lipschitz : ∃ (L : ℝ), 0 ≤ L ∧ ∀ (u v : ℝ), |bandCutoff v - bandCutoff u| ≤ L * |v - u|

theorem TrilinearHT.Auto.two_le_integral_bandCutoff : 2 ≤ ∫ (u : ℝ), bandCutoff u

theorem TrilinearHT.Auto.bandCutoff_fourier_decay : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (η : ℝ), η ≠ 0 → ‖∫ (u : ℝ), ↑(bandCutoff u) * ↑(Real.fourierChar (-(η * u)))‖ ≤ C / η ^ 2

Fourier decay of the band plateau: |ζ̂(η)| ≤ C η⁻².

noncomputable def TrilinearHT.Auto.bandAmplitude (Q : ℝ → ℂ) (r ξ : ℝ) : ℝ

The band amplitude |∫ Q(ru) ζ(u) e(-ξu) du| of a time factor at scale r.

Equations

• TrilinearHT.Auto.bandAmplitude Q r ξ = ‖∫ (u : ℝ), Q (r * u) * ↑(TrilinearHT.Auto.bandCutoff u) * ↑(Real.fourierChar (-(ξ * u)))‖

def TrilinearHT.Auto.InScaleBand (Q : ℝ → ℂ) (m : ℕ) (r : ℝ) : Prop

Blueprint lem:predictors, line 1490: the scale r lies in the m-th Fourier-supremum band, e^{-m-1} < A_r ≤ e^{-m}.

Equations

• TrilinearHT.Auto.InScaleBand Q m r = ((∀ (ξ : ℝ), TrilinearHT.Auto.bandAmplitude Q r ξ ≤ Real.exp (-↑m)) ∧ ∃ (ξ : ℝ), Real.exp (-(↑m + 1)) < TrilinearHT.Auto.bandAmplitude Q r ξ)

theorem TrilinearHT.Auto.separatedLocalForm_const_mul (r : ℝ) (w : ℝ × ℝ → ℂ) (c : ℂ) (Q : ℝ → ℂ) (a b : Fin 4) (Fa Fb : ℝ → ℂ) : separatedLocalForm r w (fun (t : ℝ) => c * Q t) a b Fa Fb = c * separatedLocalForm r w Q a b Fa Fb

theorem TrilinearHT.Auto.separatedLocalForm_hasSum {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {a b : Fin 4} (hab : a ≠ b) {τ : Type u_1} [Countable τ] (c : τ → ℂ) (φ : τ → ℝ → ℂ) (hφm : ∀ (p : τ), Measurable (φ p)) (hφ : ∀ (p : τ) (t : ℝ), ‖φ p t‖ ≤ 1) (hc : Summable fun (p : τ) => ‖c p‖) {Q : ℝ → ℂ} (hQ : ∀ (t : ℝ), |t| ≤ r → HasSum (fun (p : τ) => c p * φ p t) (Q t)) {Fa Fb : ℝ → ℂ} (hFam : Measurable Fa) (hFbm : Measurable Fb) (hFa : MeasureTheory.MemLp Fa 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) (hFb : MeasureTheory.MemLp Fb 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) : HasSum (fun (p : τ) => c p * separatedLocalForm r w (φ p) a b Fa Fb) (separatedLocalForm r w Q a b Fa Fb)

Termwise expansion of the separated form along an absolutely convergent expansion of the time factor by uniformly bounded measurable terms on the allowed range.

theorem TrilinearHT.Auto.exists_clump_representatives {ι : Type u_1} (P : Finset ι) (γ : ι → ℝ) {r ε L : ℝ} (hε : 0 ≤ ε) (h3 : 3 * ε < L) (hdich : ∀ p ∈ P, ∀ q ∈ P, r * |γ p - γ q| ≤ ε ∨ L ≤ r * |γ p - γ q|) (hr : 0 ≤ r) : ∃ (rep : ι → ι), (∀ p ∈ P, rep p ∈ P ∧ r * |γ p - γ (rep p)| ≤ ε) ∧ ∀ p ∈ P, ∀ q ∈ P, rep p ≠ rep q → L ≤ r * |γ (rep p) - γ (rep q)|

Blueprint lem:predictors, proof line 1525 (clumps): with a tiny/large dichotomy for the scaled differences of a finite catalog of frequencies, the catalog splits into clumps of scaled diameter at most ε with representatives separated by at least L.

theorem TrilinearHT.Auto.integral_bandCutoff_le_four : ∫ (u : ℝ), bandCutoff u ≤ 4

theorem TrilinearHT.Auto.bandCutoff_eq_zero_of_ne {u : ℝ} (hu : bandCutoff u ≠ 0) : |u| < 2

theorem TrilinearHT.Auto.clump_coefficient_le {Q : ℝ → ℂ} (hQm : Measurable Q) (hQb : ∀ (t : ℝ), ‖Q t‖ ≤ 1) {r : ℝ} (hr : 0 < r) (R : Finset ℝ) (bc : ℝ → ℂ) {L δ A Cζ : ℝ} (hL : 0 < L) (hCζ : ∀ (η : ℝ), η ≠ 0 → ‖∫ (u : ℝ), ↑(bandCutoff u) * ↑(Real.fourierChar (-(η * u)))‖ ≤ Cζ / η ^ 2) (hCζ0 : 0 ≤ Cζ) (hsep : ∀ c ∈ R, ∀ c' ∈ R, c ≠ c' → L ≤ r * |c - c'|) (herr : ∀ (t : ℝ), |t| ≤ 2 * r → ‖Q t - ∑ c ∈ R, bc c * ↑(Real.fourierChar (c * t))‖ ≤ δ) (hA : ∀ (ξ : ℝ), bandAmplitude Q r ξ ≤ A) {c : ℝ} (hc : c ∈ R) : ‖bc c‖ ≤ A / 2 + δ + (Cζ * ∑ c' ∈ R, ‖bc c'‖) / L ^ 2

Blueprint lem:predictors, proof line 1525: each combined clump coefficient is controlled by the band amplitude. Test the expansion against ζ(u) e(-r γ_C u); the clump's own coefficient is multiplied by ∫ ζ ≥ 2, separated clumps contribute Fourier tails of ζ, and the uniform approximation error on |t| ≤ 2r costs at most 4δ.

theorem TrilinearHT.Auto.norm_fourierChar_sub_le (x y : ℝ) : ‖↑(Real.fourierChar x) - ↑(Real.fourierChar y)‖ ≤ 2 * Real.pi * |x - y|

theorem TrilinearHT.Auto.norm_quadPhase (lam γ t : ℝ) : ‖quadPhase lam γ t‖ = 1

theorem TrilinearHT.Auto.measurable_quadPhase (lam γ : ℝ) : Measurable (quadPhase lam γ)

theorem TrilinearHT.Auto.clump_cell_bound {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {a b : Fin 4} (hab : a ≠ b) {τ : Type u_1} [Countable τ] [DecidableEq τ] (c : τ → ℂ) (hc : Summable fun (p : τ) => ‖c p‖) (lam : ℝ) (f : τ → ℝ) {Q : ℝ → ℂ} (hQ : ∀ (t : ℝ), |t| ≤ r → HasSum (fun (p : τ) => c p * quadPhase lam (f p) t) (Q t)) (P : Finset τ) (rep : τ → τ) {β : ℝ} (hβ : ∀ p ∈ P, r * |f p - f (rep p)| ≤ β) {Fa Fb : ℝ → ℂ} (hFam : Measurable Fa) (hFbm : Measurable Fb) (hFa : MeasureTheory.MemLp Fa 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) (hFb : MeasureTheory.MemLp Fb 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) : ‖separatedLocalForm r w Q a b Fa Fb‖ ≤ ∑ x ∈ Finset.image (fun (p : τ) => f (rep p)) P, ‖∑ p ∈ P with f (rep p) = x, c p‖ * ‖separatedLocalForm r w (fun (t : ℝ) => ↑(Real.fourierChar (x * t))) a b Fa Fb‖ + (∑ p ∈ P, ‖c p‖) * (localKernelSupBound κ * (2 * Real.pi * (|lam| * r ^ 2 + β)) * √(r⁻¹ * ∫ (y : ℝ) in Set.Ico a₀ (a₀ + r), ‖Fa y‖ ^ 2) * √(r⁻¹ * ∫ (y : ℝ) in Set.Ico a₀ (a₀ + r), ‖Fb y‖ ^ 2)) + ∑' (p : τ), if p ∈ P then 0 else ‖c p‖ * ‖separatedLocalForm r w (quadPhase lam (f p)) a b Fa Fb‖

Blueprint lem:predictors, proof line 1525, at one non-exceptional cell: after the chart expansion Q = Σ_p c_p e(λ t² + γ_p t) on the allowed range, the form splits into the clump terms with combined coefficients, the replacement errors (quadratic part and center shift inside a clump) and the tail outside the finite catalog P.

theorem TrilinearHT.Auto.kernelFourierConst_nonneg (κ : LocalKernelClass) : 0 ≤ kernelFourierConst κ

theorem TrilinearHT.Auto.kernelPointEnvelope_nonneg (κ : LocalKernelClass) (p : ℕ) : 0 ≤ kernelPointEnvelope κ p

theorem TrilinearHT.Auto.linearScaleConst_nonneg (κ : LocalKernelClass) : 0 ≤ linearScaleConst κ

theorem TrilinearHT.Auto.heightBandConst_nonneg (d : ℕ) {B : ℝ} (hB : 2 ≤ B) : 0 ≤ heightBandConst d B

theorem TrilinearHT.Auto.separated_form_le_band {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {a b : Fin 4} (hab : a ≠ b) {Q : ℝ → ℂ} (hQm : Measurable Q) (hQ1 : ∀ (t : ℝ), ‖Q t‖ ≤ 1) {M : ℝ} (hM : ∀ (ξ : ℝ), bandAmplitude Q r ξ ≤ M) {Fa Fb : ℝ → ℂ} (hFam : Measurable Fa) (hFbm : Measurable Fb) (hFa : MeasureTheory.MemLp Fa 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) (hFb : MeasureTheory.MemLp Fb 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) : ‖separatedLocalForm r w Q a b Fa Fb‖ ≤ kernelFourierConst κ * M * √(r⁻¹ * ∫ (y : ℝ) in Set.Ico a₀ (a₀ + r), ‖Fa y‖ ^ 2) * √(r⁻¹ * ∫ (y : ℝ) in Set.Ico a₀ (a₀ + r), ‖Fb y‖ ^ 2)

The single-scale bound of lem:separation on half-open cells with the band plateau.

theorem TrilinearHT.Auto.clump_coeff_sum_le {τ : Type u_1} (P : Finset τ) (coef : τ → ℂ) (g : τ → ℝ) : ∑ x ∈ Finset.image g P, ‖∑ p ∈ P with g p = x, coef p‖ ≤ ∑ p ∈ P, ‖coef p‖

theorem TrilinearHT.Auto.clump_fiber_sum {τ : Type u_1} (P : Finset τ) (coef : τ → ℂ) (g : τ → ℝ) (t : ℝ) : ∑ x ∈ Finset.image g P, (∑ p ∈ P with g p = x, coef p) * ↑(Real.fourierChar (x * t)) = ∑ p ∈ P, coef p * ↑(Real.fourierChar (g p * t))

theorem TrilinearHT.Auto.clump_sup_error {τ : Type u_1} [DecidableEq τ] (coef : τ → ℂ) (hc : Summable fun (p : τ) => ‖coef p‖) (lam : ℝ) (f : τ → ℝ) {Q : ℝ → ℂ} {r t : ℝ} (ht : |t| ≤ 2 * r) (hQt : HasSum (fun (p : τ) => coef p * quadPhase lam (f p) t) (Q t)) (P : Finset τ) (rep : τ → τ) {ε₁ ε₂ : ℝ} (hε₁ : 0 ≤ ε₁) (hε₂ : 0 ≤ ε₂) (hrep : ∀ p ∈ P, r * |f p - f (rep p)| ≤ ε₂) (hq : |lam| * r ^ 2 ≤ ε₁) {τt Atot : ℝ} (htail : (∑' (p : τ), if p ∈ P then 0 else ‖coef p‖) ≤ τt) (hAtot : ∑ p ∈ P, ‖coef p‖ ≤ Atot) : ‖Q t - ∑ x ∈ Finset.image (fun (p : τ) => f (rep p)) P, (∑ p ∈ P with f (rep p) = x, coef p) * ↑(Real.fourierChar (x * t))‖ ≤ τt + Atot * (8 * Real.pi * ε₁ + 4 * Real.pi * ε₂)

Blueprint lem:predictors, proof line 1525: on a non-exceptional depth the clump replacement approximates the time factor uniformly on |t| ≤ 2r.

noncomputable def TrilinearHT.Auto.clumpMultiplicity (d : ℕ) (B : ℝ) : ℝ

The multiplicity constant of the clump representatives.

Equations

• TrilinearHT.Auto.clumpMultiplicity d B = 24 * (2 * Real.pi) ^ 2 * (4 * TrilinearHT.Auto.heightBandConst d B)