Section 9, part 2: lem:chartfourier and lem:separation #
This file was automatically generated by Claude.
Formalization of blueprint Section 9, "Weyl splitting and progression separation" (sec:charts),
part 2: lem:chartfourier and lem:separation (lines 1336-1417) of
blueprint/formalization_blueprint.tex.
theorem
TrilinearHT.Auto.chart_phase_split
{d : ℕ}
(C Pf Ps : Matrix (Fin d) (Fin d) ℝ)
(hP : Pf + Ps = 1)
(hiso : Pf.transpose * (C - C.transpose) * Pf = 0)
(u n : Fin d → ℝ)
:
u ⬝ᵥ C.mulVec (u - n) = 1 / 2 * u ⬝ᵥ (realSymmetricPart C).mulVec u + Pf.mulVec u ⬝ᵥ (realSkewPart C).mulVec (Ps.mulVec u) + (1 / 2 * (u - n) ⬝ᵥ (realSymmetricPart C).mulVec (u - n) + Ps.mulVec u ⬝ᵥ (realSkewPart C).mulVec (u - n)) - 1 / 2 * n ⬝ᵥ (realSymmetricPart C).mulVec n - Pf.mulVec u ⬝ᵥ (realSkewPart C).mulVec (Ps.mulVec n)
Blueprint lem:chartfourier, lines 1349–1355: the exact phase identities.
For complementary projections P_f + P_s = 1 whose fast range is isotropic for
the skew part of C, the chart phase uᵀC(u-n) splits into the effective
quadratic ½uᵀC_sy u + u_fᵀC_sk u_s, a part depending only on (u_s, u - n),
the residue phase -½nᵀC_sy n, and the linear phase -u_fᵀC_sk P_s n.
theorem
TrilinearHT.Auto.multivariableChartPhase_split
{k d : ℕ}
(A : MultivariableQuadraticChartData k d)
(Pf Ps : Matrix (Fin d) (Fin d) ℝ)
(hP : Pf + Ps = 1)
(hiso : Pf.transpose * ((A.matrix.map fun (q : ℚ) => ↑q) - (A.matrix.map fun (q : ℚ) => ↑q).transpose) * Pf = 0)
(z : Fin k → ℝ)
(n : Fin d → ℤ)
:
have C := A.matrix.map fun (q : ℚ) => ↑q;
have u := A.horizontal.mulVec z;
have w := u - fun (i : Fin d) => ↑(n i);
multivariableChartPhase A z n = (z ⬝ᵥ (effectiveReturnQuadratic C A.quadratic A.horizontal (Pf * A.horizontal) (Ps * A.horizontal)).mulVec z + A.linear ⬝ᵥ z + (1 / 2 * w ⬝ᵥ (realSymmetricPart C).mulVec w + Ps.mulVec u ⬝ᵥ (realSkewPart C).mulVec w) - 1 / 2 * (fun (i : Fin d) => ↑(n i)) ⬝ᵥ (realSymmetricPart C).mulVec fun (i : Fin d) => ↑(n i)) - Pf.mulVec u ⬝ᵥ (realSkewPart C).mulVec (Ps.mulVec fun (i : Fin d) => ↑(n i))
The phase of one chart lattice summand after extracting Λ_*
(lem:chartfourier, lines 1349–1355).
The periodic slow amplitude of lem:chartfourier #
The tensor cutoff v ↦ ∏ ψ(vᵢ / r). With a plateau cutoff ψ it equals one
on the cube of radius r and vanishes outside the cube of radius 2r.
Equations
- TrilinearHT.Auto.tensorCutoff ψ r v = ∏ i : Fin d, ↑(ψ (v i / r))
Instances For
noncomputable def
TrilinearHT.Auto.chartSlowPhase
{d : ℕ}
(Csy Csk : Matrix (Fin d) (Fin d) ℝ)
(s w : Fin d → ℝ)
(n : Fin d → ℤ)
:
The phase of one lattice term in the slow amplitude: the part of the chart
phase depending only on the slow variable s and the remainder w = u - n,
together with the residue phase -½ nᵀC_sy n.
Equations
Instances For
noncomputable def
TrilinearHT.Auto.chartSlowAmplitude
{d : ℕ}
(χ : (Fin d → ℝ) → ℂ)
(ψ : ℝ → ℝ)
(rE S : ℝ)
(Ps Csy Csk : Matrix (Fin d) (Fin d) ℝ)
(N s u : Fin d → ℝ)
:
The two-variable slow amplitude of lem:chartfourier, lines 1357–1361:
η(s) Σₙ χ(u-n) E(s - P_s(u-n) - N) e(½wᵀC_sy w + sᵀC_sk w - ½nᵀC_sy n) with
w = u - n, the equality cutoff E of radius rE and slow cutoff η of
radius S.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The finite box of scaled slow lattice values ν, standing for N = ν / q₀.
Equations
- TrilinearHT.Auto.slowValueBox d K = Fintype.piFinset fun (x : Fin d) => Finset.Icc (-↑K) ↑K
Instances For
theorem
TrilinearHT.Auto.chartSlow_grouping
{d : ℕ}
(χ : (Fin d → ℝ) → ℂ)
{ψ : ℝ → ℝ}
(hψ1 : ∀ (x : ℝ), |x| ≤ 1 → ψ x = 1)
(hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0)
(Pf Ps Csy Csk : Matrix (Fin d) (Fin d) ℝ)
{q₀ : ℕ}
(hq : 0 < q₀)
(hPs : ∀ (i j : Fin d), ∃ (z : ℤ), ↑q₀ * Ps i j = ↑z)
{H B S : ℝ}
(hS : 0 < S)
(hχ : ∀ (w : Fin d → ℝ), χ w ≠ 0 → ∀ (i : Fin d), |w i| ≤ H)
(hPsB : ∀ (i j : Fin d), |Ps i j| ≤ B)
{K : ℕ}
(hK : ↑q₀ * (S + ↑d * B * H) ≤ ↑K)
(u : Fin d → ℝ)
(hu : ∀ (i : Fin d), |Ps.mulVec u i| ≤ S)
:
∑' (n : Fin d → ℤ), χ (u - fun (i : Fin d) => ↑(n i)) * ↑(Real.fourierChar
(chartSlowPhase Csy Csk (Ps.mulVec u) (u - fun (i : Fin d) => ↑(n i)) n - Pf.mulVec u ⬝ᵥ Csk.mulVec (Ps.mulVec fun (i : Fin d) => ↑(n i)))) = ∑ ν ∈ slowValueBox d K,
↑(Real.fourierChar (-(Pf.mulVec u ⬝ᵥ Csk.mulVec fun (i : Fin d) => ↑(ν i) / ↑q₀))) * chartSlowAmplitude χ ψ (1 / (3 * ↑q₀)) S Ps Csy Csk (fun (i : Fin d) => ↑(ν i) / ↑q₀) (Ps.mulVec u) u
Blueprint lem:chartfourier, lines 1355–1361: the exact grouping of the
remaining lattice sum by slow values N = P_s n ∈ q₀⁻¹ℤᵈ. On bounded slow values
the equality cutoff picks out exactly one N for every contributing n.
theorem
TrilinearHT.Auto.residue_phase_periodic
{d : ℕ}
(Csy : Matrix (Fin d) (Fin d) ℝ)
(hCsy : Csy.IsSymm)
{P₀ : ℕ}
(hP : ∀ (i j : Fin d), ∃ (z : ℤ), ↑P₀ * Csy i j = ↑z)
(hev : Even P₀)
(n m : Fin d → ℤ)
:
Blueprint lem:chartfourier, line 1355: with an even period P₀ clearing
C_sy, the residue phase e(-½nᵀC_sy n) is unchanged by n ↦ n + P₀m.
theorem
TrilinearHT.Auto.chartSlowAmplitude_periodic
{d : ℕ}
(χ : (Fin d → ℝ) → ℂ)
(ψ : ℝ → ℝ)
(rE S : ℝ)
(Ps Csy Csk : Matrix (Fin d) (Fin d) ℝ)
(hCsy : Csy.IsSymm)
{P₀ : ℕ}
(hP : ∀ (i j : Fin d), ∃ (z : ℤ), ↑P₀ * Csy i j = ↑z)
(hev : Even P₀)
(N s u : Fin d → ℝ)
(m : Fin d → ℤ)
:
chartSlowAmplitude χ ψ rE S Ps Csy Csk N s (u + fun (i : Fin d) => ↑↑P₀ * ↑(m i)) = chartSlowAmplitude χ ψ rE S Ps Csy Csk N s u
The slow amplitude is P₀-periodic in the horizontal variable
(lem:chartfourier, line 1361).
Geometric derivative bounds up to a fixed order #
GeomBound f x K R m records ‖Dⁱ f(x)‖ ≤ K Rⁱ for every i ≤ m. These bounds
are closed under products, finite sums, affine substitution and composition
with the Fourier character; they carry the derivative estimates of
lem:chartfourier, lines 1368–1372.
def
TrilinearHT.Auto.GeomBound
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(f : E → F)
(x : E)
(K R : ℝ)
(m : ℕ)
:
Geometric bounds on all derivatives of order at most m at one point.
Equations
- TrilinearHT.Auto.GeomBound f x K R m = ∀ i ≤ m, ‖iteratedFDeriv ℝ i f x‖ ≤ K * R ^ i
Instances For
theorem
TrilinearHT.Auto.GeomBound.K_nonneg
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : E → F}
{x : E}
{K R : ℝ}
{m : ℕ}
(h : GeomBound f x K R m)
:
theorem
TrilinearHT.Auto.GeomBound.mono
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : E → F}
{x : E}
{K R K' R' : ℝ}
{m : ℕ}
(h : GeomBound f x K R m)
(hK : K ≤ K')
(hR0 : 0 ≤ R)
(hR : R ≤ R')
:
GeomBound f x K' R' m
theorem
TrilinearHT.Auto.GeomBound.mul
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{A : Type u_2}
[NormedCommRing A]
[NormedAlgebra ℝ A]
{f g : E → A}
(hf : ContDiff ℝ (↑⊤) f)
(hg : ContDiff ℝ (↑⊤) g)
{x : E}
{K₁ R₁ K₂ R₂ : ℝ}
{m : ℕ}
(hR₁ : 0 ≤ R₁)
(h₁ : GeomBound f x K₁ R₁ m)
(h₂ : GeomBound g x K₂ R₂ m)
:
Leibniz rule for geometric bounds.
theorem
TrilinearHT.Auto.GeomBound.sum
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{ι : Type u_3}
(s : Finset ι)
{f : ι → E → F}
(hf : ∀ a ∈ s, ContDiff ℝ (↑⊤) (f a))
{x : E}
{K : ι → ℝ}
{R : ℝ}
{m : ℕ}
(h : ∀ a ∈ s, GeomBound (f a) x (K a) R m)
:
GeomBound (fun (y : E) => ∑ a ∈ s, f a y) x (∑ a ∈ s, K a) R m
Finite sums of geometric bounds with a common ratio.
theorem
TrilinearHT.Auto.GeomBound.comp_affine
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : E' → F}
(hf : ContDiff ℝ (↑⊤) f)
(L : E →L[ℝ] E')
(c : E')
{x : E}
{K R : ℝ}
{m : ℕ}
(h : GeomBound f (L x + c) K R m)
:
Substituting an affine map multiplies the ratio by the norm of its linear part.
theorem
TrilinearHT.Auto.GeomBound.const
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(c : F)
(x : E)
{R : ℝ}
(hR : 0 ≤ R)
(m : ℕ)
:
Constants have only a zeroth derivative.
theorem
TrilinearHT.Auto.GeomBound.ofReal
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : E → ℝ}
(hf : ContDiff ℝ (↑⊤) f)
{x : E}
{K R : ℝ}
{m : ℕ}
(h : GeomBound f x K R m)
:
GeomBound (fun (y : E) => ↑(f y)) x K R m
Real-valued bounds pass to the complex cast.
theorem
TrilinearHT.Auto.GeomBound.fourierChar
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{φ : E → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
{x : E}
{K R : ℝ}
{m : ℕ}
(hR : 0 ≤ R)
(h : GeomBound φ x K R m)
:
The Fourier character of a phase with geometric bounds.
noncomputable def
TrilinearHT.Auto.chartUnitAmplitude
{d : ℕ}
(χ : (Fin d → ℝ) → ℂ)
(ψ : ℝ → ℝ)
(rE S : ℝ)
(Ps Csy Csk : Matrix (Fin d) (Fin d) ℝ)
(N : Fin d → ℝ)
(P₀ P₁ : ℝ)
(x : Fin (d + d) → ℝ)
:
The slow amplitude, periodized in the slow variable with period P₁ and
rescaled to unit periods in both variables (lem:chartfourier, lines 1361–1363).
The first d coordinates of x are the slow and the last d the horizontal
variable.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TrilinearHT.Auto.chartUnitAmplitude_periodic
{d : ℕ}
(χ : (Fin d → ℝ) → ℂ)
(ψ : ℝ → ℝ)
(rE S : ℝ)
(Ps Csy Csk : Matrix (Fin d) (Fin d) ℝ)
(hCsy : Csy.IsSymm)
{P₀ : ℕ}
(hP : ∀ (i j : Fin d), ∃ (z : ℤ), ↑P₀ * Csy i j = ↑z)
(hev : Even P₀)
(N : Fin d → ℝ)
(P₁ : ℝ)
(x : Fin (d + d) → ℝ)
(k : Fin (d + d) → ℤ)
:
chartUnitAmplitude χ ψ rE S Ps Csy Csk N (↑P₀) P₁ (x + fun (i : Fin (d + d)) => ↑(k i)) = chartUnitAmplitude χ ψ rE S Ps Csy Csk N (↑P₀) P₁ x
The unit amplitude is ℤ^(d+d)-periodic.
theorem
TrilinearHT.Auto.chartUnitAmplitude_eq
{d : ℕ}
(χ : (Fin d → ℝ) → ℂ)
{ψ : ℝ → ℝ}
(hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0)
(rE : ℝ)
{S : ℝ}
(hS : 0 < S)
(Ps Csy Csk : Matrix (Fin d) (Fin d) ℝ)
(N : Fin d → ℝ)
{P₀ P₁ : ℝ}
(hP₀ : 0 < P₀)
(hP₁ : 4 * S ≤ P₁)
(s u : Fin d → ℝ)
(hs : ∀ (i : Fin d), |s i| ≤ S)
:
chartUnitAmplitude χ ψ rE S Ps Csy Csk N P₀ P₁ (Fin.append (fun (i : Fin d) => s i / P₁) fun (i : Fin d) => u i / P₀) = chartSlowAmplitude χ ψ rE S Ps Csy Csk N s u
On bounded slow values the periodization has a single contributing period,
so the unit amplitude evaluated at (s/P₁, u/P₀) is the slow amplitude.
Smoothness and derivative bounds of the unit amplitude #
The horizontal coordinates of a point of ℝ^(d+d), scaled by P₀.
Equations
- TrilinearHT.Auto.unitHorizCoord P₀ x i = P₀ * x (Fin.natAdd d i)
Instances For
noncomputable def
TrilinearHT.Auto.chartUnitTerm
{d : ℕ}
(χ : (Fin d → ℝ) → ℂ)
(ψ : ℝ → ℝ)
(rE S : ℝ)
(Ps Csy Csk : Matrix (Fin d) (Fin d) ℝ)
(N : Fin d → ℝ)
(P₀ P₁ : ℝ)
(j n : Fin d → ℤ)
(x : Fin (d + d) → ℝ)
:
One lattice term of the unit amplitude.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TrilinearHT.Auto.chartUnitAmplitude_eq_tsum_terms
{d : ℕ}
(χ : (Fin d → ℝ) → ℂ)
(ψ : ℝ → ℝ)
(rE S : ℝ)
(Ps Csy Csk : Matrix (Fin d) (Fin d) ℝ)
(N : Fin d → ℝ)
(P₀ P₁ : ℝ)
(x : Fin (d + d) → ℝ)
:
chartUnitAmplitude χ ψ rE S Ps Csy Csk N P₀ P₁ x = ∑' (j : Fin d → ℤ) (n : Fin d → ℤ), chartUnitTerm χ ψ rE S Ps Csy Csk N P₀ P₁ j n x
theorem
TrilinearHT.Auto.unitSlowCoord_contDiff
{d : ℕ}
(P₁ : ℝ)
(j : Fin d → ℤ)
:
ContDiff ℝ (↑⊤) (unitSlowCoord P₁ j)
theorem
TrilinearHT.Auto.unitHorizCoord_contDiff
{d : ℕ}
(P₀ : ℝ)
:
ContDiff ℝ (↑⊤) (unitHorizCoord P₀)
theorem
TrilinearHT.Auto.chartUnitAmplitude_local
{d : ℕ}
(χ : (Fin d → ℝ) → ℂ)
{ψ : ℝ → ℝ}
(hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0)
(rE : ℝ)
{S H : ℝ}
(hS : 0 < S)
(hχs : ∀ (w : Fin d → ℝ), χ w ≠ 0 → ∀ (i : Fin d), |w i| ≤ H)
(Ps Csy Csk : Matrix (Fin d) (Fin d) ℝ)
(N : Fin d → ℝ)
{P₀ P₁ : ℝ}
(hP₀ : 0 ≤ P₀)
(hP₁ : 0 < P₁)
(x₀ y : Fin (d + d) → ℝ)
(hy : dist y x₀ < 1)
:
chartUnitAmplitude χ ψ rE S Ps Csy Csk N P₀ P₁ y = ∑ j ∈ chartLatticeBox (1 + 2 * S / P₁) fun (i : Fin d) => -x₀ (Fin.castAdd d i),
∑ n ∈ chartLatticeBox (H + P₀) (unitHorizCoord P₀ x₀), chartUnitTerm χ ψ rE S Ps Csy Csk N P₀ P₁ j n y
Near any point the unit amplitude is a finite sum of lattice terms.
theorem
TrilinearHT.Auto.chartUnitAmplitude_eventuallyEq
{d : ℕ}
(χ : (Fin d → ℝ) → ℂ)
{ψ : ℝ → ℝ}
(hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0)
(rE : ℝ)
{S H : ℝ}
(hS : 0 < S)
(hχs : ∀ (w : Fin d → ℝ), χ w ≠ 0 → ∀ (i : Fin d), |w i| ≤ H)
(Ps Csy Csk : Matrix (Fin d) (Fin d) ℝ)
(N : Fin d → ℝ)
{P₀ P₁ : ℝ}
(hP₀ : 0 ≤ P₀)
(hP₁ : 0 < P₁)
(x₀ : Fin (d + d) → ℝ)
:
chartUnitAmplitude χ ψ rE S Ps Csy Csk N P₀ P₁ =ᶠ[nhds x₀] fun (y : Fin (d + d) → ℝ) =>
∑ j ∈ chartLatticeBox (1 + 2 * S / P₁) fun (i : Fin d) => -x₀ (Fin.castAdd d i),
∑ n ∈ chartLatticeBox (H + P₀) (unitHorizCoord P₀ x₀), chartUnitTerm χ ψ rE S Ps Csy Csk N P₀ P₁ j n y
theorem
TrilinearHT.Auto.chartUnitAmplitude_smooth
{d : ℕ}
{χ : (Fin d → ℝ) → ℂ}
(hχ : ContDiff ℝ (↑⊤) χ)
{ψ : ℝ → ℝ}
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0)
(rE : ℝ)
{S H : ℝ}
(hS : 0 < S)
(hχs : ∀ (w : Fin d → ℝ), χ w ≠ 0 → ∀ (i : Fin d), |w i| ≤ H)
(Ps Csy Csk : Matrix (Fin d) (Fin d) ℝ)
(N : Fin d → ℝ)
{P₀ P₁ : ℝ}
(hP₀ : 0 ≤ P₀)
(hP₁ : 0 < P₁)
:
ContDiff ℝ (↑⊤) (chartUnitAmplitude χ ψ rE S Ps Csy Csk N P₀ P₁)
theorem
TrilinearHT.Auto.chartUnitAmplitude_iteratedFDeriv_le
{d : ℕ}
{χ : (Fin d → ℝ) → ℂ}
(hχ : ContDiff ℝ (↑⊤) χ)
{ψ : ℝ → ℝ}
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0)
(rE : ℝ)
{S H : ℝ}
(hS : 0 < S)
(hχs : ∀ (w : Fin d → ℝ), χ w ≠ 0 → ∀ (i : Fin d), |w i| ≤ H)
(Ps Csy Csk : Matrix (Fin d) (Fin d) ℝ)
(N : Fin d → ℝ)
{P₀ P₁ : ℝ}
(hP₀ : 0 ≤ P₀)
(hP₁ : 0 < P₁)
(m : ℕ)
(x₀ : Fin (d + d) → ℝ)
:
‖iteratedFDeriv ℝ m (chartUnitAmplitude χ ψ rE S Ps Csy Csk N P₀ P₁) x₀‖ ≤ ∑ j ∈ chartLatticeBox (1 + 2 * S / P₁) fun (i : Fin d) => -x₀ (Fin.castAdd d i),
∑ n ∈ chartLatticeBox (H + P₀) (unitHorizCoord P₀ x₀),
‖iteratedFDeriv ℝ m (chartUnitTerm χ ψ rE S Ps Csy Csk N P₀ P₁ j n) x₀‖
theorem
TrilinearHT.Auto.tensorCutoff_geomBound
{d : ℕ}
{ψ : ℝ → ℝ}
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψ1 : ∀ (x : ℝ), |ψ x| ≤ 1)
{Kψ : ℕ}
(hK : 1 ≤ Kψ)
(hder : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i ψ x| ≤ (↑Kψ * (↑i + 1)) ^ (Kψ * (i + 1)))
{r : ℝ}
(hr : 0 < r)
(m : ℕ)
(v : Fin d → ℝ)
:
Geometric bounds for a tensor Gevrey cutoff at radius r.
theorem
TrilinearHT.Auto.chartAmplitude_geomBound
{k d c₀ : ℕ}
{H : ℝ}
{A : MultivariableQuadraticChartData k d}
(hA : MultivariableQuadraticChartComplexity c₀ H A)
(hc : 1 ≤ c₀)
(m : ℕ)
(w : Fin d → ℝ)
:
Geometric bounds for the chart amplitude from its complexity.
theorem
TrilinearHT.Auto.GeomBound.add
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f g : E → F}
(hf : ContDiff ℝ (↑⊤) f)
(hg : ContDiff ℝ (↑⊤) g)
{x : E}
{K₁ K₂ R : ℝ}
{m : ℕ}
(h₁ : GeomBound f x K₁ R m)
(h₂ : GeomBound g x K₂ R m)
:
The slow-coordinate projection ℝ^(d+d) → ℝᵈ.
Equations
- TrilinearHT.Auto.slowProjection d = ContinuousLinearMap.pi fun (i : Fin d) => ContinuousLinearMap.proj (Fin.castAdd d i)
Instances For
The horizontal-coordinate projection ℝ^(d+d) → ℝᵈ.
Equations
- TrilinearHT.Auto.horizProjection d = ContinuousLinearMap.pi fun (i : Fin d) => ContinuousLinearMap.proj (Fin.natAdd d i)
Instances For
theorem
TrilinearHT.Auto.chartSlowQuadratic_geomBound
{d : ℕ}
(Csy Csk : Matrix (Fin d) (Fin d) ℝ)
{Bc : ℝ}
(hsy : ∀ (a b : Fin d), |Csy a b| ≤ Bc)
(hsk : ∀ (a b : Fin d), |Csk a b| ≤ Bc)
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(Ls Lw : E →L[ℝ] Fin d → ℝ)
(cs cw : Fin d → ℝ)
{R : ℝ}
(hLs : ‖Ls‖ ≤ R)
(hLw : ‖Lw‖ ≤ R)
(x : E)
{M : ℝ}
(hM1 : 1 ≤ M)
(hs : ∀ (a : Fin d), |(Ls x + cs) a| ≤ M)
(hw : ∀ (a : Fin d), |(Lw x + cw) a| ≤ M)
(m : ℕ)
:
Geometric bounds for the slow quadratic phase at a point whose slow and
remainder coordinates are bounded by M ≥ 1.
theorem
TrilinearHT.Auto.chartUnitTerm_iteratedFDeriv_le
{k d c₀ : ℕ}
{H : ℝ}
{A : MultivariableQuadraticChartData k d}
(hA : MultivariableQuadraticChartComplexity c₀ H A)
(hc : 1 ≤ c₀)
{ψ : ℝ → ℝ}
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψ1 : ∀ (x : ℝ), |ψ x| ≤ 1)
(hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0)
{Kψ : ℕ}
(hK : 1 ≤ Kψ)
(hder : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i ψ x| ≤ (↑Kψ * (↑i + 1)) ^ (Kψ * (i + 1)))
{rE S : ℝ}
(hrE : 0 < rE)
(hS : 0 < S)
(Ps Csy Csk : Matrix (Fin d) (Fin d) ℝ)
{B Bc : ℝ}
(hB : 0 ≤ B)
(hPs : ∀ (i j : Fin d), |Ps i j| ≤ B)
(hsy : ∀ (a b : Fin d), |Csy a b| ≤ Bc)
(hsk : ∀ (a b : Fin d), |Csk a b| ≤ Bc)
(N : Fin d → ℝ)
{P₀ P₁ : ℝ}
(hP₀ : 0 ≤ P₀)
(hP₁ : 0 ≤ P₁)
(j n : Fin d → ℤ)
(m : ℕ)
(x : Fin (d + d) → ℝ)
:
have G := (↑Kψ * (↑m + 1)) ^ (2 * Kψ);
have Kχ := H ^ (2 * c₀) * (↑m + 1) ^ c₀;
have M := 2 * S + H + 1;
have Kφ := ↑d ^ 2 * (2 * Bc * M ^ 2);
have R :=
P₁ * (↑d * (G / S)) + (P₀ * Kχ + (P₁ + P₀ * (↑d * B)) * (↑d * (G / rE)) + (0 + (↑m + 1) * (2 * Real.pi) * (max Kφ 1 * (2 * (P₀ + P₁)))));
‖iteratedFDeriv ℝ m (chartUnitTerm A.amplitude ψ rE S Ps Csy Csk N P₀ P₁ j n) x‖ ≤ Kχ * R ^ m
Blueprint lem:chartfourier, lines 1368–1372: every lattice term of the unit
amplitude has derivatives of order at most m bounded geometrically, with
constants depending only on the cutoff, the chart complexity, the periods and
the entry bounds, and not on the lattice indices j, n.
theorem
TrilinearHT.Auto.chartUnitAmplitude_iteratedFDeriv_bound
{k d c₀ : ℕ}
{H : ℝ}
{A : MultivariableQuadraticChartData k d}
(hA : MultivariableQuadraticChartComplexity c₀ H A)
(hc : 1 ≤ c₀)
{ψ : ℝ → ℝ}
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψ1 : ∀ (x : ℝ), |ψ x| ≤ 1)
(hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0)
{Kψ : ℕ}
(hK : 1 ≤ Kψ)
(hder : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i ψ x| ≤ (↑Kψ * (↑i + 1)) ^ (Kψ * (i + 1)))
{rE S : ℝ}
(hrE : 0 < rE)
(hS : 0 < S)
(Ps Csy Csk : Matrix (Fin d) (Fin d) ℝ)
{B Bc : ℝ}
(hB : 0 ≤ B)
(hPs : ∀ (i j : Fin d), |Ps i j| ≤ B)
(hsy : ∀ (a b : Fin d), |Csy a b| ≤ Bc)
(hsk : ∀ (a b : Fin d), |Csk a b| ≤ Bc)
(N : Fin d → ℝ)
{P₀ P₁ : ℝ}
(hP₀ : 0 ≤ P₀)
(hP₁ : 0 < P₁)
(m : ℕ)
(x : Fin (d + d) → ℝ)
:
have G := (↑Kψ * (↑m + 1)) ^ (2 * Kψ);
have Kχ := H ^ (2 * c₀) * (↑m + 1) ^ c₀;
have M := 2 * S + H + 1;
have Kφ := ↑d ^ 2 * (2 * Bc * M ^ 2);
have R :=
P₁ * (↑d * (G / S)) + (P₀ * Kχ + (P₁ + P₀ * (↑d * B)) * (↑d * (G / rE)) + (0 + (↑m + 1) * (2 * Real.pi) * (max Kφ 1 * (2 * (P₀ + P₁)))));
‖iteratedFDeriv ℝ m (chartUnitAmplitude A.amplitude ψ rE S Ps Csy Csk N P₀ P₁) x‖ ≤ (2 * (1 + 2 * S / P₁) + 3) ^ d * (2 * (H + P₀) + 3) ^ d * (Kχ * R ^ m)
Blueprint lem:chartfourier, lines 1368–1372: a uniform bound on the m-th
derivative of the rescaled periodic amplitude.
The explicit derivative envelope of the unit amplitude at order m.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TrilinearHT.Auto.chartUnitAmplitude_fourier
{k d c₀ : ℕ}
(hd : 1 ≤ d)
{H : ℝ}
{A : MultivariableQuadraticChartData k d}
(hA : MultivariableQuadraticChartComplexity c₀ H A)
(hc : 1 ≤ c₀)
{ψ : ℝ → ℝ}
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψ1 : ∀ (x : ℝ), |ψ x| ≤ 1)
(hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0)
{Kψ : ℕ}
(hK : 1 ≤ Kψ)
(hder : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i ψ x| ≤ (↑Kψ * (↑i + 1)) ^ (Kψ * (i + 1)))
{rE S : ℝ}
(hrE : 0 < rE)
(hS : 0 < S)
(Ps Csy Csk : Matrix (Fin d) (Fin d) ℝ)
(hCsy : Csy.IsSymm)
{B Bc : ℝ}
(hB : 0 ≤ B)
(hPs : ∀ (i j : Fin d), |Ps i j| ≤ B)
(hsy : ∀ (a b : Fin d), |Csy a b| ≤ Bc)
(hsk : ∀ (a b : Fin d), |Csk a b| ≤ Bc)
{P₀ : ℕ}
(hP : ∀ (i j : Fin d), ∃ (z : ℤ), ↑P₀ * Csy i j = ↑z)
(hev : Even P₀)
(N : Fin d → ℝ)
{P₁ : ℝ}
(hP₁ : 0 < P₁)
:
have g := chartUnitAmplitude A.amplitude ψ rE S Ps Csy Csk N (↑P₀) P₁;
(∀ (x : Fin (d + d) → ℝ),
HasSum
(fun (v : Fin (d + d) → ℤ) => periodicFourierCoeff g v * ↑(Real.fourierChar (∑ i : Fin (d + d), ↑(v i) * x i)))
(g x)) ∧ (Summable fun (v : Fin (d + d) → ℤ) => ‖periodicFourierCoeff g v‖) ∧ (∀ (v : Fin (d + d) → ℤ), ‖periodicFourierCoeff g v‖ ≤ chartUnitEnvelope d c₀ Kψ 0 H S rE B Bc (↑P₀) P₁) ∧ ∀ (m : ℕ),
d + d < m →
∀ (v : Fin (d + d) → ℤ),
v ≠ 0 →
‖periodicFourierCoeff g v‖ ≤ chartUnitEnvelope d c₀ Kψ m H S rE B Bc (↑P₀) P₁ * (√↑(d + d) / (2 * Real.pi * frequencyLength v)) ^ m
Blueprint lem:chartfourier, lines 1363–1377, for one slow value: the unit
amplitude is the sum of its absolutely convergent Fourier series everywhere,
with coefficient decay of every order m > 2d controlled by the explicit
envelope, and all coefficients bounded by the order-zero envelope.
theorem
TrilinearHT.Auto.hasSum_prod_of_fintype
{ι : Type u_1}
{β : Type u_2}
{α : Type u_3}
[Fintype ι]
[AddCommMonoid α]
[TopologicalSpace α]
[ContinuousAdd α]
{f : ι × β → α}
{a : ι → α}
(h : ∀ (i : ι), HasSum (fun (b : β) => f (i, b)) (a i))
:
HasSum f (∑ i : ι, a i)
A finite family of convergent series sums over the product index.
noncomputable def
TrilinearHT.Auto.chartSplitFrequency
{d : ℕ}
(Q Csk : Matrix (Fin d) (Fin d) ℝ)
(q₀ : ℕ)
(P₀ P₁ : ℝ)
(ν : Fin d → ℤ)
(v : Fin (d + d) → ℤ)
:
The real frequency attached to the slow value ν / q₀ and Fourier index v:
σ = -P_f C_sk N + P_s p / P₁ + ℓ / P₀ (lem:chartfourier, line 1366).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TrilinearHT.Auto.chart_split_fourier_hasSum
{k d c₀ : ℕ}
(hd : 1 ≤ d)
{H : ℝ}
{A : MultivariableQuadraticChartData k d}
(hA : MultivariableQuadraticChartComplexity c₀ H A)
(hc : 1 ≤ c₀)
{ψ : ℝ → ℝ}
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψ1 : ∀ (x : ℝ), |ψ x| ≤ 1)
(hψe : ∀ (x : ℝ), |x| ≤ 1 → ψ x = 1)
(hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0)
{Kψ : ℕ}
(hK : 1 ≤ Kψ)
(hder : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i ψ x| ≤ (↑Kψ * (↑i + 1)) ^ (Kψ * (i + 1)))
(Q : Matrix (Fin d) (Fin d) ℝ)
(hQ : Q.IsSymm)
(hiso :
(1 - Q).transpose * ((A.matrix.map fun (q : ℚ) => ↑q) - (A.matrix.map fun (q : ℚ) => ↑q).transpose) * (1 - Q) = 0)
{q₀ : ℕ}
(hq : 0 < q₀)
(hqQ : ∀ (i j : Fin d), ∃ (z : ℤ), ↑q₀ * Q i j = ↑z)
{B Bc : ℝ}
(hB : 0 ≤ B)
(hQB : ∀ (i j : Fin d), |Q i j| ≤ B)
(hsy : ∀ (a b : Fin d), |realSymmetricPart (A.matrix.map fun (q : ℚ) => ↑q) a b| ≤ Bc)
(hsk : ∀ (a b : Fin d), |realSkewPart (A.matrix.map fun (q : ℚ) => ↑q) a b| ≤ Bc)
{P₀ : ℕ}
(hP₀ : 0 < P₀)
(hP : ∀ (i j : Fin d), ∃ (z : ℤ), ↑P₀ * realSymmetricPart (A.matrix.map fun (q : ℚ) => ↑q) i j = ↑z)
(hev : Even P₀)
{S P₁ : ℝ}
(hS : 0 < S)
(hP₁ : 4 * S ≤ P₁)
{K : ℕ}
(hKb : ↑q₀ * (S + ↑d * B * H) ≤ ↑K)
(z : Fin k → ℝ)
(hz : ∀ (i : Fin d), |Q.mulVec (A.horizontal.mulVec z) i| ≤ S)
:
have C := A.matrix.map fun (q : ℚ) => ↑q;
have Csy := realSymmetricPart C;
have Csk := realSkewPart C;
have u := A.horizontal.mulVec z;
have g := fun (ν : Fin d → ℤ) =>
chartUnitAmplitude A.amplitude ψ (1 / (3 * ↑q₀)) S Q Csy Csk (fun (i : Fin d) => ↑(ν i) / ↑q₀) (↑P₀) P₁;
HasSum
(fun (p : ↥(slowValueBox d K) × (Fin (d + d) → ℤ)) =>
periodicFourierCoeff (g ↑p.1) p.2 * ↑(Real.fourierChar (chartSplitFrequency Q Csk q₀ (↑P₀) P₁ (↑p.1) p.2 ⬝ᵥ u)))
(↑(Real.fourierChar
(-(z ⬝ᵥ (effectiveReturnQuadratic C A.quadratic A.horizontal ((1 - Q) * A.horizontal) (Q * A.horizontal)).mulVec
z + A.linear ⬝ᵥ z))) * multivariableQuadraticChartAtom A z)
Blueprint lem:chartfourier, eq:chartfourier: on bounded slow values the
chart, with the effective quadratic phase removed, is the absolutely
convergent sum over slow values ν and integer Fourier indices v of
a_{ν,v} e(σ_{ν,v}ᵀ V z).
Power bounds for quasipolynomial budgets #
PowLe W e x records 0 ≤ x ≤ Wᵉ for a base W ≥ 2. It is closed under the
arithmetic operations occurring in the explicit constants, and converts into a
logarithmic bound log x ≤ e log W.
theorem
TrilinearHT.Auto.chartUnitEnvelope_le_pow
{d c₀ Kψ m : ℕ}
{H S rE B Bc P₀ P₁ W : ℝ}
(hW : 2 ≤ W)
(hH1 : 1 ≤ H)
(hHW : H ≤ W)
(hS1 : 1 ≤ S)
(hSW : S ≤ W)
(hrE : 0 < rE)
(hrEW : 1 / rE ≤ W)
(hB : 0 ≤ B)
(hBW : B ≤ W)
(hBc : 0 ≤ Bc)
(hBcW : Bc ≤ W)
(hP₀ : 0 ≤ P₀)
(hP₀W : P₀ ≤ W)
(hP₁ : 1 ≤ P₁)
(hP₁W : P₁ ≤ W)
(hKW : ↑Kψ ≤ W)
(hmW : ↑m + 1 ≤ W)
(hdW : ↑d ≤ W)
(h7 : 7 ≤ W)
:
The derivative envelope is a fixed power of any common bound W of its
parameters; the exponent is linear in the order m and the dimension d.
A fixed Gevrey plateau cutoff: equal to one on [-1,1], vanishing for
|x| ≥ 2, bounded by one, with derivative bounds (K(i+1))^{K(i+1)}.
noncomputable def
TrilinearHT.Auto.chartSplitFrequencyQ
{d : ℕ}
(Q C : Matrix (Fin d) (Fin d) ℚ)
(q₀ P₀ P₁ : ℕ)
(ν : Fin d → ℤ)
(v : Fin (d + d) → ℤ)
:
The rational frequency of lem:chartfourier, line 1366:
σ = -P_f C_sk N + P_s p / P₁ + ℓ / P₀ with N = ν / q₀.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TrilinearHT.Auto.chartSplitFrequencyQ_cast
{d : ℕ}
(Q C : Matrix (Fin d) (Fin d) ℚ)
(q₀ P₀ P₁ : ℕ)
(ν : Fin d → ℤ)
(v : Fin (d + d) → ℤ)
:
(fun (i : Fin d) => ↑(chartSplitFrequencyQ Q C q₀ P₀ P₁ ν v i)) = chartSplitFrequency (Q.map fun (q : ℚ) => ↑q) (realSkewPart (C.map fun (q : ℚ) => ↑q)) q₀ (↑P₀) (↑P₁) ν v
theorem
TrilinearHT.Auto.chartSplitFrequencyQ_int
{d : ℕ}
(Q C : Matrix (Fin d) (Fin d) ℚ)
{q₀ P P₀ P₁ : ℕ}
(hq : 0 < q₀)
(hP : 0 < P)
(hP₀ : 0 < P₀)
(hP₁ : 0 < P₁)
(hqQ : ∀ (i j : Fin d), ∃ (z : ℤ), ↑q₀ * Q i j = ↑z)
(hPC : ∀ (i j : Fin d), ∃ (z : ℤ), ↑P * C i j = ↑z)
(ν : Fin d → ℤ)
(v : Fin (d + d) → ℤ)
(i : Fin d)
:
An explicit common denominator for the frequencies.
theorem
TrilinearHT.Auto.chartSplitFrequency_abs_le
{d : ℕ}
(Q Csk : Matrix (Fin d) (Fin d) ℝ)
{B H K : ℝ}
(hB : 0 ≤ B)
(hQ : ∀ (i j : Fin d), |Q i j| ≤ B)
(hsk : ∀ (i j : Fin d), |Csk i j| ≤ H)
{q₀ P₀ P₁ : ℕ}
(hq : 0 < q₀)
(hP₀ : 0 < P₀)
(hP₁ : 0 < P₁)
(ν : Fin d → ℤ)
(hν : ∀ (i : Fin d), |↑(ν i)| ≤ K)
(v : Fin (d + d) → ℤ)
(i : Fin d)
:
The frequencies grow at most linearly in the Fourier index.
theorem
TrilinearHT.Auto.chartSplitFrequencyQ_height
{d : ℕ}
(Q C : Matrix (Fin d) (Fin d) ℚ)
{B H K : ℝ}
(hB : 0 ≤ B)
(hQ : ∀ (i j : Fin d), |↑(Q i j)| ≤ B)
(hsk : ∀ (i j : Fin d), |realSkewPart (C.map fun (q : ℚ) => ↑q) i j| ≤ H)
{q₀ P P₀ P₁ : ℕ}
(hq : 0 < q₀)
(hP : 0 < P)
(hP₀ : 0 < P₀)
(hP₁ : 0 < P₁)
(hqQ : ∀ (i j : Fin d), ∃ (z : ℤ), ↑q₀ * Q i j = ↑z)
(hPC : ∀ (i j : Fin d), ∃ (z : ℤ), ↑P * C i j = ↑z)
(ν : Fin d → ℤ)
(hν : ∀ (i : Fin d), |↑(ν i)| ≤ K)
(v : Fin (d + d) → ℤ)
(i : Fin d)
:
Heights of the rational frequencies (lem:chartfourier, line 1366).
theorem
TrilinearHT.Auto.fourier_coeff_envelope_bounds
{n : ℕ}
(c : (Fin n → ℤ) → ℂ)
(hsum : Summable fun (v : Fin n → ℤ) => ‖c v‖)
{A : ℕ → ℝ}
(hA : ∀ (m : ℕ), 0 ≤ A m)
(hA0 : ∀ (v : Fin n → ℤ), ‖c v‖ ≤ A 0)
(hAm : ∀ (m : ℕ), n < m → ∀ (v : Fin n → ℤ), v ≠ 0 → ‖c v‖ ≤ A m * (√↑n / (2 * Real.pi * frequencyLength v)) ^ m)
:
(∀ (p : ℕ) (v : Fin n → ℤ),
‖c v‖ * (1 + frequencyLength v) ^ p ≤ max (A 0) (A (p + n + 1) * √↑n ^ (p + n + 1) * 2 ^ p)) ∧ (∀ (p : ℕ) (T : ℝ), 1 ≤ T → (∑ v ∈ frequencyShell n T, ‖c v‖) * T ^ p ≤ 7 ^ n * A (p + n + 1) * √↑n ^ (p + n + 1)) ∧ ∑' (v : Fin n → ℤ), ‖c v‖ ≤ A 0 + 2 * (7 ^ n * A (n + 1) * √↑n ^ (n + 1))
Coefficient bounds from derivative envelopes (lem:chartfourier, lines 1372–1377): a weighted pointwise envelope, dyadic shell bounds of every order, and the total absolute sum.
theorem
TrilinearHT.Auto.chart_split_fourier_explicit
{k d c₀ : ℕ}
(hd : 1 ≤ d)
{H : ℝ}
{A : MultivariableQuadraticChartData k d}
(hA : MultivariableQuadraticChartComplexity c₀ H A)
(hc : 1 ≤ c₀)
{ψ : ℝ → ℝ}
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψ1 : ∀ (x : ℝ), |ψ x| ≤ 1)
(hψe : ∀ (x : ℝ), |x| ≤ 1 → ψ x = 1)
(hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0)
{Kψ : ℕ}
(hK : 1 ≤ Kψ)
(hder : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i ψ x| ≤ (↑Kψ * (↑i + 1)) ^ (Kψ * (i + 1)))
(Q : Matrix (Fin d) (Fin d) ℚ)
(hQ : Q.IsSymm)
(hiso :
(1 - Q.map fun (q : ℚ) => ↑q).transpose * ((A.matrix.map fun (q : ℚ) => ↑q) - (A.matrix.map fun (q : ℚ) => ↑q).transpose) * (1 - Q.map fun (q : ℚ) => ↑q) = 0)
{q₀ : ℕ}
(hq : 0 < q₀)
(hqQ : ∀ (i j : Fin d), ∃ (z : ℤ), ↑q₀ * Q i j = ↑z)
{B : ℝ}
(hB : 0 ≤ B)
(hQB : ∀ (i j : Fin d), |↑(Q i j)| ≤ B)
(hCH : ∀ (i j : Fin d), |↑(A.matrix i j)| ≤ H)
{P : ℕ}
(hP : 0 < P)
(hPC : ∀ (i j : Fin d), ∃ (z : ℤ), ↑P * A.matrix i j = ↑z)
{S : ℝ}
(hS : 0 < S)
{P₁ : ℕ}
(hP₁ : 4 * S ≤ ↑P₁)
{K : ℕ}
(hKb : ↑q₀ * (S + ↑d * B * H) ≤ ↑K)
:
have Env := fun (m : ℕ) => chartUnitEnvelope d c₀ Kψ m H S (1 / (3 * ↑q₀)) B H ↑(2 * P) ↑P₁;
have σ := fun (p : ↥(slowValueBox d K) × (Fin (d + d) → ℤ)) => chartSplitFrequencyQ Q A.matrix q₀ (2 * P) P₁ (↑p.1) p.2;
∃ (a : ↥(slowValueBox d K) × (Fin (d + d) → ℤ) → ℂ),
(∀ (z : Fin k → ℝ),
(∀ (i : Fin d), |(Q.map fun (q : ℚ) => ↑q).mulVec (A.horizontal.mulVec z) i| ≤ S) →
HasSum
(fun (p : ↥(slowValueBox d K) × (Fin (d + d) → ℤ)) =>
a p * ↑(Real.fourierChar ((fun (i : Fin d) => ↑(σ p i)) ⬝ᵥ A.horizontal.mulVec z)))
(↑(Real.fourierChar
(-(z ⬝ᵥ (effectiveReturnQuadratic (A.matrix.map fun (q : ℚ) => ↑q) A.quadratic A.horizontal
((1 - Q.map fun (q : ℚ) => ↑q) * A.horizontal)
((Q.map fun (q : ℚ) => ↑q) * A.horizontal)).mulVec
z + A.linear ⬝ᵥ z))) * multivariableQuadraticChartAtom A z)) ∧ (Summable fun (p : ↥(slowValueBox d K) × (Fin (d + d) → ℤ)) => ‖a p‖) ∧ ∑' (p : ↥(slowValueBox d K) × (Fin (d + d) → ℤ)), ‖a p‖ ≤ ↑(slowValueBox d K).card * (Env 0 + 2 * (7 ^ (d + d) * Env (d + d + 1) * √↑(d + d) ^ (d + d + 1))) ∧ (∀ (J : ℕ) (p : ↥(slowValueBox d K) × (Fin (d + d) → ℤ)),
‖a p‖ * (1 + frequencyLength p.2) ^ (J * (d + 1) ^ 2) ≤ max (Env 0)
(Env (J * (d + 1) ^ 2 + (d + d) + 1) * √↑(d + d) ^ (J * (d + 1) ^ 2 + (d + d) + 1) * 2 ^ (J * (d + 1) ^ 2))) ∧ ∀ (J : ℕ) (T : ℝ),
1 ≤ T →
(∑ f : ↥(slowValueBox d K), ∑ v ∈ frequencyShell (d + d) T, ‖a (f, v)‖) * T ^ (J * (d + 1) ^ 2) ≤ ↑(slowValueBox d K).card * (7 ^ (d + d) * Env (J * (d + 1) ^ 2 + (d + d) + 1) * √↑(d + d) ^ (J * (d + 1) ^ 2 + (d + d) + 1))
lem:chartfourier with explicit parameters, for d ≥ 1: the exact absolutely
convergent expansion on bounded slow values, the total coefficient mass, the
weighted pointwise envelope and the shell bounds, all in terms of the explicit
derivative envelopes of the unit amplitudes.
The quasipolynomial budget of lem:chartfourier #
theorem
TrilinearHT.Auto.chart_split_fourier_dim_zero
{k : ℕ}
(A : MultivariableQuadraticChartData k 0)
(Q : Matrix (Fin 0) (Fin 0) ℚ)
(z : Fin k → ℝ)
:
↑(Real.fourierChar
(-(z ⬝ᵥ (effectiveReturnQuadratic (A.matrix.map fun (q : ℚ) => ↑q) A.quadratic A.horizontal
((1 - Q.map fun (q : ℚ) => ↑q) * A.horizontal) ((Q.map fun (q : ℚ) => ↑q) * A.horizontal)).mulVec
z + A.linear ⬝ᵥ z))) * multivariableQuadraticChartAtom A z = A.amplitude 0
lem:chartfourier when d = 0: the expansion has one term.
theorem
TrilinearHT.Auto.chartBudget_env
{d c₀ Kψ k : ℕ}
{H B R : ℝ}
(hH : Real.exp 2 ≤ H)
(hd : ↑d ≤ Real.log H)
(hB : 2 ≤ B)
(hR : 0 ≤ R)
{P q₀ P₁ : ℕ}
(hq : 0 < q₀)
(hPH : ↑P ≤ H ^ d ^ 2)
(hqB : ↑q₀ ≤ B ^ d ^ 2)
(hP₁1 : 1 ≤ ↑P₁)
(hP₁ : ↑P₁ ≤ 4 * (B * (↑k * R + 1)) + 1)
(m : ℕ)
:
The envelope at order m in exponential form.
theorem
TrilinearHT.Auto.chartBudget_card_height
{d k : ℕ}
{H B R : ℝ}
(hH : Real.exp 2 ≤ H)
(hd : ↑d ≤ Real.log H)
(hB : 2 ≤ B)
(hR : 0 ≤ R)
{P q₀ P₁ K : ℕ}
(hPH : ↑P ≤ H ^ d ^ 2)
(hqB : ↑q₀ ≤ B ^ d ^ 2)
(hP₁ : ↑P₁ ≤ 4 * (B * (↑k * R + 1)) + 1)
(hK : ↑K ≤ ↑q₀ * (B * (↑k * R + 1) + ↑d * B * H) + 1)
:
Budget of the family count and the height denominators of lem:chartfourier.
theorem
TrilinearHT.Auto.chartBudget_order
{d c₀ Kψ m : ℕ}
{X L₀ M : ℝ}
(hX : 1 ≤ X)
(hdX : ↑d ≤ X)
(hL₀ : 0 ≤ L₀)
(hM : 1 ≤ M)
(hmM : ↑m + 1 ≤ M * X ^ 2)
{E : ℝ}
(hE : E ≤ Real.exp (↑(8 * d + 3 * c₀ + (4 * Kψ + 3 * c₀ + 18) * m) * (L₀ + 4 * X ^ 3 + Real.log (↑m + 1))))
:
The envelope at an order m with m + 1 ≤ M X².
theorem
TrilinearHT.Auto.chartBudget_total
{d c₀ Kψ : ℕ}
{X L₀ : ℝ}
(hX : 3 ≤ X)
(hdX : ↑d ≤ X)
(hL₀ : 0 ≤ L₀)
(E : ℕ → ℝ)
(hE0 : ∀ (m : ℕ), 0 ≤ E m)
(hE : ∀ (m : ℕ), E m ≤ Real.exp (↑(8 * d + 3 * c₀ + (4 * Kψ + 3 * c₀ + 18) * m) * (L₀ + 4 * X ^ 3 + Real.log (↑m + 1))))
{card ccard : ℝ}
(hcard : card ≤ Real.exp (ccard * X ^ 6))
:
The total coefficient mass budget.
theorem
TrilinearHT.Auto.chartBudget_J
{d c₀ Kψ : ℕ}
{X L₀ : ℝ}
(hX : 3 ≤ X)
(hdX : ↑d ≤ X)
(hL₀ : 0 ≤ L₀)
(E : ℕ → ℝ)
(hE0 : ∀ (m : ℕ), 0 ≤ E m)
(hE : ∀ (m : ℕ), E m ≤ Real.exp (↑(8 * d + 3 * c₀ + (4 * Kψ + 3 * c₀ + 18) * m) * (L₀ + 4 * X ^ 3 + Real.log (↑m + 1))))
{card ccard : ℝ}
(hcard : card ≤ Real.exp (ccard * X ^ 6))
(hccard : 0 ≤ ccard)
(J : ℕ)
:
have c := (8 + 3 * ↑c₀ + (4 * ↑Kψ + 3 * ↑c₀ + 18) * (4 * ↑J + 4)) * (L₀ + 4 + (4 * ↑J + 4));
max (E 0) (E (J * (d + 1) ^ 2 + (d + d) + 1) * √↑(d + d) ^ (J * (d + 1) ^ 2 + (d + d) + 1) * 2 ^ (J * (d + 1) ^ 2)) ≤ Real.exp ((ccard + c + 8 * ↑J + 8) * X ^ 6) ∧ card * (7 ^ (d + d) * E (J * (d + 1) ^ 2 + (d + d) + 1) * √↑(d + d) ^ (J * (d + 1) ^ 2 + (d + d) + 1)) ≤ Real.exp ((ccard + c + 8 * ↑J + 8) * X ^ 6)
The order-J envelope budget (weighted pointwise and shell forms).