Section 15.2b: Torus sizes and Fourier tests #
This file was automatically generated by Claude.
Formalization of blueprint Section 15, "Common heights and concentration of the core terms"
(sec:core), subsection 2, "Torus norms and Fourier tests" (lines 2482-2583) of
blueprint/formalization_blueprint.tex, from the numbered display eq:torus-size (lines
2489-2496) on: the torus size of the periodic factors of the side states. Split from
Sec15_2TorusNormsFourierTests (which reached the 10,000-line limit) at this numbered item of the
blueprint.
Torus sizes on the side states (blueprint eq:torus-size, lines 2489-2496) #
theorem
TrilinearHT.Auto.eLpNorm_two_toReal_le_add
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[MeasureTheory.IsProbabilityMeasure μ]
{f g : X → ℂ}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
{B : ℝ}
(hgB : ∀ (x : X), ‖g x‖ ≤ B)
{c : ℝ}
(hc : 0 ≤ c)
(hfg : ∀ (x : X), ‖f x‖ ≤ ‖g x‖ + c)
:
A pointwise bound by a bounded measurable function plus a constant bounds the L² norm on a
probability space.
theorem
TrilinearHT.Auto.cell_average_of_approx_Ico
{P Q : ℝ → ℂ}
{η : ℝ}
(hP : Continuous P)
(hQi : IntervalIntegrable (fun (t : ℝ) => ‖Q t‖ ^ 2) MeasureTheory.volume 0 1)
(h : ∀ t ∈ Set.Ico 0 1, ‖P t‖ ≤ ‖Q t‖ + η)
:
cell_average_of_approx with the pointwise comparison on the half-open cell only.
theorem
TrilinearHT.Auto.torus_size_phys_Ico
{d : ℕ}
(V : Submodule ℚ (Fin d → ℚ))
{ι : Type u_1}
{κ : Type u_2}
(F : Finset ι)
(c : ι → ℂ)
(n : ι → Fin d → ℤ)
(ξ : Fin d → ℝ)
{a₀ r xs : ℝ}
(hr : 0 < r)
(hxs : xs ∈ Set.Icc a₀ (a₀ + r))
{ε : ℝ}
(hε : 0 < ε)
(htiny :
∀ k ∈ F,
∀ k' ∈ F,
n k - n k' ∈ rationalIntegerIntersection V →
|2 * Real.pi * r * ∑ i : Fin d, ↑(n k i) * ξ i - 2 * Real.pi * r * ∑ i : Fin d, ↑(n k' i) * ξ i| ≤ ε)
(hhuge :
∀ k ∈ F,
∀ k' ∈ F,
n k - n k' ∉ rationalIntegerIntersection V →
2 / ε ≤ |2 * Real.pi * r * ∑ i : Fin d, ↑(n k i) * ξ i - 2 * Real.pi * r * ∑ i : Fin d, ↑(n k' i) * ξ i|)
(Q : ℝ → ℂ)
(hQ : Measurable Q)
{M : ℝ}
(hQb : ∀ (y : ℝ), ‖Q y‖ ≤ M)
{e : ℝ}
(hpt :
∀ y ∈ Set.Ico a₀ (a₀ + r),
‖∑ k ∈ F, c k * torusCharacter (n k) (torusMk fun (i : Fin d) => ξ i * (y - xs))‖ ≤ ‖Q y‖ + e)
(s : Finset κ)
(A sD : κ → ℝ)
(hA : ∀ i ∈ s, 0 ≤ A i)
(hs : ∀ i ∈ s, 0 ≤ sD i)
{Dst : ℝ}
(hDst : 1 ≤ Dst)
(hcard : ↑s.card ≤ Dst)
(hεD : 2 * ε ≤ Dst ^ (-100))
(hXA : 2 * (r⁻¹ * ∫ (y : ℝ) in a₀..a₀ + r, ‖Q y‖ ^ 2) + 2 * e ^ 2 ≤ 2 * ∑ i ∈ s, A i ^ 2)
(hc : ∑ k ∈ F, ‖c k‖ ≤ ∑ i ∈ s, sD i)
:
(MeasureTheory.eLpNorm
(fun (x : ↥(torusAnnihilator (rationalIntegerIntersection V))) => ∑ k ∈ F, c k * torusCharacter (n k) ↑x) 2
(torusAnnihilatorHaar (rationalIntegerIntersection V))).toReal ≤ √2 * √(∑ i ∈ s, (A i + Dst ^ (-30) * sD i) ^ 2)
torus_size_phys with the physical comparison on the half-open cell [a₀, a₀ + r) only.
noncomputable def
TrilinearHT.Auto.ModeSystem.torusGT
{Gd : RealDyadicGrid}
{Mc : ℕ}
(Ms : ModeSystem Gd Mc)
(S : ModeSchedule)
{U : ℤ × ℤ}
(h : ℕ)
(xs : ℝ)
(F : Finset ↥(Ms.alive U))
(α : ↥(Ms.alive U) → ℂ)
(n : ↥(Ms.alive U) → Fin Ms.zc.dim → ℤ)
(x : StandardTorus Ms.zc.dim)
:
The periodic factor g_j of eq:core-torus-form as a function on the standard torus
(torusG is ℤ^d-periodic; evaluate it at the representatives in [0, 1)^d).
Equations
Instances For
theorem
TrilinearHT.Auto.ModeSystem.continuous_torusG
{Gd : RealDyadicGrid}
{Mc : ℕ}
(Ms : ModeSystem Gd Mc)
(S : ModeSchedule)
(hδ : 0 < Ms.δc)
{U : ℤ × ℤ}
(h : ℕ)
(xs : ℝ)
(F : Finset ↥(Ms.alive U))
(α : ↥(Ms.alive U) → ℂ)
(n : ↥(Ms.alive U) → Fin Ms.zc.dim → ℤ)
:
Continuous (Ms.torusG S h xs F α n)
theorem
TrilinearHT.Auto.ModeSystem.measurable_torusGT
{Gd : RealDyadicGrid}
{Mc : ℕ}
(Ms : ModeSystem Gd Mc)
(S : ModeSchedule)
(hδ : 0 < Ms.δc)
{U : ℤ × ℤ}
(h : ℕ)
(xs : ℝ)
(F : Finset ↥(Ms.alive U))
(α : ↥(Ms.alive U) → ℂ)
(n : ↥(Ms.alive U) → Fin Ms.zc.dim → ℤ)
:
Measurable (Ms.torusGT S h xs F α n)
theorem
TrilinearHT.Auto.ModeSystem.torusG_trunc
{Gd : RealDyadicGrid}
{Mc : ℕ}
(Ms : ModeSystem Gd Mc)
(S : ModeSchedule)
{U : ℤ × ℤ}
(h : ℕ)
(xs : ℝ)
(F : Finset ↥(Ms.alive U))
(α : ↥(Ms.alive U) → ℂ)
(n : ↥(Ms.alive U) → Fin Ms.zc.dim → ℤ)
(K : ℕ)
(cc : (Fin Ms.zc.dim → ℤ) → ℂ)
{τ : ℝ}
(hccT :
∀ (w : Fin Ms.zc.dim → ℝ),
‖cutoffP Ms.δc Ms.ρ w - ∑ v ∈ frequencyBox Ms.zc.dim (2 ^ (K + 1)), cc v * ↑(Real.fourierChar (∑ i : Fin Ms.zc.dim, ↑(v i) * w i))‖ ≤ τ)
(u : Fin Ms.zc.dim → ℝ)
:
Blueprint lines 2470-2476 for the periodic factor ("use the true cutoff first ... and then its
Fourier truncation"): replacing the true periodic cutoff by its truncation Σ_v cc_v e(v·w)
(within τ) turns g_j(u) into the torus trigonometric polynomial with frequencies
Q₀ L_h v + n_m, up to τ Σ_m |α_m|.
noncomputable def
TrilinearHT.Auto.ModeSystem.selComps
{Gd : RealDyadicGrid}
{Mc : ℕ}
(Ms : ModeSystem Gd Mc)
(S : ModeSchedule)
(hA : 6 ≤ S.A0)
(b : ℤ)
(J : ℤ × ℤ)
(F : Finset ↥(Ms.alive (ancAt Gd J (b - 4 * ↑S.K))))
:
The selected modes F grouped by their minimal CURRENT components: the sets D of
eq:torus-size ("D selected").
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TrilinearHT.Auto.ModeSystem.selComps_biUnion
{Gd : RealDyadicGrid}
{Mc : ℕ}
(Ms : ModeSystem Gd Mc)
(S : ModeSchedule)
(hA : 6 ≤ S.A0)
(b : ℤ)
(J : ℤ × ℤ)
(F : Finset ↥(Ms.alive (ancAt Gd J (b - 4 * ↑S.K))))
:
theorem
TrilinearHT.Auto.ModeSystem.selComps_subset
{Gd : RealDyadicGrid}
{Mc : ℕ}
(Ms : ModeSystem Gd Mc)
(S : ModeSchedule)
(hA : 6 ≤ S.A0)
{b : ℤ}
{J : ℤ × ℤ}
{F : Finset ↥(Ms.alive (ancAt Gd J (b - 4 * ↑S.K)))}
{D : Finset Ms.Md}
(hD : D ∈ Ms.selComps S hA b J F)
:
D ⊆ Finset.map { toFun := Subtype.val, inj' := ⋯ } F
theorem
TrilinearHT.Auto.ModeSystem.selComps_not_mem
{Gd : RealDyadicGrid}
{Mc : ℕ}
(Ms : ModeSystem Gd Mc)
(S : ModeSchedule)
(hA : 6 ≤ S.A0)
{b : ℤ}
{J : ℤ × ℤ}
{F : Finset ↥(Ms.alive (ancAt Gd J (b - 4 * ↑S.K)))}
{D D' : Finset Ms.Md}
(hD : D ∈ Ms.selComps S hA b J F)
(hD' : D' ∈ Ms.selComps S hA b J F)
(hne : D ≠ D')
{a a' : ↥(Ms.alive (ancAt Gd J (b - 4 * ↑S.K)))}
(ha : ↑a ∈ D)
(ha' : ↑a' ∈ D')
:
a' ∉ (Ms.blockComps S hA b J).F 0 a
Modes of two different selected groups lie in different minimal CURRENT components.
theorem
TrilinearHT.Auto.ModeSystem.selComps_disjoint
{Gd : RealDyadicGrid}
{Mc : ℕ}
(Ms : ModeSystem Gd Mc)
(S : ModeSchedule)
(hA : 6 ≤ S.A0)
{b : ℤ}
{J : ℤ × ℤ}
{F : Finset ↥(Ms.alive (ancAt Gd J (b - 4 * ↑S.K)))}
{D D' : Finset Ms.Md}
(hD : D ∈ Ms.selComps S hA b J F)
(hD' : D' ∈ Ms.selComps S hA b J F)
(hne : D ≠ D')
:
Disjoint D D'
theorem
TrilinearHT.Auto.torus_floor_budget
{ι : Type u_1}
(s : Finset ι)
(sv : ι → ℝ)
{Dst τ Sα : ℝ}
(hD : 1 ≤ Dst)
(hτ0 : 0 ≤ τ)
(hτ : τ ≤ (Dst ^ 300)⁻¹)
(hSα : Sα ^ 2 ≤ Dst * ∑ i ∈ s, sv i ^ 2)
:
The budget of the floors in eq:torus-size: with Σ_D coefficient sums s_D,
S_α² ≤ D_* Σ_D s_D², the torus-form error D_*^{-150} + τ_c and the truncation tail
τ_c ≤ D_*^{-300} are absorbed by the floors b_D = D_*^{-30} s_D.
theorem
TrilinearHT.Auto.torus_size_final
{ι : Type u_1}
(s : Finset ι)
(a sv : ι → ℝ)
{Dst a' P e : ℝ}
(hD : 1 ≤ Dst)
(ha : ∀ (i : ι), 0 ≤ a i)
(hs : ∀ (i : ι), 0 ≤ sv i)
(he0 : 0 ≤ e)
(hP : P ≤ √2 * √(∑ i ∈ s, (2 * (a i + (Dst ^ 30)⁻¹ * sv i) + (Dst ^ 2) ^ (-30) * (Dst * sv i)) ^ 2))
(ha' : a' ≤ P + e)
(he : e ^ 2 ≤ ∑ i ∈ s, ((Dst ^ 30)⁻¹ * sv i) ^ 2)
:
The final arithmetic of eq:torus-size: from
‖P‖ ≤ √2 (Σ_D (2(a_D + b_D) + (D_*²)^{-30} D_* s_D)²)^{1/2} and a' ≤ ‖P‖ + e with
e² ≤ Σ_D b_D² (b_D = D_*^{-30} s_D), a' ≤ 6 (Σ_D (a_D + b_D)²)^{1/2}.
theorem
TrilinearHT.Auto.ModeSystem.torusGT_eLpNorm_le
{Gd : RealDyadicGrid}
{Mc : ℕ}
(Ms : ModeSystem Gd Mc)
(S : ModeSchedule)
(hδ : 0 < Ms.δc)
{U : ℤ × ℤ}
(h : ℕ)
(xs : ℝ)
(F : Finset ↥(Ms.alive U))
(α : ↥(Ms.alive U) → ℂ)
(n : ↥(Ms.alive U) → Fin Ms.zc.dim → ℤ)
(K : ℕ)
(cc : (Fin Ms.zc.dim → ℤ) → ℂ)
{τ : ℝ}
(hτ0 : 0 ≤ τ)
(hccT :
∀ (w : Fin Ms.zc.dim → ℝ),
‖cutoffP Ms.δc Ms.ρ w - ∑ v ∈ frequencyBox Ms.zc.dim (2 ^ (K + 1)), cc v * ↑(Real.fourierChar (∑ i : Fin Ms.zc.dim, ↑(v i) * w i))‖ ≤ τ)
(V : Submodule ℚ (Fin Ms.zc.dim → ℚ))
:
(MeasureTheory.eLpNorm (fun (x : ↥(torusAnnihilator (rationalIntegerIntersection V))) => Ms.torusGT S h xs F α n ↑x) 2
(torusAnnihilatorHaar (rationalIntegerIntersection V))).toReal ≤ (MeasureTheory.eLpNorm
(fun (x : ↥(torusAnnihilator (rationalIntegerIntersection V))) =>
∑ p ∈ frequencyBox Ms.zc.dim (2 ^ (K + 1)) ×ˢ F,
cc p.1 * ↑(Real.fourierChar (∑ i : Fin Ms.zc.dim, ↑(p.1 i) * (Ms.zc.θ i * xs))) * (α p.2 * ↑(Real.fourierChar (Ms.phase (↑p.2) xs))) * torusCharacter (↑(S.Q0 * 6 ^ h) • p.1 + n p.2) ↑x)
2 (torusAnnihilatorHaar (rationalIntegerIntersection V))).toReal + τ * ∑ x ∈ F, ‖α x‖
The Haar norm of the periodic factor against that of its truncation (blueprint lines
2470-2476): ‖g‖_{L²(𝓗)} ≤ ‖g_trunc‖_{L²(𝓗)} + τ Σ_m |α_m| (torusG_trunc).
theorem
TrilinearHT.Auto.ModeSystem.selComps_cell_energy
{Gd : RealDyadicGrid}
{Mc : ℕ}
(Ms : ModeSystem Gd Mc)
(S : ModeSchedule)
(hA : 6 ≤ S.A0)
{b : ℤ}
{J I : ℤ × ℤ}
(hJ : J.1 = b - 2 * ↑S.K)
(hIJ : dyadicGridCell Gd I.1 I.2 ⊆ dyadicGridCell Gd J.1 J.2)
(hIt : I.1 ≤ b + ↑S.K)
(hD : 2 ≤ S.Dstar)
(hδ : 0 < Ms.δc)
(hΛ : Ms.Λ ≤ S.Dstar)
(hQ : 1 ≤ S.Q0)
(hDg : gaugeSqNorm Ms.zc.dim Ms.δc ≤ S.Dstar)
{Kf : ℕ}
(hKf : 2 * gaugeTail Ms.zc.dim Ms.δc / 2 ^ Kf * S.Dstar ^ 300 ≤ 1)
(hbox : ↑S.Q0 * 2 ^ (Kf + 1) ≤ S.Eh 0)
(hεw : ∀ (m : Ms.Md), S.Dstar⁻¹ ≤ Ms.L.εM m)
(hcard : ↑(Ms.alive (ancAt Gd J (b - 4 * ↑S.K))).card ≤ S.Dstar)
(F : Finset ↥(Ms.alive (ancAt Gd J (b - 4 * ↑S.K))))
(c : Ms.Md → ℂ)
:
Blueprint lines 2489-2491 ("almost orthogonality of minimal CURRENT components"), the
physical side of eq:torus-size: on an actual cell I ⊆ J of length at least r_{t_b}, the
physical selected sum satisfies ∫_I |Σ_{x ∈ F} α_x ψ_x|² ≤ 2 Σ_D ‖A_D‖² over the selected groups
D (pairings ≤ η |I| between different minimal CURRENT components, actualCell_inner_le).
theorem
TrilinearHT.Auto.ModeSystem.sum_norm_selComps
{Gd : RealDyadicGrid}
{Mc : ℕ}
(Ms : ModeSystem Gd Mc)
(S : ModeSchedule)
(hA : 6 ≤ S.A0)
(b : ℤ)
(J : ℤ × ℤ)
(F : Finset ↥(Ms.alive (ancAt Gd J (b - 4 * ↑S.K))))
(c : Ms.Md → ℂ)
:
The coefficient sum of the selected modes is the sum over the selected groups.
theorem
TrilinearHT.Auto.ModeSystem.trunc_tiny_huge
{Gd : RealDyadicGrid}
{Mc : ℕ}
(Ms : ModeSystem Gd Mc)
(S : ModeSchedule)
(hA6 : 6 ≤ S.A0)
(hBA : S.Bstar ≤ S.A0)
{Kf : ℕ}
(hQB : ↑S.Q0 * 2 ^ (Kf + 1) ≤ S.Bstar)
(hD : 1 ≤ S.Dstar)
(h' : ℕ)
{U : ℤ × ℤ}
(F : Finset ↥(Ms.alive U))
(n : ↥(Ms.alive U) → Fin Ms.zc.dim → ℤ)
(hn : ∀ x ∈ F, ∀ (i : Fin Ms.zc.dim), |↑(n x i)| ≤ S.Dstar * S.Eh h')
(V : Submodule ℚ (Fin Ms.zc.dim → ℚ))
{T r : ℝ}
(hT : 0 < T)
(hr : 0 < r)
(hdich :
∀ (k : Fin Ms.zc.dim → ℤ),
(∀ (i : Fin Ms.zc.dim), |↑(k i)| ≤ 4 * S.Dstar ^ 5 * S.Eh h') →
(k ∈ rationalIntegerIntersection V →
r * |∑ i : Fin Ms.zc.dim, ↑(k i) * Ms.torusξ S h' i| ≤ T⁻¹ / ModeSchedule.Lh h') ∧ (k ∉ rationalIntegerIntersection V →
T / ModeSchedule.Lh h' ≤ r * |∑ i : Fin Ms.zc.dim, ↑(k i) * Ms.torusξ S h' i|))
:
(∀ k ∈ frequencyBox Ms.zc.dim (2 ^ (Kf + 1)) ×ˢ F,
∀ k' ∈ frequencyBox Ms.zc.dim (2 ^ (Kf + 1)) ×ˢ F,
↑(S.Q0 * 6 ^ h') • k.1 + n k.2 - (↑(S.Q0 * 6 ^ h') • k'.1 + n k'.2) ∈ rationalIntegerIntersection V →
|2 * Real.pi * r * ∑ i : Fin Ms.zc.dim, ↑((↑(S.Q0 * 6 ^ h') • k.1 + n k.2) i) * Ms.torusξ S h' i - 2 * Real.pi * r * ∑ i : Fin Ms.zc.dim, ↑((↑(S.Q0 * 6 ^ h') • k'.1 + n k'.2) i) * Ms.torusξ S h' i| ≤ 2 * Real.pi * ModeSchedule.Lh h' / T) ∧ ∀ k ∈ frequencyBox Ms.zc.dim (2 ^ (Kf + 1)) ×ˢ F,
∀ k' ∈ frequencyBox Ms.zc.dim (2 ^ (Kf + 1)) ×ˢ F,
↑(S.Q0 * 6 ^ h') • k.1 + n k.2 - (↑(S.Q0 * 6 ^ h') • k'.1 + n k'.2) ∉ rationalIntegerIntersection V →
2 / (2 * Real.pi * ModeSchedule.Lh h' / T) ≤ |2 * Real.pi * r * ∑ i : Fin Ms.zc.dim, ↑((↑(S.Q0 * 6 ^ h') • k.1 + n k.2) i) * Ms.torusξ S h' i - 2 * Real.pi * r * ∑ i : Fin Ms.zc.dim, ↑((↑(S.Q0 * 6 ^ h') • k'.1 + n k'.2) i) * Ms.torusξ S h' i|
Blueprint lines 2484-2486 for the truncated periodic factor ("for every character difference
needed below, r n·ξ is tiny if n ∈ K_B and huge otherwise"): the frequencies Q₀ L_{h'} v + n_m
of the truncation (cutoff indices v in the Fourier box, shifts |n_m| ≤ D_* E_{h'}) lie in the
box 2 D_*^5 E_{h'}, so the dichotomy on 4 D_*^5 E_{h'} gives the phase alternatives of
cell_average_close with ε = 2π L_{h'}/T.
theorem
TrilinearHT.Auto.ModeSystem.torus_size_of_dichotomy
{Gd : RealDyadicGrid}
{Mc : ℕ}
(Ms : ModeSystem Gd Mc)
(S : ModeSchedule)
(hA : 6 ≤ S.A0)
{b : ℤ}
{J I : ℤ × ℤ}
(hJ : J.1 = b - 2 * ↑S.K)
(hIJ : dyadicGridCell Gd I.1 I.2 ⊆ dyadicGridCell Gd J.1 J.2)
(hIt : I.1 ≤ b + ↑S.K)
(hD : 2 ≤ S.Dstar)
(hδ : 0 < Ms.δc)
(hΛ : Ms.Λ ≤ S.Dstar)
(hQ : 1 ≤ S.Q0)
(hDg : gaugeSqNorm Ms.zc.dim Ms.δc ≤ S.Dstar)
{Kf : ℕ}
(hKf : 2 * gaugeTail Ms.zc.dim Ms.δc / 2 ^ Kf * S.Dstar ^ 300 ≤ 1)
(hQB : ↑S.Q0 * 2 ^ (Kf + 1) ≤ S.Bstar)
(hBA : S.Bstar ≤ S.A0)
(hεw : ∀ (m : Ms.Md), S.Dstar⁻¹ ≤ Ms.L.εM m)
(hcard : ↑(Ms.alive (ancAt Gd J (b - 4 * ↑S.K))).card ≤ S.Dstar)
(h' : ℕ)
(V : Submodule ℚ (Fin Ms.zc.dim → ℚ))
{T : ℝ}
(hT : 0 < T)
(hTL : 4 * Real.pi * ModeSchedule.Lh h' * S.Dstar ^ 200 ≤ T)
(hdich :
∀ (k : Fin Ms.zc.dim → ℤ),
(∀ (i : Fin Ms.zc.dim), |↑(k i)| ≤ 4 * S.Dstar ^ 5 * S.Eh h') →
(k ∈ rationalIntegerIntersection V →
dyadicGridLength Gd I.1 * |∑ i : Fin Ms.zc.dim, ↑(k i) * Ms.torusξ S h' i| ≤ T⁻¹ / ModeSchedule.Lh h') ∧ (k ∉ rationalIntegerIntersection V →
T / ModeSchedule.Lh h' ≤ dyadicGridLength Gd I.1 * |∑ i : Fin Ms.zc.dim, ↑(k i) * Ms.torusξ S h' i|))
(Fsel : Finset ↥(Ms.alive (ancAt Gd J (b - 4 * ↑S.K))))
(c : Ms.Md → ℂ)
(n : ↥(Ms.alive (ancAt Gd J (b - 4 * ↑S.K))) → Fin Ms.zc.dim → ℤ)
(hn : ∀ x ∈ Fsel, ∀ (i : Fin Ms.zc.dim), |↑(n x i)| ≤ S.Dstar * S.Eh h')
{xs : ℝ}
(hxs : xs ∈ dyadicGridCell Gd I.1 I.2)
(ph : ℝ → ℂ)
(hph : ∀ (y : ℝ), ‖ph y‖ = 1)
(hform :
∀ y ∈ dyadicGridCell Gd I.1 I.2,
‖∑ x ∈ Fsel, c ↑x * Ms.wave (↑x) y - ph y * Ms.torusG S h' xs Fsel (fun (x : ↥(Ms.alive (ancAt Gd J (b - 4 * ↑S.K)))) => c ↑x) n
fun (i : Fin Ms.zc.dim) => Ms.torusξ S h' i * (y - xs)‖ ≤ (S.Dstar ^ 150)⁻¹ * ∑ x ∈ Fsel, ‖c ↑x‖)
:
(MeasureTheory.eLpNorm
(fun (x : ↥(torusAnnihilator (rationalIntegerIntersection V))) =>
Ms.torusGT S h' xs Fsel (fun (x : ↥(Ms.alive (ancAt Gd J (b - 4 * ↑S.K)))) => c ↑x) n ↑x)
2 (torusAnnihilatorHaar (rationalIntegerIntersection V))).toReal ≤ 6 * √(∑ E ∈ Ms.selComps S hA b J Fsel,
(‖∑ m ∈ E, c m • Ms.cellMode I m‖ / √(dyadicGridLength Gd I.1) + (S.Dstar ^ 30)⁻¹ * ∑ m ∈ E, ‖c m‖) ^ 2)
Blueprint eq:torus-size (lines 2489-2496) for one role on an actual cell I of the block b
with pre-cell J: let the selected modes F have the torus form eq:core-torus-form on I
(unimodular phase φ, periodic factor g = torusG at the height h' with integer shifts of size
at most D_* E_{h'}, error D_*^{-150} times the coefficient sum), and let every integer frequency
k with |k|_∞ ≤ 4 D_*^5 E_{h'} have |I| k·ξ at most T⁻¹/L_{h'} if k ∈ K_B and at least
T/L_{h'} otherwise (box_dichotomy), with T ≥ 4π L_{h'} D_*^{200}. Then on
𝓗 = (K_B ∩ ℤ^d)^⊥,
‖g‖_{L²(𝓗)} ≤ 6 (Σ_{D selected} (‖A_D‖_{2,I} + D_*^{-30} Σ_{m ∈ D} |α_m|)²)^{1/2},
where D runs over the selected modes grouped by their minimal CURRENT components and
A_D = Σ_{m ∈ D} α_m Ψ_{I,m}.
Proof as in the blueprint: truncate the true cutoff (cutoffP_truncate_all, error
τ_c ≤ D_*^{-300}, coefficient sum at most cutNorm ≤ gaugeSqNorm ≤ D_*, torusGT_eLpNorm_le);
the Haar norm of the truncated trigonometric polynomial differs from its cell average by at most
D_*^{-200} times its squared coefficient sum (trunc_tiny_huge, torus_size_phys_Ico); the cell
average is at most twice the physical one plus the torus-form error, and almost orthogonality of
minimal CURRENT components bounds the physical average by 2 Σ_D ‖A_D‖²_{2,I}
(selComps_cell_energy); the errors are absorbed by the floors (torus_floor_budget,
torus_size_final).
theorem
TrilinearHT.Auto.ModeSystem.selComps_sum_le_compSizeSq
{Gd : RealDyadicGrid}
{Mc : ℕ}
(Ms : ModeSystem Gd Mc)
(S : ModeSchedule)
(hA : 6 ≤ S.A0)
(SP : SideParams)
{b : ℤ}
{J : ℤ × ℤ}
(I : ℤ × ℤ)
{h : ℕ}
{x : ↥(Ms.alive (ancAt Gd J (b - 4 * ↑S.K)))}
(F : Finset ↥(Ms.alive (ancAt Gd J (b - 4 * ↑S.K))))
(hFh : ∀ y ∈ F, y ∈ (Ms.blockComps S hA b J).F h x)
(hunit : ∀ y ∈ F, ∀ z ∈ (Ms.blockComps S hA b J).F 0 y, z ∈ F ↔ Ms.IsCoreAt S hA SP b J ↑z)
(c : Ms.Md → ℂ)
:
When the selected modes are exactly the core modes of a union of minimal CURRENT components
inside F_h(x) (the masks select entire units, blueprint line 2466), every selected group is the
full core part of its minimal CURRENT component, so the sum of eq:torus-size is at most the
component size σ_F² of eq:component-size.
theorem
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.Tt_ge_Lh
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
{Cj CA CT CK : ℕ}
{δs W : ℝ}
(hV : D.S.Valid Cj CA CT CK δs W)
(hCT : 4 ≤ CT)
(hd2 : 2 ≤ D.S.dmax)
(hD : 2 ≤ D.S.Dstar)
(hB : 2 ≤ D.S.Bstar)
(hQ : 1 ≤ D.S.Q0)
(hSP : D.SP = D.S.sideParams δs)
{h' : ℕ}
(hh : h' ≤ D.SP.Jst)
:
At the chosen schedule the large threshold dominates the frequency scale:
4π L_{h'} D_*^{200} ≤ T for h' ≤ J_* (T > H Ξ, H > L_{J_*}, Ξ = D_*^{1000}).
theorem
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.torus_size
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
{Cj CA CT CK : ℕ}
{δs W : ℝ}
(hV : D.S.Valid Cj CA CT CK δs W)
(hCA : 1 ≤ CA)
(hCT : 4 ≤ CT)
(hd2 : 2 ≤ D.S.dmax)
(hD : 2 ≤ D.S.Dstar)
(hB : 2 ≤ D.S.Bstar)
(hQ : 1 ≤ D.S.Q0)
(hSP : D.SP = D.S.sideParams δs)
(I : ℤ × ℤ)
(l : Fin 4)
(G : bf.Grp)
(hdim : (D.Ms l G).zc.dim ≤ D.S.dmax)
(hδ : 0 < (D.Ms l G).δc)
(hDg : gaugeSqNorm (D.Ms l G).zc.dim (D.Ms l G).δc ≤ D.S.Dstar)
{Kf : ℕ}
(hKf : 2 * gaugeTail (D.Ms l G).zc.dim (D.Ms l G).δc / 2 ^ Kf * D.S.Dstar ^ 300 ≤ 1)
(hQB : ↑D.S.Q0 * 2 ^ (Kf + 1) ≤ D.S.Bstar)
(hεw : ∀ (m : (D.Ms l G).Md), D.S.Dstar⁻¹ ≤ (D.Ms l G).L.εM m)
(hcard : ↑((D.Ms l G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))).card ≤ D.S.Dstar)
(hΛ : (D.Ms l G).Λ ≤ D.S.Dstar)
{h : ℕ}
(hh : h ≤ D.SP.Jst)
{m : ↥((D.Ms l G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))}
(hgood :
((D.Ms l G).blockComps D.S ⋯ (A.blkStart D.S.K I.1) (D.preAt I)).Good D.SP.Δ
((D.Ms l G).goodP D.S D.SP (A.blkStart D.S.K I.1)) h m)
(Fsel : Finset ↥((D.Ms l G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))))
(n : ↥((D.Ms l G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))) → Fin (D.Ms l G).zc.dim → ℤ)
(hn : ∀ x ∈ Fsel, ∀ (i : Fin (D.Ms l G).zc.dim), |↑(n x i)| ≤ D.S.Dstar * D.S.Eh (h - D.SP.Δ))
(a : ↥((D.Ms l G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))))
{xs : ℝ}
(hxs : xs ∈ dyadicGridCell A.G I.1 I.2)
(hform :
∀ y ∈ dyadicGridCell A.G I.1 I.2,
‖∑ x ∈ Fsel, D.c l G (A.blkStart D.S.K I.1) (D.preAt I) ↑x * (D.Ms l G).wave (↑x) y - ↑(Real.fourierChar (↑(D.Ms l G).cl * centerPhase (D.Ms l G).zc (D.Ms l G).ρ y)) * ↑(Real.fourierChar ((D.Ms l G).slope (↑a) xs * (y - xs))) * (D.Ms l G).torusG D.S (h - D.SP.Δ) xs Fsel
(fun (x : ↥((D.Ms l G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) =>
D.c l G (A.blkStart D.S.K I.1) (D.preAt I) ↑x)
n fun (i : Fin (D.Ms l G).zc.dim) => (D.Ms l G).torusξ D.S (h - D.SP.Δ) i * (y - xs)‖ ≤ (D.S.Dstar ^ 150)⁻¹ * ∑ x ∈ Fsel, ‖D.c l G (A.blkStart D.S.K I.1) (D.preAt I) ↑x‖)
:
(MeasureTheory.eLpNorm
(fun
(x :
↥(torusAnnihilator
(rationalIntegerIntersection
(tinySpan (fun (i : Fin (D.Ms l G).zc.dim) => (D.Ms l G).zc.θ i / ↑D.S.Q0) D.SP.Hn
(D.SP.Tt⁻¹ / dyadicGridLength A.G (A.blkStart D.S.K I.1 - 2 * ↑D.S.K)))))) =>
(D.Ms l G).torusGT D.S (h - D.SP.Δ) xs Fsel
(fun (x : ↥((D.Ms l G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) =>
D.c l G (A.blkStart D.S.K I.1) (D.preAt I) ↑x)
n ↑x)
2
(torusAnnihilatorHaar
(rationalIntegerIntersection
(tinySpan (fun (i : Fin (D.Ms l G).zc.dim) => (D.Ms l G).zc.θ i / ↑D.S.Q0) D.SP.Hn
(D.SP.Tt⁻¹ / dyadicGridLength A.G (A.blkStart D.S.K I.1 - 2 * ↑D.S.K)))))).toReal ≤ 6 * √(∑ E ∈ (D.Ms l G).selComps D.S ⋯ (A.blkStart D.S.K I.1) (D.preAt I) Fsel,
(‖∑ m ∈ E, D.c l G (A.blkStart D.S.K I.1) (D.preAt I) m • (D.Ms l G).cellMode I m‖ / √(dyadicGridLength A.G I.1) + (D.S.Dstar ^ 30)⁻¹ * ∑ m ∈ E, ‖D.c l G (A.blkStart D.S.K I.1) (D.preAt I) m‖) ^ 2)
Blueprint eq:torus-size (lines 2489-2496) on a leaf cell I of the side states, for the
role l and group G: for a mode m good at a final upper height h ≤ J_* and any selected
modes F with the torus form eq:core-torus-form (core_torus_form: shifts of size at most
D_* E_{h-Δ}, error D_*^{-150} times the coefficient sum, ξ = ϑ/L_{h-Δ}), the periodic factor
g = g_j satisfies on 𝓗 = (K_B ∩ ℤ^d)^⊥
a' = ‖g‖_{L²(𝓗)} ≤ 6 (Σ_{D selected} (‖A_D‖_{2,I} + D_*^{-30} Σ_{m ∈ D} |α_m|)²)^{1/2},
D the selected modes grouped by their minimal CURRENT components, A_D = Σ_{m ∈ D} α_m Ψ_{I,m}.
The tiny/huge alternatives come from box_dichotomy; the schedule facts are those of
size_comparison (gaugeSqNorm ≤ D_*, the Fourier cutoff K_f, private weights at least
D_*^{-1}, at most D_* alive modes, Λ ≤ D_*).
theorem
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.torus_size_compSize
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
{Cj CA CT CK : ℕ}
{δs W : ℝ}
(hV : D.S.Valid Cj CA CT CK δs W)
(hCA : 1 ≤ CA)
(hCT : 4 ≤ CT)
(hd2 : 2 ≤ D.S.dmax)
(hD : 2 ≤ D.S.Dstar)
(hB : 2 ≤ D.S.Bstar)
(hQ : 1 ≤ D.S.Q0)
(hSP : D.SP = D.S.sideParams δs)
(I : ℤ × ℤ)
(l : Fin 4)
(G : bf.Grp)
(hdim : (D.Ms l G).zc.dim ≤ D.S.dmax)
(hδ : 0 < (D.Ms l G).δc)
(hDg : gaugeSqNorm (D.Ms l G).zc.dim (D.Ms l G).δc ≤ D.S.Dstar)
{Kf : ℕ}
(hKf : 2 * gaugeTail (D.Ms l G).zc.dim (D.Ms l G).δc / 2 ^ Kf * D.S.Dstar ^ 300 ≤ 1)
(hQB : ↑D.S.Q0 * 2 ^ (Kf + 1) ≤ D.S.Bstar)
(hεw : ∀ (m : (D.Ms l G).Md), D.S.Dstar⁻¹ ≤ (D.Ms l G).L.εM m)
(hcard : ↑((D.Ms l G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))).card ≤ D.S.Dstar)
(hΛ : (D.Ms l G).Λ ≤ D.S.Dstar)
{h : ℕ}
(hh : h ≤ D.SP.Jst)
{m : ↥((D.Ms l G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))}
(hgood :
((D.Ms l G).blockComps D.S ⋯ (A.blkStart D.S.K I.1) (D.preAt I)).Good D.SP.Δ
((D.Ms l G).goodP D.S D.SP (A.blkStart D.S.K I.1)) h m)
(Fsel : Finset ↥((D.Ms l G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))))
(hFh : ∀ y ∈ Fsel, y ∈ ((D.Ms l G).blockComps D.S ⋯ (A.blkStart D.S.K I.1) (D.preAt I)).F h m)
(hunit :
∀ y ∈ Fsel,
∀ z ∈ ((D.Ms l G).blockComps D.S ⋯ (A.blkStart D.S.K I.1) (D.preAt I)).F 0 y,
z ∈ Fsel ↔ (D.Ms l G).IsCoreAt D.S ⋯ D.SP (A.blkStart D.S.K I.1) (D.preAt I) ↑z)
(n : ↥((D.Ms l G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))) → Fin (D.Ms l G).zc.dim → ℤ)
(hn : ∀ x ∈ Fsel, ∀ (i : Fin (D.Ms l G).zc.dim), |↑(n x i)| ≤ D.S.Dstar * D.S.Eh (h - D.SP.Δ))
(a : ↥((D.Ms l G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))))
{xs : ℝ}
(hxs : xs ∈ dyadicGridCell A.G I.1 I.2)
(hform :
∀ y ∈ dyadicGridCell A.G I.1 I.2,
‖∑ x ∈ Fsel, D.c l G (A.blkStart D.S.K I.1) (D.preAt I) ↑x * (D.Ms l G).wave (↑x) y - ↑(Real.fourierChar (↑(D.Ms l G).cl * centerPhase (D.Ms l G).zc (D.Ms l G).ρ y)) * ↑(Real.fourierChar ((D.Ms l G).slope (↑a) xs * (y - xs))) * (D.Ms l G).torusG D.S (h - D.SP.Δ) xs Fsel
(fun (x : ↥((D.Ms l G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) =>
D.c l G (A.blkStart D.S.K I.1) (D.preAt I) ↑x)
n fun (i : Fin (D.Ms l G).zc.dim) => (D.Ms l G).torusξ D.S (h - D.SP.Δ) i * (y - xs)‖ ≤ (D.S.Dstar ^ 150)⁻¹ * ∑ x ∈ Fsel, ‖D.c l G (A.blkStart D.S.K I.1) (D.preAt I) ↑x‖)
:
(MeasureTheory.eLpNorm
(fun
(x :
↥(torusAnnihilator
(rationalIntegerIntersection
(tinySpan (fun (i : Fin (D.Ms l G).zc.dim) => (D.Ms l G).zc.θ i / ↑D.S.Q0) D.SP.Hn
(D.SP.Tt⁻¹ / dyadicGridLength A.G (A.blkStart D.S.K I.1 - 2 * ↑D.S.K)))))) =>
(D.Ms l G).torusGT D.S (h - D.SP.Δ) xs Fsel
(fun (x : ↥((D.Ms l G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) =>
D.c l G (A.blkStart D.S.K I.1) (D.preAt I) ↑x)
n ↑x)
2
(torusAnnihilatorHaar
(rationalIntegerIntersection
(tinySpan (fun (i : Fin (D.Ms l G).zc.dim) => (D.Ms l G).zc.θ i / ↑D.S.Q0) D.SP.Hn
(D.SP.Tt⁻¹ / dyadicGridLength A.G (A.blkStart D.S.K I.1 - 2 * ↑D.S.K)))))).toReal ≤ 6 * √((D.Ms l G).compSizeSq D.S ⋯ D.SP I (A.blkStart D.S.K I.1) (D.preAt I) h m
(D.c l G (A.blkStart D.S.K I.1) (D.preAt I)))
Blueprint eq:torus-size in the form used for the component bins (line 2582: "for a core role
σ_j bins eq:component-size"): when the selected modes are exactly the core modes of a union of
minimal CURRENT components inside F_h(m) (masks select entire units), a'_j ≤ 6 σ_F with
σ_F² = compSizeSq the component size of eq:component-size.
The four-core tests (blueprint eq:four-tests, lines 2506-2520) #
The dyadic band 2^k of a positive number x ∈ [2^k, 2^{k+1}) (the fixed endpoint convention
of eq:four-tests).
Equations
- TrilinearHT.Auto.dyadicBand x = 2 ^ Int.log 2 x
Instances For
The inner minimum min_{0 ≤ j ≤ 3} r |t' - j q'| of eq:four-tests (fourMu = min(1, ·)).
Equations
- TrilinearHT.Auto.fourInner r A B = (Finset.image (fun (j : Fin 4) => ↑↑j) Finset.univ).inf' TrilinearHT.Auto.fourInner._proof_2 fun (j : ℝ) => r * |B - j * A|
Instances For
noncomputable def
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.U0
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
:
The reference threshold U₀ = D_*^{250} (blueprint line 2506).
Instances For
noncomputable def
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourQ
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(G : bf.Grp)
(I : ℤ × ℤ)
(xs : ℝ)
(a : (j : Fin 4) → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))))
:
The four-core test frequency Q = Σ_j γ_j^* (anchor l' = 0), γ_j^* = ω_{a_j}(x_*) the
slope of the hereditary representative a_j at the path point (blueprint lines 2506-2509).
Instances For
noncomputable def
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourT
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(G : bf.Grp)
(I : ℤ × ℤ)
(xs : ℝ)
(a : (j : Fin 4) → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))))
:
The four-core test frequency T = Σ_j j γ_j^* (blueprint lines 2506-2509).
Instances For
noncomputable def
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fullBox
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(d h' : ℕ)
:
The full box |n|_∞ ≤ B'_{h'} = D_*^5 E_{h'} of eq:frequency-box, as integer vectors.
Instances For
theorem
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.mem_fullBox
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(hD : 0 ≤ D.S.Dstar)
{d h' : ℕ}
{n : Fin d → ℤ}
:
noncomputable def
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourRefSet
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(G : bf.Grp)
(I : ℤ × ℤ)
(xs : ℝ)
(h' : ℕ)
(a : (j : Fin 4) → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))))
:
The candidate references of a four-core tuple (blueprint lines 2510-2513): integer n, m in the
full box with max(|q'|, |t'|) ≤ U₀ R_s, q' = Q + n·ξ, t' = T + m·ξ, R_s = |I|^{-1}, at the
torus height h' (ξ = ϑ/L_{h'} in the chart of the anchor role 0).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourRef
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(G : bf.Grp)
(I : ℤ × ℤ)
(xs : ℝ)
(h' : ℕ)
(a : (j : Fin 4) → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))))
:
The reference of a four-core tuple, chosen by a fixed rule from the candidate references (blueprint line 2514): it depends only on the cell, group, path point, height and representatives, not on masks or sampling histories.
Equations
- D.fourRef G I xs h' a = TrilinearHT.Auto.finPick (D.fourRefSet G I xs h' a)
Instances For
noncomputable def
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourQ'
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(G : bf.Grp)
(I : ℤ × ℤ)
(xs : ℝ)
(h' : ℕ)
(a : (j : Fin 4) → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))))
:
The reference test frequency q' = Q + n·ξ.
Equations
Instances For
noncomputable def
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourT'
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(G : bf.Grp)
(I : ℤ × ℤ)
(xs : ℝ)
(h' : ℕ)
(a : (j : Fin 4) → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))))
:
The reference test frequency t' = T + m·ξ.
Equations
Instances For
def
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourPasses
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(G : bf.Grp)
(I : ℤ × ℤ)
(xs : ℝ)
(h' : ℕ)
(a : (j : Fin 4) → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))))
:
The four-core test (blueprint lines 2519-2520): a tuple is kept when a reference exists and the
inner minimum min_j |t' - j q'| / R_s is at least U₀⁻¹; otherwise it is discarded.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourMuBand
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(G : bf.Grp)
(I : ℤ × ℤ)
(xs : ℝ)
(h' : ℕ)
(a : (j : Fin 4) → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))))
:
The dyadic band μ ≍ min(1, min_j |t' - j q'| / R_s) of eq:four-tests.
Equations
- D.fourMuBand G I xs h' a = TrilinearHT.Auto.dyadicBand (TrilinearHT.Auto.fourMu (TrilinearHT.Auto.dyadicGridLength A.G I.1) (D.fourQ' G I xs h' a) (D.fourT' G I xs h' a))
Instances For
noncomputable def
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourNuBand
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(G : bf.Grp)
(I : ℤ × ℤ)
(xs : ℝ)
(h' : ℕ)
(a : (j : Fin 4) → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))))
:
The dyadic band ν ≍ max(1, |q'|/R_s, |t'|/R_s) of eq:four-tests.
Equations
- D.fourNuBand G I xs h' a = TrilinearHT.Auto.dyadicBand (TrilinearHT.Auto.fourNu (TrilinearHT.Auto.dyadicGridLength A.G I.1) (D.fourQ' G I xs h' a) (D.fourT' G I xs h' a))
Instances For
theorem
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourRef_spec
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(hD : 0 ≤ D.S.Dstar)
{G : bf.Grp}
{I : ℤ × ℤ}
{xs : ℝ}
{h' : ℕ}
{a : (j : Fin 4) → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))}
(hne : (D.fourRefSet G I xs h' a).Nonempty)
:
(∀ (i : Fin (D.Ms 0 G).zc.dim), |↑((D.fourRef G I xs h' a).1 i)| ≤ D.S.Dstar ^ 5 * D.S.Eh h') ∧ (∀ (i : Fin (D.Ms 0 G).zc.dim), |↑((D.fourRef G I xs h' a).2 i)| ≤ D.S.Dstar ^ 5 * D.S.Eh h') ∧ dyadicGridLength A.G I.1 * |D.fourQ' G I xs h' a| ≤ D.U0 ∧ dyadicGridLength A.G I.1 * |D.fourT' G I xs h' a| ≤ D.U0
Blueprint lines 2510-2513: the chosen reference of a tuple with a candidate lies in the full
box and has r |q'|, r |t'| ≤ U₀ (max(|q'|, |t'|) ≤ U₀ R_s).
theorem
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourBands_spec
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(hD : 0 ≤ D.S.Dstar)
(hU : 1 ≤ D.U0)
{G : bf.Grp}
{I : ℤ × ℤ}
{xs : ℝ}
{h' : ℕ}
{a : (j : Fin 4) → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))}
(hp : D.fourPasses G I xs h' a)
:
D.fourMuBand G I xs h' a ≤ fourMu (dyadicGridLength A.G I.1) (D.fourQ' G I xs h' a) (D.fourT' G I xs h' a) ∧ fourMu (dyadicGridLength A.G I.1) (D.fourQ' G I xs h' a) (D.fourT' G I xs h' a) < 2 * D.fourMuBand G I xs h' a ∧ D.U0⁻¹ / 2 < D.fourMuBand G I xs h' a ∧ D.fourMuBand G I xs h' a ≤ 1 ∧ D.fourNuBand G I xs h' a ≤ fourNu (dyadicGridLength A.G I.1) (D.fourQ' G I xs h' a) (D.fourT' G I xs h' a) ∧ fourNu (dyadicGridLength A.G I.1) (D.fourQ' G I xs h' a) (D.fourT' G I xs h' a) < 2 * D.fourNuBand G I xs h' a ∧ 1 ≤ D.fourNuBand G I xs h' a ∧ D.fourNuBand G I xs h' a ≤ D.U0
Blueprint lines 2514-2520 (the bands of a kept tuple): when U₀ ≥ 1, a tuple passing the test
has μ ≤ min(1, min_j |t' - j q'|/R_s) < 2μ with U₀⁻¹/2 < μ ≤ 1, and
ν ≤ max(1, |q'|/R_s, |t'|/R_s) < 2ν with 1 ≤ ν ≤ U₀.
The four-core test and its error (blueprint lines 2522-2530) #
theorem
TrilinearHT.Auto.four_core_principal_of
{κ : LocalKernelClass}
{a₀ r : ℝ}
(hr : 0 < r)
{w : ℝ × ℝ → ℂ}
(hw : IsAdmissibleLocalKernel κ a₀ r w)
(z : ChartTag)
{δ δ'' : ℝ}
(hδ : 0 < δ)
(hδ'' : 0 < δ'')
(ρ : Fin 4 → Fin z.dim → ℝ)
(hρ : ∀ (j : Fin 4) (a : Fin z.dim), ρ j a ∈ Set.Icc 0 1)
{Q0 : ℕ}
(hQ0 : 0 < Q0)
(hQ : ∀ (a b : Fin z.dim), ∃ (k : ℤ), ↑Q0 * ↑(z.C a b) = ↑k)
{Cm : ℝ}
(hCm : ∀ (a b : Fin z.dim), |↑(z.C a b)| ≤ Cm)
{L : ℕ}
(hL : 0 < L)
(Kt : ℕ)
{xs : ℝ}
(hxs : xs ∈ Set.Icc a₀ (a₀ + r))
(γ : Fin 4 → ℝ)
{ι : Fin 4 → Type u_1}
(F : (j : Fin 4) → Finset (ι j))
(c : (j : Fin 4) → ι j → ℂ)
(n : (j : Fin 4) → ι j → Fin z.dim → ℤ)
(f : Fin 4 → ℝ → ℂ)
(hfi :
MeasureTheory.Integrable (fun (zz : ℝ × ℝ) => w zz * ∏ j : Fin 4, f j (realProgressionCoordinate j zz))
MeasureTheory.volume)
{η : ℝ}
(hη : 0 ≤ η)
(hfa :
∀ (j : Fin 4),
∀ y ∈ Set.Icc a₀ (a₀ + r),
‖f j y - ↑(centerCut z δ (ρ j) y) * ↑(Real.fourierChar (↑(slotCoeff j) * centerPhase z (ρ j) y)) * (↑(Real.fourierChar (γ j * (y - xs))) * ∑ k ∈ F j,
c j k * torusCharacter (n j k) (torusMk fun (i : Fin z.dim) => z.θ i / (↑Q0 * ↑L) * (y - xs)))‖ ≤ η * ∑ k ∈ F j, ‖c j k‖)
(hfb : ∀ (j : Fin 4), ∀ y ∈ Set.Icc a₀ (a₀ + r), ‖f j y‖ ≤ ∑ k ∈ F j, ‖c j k‖)
(cc0 : Fin 4 → (Fin z.dim → ℤ) → ℂ)
(hcc0 : ∀ (j : Fin 4) (v : Fin z.dim → ℤ), ‖cc0 j v‖ ≤ 1)
(hccT :
∀ (j : Fin 4) (w : Fin z.dim → ℝ),
‖cutoffP δ (ρ j) w - ∑ v ∈ frequencyBox z.dim (2 ^ (Kt + 1)), cc0 j v * ↑(Real.fourierChar (∑ i : Fin z.dim, ↑(v i) * w i))‖ ≤ cutTail z.dim δ Kt)
(cm0 : (Fin (z.dim + z.dim) → ℤ) → ℂ)
(hcm0 : ∀ (v : Fin (z.dim + z.dim) → ℤ), ‖cm0 v‖ ≤ 1)
(hcmT :
∀ (w : Fin (z.dim + z.dim) → ℝ),
‖gaugeMult δ'' Q0 0 z.C ρ w - ∑ v ∈ frequencyBox (z.dim + z.dim) (2 ^ (Kt + 1)),
cm0 v * ↑(Real.fourierChar (∑ i : Fin (z.dim + z.dim), ↑(v i) * w i))‖ ≤ multTail z.dim δ'' Q0 Cm Kt)
(V : Submodule ℚ (Fin z.dim → ℚ))
(p₀ : (Fin z.dim → ℤ) × (Fin z.dim → ℤ))
{ε₁ H U : ℝ}
(J : ℕ)
(hnear :
∀
x ∈
frequencyBox (z.dim + z.dim) (2 ^ (Kt + 1)) ×ˢ Fintype.piFinset fun (j : Fin 4) => frequencyBox z.dim (2 ^ (Kt + 1)) ×ˢ F j,
expP1 L (Q0 * L) n x - p₀.1 ∈ rationalIntegerIntersection V ∧ expP2 L (Q0 * L) n x - p₀.2 ∈ rationalIntegerIntersection V →
r * |∑ j : Fin 4, γ j + ∑ i : Fin z.dim, ↑(expP1 L (Q0 * L) n x i) * (z.θ i / (↑Q0 * ↑L)) - (∑ j : Fin 4, γ j + ∑ i : Fin z.dim, ↑(p₀.1 i) * (z.θ i / (↑Q0 * ↑L)))| ≤ ε₁ ∧ r * |∑ j : Fin 4, ↑↑j * γ j + ∑ i : Fin z.dim, ↑(expP2 L (Q0 * L) n x i) * (z.θ i / (↑Q0 * ↑L)) - (∑ j : Fin 4, ↑↑j * γ j + ∑ i : Fin z.dim, ↑(p₀.2 i) * (z.θ i / (↑Q0 * ↑L)))| ≤ ε₁)
(hfar :
∀
x ∈
frequencyBox (z.dim + z.dim) (2 ^ (Kt + 1)) ×ˢ Fintype.piFinset fun (j : Fin 4) => frequencyBox z.dim (2 ^ (Kt + 1)) ×ˢ F j,
¬(expP1 L (Q0 * L) n x - p₀.1 ∈ rationalIntegerIntersection V ∧ expP2 L (Q0 * L) n x - p₀.2 ∈ rationalIntegerIntersection V) →
H ≤ r * |∑ j : Fin 4, γ j + ∑ i : Fin z.dim, ↑(expP1 L (Q0 * L) n x i) * (z.θ i / (↑Q0 * ↑L)) - (∑ j : Fin 4, γ j + ∑ i : Fin z.dim, ↑(p₀.1 i) * (z.θ i / (↑Q0 * ↑L)))| ∨ H ≤ r * |∑ j : Fin 4, ↑↑j * γ j + ∑ i : Fin z.dim, ↑(expP2 L (Q0 * L) n x i) * (z.θ i / (↑Q0 * ↑L)) - (∑ j : Fin 4, ↑↑j * γ j + ∑ i : Fin z.dim, ↑(p₀.2 i) * (z.θ i / (↑Q0 * ↑L)))|)
(hA₀ : r * |∑ j : Fin 4, γ j + ∑ i : Fin z.dim, ↑(p₀.1 i) * (z.θ i / (↑Q0 * ↑L))| ≤ U)
(hB₀ : r * |∑ j : Fin 4, ↑↑j * γ j + ∑ i : Fin z.dim, ↑(p₀.2 i) * (z.θ i / (↑Q0 * ↑L))| ≤ U)
(hHU : 1 ≤ H - U)
:
‖localProgressionForm r w f‖ ≤ 2 * localKernelSupBound κ * ((4 * η + (gaugeErr z.dim δ δ'' + 4 * (1 + cutTail z.dim δ Kt) ^ 3 * cutTail z.dim δ Kt + (1 + cutTail z.dim δ Kt) ^ 4 * multTail z.dim δ'' Q0 Cm Kt)) * ∏ j : Fin 4, ∑ k ∈ F j, ‖c j k‖) + (‖fourK a₀ r w xs (∑ j : Fin 4, γ j + ∑ i : Fin z.dim, ↑(p₀.1 i) * (z.θ i / (↑Q0 * ↑L)))
(∑ j : Fin 4, ↑↑j * γ j + ∑ i : Fin z.dim, ↑(p₀.2 i) * (z.θ i / (↑Q0 * ↑L)))‖ * ((1 + multTail z.dim δ'' Q0 Cm Kt) * ∏ j : Fin 4,
(MeasureTheory.eLpNorm
(fun (u : ↥(torusAnnihilator (rationalIntegerIntersection V))) =>
∑ p ∈ frequencyBox z.dim (2 ^ (Kt + 1)) ×ˢ F j,
cc0 j p.1 * ↑(Real.fourierChar (∑ i : Fin z.dim, ↑(p.1 i) * (z.θ i * xs))) * c j p.2 * torusCharacter (↑(Q0 * L) • p.1 + n j p.2) ↑u)
2 (torusAnnihilatorHaar (rationalIntegerIntersection V))).toReal) + max ((Real.pi * kerC κ 0 + 2 * (2 * 4 * (2 * 4 * (2 * Real.pi * 4 * kernelDerivBound κ 0)))) * ε₁)
(kerC κ J * ((H - U) ^ J)⁻¹) * ∑
x ∈
frequencyBox (z.dim + z.dim) (2 ^ (Kt + 1)) ×ˢ Fintype.piFinset fun (j : Fin 4) => frequencyBox z.dim (2 ^ (Kt + 1)) ×ˢ F j,
‖cm0 x.1 * ↑(Real.fourierChar (∑ a : Fin z.dim, ↑(x.1 (Fin.castAdd z.dim a)) * (z.θ a * xs / ↑Q0))) * ∏ j : Fin 4,
cc0 j (x.2 j).1 * ↑(Real.fourierChar (∑ i : Fin z.dim, ↑((x.2 j).1 i) * (z.θ i * xs))) * c j (x.2 j).2‖)
Blueprint lines 2522-2530 for one four-core tuple on a cell, with the Fourier truncations made
explicit: let the four inputs be close to the torus forms of a common chart (four_core_product),
let cc0_j truncate the true periodic cutoffs and cm0 the gauge multiplier (eq:gauge-cancel)
within τ_c, τ_m, and let the expansion frequencies have the tiny/huge coset structure around a
moderate reference (p₀, A₀, B₀) (eq:gap, eq:four-tests). Then, with the phase-corrected
coefficients cc_j(v) = cc0_j(v) e(v·θ x*) and cm(v) = cm0(v) e(v₁·θ x*/Q₀), the local form is
at most 2‖w‖_∞ (4η + E_g) Π_j Σ|c_j| + |K₀| (1 + τ_m) Π_j ‖g_j‖_{L²(𝓗)} + max(ε, τ) Σ_x |C_x|:
the characters of D(u, v) = R_z(u, v) Π_j g_j(u + j v) sample the kernel at the expansion
frequencies, the reference coset is replaced by its reference value, the other cosets have rapidly
decreasing Fourier tails (fourK_reference), the retained coset coefficient is bounded by
eq:Haar-four (four_core_cell_bound), and the truncated multiplier R_z is bounded by
1 + τ_m on 𝓗² (multTrunc_sup).
theorem
TrilinearHT.Auto.ModeSystem.torusG_line_eq
{Gd : RealDyadicGrid}
{Mc : ℕ}
(Ms : ModeSystem Gd Mc)
(S : ModeSchedule)
{U : ℤ × ℤ}
(h : ℕ)
(xs : ℝ)
(F : Finset ↥(Ms.alive U))
(α : ↥(Ms.alive U) → ℂ)
(n : ↥(Ms.alive U) → Fin Ms.zc.dim → ℤ)
(hQ : 0 < S.Q0)
(s y : ℝ)
:
(↑(Real.fourierChar (↑Ms.cl * centerPhase Ms.zc Ms.ρ y)) * ↑(Real.fourierChar (s * (y - xs))) * Ms.torusG S h xs F α n fun (i : Fin Ms.zc.dim) => Ms.torusξ S h i * (y - xs)) = ↑(centerCut Ms.zc Ms.δc Ms.ρ y) * ↑(Real.fourierChar (↑Ms.cl * centerPhase Ms.zc Ms.ρ y)) * (↑(Real.fourierChar (s * (y - xs))) * ∑ x ∈ F,
α x * ↑(Real.fourierChar (Ms.phase (↑x) xs)) * torusCharacter (n x) (torusMk fun (i : Fin Ms.zc.dim) => Ms.zc.θ i / (↑S.Q0 * ↑(6 ^ h)) * (y - xs)))
The torus form of core_torus_form in the shape of the four-core estimate: along the cell line
u = ξ(y - x*) the true periodic cutoff is the chart cutoff at y, so the periodic factor is the
gauge cutoff times Σ_m (α_m e(φ_m(x*))) χ_{n_m}(ξ(y - x*)) with ξ = θ/(Q₀ 6^h).
theorem
TrilinearHT.Auto.ModeSystem.trunc_eLpNorm_le_torusGT
{Gd : RealDyadicGrid}
{Mc : ℕ}
(Ms : ModeSystem Gd Mc)
(S : ModeSchedule)
(hδ : 0 < Ms.δc)
{U : ℤ × ℤ}
(h : ℕ)
(xs : ℝ)
(F : Finset ↥(Ms.alive U))
(α : ↥(Ms.alive U) → ℂ)
(n : ↥(Ms.alive U) → Fin Ms.zc.dim → ℤ)
(K : ℕ)
(cc : (Fin Ms.zc.dim → ℤ) → ℂ)
{τ : ℝ}
(hτ0 : 0 ≤ τ)
(hccT :
∀ (w : Fin Ms.zc.dim → ℝ),
‖cutoffP Ms.δc Ms.ρ w - ∑ v ∈ frequencyBox Ms.zc.dim (2 ^ (K + 1)), cc v * ↑(Real.fourierChar (∑ i : Fin Ms.zc.dim, ↑(v i) * w i))‖ ≤ τ)
(V : Submodule ℚ (Fin Ms.zc.dim → ℚ))
:
(MeasureTheory.eLpNorm
(fun (x : ↥(torusAnnihilator (rationalIntegerIntersection V))) =>
∑ p ∈ frequencyBox Ms.zc.dim (2 ^ (K + 1)) ×ˢ F,
cc p.1 * ↑(Real.fourierChar (∑ i : Fin Ms.zc.dim, ↑(p.1 i) * (Ms.zc.θ i * xs))) * (α p.2 * ↑(Real.fourierChar (Ms.phase (↑p.2) xs))) * torusCharacter (↑(S.Q0 * 6 ^ h) • p.1 + n p.2) ↑x)
2 (torusAnnihilatorHaar (rationalIntegerIntersection V))).toReal ≤ (MeasureTheory.eLpNorm (fun (x : ↥(torusAnnihilator (rationalIntegerIntersection V))) => Ms.torusGT S h xs F α n ↑x) 2
(torusAnnihilatorHaar (rationalIntegerIntersection V))).toReal + τ * ∑ x ∈ F, ‖α x‖
The Haar norm of the truncated periodic factor against that of the true one (blueprint lines
2470-2476): ‖g_trunc‖_{L²(𝓗)} ≤ ‖g‖_{L²(𝓗)} + τ Σ_m |α_m| (torusG_trunc).
theorem
TrilinearHT.Auto.ModeSystem.role_transport
{Gd : RealDyadicGrid}
{Mc : ℕ}
(Ms : ModeSystem Gd Mc)
(S : ModeSchedule)
(z : ChartTag)
(hz : Ms.zc = z)
(hδ : 0 < Ms.δc)
(hQ : 0 < S.Q0)
{U : ℤ × ℤ}
(h : ℕ)
(xs : ℝ)
(F : Finset ↥(Ms.alive U))
(α : ↥(Ms.alive U) → ℂ)
(n : ↥(Ms.alive U) → Fin Ms.zc.dim → ℤ)
(K Hn : ℕ)
(thr : ℝ)
:
∃ (ρ' : Fin z.dim → ℝ) (n' : ↥(Ms.alive U) → Fin z.dim → ℤ),
(∀ (i : Fin z.dim), ∃ (k : Fin Ms.zc.dim), ρ' i = Ms.ρ k) ∧ (∀ (x : ↥(Ms.alive U)) (i : Fin z.dim), ∃ (k : Fin Ms.zc.dim), n' x i = n x k) ∧ (∀ (s y : ℝ),
(↑(Real.fourierChar (↑Ms.cl * centerPhase Ms.zc Ms.ρ y)) * ↑(Real.fourierChar (s * (y - xs))) * Ms.torusG S h xs F α n fun (i : Fin Ms.zc.dim) => Ms.torusξ S h i * (y - xs)) = ↑(centerCut z Ms.δc ρ' y) * ↑(Real.fourierChar (↑Ms.cl * centerPhase z ρ' y)) * (↑(Real.fourierChar (s * (y - xs))) * ∑ x ∈ F,
α x * ↑(Real.fourierChar (Ms.phase (↑x) xs)) * torusCharacter (n' x) (torusMk fun (i : Fin z.dim) => z.θ i / (↑S.Q0 * ↑(6 ^ h)) * (y - xs)))) ∧ ∀ (cc0 : (Fin z.dim → ℤ) → ℂ),
(∀ (w : Fin z.dim → ℝ),
‖cutoffP Ms.δc ρ' w - ∑ v ∈ frequencyBox z.dim (2 ^ (K + 1)),
cc0 v * ↑(Real.fourierChar (∑ i : Fin z.dim, ↑(v i) * w i))‖ ≤ cutTail z.dim Ms.δc K) →
(MeasureTheory.eLpNorm
(fun
(u :
↥(torusAnnihilator
(rationalIntegerIntersection (tinySpan (fun (i : Fin z.dim) => z.θ i / ↑S.Q0) Hn thr)))) =>
∑ p ∈ frequencyBox z.dim (2 ^ (K + 1)) ×ˢ F,
cc0 p.1 * ↑(Real.fourierChar (∑ i : Fin z.dim, ↑(p.1 i) * (z.θ i * xs))) * (α p.2 * ↑(Real.fourierChar (Ms.phase (↑p.2) xs))) * torusCharacter (↑(S.Q0 * 6 ^ h) • p.1 + n' p.2) ↑u)
2
(torusAnnihilatorHaar
(rationalIntegerIntersection (tinySpan (fun (i : Fin z.dim) => z.θ i / ↑S.Q0) Hn thr)))).toReal ≤ (MeasureTheory.eLpNorm
(fun
(u :
↥(torusAnnihilator
(rationalIntegerIntersection
(tinySpan (fun (i : Fin Ms.zc.dim) => Ms.zc.θ i / ↑S.Q0) Hn thr)))) =>
Ms.torusGT S h xs F α n ↑u)
2
(torusAnnihilatorHaar
(rationalIntegerIntersection
(tinySpan (fun (i : Fin Ms.zc.dim) => Ms.zc.θ i / ↑S.Q0) Hn thr)))).toReal + cutTail z.dim Ms.δc K * ∑ x ∈ F, ‖α x‖
Transport of one role to a common chart tag z = Ms.zc (blueprint line 2470: the four roles
of a group share their chart tag): the offsets ρ', the integer shifts n', the torus form along
the cell line in the chart z, and the Haar norms of the truncated periodic factors on the
annihilator torus of z against the true periodic factor of the role.
theorem
TrilinearHT.Auto.cell_input_patch
{a₀ r : ℝ}
(Q P : ℝ → ℂ)
(hQ : Measurable Q)
{η M : ℝ}
(hη : 0 ≤ η)
(happ : ∀ y ∈ Set.Ico a₀ (a₀ + r), ‖Q y - P y‖ ≤ η)
(hQb : ∀ (y : ℝ), ‖Q y‖ ≤ M)
(hPb : ‖P (a₀ + r)‖ ≤ M)
:
A role input on the closed cell [a₀, a₀ + r]: the selected sum Q on the half-open cell,
patched at the right endpoint by its torus approximation P (the local form only sees the cell
a.e.).
theorem
TrilinearHT.Auto.gaugeMult_truncate_all
{d : ℕ}
{δ : ℝ}
(hδ : 0 < δ)
(Q0 : ℕ)
(l' : Fin 4)
(C : Matrix (Fin d) (Fin d) ℚ)
(ρ : Fin 4 → Fin d → ℝ)
(hρ : ∀ (j : Fin 4) (a : Fin d), ρ j a ∈ Set.Icc 0 1)
(hQ : ∀ (a b : Fin d), ∃ (z : ℤ), ↑Q0 * ↑(C a b) = ↑z)
{Cm : ℝ}
(hCm0 : 0 ≤ Cm)
(hCm : ∀ (a b : Fin d), |↑(C a b)| ≤ Cm)
(K : ℕ)
:
∃ (c : (Fin (d + d) → ℤ) → ℂ),
(∀ (v : Fin (d + d) → ℤ), ‖c v‖ ≤ 1) ∧ (∀ (s : Finset (Fin (d + d) → ℤ)), ∑ v ∈ s, ‖c v‖ ≤ multNorm d δ Q0 Cm) ∧ ∀ (w : Fin (d + d) → ℝ),
‖gaugeMult δ Q0 l' C ρ w - ∑ v ∈ frequencyBox (d + d) (2 ^ (K + 1)), c v * ↑(Real.fourierChar (∑ i : Fin (d + d), ↑(v i) * w i))‖ ≤ multTail d δ Q0 Cm K
gaugeMult_truncate in every dimension (including the zero-dimensional chart), with the full
absolute coefficient bound multNorm (blueprint line 2476: "absolute Fourier costs ... are fixed
powers of D_*").
theorem
TrilinearHT.Auto.expansion_coeff_sum
{d : ℕ}
{ι : Fin 4 → Type u_1}
(B : ℕ)
(F : (j : Fin 4) → Finset (ι j))
(cm : (Fin (d + d) → ℤ) → ℂ)
(cc : Fin 4 → (Fin d → ℤ) → ℂ)
(c : (j : Fin 4) → ι j → ℂ)
:
∑ x ∈ frequencyBox (d + d) B ×ˢ Fintype.piFinset fun (j : Fin 4) => frequencyBox d B ×ˢ F j,
‖cm x.1 * ∏ j : Fin 4, cc j (x.2 j).1 * c j (x.2 j).2‖ = (∑ v ∈ frequencyBox (d + d) B, ‖cm v‖) * ∏ j : Fin 4, (∑ v ∈ frequencyBox d B, ‖cc j v‖) * ∑ k ∈ F j, ‖c j k‖
The absolute coefficient sum of the four-core expansion factors: the multiplier sum times the products of the truncated cutoff sums and the mode coefficient sums.
theorem
TrilinearHT.Auto.expansion_near_far
{d : ℕ}
(V : Submodule ℚ (Fin d → ℚ))
(ξ : Fin d → ℝ)
{r ε₁ H B : ℝ}
(hB : 0 ≤ B)
(hdich :
∀ (k : Fin d → ℤ),
(∀ (i : Fin d), |↑(k i)| ≤ 16 * B) →
(k ∈ rationalIntegerIntersection V → r * |∑ i : Fin d, ↑(k i) * ξ i| ≤ ε₁) ∧ (k ∉ rationalIntegerIntersection V → H ≤ r * |∑ i : Fin d, ↑(k i) * ξ i|))
{ι : Fin 4 → Type u_1}
(L QL Kt : ℕ)
(F : (j : Fin 4) → Finset (ι j))
(n : (j : Fin 4) → ι j → Fin d → ℤ)
(hLb : ∀ v ∈ frequencyBox (d + d) (2 ^ (Kt + 1)), ∀ (i : Fin (d + d)), |↑L * ↑(v i)| ≤ B)
(hQLb : ∀ v ∈ frequencyBox d (2 ^ (Kt + 1)), ∀ (i : Fin d), |↑QL * ↑(v i)| ≤ B)
(hn : ∀ (j : Fin 4), ∀ k ∈ F j, ∀ (i : Fin d), |↑(n j k i)| ≤ B)
(p₀ : (Fin d → ℤ) × (Fin d → ℤ))
(hp₁ : ∀ (i : Fin d), |↑(p₀.1 i)| ≤ B)
(hp₂ : ∀ (i : Fin d), |↑(p₀.2 i)| ≤ B)
(cA cB : ℝ)
:
(∀ x ∈ frequencyBox (d + d) (2 ^ (Kt + 1)) ×ˢ Fintype.piFinset fun (j : Fin 4) => frequencyBox d (2 ^ (Kt + 1)) ×ˢ F j,
expP1 L QL n x - p₀.1 ∈ rationalIntegerIntersection V ∧ expP2 L QL n x - p₀.2 ∈ rationalIntegerIntersection V →
r * |cA + ∑ i : Fin d, ↑(expP1 L QL n x i) * ξ i - (cA + ∑ i : Fin d, ↑(p₀.1 i) * ξ i)| ≤ ε₁ ∧ r * |cB + ∑ i : Fin d, ↑(expP2 L QL n x i) * ξ i - (cB + ∑ i : Fin d, ↑(p₀.2 i) * ξ i)| ≤ ε₁) ∧ ∀ x ∈ frequencyBox (d + d) (2 ^ (Kt + 1)) ×ˢ Fintype.piFinset fun (j : Fin 4) => frequencyBox d (2 ^ (Kt + 1)) ×ˢ F j,
¬(expP1 L QL n x - p₀.1 ∈ rationalIntegerIntersection V ∧ expP2 L QL n x - p₀.2 ∈ rationalIntegerIntersection V) →
H ≤ r * |cA + ∑ i : Fin d, ↑(expP1 L QL n x i) * ξ i - (cA + ∑ i : Fin d, ↑(p₀.1 i) * ξ i)| ∨ H ≤ r * |cB + ∑ i : Fin d, ↑(expP2 L QL n x i) * ξ i - (cB + ∑ i : Fin d, ↑(p₀.2 i) * ξ i)|
Blueprint lines 2523-2526 (the coset hypotheses of the four-core test from the gap): if every
integer frequency of size at most 16 B is tiny (≤ ε₁) in K_B and huge (≥ H) outside, the
multiplier, cutoff and shift indices are at most B and the reference is at most B, then the
expansion frequencies of the four-core test satisfy the near/far hypotheses of
four_core_principal_of around the reference.
theorem
TrilinearHT.Auto.ModeSystem.role_four_input
{Gd : RealDyadicGrid}
{Mc : ℕ}
(Ms : ModeSystem Gd Mc)
(S : ModeSchedule)
(z : ChartTag)
(hz : Ms.zc = z)
(hδ : 0 < Ms.δc)
(hQ : 0 < S.Q0)
{U : ℤ × ℤ}
(h : ℕ)
(xs : ℝ)
(F : Finset ↥(Ms.alive U))
(α : ↥(Ms.alive U) → ℂ)
(n : ↥(Ms.alive U) → Fin Ms.zc.dim → ℤ)
(K Hn : ℕ)
(thr : ℝ)
{a₀ r η : ℝ}
(hη : 0 ≤ η)
(s : ℝ)
(hform :
∀ y ∈ Set.Ico a₀ (a₀ + r),
‖∑ x ∈ F, α x * Ms.wave (↑x) y - ↑(Real.fourierChar (↑Ms.cl * centerPhase Ms.zc Ms.ρ y)) * ↑(Real.fourierChar (s * (y - xs))) * Ms.torusG S h xs F α n fun (i : Fin Ms.zc.dim) => Ms.torusξ S h i * (y - xs)‖ ≤ η * ∑ x ∈ F, ‖α x‖)
:
∃ (ρ' : Fin z.dim → ℝ) (n' : ↥(Ms.alive U) → Fin z.dim → ℤ) (f : ℝ → ℂ),
(∀ (i : Fin z.dim), ∃ (k : Fin Ms.zc.dim), ρ' i = Ms.ρ k) ∧ (∀ (x : ↥(Ms.alive U)) (i : Fin z.dim), ∃ (k : Fin Ms.zc.dim), n' x i = n x k) ∧ Measurable f ∧ (∀ y ∈ Set.Icc a₀ (a₀ + r),
‖f y - ↑(centerCut z Ms.δc ρ' y) * ↑(Real.fourierChar (↑Ms.cl * centerPhase z ρ' y)) * (↑(Real.fourierChar (s * (y - xs))) * ∑ x ∈ F,
α x * ↑(Real.fourierChar (Ms.phase (↑x) xs)) * torusCharacter (n' x)
(torusMk fun (i : Fin z.dim) => z.θ i / (↑S.Q0 * ↑(6 ^ h)) * (y - xs)))‖ ≤ η * ∑ x ∈ F, ‖α x * ↑(Real.fourierChar (Ms.phase (↑x) xs))‖) ∧ (∀ y ∈ Set.Icc a₀ (a₀ + r), ‖f y‖ ≤ ∑ x ∈ F, ‖α x * ↑(Real.fourierChar (Ms.phase (↑x) xs))‖) ∧ ((Set.Ico a₀ (a₀ + r)).indicator f = (Set.Ico a₀ (a₀ + r)).indicator fun (y : ℝ) => ∑ x ∈ F, α x * Ms.wave (↑x) y) ∧ ∀ (cc0 : (Fin z.dim → ℤ) → ℂ),
(∀ (w : Fin z.dim → ℝ),
‖cutoffP Ms.δc ρ' w - ∑ v ∈ frequencyBox z.dim (2 ^ (K + 1)),
cc0 v * ↑(Real.fourierChar (∑ i : Fin z.dim, ↑(v i) * w i))‖ ≤ cutTail z.dim Ms.δc K) →
(MeasureTheory.eLpNorm
(fun
(u :
↥(torusAnnihilator
(rationalIntegerIntersection
(tinySpan (fun (i : Fin z.dim) => z.θ i / ↑S.Q0) Hn thr)))) =>
∑ p ∈ frequencyBox z.dim (2 ^ (K + 1)) ×ˢ F,
cc0 p.1 * ↑(Real.fourierChar (∑ i : Fin z.dim, ↑(p.1 i) * (z.θ i * xs))) * (α p.2 * ↑(Real.fourierChar (Ms.phase (↑p.2) xs))) * torusCharacter (↑(S.Q0 * 6 ^ h) • p.1 + n' p.2) ↑u)
2
(torusAnnihilatorHaar
(rationalIntegerIntersection
(tinySpan (fun (i : Fin z.dim) => z.θ i / ↑S.Q0) Hn thr)))).toReal ≤ (MeasureTheory.eLpNorm
(fun
(u :
↥(torusAnnihilator
(rationalIntegerIntersection
(tinySpan (fun (i : Fin Ms.zc.dim) => Ms.zc.θ i / ↑S.Q0) Hn thr)))) =>
Ms.torusGT S h xs F α n ↑u)
2
(torusAnnihilatorHaar
(rationalIntegerIntersection
(tinySpan (fun (i : Fin Ms.zc.dim) => Ms.zc.θ i / ↑S.Q0) Hn thr)))).toReal + cutTail z.dim Ms.δc K * ∑ x ∈ F, ‖α x‖
One core role of a four-core tuple on a cell [a₀, a₀ + r) in a common chart z = Ms.zc
(blueprint lines 2466-2476): from the torus form of the selected modes (core_torus_form), the
role input on the closed cell (patched at the right end, cell_input_patch) satisfies the
hypotheses of four_core_principal_of with offsets ρ', shifts n' and coefficients
α_m e(φ_m(x*)), and the truncated periodic factors in the chart z have Haar norms at most
that of the true periodic factor of the role plus the truncation tail (role_transport).
theorem
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.Tt_ge_U0
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
{Cj CA CT CK : ℕ}
{δs W : ℝ}
(hV : D.S.Valid Cj CA CT CK δs W)
(hCT : 4 ≤ CT)
(hd2 : 2 ≤ D.S.dmax)
(hD : 2 ≤ D.S.Dstar)
(hB : 2 ≤ D.S.Bstar)
(hQ : 1 ≤ D.S.Q0)
(hSP : D.SP = D.S.sideParams δs)
{h' : ℕ}
(hh : h' ≤ D.SP.Jst)
:
At the chosen schedule L_{h'} (U₀ + 1) ≤ T for h' ≤ J_* (T > H Ξ, H > L_{J_*},
U₀ + 1 = D_*^{250} + 1 ≤ Ξ): the far cosets of the four-core test are separated by more than
one from the reference (H - U ≥ 1 in fourK_reference).
theorem
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.Λc_selected_eq
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
{I : ℤ × ℤ}
(hI : I ∈ A.cells)
(G : bf.Grp)
(Fsel : (j : Fin 4) → Finset ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))))
(f : Fin 4 → ℝ → ℂ)
(hind :
∀ (j : Fin 4),
(Set.Ico (dyadicGridLeft A.G I.1 I.2) (dyadicGridLeft A.G I.1 I.2 + dyadicGridLength A.G I.1)).indicator (f j) = (Set.Ico (dyadicGridLeft A.G I.1 I.2) (dyadicGridLeft A.G I.1 I.2 + dyadicGridLength A.G I.1)).indicator
fun (y : ℝ) => ∑ x ∈ Fsel j, D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x * (D.Ms j G).wave (↑x) y)
:
((fp.Λc I) fun (j : Fin 4) => D.compSub j G I (Finset.map { toFun := Subtype.val, inj' := ⋯ } (Fsel j))) = localProgressionForm (dyadicGridLength A.G I.1) (A.w I) f
The cell form of four selected subtotals on an active cell is the local form of any inputs that agree with the selected wave sums on the half-open cell (blueprint lines 2463-2470).
theorem
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.four_core_test
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
{Cj CA CT CK : ℕ}
{δs W : ℝ}
(hV : D.S.Valid Cj CA CT CK δs W)
(hCA : 1 ≤ CA)
(hCT : 4 ≤ CT)
(hd2 : 2 ≤ D.S.dmax)
(hD : 2 ≤ D.S.Dstar)
(hB : 2 ≤ D.S.Bstar)
(hQ : 1 ≤ D.S.Q0)
(hSP : D.SP = D.S.sideParams δs)
{I : ℤ × ℤ}
(hI : I ∈ A.cells)
(G : bf.Grp)
(hz : ∀ (j : Fin 4), (D.Ms j G).zc = (D.Ms 0 G).zc)
(hdim : (D.Ms 0 G).zc.dim ≤ D.S.dmax)
{δ : ℝ}
(hδ : 0 < δ)
(hδc : ∀ (j : Fin 4), (D.Ms j G).δc = δ)
(hcl : ∀ (j : Fin 4), (D.Ms j G).cl = slotCoeff j)
(hρ : ∀ (j : Fin 4) (k : Fin (D.Ms j G).zc.dim), (D.Ms j G).ρ k ∈ Set.Icc 0 1)
(hQC : ∀ (a b : Fin (D.Ms 0 G).zc.dim), ∃ (k : ℤ), ↑D.S.Q0 * ↑((D.Ms 0 G).zc.C a b) = ↑k)
{Cm : ℝ}
(hCm0 : 0 ≤ Cm)
(hCm : ∀ (a b : Fin (D.Ms 0 G).zc.dim), |↑((D.Ms 0 G).zc.C a b)| ≤ Cm)
{δ'' : ℝ}
(hδ'' : 0 < δ'')
{Kt : ℕ}
(hQB : ↑D.S.Q0 * 2 ^ (Kt + 1) ≤ D.S.Bstar)
(J : ℕ)
{h : ℕ}
(hh : h ≤ D.SP.Jst)
{m₀ : ↥((D.Ms 0 G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))}
(hgood :
((D.Ms 0 G).blockComps D.S ⋯ (A.blkStart D.S.K I.1) (D.preAt I)).Good D.SP.Δ
((D.Ms 0 G).goodP D.S D.SP (A.blkStart D.S.K I.1)) h m₀)
(Fsel : (j : Fin 4) → Finset ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))))
(n :
(j : Fin 4) →
↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))) → Fin (D.Ms j G).zc.dim → ℤ)
(hn : ∀ (j : Fin 4), ∀ x ∈ Fsel j, ∀ (i : Fin (D.Ms j G).zc.dim), |↑(n j x i)| ≤ D.S.Dstar * D.S.Eh (h - D.SP.Δ))
(a : (j : Fin 4) → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))))
{xs : ℝ}
(hxs : xs ∈ dyadicGridCell A.G I.1 I.2)
(hform :
∀ (j : Fin 4),
∀ y ∈ dyadicGridCell A.G I.1 I.2,
‖∑ x ∈ Fsel j, D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x * (D.Ms j G).wave (↑x) y - ↑(Real.fourierChar (↑(D.Ms j G).cl * centerPhase (D.Ms j G).zc (D.Ms j G).ρ y)) * ↑(Real.fourierChar ((D.Ms j G).slope (↑(a j)) xs * (y - xs))) * (D.Ms j G).torusG D.S (h - D.SP.Δ) xs (Fsel j)
(fun (x : ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) =>
D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x)
(n j) fun (i : Fin (D.Ms j G).zc.dim) => (D.Ms j G).torusξ D.S (h - D.SP.Δ) i * (y - xs)‖ ≤ (D.S.Dstar ^ 150)⁻¹ * ∑ x ∈ Fsel j, ‖D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x‖)
(hne : (D.fourRefSet G I xs (h - D.SP.Δ) a).Nonempty)
:
‖(fp.Λc I) fun (j : Fin 4) => D.compSub j G I (Finset.map { toFun := Subtype.val, inj' := ⋯ } (Fsel j))‖ ≤ 2 * localKernelSupBound κ' * ((4 * (D.S.Dstar ^ 150)⁻¹ + (gaugeErr (D.Ms 0 G).zc.dim δ δ'' + 4 * (1 + cutTail (D.Ms 0 G).zc.dim δ Kt) ^ 3 * cutTail (D.Ms 0 G).zc.dim δ Kt + (1 + cutTail (D.Ms 0 G).zc.dim δ Kt) ^ 4 * multTail (D.Ms 0 G).zc.dim δ'' D.S.Q0 Cm Kt)) * ∏ j : Fin 4, ∑ x ∈ Fsel j, ‖D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x‖) + (‖fourK (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1) (A.w I) xs (D.fourQ' G I xs (h - D.SP.Δ) a)
(D.fourT' G I xs (h - D.SP.Δ) a)‖ * ((1 + multTail (D.Ms 0 G).zc.dim δ'' D.S.Q0 Cm Kt) * ∏ j : Fin 4,
((MeasureTheory.eLpNorm
(fun
(u :
↥(torusAnnihilator
(rationalIntegerIntersection
(tinySpan (fun (i : Fin (D.Ms j G).zc.dim) => (D.Ms j G).zc.θ i / ↑D.S.Q0) D.SP.Hn
(D.SP.Tt⁻¹ / dyadicGridLength A.G (A.blkStart D.S.K I.1 - 2 * ↑D.S.K)))))) =>
(D.Ms j G).torusGT D.S (h - D.SP.Δ) xs (Fsel j)
(fun (x : ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) =>
D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x)
(n j) ↑u)
2
(torusAnnihilatorHaar
(rationalIntegerIntersection
(tinySpan (fun (i : Fin (D.Ms j G).zc.dim) => (D.Ms j G).zc.θ i / ↑D.S.Q0) D.SP.Hn
(D.SP.Tt⁻¹ / dyadicGridLength A.G (A.blkStart D.S.K I.1 - 2 * ↑D.S.K)))))).toReal + cutTail (D.Ms 0 G).zc.dim δ Kt * ∑ x ∈ Fsel j, ‖D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x‖)) + max
((Real.pi * kerC κ' 0 + 2 * (2 * 4 * (2 * 4 * (2 * Real.pi * 4 * kernelDerivBound κ' 0)))) * (D.SP.Tt⁻¹ / ModeSchedule.Lh (h - D.SP.Δ)))
(kerC κ' J * ((D.SP.Tt / ModeSchedule.Lh (h - D.SP.Δ) - D.U0) ^ J)⁻¹) * (multNorm (D.Ms 0 G).zc.dim δ'' D.S.Q0 Cm * ∏ j : Fin 4, cutNorm (D.Ms 0 G).zc.dim δ * ∑ x ∈ Fsel j, ‖D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x‖))
Blueprint lines 2522-2530 (the four-core test and its error) on a leaf cell I of the side
states, for a tuple of four core roles of the group G sharing the chart of the anchor role 0:
let F_j be the selected modes of role j with their torus forms eq:core-torus-form at the final
height h ≤ J_* (core_torus_form: representatives a_j, shifts of size at most
D_* E_{h-Δ}, error D_*^{-150}), let the anchor role be good at h, and let the tuple have a
reference for the four-core test eq:four-tests (its fixed-rule reference (q', t'); the
inner-minimum part of the test is not used). Then the cell form of the four selected subtotals is at
most
- the torus-form and gauge errors
2‖w‖_∞ (4 D_*^{-150} + E_g) Π_j Σ_{F_j} |α|(eq:gauge-cancel, truncation tailsτ_c,τ_m, smoothingδ''), plus - the reference kernel sample
|WFourier_s(r q', r t')|times(1 + τ_m) Π_j (a'_j + τ_c Σ_{F_j} |α|), wherea'_j = ‖g_j‖_{L²(𝓗)}is the torus size of the true periodic factor of rolej(eq:torus-size) — the retained coset coefficient, bounded byeq:Haar-fourwith the truncated multiplierR_zbounded by1 + τ_m— plus - the coset errors: the tiny replacement error on the reference coset (frequencies within
T⁻¹/L_{h-Δ}after multiplication byr) and the rapidly decreasing tails of the other cosets (separated byT/L_{h-Δ} - U₀ ≥ 1), times the absolute coefficient summultNorm Π_j (cutNorm Σ_{F_j} |α|)(fixed powers ofD_*by the schedule).
The tiny/huge structure of all expansion frequencies relative to the reference comes from the gap of
a nonexceptional key of the anchor's successful component (box_dichotomy, expansion_near_far);
the kernel sample itself satisfies |WFourier_s(r q', r t')| ν^J ≤ C_J μ (fourK_mu_nu).
theorem
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.four_core_kernel_sample
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
{I : ℤ × ℤ}
(hI : I ∈ A.cells)
(G : bf.Grp)
(xs : ℝ)
(h' : ℕ)
(a : (j : Fin 4) → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))))
(J : ℕ)
:
‖fourK (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1) (A.w I) xs (D.fourQ' G I xs h' a)
(D.fourT' G I xs h' a)‖ * fourNu (dyadicGridLength A.G I.1) (D.fourQ' G I xs h' a) (D.fourT' G I xs h' a) ^ J ≤ fourKC κ' J * fourMu (dyadicGridLength A.G I.1) (D.fourQ' G I xs h' a) (D.fourT' G I xs h' a)
Blueprint lines 2528-2530 at the reference of a four-core tuple: the four marginals give zeros
of WFourier_s(q, t) on the lines t = j q, and smoothness near these lines with rapid decay
give, for
every fixed J, |WFourier_s(r q', r t')| ν^J ≤ C_J μ with μ = min(1, min_j |t' - j q'|/R_s) and
ν = max(1, |q'|/R_s, |t'|/R_s) (fourK_mu_nu).
The three-core tests (blueprint lines 2536-2540) #
noncomputable def
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeQ
(l : Fin 4)
(a : Fin 4 → ℝ)
:
The three-core test frequency Q = Σ_{j ≠ l} γ_j^* for the side role l (blueprint line 2538).
The three-core tests take the tuple a j = γ_j^* = ω_{a_j}(x_*) of the slopes at the path point of
the representatives of the core roles (its side entry is not used).
Equations
Instances For
noncomputable def
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeT
(l : Fin 4)
(a : Fin 4 → ℝ)
:
The anchored three-core test frequency T_l = Σ_{j ≠ l} (j - l) γ_j^* (blueprint line 2538).
Equations
- TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeT l a = ∑ j ∈ Finset.univ.erase l, (↑↑j - ↑↑l) * a j
Instances For
noncomputable def
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeRefSet
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(G : bf.Grp)
(I : ℤ × ℤ)
(_xs : ℝ)
(h' : ℕ)
(l : Fin 4)
(a : Fin 4 → ℝ)
:
The candidate references of a three-core tuple (blueprint line 2540): integer m in the full
box with |T_l + m·ξ| ≤ U₀ R_s (R_s = |I|^{-1}, ξ = ϑ/L_{h'} in the chart of role 0).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeRef
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(G : bf.Grp)
(I : ℤ × ℤ)
(xs : ℝ)
(h' : ℕ)
(l : Fin 4)
(a : Fin 4 → ℝ)
:
The mask-independent reference of a three-core tuple, chosen by a fixed rule (blueprint line 2540).
Equations
- D.threeRef G I xs h' l a = TrilinearHT.Auto.finPick (D.threeRefSet G I xs h' l a)
Instances For
noncomputable def
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeBeta
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(G : bf.Grp)
(I : ℤ × ℤ)
(xs : ℝ)
(h' : ℕ)
(l : Fin 4)
(a : Fin 4 → ℝ)
:
The normalized anchored reference frequency β = r (T_l + m·ξ) (blueprint line 2540).
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threePasses
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(G : bf.Grp)
(I : ℤ × ℤ)
(xs : ℝ)
(h' : ℕ)
(l : Fin 4)
(a : Fin 4 → ℝ)
:
The three-core test (blueprint line 2540): a tuple is kept when a reference exists and
|β| ≥ U₀⁻¹; otherwise it is discarded.
Equations
Instances For
noncomputable def
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeMuBand
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(G : bf.Grp)
(I : ℤ × ℤ)
(xs : ℝ)
(h' : ℕ)
(l : Fin 4)
(a : Fin 4 → ℝ)
:
The dyadic band μ ≍ min(1, |β|) of the three-core test (blueprint line 2540).
Equations
- D.threeMuBand G I xs h' l a = TrilinearHT.Auto.dyadicBand (min 1 |D.threeBeta G I xs h' l a|)
Instances For
noncomputable def
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeNuBand
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(G : bf.Grp)
(I : ℤ × ℤ)
(xs : ℝ)
(h' : ℕ)
(l : Fin 4)
(a : Fin 4 → ℝ)
:
The dyadic band ν ≍ max(1, |β|) of the three-core test (blueprint line 2540).
Equations
- D.threeNuBand G I xs h' l a = TrilinearHT.Auto.dyadicBand (max 1 |D.threeBeta G I xs h' l a|)
Instances For
theorem
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeRef_spec
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(hD : 0 ≤ D.S.Dstar)
{G : bf.Grp}
{I : ℤ × ℤ}
{xs : ℝ}
{h' : ℕ}
{l : Fin 4}
{a : Fin 4 → ℝ}
(hne : (D.threeRefSet G I xs h' l a).Nonempty)
:
Blueprint line 2540: the chosen reference of a three-core tuple with a candidate lies in the
full box and has |β| ≤ U₀.
theorem
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeBands_spec
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(hD : 0 ≤ D.S.Dstar)
(hU : 1 ≤ D.U0)
{G : bf.Grp}
{I : ℤ × ℤ}
{xs : ℝ}
{h' : ℕ}
{l : Fin 4}
{a : Fin 4 → ℝ}
(hp : D.threePasses G I xs h' l a)
:
D.threeMuBand G I xs h' l a ≤ min 1 |D.threeBeta G I xs h' l a| ∧ min 1 |D.threeBeta G I xs h' l a| < 2 * D.threeMuBand G I xs h' l a ∧ D.U0⁻¹ / 2 < D.threeMuBand G I xs h' l a ∧ D.threeMuBand G I xs h' l a ≤ 1 ∧ D.threeNuBand G I xs h' l a ≤ max 1 |D.threeBeta G I xs h' l a| ∧ max 1 |D.threeBeta G I xs h' l a| < 2 * D.threeNuBand G I xs h' l a ∧ 1 ≤ D.threeNuBand G I xs h' l a ∧ D.threeNuBand G I xs h' l a ≤ D.U0
Blueprint line 2540 (the bands of a kept three-core tuple): when U₀ ≥ 1, a tuple passing the
test has μ ≤ min(1, |β|) < 2μ with U₀⁻¹/2 < μ ≤ 1, and ν ≤ max(1, |β|) < 2ν with
1 ≤ ν ≤ U₀.
The three-core cosets (blueprint lines 2542-2547) #
theorem
TrilinearHT.Auto.three_cosets_of_dichotomy
{d : ℕ}
(V : Submodule ℚ (Fin d → ℚ))
(ξ : Fin d → ℝ)
{r ε₁ H B : ℝ}
(hr : 0 < r)
(hB : 0 ≤ B)
(hdich :
∀ (k : Fin d → ℤ),
(∀ (i : Fin d), |↑(k i)| ≤ 64 * B) →
(k ∈ rationalIntegerIntersection V → r * |∑ i : Fin d, ↑(k i) * ξ i| ≤ ε₁) ∧ (k ∉ rationalIntegerIntersection V → H ≤ r * |∑ i : Fin d, ↑(k i) * ξ i|))
(hH : 1 ≤ H)
{ι : Fin 4 → Type u_1}
(L QL Kt : ℕ)
(F : (j : Fin 4) → Finset (ι j))
(n : (j : Fin 4) → ι j → Fin d → ℤ)
(hLb : ∀ v ∈ frequencyBox (d + d) (2 ^ (Kt + 1)), ∀ (i : Fin (d + d)), |↑L * ↑(v i)| ≤ B)
(hQLb : ∀ v ∈ frequencyBox d (2 ^ (Kt + 1)), ∀ (i : Fin d), |↑QL * ↑(v i)| ≤ B)
(hn : ∀ (j : Fin 4), ∀ k ∈ F j, ∀ (i : Fin d), |↑(n j k i)| ≤ B)
(γ : Fin 4 → ℝ)
(l : Fin 4)
(m₀ : Fin d → ℤ)
(hm₀ : ∀ (i : Fin d), |↑(m₀ i)| ≤ B)
{U : ℝ}
(hU : r * |∑ j : Fin 4, ↑↑j * γ j - ↑↑l * ∑ j : Fin 4, γ j + ∑ i : Fin d, ↑(m₀ i) * ξ i| ≤ U)
:
∃ (N : Finset (Fin d → ℤ)) (nref : (Fin (d + d) → ℤ) × ((j : Fin 4) → (Fin d → ℤ) × ι j) → Fin d → ℤ),
(∀ n ∈ N, ∀ (i : Fin d), |↑(n i)| ≤ 16 * B) ∧ (∀ n ∈ N, ∀ n' ∈ N, n ≠ n' → n - n' ∉ rationalIntegerIntersection V) ∧ (∀ n ∈ N,
∀ n' ∈ N,
n ≠ n' →
1 ≤ |-(r * (∑ j : Fin 4, γ j + ∑ i : Fin d, ↑(n i) * ξ i)) - -(r * (∑ j : Fin 4, γ j + ∑ i : Fin d, ↑(n' i) * ξ i))|) ∧ (∀
x ∈
frequencyBox (d + d) (2 ^ (Kt + 1)) ×ˢ Fintype.piFinset fun (j : Fin 4) => frequencyBox d (2 ^ (Kt + 1)) ×ˢ F j,
expP2 L QL n x - ↑↑l • expP1 L QL n x - m₀ ∈ rationalIntegerIntersection V →
nref x ∈ N ∧ expP1 L QL n x - nref x ∈ rationalIntegerIntersection V ∧ |r * (∑ j : Fin 4, γ j + ∑ i : Fin d, ↑(expP1 L QL n x i) * ξ i) - r * (∑ j : Fin 4, γ j + ∑ i : Fin d, ↑(nref x i) * ξ i)| ≤ ε₁ ∧ |r * (∑ j : Fin 4, ↑↑j * γ j + ∑ i : Fin d, ↑(expP2 L QL n x i) * ξ i - ↑↑l * (∑ j : Fin 4, γ j + ∑ i : Fin d, ↑(expP1 L QL n x i) * ξ i)) - r * (∑ j : Fin 4, ↑↑j * γ j - ↑↑l * ∑ j : Fin 4, γ j + ∑ i : Fin d, ↑(m₀ i) * ξ i)| ≤ ε₁) ∧ ∀
x ∈
frequencyBox (d + d) (2 ^ (Kt + 1)) ×ˢ Fintype.piFinset fun (j : Fin 4) => frequencyBox d (2 ^ (Kt + 1)) ×ˢ F j,
expP2 L QL n x - ↑↑l • expP1 L QL n x - m₀ ∉ rationalIntegerIntersection V →
H - U ≤ |r * (∑ j : Fin 4, ↑↑j * γ j + ∑ i : Fin d, ↑(expP2 L QL n x i) * ξ i - ↑↑l * (∑ j : Fin 4, γ j + ∑ i : Fin d, ↑(expP1 L QL n x i) * ξ i))|
Blueprint lines 2542-2547 (the three-core cosets from the tiny/huge dichotomy): let every
integer frequency of size at most 64 B be tiny (r|k·ξ| ≤ ε₁) in K_B and huge (≥ H ≥ 1)
outside, let the multiplier, cutoff and shift indices of the expansion be at most B and the
vertical reference m₀ at most B with r |β₀| ≤ U. Then one reference n per horizontal coset
modulo K_B of the expansion frequencies (cosetRep, "choose one reference n from the box per
coset") gives references N in distinct cosets, at most 16 B, whose real frequencies r(Q + n·ξ)
are more than 1 apart; on the reference vertical coset m₀ + K_B every expansion term is within
ε₁ of its references (replacing the other frequencies of a coset by its reference has tiny error),
and off it the anchored frequency is at least H - U.
theorem
TrilinearHT.Auto.ModeSchedule.Valid.box64_lt_H
{S : ModeSchedule}
{Cj CA CT CK : ℕ}
{δs W : ℝ}
(hV : S.Valid Cj CA CT CK δs W)
(hCA : 1 ≤ CA)
(hd2 : 2 ≤ S.dmax)
(hD : 2 ≤ S.Dstar)
(hB : 2 ≤ S.Bstar)
(hQ : 1 ≤ S.Q0)
{h : ℕ}
(hh : h ≤ S.Jstar)
:
Sixty-four times the frequency box is below H (blueprint lines 2483-2487, "all the boxes
under consideration", including the anchored three-core combinations): 64 D_*^5 E_h < H for
h ≤ J_*.
theorem
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.box_dichotomy64
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
{Cj CA CT CK : ℕ}
{δs W : ℝ}
(hV : D.S.Valid Cj CA CT CK δs W)
(hCA : 1 ≤ CA)
(hCT : 4 ≤ CT)
(hd2 : 2 ≤ D.S.dmax)
(hD : 2 ≤ D.S.Dstar)
(hB : 2 ≤ D.S.Bstar)
(hQ : 1 ≤ D.S.Q0)
(hSP : D.SP = D.S.sideParams δs)
(I : ℤ × ℤ)
(l : Fin 4)
(G : bf.Grp)
(hdim : (D.Ms l G).zc.dim ≤ D.S.dmax)
{h : ℕ}
(hh : h ≤ D.SP.Jst)
{m : ↥((D.Ms l G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))}
(hgood :
((D.Ms l G).blockComps D.S ⋯ (A.blkStart D.S.K I.1) (D.preAt I)).Good D.SP.Δ
((D.Ms l G).goodP D.S D.SP (A.blkStart D.S.K I.1)) h m)
(n : Fin (D.Ms l G).zc.dim → ℤ)
:
(∀ (i : Fin (D.Ms l G).zc.dim), |↑(n i)| ≤ 64 * (D.S.Dstar ^ 5 * D.S.Eh (h - D.SP.Δ))) →
(n ∈ rationalIntegerIntersection
(tinySpan (fun (i : Fin (D.Ms l G).zc.dim) => (D.Ms l G).zc.θ i / ↑D.S.Q0) D.SP.Hn
(D.SP.Tt⁻¹ / dyadicGridLength A.G (A.blkStart D.S.K I.1 - 2 * ↑D.S.K))) →
dyadicGridLength A.G I.1 * |∑ i : Fin (D.Ms l G).zc.dim, ↑(n i) * (D.Ms l G).torusξ D.S (h - D.SP.Δ) i| ≤ D.SP.Tt⁻¹ / ModeSchedule.Lh (h - D.SP.Δ)) ∧ (n ∉
rationalIntegerIntersection
(tinySpan (fun (i : Fin (D.Ms l G).zc.dim) => (D.Ms l G).zc.θ i / ↑D.S.Q0) D.SP.Hn
(D.SP.Tt⁻¹ / dyadicGridLength A.G (A.blkStart D.S.K I.1 - 2 * ↑D.S.K))) →
D.SP.Tt / ModeSchedule.Lh (h - D.SP.Δ) ≤ dyadicGridLength A.G I.1 * |∑ i : Fin (D.Ms l G).zc.dim, ↑(n i) * (D.Ms l G).torusξ D.S (h - D.SP.Δ) i|)
box_dichotomy for every integer frequency n with |n|_∞ ≤ 64 D_*^5 E_{h-Δ} (blueprint
lines 2483-2487, "apply its gap to pure ϑ shifts in all the boxes under consideration": the
anchored three-core combinations P₂ - l P₁ - m₀ reach 41 D_*^5 E_{h-Δ}).
theorem
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.three_cosets
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
{Cj CA CT CK : ℕ}
{δs W : ℝ}
(hV : D.S.Valid Cj CA CT CK δs W)
(hCA : 1 ≤ CA)
(hCT : 4 ≤ CT)
(hd2 : 2 ≤ D.S.dmax)
(hD : 2 ≤ D.S.Dstar)
(hB : 2 ≤ D.S.Bstar)
(hQ : 1 ≤ D.S.Q0)
(hSP : D.SP = D.S.sideParams δs)
(I : ℤ × ℤ)
(G : bf.Grp)
(j₀ : Fin 4)
(hz₀ : (D.Ms j₀ G).zc = (D.Ms 0 G).zc)
(hdim : (D.Ms 0 G).zc.dim ≤ D.S.dmax)
{h : ℕ}
(hh : h ≤ D.SP.Jst)
{m₀ : ↥((D.Ms j₀ G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))}
(hgood :
((D.Ms j₀ G).blockComps D.S ⋯ (A.blkStart D.S.K I.1) (D.preAt I)).Good D.SP.Δ
((D.Ms j₀ G).goodP D.S D.SP (A.blkStart D.S.K I.1)) h m₀)
{Kt : ℕ}
(hQB : ↑D.S.Q0 * 2 ^ (Kt + 1) ≤ D.S.Bstar)
{ι : Fin 4 → Type u_1}
(F : (j : Fin 4) → Finset (ι j))
(n : (j : Fin 4) → ι j → Fin (D.Ms 0 G).zc.dim → ℤ)
(hn : ∀ (j : Fin 4), ∀ k ∈ F j, ∀ (i : Fin (D.Ms 0 G).zc.dim), |↑(n j k i)| ≤ D.S.Dstar * D.S.Eh (h - D.SP.Δ))
(xs : ℝ)
(l : Fin 4)
(a : Fin 4 → ℝ)
(hne : (D.threeRefSet G I xs (h - D.SP.Δ) l a).Nonempty)
:
∃ (N : Finset (Fin (D.Ms 0 G).zc.dim → ℤ)) (nref :
(Fin ((D.Ms 0 G).zc.dim + (D.Ms 0 G).zc.dim) → ℤ) × ((j : Fin 4) → (Fin (D.Ms 0 G).zc.dim → ℤ) × ι j) →
Fin (D.Ms 0 G).zc.dim → ℤ),
(∀ n ∈ N, ∀ (i : Fin (D.Ms 0 G).zc.dim), |↑(n i)| ≤ 16 * (D.S.Dstar ^ 5 * D.S.Eh (h - D.SP.Δ))) ∧ (∀ n ∈ N,
∀ n' ∈ N,
n ≠ n' →
n - n' ∉
rationalIntegerIntersection
(tinySpan (fun (i : Fin (D.Ms 0 G).zc.dim) => (D.Ms 0 G).zc.θ i / ↑D.S.Q0) D.SP.Hn
(D.SP.Tt⁻¹ / dyadicGridLength A.G (A.blkStart D.S.K I.1 - 2 * ↑D.S.K)))) ∧ (∀ n ∈ N,
∀ n' ∈ N,
n ≠ n' →
1 ≤ |-(dyadicGridLength A.G I.1 * ((∑ j : Fin 4, if j = l then 0 else a j) + ∑ i : Fin (D.Ms 0 G).zc.dim,
↑(n i) * ((D.Ms 0 G).zc.θ i / (↑D.S.Q0 * ↑(6 ^ (h - D.SP.Δ)))))) - -(dyadicGridLength A.G I.1 * ((∑ j : Fin 4, if j = l then 0 else a j) + ∑ i : Fin (D.Ms 0 G).zc.dim,
↑(n' i) * ((D.Ms 0 G).zc.θ i / (↑D.S.Q0 * ↑(6 ^ (h - D.SP.Δ))))))|) ∧ (∀
x ∈
frequencyBox ((D.Ms 0 G).zc.dim + (D.Ms 0 G).zc.dim) (2 ^ (Kt + 1)) ×ˢ Fintype.piFinset fun (j : Fin 4) => frequencyBox (D.Ms 0 G).zc.dim (2 ^ (Kt + 1)) ×ˢ F j,
expP2 (6 ^ (h - D.SP.Δ)) (D.S.Q0 * 6 ^ (h - D.SP.Δ)) n x - ↑↑l • expP1 (6 ^ (h - D.SP.Δ)) (D.S.Q0 * 6 ^ (h - D.SP.Δ)) n x - D.threeRef G I xs (h - D.SP.Δ) l a ∈ rationalIntegerIntersection
(tinySpan (fun (i : Fin (D.Ms 0 G).zc.dim) => (D.Ms 0 G).zc.θ i / ↑D.S.Q0) D.SP.Hn
(D.SP.Tt⁻¹ / dyadicGridLength A.G (A.blkStart D.S.K I.1 - 2 * ↑D.S.K))) →
nref x ∈ N ∧ expP1 (6 ^ (h - D.SP.Δ)) (D.S.Q0 * 6 ^ (h - D.SP.Δ)) n x - nref x ∈ rationalIntegerIntersection
(tinySpan (fun (i : Fin (D.Ms 0 G).zc.dim) => (D.Ms 0 G).zc.θ i / ↑D.S.Q0) D.SP.Hn
(D.SP.Tt⁻¹ / dyadicGridLength A.G (A.blkStart D.S.K I.1 - 2 * ↑D.S.K))) ∧ |dyadicGridLength A.G I.1 * ((∑ j : Fin 4, if j = l then 0 else a j) + ∑ i : Fin (D.Ms 0 G).zc.dim,
↑(expP1 (6 ^ (h - D.SP.Δ)) (D.S.Q0 * 6 ^ (h - D.SP.Δ)) n x i) * ((D.Ms 0 G).zc.θ i / (↑D.S.Q0 * ↑(6 ^ (h - D.SP.Δ))))) - dyadicGridLength A.G I.1 * ((∑ j : Fin 4, if j = l then 0 else a j) + ∑ i : Fin (D.Ms 0 G).zc.dim,
↑(nref x i) * ((D.Ms 0 G).zc.θ i / (↑D.S.Q0 * ↑(6 ^ (h - D.SP.Δ)))))| ≤ D.SP.Tt⁻¹ / ModeSchedule.Lh (h - D.SP.Δ) ∧ |dyadicGridLength A.G I.1 * ((∑ j : Fin 4, ↑↑j * if j = l then 0 else a j) + ∑ i : Fin (D.Ms 0 G).zc.dim,
↑(expP2 (6 ^ (h - D.SP.Δ)) (D.S.Q0 * 6 ^ (h - D.SP.Δ)) n x i) * ((D.Ms 0 G).zc.θ i / (↑D.S.Q0 * ↑(6 ^ (h - D.SP.Δ)))) - ↑↑l * ((∑ j : Fin 4, if j = l then 0 else a j) + ∑ i : Fin (D.Ms 0 G).zc.dim,
↑(expP1 (6 ^ (h - D.SP.Δ)) (D.S.Q0 * 6 ^ (h - D.SP.Δ)) n x i) * ((D.Ms 0 G).zc.θ i / (↑D.S.Q0 * ↑(6 ^ (h - D.SP.Δ)))))) - D.threeBeta G I xs (h - D.SP.Δ) l a| ≤ D.SP.Tt⁻¹ / ModeSchedule.Lh (h - D.SP.Δ)) ∧ ∀
x ∈
frequencyBox ((D.Ms 0 G).zc.dim + (D.Ms 0 G).zc.dim) (2 ^ (Kt + 1)) ×ˢ Fintype.piFinset fun (j : Fin 4) => frequencyBox (D.Ms 0 G).zc.dim (2 ^ (Kt + 1)) ×ˢ F j,
expP2 (6 ^ (h - D.SP.Δ)) (D.S.Q0 * 6 ^ (h - D.SP.Δ)) n x - ↑↑l • expP1 (6 ^ (h - D.SP.Δ)) (D.S.Q0 * 6 ^ (h - D.SP.Δ)) n x - D.threeRef G I xs (h - D.SP.Δ) l a ∉
rationalIntegerIntersection
(tinySpan (fun (i : Fin (D.Ms 0 G).zc.dim) => (D.Ms 0 G).zc.θ i / ↑D.S.Q0) D.SP.Hn
(D.SP.Tt⁻¹ / dyadicGridLength A.G (A.blkStart D.S.K I.1 - 2 * ↑D.S.K))) →
D.SP.Tt / ModeSchedule.Lh (h - D.SP.Δ) - D.U0 ≤ |dyadicGridLength A.G I.1 * ((∑ j : Fin 4, ↑↑j * if j = l then 0 else a j) + ∑ i : Fin (D.Ms 0 G).zc.dim,
↑(expP2 (6 ^ (h - D.SP.Δ)) (D.S.Q0 * 6 ^ (h - D.SP.Δ)) n x i) * ((D.Ms 0 G).zc.θ i / (↑D.S.Q0 * ↑(6 ^ (h - D.SP.Δ)))) - ↑↑l * ((∑ j : Fin 4, if j = l then 0 else a j) + ∑ i : Fin (D.Ms 0 G).zc.dim,
↑(expP1 (6 ^ (h - D.SP.Δ)) (D.S.Q0 * 6 ^ (h - D.SP.Δ)) n x i) * ((D.Ms 0 G).zc.θ i / (↑D.S.Q0 * ↑(6 ^ (h - D.SP.Δ))))))|
Blueprint lines 2542-2547 on a leaf cell I of the side states for a three-core tuple with side
role l passing the three-core test (reference m₀ = threeRef), with the gap of a good component
of any role j₀ in the common chart (a successful core component; the side role may be role 0):
for the anchored expansion of the
transported core data (indices F_j, shifts of size at most D_* E_{h-Δ}, multiplier and cutoff
indices in the truncation box, chart of role 0), there are references N, one from the box per
horizontal coset modulo K_B, in distinct cosets, whose real frequencies r(Q + n·ξ) are more than
1 apart; on the reference vertical coset m₀ + K_B every term is within T⁻¹/L_{h-Δ} of its
references, and off it the anchored frequency is at least T/L_{h-Δ} - U₀ (box_dichotomy64,
three_cosets_of_dichotomy; the slopes γ_j = ω_{a_j}(x*) of the core roles, γ_l = 0).
theorem
TrilinearHT.Auto.three_core_main_l2
{κ : LocalKernelClass}
{a₀ r : ℝ}
{w : ℝ × ℝ → ℂ}
(hr : 0 < r)
(hw : IsAdmissibleLocalKernel κ a₀ r w)
(l : Fin 4)
(S : ℝ → ℂ)
(hS : MeasureTheory.IntegrableOn S (Set.Ico a₀ (a₀ + r)) MeasureTheory.volume)
(hS2 : MeasureTheory.MemLp S 2 (MeasureTheory.volume.restrict (Set.Ioc a₀ (a₀ + r))))
(x₀ : ℝ)
{d : ℕ}
(V : Submodule ℚ (Fin d → ℚ))
(Rm : ↥(torusAnnihilator (rationalIntegerIntersection V)) × ↥(torusAnnihilator (rationalIntegerIntersection V)) → ℂ)
(hRm : Continuous Rm)
{W : ℝ}
(hW : 0 ≤ W)
(hRb :
∀ (z : ↥(torusAnnihilator (rationalIntegerIntersection V)) × ↥(torusAnnihilator (rationalIntegerIntersection V))),
‖Rm z‖ ≤ W)
(g : Fin 4 → ↥(torusAnnihilator (rationalIntegerIntersection V)) → ℂ)
(hg : ∀ (i : Fin 4), Continuous (g i))
(m₀ : Fin d → ℤ)
(N : Finset (Fin d → ℤ))
(hN : ∀ n ∈ N, ∀ n' ∈ N, n ≠ n' → n - n' ∉ rationalIntegerIntersection V)
(αN : (Fin d → ℤ) → ℝ)
(β₀ : ℝ)
(hsep : ∀ n ∈ N, ∀ n' ∈ N, n ≠ n' → 1 ≤ |-(r * αN n) - -(r * αN n')|)
(J A I : ℕ)
(hA : 1 ≤ A)
:
‖∑ n ∈ N,
(∫ (u : ↥(torusAnnihilator (rationalIntegerIntersection V))), dualSlice V Rm l g m₀ u * (starRingEnd ℂ) (torusCharacter n ↑u) ∂torusAnnihilatorHaar (rationalIntegerIntersection V)) * anchorP r w l S x₀ (αN n) β₀‖ ≤ r⁻¹ * entryC κ J A (r * β₀) * 2 ^ (A + 4) * ∑ i ∈ Finset.range (I + 1),
(2 ^ i)⁻¹ ^ (A + 1) * ((W * ∏ i ∈ Finset.univ.erase l,
(MeasureTheory.eLpNorm (g i) 2 (torusAnnihilatorHaar (rationalIntegerIntersection V))).toReal) * √(∑ k ∈ windowSet N (fun (n : Fin d → ℤ) => r * αN n) I with ∃ n ∈ N, |↑k + -(r * αN n)| ≤ 2 ^ i,
‖∫ (y : ℝ) in Set.Ico a₀ (a₀ + r), S y * Complex.exp (2 * ↑Real.pi * Complex.I * ↑k * ↑y / ↑r)‖ ^ 2)) + r⁻¹ * entryC κ J A (r * β₀) * 2 ^ (A + 4) * (2 * (2 ^ (I + 1))⁻¹ ^ (A + 1)) * ((W * ∏ i ∈ Finset.univ.erase l,
(MeasureTheory.eLpNorm (g i) 2 (torusAnnihilatorHaar (rationalIntegerIntersection V))).toReal) * √(r * ∫ (y : ℝ) in a₀..a₀ + r, ‖S y‖ ^ 2))
Blueprint eq:side-windows (lines 2549-2560) for the reference terms of a three-core test,
with only ℓ² norms: with Haar coefficients a_n = ⟨D_{m₀}, χ_n⟩ at 1-separated reference
frequencies r α_n, |Σ_n a_n P(α_n, β₀)| is at most
C 2^{A+4} Σ_{Λ = 2^i ≤ 2^I} Λ^{-(A+1)} (W Π_{j ≠ l} ‖g_j‖) b_Λ plus the shells above 2^I,
C 2^{A+5} 2^{-(I+1)(A+1)} (W Π_{j ≠ l} ‖g_j‖) (r ∫_I |S|²)^{1/2} ("shells above U₀ are
negligible by the same estimate or ordinary L² pairing"), for A ≥ 1 (three_core_main at every
larger shell cutoff, cell_coeff_bessel, and the vanishing of its ℓ¹ remainder).
theorem
TrilinearHT.Auto.three_core_anchored_bound_l2
{κ : LocalKernelClass}
{a₀ r : ℝ}
{w : ℝ × ℝ → ℂ}
(hr : 0 < r)
(hw : IsAdmissibleLocalKernel κ a₀ r w)
(l : Fin 4)
(Fc : ℝ × ℝ → ℂ)
(Sd : ℝ → ℂ)
(hfm : MeasureTheory.AEStronglyMeasurable Sd MeasureTheory.volume)
(hfl : MeasureTheory.IntegrableOn Sd (Set.Icc a₀ (a₀ + r)) MeasureTheory.volume)
(hS2 : MeasureTheory.MemLp Sd 2 (MeasureTheory.volume.restrict (Set.Ioc a₀ (a₀ + r))))
(hfi :
MeasureTheory.Integrable (fun (z : ℝ × ℝ) => w z * (Fc z * Sd (realProgressionCoordinate l z))) MeasureTheory.volume)
{x₀ : ℝ}
(hx₀ : x₀ ∈ Set.Icc a₀ (a₀ + r))
{d : ℕ}
(V : Submodule ℚ (Fin d → ℚ))
{ι : Type u_1}
(P : Finset ι)
(C : ι → ℂ)
(fr : ι → (Fin d → ℤ) × (Fin d → ℤ))
(α β : ι → ℝ)
{ε : ℝ}
(hε0 : 0 ≤ ε)
(hε :
∀ (z : ℝ × ℝ),
w z ≠ 0 → ‖Fc z - ∑ x ∈ P, C x * ↑(Real.fourierChar (α x * (realProgressionCoordinate l z - x₀) + β x * z.2))‖ ≤ ε)
(Rm : ↥(torusAnnihilator (rationalIntegerIntersection V)) × ↥(torusAnnihilator (rationalIntegerIntersection V)) → ℂ)
(hRm : Continuous Rm)
{W : ℝ}
(hW : 0 ≤ W)
(hRb :
∀ (z : ↥(torusAnnihilator (rationalIntegerIntersection V)) × ↥(torusAnnihilator (rationalIntegerIntersection V))),
‖Rm z‖ ≤ W)
(g : Fin 4 → ↥(torusAnnihilator (rationalIntegerIntersection V)) → ℂ)
(hg : ∀ (i : Fin 4), Continuous (g i))
(hexp :
∀ (u v : ↥(torusAnnihilator (rationalIntegerIntersection V))),
Rm (u, v) * ∏ i ∈ Finset.univ.erase l, g i (u + (↑↑i - ↑↑l) • v) = ∑ x ∈ P, C x * (torusCharacter (fr x).1 ↑u * torusCharacter (fr x).2 ↑v))
(m₀ : Fin d → ℤ)
(N : Finset (Fin d → ℤ))
(hN : ∀ n ∈ N, ∀ n' ∈ N, n ≠ n' → n - n' ∉ rationalIntegerIntersection V)
(αN : (Fin d → ℤ) → ℝ)
(β₀ : ℝ)
(hsep : ∀ n ∈ N, ∀ n' ∈ N, n ≠ n' → 1 ≤ |-(r * αN n) - -(r * αN n')|)
(nref : ι → Fin d → ℤ)
{ε₁ H : ℝ}
(hε₁ : 0 ≤ ε₁)
(hH : 4 ≤ H)
(hnear :
∀ x ∈ P,
(fr x).2 - m₀ ∈ rationalIntegerIntersection V →
nref x ∈ N ∧ (fr x).1 - nref x ∈ rationalIntegerIntersection V ∧ |r * α x - r * αN (nref x)| ≤ ε₁ ∧ |r * β x - r * β₀| ≤ ε₁)
(hfar : ∀ x ∈ P, (fr x).2 - m₀ ∉ rationalIntegerIntersection V → H ≤ |r * β x|)
{J : ℕ}
(hJ : 2 ≤ J)
(A I : ℕ)
(hA : 1 ≤ A)
:
‖(↑r)⁻¹ ^ 2 * ∫ (z : ℝ × ℝ), w z * (Fc z * Sd (realProgressionCoordinate l z))‖ ≤ 2 * localKernelSupBound κ * ε * (r⁻¹ * ∫ (y : ℝ) in Set.Icc a₀ (a₀ + r), ‖Sd y‖) + (r⁻¹ * entryC κ J A (r * β₀) * 2 ^ (A + 4) * ∑ i ∈ Finset.range (I + 1),
(2 ^ i)⁻¹ ^ (A + 1) * ((W * ∏ i ∈ Finset.univ.erase l,
(MeasureTheory.eLpNorm (g i) 2 (torusAnnihilatorHaar (rationalIntegerIntersection V))).toReal) * √(∑ k ∈ windowSet N (fun (n : Fin d → ℤ) => r * αN n) I with ∃ n ∈ N, |↑k + -(r * αN n)| ≤ 2 ^ i,
‖∫ (y : ℝ) in Set.Ico a₀ (a₀ + r), Sd y * Complex.exp (2 * ↑Real.pi * Complex.I * ↑k * ↑y / ↑r)‖ ^ 2)) + r⁻¹ * entryC κ J A (r * β₀) * 2 ^ (A + 4) * (2 * (2 ^ (I + 1))⁻¹ ^ (A + 1)) * ((W * ∏ i ∈ Finset.univ.erase l,
(MeasureTheory.eLpNorm (g i) 2 (torusAnnihilatorHaar (rationalIntegerIntersection V))).toReal) * √(r * ∫ (y : ℝ) in a₀..a₀ + r, ‖Sd y‖ ^ 2))) + (∑ x ∈ P, ‖C x‖) * ((r⁻¹ * ∫ (y : ℝ) in Set.Ico a₀ (a₀ + r), ‖Sd y‖) * (nearB κ ε₁ + 12 * (kerC κ J * (4 / H) ^ (J - 2))))
three_core_anchored_bound with only ℓ² norms in its main term (blueprint
eq:side-windows, lines 2549-2560): the window bound over the shells Λ = 2^i ≤ 2^I plus the
shells above 2^I bounded by the L² norm of the side on the cell (three_core_main_l2), plus the
numerical errors 2‖w‖_∞ ε r⁻¹ ‖f_l‖_{L¹} and the near and far coset terms
Σ_x |C_x| r⁻¹ ‖f_l‖_{L¹} (nearB(ε₁) + 12 C_J (4/H)^{J-2}), for A ≥ 1.
theorem
TrilinearHT.Auto.three_core_Fc_approx_of
(z : ChartTag)
{δ δ'' : ℝ}
(hδ : 0 < δ)
(hδ'' : 0 < δ'')
(ρ : Fin 4 → Fin z.dim → ℝ)
(hρ : ∀ (j : Fin 4) (a : Fin z.dim), ρ j a ∈ Set.Icc 0 1)
{Q0 : ℕ}
(hQ0 : 0 < Q0)
(hQ : ∀ (a b : Fin z.dim), ∃ (k : ℤ), ↑Q0 * ↑(z.C a b) = ↑k)
{Cm : ℝ}
(hCm : ∀ (a b : Fin z.dim), |↑(z.C a b)| ≤ Cm)
{L : ℕ}
(hL : 0 < L)
(Kt : ℕ)
(xs : ℝ)
(l : Fin 4)
(γ : Fin 4 → ℝ)
(hγl : γ l = 0)
{ι : Fin 4 → Type u_1}
(F : (j : Fin 4) → Finset (ι j))
(c : (j : Fin 4) → ι j → ℂ)
(n : (j : Fin 4) → ι j → Fin z.dim → ℤ)
{k₀ : ι l}
(hFl : F l = {k₀})
(hcl : c l k₀ = 1)
(hnl : n l k₀ = 0)
(f : Fin 4 → ℝ → ℂ)
(hfl : ∀ (y : ℝ), f l y = ↑(centerCut z δ (ρ l) y) * ↑(Real.fourierChar (↑(slotCoeff l) * centerPhase z (ρ l) y)))
(lo hi : ℝ)
{η : ℝ}
(hη : 0 ≤ η)
(hfa :
∀ (j : Fin 4),
j ≠ l →
∀ y ∈ Set.Icc lo hi,
‖f j y - ↑(centerCut z δ (ρ j) y) * ↑(Real.fourierChar (↑(slotCoeff j) * centerPhase z (ρ j) y)) * (↑(Real.fourierChar (γ j * (y - xs))) * ∑ k ∈ F j,
c j k * torusCharacter (n j k) (torusMk fun (i : Fin z.dim) => z.θ i / (↑Q0 * ↑L) * (y - xs)))‖ ≤ η * ∑ k ∈ F j, ‖c j k‖)
(hfb : ∀ (j : Fin 4), j ≠ l → ∀ y ∈ Set.Icc lo hi, ‖f j y‖ ≤ ∑ k ∈ F j, ‖c j k‖)
(cc0 : Fin 4 → (Fin z.dim → ℤ) → ℂ)
(hcc0 : ∀ (j : Fin 4) (v : Fin z.dim → ℤ), ‖cc0 j v‖ ≤ 1)
(hccT :
∀ (j : Fin 4) (w : Fin z.dim → ℝ),
‖cutoffP δ (ρ j) w - ∑ v ∈ frequencyBox z.dim (2 ^ (Kt + 1)), cc0 j v * ↑(Real.fourierChar (∑ i : Fin z.dim, ↑(v i) * w i))‖ ≤ cutTail z.dim δ Kt)
(cm0 : (Fin (z.dim + z.dim) → ℤ) → ℂ)
(hcm0 : ∀ (v : Fin (z.dim + z.dim) → ℤ), ‖cm0 v‖ ≤ 1)
(hcmT :
∀ (w : Fin (z.dim + z.dim) → ℝ),
‖gaugeMult δ'' Q0 0 z.C ρ w - ∑ v ∈ frequencyBox (z.dim + z.dim) (2 ^ (Kt + 1)),
cm0 v * ↑(Real.fourierChar (∑ i : Fin (z.dim + z.dim), ↑(v i) * w i))‖ ≤ multTail z.dim δ'' Q0 Cm Kt)
(cc : Fin 4 → (Fin z.dim → ℤ) → ℂ)
(hccE :
∀ (j : Fin 4) (v : Fin z.dim → ℤ), cc j v = cc0 j v * ↑(Real.fourierChar (∑ i : Fin z.dim, ↑(v i) * (z.θ i * xs))))
(cm : (Fin (z.dim + z.dim) → ℤ) → ℂ)
(hcmE :
∀ (v : Fin (z.dim + z.dim) → ℤ),
cm v = cm0 v * ↑(Real.fourierChar (∑ a : Fin z.dim, ↑(v (Fin.castAdd z.dim a)) * (z.θ a * xs / ↑Q0))))
(x t : ℝ)
:
(∀ (j : Fin 4), x + ↑↑j * t ∈ Set.Icc lo hi) →
‖∏ j : Fin 4, f j (x + ↑↑j * t) - ↑(Real.fourierChar (∑ j : Fin 4, γ j * (x + ↑↑j * t - xs))) * ((∑ v ∈ frequencyBox (z.dim + z.dim) (2 ^ (Kt + 1)),
cm v * (torusCharacter (↑L • fun (a : Fin z.dim) => v (Fin.castAdd z.dim a))
(torusMk fun (i : Fin z.dim) => z.θ i / (↑Q0 * ↑L) * (x - xs)) * torusCharacter (↑L • fun (a : Fin z.dim) => v (Fin.natAdd z.dim a))
(torusMk fun (i : Fin z.dim) => z.θ i / (↑Q0 * ↑L) * t))) * ∏ j : Fin 4,
∑ p ∈ frequencyBox z.dim (2 ^ (Kt + 1)) ×ˢ F j,
cc j p.1 * c j p.2 * torusCharacter (↑(Q0 * L) • p.1 + n j p.2)
((torusMk fun (i : Fin z.dim) => z.θ i / (↑Q0 * ↑L) * (x - xs)) + (↑↑j - 0) • torusMk fun (i : Fin z.dim) => z.θ i / (↑Q0 * ↑L) * t))‖ ≤ (4 * η + (gaugeErr z.dim δ δ'' + 4 * (1 + cutTail z.dim δ Kt) ^ 3 * cutTail z.dim δ Kt + (1 + cutTail z.dim δ Kt) ^ 4 * multTail z.dim δ'' Q0 Cm Kt)) * ∏ j : Fin 4, ∑ k ∈ F j, ‖c j k‖
three_core_Fc_approx with the Fourier truncations of the cutoffs and of the gauge multiplier
made explicit (gauge_torus_approx_of): the phase-corrected coefficients cc_j(v) = cc0_j(v) e(v·θ x*) and cm(v) = cm0(v) e(v₁·θ x*/Q₀).
theorem
TrilinearHT.Auto.three_core_principal_of
{κ : LocalKernelClass}
{a₀ r : ℝ}
(hr : 0 < r)
{w : ℝ × ℝ → ℂ}
(hw : IsAdmissibleLocalKernel κ a₀ r w)
(z : ChartTag)
{δ δ'' : ℝ}
(hδ : 0 < δ)
(hδ'' : 0 < δ'')
(ρ : Fin 4 → Fin z.dim → ℝ)
(hρ : ∀ (j : Fin 4) (a : Fin z.dim), ρ j a ∈ Set.Icc 0 1)
{Q0 : ℕ}
(hQ0 : 0 < Q0)
(hQ : ∀ (a b : Fin z.dim), ∃ (k : ℤ), ↑Q0 * ↑(z.C a b) = ↑k)
{Cm : ℝ}
(hCm : ∀ (a b : Fin z.dim), |↑(z.C a b)| ≤ Cm)
{L : ℕ}
(hL : 0 < L)
(Kt : ℕ)
{xs : ℝ}
(hxs : xs ∈ Set.Icc a₀ (a₀ + r))
(l : Fin 4)
(γ : Fin 4 → ℝ)
(hγl : γ l = 0)
{ι : Fin 4 → Type u_1}
(F : (j : Fin 4) → Finset (ι j))
(c : (j : Fin 4) → ι j → ℂ)
(n : (j : Fin 4) → ι j → Fin z.dim → ℤ)
{k₀ : ι l}
(hFl : F l = {k₀})
(hcl : c l k₀ = 1)
(hnl : n l k₀ = 0)
(f : Fin 4 → ℝ → ℂ)
(hfm : MeasureTheory.AEStronglyMeasurable (sideSd z (ρ l) l (f l)) MeasureTheory.volume)
(hfl : MeasureTheory.IntegrableOn (sideSd z (ρ l) l (f l)) (Set.Icc a₀ (a₀ + r)) MeasureTheory.volume)
(hS2 : MeasureTheory.MemLp (sideSd z (ρ l) l (f l)) 2 (MeasureTheory.volume.restrict (Set.Ioc a₀ (a₀ + r))))
(hfi :
MeasureTheory.Integrable
(fun (zz : ℝ × ℝ) =>
w zz * ∏ j : Fin 4,
Function.update f l (fun (y : ℝ) => ↑(centerCut z δ (ρ l) y) * f l y) j (realProgressionCoordinate j zz))
MeasureTheory.volume)
{η : ℝ}
(hη : 0 ≤ η)
(hfa :
∀ (j : Fin 4),
j ≠ l →
∀ y ∈ Set.Icc a₀ (a₀ + r),
‖f j y - ↑(centerCut z δ (ρ j) y) * ↑(Real.fourierChar (↑(slotCoeff j) * centerPhase z (ρ j) y)) * (↑(Real.fourierChar (γ j * (y - xs))) * ∑ k ∈ F j,
c j k * torusCharacter (n j k) (torusMk fun (i : Fin z.dim) => z.θ i / (↑Q0 * ↑L) * (y - xs)))‖ ≤ η * ∑ k ∈ F j, ‖c j k‖)
(hfb : ∀ (j : Fin 4), j ≠ l → ∀ y ∈ Set.Icc a₀ (a₀ + r), ‖f j y‖ ≤ ∑ k ∈ F j, ‖c j k‖)
(cc0 : Fin 4 → (Fin z.dim → ℤ) → ℂ)
(hcc0 : ∀ (j : Fin 4) (v : Fin z.dim → ℤ), ‖cc0 j v‖ ≤ 1)
(hccT :
∀ (j : Fin 4) (w : Fin z.dim → ℝ),
‖cutoffP δ (ρ j) w - ∑ v ∈ frequencyBox z.dim (2 ^ (Kt + 1)), cc0 j v * ↑(Real.fourierChar (∑ i : Fin z.dim, ↑(v i) * w i))‖ ≤ cutTail z.dim δ Kt)
(cm0 : (Fin (z.dim + z.dim) → ℤ) → ℂ)
(hcm0 : ∀ (v : Fin (z.dim + z.dim) → ℤ), ‖cm0 v‖ ≤ 1)
(hcmT :
∀ (w : Fin (z.dim + z.dim) → ℝ),
‖gaugeMult δ'' Q0 0 z.C ρ w - ∑ v ∈ frequencyBox (z.dim + z.dim) (2 ^ (Kt + 1)),
cm0 v * ↑(Real.fourierChar (∑ i : Fin (z.dim + z.dim), ↑(v i) * w i))‖ ≤ multTail z.dim δ'' Q0 Cm Kt)
(cc : Fin 4 → (Fin z.dim → ℤ) → ℂ)
(hccE :
∀ (j : Fin 4) (v : Fin z.dim → ℤ), cc j v = cc0 j v * ↑(Real.fourierChar (∑ i : Fin z.dim, ↑(v i) * (z.θ i * xs))))
(cm : (Fin (z.dim + z.dim) → ℤ) → ℂ)
(hcmE :
∀ (v : Fin (z.dim + z.dim) → ℤ),
cm v = cm0 v * ↑(Real.fourierChar (∑ a : Fin z.dim, ↑(v (Fin.castAdd z.dim a)) * (z.θ a * xs / ↑Q0))))
(V : Submodule ℚ (Fin z.dim → ℚ))
(m₀ : Fin z.dim → ℤ)
(N : Finset (Fin z.dim → ℤ))
(hN : ∀ n ∈ N, ∀ n' ∈ N, n ≠ n' → n - n' ∉ rationalIntegerIntersection V)
(αN : (Fin z.dim → ℤ) → ℝ)
(β₀ : ℝ)
(hsep : ∀ n ∈ N, ∀ n' ∈ N, n ≠ n' → 1 ≤ |-(r * αN n) - -(r * αN n')|)
(nref : (Fin (z.dim + z.dim) → ℤ) × ((j : Fin 4) → (Fin z.dim → ℤ) × ι j) → Fin z.dim → ℤ)
{ε₁ H : ℝ}
(hε₁ : 0 ≤ ε₁)
(hH : 4 ≤ H)
(hnear :
∀
x ∈
frequencyBox (z.dim + z.dim) (2 ^ (Kt + 1)) ×ˢ Fintype.piFinset fun (j : Fin 4) => frequencyBox z.dim (2 ^ (Kt + 1)) ×ˢ F j,
expP2 L (Q0 * L) n x - ↑↑l • expP1 L (Q0 * L) n x - m₀ ∈ rationalIntegerIntersection V →
nref x ∈ N ∧ expP1 L (Q0 * L) n x - nref x ∈ rationalIntegerIntersection V ∧ |r * (∑ j : Fin 4, γ j + ∑ i : Fin z.dim, ↑(expP1 L (Q0 * L) n x i) * (z.θ i / (↑Q0 * ↑L))) - r * αN (nref x)| ≤ ε₁ ∧ |r * (∑ j : Fin 4, ↑↑j * γ j + ∑ i : Fin z.dim, ↑(expP2 L (Q0 * L) n x i) * (z.θ i / (↑Q0 * ↑L)) - ↑↑l * (∑ j : Fin 4, γ j + ∑ i : Fin z.dim, ↑(expP1 L (Q0 * L) n x i) * (z.θ i / (↑Q0 * ↑L)))) - r * β₀| ≤ ε₁)
(hfar :
∀
x ∈
frequencyBox (z.dim + z.dim) (2 ^ (Kt + 1)) ×ˢ Fintype.piFinset fun (j : Fin 4) => frequencyBox z.dim (2 ^ (Kt + 1)) ×ˢ F j,
expP2 L (Q0 * L) n x - ↑↑l • expP1 L (Q0 * L) n x - m₀ ∉ rationalIntegerIntersection V →
H ≤ |r * (∑ j : Fin 4, ↑↑j * γ j + ∑ i : Fin z.dim, ↑(expP2 L (Q0 * L) n x i) * (z.θ i / (↑Q0 * ↑L)) - ↑↑l * (∑ j : Fin 4, γ j + ∑ i : Fin z.dim, ↑(expP1 L (Q0 * L) n x i) * (z.θ i / (↑Q0 * ↑L))))|)
{J : ℕ}
(hJ : 2 ≤ J)
(A I : ℕ)
(hA : 1 ≤ A)
:
‖localProgressionForm r w (Function.update f l fun (y : ℝ) => ↑(centerCut z δ (ρ l) y) * f l y)‖ ≤ 2 * localKernelSupBound κ * ((4 * η + (gaugeErr z.dim δ δ'' + 4 * (1 + cutTail z.dim δ Kt) ^ 3 * cutTail z.dim δ Kt + (1 + cutTail z.dim δ Kt) ^ 4 * multTail z.dim δ'' Q0 Cm Kt)) * ∏ j : Fin 4, ∑ k ∈ F j, ‖c j k‖) * (r⁻¹ * ∫ (y : ℝ) in Set.Icc a₀ (a₀ + r), ‖sideSd z (ρ l) l (f l) y‖) + (r⁻¹ * entryC κ J A (r * β₀) * 2 ^ (A + 4) * ∑ i ∈ Finset.range (I + 1),
(2 ^ i)⁻¹ ^ (A + 1) * (((1 + multTail z.dim δ'' Q0 Cm Kt) * (1 + cutTail z.dim δ Kt) * ∏ i ∈ Finset.univ.erase l,
(MeasureTheory.eLpNorm
(fun (u : ↥(torusAnnihilator (rationalIntegerIntersection V))) =>
coreG (Q0 * L) (2 ^ (Kt + 1)) F c n cc i ↑u)
2 (torusAnnihilatorHaar (rationalIntegerIntersection V))).toReal) * √(∑ k ∈ windowSet N (fun (n : Fin z.dim → ℤ) => r * αN n) I with ∃ n ∈ N, |↑k + -(r * αN n)| ≤ 2 ^ i,
‖∫ (y : ℝ) in Set.Ico a₀ (a₀ + r), sideSd z (ρ l) l (f l) y * Complex.exp (2 * ↑Real.pi * Complex.I * ↑k * ↑y / ↑r)‖ ^ 2)) + r⁻¹ * entryC κ J A (r * β₀) * 2 ^ (A + 4) * (2 * (2 ^ (I + 1))⁻¹ ^ (A + 1)) * (((1 + multTail z.dim δ'' Q0 Cm Kt) * (1 + cutTail z.dim δ Kt) * ∏ i ∈ Finset.univ.erase l,
(MeasureTheory.eLpNorm
(fun (u : ↥(torusAnnihilator (rationalIntegerIntersection V))) =>
coreG (Q0 * L) (2 ^ (Kt + 1)) F c n cc i ↑u)
2 (torusAnnihilatorHaar (rationalIntegerIntersection V))).toReal) * √(r * ∫ (y : ℝ) in a₀..a₀ + r, ‖sideSd z (ρ l) l (f l) y‖ ^ 2))) + (∑
x ∈
frequencyBox (z.dim + z.dim) (2 ^ (Kt + 1)) ×ˢ Fintype.piFinset fun (j : Fin 4) => frequencyBox z.dim (2 ^ (Kt + 1)) ×ˢ F j,
‖cm x.1 * ∏ j : Fin 4, cc j (x.2 j).1 * c j (x.2 j).2‖) * ((r⁻¹ * ∫ (y : ℝ) in Set.Ico a₀ (a₀ + r), ‖sideSd z (ρ l) l (f l) y‖) * (nearB κ ε₁ + 12 * (kerC κ J * (4 / H) ^ (J - 2))))
Blueprint lines 2537-2560 (the three-core principal estimate at a fixed side offset) with the
Fourier truncations made explicit: the re-anchored multiplier is bounded by (1 + τ_m)(1 + τ_c)
(multTrunc_sup, trunc_cut_sup; no |box| factor), and the main term has only ℓ² norms
(three_core_anchored_bound_l2: windows Λ = 2^i ≤ 2^I and the shells above, for A ≥ 1).
theorem
TrilinearHT.Auto.three_core_averaged_of
{κ : LocalKernelClass}
{a₀ r : ℝ}
(hr : 0 < r)
{w : ℝ × ℝ → ℂ}
(hw : IsAdmissibleLocalKernel κ a₀ r w)
(z : ChartTag)
{δ δ'' : ℝ}
(hδ : 0 < δ)
(hδ'' : 0 < δ'')
(hdδ : 8 * ↑z.dim * δ ≤ 1)
(hδ8 : δ ≤ 1 / 8)
(ρc : Fin 4 → Fin z.dim → ℝ)
(hρc : ∀ (j : Fin 4) (a : Fin z.dim), ρc j a ∈ Set.Icc 0 1)
{Q0 : ℕ}
(hQ0 : 0 < Q0)
(hQ : ∀ (a b : Fin z.dim), ∃ (k : ℤ), ↑Q0 * ↑(z.C a b) = ↑k)
{Cm : ℝ}
(hCm0 : 0 ≤ Cm)
(hCm : ∀ (a b : Fin z.dim), |↑(z.C a b)| ≤ Cm)
{L : ℕ}
(hL : 0 < L)
(Kt : ℕ)
{xs : ℝ}
(hxs : xs ∈ Set.Icc a₀ (a₀ + r))
(l : Fin 4)
(γ : Fin 4 → ℝ)
(hγl : γ l = 0)
{ι : Fin 4 → Type u_1}
(F : (j : Fin 4) → Finset (ι j))
(c : (j : Fin 4) → ι j → ℂ)
(n : (j : Fin 4) → ι j → Fin z.dim → ℤ)
{k₀ : ι l}
(hFl : F l = {k₀})
(hcl : c l k₀ = 1)
(hnl : n l k₀ = 0)
(f : Fin 4 → ℝ → ℂ)
(hgm : Measurable (f l))
(hL2 : MeasureTheory.MemLp (f l) 2 (MeasureTheory.volume.restrict (Set.Ioc a₀ (a₀ + r))))
(hfi :
MeasureTheory.Integrable (fun (zz : ℝ × ℝ) => w zz * ∏ j : Fin 4, f j (realProgressionCoordinate j zz))
MeasureTheory.volume)
(hfiρ :
∀ (ρ' : Fin z.dim → ℝ),
MeasureTheory.Integrable
(fun (zz : ℝ × ℝ) =>
w zz * ∏ j : Fin 4,
Function.update f l (fun (y : ℝ) => ↑(centerCut z δ ρ' y) * f l y) j (realProgressionCoordinate j zz))
MeasureTheory.volume)
{η : ℝ}
(hη : 0 ≤ η)
(hfa :
∀ (j : Fin 4),
j ≠ l →
∀ y ∈ Set.Icc a₀ (a₀ + r),
‖f j y - ↑(centerCut z δ (ρc j) y) * ↑(Real.fourierChar (↑(slotCoeff j) * centerPhase z (ρc j) y)) * (↑(Real.fourierChar (γ j * (y - xs))) * ∑ k ∈ F j,
c j k * torusCharacter (n j k) (torusMk fun (i : Fin z.dim) => z.θ i / (↑Q0 * ↑L) * (y - xs)))‖ ≤ η * ∑ k ∈ F j, ‖c j k‖)
(hfb : ∀ (j : Fin 4), j ≠ l → ∀ y ∈ Set.Icc a₀ (a₀ + r), ‖f j y‖ ≤ ∑ k ∈ F j, ‖c j k‖)
(cc0 : Fin 4 → (Fin z.dim → ℤ) → ℂ)
(hcc0 : ∀ (j : Fin 4) (v : Fin z.dim → ℤ), ‖cc0 j v‖ ≤ 1)
(hccN : ∀ (j : Fin 4) (s : Finset (Fin z.dim → ℤ)), ∑ v ∈ s, ‖cc0 j v‖ ≤ cutNorm z.dim δ)
(hccT :
∀ (j : Fin 4),
j ≠ l →
∀ (w : Fin z.dim → ℝ),
‖cutoffP δ (ρc j) w - ∑ v ∈ frequencyBox z.dim (2 ^ (Kt + 1)), cc0 j v * ↑(Real.fourierChar (∑ i : Fin z.dim, ↑(v i) * w i))‖ ≤ cutTail z.dim δ Kt)
(V : Submodule ℚ (Fin z.dim → ℚ))
(m₀ : Fin z.dim → ℤ)
(N : Finset (Fin z.dim → ℤ))
(hN : ∀ n ∈ N, ∀ n' ∈ N, n ≠ n' → n - n' ∉ rationalIntegerIntersection V)
(αN : (Fin z.dim → ℤ) → ℝ)
(β₀ : ℝ)
(hsep : ∀ n ∈ N, ∀ n' ∈ N, n ≠ n' → 1 ≤ |-(r * αN n) - -(r * αN n')|)
(nref : (Fin (z.dim + z.dim) → ℤ) × ((j : Fin 4) → (Fin z.dim → ℤ) × ι j) → Fin z.dim → ℤ)
{ε₁ H : ℝ}
(hε₁ : 0 ≤ ε₁)
(hH : 4 ≤ H)
(hnear :
∀
x ∈
frequencyBox (z.dim + z.dim) (2 ^ (Kt + 1)) ×ˢ Fintype.piFinset fun (j : Fin 4) => frequencyBox z.dim (2 ^ (Kt + 1)) ×ˢ F j,
expP2 L (Q0 * L) n x - ↑↑l • expP1 L (Q0 * L) n x - m₀ ∈ rationalIntegerIntersection V →
nref x ∈ N ∧ expP1 L (Q0 * L) n x - nref x ∈ rationalIntegerIntersection V ∧ |r * (∑ j : Fin 4, γ j + ∑ i : Fin z.dim, ↑(expP1 L (Q0 * L) n x i) * (z.θ i / (↑Q0 * ↑L))) - r * αN (nref x)| ≤ ε₁ ∧ |r * (∑ j : Fin 4, ↑↑j * γ j + ∑ i : Fin z.dim, ↑(expP2 L (Q0 * L) n x i) * (z.θ i / (↑Q0 * ↑L)) - ↑↑l * (∑ j : Fin 4, γ j + ∑ i : Fin z.dim, ↑(expP1 L (Q0 * L) n x i) * (z.θ i / (↑Q0 * ↑L)))) - r * β₀| ≤ ε₁)
(hfar :
∀
x ∈
frequencyBox (z.dim + z.dim) (2 ^ (Kt + 1)) ×ˢ Fintype.piFinset fun (j : Fin 4) => frequencyBox z.dim (2 ^ (Kt + 1)) ×ˢ F j,
expP2 L (Q0 * L) n x - ↑↑l • expP1 L (Q0 * L) n x - m₀ ∉ rationalIntegerIntersection V →
H ≤ |r * (∑ j : Fin 4, ↑↑j * γ j + ∑ i : Fin z.dim, ↑(expP2 L (Q0 * L) n x i) * (z.θ i / (↑Q0 * ↑L)) - ↑↑l * (∑ j : Fin 4, γ j + ∑ i : Fin z.dim, ↑(expP1 L (Q0 * L) n x i) * (z.θ i / (↑Q0 * ↑L))))|)
{J : ℕ}
(hJ : 2 ≤ J)
(A I : ℕ)
(hA : 1 ≤ A)
:
‖localProgressionForm r w f‖ ≤ 2 * (2 * localKernelSupBound κ * ((4 * η + (gaugeErr z.dim δ δ'' + 4 * (1 + cutTail z.dim δ Kt) ^ 3 * cutTail z.dim δ Kt + (1 + cutTail z.dim δ Kt) ^ 4 * multTail z.dim δ'' Q0 Cm Kt)) * ∏ j : Fin 4, ∑ k ∈ F j, ‖c j k‖) * (r⁻¹ * ∫ (y : ℝ) in Set.Icc a₀ (a₀ + r), ‖f l y‖) + r⁻¹ * entryC κ J A (r * β₀) * 2 ^ (A + 4) * (2 * (2 ^ (I + 1))⁻¹ ^ (A + 1)) * (((1 + multTail z.dim δ'' Q0 Cm Kt) * (1 + cutTail z.dim δ Kt) * ∏ i ∈ Finset.univ.erase l,
(MeasureTheory.eLpNorm
(fun (u : ↥(torusAnnihilator (rationalIntegerIntersection V))) =>
coreG (Q0 * L) (2 ^ (Kt + 1)) F c n
(fun (j : Fin 4) (v : Fin z.dim → ℤ) =>
cc0 j v * ↑(Real.fourierChar (∑ i : Fin z.dim, ↑(v i) * (z.θ i * xs))))
i ↑u)
2 (torusAnnihilatorHaar (rationalIntegerIntersection V))).toReal) * √(r * ∫ (y : ℝ) in a₀..a₀ + r, ‖f l y‖ ^ 2)) + (multNorm z.dim δ'' Q0 Cm * ∏ j : Fin 4, cutNorm z.dim δ * ∑ k ∈ F j, ‖c j k‖) * ((r⁻¹ * ∫ (y : ℝ) in Set.Ico a₀ (a₀ + r), ‖f l y‖) * (nearB κ ε₁ + 12 * (kerC κ J * (4 / H) ^ (J - 2)))) + ∑ i ∈ Finset.range (I + 1),
r⁻¹ * entryC κ J A (r * β₀) * 2 ^ (A + 4) * (2 ^ i)⁻¹ ^ (A + 1) * ((1 + multTail z.dim δ'' Q0 Cm Kt) * (1 + cutTail z.dim δ Kt) * ∏ i ∈ Finset.univ.erase l,
(MeasureTheory.eLpNorm
(fun (u : ↥(torusAnnihilator (rationalIntegerIntersection V))) =>
coreG (Q0 * L) (2 ^ (Kt + 1)) F c n
(fun (j : Fin 4) (v : Fin z.dim → ℤ) =>
cc0 j v * ↑(Real.fourierChar (∑ i : Fin z.dim, ↑(v i) * (z.θ i * xs))))
i ↑u)
2 (torusAnnihilatorHaar (rationalIntegerIntersection V))).toReal) * √(∫ (ρ' : Fin z.dim → ℝ), sideWinE z l (f l) a₀ r
({k ∈ windowSet N (fun (n : Fin z.dim → ℤ) => r * αN n) I | ∃ n ∈ N, |↑k + -(r * αN n)| ≤ 2 ^ i})
ρ' ∂offsetMeasure z.dim))
Blueprint lines 2536-2560 (three cores at a cell, fresh side offset averaged, eq:side-windows)
with explicit Fourier truncations: the form with three core inputs and side f_l is at most twice
the offset average of three_core_principal_of (the side cutoff and the gauge multiplier are
truncated afresh at each side offset ρ', the core cutoffs by the given cc0), with
- the re-anchored multiplier bounded by
(1 + τ_m)(1 + τ_c)and the core torus sizes‖g_j‖_{L²(𝓗)}of the truncated cores (no|box|or√|N|factor), - the side windows
b_i = (E_ρ X_i)^{1/2}of radius2^i ≤ 2^Iafter Cauchy-Schwarz (sideWinE) and the shells above2^Iby theL²norm of the side, - the absolute expansion coefficient sum by
multNorm Π_j (cutNorm Σ_{F_j} |c|).
theorem
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.Tt_ge_U0_four
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
{Cj CA CT CK : ℕ}
{δs W : ℝ}
(hV : D.S.Valid Cj CA CT CK δs W)
(hCT : 4 ≤ CT)
(hd2 : 2 ≤ D.S.dmax)
(hD : 2 ≤ D.S.Dstar)
(hB : 2 ≤ D.S.Bstar)
(hQ : 1 ≤ D.S.Q0)
(hSP : D.SP = D.S.sideParams δs)
{h' : ℕ}
(hh : h' ≤ D.SP.Jst)
:
At the chosen schedule L_{h'} (U₀ + 4) ≤ T for h' ≤ J_* (as Tt_ge_U0, with
U₀ + 4 ≤ Ξ = D_*^{1000}): the far cosets of the three-core test are at least 4 away from the
reference (H ≥ 4 in three_core_averaged_of).
noncomputable def
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeWin
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(G : bf.Grp)
(I : ℤ × ℤ)
(_xs : ℝ)
(h' : ℕ)
(l : Fin 4)
(a : Fin 4 → ℝ)
(Λ : ℝ)
:
The side windows of a three-core tuple with side role l (blueprint lines 2556-2560): the
integers k with |k - r(Q + n·ξ)| ≤ 2Λ for some integer n in the box |n|_∞ ≤ 16 B'_{h'}
(Q = Σ_{j ≠ l} γ_j^*, ξ = ϑ/L_{h'} in the chart of role 0). The windows use the entire box
and do not depend on the mode masks.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.mem_threeWin
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
(hD : 0 ≤ D.S.Dstar)
{G : bf.Grp}
{I : ℤ × ℤ}
{xs : ℝ}
{h' : ℕ}
{l : Fin 4}
{a : Fin 4 → ℝ}
{Λ : ℝ}
{k : ℤ}
{n : Fin (D.Ms 0 G).zc.dim → ℤ}
(hn : ∀ (i : Fin (D.Ms 0 G).zc.dim), |↑(n i)| ≤ 16 * (D.S.Dstar ^ 5 * D.S.Eh h'))
(hk :
|↑k - dyadicGridLength A.G I.1 * (threeQ l a + ∑ i : Fin (D.Ms 0 G).zc.dim, ↑(n i) * (D.Ms 0 G).torusξ D.S h' i)| ≤ 2 * Λ)
:
theorem
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.three_core_inputs
(κ' : LocalKernelClass)
(c₀ : ℕ)
(A : ActiveSetup κ' c₀)
(bf : A.BasicFamilies)
(fp : bf.FamParams)
(D : fp.SideInput)
(I : ℤ × ℤ)
(G : bf.Grp)
(hz : ∀ (j : Fin 4), (D.Ms j G).zc = (D.Ms 0 G).zc)
(δ : ℝ)
(hδ : 0 < δ)
(hδc : ∀ (j : Fin 4), (D.Ms j G).δc = δ)
(hρ : ∀ (j : Fin 4) (k : Fin (D.Ms j G).zc.dim), (D.Ms j G).ρ k ∈ Set.Icc 0 1)
(Kt h : ℕ)
(l : Fin 4)
(Fsel : (j : Fin 4) → Finset ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))))
(n :
(j : Fin 4) →
↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))) → Fin (D.Ms j G).zc.dim → ℤ)
(hn :
∀ (j : Fin 4), j ≠ l → ∀ x ∈ Fsel j, ∀ (i : Fin (D.Ms j G).zc.dim), |↑(n j x i)| ≤ D.S.Dstar * D.S.Eh (h - D.SP.Δ))
(a : Fin 4 → ℝ)
(xs : ℝ)
(hform :
∀ (j : Fin 4),
j ≠ l →
∀ y ∈ dyadicGridCell A.G I.1 I.2,
‖∑ x ∈ Fsel j, D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x * (D.Ms j G).wave (↑x) y - ↑(Real.fourierChar (↑(D.Ms j G).cl * centerPhase (D.Ms j G).zc (D.Ms j G).ρ y)) * ↑(Real.fourierChar (a j * (y - xs))) * (D.Ms j G).torusG D.S (h - D.SP.Δ) xs (Fsel j)
(fun (x : ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) =>
D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x)
(n j) fun (i : Fin (D.Ms j G).zc.dim) => (D.Ms j G).torusξ D.S (h - D.SP.Δ) i * (y - xs)‖ ≤ (D.S.Dstar ^ 150)⁻¹ * ∑ x ∈ Fsel j, ‖D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x‖)
(X : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)))
(hr : 0 < dyadicGridLength A.G I.1)
(hw : IsAdmissibleLocalKernel κ' (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1) (A.w I))
(hDp : 0 < D.S.Dstar)
(hQ0 : 0 < D.S.Q0)
(hE0 : 0 ≤ D.S.Eh (h - D.SP.Δ))
(hη : 0 ≤ (D.S.Dstar ^ 150)⁻¹)
:
∃ (ρ' : (j : Fin 4) → j ≠ l → Fin (D.Ms 0 G).zc.dim → ℝ) (n' :
(j : Fin 4) →
j ≠ l → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))) → Fin (D.Ms 0 G).zc.dim → ℤ)
(f : (j : Fin 4) → j ≠ l → ℝ → ℂ) (ρc : Fin 4 → Fin (D.Ms 0 G).zc.dim → ℝ) (nn :
(j : Fin 4) →
↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))) → Fin (D.Ms 0 G).zc.dim → ℤ)
(fv : Fin 4 → ℝ → ℂ) (cα :
(j : Fin 4) → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))) → ℂ) (cc0 :
Fin 4 → (Fin (D.Ms 0 G).zc.dim → ℤ) → ℂ),
(∀ (j : Fin 4) (hj : j ≠ l),
∀ y ∈ Set.Icc (dyadicGridLeft A.G I.1 I.2) (dyadicGridLeft A.G I.1 I.2 + dyadicGridLength A.G I.1),
‖f j hj y - ↑(centerCut (D.Ms 0 G).zc (D.Ms j G).δc (ρ' j hj) y) * ↑(Real.fourierChar (↑(D.Ms j G).cl * centerPhase (D.Ms 0 G).zc (ρ' j hj) y)) * (↑(Real.fourierChar (a j * (y - xs))) * ∑ x ∈ Fsel j,
D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x * ↑(Real.fourierChar ((D.Ms j G).phase (↑x) xs)) * torusCharacter (n' j hj x)
(torusMk fun (i : Fin (D.Ms 0 G).zc.dim) =>
(D.Ms 0 G).zc.θ i / (↑D.S.Q0 * ↑(6 ^ (h - D.SP.Δ))) * (y - xs)))‖ ≤ (D.S.Dstar ^ 150)⁻¹ * ∑ x ∈ Fsel j,
‖D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x * ↑(Real.fourierChar ((D.Ms j G).phase (↑x) xs))‖) ∧ (∀ (j : Fin 4) (hj : j ≠ l),
∀ y ∈ Set.Icc (dyadicGridLeft A.G I.1 I.2) (dyadicGridLeft A.G I.1 I.2 + dyadicGridLength A.G I.1),
‖f j hj y‖ ≤ ∑ x ∈ Fsel j,
‖D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x * ↑(Real.fourierChar ((D.Ms j G).phase (↑x) xs))‖) ∧ (∀ (j : Fin 4) (hj : j ≠ l),
(Set.Ico (dyadicGridLeft A.G I.1 I.2) (dyadicGridLeft A.G I.1 I.2 + dyadicGridLength A.G I.1)).indicator
(f j hj) = (Set.Ico (dyadicGridLeft A.G I.1 I.2) (dyadicGridLeft A.G I.1 I.2 + dyadicGridLength A.G I.1)).indicator
fun (y : ℝ) => ∑ x ∈ Fsel j, D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x * (D.Ms j G).wave (↑x) y) ∧ (∀ (j : Fin 4) (hj : j ≠ l) (cc0 : (Fin (D.Ms 0 G).zc.dim → ℤ) → ℂ),
(∀ (w : Fin (D.Ms 0 G).zc.dim → ℝ),
‖cutoffP (D.Ms j G).δc (ρ' j hj) w - ∑ v ∈ frequencyBox (D.Ms 0 G).zc.dim (2 ^ (Kt + 1)),
cc0 v * ↑(Real.fourierChar (∑ i : Fin (D.Ms 0 G).zc.dim, ↑(v i) * w i))‖ ≤ cutTail (D.Ms 0 G).zc.dim (D.Ms j G).δc Kt) →
(MeasureTheory.eLpNorm
(fun
(u :
↥(torusAnnihilator
(rationalIntegerIntersection
(tinySpan (fun (i : Fin (D.Ms 0 G).zc.dim) => (D.Ms 0 G).zc.θ i / ↑D.S.Q0) D.SP.Hn
(D.SP.Tt⁻¹ / dyadicGridLength A.G (A.blkStart D.S.K I.1 - 2 * ↑D.S.K)))))) =>
∑ p ∈ frequencyBox (D.Ms 0 G).zc.dim (2 ^ (Kt + 1)) ×ˢ Fsel j,
cc0 p.1 * ↑(Real.fourierChar (∑ i : Fin (D.Ms 0 G).zc.dim, ↑(p.1 i) * ((D.Ms 0 G).zc.θ i * xs))) * (D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑p.2 * ↑(Real.fourierChar ((D.Ms j G).phase (↑p.2) xs))) * torusCharacter (↑(D.S.Q0 * 6 ^ (h - D.SP.Δ)) • p.1 + n' j hj p.2) ↑u)
2
(torusAnnihilatorHaar
(rationalIntegerIntersection
(tinySpan (fun (i : Fin (D.Ms 0 G).zc.dim) => (D.Ms 0 G).zc.θ i / ↑D.S.Q0) D.SP.Hn
(D.SP.Tt⁻¹ / dyadicGridLength A.G (A.blkStart D.S.K I.1 - 2 * ↑D.S.K)))))).toReal ≤ (MeasureTheory.eLpNorm
(fun
(u :
↥(torusAnnihilator
(rationalIntegerIntersection
(tinySpan (fun (i : Fin (D.Ms j G).zc.dim) => (D.Ms j G).zc.θ i / ↑D.S.Q0) D.SP.Hn
(D.SP.Tt⁻¹ / dyadicGridLength A.G (A.blkStart D.S.K I.1 - 2 * ↑D.S.K)))))) =>
(D.Ms j G).torusGT D.S (h - D.SP.Δ) xs (Fsel j)
(fun (x : ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) =>
D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x)
(n j) ↑u)
2
(torusAnnihilatorHaar
(rationalIntegerIntersection
(tinySpan (fun (i : Fin (D.Ms j G).zc.dim) => (D.Ms j G).zc.θ i / ↑D.S.Q0) D.SP.Hn
(D.SP.Tt⁻¹ / dyadicGridLength A.G (A.blkStart D.S.K I.1 - 2 * ↑D.S.K)))))).toReal + cutTail (D.Ms 0 G).zc.dim (D.Ms j G).δc Kt * ∑ x ∈ Fsel j, ‖D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x‖) ∧ (∀ (j : Fin 4) (k : Fin (D.Ms 0 G).zc.dim), ρc j k ∈ Set.Icc 0 1) ∧ (∀ (j : Fin 4) (hj : j ≠ l), ρc j = ρ' j hj) ∧ (∀ (j : Fin 4) (hj : j ≠ l)
(x : ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))),
nn j x = n' j hj x) ∧ fv l = augPhys X ∧ (∀ (j : Fin 4) (hj : j ≠ l), fv j = f j hj) ∧ (∀ (j : Fin 4)
(x : ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))),
cα j x = D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x * ↑(Real.fourierChar ((D.Ms j G).phase (↑x) xs))) ∧ (∀ (j : Fin 4), j ≠ l → sideOptF l Fsel j = Finset.map Function.Embedding.some (Fsel j)) ∧ Measurable (augPhys X) ∧ MeasureTheory.MemLp (augPhys X) 2
(MeasureTheory.volume.restrict
(Set.Ioc (dyadicGridLeft A.G I.1 I.2)
(dyadicGridLeft A.G I.1 I.2 + dyadicGridLength A.G I.1))) ∧ MeasureTheory.Integrable
(fun (zz : ℝ × ℝ) => A.w I zz * ∏ j : Fin 4, fv j (realProgressionCoordinate j zz))
MeasureTheory.volume ∧ (∀ (ρ'' : Fin (D.Ms 0 G).zc.dim → ℝ),
MeasureTheory.Integrable
(fun (zz : ℝ × ℝ) =>
A.w I zz * ∏ j : Fin 4,
Function.update fv l
(fun (y : ℝ) => ↑(centerCut (D.Ms 0 G).zc δ ρ'' y) * fv l y) j
(realProgressionCoordinate j zz))
MeasureTheory.volume) ∧ (∀ (j : Fin 4) (v : Fin (D.Ms 0 G).zc.dim → ℤ), ‖cc0 j v‖ ≤ 1) ∧ (∀ (j : Fin 4) (s : Finset (Fin (D.Ms 0 G).zc.dim → ℤ)),
∑ v ∈ s, ‖cc0 j v‖ ≤ cutNorm (D.Ms 0 G).zc.dim δ) ∧ (∀ (j : Fin 4) (w : Fin (D.Ms 0 G).zc.dim → ℝ),
‖cutoffP δ (ρc j) w - ∑ v ∈ frequencyBox (D.Ms 0 G).zc.dim (2 ^ (Kt + 1)),
cc0 j v * ↑(Real.fourierChar (∑ i : Fin (D.Ms 0 G).zc.dim, ↑(v i) * w i))‖ ≤ cutTail (D.Ms 0 G).zc.dim δ Kt) ∧ ∀ (j : Fin 4),
∀ k ∈ sideOptF l Fsel j,
∀ (i : Fin (D.Ms 0 G).zc.dim),
|↑(sideOptN nn j k i)| ≤ D.S.Dstar * D.S.Eh (h - D.SP.Δ)
Prepare the three core roles in a common chart, with bounded offset frequencies, integrable physical products and simultaneous cutoff truncations. Both reference and nonreference estimates consume the same evidence.
theorem
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.three_core_form
(κ' : LocalKernelClass)
(c₀ : ℕ)
(A : ActiveSetup κ' c₀)
(bf : A.BasicFamilies)
(fp : bf.FamParams)
(D : fp.SideInput)
(I : ℤ × ℤ)
(hI : I ∈ A.cells)
(G : bf.Grp)
(l : Fin 4)
(Fsel : (j : Fin 4) → Finset ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))))
(X : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)))
(f : (j : Fin 4) → j ≠ l → ℝ → ℂ)
(fv : Fin 4 → ℝ → ℂ)
(hind :
∀ (j : Fin 4) (hj : j ≠ l),
(Set.Ico (dyadicGridLeft A.G I.1 I.2) (dyadicGridLeft A.G I.1 I.2 + dyadicGridLength A.G I.1)).indicator (f j hj) = (Set.Ico (dyadicGridLeft A.G I.1 I.2) (dyadicGridLeft A.G I.1 I.2 + dyadicGridLength A.G I.1)).indicator
fun (y : ℝ) => ∑ x ∈ Fsel j, D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x * (D.Ms j G).wave (↑x) y)
(hfvl : fv l = augPhys X)
(hfvj : ∀ (j : Fin 4) (hj : j ≠ l), fv j = f j hj)
:
(fp.Λc I)
(Function.update (fun (j : Fin 4) => D.compSub j G I (Finset.map { toFun := Subtype.val, inj' := ⋯ } (Fsel j))) l
X) = localProgressionForm (dyadicGridLength A.G I.1) (A.w I) fv
The cell form agrees with the common-chart physical inputs.
theorem
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.three_core_coefficient_products
(κ' : LocalKernelClass)
(c₀ : ℕ)
(A : ActiveSetup κ' c₀)
(bf : A.BasicFamilies)
(fp : bf.FamParams)
(D : fp.SideInput)
(I : ℤ × ℤ)
(G : bf.Grp)
(l : Fin 4)
(Fsel : (j : Fin 4) → Finset ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))))
(xs : ℝ)
(cα : (j : Fin 4) → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))) → ℂ)
(hcα :
∀ (j : Fin 4) (x : ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))),
cα j x = D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x * ↑(Real.fourierChar ((D.Ms j G).phase (↑x) xs)))
(δ : ℝ)
:
(∀ (j : Fin 4),
j ≠ l →
∑ k ∈ sideOptF l Fsel j, ‖sideOptC cα j k‖ = ∑ x ∈ Fsel j, ‖D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x‖) ∧ ∏ j : Fin 4, ∑ k ∈ sideOptF l Fsel j, ‖sideOptC cα j k‖ = ∏ j ∈ Finset.univ.erase l, ∑ x ∈ Fsel j, ‖D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x‖ ∧ ∏ j : Fin 4, cutNorm (D.Ms 0 G).zc.dim δ * ∑ k ∈ sideOptF l Fsel j, ‖sideOptC cα j k‖ = cutNorm (D.Ms 0 G).zc.dim δ * ∏ j ∈ Finset.univ.erase l,
cutNorm (D.Ms 0 G).zc.dim δ * ∑ x ∈ Fsel j, ‖D.c j G (A.blkStart D.S.K I.1) (D.preAt I) ↑x‖
The distinguished side contributes one to both coefficient products.