Trilinear Hilbert transform: band_scale_sum_core

theorem TrilinearHT.Auto.band_scale_sum_core (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) {Q : ℝ → ℂ} (hQm : Measurable Q) (hQ1 : ∀ (t : ℝ), ‖Q t‖ ≤ 1) {ψ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))) {A₀ : ℝ} (hband : ∀ I ∈ S, ∀ (ξ : ℝ), bandAmplitude Q (dyadicGridLength G I.1) ξ ≤ A₀) {τ : Type} [Countable τ] [DecidableEq τ] (coef : ℤ → τ → ℂ) (lam : ℤ → ℝ) (freq : ℤ → τ → ℝ) (hexp : ∀ s ∈ Finset.image Prod.fst S, ∀ (t : ℝ), |t| ≤ 2 * dyadicGridLength G s → HasSum (fun (p : τ) => coef s p * quadPhase (lam s) (freq s p) t) (Q t)) (hcs : ∀ (s : ℤ), Summable fun (p : τ) => ‖coef s p‖) (P : Finset τ) (X : Finset ℤ) {ε₁ ε₂ L₂ : ℝ} (hε₁ : 0 ≤ ε₁) (hε₂ : 0 ≤ ε₂) (h3 : 3 * ε₂ < L₂) (hL₂ : 3 ≤ L₂) (hdich : ∀ s ∈ Finset.image Prod.fst S, s ∉ X → ∀ p ∈ P, ∀ q ∈ P, dyadicGridLength G s * |freq s p - freq s q| ≤ ε₂ ∨ L₂ ≤ dyadicGridLength G s * |freq s p - freq s q|) (hquad : ∀ s ∈ Finset.image Prod.fst S, s ∉ X → |lam s| * dyadicGridLength G s ^ 2 ≤ ε₁) (tiny : ℤ → ℝ) (htiny0 : ∀ (s : ℤ), 0 ≤ tiny s) (htiny : ∀ s ∈ Finset.image Prod.fst S, s ∉ X → ∀ p ∈ P, ∀ q ∈ P, dyadicGridLength G s * |freq s p - freq s q| ≤ ε₂ → dyadicGridLength G s * |freq s p - freq s q| ≤ tiny s) {Θ : ℝ} (hΘ : ∑ s ∈ Finset.image Prod.fst S with s ∉ X, (|lam s| * dyadicGridLength G s ^ 2 + tiny s) ≤ Θ) {Atot τt Cζ : ℝ} (hCζ : ∀ (η : ℝ), η ≠ 0 → ‖∫ (u : ℝ), ↑(bandCutoff u) * ↑(Real.fourierChar (-(η * u)))‖ ≤ Cζ / η ^ 2) (hCζ0 : 0 ≤ Cζ) (hAtot : ∀ (s : ℤ), ∑ p ∈ P, ‖coef s p‖ ≤ Atot) (htail : ∀ (s : ℤ), (∑' (p : τ), if p ∈ P then 0 else ‖coef s p‖) ≤ τt) (hsmall : τt + Atot * (8 * Real.pi * ε₁ + 4 * Real.pi * ε₂) + Cζ * Atot / L₂ ^ 2 ≤ A₀ / 2) {dχ : ℕ} (χ : Fin dχ → ℝ) {Bc : ℝ} (hBc : 2 ≤ Bc) (hrat : ∀ s ∈ Finset.image Prod.fst S, ∀ p ∈ P, ∃ (q : Fin dχ → ℚ), (∀ (j : Fin dχ), ↑(rationalHeight (q j)) ≤ Bc) ∧ freq s p / (↑↑b - ↑↑a) = ∑ j : Fin dχ, ↑(q j) * χ j) (env : τ → ℝ) (henv : ∀ (s : ℤ) (p : τ), ‖coef s p‖ ≤ env p) (hens : Summable env) (Mt : τ → ℝ) (hMt : ∀ p ∉ P, ∀ (ξ : ℝ), ∑ x ∈ Finset.image (fun (I : ℤ × ℤ) => (I.1, freq I.1 p / (↑↑b - ↑↑a))) S, bumpMultiplier (dyadicGridLength G x.1 * (ξ - x.2)) ≤ Mt p) {Λ : ℝ} (hΛ : ∑ s ∈ Finset.image Prod.fst S, 2 * Real.pi * |lam s| * dyadicGridLength G s ^ 2 ≤ Λ) {Tt : ℝ} (hTs : Summable fun (p : τ) => if p ∈ P then 0 else env p * (linearScaleConst κ * Mt p + localKernelSupBound κ * Λ)) (hTt : (∑' (p : τ), if p ∈ P then 0 else env p * (linearScaleConst κ * Mt p + localKernelSupBound κ * Λ)) ≤ Tt) : ∑ I ∈ S, dyadicGridLength G I.1 * ‖separatedLocalForm (dyadicGridLength G I.1) (w I) Q a b (fun (y : ℝ) => ψa y * za I y) fun (y : ℝ) => ψb y * zb I y‖ ≤ (kernelFourierConst κ * A₀ * ↑X.card + A₀ * linearScaleConst κ * clumpMultiplicity dχ Bc + localKernelSupBound κ * Atot * (2 * Real.pi) * Θ + Tt) * 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 1517–1542 (core of eq:band-scale-sum): given at every depth an expansion Q = Σ_p c_p e(λ t² + γ_p t) on |t| ≤ 2r, a finite catalog P, a set X of exceptional depths, and outside X the tiny/large dichotomy for the catalog frequencies and tiny quadratics, the absolute scale sum is bounded by the exceptional contribution, the clump contribution (with clump coefficients ≤ A₀), the replacement errors and the tail outside the catalog.

