Trilinear Hilbert transform: separated_moment_extraction

theorem TrilinearHT.Auto.separated_moment_extraction (κ : LocalKernelClass) (c₁ : ℕ) (hc₁ : 1 ≤ c₁) : ∃ (Dk : ℕ) (Lζ : ℝ), 1 ≤ Dk ∧ 1 ≤ Lζ ∧ ∀ {d : ℕ} {a₀ r H₁ C₁ δ₃ Λ : ℝ} (A : QuadraticChartData d), QuadraticChartComplexity c₁ H₁ A → IsBoundedQuadraticChart A → 0 < r → ∀ {w : ℝ × ℝ → ℂ}, IsAdmissibleLocalKernel κ a₀ r w → ∀ {a b : Fin 4}, a ≠ b → ∀ {R v ψa ψb : ℝ → ℂ}, Measurable R → Measurable v → Measurable ψa → Measurable ψb → (∀ (y : ℝ), ‖ψa y‖ ≤ 1) → (∀ (y : ℝ), ‖ψb y‖ ≤ 1) → 1 ≤ C₁ → MeasureTheory.eLpNorm R 2 (normalizedIntervalMeasure a₀ r) ≤ ENNReal.ofReal C₁ → MeasureTheory.eLpNorm v 2 (normalizedIntervalMeasure a₀ r) ≤ 1 → 0 < δ₃ → δ₃ < ‖separatedLocalForm r w (quadraticChartAtom A) a b (fun (y : ℝ) => R y * ψa y) fun (y : ℝ) => v y * ψb y‖ → 1 ≤ Λ → H₁ ≤ Λ → Lζ ≤ Λ → (kernelFourierConst κ + 1) * C₁ / δ₃ ≤ Λ → 2 * C₁ / δ₃ ≤ Λ → ∃ (α : ℝ), δ₃ / (2 * Real.exp (↑Dk * (1 + 3 * Real.log Λ) ^ Dk)) ≤ r⁻¹ * ‖∫ (y : ℝ) in Set.Icc a₀ (a₀ + r), R y * ψa y * ↑(Real.fourierChar (α * y))‖

Blueprint lem:detection, line 1473: a large separated form forces A_r to be large, its kernel is separated by lem:separation, and one normalized moment of R against ψ_a e(α ·) is large.

theorem TrilinearHT.Auto.moment_witness_chart {d c₁ : ℕ} {H₁ : ℝ} (A : QuadraticChartData d) (hA : QuadraticChartComplexity c₁ H₁ A) (hAb : IsBoundedQuadraticChart A) (hc₁ : 1 ≤ c₁) (α : ℝ) : ∃ (Φ : QuadraticChartData (d + 0)), QuadraticChartComplexity c₁ (H₁ ^ 6) Φ ∧ IsBoundedQuadraticChart Φ ∧ ∀ (y : ℝ), (starRingEnd ℂ) (quadraticChartAtom Φ y) = quadraticChartAtom A y * ↑(Real.fourierChar (α * y))

The witness chart conj(ψ_a e(α ·)) of a moment ∫ R ψ_a e(α ·).

theorem TrilinearHT.Auto.intervalIntegral_eq_Icc {a₀ r : ℝ} (hr : 0 < r) (F : ℝ → ℂ) : ∫ (x : ℝ) in a₀..a₀ + r, F x = ∫ (x : ℝ) in Set.Icc a₀ (a₀ + r), F x

theorem TrilinearHT.Auto.qple_max {Y a b : ℝ} {K : ℕ} (ha : QPLe Y K a) (hb : QPLe Y K b) : QPLe Y K (max a b)

theorem TrilinearHT.Auto.qple_of_exp_Y {Y a : ℝ} (ha : 0 < a) (h : Real.log a ≤ Y) : QPLe Y 1 a

theorem TrilinearHT.Auto.fin_cast_int_real (a : Fin 4) : ↑↑↑a = ↑↑a

theorem TrilinearHT.Auto.abs_fin_int_le (a : Fin 4) : |↑↑a| ≤ 3

theorem TrilinearHT.Auto.exp_three_log_le {Λ : ℝ} (hΛ : 1 ≤ Λ) (Dk : ℕ) : Real.exp (↑Dk * (1 + 3 * Real.log Λ) ^ Dk) ≤ Real.exp (↑(Dk * 3 ^ Dk) * (1 + Real.log Λ) ^ (Dk * 3 ^ Dk))

