Trilinear Hilbert transform: delay_rows_sum

theorem TrilinearHT.Auto.delay_rows_sum (G : RealDyadicGrid) (J : ℤ × ℤ) (S : Finset (ℤ × ℤ)) (hSJ : ∀ I ∈ S, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G J.1 J.2) (θ : ℤ × ℤ → ℝ → ℂ) {L : ℝ} (hL : 0 ≤ L) (hθc : ∀ I ∈ S, Continuous (θ I)) (hθb : ∀ I ∈ S, ∀ (y : ℝ), ‖θ I y‖ ≤ L) (hLip : ∀ I ∈ S, ∀ (y z : ℝ), ‖θ I y - θ I z‖ ≤ L / dyadicGridLength G I.1 * |y - z|) (Dg μg : ℤ → ℝ → ℂ) (e : ℤ → ℝ → ℝ) {ε E : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (N : ℤ) (K₀ : ℕ) (hN : ∀ I ∈ S, I.1 + ↑K₀ ≤ N) (hD2 : ∀ I ∈ S, ∀ (h : ℤ), MeasureTheory.MemLp (Dg h) 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) (hμ2 : ∀ I ∈ S, ∀ (h : ℤ), MeasureTheory.MemLp (μg h) 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) (hμc : ∀ I ∈ S, ∀ (j : ℕ), I.1 + ↑j ≤ N → ∀ Q ∈ dyadicGeneration G I j, ∀ y ∈ dyadicGridCell G Q.1 Q.2, ∀ z ∈ dyadicGridCell G Q.1 Q.2, μg (I.1 + ↑j) y = μg (I.1 + ↑j) z) (hDμ : ∀ I ∈ S, ∀ (j : ℕ), I.1 + ↑j ≤ N → ∀ Q ∈ dyadicGeneration G I j, ∫ (y : ℝ) in dyadicGridCell G Q.1 Q.2, Dg (I.1 + ↑j) y = ∫ (y : ℝ) in dyadicGridCell G Q.1 Q.2, μg (I.1 + ↑j) y) (he0 : ∀ (h : ℤ) (y : ℝ), 0 ≤ e h y) (hei : ∀ (h : ℤ), MeasureTheory.IntegrableOn (e h) (dyadicGridCell G J.1 J.2) MeasureTheory.volume) (heD : ∀ I ∈ S, ∀ (h : ℤ), I.1 ≤ h → h < N → ∀ᵐ (y : ℝ) ∂MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2), ‖Dg h y - Dg (h + 1) y‖ ^ 2 ≤ e h y) (heμ : ∀ I ∈ S, ∀ (h : ℤ), I.1 ≤ h → h < N → ∀ᵐ (y : ℝ) ∂MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2), ‖μg (h + 1) y - μg h y‖ ^ 2 ≤ ε * e h y) (hE : ∀ (Hs : Finset ℤ), ∑ h ∈ Hs, ∫ (y : ℝ) in dyadicGridCell G J.1 J.2, e h y ≤ E) (m : ℝ → ℝ) (hm0 : ∀ (y : ℝ), 0 ≤ m y) (hmi : MeasureTheory.IntegrableOn m (dyadicGridCell G J.1 J.2) MeasureTheory.volume) (hmE : ∫ (y : ℝ) in dyadicGridCell G J.1 J.2, m y ≤ E) (hDN : ∀ I ∈ S, ∫ (y : ℝ) in dyadicGridCell G I.1 I.2, ‖Dg N y‖ ^ 2 ≤ 4 * ∫ (y : ℝ) in dyadicGridCell G I.1 I.2, m y) : ∑ I ∈ S, (dyadicGridLength G I.1)⁻¹ * ‖∫ (y : ℝ) in dyadicGridCell G I.1 I.2, Dg (I.1 + ↑K₀) y * θ I y‖ ^ 2 ≤ 3 * ∑ I ∈ S, (dyadicGridLength G I.1)⁻¹ * ‖∫ (y : ℝ) in dyadicGridCell G I.1 I.2, μg (I.1 + ↑K₀) y * θ I y‖ ^ 2 + 3 * (9 * L * 2⁻¹ ^ K₀) ^ 2 * E

Blueprint lem:delay, proof lines 1558–1559: the delayed rows |I|^{-1/2} ∫_I D_{s+K₀} θ_I of all use cells, against arbitrary bumps, are controlled by the predictor start terms and the geometrically decaying telescoping rows, C 2^{-K₀} ‖F_a‖₂ (orthogonal increments summed over disjoint cells of each depth). The telescoping is stopped at the depth N ≥ s + K₀ of the projection family; the terminal remainder costs C 2^{s - N} ‖1_I F_a‖.

