Trilinear Hilbert transform: three_core_ref_bound #
theorem
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.three_core_ref_bound
{κ' : 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 < δ)
(hdδ : 8 * ↑(D.Ms 0 G).zc.dim * δ ≤ 1)
(hδ8 : δ ≤ 1 / 8)
(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)
{Kt : ℕ}
(hQB : ↑D.S.Q0 * 2 ^ (Kt + 1) ≤ D.S.Bstar)
(hτc : cutTail (D.Ms 0 G).zc.dim δ Kt ≤ (D.S.Dstar ^ 300)⁻¹)
(hτm : multTail (D.Ms 0 G).zc.dim (δ / 2) D.S.Q0 Cm Kt ≤ (D.S.Dstar ^ 300)⁻¹)
(hMN : multNorm (D.Ms 0 G).zc.dim (δ / 2) D.S.Q0 Cm ≤ D.S.Dstar)
(hCN : cutNorm (D.Ms 0 G).zc.dim δ ≤ D.S.Dstar)
{J : ℕ}
(hJ : 3 ≤ J)
{h : ℕ}
(hh : h ≤ D.SP.Jst)
(j₀ : Fin 4)
{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₀)
(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 : ℝ}
(hxs : xs ∈ dyadicGridCell A.G I.1 I.2)
(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‖)
(hne : (D.threeRefSet G I xs (h - D.SP.Δ) l a).Nonempty)
(X : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)))
(Aw Iw : ℕ)
(hAw : 1 ≤ Aw)
(hIw : D.U0 ≤ 2 ^ (Iw + 1))
:
‖(fp.Λc I)
(Function.update (fun (j : Fin 4) => D.compSub j G I (Finset.map { toFun := Subtype.val, inj' := ⋯ } (Fsel j))) l
X)‖ ≤ D.threePrin G I xs (h - D.SP.Δ) l a Fsel n X J Aw Iw + ((208 * localKernelSupBound κ' + 252 * 2 ^ (Aw + 4) * entryCU κ' J Aw + 2 * nearBC κ' + 96 * kerC κ' J) * (D.S.Dstar ^ 100)⁻¹ * ∏ j ∈ Finset.univ.erase l, D.coefSum G I j (Fsel j)) * √((dyadicGridLength A.G I.1)⁻¹ * ∫ (y : ℝ) in dyadicGridLeft A.G I.1 I.2..dyadicGridLeft A.G I.1 I.2 + dyadicGridLength A.G I.1, ‖augPhys X y‖ ^ 2)
Blueprint eq:core-numerical (lines 2562-2567) for a three-core tuple with a reference on a
leaf cell of the side states (enlarged gauge cutoff δ/2, truncation tails at most D_*^{-300},
full Fourier norms at most D_*, J ≥ 3, windows up to 2^{I_w} ≥ U₀/2): the cell form with the
side X in slot l is at most the principal window quantity threePrin (true torus sizes) plus
C D_*^{-100} Π_{j ≠ l} Σ_{F_j} |α| σ, with σ = (r⁻¹ ∫_I |S_phys|²)^{1/2} the local side size.
The error collects the torus-form and gauge errors (gauge_err_le), the truncation parts of the
core sizes (trunc_core_err3, window_split), the shells above 2^{I_w} (2^{-(I_w+1)(A+1)} ≤ U₀⁻¹), and the coset replacement and tails (nearB_le, T⁻¹/L ≤ D_*^{-999}).