Trilinear Hilbert transform: expansion_catalog_tail

theorem TrilinearHT.Auto.expansion_catalog_tail (κ : LocalKernelClass) {d : ℕ} (hd : 1 ≤ d) (A : QuadraticChartData d) {E E1 : ℝ} (hE : 1 ≤ E) (hE10 : 0 ≤ E1) (K₀ : ℕ) (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))) (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)) ≤ E) ∧ 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 ≤ E ∧ (∀ (p : ℕ × (Fin (d + d) → ℤ)) (i : Fin d), ↑(rationalHeight (σf s p i)) ≤ E * (1 + frequencyLength p.2)) ∧ (∀ (p : ℕ × (Fin (d + d) → ℤ)), ⌊E⌋₊ ≤ p.1 → coeff s p = 0) ∧ ∀ (p : ℕ × (Fin (d + d) → ℤ)), ‖coeff s p‖ * (1 + frequencyLength p.2) ^ (d + 1) ^ 2 ≤ E1) : (∑ I ∈ S, dyadicGridLength G I.1 * ∑' (p : ℕ × (Fin (d + d) → ℤ)), if p ∈ Finset.range ⌊E⌋₊ ×ˢ frequencyTruncationSet (d + d) K₀ then 0 else ‖coeff I.1 p‖ * ‖separatedLocalForm (dyadicGridLength G I.1) (w I) (quadPhase (lamf I.1) (A.linear + ∑ i : Fin d, ↑(σf I.1 p i) * A.horizontal i)) a b (fun (y : ℝ) => ψa y * za I y) fun (y : ℝ) => ψb y * zb I y‖) ≤ ↑⌊E⌋₊ * (E1 * tailCT κ d E * (2 * 7 ^ (d + d) * (2 * Real.pi) ^ ((d + 1) ^ 2 - 1) / 2 ^ K₀)) * 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 1519-1523: the pooled chart-expansion tails outside a finite catalog are small in the absolute scale-sum norm.

theorem TrilinearHT.Auto.weighted_shell_tail {τ : Type u_1} (cf : τ → ℂ) (size : τ → ℝ) {Es : ℝ} (hEs : 0 ≤ Es) (htail : ∀ (T : ℝ), 1 ≤ T → (∑' (q : τ), if T ≤ size q then ‖cf q‖ else 0) ≤ Es / T ^ 100) (hcs : Summable fun (q : τ) => ‖cf q‖) {T₀ : ℝ} (hT₀ : 1 ≤ T₀) : (Summable fun (q : τ) => if T₀ < size q then ‖cf q‖ * size q else 0) ∧ (∑' (q : τ), if T₀ < size q then ‖cf q‖ * size q else 0) ≤ 4 * Es / T₀ ^ 99

Layer-cake form of the separation shell bound: the size-weighted coefficient mass beyond T₀ is at most 4 E / T₀^{99} (blueprint lem:predictors, line 1546).

theorem TrilinearHT.Auto.log_weight_le {a₀ s : ℝ} (ha₀ : 1 ≤ a₀) (hs : 1 ≤ s) (C : ℕ) : (a₀ + 6 * Real.log s) ^ C ≤ a₀ ^ C * (1 + 6 * ↑C) ^ C * s

Polynomials in log s are dominated by s: (a₀ + 6 log s)^C ≤ a₀^C (1 + 6C)^C s.

theorem TrilinearHT.Auto.norm_tsum_compl_le {π : Type u_1} [DecidableEq π] (P : Finset π) (f : π → ℂ) (hf : Summable fun (p : π) => ‖f p‖) : ‖∑' (p : ↑(↑P)ᶜ), f ↑p‖ ≤ ∑' (p : π), if p ∈ P then 0 else ‖f p‖

The norm of a tail sum over the complement of a finite set.

theorem TrilinearHT.Auto.predictor_cell_bound {τ : Type u_1} {π : Type u_2} [DecidableEq τ] [DecidableEq π] (cf : τ → ℂ) (hcs : Summable fun (q : τ) => ‖cf q‖) (sepQ : τ → ℂ) {M : ℝ} (hsepQ : ∀ (q : τ), ‖sepQ q‖ ≤ M) {LF : ℂ} (hLF : HasSum (fun (q : τ) => cf q * sepQ q) LF) (R : Finset τ) (ret : τ → Prop) [DecidablePred ret] (P : Finset π) (coeff sepP : τ → π → ℂ) (hcoeff : ∀ (q : τ), Summable fun (p : π) => ‖coeff q p‖) {M' : ℝ} (hsepP : ∀ (q : τ) (p : π), ‖sepP q p‖ ≤ M') (hexp : ∀ q ∈ R, ret q → HasSum (fun (p : π) => coeff q p * sepP q p) (sepQ q / 4)) : ‖LF - ∑ q ∈ R, if ret q then 4 * cf q * ∑ p ∈ P, coeff q p * sepP q p else 0‖ ≤ ((∑' (q : τ), if q ∈ R then 0 else ‖cf q‖ * ‖sepQ q‖) + ∑ q ∈ R, if ret q then 0 else ‖cf q‖ * ‖sepQ q‖) + ∑ q ∈ R, if ret q then 4 * ‖cf q‖ * ∑' (p : π), if p ∈ P then 0 else ‖coeff q p‖ * ‖sepP q p‖ else 0

Blueprint lem:predictors, proof lines 1544-1547, at one cell: the replacement of the atom-pair form by the retained catalog terms leaves the discarded shells, the discarded bands and the catalog tails.

theorem TrilinearHT.Auto.predictor_grouping {τ : Type u_1} {π : Type u_2} {μ : Type u_3} {ν : Type u_4} [DecidableEq μ] [DecidableEq ν] (R : Finset τ) (Mset : Finset μ) (σset : Finset ν) (P : Finset π) (ret : τ → Prop) [DecidablePred ret] (Mq : τ → μ) (σq : τ → π → ν) (cf : τ → ℂ) (coeff : τ → π → ℂ) (X : τ → μ → ν → ℂ) (sepP : τ → π → ℂ) (hM : ∀ q ∈ R, ret q → Mq q ∈ Mset) (hσ : ∀ q ∈ R, ret q → ∀ p ∈ P, σq q p ∈ σset) (hX : ∀ q ∈ R, ret q → ∀ p ∈ P, X q (Mq q) (σq q p) = sepP q p) : ∑ ℓ ∈ R ×ˢ Mset ×ˢ σset, (if ret ℓ.1 ∧ Mq ℓ.1 = ℓ.2.1 then 4 * cf ℓ.1 * ∑ p ∈ P with σq ℓ.1 p = ℓ.2.2, coeff ℓ.1 p else 0) * X ℓ.1 ℓ.2.1 ℓ.2.2 = ∑ q ∈ R, if ret q then 4 * cf q * ∑ p ∈ P, coeff q p * sepP q p else 0

Regrouping the retained catalog terms of all retained separation terms into the finite predictor list (q, M, σ) with scale-dependent coefficients.

theorem TrilinearHT.Auto.eLpNorm_normalized_ne_top {a r : ℝ} {g : ℝ → ℂ} (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (Set.Ico a (a + r)))) : MeasureTheory.eLpNorm g 2 (normalizedIntervalMeasure a r) ≠ ⊤

theorem TrilinearHT.Auto.eLpNorm_normalized_le_toReal {a r : ℝ} {g : ℝ → ℂ} (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (Set.Ico a (a + r)))) : MeasureTheory.eLpNorm g 2 (normalizedIntervalMeasure a r) ≤ ENNReal.ofReal (MeasureTheory.eLpNorm g 2 (normalizedIntervalMeasure a r)).toReal

Explicit parameters of the predictor list (blueprint lem:predictors, lines 1495-1503 and proof lines 1544-1547).

noncomputable def TrilinearHT.Auto.pdX (H : ℝ) : ℝ

Logarithmic height parameter for the predictor catalog.

Equations

• TrilinearHT.Auto.pdX H = 1 + Real.log H

noncomputable def TrilinearHT.Auto.pdEs (Ds : ℕ) (H : ℝ) : ℝ

Initial exponential chart budget for the predictor construction.

Equations

• TrilinearHT.Auto.pdEs Ds H = Real.exp (↑Ds * TrilinearHT.Auto.pdX H ^ Ds)

noncomputable def TrilinearHT.Auto.pdA0 (Ds : ℕ) (H : ℝ) : ℝ

Polynomial base controlling the predictor tail estimates.

Equations

• TrilinearHT.Auto.pdA0 Ds H = 2 + 6 * (↑Ds * TrilinearHT.Auto.pdX H ^ Ds)

noncomputable def TrilinearHT.Auto.pdT0 (Ds Cr : ℕ) (H B : ℝ) : ℝ

Initial predictor scale determined by chart complexity and accuracy.

Equations

• TrilinearHT.Auto.pdT0 Ds Cr H B = 12 * ↑Cr * TrilinearHT.Auto.pdA0 Ds H ^ Cr * (1 + 6 * ↑Cr) ^ Cr * TrilinearHT.Auto.pdEs Ds H * Real.exp B + 1

noncomputable def TrilinearHT.Auto.pdH0 (Ds Cr : ℕ) (H B : ℝ) : ℝ

Height budget used to construct the predictor catalog.

Equations

• TrilinearHT.Auto.pdH0 Ds Cr H B = max ((TrilinearHT.Auto.pdEs Ds H * TrilinearHT.Auto.pdT0 Ds Cr H B) ^ 6) (TrilinearHT.Auto.bandLip + 1)

noncomputable def TrilinearHT.Auto.pdM0 (Ds Cr : ℕ) (H B : ℝ) : ℕ

Integer accuracy level used in the predictor tail cutoff.

Equations

• TrilinearHT.Auto.pdM0 Ds Cr H B = ⌈2 * (B + Real.log (3 * TrilinearHT.Auto.pdEs Ds H * ↑Cr * (2 + Real.log (TrilinearHT.Auto.pdH0 Ds Cr H B)) ^ Cr + 1))⌉₊

noncomputable def TrilinearHT.Auto.pdLE (Ds Cr : ℕ) (H B : ℝ) : ℝ

Combined logarithmic height and accuracy parameter for the predictor catalog.

Equations

• TrilinearHT.Auto.pdLE Ds Cr H B = 2 + Real.log (TrilinearHT.Auto.pdH0 Ds Cr H B) + ↑(TrilinearHT.Auto.pdM0 Ds Cr H B)

noncomputable def TrilinearHT.Auto.pdE (Dc Ds Cr : ℕ) (H B : ℝ) : ℝ

Exponential predictor coefficient budget.

Equations

• TrilinearHT.Auto.pdE Dc Ds Cr H B = Real.exp (↑Dc * TrilinearHT.Auto.pdLE Ds Cr H B ^ Dc)

noncomputable def TrilinearHT.Auto.pdE1 (J1 Ds Cr : ℕ) (H B : ℝ) : ℝ

Exponential higher-order coefficient-tail budget for the predictor catalog.

Equations

• TrilinearHT.Auto.pdE1 J1 Ds Cr H B = Real.exp (↑J1 * TrilinearHT.Auto.pdLE Ds Cr H B ^ J1)

noncomputable def TrilinearHT.Auto.pdK0 (κ : LocalKernelClass) (d' Dc J1 Ds Cr : ℕ) (H B : ℝ) : ℕ

Dyadic truncation depth sufficient for the predictor coefficient tail.

Equations

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

theorem TrilinearHT.Auto.pdX_nonneg {H : ℝ} (hH : 1 ≤ H) : 0 ≤ pdX H

theorem TrilinearHT.Auto.one_le_pdEs {Ds : ℕ} {H : ℝ} (hH : 1 ≤ H) : 1 ≤ pdEs Ds H

theorem TrilinearHT.Auto.one_le_pdA0 {Ds : ℕ} {H : ℝ} (hH : 1 ≤ H) : 1 ≤ pdA0 Ds H

theorem TrilinearHT.Auto.one_le_pdT0 {Ds Cr : ℕ} {H B : ℝ} (hH : 1 ≤ H) : 1 ≤ pdT0 Ds Cr H B

theorem TrilinearHT.Auto.one_le_pdH0 {Ds Cr : ℕ} {H B : ℝ} : 1 ≤ pdH0 Ds Cr H B

theorem TrilinearHT.Auto.pd_shell_budget {Ds Cr : ℕ} {H B : ℝ} (hH : 1 ≤ H) : ↑Cr * pdA0 Ds H ^ Cr * (1 + 6 * ↑Cr) ^ Cr * (4 * pdEs Ds H / pdT0 Ds Cr H B ^ 99) ≤ Real.exp (-B) / 3

The shell budget: the size-weighted tail beyond T₀ costs at most e^{-B}/3.

theorem TrilinearHT.Auto.pd_band_budget {Ds Cr : ℕ} {H B : ℝ} (hH : 1 ≤ H) : pdEs Ds H * (Real.exp (-↑(pdM0 Ds Cr H B) / 2) * (↑Cr * (2 + Real.log (pdH0 Ds Cr H B)) ^ Cr)) ≤ Real.exp (-B) / 3

The band budget: discarding the bands m > M₀ costs at most e^{-B}/3.

theorem TrilinearHT.Auto.one_le_pdE (Dc Ds Cr : ℕ) (H B : ℝ) : 1 ≤ pdE Dc Ds Cr H B

theorem TrilinearHT.Auto.pd_catalog_budget (κ : LocalKernelClass) (d' Dc J1 Ds Cr : ℕ) {H B : ℝ} (hH : 1 ≤ H) : 4 * pdEs Ds H * (↑⌊pdE Dc Ds Cr H B⌋₊ * (pdE1 J1 Ds Cr H B * tailCT κ d' (pdE Dc Ds Cr H B) * (2 * 7 ^ (d' + d') * (2 * Real.pi) ^ ((d' + 1) ^ 2 - 1) / 2 ^ pdK0 κ d' Dc J1 Ds Cr H B))) ≤ Real.exp (-B) / 3

The catalog budget: the pooled catalog tails cost at most e^{-B}/3.

theorem TrilinearHT.Auto.predictor_sum_bound {τ : Type u_1} {π : Type u_2} [DecidableEq τ] [DecidableEq π] (S : Finset (ℤ × ℤ)) (len : ℤ × ℤ → ℝ) (hlen : ∀ (I : ℤ × ℤ), 0 ≤ len I) (cf : τ → ℂ) (hcs : Summable fun (q : τ) => ‖cf q‖) (LF : ℤ × ℤ → ℂ) (sepQ : ℤ × ℤ → τ → ℂ) (MQ : ℤ × ℤ → ℝ) (hsepQ : ∀ I ∈ S, ∀ (q : τ), ‖sepQ I q‖ ≤ MQ I) (hLF : ∀ I ∈ S, HasSum (fun (q : τ) => cf q * sepQ I q) (LF I)) (R : Finset τ) (ret : τ → ℤ × ℤ → Prop) [(q : τ) → (I : ℤ × ℤ) → Decidable (ret q I)] (P : Finset π) (coeff sepP : ℤ × ℤ → τ → π → ℂ) (hcoeff : ∀ (I : ℤ × ℤ) (q : τ), Summable fun (p : π) => ‖coeff I q p‖) (MP : ℤ × ℤ → ℝ) (hsepP : ∀ I ∈ S, ∀ (q : τ) (p : π), ‖sepP I q p‖ ≤ MP I) (hexp : ∀ I ∈ S, ∀ q ∈ R, ret q I → HasSum (fun (p : π) => coeff I q p * sepP I q p) (sepQ I q / 4)) : ∑ I ∈ S, len I * ‖LF I - ∑ q ∈ R, if ret q I then 4 * cf q * ∑ p ∈ P, coeff I q p * sepP I q p else 0‖ ≤ (∑' (q : τ), if q ∈ R then 0 else ‖cf q‖ * ∑ I ∈ S, len I * ‖sepQ I q‖) + ∑ q ∈ R, ‖cf q‖ * ∑ I ∈ S with ¬ret q I, len I * ‖sepQ I q‖ + ∑ q ∈ R, 4 * ‖cf q‖ * ∑ I ∈ S with ret q I, len I * ∑' (p : π), if p ∈ P then 0 else ‖coeff I q p‖ * ‖sepP I q p‖

The cell-summed form of predictor_cell_bound.

theorem TrilinearHT.Auto.separatedLocalForm_smul_right (r : ℝ) (w : ℝ × ℝ → ℂ) (Q : ℝ → ℂ) (a b : Fin 4) (Fa Fb : ℝ → ℂ) (c : ℂ) : (separatedLocalForm r w Q a b Fa fun (y : ℝ) => c * Fb y) = c * separatedLocalForm r w Q a b Fa Fb

theorem TrilinearHT.Auto.pair_expansion_cell {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {a i k b : Fin 4} (hai : a ≠ i) (hak : a ≠ k) (hab : a ≠ b) (hik : i ≠ k) (hib : i ≠ b) (hkb : k ≠ b) {R v φ φ' : ℝ → ℂ} (hRm : Measurable R) (hvm : Measurable v) (hR2 : MeasureTheory.MemLp R 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) (hv2 : MeasureTheory.MemLp v 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) {τ : Type u_1} [Countable τ] (cf : τ → ℂ) (ψa ψb Q : τ → ℝ → ℂ) (hψam : ∀ (q : τ), Measurable (ψa q)) (hψbm : ∀ (q : τ), Measurable (ψb q)) (hQm : ∀ (q : τ), Measurable (Q q)) (hψab : ∀ (q : τ) (y : ℝ), ‖ψa q y‖ ≤ 1) (hψbb : ∀ (q : τ) (y : ℝ), ‖ψb q y‖ ≤ 1) (hQb : ∀ (q : τ) (y : ℝ), ‖Q q y‖ ≤ 1) (hcs : Summable fun (q : τ) => ‖cf q‖) (hexp : ∀ (x t : ℝ), HasSum (fun (q : τ) => cf q * ψa q (x + ↑↑a * t) * ψb q (x + ↑↑b * t) * Q q t) (φ (x + ↑↑i * t) * φ' (x + ↑↑k * t))) (f : Fin 4 → ℝ → ℂ) (hfa : f a = R) (hfi : f i = φ) (hfk : f k = φ') (hfb : f b = v) : ∃ (M : ℝ), HasSum (fun (q : τ) => cf q * separatedLocalForm r w (Q q) a b (fun (y : ℝ) => ψa q y * R y) fun (y : ℝ) => ψb q y * v y) (localProgressionForm r w f) ∧ ∀ (q : τ), ‖separatedLocalForm r w (Q q) a b (fun (y : ℝ) => ψa q y * R y) fun (y : ℝ) => ψb q y * v y‖ ≤ M

The atom-pair expansion of the local form at one cell, for arbitrary cell-local L² inputs in the remaining slots, with a uniform bound of the separated forms.

theorem TrilinearHT.Auto.separatedLocalForm_bounded_le {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {a b : Fin 4} (hab : a ≠ b) {K : ℝ → ℂ} (hK : ∀ (t : ℝ), ‖K t‖ ≤ 1) {ψa ψb za zb : ℝ → ℂ} (hψam : Measurable ψa) (hψbm : Measurable ψb) (hψa : ∀ (y : ℝ), ‖ψa y‖ ≤ 1) (hψb : ∀ (y : ℝ), ‖ψb y‖ ≤ 1) (hzam : Measurable za) (hzbm : Measurable zb) (hza : MeasureTheory.MemLp za 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) (hzb : MeasureTheory.MemLp zb 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) : ‖separatedLocalForm r w K a b (fun (y : ℝ) => ψa y * za y) fun (y : ℝ) => ψb y * zb y‖ ≤ localKernelSupBound κ * √(r⁻¹ * ∫ (y : ℝ) in Set.Ico a₀ (a₀ + r), ‖za y‖ ^ 2) * √(r⁻¹ * ∫ (y : ℝ) in Set.Ico a₀ (a₀ + r), ‖zb y‖ ^ 2)

A uniform bound of separated forms with bounded time factor and bounded multipliers.

theorem TrilinearHT.Auto.pd_shell_log (Ds : ℕ) {H s : ℝ} (hs : 1 ≤ s) : 2 + Real.log ((pdEs Ds H * s) ^ 6) = pdA0 Ds H + 6 * Real.log s

noncomputable def TrilinearHT.Auto.pdCard (κ : LocalKernelClass) (d' Dc J1 Ds Cr : ℕ) (H B : ℝ) : ℝ

The size bound of the predictor list.

Equations

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