theorem TrilinearHT.Auto.detection_atom_pair (κ : LocalKernelClass) (c₀ : ℕ) (hc₀ : 1 ≤ c₀) : ∃ (c₂ : ℕ) (K : ℕ), 1 ≤ c₂ ∧ 1 ≤ K ∧ ∀ {a₀ r H C₁ δ₀ : ℝ} {d e : ℕ} (A : QuadraticChartData d) (A' : QuadraticChartData e), QuadraticChartComplexity c₀ H A → QuadraticChartComplexity c₀ H A' → IsBoundedQuadraticChart A → IsBoundedQuadraticChart A' → 0 < r → ∀ {w : ℝ × ℝ → ℂ}, IsAdmissibleLocalKernel κ a₀ r w → ∀ (f : Fin 4 → ℝ → ℂ), (∀ (j : Fin 4), Measurable (f j)) → ∀ {jR i k lv : Fin 4}, jR ≠ i → jR ≠ k → jR ≠ lv → i ≠ k → i ≠ lv → k ≠ lv → f i = quadraticChartAtom A → f k = quadraticChartAtom A' → 1 ≤ C₁ → MeasureTheory.eLpNorm (f jR) 2 (normalizedIntervalMeasure a₀ r) ≤ ENNReal.ofReal C₁ → MeasureTheory.eLpNorm (f lv) 2 (normalizedIntervalMeasure a₀ r) ≤ 1 → 0 < δ₀ → δ₀ ≤ 1 → δ₀ < ‖localProgressionForm r w f‖ → ∃ (d'' : ℕ) (Φ : QuadraticChartData d''), QuadraticChartComplexity c₂ (Real.exp (↑K * (1 + Real.log H + Real.log C₁ + Real.log (1 / δ₀)) ^ K)) Φ ∧ IsBoundedQuadraticChart Φ ∧ (Real.exp (↑K * (1 + Real.log H + Real.log C₁ + Real.log (1 / δ₀)) ^ K))⁻¹ ≤ r⁻¹ * ‖∫ (x : ℝ) in a₀..a₀ + r, f jR x * (starRingEnd ℂ) (quadraticChartAtom Φ x)‖

Blueprint lem:detection, line 1473: an atom pair with a large local form against R, v yields a large normalized moment of R against a bounded atom, with complexity and moment quasipolynomial in H, C₁, δ₀⁻¹.

theorem TrilinearHT.Auto.qple_of_quasipolynomial {D : ℝ → ℝ} (hD : QuasipolynomialBound D) : ∃ (kD : ℕ), ∀ {Y t : ℝ} {K : ℕ}, 1 ≤ Y → 2 ≤ t → QPLe Y K t → QPLe Y (kD * (1 + K) ^ kD + K * kD) (D t) ∧ 0 ≤ D t

theorem TrilinearHT.Auto.truncateNorm_eLpNorm_le {μ : MeasureTheory.Measure ℝ} {p : ENNReal} {g : ℝ → ℂ} (hg : Measurable g) (B : ℝ) : MeasureTheory.eLpNorm (truncateNorm B g) p μ ≤ MeasureTheory.eLpNorm g p μ

theorem TrilinearHT.Auto.clipExcept_apply_self (B : ℝ) (k : Fin 4) (f : Fin 4 → ℝ → ℂ) : clipExcept B k f k = f k

theorem TrilinearHT.Auto.clipExcept_apply_ne (B : ℝ) {k j : Fin 4} (h : j ≠ k) (f : Fin 4 → ℝ → ℂ) : clipExcept B k f j = truncateNorm B (f j)

theorem TrilinearHT.Auto.qple_of_le_nat {Y c : ℝ} {k : ℕ} (hY : 1 ≤ Y) (hc : c ≤ ↑k) : QPLe Y k c

theorem TrilinearHT.Auto.detection_budget {D : ℝ → ℝ} {kD K₃ : ℕ} (hkD : ∀ {Y t : ℝ} {K : ℕ}, 1 ≤ Y → 2 ≤ t → QPLe Y K t → QPLe Y (kD * (1 + K) ^ kD + K * kD) (D t) ∧ 0 ≤ D t) {Cv W' q C₁ δ X B dinv1 t₁ M₁ dinv2 t₂ M₂ dinv3 Hc δ₀ cB : ℝ} {kδ1 kc kτ1 kD1 kδ2 kτ2 kD2 kδ3 kδ0 kH kP kE : ℕ} (hkδ1 : kδ1 = 2 + 1) (hkc : kc = ⌈4 * (Cv + 1)⌉₊) (hkτ1 : kτ1 = 4 + (kc + 1 + (3 * 1 + 1) + kδ1)) (hkD1 : kD1 = kD * (1 + kτ1) ^ kD + kτ1 * kD) (hkδ2 : kδ2 = 2 + 1 + kD1 + kδ1) (hkτ2 : kτ2 = 4 + (kc + 1 + (3 * 1 + 1) + kδ2)) (hkD2 : kD2 = kD * (1 + kτ2) ^ kD + kτ2 * kD) (hkδ3 : kδ3 = 2 + 1 + kD2 + kδ2) (hkδ0 : kδ0 = 2 + kδ3) (hkH : kH = kD1 + kD2) (hkP : kP = kH + 1 + kδ0) (hkE : kE = K₃ * (1 + kP) ^ K₃ + kP * K₃) (hW'0 : 0 ≤ W') (hq : 2 < q) (hC₁ : 1 ≤ C₁) (hδ : 0 < δ) (hδ2 : δ < 1 / 2) (hX : X = 12 * (W' + 1) * C₁ * (1 / δ)) (hX1 : 1 ≤ X) (hB : B = max 2 (X ^ (q / (q - 2)))) (hdinv1 : dinv1 = 4 / 3 * (1 / δ)) (ht₁ : t₁ = max 4 (4 * (Cv + 1) * C₁ * B ^ 3 * dinv1)) (hM₁ : M₁ = max 1 (D t₁)) (hdinv2 : dinv2 = 2 * B * M₁ * dinv1) (ht₂ : t₂ = max 4 (4 * (Cv + 1) * C₁ * B ^ 3 * dinv2)) (hM₂ : M₂ = max 1 (D t₂)) (hdinv3 : dinv3 = 2 * B * M₂ * dinv2) (hHc : Hc = max (D t₁) (D t₂)) (hHc1 : 1 ≤ Hc) (hδ₀ : δ₀ = (max 2 dinv3)⁻¹) (hcB : cB = Real.log 2 + q / (q - 2) * (1 + Real.log (12 * (W' + 1)))) : Real.exp (↑K₃ * (1 + Real.log Hc + Real.log C₁ + Real.log (1 / δ₀)) ^ K₃) ≤ Real.exp (↑kE * (1 + cB) ^ kE * (1 + Real.log C₁ + Real.log (1 / δ)) ^ kE)

The quasipolynomial budget of blueprint lem:detection, line 1473: the final complexity is quasipolynomial in B, C₁, δ⁻¹, and the clipping height contributes only a q-dependent factor to the logarithm.

theorem TrilinearHT.Auto.detectResidual (κ : LocalKernelClass) : ∃ (c₂ : ℕ) (C : ℕ), 1 ≤ c₂ ∧ 1 ≤ C ∧ ∀ (q : ℝ), 2 < q → ∃ (Cq : ℝ), 0 < Cq ∧ ∀ {a₀ r C₁ δ : ℝ}, 0 < r → ∀ {w : ℝ × ℝ → ℂ}, IsAdmissibleLocalKernel κ a₀ r w → ∀ (f : Fin 4 → ℝ → ℂ), (∀ (j : Fin 4), Measurable (f j)) → ∀ {jR ih ku lv : Fin 4}, jR ≠ ih → jR ≠ ku → jR ≠ lv → ih ≠ ku → ih ≠ lv → ku ≠ lv → 1 ≤ C₁ → 0 < δ → δ < 1 / 2 → MeasureTheory.eLpNorm (f jR) 2 (normalizedIntervalMeasure a₀ r) ≤ ENNReal.ofReal C₁ → MeasureTheory.eLpNorm (f ih) (ENNReal.ofReal q) (normalizedIntervalMeasure a₀ r) ≤ 1 → MeasureTheory.eLpNorm (f ku) 2 (normalizedIntervalMeasure a₀ r) ≤ 1 → MeasureTheory.eLpNorm (f lv) 2 (normalizedIntervalMeasure a₀ r) ≤ 1 → δ < ‖localProgressionForm r w f‖ → ∃ (d : ℕ) (Φ : QuadraticChartData d), QuadraticChartComplexity c₂ (Real.exp (Cq * (1 + Real.log C₁ + Real.log (1 / δ)) ^ C)) Φ ∧ IsBoundedQuadraticChart Φ ∧ (Real.exp (Cq * (1 + Real.log C₁ + Real.log (1 / δ)) ^ C))⁻¹ ≤ r⁻¹ * ‖∫ (x : ℝ) in a₀..a₀ + r, f jR x * (starRingEnd ℂ) (quadraticChartAtom Φ x)‖

Blueprint lem:detection (Declaration detection, line 1475, THT.LocalForm.detectResidual): if ‖R‖_{2,I} ≤ C₁, ‖h‖_{q,I} ≤ 1, ‖u‖_{2,I}, ‖v‖_{2,I} ≤ 1 and |H_I(R,h,u,v)| > δ (any four distinct slots), then R has a normalized moment of magnitude at least D⁻¹ against a bounded atom of complexity D, where D = exp(C_q (1 + log C₁ + log δ⁻¹)^C) with an absolute degree C.