theorem TrilinearHT.Auto.one_le_rationalHeight (q : ℚ) : 1 ≤ ↑(rationalHeight q)

theorem TrilinearHT.Auto.rationalHeight_add_le (q r : ℚ) : ↑(rationalHeight (q + r)) ≤ 3 * (↑(rationalHeight q) * ↑(rationalHeight r)) ^ 2

Heights of sums of rationals.

theorem TrilinearHT.Auto.rationalHeight_sub_le (q r : ℚ) : ↑(rationalHeight (q - r)) ≤ 3 * (↑(rationalHeight q) * ↑(rationalHeight r)) ^ 2

theorem TrilinearHT.Auto.rationalHeight_div_intCast_le (q : ℚ) {k : ℤ} (hk : k ≠ 0) : ↑(rationalHeight (q / ↑k)) ≤ 2 * |↑k| * ↑(rationalHeight q) ^ 2

Heights of quotients by a nonzero integer.

theorem TrilinearHT.Auto.chart_depth_expansion (c₀ : ℕ) (hc : 1 ≤ c₀) : ∃ (D : ℕ), 1 ≤ D ∧ ∃ (DJ : ℕ → ℕ), ∀ {d : ℕ} (H δ r : ℝ) (A : QuadraticChartData d), QuadraticChartComplexity c₀ H A → 0 < r → 0 < δ → (∀ (u : ℝ), ‖↑(bandCutoff u)‖ ≤ H) → (∀ (u v : ℝ), ‖↑(bandCutoff v) - ↑(bandCutoff u)‖ ≤ H * |v - u|) → (∃ (ξ : ℝ), δ < bandAmplitude (quadraticChartAtom A) r ξ) → ∃ (lam : ℝ) (M : Matrix (Fin d) (Fin d) ℚ) (σ : ℕ × (Fin (d + d) → ℤ) → Fin d → ℚ) (coef : ℕ × (Fin (d + d) → ℤ) → ℂ), (∀ (i j : Fin d), ↑(rationalHeight (M i j)) ≤ Real.exp (↑D * (1 + Real.log H + Real.log (max 1 δ⁻¹)) ^ D)) ∧ lam = A.quadratic + ∑ i : Fin d, ∑ j : Fin d, A.horizontal i * ↑(M i j) * A.horizontal j ∧ |lam| * r ^ 2 ≤ Real.exp (↑D * (1 + Real.log H + Real.log (max 1 δ⁻¹)) ^ D) ∧ (∀ (p : ℕ × (Fin (d + d) → ℤ)) (i : Fin d), ↑(rationalHeight (σ p i)) ≤ Real.exp (↑D * (1 + Real.log H + Real.log (max 1 δ⁻¹)) ^ D) * (1 + frequencyLength p.2)) ∧ (∀ (t : ℝ), |t| ≤ 2 * r → HasSum (fun (p : ℕ × (Fin (d + d) → ℤ)) => coef p * quadPhase lam (A.linear + ∑ i : Fin d, ↑(σ p i) * A.horizontal i) t) (quadraticChartAtom A t)) ∧ (Summable fun (p : ℕ × (Fin (d + d) → ℤ)) => ‖coef p‖) ∧ ∑' (p : ℕ × (Fin (d + d) → ℤ)), ‖coef p‖ ≤ Real.exp (↑D * (1 + Real.log H + Real.log (max 1 δ⁻¹)) ^ D) ∧ (∀ (p : ℕ × (Fin (d + d) → ℤ)), ⌊Real.exp (↑D * (1 + Real.log H + Real.log (max 1 δ⁻¹)) ^ D)⌋₊ ≤ p.1 → coef p = 0) ∧ ∀ (p : ℕ × (Fin (d + d) → ℤ)), ‖coef p‖ * (1 + frequencyLength p.2) ^ (d + 1) ^ 2 ≤ Real.exp (↑(DJ 1) * (1 + Real.log H + Real.log (max 1 δ⁻¹)) ^ DJ 1)

