Trilinear Hilbert transform: band_scale_sum_assembly #
theorem
TrilinearHT.Auto.band_scale_sum_assembly
(κ : LocalKernelClass)
{d : ℕ}
(hd : 1 ≤ d)
(A : QuadraticChartData d)
(hAb : IsBoundedQuadraticChart A)
(D J1 m : ℕ)
{Lh : ℝ}
(hLh : 0 ≤ Lh)
(G : RealDyadicGrid)
(J : ℤ × ℤ)
(S : Finset (ℤ × ℤ))
(hSJ : ∀ I ∈ S, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G J.1 J.2)
(w : ℤ × ℤ → ℝ × ℝ → ℂ)
(hw : ∀ I ∈ S, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I))
{a b : Fin 4}
(hab : a ≠ b)
{ψa ψb : ℝ → ℂ}
(hψam : Measurable ψa)
(hψbm : Measurable ψb)
(hψa : ∀ (y : ℝ), ‖ψa y‖ ≤ 1)
(hψb : ∀ (y : ℝ), ‖ψb y‖ ≤ 1)
{Fa Fb : ℝ → ℂ}
{za zb : ℤ × ℤ → ℝ → ℂ}
{Ka Kb : ℝ}
(hKa : 0 ≤ Ka)
(hKb : 0 ≤ Kb)
(hza : IsAdmissibleOpponent G J Fa za Ka)
(hzb : IsAdmissibleOpponent G J Fb zb Kb)
(hEa : HasDepthEnergy G J Fa za Ka)
(hEb : HasDepthEnergy G J Fb zb Kb)
(hzam : ∀ (I : ℤ × ℤ), Measurable (za I))
(hzbm : ∀ (I : ℤ × ℤ), Measurable (zb I))
(hza2 : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (za I) 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2)))
(hzb2 : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (zb I) 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2)))
(hband : ∀ I ∈ S, ∀ (ξ : ℝ), bandAmplitude (quadraticChartAtom A) (dyadicGridLength G I.1) ξ ≤ Real.exp (-↑m))
(lamf : ℤ → ℝ)
(Mf : ℤ → Matrix (Fin d) (Fin d) ℚ)
(σf : ℤ → ℕ × (Fin (d + d) → ℤ) → Fin d → ℚ)
(coeff : ℤ → ℕ × (Fin (d + d) → ℤ) → ℂ)
(hprops :
∀ s ∈ Finset.image Prod.fst S,
(∀ (i j : Fin d), ↑(rationalHeight (Mf s i j)) ≤ bsE D m Lh) ∧ lamf s = A.quadratic + ∑ i : Fin d, ∑ j : Fin d, A.horizontal i * ↑(Mf s i j) * A.horizontal j ∧ |lamf s| * dyadicGridLength G s ^ 2 ≤ bsE D m Lh ∧ (∀ (p : ℕ × (Fin (d + d) → ℤ)) (i : Fin d),
↑(rationalHeight (σf s p i)) ≤ bsE D m Lh * (1 + frequencyLength p.2)) ∧ (∀ (t : ℝ),
|t| ≤ 2 * dyadicGridLength G s →
HasSum
(fun (p : ℕ × (Fin (d + d) → ℤ)) =>
coeff s p * quadPhase (lamf s) (A.linear + ∑ i : Fin d, ↑(σf s p i) * A.horizontal i) t)
(quadraticChartAtom A t)) ∧ (Summable fun (p : ℕ × (Fin (d + d) → ℤ)) => ‖coeff s p‖) ∧ ∑' (p : ℕ × (Fin (d + d) → ℤ)), ‖coeff s p‖ ≤ bsE D m Lh ∧ (∀ (p : ℕ × (Fin (d + d) → ℤ)), ⌊bsE D m Lh⌋₊ ≤ p.1 → coeff s p = 0) ∧ ∀ (p : ℕ × (Fin (d + d) → ℤ)), ‖coeff s p‖ * (1 + frequencyLength p.2) ^ (d + 1) ^ 2 ≤ bsE1 J1 m Lh)
(hzero : ∀ s ∉ Finset.image Prod.fst S, coeff s = 0)
:
∑ I ∈ S,
dyadicGridLength G I.1 * ‖separatedLocalForm (dyadicGridLength G I.1) (w I) (quadraticChartAtom A) a b (fun (y : ℝ) => ψa y * za I y)
fun (y : ℝ) => ψb y * zb I y‖ ≤ Real.exp (-↑m) * bandBracket κ d D J1 m Lh * Ka * Kb * √(∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖Fa y‖ ^ 2) * √(∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖Fb y‖ ^ 2)
Assembly of eq:band-scale-sum from per-depth chart expansions with the explicit
parameters (blueprint lem:predictors, proof lines 1517–1542).
theorem
TrilinearHT.Auto.band_scale_sum_param
(c₀ : ℕ)
(hc : 1 ≤ c₀)
(κ : LocalKernelClass)
:
∃ (D : ℕ) (J1 : ℕ),
1 ≤ D ∧ ∀ {d : ℕ} (H : ℝ) (A : QuadraticChartData d),
1 ≤ d →
QuadraticChartComplexity c₀ H A →
IsBoundedQuadraticChart A →
∀ (m : ℕ) (G : RealDyadicGrid) (J : ℤ × ℤ) (S : Finset (ℤ × ℤ)),
(∀ I ∈ S, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G J.1 J.2) →
∀ (w : ℤ × ℤ → ℝ × ℝ → ℂ),
(∀ I ∈ S, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) →
∀ {a b : Fin 4},
a ≠ b →
∀ {ψa ψb : ℝ → ℂ},
Measurable ψa →
Measurable ψb →
(∀ (y : ℝ), ‖ψa y‖ ≤ 1) →
(∀ (y : ℝ), ‖ψb y‖ ≤ 1) →
∀ {Fa Fb : ℝ → ℂ} {za zb : ℤ × ℤ → ℝ → ℂ} {Ka Kb : ℝ},
0 ≤ Ka →
0 ≤ Kb →
IsAdmissibleOpponent G J Fa za Ka →
IsAdmissibleOpponent G J Fb zb Kb →
HasDepthEnergy G J Fa za Ka →
HasDepthEnergy G J Fb zb Kb →
(∀ (I : ℤ × ℤ), Measurable (za I)) →
(∀ (I : ℤ × ℤ), Measurable (zb I)) →
(∀ (I : ℤ × ℤ),
MeasureTheory.MemLp (za I) 2
(MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) →
(∀ (I : ℤ × ℤ),
MeasureTheory.MemLp (zb I) 2
(MeasureTheory.volume.restrict
(dyadicGridCell G I.1 I.2))) →
(∀ I ∈ S,
InScaleBand (quadraticChartAtom A) m
(dyadicGridLength G I.1)) →
∑ I ∈ S,
dyadicGridLength G I.1 * ‖separatedLocalForm (dyadicGridLength G I.1) (w I)
(quadraticChartAtom A) a b
(fun (y : ℝ) => ψa y * za I y) fun (y : ℝ) =>
ψb y * zb I y‖ ≤ Real.exp (-↑m) * bandBracket κ d D J1 m
(Real.log (max H (bandLip + 1))) * Ka * Kb * √(∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖Fa y‖ ^ 2) * √(∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖Fb y‖ ^ 2)
Blueprint lem:predictors, eq:band-scale-sum with explicit parameters: for one
separated time factor Q (a bounded chart of complexity H) and admissible opponents,
the absolute length-weighted sum over the cells of the m-th Fourier-supremum band is at
most e^{-m} times the explicit bracket bandBracket (a polynomial in 1 + m, log H;
see band_scale_sum).
A uniform numeric constant bounding log(128π (3 + 8 C_ζ)).
Equations
- TrilinearHT.Auto.bsLConst = Real.log (128 * Real.pi * (3 + 8 * TrilinearHT.Auto.bandDecay))
Instances For
The explicit constant controlling log(1 + C_T).
Equations
Instances For
The explicit constant of the final polynomial bound of the band bracket.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TrilinearHT.Auto.bandBracket_le
{D J1 m : ℕ}
{Lh : ℝ}
(κ : LocalKernelClass)
{d : ℕ}
(hLh : 0 ≤ Lh)
(hdL : ↑d ≤ Lh)
:
The eq:band-scale-sum bracket is polynomial in W = 2 + m + log H.
theorem
TrilinearHT.Auto.band_scale_sum
(c₀ : ℕ)
(hc : 1 ≤ c₀)
(κ : LocalKernelClass)
:
∃ (C : ℕ),
∀ {d : ℕ} (H : ℝ) (A : QuadraticChartData d),
1 ≤ d →
QuadraticChartComplexity c₀ H A →
IsBoundedQuadraticChart A →
∀ (m : ℕ) (G : RealDyadicGrid) (J : ℤ × ℤ) (S : Finset (ℤ × ℤ)),
(∀ I ∈ S, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G J.1 J.2) →
∀ (w : ℤ × ℤ → ℝ × ℝ → ℂ),
(∀ I ∈ S, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) →
∀ {a b : Fin 4},
a ≠ b →
∀ {ψa ψb : ℝ → ℂ},
Measurable ψa →
Measurable ψb →
(∀ (y : ℝ), ‖ψa y‖ ≤ 1) →
(∀ (y : ℝ), ‖ψb y‖ ≤ 1) →
∀ {Fa Fb : ℝ → ℂ} {za zb : ℤ × ℤ → ℝ → ℂ} {Ka Kb : ℝ},
0 ≤ Ka →
0 ≤ Kb →
IsAdmissibleOpponent G J Fa za Ka →
IsAdmissibleOpponent G J Fb zb Kb →
HasDepthEnergy G J Fa za Ka →
HasDepthEnergy G J Fb zb Kb →
(∀ (I : ℤ × ℤ), Measurable (za I)) →
(∀ (I : ℤ × ℤ), Measurable (zb I)) →
(∀ (I : ℤ × ℤ),
MeasureTheory.MemLp (za I) 2
(MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) →
(∀ (I : ℤ × ℤ),
MeasureTheory.MemLp (zb I) 2
(MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) →
(∀ I ∈ S,
InScaleBand (quadraticChartAtom A) m
(dyadicGridLength G I.1)) →
∑ I ∈ S,
dyadicGridLength G I.1 * ‖separatedLocalForm (dyadicGridLength G I.1) (w I)
(quadraticChartAtom A) a b
(fun (y : ℝ) => ψa y * za I y) fun (y : ℝ) =>
ψb y * zb I y‖ ≤ Real.exp (-↑m) * (↑C * (2 + ↑m + Real.log H) ^ C) * Ka * Kb * √(∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖Fa y‖ ^ 2) * √(∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖Fb y‖ ^ 2)
Blueprint lem:predictors, eq:band-scale-sum: for one separated time factor
Q = quadraticChartAtom A, a bounded chart of complexity H (fixed Gevrey order c₀), and
admissible opponents with transfer constants K_a, K_b, the absolute length-weighted sum
over the cells of the m-th Fourier-supremum band e^{-m-1} < A_{|I|} ≤ e^{-m} is at most
e^{-m} C (2 + m + log H)^C K_a K_b ‖1_J F_a‖₂ ‖1_J F_b‖₂, with C depending only on the
Gevrey order and the kernel class.
theorem
TrilinearHT.Auto.separatedLocalForm_phase_distribute
(r : ℝ)
(w : ℝ × ℝ → ℂ)
(lam γ : ℝ)
{a b : Fin 4}
(hab : a ≠ b)
(Fa Fb : ℝ → ℂ)
:
separatedLocalForm r w (quadPhase lam γ) a b Fa Fb = separatedLocalForm r w (fun (t : ℝ) => ↑(Real.fourierChar (lam * t ^ 2))) a b
(fun (y : ℝ) => ↑(Real.fourierChar (-(γ / (↑↑b - ↑↑a) * y))) * Fa y) fun (y : ℝ) =>
↑(Real.fourierChar (γ / (↑↑b - ↑↑a) * y)) * Fb y
Blueprint lem:predictors, proof line 1543 ("distribute each e(γt) between the two
remaining slots"): on the progression t = (y_b - y_a)/(b - a).
The Fourier-supremum A_r = sup_ξ |∫ Q(ru) ζ(u) e(-ξu) du| of a time factor.
Equations
- TrilinearHT.Auto.bandSup Q r = ⨆ (ξ : ℝ), TrilinearHT.Auto.bandAmplitude Q r ξ
Instances For
theorem
TrilinearHT.Auto.separatedLocalForm_eq_zero_of_bandSup
{κ : LocalKernelClass}
{a₀ r : ℝ}
(hr : 0 < r)
{w : ℝ × ℝ → ℂ}
(hw : IsAdmissibleLocalKernel κ a₀ r w)
{a b : Fin 4}
(hab : a ≠ b)
{Q : ℝ → ℂ}
(hQm : Measurable Q)
(hQ1 : ∀ (t : ℝ), ‖Q t‖ ≤ 1)
(h0 : bandSup Q r = 0)
{Fa Fb : ℝ → ℂ}
(hFam : Measurable Fa)
(hFbm : Measurable Fb)
(hFa : MeasureTheory.MemLp Fa 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r))))
(hFb : MeasureTheory.MemLp Fb 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r))))
:
The separated form vanishes at scales whose band supremum vanishes
(blueprint lem:predictors, line 1495: "the term vanishes when A_{|I|} = 0").
theorem
TrilinearHT.Auto.quarterChart_bounded
{d : ℕ}
{A : QuadraticChartData d}
(hAb : IsBoundedQuadraticChart A)
:
IsBoundedQuadraticChart (scaleQuadraticChartAmplitude (1 / 4) A)
theorem
TrilinearHT.Auto.quarterChart_norm_le
{d : ℕ}
{A : QuadraticChartData d}
(hAb : IsBoundedQuadraticChart A)
(y : ℝ)
:
theorem
TrilinearHT.Auto.chart_band_range_scale_sum
(c₀ : ℕ)
(hc : 1 ≤ c₀)
(κ : LocalKernelClass)
:
∃ (C : ℕ),
∀ {d : ℕ} (H : ℝ) (A : QuadraticChartData d),
1 ≤ d →
QuadraticChartComplexity c₀ H A →
IsBoundedQuadraticChart A →
∀ (M₀ : ℕ) (G : RealDyadicGrid) (J : ℤ × ℤ) (S : Finset (ℤ × ℤ)),
(∀ I ∈ S, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G J.1 J.2) →
∀ (w : ℤ × ℤ → ℝ × ℝ → ℂ),
(∀ I ∈ S, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) →
∀ {a b : Fin 4},
a ≠ b →
∀ {ψa ψb : ℝ → ℂ},
Measurable ψa →
Measurable ψb →
(∀ (y : ℝ), ‖ψa y‖ ≤ 1) →
(∀ (y : ℝ), ‖ψb y‖ ≤ 1) →
∀ {Fa Fb : ℝ → ℂ} {za zb : ℤ × ℤ → ℝ → ℂ} {Ka Kb : ℝ},
0 ≤ Ka →
0 ≤ Kb →
IsAdmissibleOpponent G J Fa za Ka →
IsAdmissibleOpponent G J Fb zb Kb →
HasDepthEnergy G J Fa za Ka →
HasDepthEnergy G J Fb zb Kb →
(∀ (I : ℤ × ℤ), Measurable (za I)) →
(∀ (I : ℤ × ℤ), Measurable (zb I)) →
(∀ (I : ℤ × ℤ),
MeasureTheory.MemLp (za I) 2
(MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) →
(∀ (I : ℤ × ℤ),
MeasureTheory.MemLp (zb I) 2
(MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) →
(∀ I ∈ S,
bandSup
(quadraticChartAtom
(scaleQuadraticChartAmplitude (1 / 4) A))
(dyadicGridLength G I.1) ≤ Real.exp (-↑M₀)) →
∑ I ∈ S,
dyadicGridLength G I.1 * ‖separatedLocalForm (dyadicGridLength G I.1) (w I)
(quadraticChartAtom A) a b
(fun (y : ℝ) => ψa y * za I y) fun (y : ℝ) =>
ψb y * zb I y‖ ≤ Real.exp (-↑M₀ / 2) * (↑C * (2 + Real.log H) ^ C) * Ka * Kb * √(∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖Fa y‖ ^ 2) * √(∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖Fb y‖ ^ 2)
Blueprint lem:predictors, proof lines 1544-1546: the band scale sums of one separated
time factor summed over all bands m ≥ M₀ of the normalized factor Q/4.