theorem TrilinearHT.Auto.delay_start_meanZero (G : RealDyadicGrid) (J : ℤ × ℤ) (S : Finset (ℤ × ℤ)) (hSJ : ∀ I ∈ S, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G J.1 J.2) (θ : ℤ × ℤ → ℝ → ℂ) {L : ℝ} (hL : 0 ≤ L) (hθc : ∀ I ∈ S, Continuous (θ I)) (hθb : ∀ I ∈ S, ∀ (y : ℝ), ‖θ I y‖ ≤ L) (hθ0 : ∀ I ∈ S, ∫ (y : ℝ) in dyadicGridCell G I.1 I.2, θ I y = 0) (μg : ℤ → ℝ → ℂ) (e : ℤ → ℝ → ℝ) {ε E : ℝ} (hε0 : 0 ≤ ε) (hμ2 : ∀ I ∈ S, ∀ (h : ℤ), MeasureTheory.MemLp (μg h) 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) (hμI : ∀ I ∈ S, ∀ y ∈ dyadicGridCell G I.1 I.2, ∀ z ∈ dyadicGridCell G I.1 I.2, μg I.1 y = μg I.1 z) (he0 : ∀ (h : ℤ) (y : ℝ), 0 ≤ e h y) (hei : ∀ (h : ℤ), MeasureTheory.IntegrableOn (e h) (dyadicGridCell G J.1 J.2) MeasureTheory.volume) (N : ℤ) (K₀ : ℕ) (hN : ∀ I ∈ S, I.1 + ↑K₀ ≤ N) (heμ : ∀ I ∈ S, ∀ (h : ℤ), I.1 ≤ h → h < N → ∀ᵐ (y : ℝ) ∂MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2), ‖μg (h + 1) y - μg h y‖ ^ 2 ≤ ε * e h y) (hE : ∀ (Hs : Finset ℤ), ∑ h ∈ Hs, ∫ (y : ℝ) in dyadicGridCell G J.1 J.2, e h y ≤ E) : ∑ I ∈ S, (dyadicGridLength G I.1)⁻¹ * ‖∫ (y : ℝ) in dyadicGridCell G I.1 I.2, μg (I.1 + ↑K₀) y * θ I y‖ ^ 2 ≤ (L * ↑K₀) ^ 2 * ε * E

Blueprint lem:delay, proof line 1559: for mean-zero bumps the start term is ∫_I (μ_H - μ_s) ω_I, a sum of K₀ private increments, costing K₀ √ε ‖F_a‖₂.

theorem TrilinearHT.Auto.delay_start_depth (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (θ : ℤ × ℤ → ℝ → ℂ) {L : ℝ} (hL : 0 ≤ L) (hθb : ∀ I ∈ S, ∀ (y : ℝ), ‖θ I y‖ ≤ L) (μ : ℝ → ℂ) (hμ2 : ∀ I ∈ S, MeasureTheory.MemLp μ 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) : ∑ I ∈ S, (dyadicGridLength G I.1)⁻¹ * ‖∫ (y : ℝ) in dyadicGridCell G I.1 I.2, μ y * θ I y‖ ^ 2 ≤ L ^ 2 * ∑ I ∈ S, ∫ (y : ℝ) in dyadicGridCell G I.1 I.2, ‖μ y‖ ^ 2

The start term for general bumps: Σ_I |I|⁻¹ |∫_I μ_H θ_I|² ≤ L² Σ_I ‖1_I μ_H‖².

theorem TrilinearHT.Auto.norm_deriv_le_of_support {f : ℝ → ℂ} {a₀ r B : ℝ} (hr : 0 < r) (hf : ContDiff ℝ 2 f) (hsupp : ∀ y ∉ Set.Ico a₀ (a₀ + r), f y = 0) (hB : ∀ (y : ℝ), ‖deriv (deriv f) y‖ ≤ B) (y : ℝ) : ‖deriv f y‖ ≤ 2 * r * B

A compactly supported C² bump on [a₀, a₀ + r) has ‖f'‖ ≤ 2 r sup ‖f''‖.

theorem TrilinearHT.Auto.lipschitz_of_support {f : ℝ → ℂ} {a₀ r B : ℝ} (hr : 0 < r) (hf : ContDiff ℝ 2 f) (hsupp : ∀ y ∉ Set.Ico a₀ (a₀ + r), f y = 0) (hB : ∀ (y : ℝ), ‖deriv (deriv f) y‖ ≤ B) (y z : ℝ) : ‖f y - f z‖ ≤ 2 * r * B * |y - z|

The Lipschitz bound ‖f y - f z‖ ≤ 2 r B |y - z| for such bumps.

theorem TrilinearHT.Auto.classWave_mod_bounds (κ : LocalKernelClass) {a₀ r : ℝ} (hr : 0 < r) (α c : ℝ) {A : ℝ} (hA : 2 * (kernelPlateau κ).K * (1 + 6 * Real.pi * (r * |α|)) ^ 2 ≤ A) : (Continuous fun (y : ℝ) => classWave κ a₀ r α y * ↑(Real.fourierChar (c * y))) ∧ (∀ (y : ℝ), ‖classWave κ a₀ r α y * ↑(Real.fourierChar (c * y))‖ ≤ 2) ∧ ∀ (y z : ℝ), ‖classWave κ a₀ r α y * ↑(Real.fourierChar (c * y)) - classWave κ a₀ r α z * ↑(Real.fourierChar (c * z))‖ ≤ (2 * A + 4 * Real.pi * (r * |c|)) / r * |y - z|

The modulated class wave θ(y) = W(y) e(c y) is bounded by two and Lipschitz with constant (2A + 4π r |c|)/r.

theorem TrilinearHT.Auto.bumpMultiplier_le_small {η : ℝ} (h : |η| ≤ 1) : bumpMultiplier η ≤ (2 * Real.pi) ^ 2 * |η|

theorem TrilinearHT.Auto.bumpMultiplier_le_large {η : ℝ} (h : 1 < |η|) : bumpMultiplier η ≤ (2 * Real.pi) ^ 2 * |η|⁻¹

theorem TrilinearHT.Auto.bumpMultiplier_depth_sum_le (G : RealDyadicGrid) (Ds : Finset ℤ) (x : ℝ) : ∑ s ∈ Ds, bumpMultiplier (dyadicGridLength G s * x) ≤ 4 * (2 * Real.pi) ^ 2

The multiplicity of a fixed center over distinct depths: the band multipliers at the scales |I_s| x of a set of distinct depths sum to at most 4 (2π)².