Blueprint lem:predictors, proof line 1517: at a scale of the band A_r > δ, lemmas lem:weyl and lem:chartfourier (through separatedPhase) expand the time factor into phases e(λ_* t² + γ t) on |t| ≤ 2r, with λ_* and γ - β bounded-height rational evaluations of the fixed chart parameters, indexed by ℕ × ℤ^{2d}.

theorem TrilinearHT.Auto.lattice_weight_tail {D k : ℕ} (hD : 1 ≤ D) (hk : D < k) (K₀ : ℕ) : (Summable fun (v : Fin D → ℤ) => if v ≠ 0 ∧ 2 ^ K₀ ≤ 1 + frequencyLength v then ((1 + frequencyLength v) ^ k)⁻¹ else 0) ∧ (∑' (v : Fin D → ℤ), if v ≠ 0 ∧ 2 ^ K₀ ≤ 1 + frequencyLength v then ((1 + frequencyLength v) ^ k)⁻¹ else 0) ≤ 2 * 7 ^ D * (2 * Real.pi) ^ k / 2 ^ K₀

Lattice tail of the weight (1 + |v|)^{-k} beyond a dyadic radius, k > D.

theorem TrilinearHT.Auto.tsum_prod_range_le {V : Type u_1} (f : ℕ × V → ℝ) (hf0 : ∀ (q : ℕ × V), 0 ≤ f q) (N : ℕ) (w : V → ℝ) (hw : Summable w) (hfw : ∀ (q : ℕ × V), f q ≤ if q.1 < N then w q.2 else 0) : Summable f ∧ ∑' (q : ℕ × V), f q ≤ ↑N * ∑' (v : V), w v

Sums over ℕ × V of functions supported on finitely many first coordinates.

theorem TrilinearHT.Auto.rationalHeight_le_floor {q : ℚ} {B : ℝ} (h : ↑(rationalHeight q) ≤ B) : rationalHeight q ≤ ⌊B⌋₊

theorem TrilinearHT.Auto.le_tinyMaximum_of_rational {d : ℕ} (χ : Fin d → ℝ) {B : ℝ} (a : Fin d → ℚ) (ha : ∀ (j : Fin d), ↑(rationalHeight (a j)) ≤ B) {w ε : ℝ} (hw : 0 ≤ w) (hsmall : w * |∑ j : Fin d, ↑(a j) * χ j| ≤ ε) : w * |∑ j : Fin d, ↑(a j) * χ j| ≤ finiteTinyMaximum (boundedRationalMagnitudes ⌊B⌋₊ (rationalEvaluation χ)) w ε

A tiny scaled bounded-height rational evaluation is dominated by the tiny maximum.

theorem TrilinearHT.Auto.grid_tiny_sum_le {d u : ℕ} (G : RealDyadicGrid) (χ : Fin d → ℝ) {B ε : ℝ} (hB : 2 ≤ B) (hu : 1 ≤ u) (hε : 0 ≤ ε) (T : Finset ℤ) : ∑ s ∈ T, finiteTinyMaximum (boundedRationalMagnitudes ⌊B⌋₊ (rationalEvaluation χ)) (dyadicGridLength G s ^ u) ε ≤ 128 * (↑d + 1) ^ 4 * Real.log (2 * B) * ε

lem:height, eq:tiny-sum on a finite set of depths of a dyadic grid.

noncomputable def TrilinearHT.Auto.quadraticParamVector {d : ℕ} (lam : ℝ) (θ : Fin d → ℝ) : Fin (d * d + 1) → ℝ

The vector (λ, θ_i θ_j) whose bounded-height rational evaluations are the effective quadratic coefficients λ_* = λ + θᵀ M θ.

Equations

• TrilinearHT.Auto.quadraticParamVector lam θ = Fin.cons lam fun (x : Fin (d * d)) => θ (finProdFinEquiv.symm x).1 * θ (finProdFinEquiv.symm x).2

theorem TrilinearHT.Auto.quadraticParam_eval {d : ℕ} (lam : ℝ) (θ : Fin d → ℝ) (M : Matrix (Fin d) (Fin d) ℚ) : ∑ j : Fin (d * d + 1), ↑(Fin.cons 1 (fun (x : Fin (d * d)) => M (finProdFinEquiv.symm x).1 (finProdFinEquiv.symm x).2) j) * quadraticParamVector lam θ j = lam + ∑ i : Fin d, ∑ j : Fin d, θ i * ↑(M i j) * θ j

theorem TrilinearHT.Auto.quadraticParam_height {d : ℕ} (M : Matrix (Fin d) (Fin d) ℚ) {B : ℝ} (hB : 1 ≤ B) (hM : ∀ (i j : Fin d), ↑(rationalHeight (M i j)) ≤ B) (j : Fin (d * d + 1)) : ↑(rationalHeight (Fin.cons 1 (fun (x : Fin (d * d)) => M (finProdFinEquiv.symm x).1 (finProdFinEquiv.symm x).2) j)) ≤ B

theorem TrilinearHT.Auto.center_rational {d : ℕ} (β : ℝ) (θ : Fin d → ℝ) (σ : Fin d → ℚ) {k : ℤ} (hk : k ≠ 0) (hk3 : |↑k| ≤ 3) {B : ℝ} (hσ : ∀ (i : Fin d), ↑(rationalHeight (σ i)) ≤ B) : (∀ (j : Fin (d + 1)), ↑(rationalHeight (Fin.cons (1 / ↑k) (fun (i : Fin d) => σ i / ↑k) j)) ≤ 6 * B ^ 2 + 6) ∧ (β + ∑ i : Fin d, ↑(σ i) * θ i) / ↑k = ∑ j : Fin (d + 1), ↑(Fin.cons (1 / ↑k) (fun (i : Fin d) => σ i / ↑k) j) * Fin.cons β θ j

Centers (β + σ·θ)/(b-a) as rational evaluations of (β, θ).

noncomputable def TrilinearHT.Auto.bandLip : ℝ

The Lipschitz constant of the band plateau.

Equations

• TrilinearHT.Auto.bandLip = Classical.choose TrilinearHT.Auto.bandCutoff_lipschitz

theorem TrilinearHT.Auto.bandLip_spec : 0 ≤ bandLip ∧ ∀ (u v : ℝ), |bandCutoff v - bandCutoff u| ≤ bandLip * |v - u|

noncomputable def TrilinearHT.Auto.bandDecay : ℝ

The Fourier decay constant of the band plateau.

Equations

• TrilinearHT.Auto.bandDecay = Classical.choose TrilinearHT.Auto.bandCutoff_fourier_decay

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

Explicit parameters of the band scale sum (blueprint lem:predictors, proof lines 1517–1527), as functions of the chart-expansion exponents D, J₁, the dimension d, the band index m and Lh = log H.

noncomputable def TrilinearHT.Auto.bsX (m : ℕ) (Lh : ℝ) : ℝ

Combined logarithmic-size and accuracy parameter for the band-scale estimates.

Equations

• TrilinearHT.Auto.bsX m Lh = 2 + Lh + ↑m

noncomputable def TrilinearHT.Auto.bsE (D m : ℕ) (Lh : ℝ) : ℝ

Exponential complexity budget in the band-scale estimates.

Equations

• TrilinearHT.Auto.bsE D m Lh = Real.exp (↑D * TrilinearHT.Auto.bsX m Lh ^ D)

noncomputable def TrilinearHT.Auto.bsE1 (J1 m : ℕ) (Lh : ℝ) : ℝ

Exponential coefficient-tail budget in the band-scale estimates.

Equations

• TrilinearHT.Auto.bsE1 J1 m Lh = Real.exp (↑J1 * TrilinearHT.Auto.bsX m Lh ^ J1)

noncomputable def TrilinearHT.Auto.bsEps (D m : ℕ) (Lh : ℝ) : ℝ

Approximation tolerance balancing the band-scale complexity and accuracy.

Equations

• TrilinearHT.Auto.bsEps D m Lh = Real.exp (-↑m) / (64 * Real.pi * TrilinearHT.Auto.bsE D m Lh)

noncomputable def TrilinearHT.Auto.bsL2 (D m : ℕ) (Lh : ℝ) : ℝ

Cutoff scale controlling the band-scale L² tail.

Equations

• TrilinearHT.Auto.bsL2 D m Lh = 3 + 8 * TrilinearHT.Auto.bandDecay * TrilinearHT.Auto.bsE D m Lh * Real.exp ↑m

noncomputable def TrilinearHT.Auto.bsLam (d D m : ℕ) (Lh : ℝ) : ℝ

Frequency cutoff in the band-scale expansion.

Equations

• TrilinearHT.Auto.bsLam d D m Lh = 2 * Real.pi * (128 * (↑(d * d + 1) + 1) ^ 4 * Real.log (2 * (TrilinearHT.Auto.bsE D m Lh + 2)) * TrilinearHT.Auto.bsE D m Lh)

noncomputable def TrilinearHT.Auto.bsAlpha (d D m : ℕ) (Lh : ℝ) : ℝ

Phase-growth budget in the band-scale expansion.

Equations

• TrilinearHT.Auto.bsAlpha d D m Lh = 24 * (2 * Real.pi) ^ 2 * (4 * (32 * (↑(d + 1) + 1 + 1) ^ 4 * (Real.log 24 + 2 * (↑D * TrilinearHT.Auto.bsX m Lh ^ D) + 2 + Real.log 4)))

noncomputable def TrilinearHT.Auto.bsCT (κ : LocalKernelClass) (d D m : ℕ) (Lh : ℝ) : ℝ

Kernel-weighted combination of phase and frequency budgets for band-scale summation.

Equations

• TrilinearHT.Auto.bsCT κ d D m Lh = TrilinearHT.Auto.linearScaleConst κ * TrilinearHT.Auto.bsAlpha d D m Lh + TrilinearHT.Auto.localKernelSupBound κ * TrilinearHT.Auto.bsLam d D m Lh

noncomputable def TrilinearHT.Auto.bsK0 (κ : LocalKernelClass) (d D J1 m : ℕ) (Lh : ℝ) : ℕ

Dyadic truncation depth sufficient for the band-scale approximation error.

Equations

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

noncomputable def TrilinearHT.Auto.bsBσ (κ : LocalKernelClass) (d D J1 m : ℕ) (Lh : ℝ) : ℝ

Frequency-size budget after dyadic truncation of the band-scale expansion.

Equations

• TrilinearHT.Auto.bsBσ κ d D J1 m Lh = TrilinearHT.Auto.bsE D m Lh * 2 ^ TrilinearHT.Auto.bsK0 κ d D J1 m Lh

noncomputable def TrilinearHT.Auto.bsB2 (κ : LocalKernelClass) (d D J1 m : ℕ) (Lh : ℝ) : ℝ

Quadratic-size budget derived from the truncated frequency-size bound.

Equations

• TrilinearHT.Auto.bsB2 κ d D J1 m Lh = 3 * TrilinearHT.Auto.bsBσ κ d D J1 m Lh ^ 4 + 2

noncomputable def TrilinearHT.Auto.bsB1 (D m : ℕ) (Lh : ℝ) : ℝ

Basic chart-complexity budget in the band-scale expansion.

Equations

• TrilinearHT.Auto.bsB1 D m Lh = TrilinearHT.Auto.bsE D m Lh + 2

noncomputable def TrilinearHT.Auto.bsBc (κ : LocalKernelClass) (d D J1 m : ℕ) (Lh : ℝ) : ℝ

Coefficient-sum budget derived from the truncated frequency-size bound.

Equations

• TrilinearHT.Auto.bsBc κ d D J1 m Lh = 6 * TrilinearHT.Auto.bsBσ κ d D J1 m Lh ^ 2 + 6

noncomputable def TrilinearHT.Auto.bandBracket (κ : LocalKernelClass) (d D J1 m : ℕ) (Lh : ℝ) : ℝ

The polynomial factor in eq:band-scale-sum before its final simplification.

Equations

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

theorem TrilinearHT.Auto.frequencyTruncationSet_le {D K : ℕ} {v : Fin D → ℤ} (hv : v ∈ frequencyTruncationSet D K) : 1 + frequencyLength v ≤ 2 ^ K

theorem TrilinearHT.Auto.not_mem_frequencyTruncationSet {D K : ℕ} {v : Fin D → ℤ} (hv : v ∉ frequencyTruncationSet D K) : v ≠ 0 ∧ 2 ^ K ≤ 1 + frequencyLength v

theorem TrilinearHT.Auto.two_pow_ceil_logb_ge {Z : ℝ} (hZ : 0 < Z) : Z ≤ 2 ^ ⌈Real.logb 2 Z⌉₊

theorem TrilinearHT.Auto.bsE_one_le (D m : ℕ) {Lh : ℝ} (hLh : 0 ≤ Lh) : 1 ≤ bsE D m Lh

theorem TrilinearHT.Auto.summable_lattice_weight {D k : ℕ} (hD : 1 ≤ D) (hk : D < k) : Summable fun (v : Fin D → ℤ) => ((1 + frequencyLength v) ^ k)⁻¹

theorem TrilinearHT.Auto.bsEps_pos (D m : ℕ) {Lh : ℝ} (hLh : 0 ≤ Lh) : 0 < bsEps D m Lh

theorem TrilinearHT.Auto.bsEps_le_one (D m : ℕ) {Lh : ℝ} (hLh : 0 ≤ Lh) : bsEps D m Lh ≤ 1

theorem TrilinearHT.Auto.three_le_bsL2 (D m : ℕ) {Lh : ℝ} (hLh : 0 ≤ Lh) : 3 ≤ bsL2 D m Lh

theorem TrilinearHT.Auto.one_le_bsBσ (κ : LocalKernelClass) (d D J1 m : ℕ) {Lh : ℝ} (hLh : 0 ≤ Lh) : 1 ≤ bsBσ κ d D J1 m Lh

theorem TrilinearHT.Auto.two_le_bsB2 (κ : LocalKernelClass) (d D J1 m : ℕ) {Lh : ℝ} (hLh : 0 ≤ Lh) : 2 ≤ bsB2 κ d D J1 m Lh

theorem TrilinearHT.Auto.two_le_bsB1 (D m : ℕ) {Lh : ℝ} (hLh : 0 ≤ Lh) : 2 ≤ bsB1 D m Lh

theorem TrilinearHT.Auto.two_le_bsBc (κ : LocalKernelClass) (d D J1 m : ℕ) (Lh : ℝ) : 2 ≤ bsBc κ d D J1 m Lh

theorem TrilinearHT.Auto.bs_quadratic_budget (D m : ℕ) {Lh : ℝ} (hLh : 0 ≤ Lh) : bsE D m Lh * (8 * Real.pi * bsEps D m Lh + 4 * Real.pi * bsEps D m Lh) = 3 / 16 * Real.exp (-↑m)

theorem TrilinearHT.Auto.bs_decay_budget (D m : ℕ) {Lh : ℝ} (hLh : 0 ≤ Lh) : bandDecay * bsE D m Lh / bsL2 D m Lh ^ 2 ≤ Real.exp (-↑m) / 8

theorem TrilinearHT.Auto.bsCT_nonneg (κ : LocalKernelClass) (d D m : ℕ) {Lh : ℝ} (hLh : 0 ≤ Lh) : 0 ≤ bsCT κ d D m Lh

theorem TrilinearHT.Auto.bs_tail_budget (κ : LocalKernelClass) (d D J1 m : ℕ) {Lh : ℝ} (hLh : 0 ≤ Lh) {k : ℕ} (hk : k ≤ (d + 1) ^ 2) {C : ℝ} (hC0 : 0 ≤ C) (hC : C ≤ bsCT κ d D m Lh + 1) : ↑⌊bsE D m Lh⌋₊ * bsE1 J1 m Lh * C * (2 * 7 ^ (d + d) * (2 * Real.pi) ^ k / 2 ^ bsK0 κ d D J1 m Lh) ≤ Real.exp (-↑m) / 8

The catalog truncation level makes the pooled tails small.

theorem TrilinearHT.Auto.catalog_tail_le {d : ℕ} (hd : 1 ≤ d) (coef : ℕ × (Fin (d + d) → ℤ) → ℂ) {N₀ K₀ : ℕ} {E1 : ℝ} (hE1 : 0 ≤ E1) (hvan : ∀ (p : ℕ × (Fin (d + d) → ℤ)), N₀ ≤ p.1 → coef p = 0) (henv : ∀ (p : ℕ × (Fin (d + d) → ℤ)), ‖coef p‖ * (1 + frequencyLength p.2) ^ (d + 1) ^ 2 ≤ E1) : (∑' (p : ℕ × (Fin (d + d) → ℤ)), if p ∈ Finset.range N₀ ×ˢ frequencyTruncationSet (d + d) K₀ then 0 else ‖coef p‖) ≤ ↑N₀ * (E1 * (2 * 7 ^ (d + d) * (2 * Real.pi) ^ (d + 1) ^ 2 / 2 ^ K₀))

The pooled catalog tail of one depth expansion.

theorem TrilinearHT.Auto.catalog_weighted_tail {d : ℕ} (hd : 1 ≤ d) {N₀ K₀ : ℕ} {E1 CT : ℝ} (hE1 : 0 ≤ E1) (hCT : 0 ≤ CT) (g : ℕ × (Fin (d + d) → ℤ) → ℝ) (hg0 : ∀ (p : ℕ × (Fin (d + d) → ℤ)), 0 ≤ g p) (hg : ∀ (p : ℕ × (Fin (d + d) → ℤ)), g p ≤ CT * (1 + frequencyLength p.2)) : (Summable fun (p : ℕ × (Fin (d + d) → ℤ)) => if p.1 < N₀ then E1 * ((1 + frequencyLength p.2) ^ (d + 1) ^ 2)⁻¹ else 0) ∧ (Summable fun (p : ℕ × (Fin (d + d) → ℤ)) => if p ∈ Finset.range N₀ ×ˢ frequencyTruncationSet (d + d) K₀ then 0 else (if p.1 < N₀ then E1 * ((1 + frequencyLength p.2) ^ (d + 1) ^ 2)⁻¹ else 0) * g p) ∧ (∑' (p : ℕ × (Fin (d + d) → ℤ)), if p ∈ Finset.range N₀ ×ˢ frequencyTruncationSet (d + d) K₀ then 0 else (if p.1 < N₀ then E1 * ((1 + frequencyLength p.2) ^ (d + 1) ^ 2)⁻¹ else 0) * g p) ≤ ↑N₀ * (E1 * CT * (2 * 7 ^ (d + d) * (2 * Real.pi) ^ ((d + 1) ^ 2 - 1) / 2 ^ K₀))

The weighted pooled tail against the coefficient envelope.

theorem TrilinearHT.Auto.clumpMultiplicity_tail_le (d D m : ℕ) {Lh : ℝ} (hLh : 0 ≤ Lh) {u : ℝ} (hu : 1 ≤ u) : clumpMultiplicity (d + 1) (6 * (bsE D m Lh * u) ^ 2 + 6) ≤ bsAlpha d D m Lh * u

The tail multiplicity constant grows at most linearly in 1 + |v|.

theorem TrilinearHT.Auto.band_exceptional_depths (G : RealDyadicGrid) {d : ℕ} (θ : Fin d → ℝ) (q₀ : ℝ) (T : Finset ℤ) (lam : ℤ → ℝ) (M : ℤ → Matrix (Fin d) (Fin d) ℚ) {τ : Type u_1} (P : Finset τ) (σ : ℤ → τ → Fin d → ℚ) {ε L₂ E B₁ B₂ : ℝ} (hε : 0 < ε) (hεL : ε ≤ L₂) (hεE : ε ≤ E) (hB₁ : 2 ≤ B₁) (hB₂ : 2 ≤ B₂) (hlam : ∀ s ∈ T, lam s = q₀ + ∑ i : Fin d, ∑ j : Fin d, θ i * ↑(M s i j) * θ j) (hM : ∀ s ∈ T, ∀ (i j : Fin d), ↑(rationalHeight (M s i j)) ≤ B₁) (hlamE : ∀ s ∈ T, |lam s| * dyadicGridLength G s ^ 2 ≤ E) (hσ : ∀ s ∈ T, ∀ p ∈ P, ∀ q ∈ P, ∀ (i : Fin d), ↑(rationalHeight (σ s p i - σ s q i)) ≤ B₂) : ∃ (X : Finset ℤ), ↑X.card ≤ 32 * (↑d + 1) ^ 4 * (Real.log (2 * B₂) + Real.log (2 * L₂ / ε)) + 32 * (↑(d * d + 1) + 1) ^ 4 * (Real.log (2 * B₁) + Real.log (2 * E / ε)) ∧ (∀ s ∈ T, s ∉ X → ∀ p ∈ P, ∀ q ∈ P, dyadicGridLength G s * |∑ i : Fin d, ↑(σ s p i - σ s q i) * θ i| ≤ ε ∨ L₂ ≤ dyadicGridLength G s * |∑ i : Fin d, ↑(σ s p i - σ s q i) * θ i|) ∧ ∀ s ∈ T, s ∉ X → |lam s| * dyadicGridLength G s ^ 2 ≤ ε

Blueprint lem:predictors, proof line 1525: exceptional depths. Outside a set of lem:height-many depths, all scaled catalog differences are tiny or large, and the effective quadratic coefficient is tiny.

theorem TrilinearHT.Auto.band_tiny_sum (G : RealDyadicGrid) {d : ℕ} (θ : Fin d → ℝ) (q₀ : ℝ) (T : Finset ℤ) (lam : ℤ → ℝ) (M : ℤ → Matrix (Fin d) (Fin d) ℚ) {ε B₁ B₂ : ℝ} (hε : 0 ≤ ε) (hB₁ : 2 ≤ B₁) (hB₂ : 2 ≤ B₂) (hlam : ∀ s ∈ T, lam s = q₀ + ∑ i : Fin d, ∑ j : Fin d, θ i * ↑(M s i j) * θ j) (hM : ∀ s ∈ T, ∀ (i j : Fin d), ↑(rationalHeight (M s i j)) ≤ B₁) (hquad : ∀ s ∈ T, |lam s| * dyadicGridLength G s ^ 2 ≤ ε) : ∑ s ∈ T, (|lam s| * dyadicGridLength G s ^ 2 + finiteTinyMaximum (boundedRationalMagnitudes ⌊B₂⌋₊ (rationalEvaluation θ)) (dyadicGridLength G s ^ 1) ε) ≤ 128 * (↑(d * d + 1) + 1) ^ 4 * Real.log (2 * B₁) * ε + 128 * (↑d + 1) ^ 4 * Real.log (2 * B₂) * ε

Blueprint lem:predictors, proof line 1525 with eq:tiny-sum: the replacement errors on the non-exceptional depths sum to O(ε log) over all depths.

theorem TrilinearHT.Auto.band_quadratic_total (G : RealDyadicGrid) {d : ℕ} (θ : Fin d → ℝ) (q₀ : ℝ) (T : Finset ℤ) (lam : ℤ → ℝ) (M : ℤ → Matrix (Fin d) (Fin d) ℚ) {E B₁ : ℝ} (hE : 0 ≤ E) (hB₁ : 2 ≤ B₁) (hlam : ∀ s ∈ T, lam s = q₀ + ∑ i : Fin d, ∑ j : Fin d, θ i * ↑(M s i j) * θ j) (hM : ∀ s ∈ T, ∀ (i j : Fin d), ↑(rationalHeight (M s i j)) ≤ B₁) (hlamE : ∀ s ∈ T, |lam s| * dyadicGridLength G s ^ 2 ≤ E) : ∑ s ∈ T, 2 * Real.pi * |lam s| * dyadicGridLength G s ^ 2 ≤ 2 * Real.pi * (128 * (↑(d * d + 1) + 1) ^ 4 * Real.log (2 * B₁) * E)

The total quadratic size over all depths, by eq:tiny-sum at the threshold E.