Section 14.2, part 2b: lem:shortblock, window masses, deletion, sums

This file was automatically generated by Claude.

Formalization of blueprint Section 14, "The two-side estimate" (sec:sides), subsection 2, "Comparison on a short depth block", part 2b: lem:shortblock: window masses, deletion, comparison, sums (lines 2318-2371) of blueprint/formalization_blueprint.tex.

theorem TrilinearHT.Auto.leafUnion_mass_le {ι : Type u_1} {S : Finset ι} {aL lL : ι → ℝ} (hdis : (↑S).PairwiseDisjoint (leafInterval aL lL)) (z : ℝ → ℂ) (hz : ∀ i ∈ S, ∫⁻ (x : ℝ) in leafInterval aL lL i, ‖z x‖ₑ ^ 2 ≤ ENNReal.ofReal (lL i)) : ∫⁻ (x : ℝ) in leafUnion S aL lL, ‖z x‖ₑ ^ 2 ≤ MeasureTheory.volume (leafUnion S aL lL)

Blueprint line 2331 (total mass): ∫_E |z|² ≤ |E|.

theorem TrilinearHT.Auto.leaf_window_mass_le {ι : Type u_1} {S : Finset ι} {aL lL : ι → ℝ} (hdis : (↑S).PairwiseDisjoint (leafInterval aL lL)) (z : ℝ → ℂ) (hz : ∀ i ∈ S, ∫⁻ (x : ℝ) in leafInterval aL lL i, ‖z x‖ₑ ^ 2 ≤ ENNReal.ofReal (lL i)) {ρ : ℝ} (hρ : ∀ i ∈ S, lL i ≤ ρ) (x₀ ℓ : ℝ) : ∫⁻ (x : ℝ) in Set.Ico x₀ (x₀ + ℓ) ∩ leafUnion S aL lL, ‖z x‖ₑ ^ 2 ≤ ENNReal.ofReal (ℓ + 2 * ρ)

Blueprint lines 2332-2333 (regular slots): leaves of length at most ρ meeting an interval window of length ℓ carry mass at most ℓ + 2ρ.

theorem TrilinearHT.Auto.leaf_local_mass_le {ι : Type u_1} {S : Finset ι} {aL lL : ι → ℝ} (hdis : (↑S).PairwiseDisjoint (leafInterval aL lL)) (z : ℝ → ℂ) (hz : ∀ i ∈ S, ∫⁻ (x : ℝ) in leafInterval aL lL i, ‖z x‖ₑ ^ 2 ≤ ENNReal.ofReal (lL i)) (I : Set ℝ) (hI : ∀ i ∈ S, (I ∩ leafInterval aL lL i).Nonempty → leafInterval aL lL i ⊆ I) : ∫⁻ (x : ℝ) in I ∩ leafUnion S aL lL, ‖z x‖ₑ ^ 2 ≤ MeasureTheory.volume I

Blueprint line 2334 (local bound): if every leaf meeting a set I lies inside I, the mass on I is at most |I|.

theorem TrilinearHT.Auto.lintegral_window_tiling {δ : ℝ} (hδ : 0 < δ) (c : ℝ) (g : ℝ → ENNReal) : ∑' (n : ℤ), ∫⁻ (x : ℝ) in Set.Ico (δ * (↑n + c)) (δ * (↑n + c + 1)), g x = ∫⁻ (x : ℝ), g x

The δ-windows [δ(n + c), δ(n + c + 1)), n ∈ ℤ, tile the line: for every shift c, Σ_n ∫_{window n} g = ∫ g.

theorem TrilinearHT.Auto.lintegral_window_sum (K : ℕ) {δ : ℝ} (hδ : 0 < δ) (c : ℝ) (g : ℝ → ENNReal) : ∑' (n : ℤ), ∫⁻ (x : ℝ) in Set.Ico (δ * (↑n + c)) (δ * (↑n + c + ↑K)), g x = ↑K * ∫⁻ (x : ℝ), g x

Windows of K consecutive unit lengths cover every point K times: Σ_n ∫_{[δ(n+c), δ(n+c+K))} g = K ∫ g (the lift intervals in slots 2, 3).

theorem TrilinearHT.Auto.fast_parseval (s : Finset ℤ) (a : ℤ → ℂ) : 1 / 16 * ∫ (w : ℝ) in 0..16, ‖∑ m ∈ s, a m * ePhase (↑m * w / 16)‖ ^ 2 = ∑ m ∈ s, ‖a m‖ ^ 2

Parseval for fast trigonometric sums on the circle of length 16: (1/16) ∫₀¹⁶ |Σ_m a_m e(m w / 16)|² dw = Σ_m |a_m|².

theorem TrilinearHT.Auto.random_L2_moment {Ω : Type u_1} {T : Type u_2} [MeasurableSpace Ω] [MeasurableSpace T] (P : MeasureTheory.Measure Ω) [MeasureTheory.SigmaFinite P] (ν : MeasureTheory.Measure T) [MeasureTheory.SFinite ν] (F : Ω → T → ℂ) (hF : Measurable (Function.uncurry F)) {a : ℝ} (ha : 2 ≤ a) {Z : T → ENNReal} (hZ : Measurable Z) {Ca : ENNReal} (hmom : ∀ (w : T), (∫⁻ (σ : Ω), ‖F σ w‖ₑ ^ a ∂P) ^ (1 / a) ≤ Ca * Z w) : (∫⁻ (σ : Ω), (∫⁻ (w : T), ‖F σ w‖ₑ ^ 2 ∂ν) ^ (a / 2) ∂P) ^ (1 / a) ≤ Ca * (∫⁻ (w : T), Z w ^ 2 ∂ν) ^ (1 / 2)

Blueprint line 2330 ("Minkowski and the sign moments"): if a random function F^σ on a window satisfies the pointwise moment bound (E|F^σ(w)|^a)^{1/a} ≤ C_a Z(w) with a ≥ 2, then (E ‖F^σ‖₂^a)^{1/a} ≤ C_a ‖Z‖₂.

theorem TrilinearHT.Auto.latticeTorus_random_holder (B : Finset (ℤ × ℤ)) {ε M C : ENNReal} (hC1 : 1 ≤ C) (hB : ε ^ 2 * ↑B.card ≤ C) (hM : ε * M ≤ C) (hfib : ∀ (j : Fin 4) (m : ℤ), ↑{n ∈ B | latticeCoord (↑↑j) n = m}.card ≤ M) {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) (g : Ω → Fin 4 → ℤ × FastCircle → ENNReal) (hg : ∀ (ω : Ω) (i : Fin 4), Measurable (g ω i)) (p : Fin 4 → ENNReal) (hp : ∀ (i : Fin 4), 1 ≤ p i) (hsum : ∑ i : Fin 4, (p i).toReal⁻¹ ≤ 2) (hgm : ∀ (i : Fin 4), AEMeasurable (fun (ω : Ω) => MeasureTheory.eLpNorm (g ω i) (p i) (latticeCircleMeasure ε)) P) : ∫⁻ (ω : Ω), ∫⁻ (x : (ℤ × ℤ) × FastCircle × FastCircle), ∏ i : Fin 4, g ω i (latticeTorusProj (↑↑i) x) ∂latticeTorusMeasure B ε ∂P ≤ C * ∏ i : Fin 4, (∫⁻ (ω : Ω), MeasureTheory.eLpNorm (g ω i) (p i) (latticeCircleMeasure ε) ^ 4 ∂P) ^ (1 / 4)

Blueprint lines 2336-2340 ("Hölder in the random variables"): averaging the mixed absolute estimate over a random parameter ω ∈ (Ω, P) and applying Hölder with four L⁴(P) factors, E ∫ Π_j g_j^ω(n_j, w_j) ≤ C Π_j (E ‖g_j^ω‖_{L^{p_j}}⁴)^{1/4}.

theorem TrilinearHT.Auto.lintegral_fastHaar_le_sqrt {h : FastCircle → ENNReal} (hh : Measurable h) : ∫⁻ (t : FastCircle), h t ∂fastHaar ≤ (∫⁻ (t : FastCircle), h t ^ 2 ∂fastHaar) ^ (1 / 2)

Cauchy–Schwarz on the normalized fast circle: ∫ h ≤ (∫ h²)^{1/2}.

theorem TrilinearHT.Auto.heavy_slot_L4_le (ε : ENNReal) {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.SigmaFinite P] (g : Ω → ℤ × FastCircle → ENNReal) (hg : Measurable (Function.uncurry g)) : (∫⁻ (ω : Ω), (∫⁻ (y : ℤ × FastCircle), g ω y ∂latticeCircleMeasure ε) ^ 4 ∂P) ^ (1 / 4) ≤ ε * ∑' (m : ℤ), (∫⁻ (ω : Ω), ((∫⁻ (t : FastCircle), g ω (m, t) ^ 2 ∂fastHaar) ^ (1 / 2)) ^ 4 ∂P) ^ (1 / 4)

Blueprint lines 2336-2337 (the heavy slot, "unitarity and Minkowski"): the L⁴(P) norm of the local L¹ norm is at most ε Σ_m (E ‖g(m, ·)‖₂⁴)^{1/4}.

theorem TrilinearHT.Auto.regular_slot_L3_le_L4 (ε : ENNReal) (S : Finset ℤ) {g : ℤ × FastCircle → ENNReal} (hg : Measurable g) (hS : ∀ (y : ℤ × FastCircle), y.1 ∉ S → g y = 0) : MeasureTheory.eLpNorm g 3 (latticeCircleMeasure ε) ≤ MeasureTheory.eLpNorm g 4 (latticeCircleMeasure ε) * (ε * ↑S.card) ^ (1 / 12)

Blueprint line 2338 ("normalized norm monotonicity", regular slots): a function supported on the windows of finitely many slow points S has local L³ norm at most (ε |S|)^{1/12} times its local L⁴ norm.

theorem TrilinearHT.Auto.latticeCircle_eLpNorm_four (ε : ENNReal) {g : ℤ × FastCircle → ENNReal} (hg : Measurable g) : MeasureTheory.eLpNorm g 4 (latticeCircleMeasure ε) ^ 4 = ε * ∑' (m : ℤ), ∫⁻ (t : FastCircle), g (m, t) ^ 4 ∂fastHaar

The fourth power of the local L⁴ norm: ‖g‖₄⁴ = ε Σ_m ∫ g(m, ·)⁴.

theorem TrilinearHT.Auto.integral_fastHaar_eq (f : FastCircle → ℝ) : ∫ (t : FastCircle), f t ∂fastHaar = 1 / 16 * ∫ (x : ℝ) in 0..16, f ↑x

Haar averages on the fast circle are interval averages over one period.

noncomputable def TrilinearHT.Auto.fastCircleMultiplied (s : Finset ℤ) (a : ℤ → ℂ) (c : ℤ) (γ : ℝ) (t : FastCircle) : ℂ

The multiplied fast trigonometric polynomial as a function on the fast circle.

Equations

• TrilinearHT.Auto.fastCircleMultiplied s a c γ t = ∑ m ∈ s, a m * TrilinearHT.Auto.ePhase (γ * ↑m ^ 2 / ↑c) * (fourier m) t

theorem TrilinearHT.Auto.fastCircleMultiplied_coe (s : Finset ℤ) (a : ℤ → ℂ) (c : ℤ) (γ x : ℝ) : fastCircleMultiplied s a c γ ↑x = fastMultiplied s a c γ x

theorem TrilinearHT.Auto.continuous_fastCircleMultiplied (s : Finset ℤ) (a : ℤ → ℂ) (c : ℤ) (γ : ℝ) : Continuous (fastCircleMultiplied s a c γ)

theorem TrilinearHT.Auto.fast_fourth_moment_circle (s : Finset ℤ) (a : ℤ → ℂ) {c : ℤ} (hc0 : c ≠ 0) (hc : c ∣ 3) : 1 / 3 * ∫ (γ : ℝ) in 0..3, ∫ (t : FastCircle), ‖fastCircleMultiplied s a c γ t‖ ^ 4 ∂fastHaar ≤ 2 * (∑ m ∈ s, ‖a m‖ ^ 2) ^ 2

Blueprint eq:fourth-moment (lines 2318-2322) on the fast circle with normalized Haar measure, for finite Fourier sums: E_γ ∫ |U_γ F|⁴ ≤ 2 ‖F‖₂⁴ with ‖F‖₂² = Σ |a_m|².

theorem TrilinearHT.Auto.fast_circle_parseval (s : Finset ℤ) (a : ℤ → ℂ) (c : ℤ) (γ : ℝ) : ∫ (t : FastCircle), ‖fastCircleMultiplied s a c γ t‖ ^ 2 ∂fastHaar = ∑ m ∈ s, ‖a m‖ ^ 2

Unitarity of the fast multipliers (Parseval on the fast circle): ∫ |U_γ F|² = Σ_m |a_m|².

theorem TrilinearHT.Auto.continuous_fastCircleMultiplied_joint (s : Finset ℤ) (a : ℤ → ℂ) (c : ℤ) : Continuous fun (p : ℝ × FastCircle) => fastCircleMultiplied s a c p.1 p.2

theorem TrilinearHT.Auto.lintegral_fastCircle_sq (s : Finset ℤ) (a : ℤ → ℂ) (c : ℤ) (γ : ℝ) : ∫⁻ (t : FastCircle), ‖fastCircleMultiplied s a c γ t‖ₑ ^ 2 ∂fastHaar = ENNReal.ofReal (∑ m ∈ s, ‖a m‖ ^ 2)

Unitarity in ℝ≥0∞ form: ∫⁻ |U_γ F|² = Σ |a_m|².

theorem TrilinearHT.Auto.lintegral_fastCircle_fourth (s : Finset ℤ) (a : ℤ → ℂ) {c : ℤ} (hc0 : c ≠ 0) (hc : c ∣ 3) : ∫⁻ (γ : ℝ), ∫⁻ (t : FastCircle), ‖fastCircleMultiplied s a c γ t‖ₑ ^ 4 ∂fastHaar ∂gammaMeasure ≤ ENNReal.ofReal (2 * (∑ m ∈ s, ‖a m‖ ^ 2) ^ 2)

eq:fourth-moment in ℝ≥0∞ form with the uniform γ-average.

noncomputable def TrilinearHT.Auto.fastWindow {Ω : Type u_1} (s : Finset ℤ) (A : Ω → ℤ → ℤ → ℂ) (c : ℤ) (q : Ω × ℝ) (y : ℤ × FastCircle) : ENNReal

The random multiplied fast window of slot data A: at the random parameter q = (ω, γ) and the point (m, t), |U_γ F^ω(m, ·)(t)| with F^ω(m, ·) = Σ_k A(ω, m, k) e(k t / 16).

Equations

• TrilinearHT.Auto.fastWindow s A c q y = ‖TrilinearHT.Auto.fastCircleMultiplied s (A q.1 y.1) c q.2 y.2‖ₑ

theorem TrilinearHT.Auto.measurable_fastWindow {Ω : Type u_1} [MeasurableSpace Ω] (s : Finset ℤ) {A : Ω → ℤ → ℤ → ℂ} (hA : ∀ (m k : ℤ), Measurable fun (ω : Ω) => A ω m k) (c : ℤ) : Measurable fun (p : (Ω × ℝ) × ℤ × FastCircle) => fastWindow s A c p.1 p.2

theorem TrilinearHT.Auto.measurable_fastWindow_section {Ω : Type u_1} (s : Finset ℤ) (A : Ω → ℤ → ℤ → ℂ) (c : ℤ) (q : Ω × ℝ) : Measurable (fastWindow s A c q)

theorem TrilinearHT.Auto.fastCircleMultiplied_zero (s : Finset ℤ) (c : ℤ) (γ : ℝ) (t : FastCircle) : fastCircleMultiplied s (fun (x : ℤ) => 0) c γ t = 0

theorem TrilinearHT.Auto.per_cell_deletion_bound (B : Finset (ℤ × ℤ)) {ε M C : ENNReal} (hC1 : 1 ≤ C) (hB : ε ^ 2 * ↑B.card ≤ C) (hM : ε * M ≤ C) (hfib : ∀ (j : Fin 4) (m : ℤ), ↑{n ∈ B | latticeCoord (↑↑j) n = m}.card ≤ M) {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (s : Finset ℤ) (A : Fin 4 → Ω → ℤ → ℤ → ℂ) (hA : ∀ (j : Fin 4) (m k : ℤ), Measurable fun (ω : Ω) => A j ω m k) (S : Fin 4 → Finset ℤ) (hS : ∀ (j : Fin 4) (ω : Ω), ∀ m ∉ S j, A j ω m = fun (x : ℤ) => 0) (h : Fin 4) : ∫⁻ (q : Ω × ℝ), ∫⁻ (x : (ℤ × ℤ) × FastCircle × FastCircle), ∏ j : Fin 4, fastWindow s (A j) (fastSlotC j) q (latticeTorusProj (↑↑j) x) ∂latticeTorusMeasure B ε ∂P.prod gammaMeasure ≤ C * ∏ j : Fin 4, if j = h then ε * ∑ m ∈ S j, (∫⁻ (ω : Ω), ENNReal.ofReal (fastMass s (A j) ω m) ^ 2 ∂P) ^ (1 / 4) else ((ε * ↑(S j).card) ^ (1 / 3) * (ε * ∑ m ∈ S j, ∫⁻ (ω : Ω), ENNReal.ofReal (2 * fastMass s (A j) ω m ^ 2) ∂P)) ^ (1 / 4)

Blueprint lines 2334-2340 (deletion error at one cell): for random multiplied windows built from fast data A_j supported on slow points S_j, the expected positive form is at most C times, in the heavy slot h, ε Σ_m (E e_h(m)⁴)^{1/4}, and in each regular slot, ((ε|S_j|)^{1/3} ε Σ_m E 2 e_j(m)⁴)^{1/4} (exponents (1, 3, 3, 3), Hölder in (ω, γ), Minkowski and unitarity in the heavy slot, eq:fourth-moment in the regular slots).

noncomputable def TrilinearHT.Auto.intervalInput (δ c : ℝ) (T : Finset ℤ) (G : ℤ → ℂ) (y : ℝ) : ℂ

The interval input g(y) = Σ_{m ∈ T} G(m) 1_{|y - δ m| < c δ} of blueprint line 2346.

Equations

• TrilinearHT.Auto.intervalInput δ c T G y = ∑ m ∈ T, G m * if |y - δ * ↑m| < c * δ then 1 else 0

def TrilinearHT.Auto.intervalCell (δ c : ℝ) (n : ℤ × ℤ) : Set (ℝ × ℝ)

The cell of the lattice pair n: all four progression coordinates within c δ of the centers δ n_j.

Equations

• TrilinearHT.Auto.intervalCell δ c n = {z : ℝ × ℝ | ∀ (j : Fin 4), |TrilinearHT.Auto.realProgressionCoordinate j z - δ * ↑(TrilinearHT.Auto.latticeCoord (↑↑j) n)| < c * δ}

theorem TrilinearHT.Auto.intervalInput_prod {δ c : ℝ} (hδ : 0 < δ) (hc : c < 1 / 7) (T : Fin 4 → Finset ℤ) (G : Fin 4 → ℤ → ℂ) (hG : ∀ (j : Fin 4), ∀ m ∉ T j, G j m = 0) (z : ℝ × ℝ) : ∏ j : Fin 4, intervalInput δ c (T j) (G j) (realProgressionCoordinate j z) = ∑ n ∈ T 0 ×ˢ T 1, (∏ j : Fin 4, G j (latticeCoord (↑↑j) n)) * if z ∈ intervalCell δ c n then 1 else 0

Blueprint lines 2347-2349, pointwise: the product of the four interval inputs on a real progression is the sum over lattice pairs n of Π_j G_j(n_j) on the cell of n.

def TrilinearHT.Auto.offsetPolygon (c : ℝ) : Set (ℝ × ℝ)

The fixed offset polygon {(u, v) : |u + j v| < c, j = 0, …, 3} of blueprint line 2350.

Equations

• TrilinearHT.Auto.offsetPolygon c = {a : ℝ × ℝ | ∀ (j : Fin 4), |a.1 + ↑↑j * a.2| < c}

theorem TrilinearHT.Auto.intervalCell_eq {δ c : ℝ} (hδ : 0 < δ) (n : ℤ × ℤ) : intervalCell δ c n = (fun (z : ℝ × ℝ) => δ⁻¹ • (z + -(δ * ↑n.1, δ * (↑n.2 - ↑n.1)))) ⁻¹' offsetPolygon c

Each interval cell is the preimage of the offset polygon under z ↦ δ⁻¹ (z - a_n).

theorem TrilinearHT.Auto.volume_intervalCell {δ c : ℝ} (hδ : 0 < δ) (n : ℤ × ℤ) : MeasureTheory.volume (intervalCell δ c n) = ENNReal.ofReal (δ ^ 2) * MeasureTheory.volume (offsetPolygon c)

|intervalCell| = δ² |offsetPolygon|.

theorem TrilinearHT.Auto.measurableSet_intervalCell (δ c : ℝ) (n : ℤ × ℤ) : MeasurableSet (intervalCell δ c n)

theorem TrilinearHT.Auto.offsetPolygon_subset (c : ℝ) : offsetPolygon c ⊆ Set.Icc (-c) c ×ˢ Set.Icc (-(2 * c)) (2 * c)

theorem TrilinearHT.Auto.volume_offsetPolygon_lt_top (c : ℝ) : MeasureTheory.volume (offsetPolygon c) < ⊤

theorem TrilinearHT.Auto.round_center {δ c x : ℝ} (hδ : 0 < δ) (hc : c ≤ 1 / 2) {m : ℤ} (h : |x - δ * ↑m| < c * δ) : ⌊x / δ + 1 / 2⌋ = m

The rounding to the nearest center: if |x - δ m| < c δ with c ≤ 1/2, then ⌊x/δ + 1/2⌋ = m.

theorem TrilinearHT.Auto.interval_form_identity {δ c : ℝ} (hδ : 0 < δ) (hc : c < 1 / 7) (T : Fin 4 → Finset ℤ) (G : Fin 4 → ℤ → ℂ) (hG : ∀ (j : Fin 4), ∀ m ∉ T j, G j m = 0) (K : ℤ × ℤ → ℂ) : ∫ (z : ℝ × ℝ), K (⌊z.1 / δ + 1 / 2⌋, ⌊(z.1 + z.2) / δ + 1 / 2⌋) * ∏ j : Fin 4, intervalInput δ c (T j) (G j) (realProgressionCoordinate j z) = ↑(δ ^ 2 * (MeasureTheory.volume (offsetPolygon c)).toReal) * ∑ n ∈ T 0 ×ˢ T 1, K n * ∏ j : Fin 4, G j (latticeCoord (↑↑j) n)

Blueprint lines 2347-2352 (continuous comparison, sampled kernel): with interval inputs and the kernel sampled at the rounded centers, the continuous progression form equals δ² |offsetPolygon| times the lattice form Σ_n K(n) Π_j G_j(n_j).

noncomputable def TrilinearHT.Auto.roundSampledKernel (δ : ℝ) (w : ℝ × ℝ → ℂ) (z : ℝ × ℝ) : ℂ

The kernel sampled at the rounded centers: with n₀ = ⌊x/δ + 1/2⌋ and n₁ = ⌊(x + t)/δ + 1/2⌋, its value is w(δ n₀, δ(n₁ - n₀)) (blueprint line 2353).

Equations

• TrilinearHT.Auto.roundSampledKernel δ w z = w (δ * ↑⌊z.1 / δ + 1 / 2⌋, δ * ↑⌊(z.1 + z.2) / δ + 1 / 2⌋ - δ * ↑⌊z.1 / δ + 1 / 2⌋)

theorem TrilinearHT.Auto.roundSampled_offsets {δ : ℝ} (hδ : 0 < δ) (z : ℝ × ℝ) : -(δ / 2) ≤ z.1 - δ * ↑⌊z.1 / δ + 1 / 2⌋ ∧ z.1 - δ * ↑⌊z.1 / δ + 1 / 2⌋ < δ / 2 ∧ -(δ / 2) ≤ z.1 + z.2 - δ * ↑⌊(z.1 + z.2) / δ + 1 / 2⌋ ∧ z.1 + z.2 - δ * ↑⌊(z.1 + z.2) / δ + 1 / 2⌋ < δ / 2

theorem TrilinearHT.Auto.roundSampled_form_error {κ : LocalKernelClass} {a r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a r w) {δ : ℝ} (hδ : 0 < δ) (hδr : 5 * δ ≤ κ.margin * r) (f : Fin 4 → ℝ → ℂ) (hf : ∀ (i : Fin 4), Measurable (f i)) (p : Fin 4 → ENNReal) (hp : ∀ (i : Fin 4), 1 ≤ p i) (hsum : ∑ i : Fin 4, (p i).toReal⁻¹ ≤ 2) : ‖localProgressionForm r (fun (z : ℝ × ℝ) => w z - roundSampledKernel δ w z) f‖ₑ ≤ ENNReal.ofReal (4 * admissibleLipConst κ * (δ / r)) * ∏ i : Fin 4, MeasureTheory.eLpNorm (f i) (p i) (normalizedIntervalMeasure a r)

Blueprint lines 2353-2355 (second kernel-sampling error): replacing an admissible kernel on a cell of length r by its values at the rounded centers changes the form by at most 4 C_κ (δ / r) times the product of normalized local norms, for 5 δ ≤ μ r.

theorem TrilinearHT.Auto.measurable_intervalInput (δ c : ℝ) (T : Finset ℤ) (G : ℤ → ℂ) : Measurable (intervalInput δ c T G)

theorem TrilinearHT.Auto.intervalInput_eq_zero {δ c : ℝ} (T : Finset ℤ) (G : ℤ → ℂ) {y : ℝ} (hy : ∀ m ∈ T, c * δ ≤ |y - δ * ↑m|) : intervalInput δ c T G y = 0

theorem TrilinearHT.Auto.hasCompactSupport_intervalInput (δ c : ℝ) (T : Finset ℤ) (G : ℤ → ℂ) : HasCompactSupport (intervalInput δ c T G)

Interval inputs have compact support.

theorem TrilinearHT.Auto.norm_intervalInput_le (δ c : ℝ) (T : Finset ℤ) (G : ℤ → ℂ) (y : ℝ) : ‖intervalInput δ c T G y‖ ≤ ∑ m ∈ T, ‖G m‖

Interval inputs are bounded by Σ_m |G(m)|.

theorem TrilinearHT.Auto.memLp_intervalInput (δ c : ℝ) (T : Finset ℤ) (G : ℤ → ℂ) (p : ENNReal) : MeasureTheory.MemLp (intervalInput δ c T G) p MeasureTheory.volume

Interval inputs lie in every L^p.

theorem TrilinearHT.Auto.cn_interval_inputs {κ : LocalKernelClass} {q : ℝ} (hq : 2 ≤ q) {N : ℕ} (grid : RealDyadicGrid) (cells : Finset (ℤ × ℤ)) (firstDepth : ℤ) (depths : ∀ c ∈ cells, firstDepth ≤ c.1 ∧ c.1 < firstDepth + ↑N) (kernel : ℤ × ℤ → ℝ × ℝ → ℂ) (admissible : ∀ c ∈ cells, IsAdmissibleLocalKernel κ (dyadicGridLeft grid c.1 c.2) (dyadicGridLength grid c.1) (kernel c)) (δ c : ℝ) (T : Fin 4 → Finset ℤ) (G : Fin 4 → ℤ → ℂ) : ENNReal.ofReal (∑ I ∈ cells, dyadicGridLength grid I.1 * ‖localProgressionForm (dyadicGridLength grid I.1) (kernel I) fun (j : Fin 4) => intervalInput δ c (T j) (G j)‖) ≤ ENNReal.ofReal (finiteDepthConstant κ q N) * ∫⁻ (x : ℝ), ∏ j : Fin 4, scalarMaximalQ q (intervalInput δ c (T j) (G j)) x

Blueprint lines 2355-2357 (eq:CN for the interval inputs): for fixed fast and random parameters the interval inputs are measurable, compactly supported and in every L^q, so the original admissible kernels on the original summation cells (at most N consecutive depths) satisfy Σ_I |I| |H_I(g)| ≤ C_N ∫ Π_j M_q g_j.

theorem TrilinearHT.Auto.mixed_holder_four {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.SFinite P] (h : Fin 4 → ℝ × Ω × FastCircle → ENNReal) (hh : ∀ (j : Fin 4), Measurable (h j)) (p : Fin 4 → ℝ) (hp : ∀ (j : Fin 4), 0 < p j) (hsum : ∑ j : Fin 4, 1 / p j = 1) : ∫⁻ (y : ℝ), ∫⁻ (q : Ω × FastCircle × FastCircle), ∏ j : Fin 4, h j (y, q.1, (fastCoord ↑↑j) q.2) ∂P.prod (fastHaar.prod fastHaar) ≤ ∏ j : Fin 4, ClassicalMaximal.mixedENorm MeasureTheory.volume (P.prod fastHaar) (p j) 4 (h j)

Blueprint lines 2358-2362 ("one Hölder inequality of exponent four in (γ, σ, u, v), then spatial Hölder"): for exponents p_j > 0 with Σ 1/p_j = 1, ∫_y E ∫∫ Π_j h_j(y, ω, (1-j)u + jv) ≤ Π_j ‖h_j‖_{L^{p_j}_y L⁴_{ω, w}}; each map (u, v) ↦ (1-j)u + jv has Haar pushforward, so the inner norm is a single L⁴ norm.

noncomputable def TrilinearHT.Auto.fastIntervalInput {Ω : Type u_1} (δ c : ℝ) (T : Finset ℤ) (F : ℤ → Ω → ℂ) (p : ℝ × Ω) : ℂ

The interval inputs with fast/random data F_n (blueprint line 2346): g(y, z) = Σ_{n ∈ T} F_n(z) 1_{|y - δ n| < c δ}.

Equations

• TrilinearHT.Auto.fastIntervalInput δ c T F p = ∑ n ∈ T, F n p.2 * if |p.1 - δ * ↑n| < c * δ then 1 else 0

theorem TrilinearHT.Auto.interval_unique {δ c y : ℝ} (hδ : 0 < δ) (hc2 : c ≤ 1 / 2) {m n : ℤ} (hm : |y - δ * ↑m| < c * δ) (hn : |y - δ * ↑n| < c * δ) : m = n

For c ≤ 1/2 the intervals around distinct centers are disjoint.

theorem TrilinearHT.Auto.mixedENorm_fastIntervalInput_pow {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.Measure Ω) {δ c : ℝ} (hδ : 0 < δ) (hc2 : c ≤ 1 / 2) (T : Finset ℤ) (F : ℤ → Ω → ℂ) {p : ℝ} (hp : 0 < p) : (ClassicalMaximal.mixedENorm MeasureTheory.volume ν p 4 fun (z : ℝ × Ω) => ‖fastIntervalInput δ c T F z‖ₑ) ^ p = ∑ n ∈ T, ENNReal.ofReal (2 * (c * δ)) * (∫⁻ (z : Ω), ‖F n z‖ₑ ^ 4 ∂ν) ^ (p / 4)

Blueprint lines 2362-2364: for c ≤ 1/2, the mixed L^p_y L⁴ norm of an interval input is ‖g‖^p = Σ_{n ∈ T} 2 c δ (∫ |F_n|⁴)^{p/4}.

Assembly of eq:shortblock: the rectangle decomposition (blueprint lines 2290-2296)

def TrilinearHT.Auto.DepthRect.Side : DepthRect → Fin 4 → ℕ → Prop

The per-slot condition of a rectangle; membership is the product of these conditions.

Equations

• (TrilinearHT.Auto.DepthRect.rep S v).Side x✝¹ x✝ = ((x✝¹ ∈ S → x✝ = v) ∧ (x✝¹ ∉ S → v < x✝))
• (TrilinearHT.Auto.DepthRect.uniq a S h k).Side x✝¹ x✝ = if x✝¹ = a then x✝ / 2 ^ h = 2 * k else (x✝¹ ∈ S → x✝ / 2 ^ h = 2 * k + 1) ∧ (x✝¹ ∉ S → 2 * k + 2 ≤ x✝ / 2 ^ h)

@[instance_reducible]

instance TrilinearHT.Auto.DepthRect.instDecidableSide (R : DepthRect) (j : Fin 4) (x : ℕ) : Decidable (R.Side j x)

Equations

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

@[instance_reducible]

instance TrilinearHT.Auto.DepthRect.instDecidablePredValid : DecidablePred Valid

Equations

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

theorem TrilinearHT.Auto.DepthRect.mem_iff_side (R : DepthRect) (d : Fin 4 → ℕ) : R.Mem d ↔ ∀ (j : Fin 4), R.Side j (d j)

noncomputable def TrilinearHT.Auto.DepthRect.upTo (m : ℕ) : Finset DepthRect

The finitely many rectangle parameters relevant for depths below 2^m.

Equations

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

theorem TrilinearHT.Auto.DepthRect.mem_upTo_of_mem {m : ℕ} {R : DepthRect} {d : Fin 4 → ℕ} (hd : ∀ (j : Fin 4), d j < 2 ^ m) (hv : R.Valid) (hm : R.Mem d) : R ∈ upTo m

theorem TrilinearHT.Auto.DepthRect.side_partition (m : ℕ) (d : Fin 4 → ℕ) (hd : ∀ (j : Fin 4), d j < 2 ^ m) : (∑ R ∈ upTo m with Valid R, ∏ j : Fin 4, if R.Side j (d j) then 1 else 0) = 1

Blueprint lines 2290-2296 (the rectangles partition the depth tuples), as a partition of unity: for depths below 2^m, exactly one valid rectangle of upTo m has all four side conditions.

theorem TrilinearHT.Auto.localProgressionForm_rect_split (m : ℕ) (dep : ℝ → ℕ) (hdep : Measurable dep) (hd : ∀ (y : ℝ), dep y < 2 ^ m) (r : ℝ) (w : ℝ × ℝ → ℂ) (f : Fin 4 → ℝ → ℂ) (hint : MeasureTheory.Integrable (fun (z : ℝ × ℝ) => w z * ∏ j : Fin 4, f j (realProgressionCoordinate j z)) MeasureTheory.volume) : localProgressionForm r w f = ∑ R ∈ DepthRect.upTo m with DepthRect.Valid R, localProgressionForm r w fun (j : Fin 4) (y : ℝ) => f j y * if R.Side j (dep y) then 1 else 0

Blueprint lines 2290-2296 (multilinear splitting along the rectangles): if every point has a leaf depth below 2^m (a measurable labelling dep), then the local form splits as the sum over the valid rectangles of the forms with the inputs restricted to the side conditions.

theorem TrilinearHT.Auto.coeFn_fast_partial_sum (f : ↥(MeasureTheory.Lp ℂ 2 fastHaar)) (s : Finset ℤ) : ↑↑(∑ m ∈ s, fourierCoeff (↑↑f) m • fourierLp 2 m) =ᵐ[fastHaar] fastCircleMultiplied s (fourierCoeff ↑↑f) 1 0

The partial sum, as a function, is the unmultiplied fast trigonometric polynomial.

theorem TrilinearHT.Auto.fast_form_tendsto (g : Fin 4 → FastCircle → ℂ) (gN : ℕ → Fin 4 → FastCircle → ℂ) (hg : ∀ (j : Fin 4), Measurable (g j)) (hgN : ∀ (N : ℕ) (j : Fin 4), Measurable (gN N j)) (hL : ∀ (j : Fin 4), MeasureTheory.MemLp (g j) 2 fastHaar) (hLN : ∀ (N : ℕ) (j : Fin 4), MeasureTheory.MemLp (gN N j) 2 fastHaar) (hconv : ∀ (j : Fin 4), Filter.Tendsto (fun (N : ℕ) => MeasureTheory.eLpNorm (gN N j - g j) 2 fastHaar) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (N : ℕ) => ∫ (x : FastCircle × FastCircle), ∏ j : Fin 4, gN N j ((fastCoord ↑↑j) x) ∂fastHaar.prod fastHaar) Filter.atTop (nhds (∫ (x : FastCircle × FastCircle), ∏ j : Fin 4, g j ((fastCoord ↑↑j) x) ∂fastHaar.prod fastHaar))

Blueprint lines 2324-2325 ("the L² progression estimate passes to limits"): the fast form of one slow tuple is continuous in L² of each slot.

theorem TrilinearHT.Auto.fourierCoeff_congr_fast {F G : FastCircle → ℂ} (h : F =ᵐ[fastHaar] G) (m : ℤ) : fourierCoeff F m = fourierCoeff G m

noncomputable def TrilinearHT.Auto.fastPartialSum (N : ℕ) (F : FastCircle → ℂ) : FastCircle → ℂ

The symmetric fast partial sums S_N F = Σ_{|m| ≤ N} F̂(m) e(m ·/16) of an L² function on the fast circle, as functions.

Equations

• TrilinearHT.Auto.fastPartialSum N F = TrilinearHT.Auto.fastCircleMultiplied (Finset.Icc (-↑N) ↑N) (fourierCoeff F) 1 0

theorem TrilinearHT.Auto.continuous_fastPartialSum (N : ℕ) (F : FastCircle → ℂ) : Continuous (fastPartialSum N F)

theorem TrilinearHT.Auto.fastPartialSum_tendsto {F : FastCircle → ℂ} (hF : MeasureTheory.MemLp F 2 fastHaar) : Filter.Tendsto (fun (N : ℕ) => MeasureTheory.eLpNorm (fastPartialSum N F - F) 2 fastHaar) Filter.atTop (nhds 0)

S_N F → F in L² (blueprint lines 2324-2325, limiting route).

theorem TrilinearHT.Auto.fast_bessel_fn {F : FastCircle → ℂ} (hF : MeasureTheory.MemLp F 2 fastHaar) (s : Finset ℤ) : ENNReal.ofReal (∑ m ∈ s, ‖fourierCoeff F m‖ ^ 2) ≤ ∫⁻ (t : FastCircle), ‖F t‖ₑ ^ 2 ∂fastHaar

Bessel's inequality for the Fourier coefficients of a function.

theorem TrilinearHT.Auto.memLp_of_continuous_fast {g : FastCircle → ℂ} (hg : Continuous g) (p : ENNReal) : MeasureTheory.MemLp g p fastHaar

theorem TrilinearHT.Auto.memLp_fastPartialSum (N : ℕ) (F : FastCircle → ℂ) : MeasureTheory.MemLp (fastPartialSum N F) 2 fastHaar

Measurability of the uncentered maximal function in all variables

theorem TrilinearHT.Auto.uncenteredRealMaximal_eq_rat {E : Type u_1} [NormedAddCommGroup E] (g : ℝ → E) (x : ℝ) : uncenteredRealMaximal g x = ⨆ (p : ℚ × ℚ), if ↑p.1 < ↑p.2 ∧ x ∈ Set.Ioo ↑p.1 ↑p.2 then (ENNReal.ofReal (↑p.2 - ↑p.1))⁻¹ * ∫⁻ (y : ℝ) in Set.Icc ↑p.1 ↑p.2, ‖g y‖ₑ else 0

The uncentered maximal function is a supremum over intervals with rational endpoints containing the point in their interior.

theorem TrilinearHT.Auto.measurable_maximalQ {Ω : Type u_1} [MeasurableSpace Ω] (q : ℝ) {f : ℝ × Ω → ℂ} (hf : Measurable f) : Measurable (maximalQ q f)

The source's maximal function M_q f(y, ω) of a jointly measurable family is jointly measurable.

theorem TrilinearHT.Auto.window_sum_le_of_subset {δ : ℝ} (hδ : 0 < δ) (j : Fin 4) (g : ℝ → ENNReal) (S : Finset ℤ) (J : Set ℝ) (hJ : MeasurableSet J) (hS : ∀ m ∈ S, Set.Ico (δ * (↑m + fastLiftLeft j)) (δ * (↑m + fastLiftLeft j + fastLiftLen j)) ⊆ J) : ∑ m ∈ S, ∫⁻ (y : ℝ) in Set.Ico (δ * (↑m + fastLiftLeft j)) (δ * (↑m + fastLiftLeft j + fastLiftLen j)), g y ≤ ↑(fastLiftLenNat j) * ∫⁻ (y : ℝ) in J, g y

Window masses inside an interval: if the windows of all m ∈ S lie in J, then Σ_{m ∈ S} ∫_{window m} g ≤ L_j ∫_J g.

theorem TrilinearHT.Auto.volume_offsetPolygon_pos {c : ℝ} (hc : 0 < c) : 0 < MeasureTheory.volume (offsetPolygon c)

theorem TrilinearHT.Auto.random_local_L2 {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.SigmaFinite P] (ν : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite ν] (z : Ω → ℝ → ℂ) (hz : Measurable (Function.uncurry z)) (Z : ℝ → ℝ) (hZ : Measurable Z) {C4 : ℝ} (hmom : ∀ (y : ℝ), (∫⁻ (σ : Ω), ‖z σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ENNReal.ofReal (Z y)) : (∫⁻ (σ : Ω), MeasureTheory.eLpNorm (z σ) 2 ν ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * (∫⁻ (y : ℝ), ENNReal.ofReal (Z y) ^ 2 ∂ν) ^ (1 / 2)

The fourth random moment of a local L² norm (blueprint line 2330, "Minkowski and the sign moments"): (E ‖z^σ‖_{L²(ν)}⁴)^{1/4} ≤ C₄ ‖Z‖_{L²(ν)}.

theorem TrilinearHT.Auto.BlockData.sum_depth_le {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (s : ℤ) (g : ℝ → ENNReal) : ∑ I ∈ D.cells with I.1 = s, ∫⁻ (y : ℝ) in Set.Icc (D.left I) (D.left I + D.len I), g y ≤ ∫⁻ (y : ℝ), g y

Distinct cells at one depth are disjoint: their masses add up to at most the total mass.

theorem TrilinearHT.Auto.BlockData.err1_bound {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {C4 : ℝ} (hC4 : 0 ≤ C4) (hmom : ∀ (j : Fin 4) (y : ℝ), (∫⁻ (σ : Ω), ‖D.z j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ENNReal.ofReal (D.Z j y)) {a b : Fin 4} (hab : a ≠ b) (m : Fin 4 → ℝ) (hm : ∀ (j : Fin 4), ∫⁻ (y : ℝ), ENNReal.ofReal (D.Z j y) ^ 2 ≤ ENNReal.ofReal (m j)) (hloc : ∀ I ∈ D.cells, ∀ (j : Fin 4), ∫⁻ (y : ℝ) in Set.Icc (D.left I) (D.left I + D.len I), ENNReal.ofReal (D.Z j y) ^ 2 ≤ ENNReal.ofReal (D.len I)) (hw : ∑ s ∈ Finset.image Prod.fst D.cells, D.δ / dyadicGridLength D.grid s ≤ 1) : ∫⁻ (σ : Ω), ∑ I ∈ D.cells, ENNReal.ofReal (D.len I) * ‖D.err1 I σ‖ₑ ∂P ≤ ENNReal.ofReal (4 * admissibleLipConst κ * C4 ^ 4) * ENNReal.ofReal (m a) ^ (1 / 2) * ENNReal.ofReal (m b) ^ (1 / 2)

Blueprint lines 2307-2312 (summed first sampling error): with the local bounds ∫_I Z_j² ≤ |I|, the masses ∫ Z_j² ≤ m_j and Σ_{s} δ/r_s ≤ 1 over the occurring depths, E Σ_I |I| |H_I^{err}(z^σ)| ≤ 4 C_κ C₄⁴ m_a^{1/2} m_b^{1/2} for any two distinct slots.

theorem TrilinearHT.Auto.measurable_multiplied_slotLift {Ω : Type u_1} [MeasurableSpace Ω] {δ : ℝ} {z : Fin 4 → Ω → ℝ → ℂ} (hz : ∀ (j : Fin 4), Measurable (Function.uncurry (z j))) (j : Fin 4) (m : ℤ) (s : Finset ℤ) (c : ℤ) (g : Ω → ℤ → ℂ) (hg : Measurable fun (p : Ω × ℤ) => g p.1 p.2) : Measurable fun (p : (Ω × ℝ) × FastCircle) => fastCircleMultiplied s (fun (k : ℤ) => g p.1.1 m * fourierCoeff (slotLift δ (fun (i : Fin 4) => z i p.1.1) j m) k) c p.1.2 p.2

Joint measurability of the multiplied partial sums of the lifted random slots.

theorem TrilinearHT.Auto.BlockData.ae_memLp {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {C4 : ℝ} (hmom : ∀ (j : Fin 4) (y : ℝ), (∫⁻ (σ : Ω), ‖D.z j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ENNReal.ofReal (D.Z j y)) (hfin : ∀ (j : Fin 4), ∫⁻ (y : ℝ), ENNReal.ofReal (D.Z j y) ^ 2 < ⊤) : ∀ᵐ (σ : Ω) ∂P, ∀ (j : Fin 4), MeasureTheory.MemLp (D.inp σ j) 2 MeasureTheory.volume

Almost every random parameter gives L² inputs (fourth moments and finite masses).

noncomputable def TrilinearHT.Auto.BlockData.partialData {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (N : ℕ) (σ : Ω) : Fin 4 → ℤ → FastCircle → ℂ

The fast data of the partial sums S_N F^σ.

Equations

• D.partialData N σ j m = TrilinearHT.Auto.fastPartialSum N (TrilinearHT.Auto.slotLift D.δ (D.inp σ) j m)

theorem TrilinearHT.Auto.BlockData.latticeSum_tendsto {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (ε : ℤ × ℤ → Ω → ℂ) (σ : Ω) (hL : ∀ (j : Fin 4), MeasureTheory.MemLp (D.inp σ j) 2 MeasureTheory.volume) : Filter.Tendsto (fun (N : ℕ) => D.latticeSum ε σ (D.partialData N σ)) Filter.atTop (nhds (D.latticeSum ε σ (slotLift D.δ (D.inp σ))))

For L² inputs the lattice sums of S_N F^σ converge to that of F^σ (blueprint lines 2324-2325).

theorem TrilinearHT.Auto.BlockData.measurable_fastFormAt_partial {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (N : ℕ) (n : ℤ × ℤ) : Measurable fun (σ : Ω) => fastFormAt (D.partialData N σ) n

theorem TrilinearHT.Auto.BlockData.measurable_latticeSum_partial {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (ε : ℤ × ℤ → Ω → ℂ) (hε : ∀ (I : ℤ × ℤ), Measurable (ε I)) (N : ℕ) : Measurable fun (σ : Ω) => D.latticeSum ε σ (D.partialData N σ)

theorem TrilinearHT.Auto.BlockData.lintegral_latticeSum_le_liminf {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {C4 : ℝ} (hmom : ∀ (j : Fin 4) (y : ℝ), (∫⁻ (σ : Ω), ‖D.z j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ENNReal.ofReal (D.Z j y)) (hfin : ∀ (j : Fin 4), ∫⁻ (y : ℝ), ENNReal.ofReal (D.Z j y) ^ 2 < ⊤) (ε : ℤ × ℤ → Ω → ℂ) (hε : ∀ (I : ℤ × ℤ), Measurable (ε I)) : ∫⁻ (σ : Ω), ‖D.latticeSum ε σ (slotLift D.δ (D.inp σ))‖ₑ ∂P ≤ Filter.liminf (fun (N : ℕ) => ∫⁻ (σ : Ω), ‖D.latticeSum ε σ (D.partialData N σ)‖ₑ ∂P) Filter.atTop

Blueprint lines 2324-2325 ("pass to limits"): by Fatou, the expected lattice sum of the lifted inputs is at most the limit inferior of those of the partial sums.

theorem TrilinearHT.Auto.continuous_fastMultiplied (s : Finset ℤ) (a : ℤ → ℂ) (c : ℤ) (γ : ℝ) : Continuous (fastMultiplied s a c γ)

theorem TrilinearHT.Auto.fastForm_multiplied_eq_iter (s : Finset ℤ) (a : Fin 4 → ℤ → ℂ) (γ : ℝ) : ∫ (x : FastCircle × FastCircle), ∏ j : Fin 4, fastCircleMultiplied s (a j) (fastSlotC j) γ ((fastCoord ↑↑j) x) ∂fastHaar.prod fastHaar = (1 / 256) • ∫ (u : ℝ) (v : ℝ) in 0..16, ∏ j : Fin 4, fastMultiplied s (a j) (fastSlotC j) γ ((1 - ↑↑j) * u + ↑↑j * v)

The multiplied fast form on T₀² as an iterated integral over [0, 16]².

theorem TrilinearHT.Auto.fastForm_multiplied_invariant (s : Finset ℤ) (a : Fin 4 → ℤ → ℂ) (γ : ℝ) : ∫ (x : FastCircle × FastCircle), ∏ j : Fin 4, fastCircleMultiplied s (a j) (fastSlotC j) γ ((fastCoord ↑↑j) x) ∂fastHaar.prod fastHaar = ∫ (x : FastCircle × FastCircle), ∏ j : Fin 4, fastCircleMultiplied s (a j) (fastSlotC j) 0 ((fastCoord ↑↑j) x) ∂fastHaar.prod fastHaar

Blueprint lines 2314-2317 on T₀²: the multipliers leave the fast form unchanged.

noncomputable def TrilinearHT.Auto.BlockData.multWith {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (N : ℕ) (w : Fin 4 → ℤ → ℂ) (γ : ℝ) (σ : Ω) : Fin 4 → ℤ → FastCircle → ℂ

The multiplied partial sums U_{j,γ} S_N of the weighted lifted slots.

Equations

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

theorem TrilinearHT.Auto.BlockData.continuous_multWith {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (N : ℕ) (w : Fin 4 → ℤ → ℂ) (γ : ℝ) (σ : Ω) (j : Fin 4) (m : ℤ) : Continuous (D.multWith N w γ σ j m)

theorem TrilinearHT.Auto.BlockData.partialData_eq {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (N : ℕ) (σ : Ω) : D.partialData N σ = D.multWith N (fun (x : Fin 4) (x_1 : ℤ) => 1) 0 σ

theorem TrilinearHT.Auto.BlockData.fastFormAt_split {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (N : ℕ) (γ : ℝ) (σ : Ω) (a : Fin 4) (keep : Set ℤ) (n : ℤ × ℤ) : fastFormAt (D.multWith N (fun (x : Fin 4) (x_1 : ℤ) => 1) γ σ) n = fastFormAt (D.multWith N (wRet a keep) γ σ) n + fastFormAt (D.multWith N (wDel a keep) γ σ) n

theorem TrilinearHT.Auto.BlockData.norm_latticeSum_partial_le {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (ε : ℤ × ℤ → Ω → ℂ) (σ : Ω) (N : ℕ) (a : Fin 4) (keep : Set ℤ) : ‖D.latticeSum ε σ (D.partialData N σ)‖ₑ ≤ ∫⁻ (γ : ℝ), ‖D.latticeSum ε σ (D.multWith N (wRet a keep) γ σ)‖ₑ + ‖D.latticeSum ε σ (D.multWith N (wDel a keep) γ σ)‖ₑ ∂gammaMeasure

Blueprint lines 2314-2343 (first step of the comparison for fixed N): the lattice sum of S_N F^σ equals that of U_γ S_N F^σ for every γ; splitting the heavy slot into retained and deleted windows bounds it by the γ-average of the two lattice sums.

theorem TrilinearHT.Auto.fast_bessel_enorm {F : FastCircle → ℂ} (hF : Measurable F) (s : Finset ℤ) : ENNReal.ofReal (∑ m ∈ s, ‖fourierCoeff F m‖ ^ 2) ≤ ∫⁻ (t : FastCircle), ‖F t‖ₑ ^ 2 ∂fastHaar

Bessel's inequality in ℝ≥0∞ for any measurable function on the fast circle.

noncomputable def TrilinearHT.Auto.BlockData.ewin {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (j : Fin 4) (m : ℤ) : ENNReal

The deterministic fast window size e_j(m) = ‖Z_j(δ(m + ·))‖_{L²(T₀)} (blueprint line 2328).

Equations

• D.ewin j m = (∫⁻ (t : TrilinearHT.Auto.FastCircle), ‖TrilinearHT.Auto.slotLift D.δ D.Zc j m t‖ₑ ^ 2 ∂TrilinearHT.Auto.fastHaar) ^ (1 / 2)

noncomputable def TrilinearHT.Auto.BlockData.window {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (j : Fin 4) (m : ℤ) : Set ℝ

The window of the slow point m in slot j.

Equations

• D.window j m = Set.Ico (D.δ * (↑m + TrilinearHT.Auto.fastLiftLeft j)) (D.δ * (↑m + TrilinearHT.Auto.fastLiftLeft j + TrilinearHT.Auto.fastLiftLen j))

theorem TrilinearHT.Auto.BlockData.ewin_sq {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (j : Fin 4) (m : ℤ) : D.ewin j m ^ 2 = (ENNReal.ofReal (16 * D.δ))⁻¹ * ∫⁻ (y : ℝ) in D.window j m, ENNReal.ofReal (D.Z j y) ^ 2

theorem TrilinearHT.Auto.BlockData.window_moment {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {C4 : ℝ} (hmom : ∀ (j : Fin 4) (y : ℝ), (∫⁻ (σ : Ω), ‖D.z j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ENNReal.ofReal (D.Z j y)) (j : Fin 4) (m : ℤ) : (∫⁻ (σ : Ω), (∫⁻ (t : FastCircle), ‖slotLift D.δ (D.inp σ) j m t‖ₑ ^ 2 ∂fastHaar) ^ (4 / 2) ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * D.ewin j m

Blueprint line 2330 ("Minkowski and the sign moments") at a fast window: (E ‖F_j^σ(m, ·)‖₂⁴)^{1/4} ≤ C₄ e_j(m).

noncomputable def TrilinearHT.Auto.BlockData.supp {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (I : ℤ × ℤ) : Finset (ℤ × ℤ)

The kernel support of a cell: the slow pairs with nonzero sampled kernel.

Equations

• D.supp I = {n ∈ D.box I | D.kernel I (D.δ * ↑n.1, D.δ * ↑n.2 - D.δ * ↑n.1) ≠ 0}

noncomputable def TrilinearHT.Auto.BlockData.slow {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (I : ℤ × ℤ) (j : Fin 4) : Finset ℤ

The slow points of slot j relevant to the cell I.

Equations

• D.slow I j = Finset.image (TrilinearHT.Auto.latticeCoord ↑↑j) (D.supp I)

theorem TrilinearHT.Auto.BlockData.mem_supp {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) {I n : ℤ × ℤ} (hn : n ∈ D.supp I) : n ∈ D.box I ∧ D.kernel I (D.δ * ↑n.1, D.δ * ↑n.2 - D.δ * ↑n.1) ≠ 0

theorem TrilinearHT.Auto.BlockData.slow_mem {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) {I : ℤ × ℤ} (hI : I ∈ D.cells) {j : Fin 4} {m : ℤ} (hm : m ∈ D.slow I j) : D.left I + κ.margin * D.len I ≤ D.δ * ↑m ∧ D.δ * ↑m ≤ D.left I + D.len I - κ.margin * D.len I

The sample point of a relevant slow pair has all progression coordinates δ n_j in the interior part [a + μ r, a + r - μ r] of the cell.

theorem TrilinearHT.Auto.BlockData.window_subset {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) {I : ℤ × ℤ} (hI : I ∈ D.cells) {j : Fin 4} {m : ℤ} (hm : m ∈ D.slow I j) : D.window j m ⊆ Set.Icc (D.left I) (D.left I + D.len I)

The windows of relevant slow points lie in the cell.

theorem TrilinearHT.Auto.card_Icc_ceil_floor_le {a r δ : ℝ} (hδ : 0 < δ) (hr : 0 ≤ r) : ↑(Finset.Icc ⌈a / δ⌉ ⌊(a + r) / δ⌋).card ≤ r / δ + 1

noncomputable def TrilinearHT.Auto.BlockData.boxRange {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (I : ℤ × ℤ) : Finset ℤ

The one-dimensional index range of the box.

Equations

• D.boxRange I = Finset.Icc ⌈D.left I / D.δ⌉ ⌊(D.left I + D.len I) / D.δ⌋

theorem TrilinearHT.Auto.BlockData.card_boxRange {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (I : ℤ × ℤ) : ↑(D.boxRange I).card ≤ D.len I / D.δ + 1

theorem TrilinearHT.Auto.BlockData.card_supp_le {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (I : ℤ × ℤ) : ↑(D.supp I).card ≤ (D.len I / D.δ + 1) ^ 2

theorem TrilinearHT.Auto.BlockData.card_fiber_le {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (I : ℤ × ℤ) (j : Fin 4) (m : ℤ) : ↑{n ∈ D.supp I | latticeCoord (↑↑j) n = m}.card ≤ D.len I / D.δ + 1

theorem TrilinearHT.Auto.BlockData.card_slow_le {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) {I : ℤ × ℤ} (hI : I ∈ D.cells) (j : Fin 4) : ↑(D.slow I j).card ≤ D.len I / D.δ + 1

noncomputable def TrilinearHT.Auto.BlockData.cellCoef {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (w : Fin 4 → ℤ → ℂ) (I : ℤ × ℤ) (j : Fin 4) (σ : Ω) (m k : ℤ) : ℂ

The coefficients of the weighted multiplied slots restricted to the relevant slow points of a cell.

Equations

• D.cellCoef w I j σ m k = if m ∈ D.slow I j then w j m * fourierCoeff (TrilinearHT.Auto.slotLift D.δ (D.inp σ) j m) k else 0

theorem TrilinearHT.Auto.BlockData.cellCoef_of_mem {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (w : Fin 4 → ℤ → ℂ) {I : ℤ × ℤ} {j : Fin 4} (σ : Ω) {m : ℤ} (hm : m ∈ D.slow I j) : D.cellCoef w I j σ m = fun (k : ℤ) => w j m * fourierCoeff (slotLift D.δ (D.inp σ) j m) k

theorem TrilinearHT.Auto.BlockData.measurable_cellCoef {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (w : Fin 4 → ℤ → ℂ) (I : ℤ × ℤ) (j : Fin 4) (m k : ℤ) : Measurable fun (σ : Ω) => D.cellCoef w I j σ m k

theorem TrilinearHT.Auto.BlockData.norm_latticeSum_le_windows {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (ε : ℤ × ℤ → Ω → ℂ) (hε1 : ∀ (I : ℤ × ℤ) (σ : Ω), ‖ε I σ‖ ≤ 1) (N : ℕ) (w : Fin 4 → ℤ → ℂ) (γ : ℝ) (σ : Ω) : ‖D.latticeSum ε σ (D.multWith N w γ σ)‖ₑ ≤ ∑ I ∈ D.cells, ENNReal.ofReal (256 * localKernelSupBound κ * D.len I) * ∫⁻ (x : (ℤ × ℤ) × FastCircle × FastCircle), ∏ j : Fin 4, fastWindow (Finset.Icc (-↑N) ↑N) (fun (σ' : Ω) => D.cellCoef w I j σ') (fastSlotC j) (σ, γ) (latticeTorusProj (↑↑j) x) ∂latticeTorusMeasure (D.supp I) (ENNReal.ofReal (D.δ / D.len I))

Blueprint lines 2334-2337 (the lattice form dominates): the lattice sum of weighted multiplied slots is at most 256 C_κ' Σ_I |I| times the positive mixed forms of the fast windows on the kernel supports, with weights ε = δ / r_I.

noncomputable def TrilinearHT.Auto.BlockData.slotMass {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (σ : Ω) (j : Fin 4) (m : ℤ) : ENNReal

The squared fast mass of a lifted random slot.

Equations

• D.slotMass σ j m = ∫⁻ (t : TrilinearHT.Auto.FastCircle), ‖TrilinearHT.Auto.slotLift D.δ (D.inp σ) j m t‖ₑ ^ 2 ∂TrilinearHT.Auto.fastHaar

theorem TrilinearHT.Auto.BlockData.fastMass_cellCoef_le {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (w : Fin 4 → ℤ → ℂ) {I : ℤ × ℤ} {j : Fin 4} {m : ℤ} (hm : m ∈ D.slow I j) (s : Finset ℤ) (σ : Ω) : ENNReal.ofReal (fastMass s (fun (σ' : Ω) => D.cellCoef w I j σ') σ m) ≤ ‖w j m‖ₑ ^ 2 * D.slotMass σ j m

theorem TrilinearHT.Auto.BlockData.slotMass_moment {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {C4 : ℝ} (hmom : ∀ (j : Fin 4) (y : ℝ), (∫⁻ (σ : Ω), ‖D.z j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ENNReal.ofReal (D.Z j y)) (j : Fin 4) (m : ℤ) : (∫⁻ (σ : Ω), D.slotMass σ j m ^ 2 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * D.ewin j m

Fourth moment of the slot masses: (E X²)^{1/4} ≤ C₄ e_j(m).

theorem TrilinearHT.Auto.BlockData.sum_ewin_sq_le {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) {I : ℤ × ℤ} (hI : I ∈ D.cells) (j : Fin 4) : ∑ m ∈ D.slow I j, D.ewin j m ^ 2 ≤ (ENNReal.ofReal (16 * D.δ))⁻¹ * 8 * ∫⁻ (y : ℝ) in Set.Icc (D.left I) (D.left I + D.len I), ENNReal.ofReal (D.Z j y) ^ 2

The window sum of a cell: Σ_{m relevant} e_j(m)² ≤ (16 δ)⁻¹ 8 ∫_I Z_j².

theorem TrilinearHT.Auto.BlockData.heavy_factor_le {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {C4 : ℝ} (hmom : ∀ (j : Fin 4) (y : ℝ), (∫⁻ (σ : Ω), ‖D.z j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ENNReal.ofReal (D.Z j y)) {I : ℤ × ℤ} (hI : I ∈ D.cells) (a : Fin 4) {A : ℝ} (hA : 0 < A) (s : Finset ℤ) : ENNReal.ofReal (D.δ / D.len I) * ∑ m ∈ D.slow I a, (∫⁻ (σ : Ω), ENNReal.ofReal (fastMass s (fun (σ' : Ω) => D.cellCoef (wDel a {m : ℤ | D.ewin a m ≤ ENNReal.ofReal A}) I a σ') σ m) ^ 2 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * (ENNReal.ofReal A)⁻¹ * (ENNReal.ofReal (D.len I))⁻¹ * ∫⁻ (y : ℝ) in Set.Icc (D.left I) (D.left I + D.len I), ENNReal.ofReal (D.Z a y) ^ 2

The heavy factor of the deletion bound at one cell (blueprint lines 2335-2337): ε Σ_m (E fastMass²)^{1/4} ≤ C₄ A⁻¹ (2 r_I)⁻¹ ∫_I Z_a² for the deleted windows e_a > A.

theorem TrilinearHT.Auto.BlockData.regular_factor_le {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {C4 E2 : ℝ} (hmom : ∀ (j : Fin 4) (y : ℝ), (∫⁻ (σ : Ω), ‖D.z j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ENNReal.ofReal (D.Z j y)) {I : ℤ × ℤ} (hI : I ∈ D.cells) (j : Fin 4) (w : Fin 4 → ℤ → ℂ) (hw : ∀ (m : ℤ), ‖w j m‖ₑ ≤ 1) (hreg : ∀ (m : ℤ), D.ewin j m ^ 2 ≤ ENNReal.ofReal E2) (s : Finset ℤ) : ((ENNReal.ofReal (D.δ / D.len I) * ↑(D.slow I j).card) ^ (1 / 3) * (ENNReal.ofReal (D.δ / D.len I) * ∑ m ∈ D.slow I j, ∫⁻ (σ : Ω), ENNReal.ofReal (2 * fastMass s (fun (σ' : Ω) => D.cellCoef w I j σ') σ m ^ 2) ∂P)) ^ (1 / 4) ≤ (2 ^ (1 / 3) * (4 * ENNReal.ofReal C4 ^ 4 * ENNReal.ofReal E2 ^ 2)) ^ (1 / 4)

The regular factor of the deletion bound at one cell (blueprint line 2338): ((ε|S|)^{1/3} ε Σ_m E 2 fastMass²)^{1/4} ≤ (2^{1/3} · 4 C₄⁴ E₂²)^{1/4} when e_j² ≤ E₂.

theorem TrilinearHT.Auto.prod_ite_le_four {a : Fin 4} {g : Fin 4 → ENNReal} {H R : ENNReal} (ha : g a ≤ H) (hr : ∀ (j : Fin 4), j ≠ a → g j ≤ R) : ∏ j : Fin 4, g j ≤ H * R ^ 3

theorem TrilinearHT.Auto.measurable_fastWindow_proj {Ω : Type u_1} [MeasurableSpace Ω] (A : Ω → ℤ → ℤ → ℂ) (hA : ∀ (m k : ℤ), Measurable fun (ω : Ω) => A ω m k) (s : Finset ℤ) (j : Fin 4) : Measurable fun (p : (Ω × ℝ) × (ℤ × ℤ) × FastCircle × FastCircle) => fastWindow s A (fastSlotC j) p.1 (latticeTorusProj (↑↑j) p.2)

instance TrilinearHT.Auto.BlockData.instSFiniteProdIntFastCircleLatticeTorusMeasure (B : Finset (ℤ × ℤ)) (ε : ENNReal) : MeasureTheory.SFinite (latticeTorusMeasure B ε)

theorem TrilinearHT.Auto.BlockData.measurable_cellWindow {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (w : Fin 4 → ℤ → ℂ) (I : ℤ × ℤ) (s : Finset ℤ) (j : Fin 4) : Measurable fun (p : (Ω × ℝ) × (ℤ × ℤ) × FastCircle × FastCircle) => fastWindow s (fun (σ' : Ω) => D.cellCoef w I j σ') (fastSlotC j) p.1 (latticeTorusProj (↑↑j) p.2)

noncomputable def TrilinearHT.Auto.BlockData.regConst (C4 E2 : ℝ) : ENNReal

The regular-slot constant of the deletion bound.

Equations

• TrilinearHT.Auto.BlockData.regConst C4 E2 = (2 ^ (1 / 3) * (4 * ENNReal.ofReal C4 ^ 4 * ENNReal.ofReal E2 ^ 2)) ^ (1 / 4)

theorem TrilinearHT.Auto.BlockData.deletion_bound {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {C4 E2 : ℝ} (hmom : ∀ (j : Fin 4) (y : ℝ), (∫⁻ (σ : Ω), ‖D.z j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ENNReal.ofReal (D.Z j y)) (ε : ℤ × ℤ → Ω → ℂ) (hε1 : ∀ (I : ℤ × ℤ) (σ : Ω), ‖ε I σ‖ ≤ 1) (N : ℕ) (a : Fin 4) {A : ℝ} (hA : 0 < A) (hreg : ∀ (j : Fin 4), j ≠ a → ∀ (m : ℤ), D.ewin j m ^ 2 ≤ ENNReal.ofReal E2) : ∫⁻ (σ : Ω), ∫⁻ (γ : ℝ), ‖D.latticeSum ε σ (D.multWith N (wDel a {m : ℤ | D.ewin a m ≤ ENNReal.ofReal A}) γ σ)‖ₑ ∂gammaMeasure ∂P ≤ 4 * ENNReal.ofReal (256 * localKernelSupBound κ) * regConst C4 E2 ^ 3 * ENNReal.ofReal C4 * (ENNReal.ofReal A)⁻¹ * ∑ I ∈ D.cells, ∫⁻ (y : ℝ) in Set.Icc (D.left I) (D.left I + D.len I), ENNReal.ofReal (D.Z a y) ^ 2

Blueprint lines 2334-2343 (deletion of the large heavy windows): deleting in the heavy slot the slow points with e_a(m) > A, the expected lattice sum of the deleted part is at most C A⁻¹ Σ_I ∫_I Z_a² (exponents (1,3,3,3), Hölder in (σ, γ), regular windows e_j² ≤ E₂).

theorem TrilinearHT.Auto.fastRep_mem (j : Fin 4) (t : FastCircle) : fastRep j t ∈ Set.Ico (fastLiftLeft j) (fastLiftLeft j + 16)

theorem TrilinearHT.Auto.roundSampled_support {w : ℝ × ℝ → ℂ} {a r δ : ℝ} (hδ : 0 < δ) (hw : HasLocalProgressionSupport a r w) : HasLocalProgressionSupport (a - 3 * δ) (r + 6 * δ) (roundSampledKernel δ w)

The rounded-center kernel of a kernel with local progression support on [a, a + r] has local progression support on [a - 3δ, a + r + 3δ].

theorem TrilinearHT.Auto.measurable_roundSampledKernel {w : ℝ × ℝ → ℂ} (hw : Measurable w) (δ : ℝ) : Measurable (roundSampledKernel δ w)

noncomputable def TrilinearHT.Auto.BlockData.T {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) : Finset ℤ

The finitely many slow points whose windows can meet the support [lo, hi].

Equations

• D.T = Finset.Icc (⌊D.lo / D.δ⌋ - 8) (⌈D.hi / D.δ⌉ + 8)

theorem TrilinearHT.Auto.BlockData.slotLift_eq_zero {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) {m : ℤ} (hm : m ∉ D.T) (σ : Ω) (j : Fin 4) : slotLift D.δ (D.inp σ) j m = 0

theorem TrilinearHT.Auto.BlockData.multWith_eq_zero {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (N : ℕ) (w : Fin 4 → ℤ → ℂ) (γ : ℝ) (σ : Ω) (j : Fin 4) {m : ℤ} (hm : m ∉ D.T) : D.multWith N w γ σ j m = 0

noncomputable def TrilinearHT.Auto.BlockData.gin {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (N : ℕ) (w : Fin 4 → ℤ → ℂ) (γ : ℝ) (σ : Ω) (x : FastCircle × FastCircle) (j : Fin 4) : ℝ → ℂ

The interval inputs of the comparison at the fast point x ∈ T₀² (blueprint line 2346), with c = 1/8.

Equations

• D.gin N w γ σ x j = TrilinearHT.Auto.intervalInput D.δ (1 / 8) D.T fun (m : ℤ) => D.multWith N w γ σ j m ((TrilinearHT.Auto.fastCoord ↑↑j) x)

noncomputable def TrilinearHT.Auto.BlockData.err2 {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (I : ℤ × ℤ) (f : Fin 4 → ℝ → ℂ) : ℂ

The second kernel-sampling error at a cell.

Equations

• D.err2 I f = TrilinearHT.Auto.localProgressionForm (D.len I) (fun (w : ℝ × ℝ) => D.kernel I w - TrilinearHT.Auto.roundSampledKernel D.δ (D.kernel I) w) f

theorem TrilinearHT.Auto.sum_lintegral_le_lintegral_sum {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Finset ι) (f : ι → α → ENNReal) : ∑ i ∈ s, ∫⁻ (x : α), f i x ∂μ ≤ ∫⁻ (x : α), ∑ i ∈ s, f i x ∂μ

theorem TrilinearHT.Auto.BlockData.measurable_gin {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (N : ℕ) (w : Fin 4 → ℤ → ℂ) (γ : ℝ) (σ : Ω) (x : FastCircle × FastCircle) (j : Fin 4) : Measurable (D.gin N w γ σ x j)

theorem TrilinearHT.Auto.BlockData.memLp_gin {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (N : ℕ) (w : Fin 4 → ℤ → ℂ) (γ : ℝ) (σ : Ω) (x : FastCircle × FastCircle) (j : Fin 4) : MeasureTheory.MemLp (D.gin N w γ σ x j) 2 MeasureTheory.volume

theorem TrilinearHT.Auto.BlockData.cell_lattice_eq_interval {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (N : ℕ) (w : Fin 4 → ℤ → ℂ) (γ : ℝ) (σ : Ω) {I : ℤ × ℤ} (hI : I ∈ D.cells) : (↑(D.len I))⁻¹ ^ 2 * ↑(D.δ ^ 2) * 256 * ∑ n ∈ D.box I, D.kernel I (D.δ * ↑n.1, D.δ * ↑n.2 - D.δ * ↑n.1) * fastFormAt (D.multWith N w γ σ) n = ↑(256 / (MeasureTheory.volume (offsetPolygon (1 / 8))).toReal) * ∫ (x : FastCircle × FastCircle), localProgressionForm (D.len I) (roundSampledKernel D.δ (D.kernel I)) (D.gin N w γ σ x) ∂fastHaar.prod fastHaar

Blueprint lines 2345-2352 at one cell: the sampled lattice sum of the multiplied slots is (256 / |polygon|) ∫_{T₀²} H_I^{round}(g^x), the form of the interval inputs with the kernel sampled at the rounded centers.

theorem TrilinearHT.Auto.BlockData.round_form_eq {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (I : ℤ × ℤ) (hI : I ∈ D.cells) (f : Fin 4 → ℝ → ℂ) (hf : ∀ (j : Fin 4), Measurable (f j)) (hL : ∀ (j : Fin 4), MeasureTheory.MemLp (f j) 2 MeasureTheory.volume) : localProgressionForm (D.len I) (roundSampledKernel D.δ (D.kernel I)) f = localProgressionForm (D.len I) (D.kernel I) f - D.err2 I f

theorem TrilinearHT.Auto.BlockData.norm_latticeSum_interval {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (ε : ℤ × ℤ → Ω → ℂ) (hε1 : ∀ (I : ℤ × ℤ) (σ : Ω), ‖ε I σ‖ ≤ 1) (N : ℕ) (w : Fin 4 → ℤ → ℂ) (γ : ℝ) (σ : Ω) : ‖D.latticeSum ε σ (D.multWith N w γ σ)‖ₑ ≤ ENNReal.ofReal (256 / (MeasureTheory.volume (offsetPolygon (1 / 8))).toReal) * ∫⁻ (x : FastCircle × FastCircle), ENNReal.ofReal (∑ I ∈ D.cells, D.len I * ‖localProgressionForm (D.len I) (D.kernel I) (D.gin N w γ σ x)‖) + ∑ I ∈ D.cells, ENNReal.ofReal (D.len I) * ‖D.err2 I (D.gin N w γ σ x)‖ₑ ∂fastHaar.prod fastHaar

Blueprint lines 2345-2357 (continuous comparison): for every σ, γ the lattice sum of the multiplied slots is at most (256/|polygon|) ∫_{T₀²} of the summed absolute forms of the interval inputs plus their second sampling errors.

theorem TrilinearHT.Auto.BlockData.measurable_multWith_joint {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (N : ℕ) (w : Fin 4 → ℤ → ℂ) (j : Fin 4) (m : ℤ) : Measurable fun (z : (Ω × ℝ) × FastCircle) => D.multWith N w z.1.2 z.1.1 j m z.2

noncomputable def TrilinearHT.Auto.BlockData.ginFam {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (N : ℕ) (w : Fin 4 → ℤ → ℂ) (j : Fin 4) (p : ℝ × (Ω × ℝ) × FastCircle) : ℂ

The interval-input family of slot j, as a function of y and the inner variables ((σ, γ), w).

Equations

• D.ginFam N w j p = TrilinearHT.Auto.intervalInput D.δ (1 / 8) D.T (fun (m : ℤ) => D.multWith N w p.2.1.2 p.2.1.1 j m p.2.2) p.1

theorem TrilinearHT.Auto.BlockData.measurable_ginFam {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (N : ℕ) (w : Fin 4 → ℤ → ℂ) (j : Fin 4) : Measurable (D.ginFam N w j)

theorem TrilinearHT.Auto.BlockData.multWith_fourth {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {C4 : ℝ} (hmom : ∀ (j : Fin 4) (y : ℝ), (∫⁻ (σ : Ω), ‖D.z j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ENNReal.ofReal (D.Z j y)) (N : ℕ) (w : Fin 4 → ℤ → ℂ) (j : Fin 4) (m : ℤ) : ∫⁻ (z : (Ω × ℝ) × FastCircle), ‖D.multWith N w z.1.2 z.1.1 j m z.2‖ₑ ^ 4 ∂(P.prod gammaMeasure).prod fastHaar ≤ 2 * ‖w j m‖ₑ ^ 4 * (ENNReal.ofReal C4 * D.ewin j m) ^ 4

Blueprint eq:fourth-moment with the sign moments (lines 2318-2330): the fourth moment of a weighted multiplied slot over (σ, γ, w) is at most 2 |w|⁴ (C₄ e_j(m))⁴.

theorem TrilinearHT.Auto.BlockData.mixed_ginFam_pow {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {C4 : ℝ} (hmom : ∀ (j : Fin 4) (y : ℝ), (∫⁻ (σ : Ω), ‖D.z j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ENNReal.ofReal (D.Z j y)) (N : ℕ) (w : Fin 4 → ℤ → ℂ) (j : Fin 4) {p : ℝ} (hp : 0 < p) : (ClassicalMaximal.mixedENorm MeasureTheory.volume ((P.prod gammaMeasure).prod fastHaar) p 4 fun (z : ℝ × (Ω × ℝ) × FastCircle) => ‖D.ginFam N w j z‖ₑ) ^ p ≤ ∑ m ∈ D.T, ENNReal.ofReal (D.δ / 4) * (2 * ‖w j m‖ₑ ^ 4 * (ENNReal.ofReal C4 * D.ewin j m) ^ 4) ^ (p / 4)

Blueprint lines 2362-2364 for the comparison inputs: ‖g_j‖^p_{L^p_y L⁴} = Σ_m 2cδ (E ∫ |G_j(m)|⁴)^{p/4} ≤ Σ_m (δ/4) (2 |w|⁴ (C₄ e_j(m))⁴)^{p/4}.

theorem TrilinearHT.Auto.BlockData.main_bound {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {q : ℝ} (hq : 2 ≤ q) {Nd : ℕ} (first : ℤ) (hdepth : ∀ I ∈ D.cells, first ≤ I.1 ∧ I.1 < first + ↑Nd) (N : ℕ) (w : Fin 4 → ℤ → ℂ) (p : Fin 4 → ℝ) (hp : ∀ (j : Fin 4), 0 < p j) (hsum : ∑ j : Fin 4, 1 / p j = 1) (Cm : Fin 4 → ENNReal) (hCm : ∀ (j : Fin 4) (f : ℝ × (Ω × ℝ) × FastCircle → ℂ), Measurable f → ClassicalMaximal.mixedENorm MeasureTheory.volume ((P.prod gammaMeasure).prod fastHaar) (p j) 4 (maximalQ q f) ≤ Cm j * ClassicalMaximal.mixedENorm MeasureTheory.volume ((P.prod gammaMeasure).prod fastHaar) (p j) 4 fun (z : ℝ × (Ω × ℝ) × FastCircle) => ‖f z‖ₑ) : ∫⁻ (σ : Ω), ∫⁻ (γ : ℝ), ∫⁻ (x : FastCircle × FastCircle), ENNReal.ofReal (∑ I ∈ D.cells, D.len I * ‖localProgressionForm (D.len I) (D.kernel I) (D.gin N w γ σ x)‖) ∂fastHaar.prod fastHaar ∂gammaMeasure ∂P ≤ ENNReal.ofReal (finiteDepthConstant κ q Nd) * ∏ j : Fin 4, Cm j * ClassicalMaximal.mixedENorm MeasureTheory.volume ((P.prod gammaMeasure).prod fastHaar) (p j) 4 fun (z : ℝ × (Ω × ℝ) × FastCircle) => ‖D.ginFam N w j z‖ₑ

Blueprint lines 2355-2364 (the main term): eq:CN for the interval inputs at every fast and random parameter, Tonelli, one Hölder inequality of exponent four in (γ, σ, u, v) and spatial Hölder, and the mixed maximal estimate eq:mixed-Mq give E ∫∫ Σ_I |I| |H_I(g)| ≤ C_N Π_j C_j ‖g_j‖_{L^{p_j}_y L⁴}.

theorem TrilinearHT.Auto.lintegral_intervalInput_sq_le {δ c : ℝ} (hδ : 0 < δ) (hc2 : c ≤ 1 / 2) (T : Finset ℤ) (G : ℤ → ℂ) (J : Set ℝ) (hJ : MeasurableSet J) : ∫⁻ (y : ℝ) in J, ‖intervalInput δ c T G y‖ₑ ^ 2 ≤ ∑ m ∈ T with (Metric.ball (δ * ↑m) (c * δ) ∩ J).Nonempty, ENNReal.ofReal (2 * (c * δ)) * ‖G m‖ₑ ^ 2

The squared local L² mass of an interval input on a set J: ∫_J |g|² ≤ Σ_{m : interval meets J} 2cδ |G(m)|² for c ≤ 1/2.

theorem TrilinearHT.Auto.eLpNorm_indicator_intervalInput_le {δ c a r : ℝ} (hδ : 0 < δ) (hc2 : c ≤ 1 / 2) (T : Finset ℤ) (G : ℤ → ℂ) (J : Set ℝ) (hJ : MeasurableSet J) : MeasureTheory.eLpNorm (J.indicator (intervalInput δ c T G)) 2 (normalizedIntervalMeasure a r) ≤ (ENNReal.ofReal r⁻¹ * ∑ m ∈ T with (Metric.ball (δ * ↑m) (c * δ) ∩ J).Nonempty, ENNReal.ofReal (2 * (c * δ)) * ‖G m‖ₑ ^ 2) ^ (1 / 2)

The normalized local L² norm of a localized interval input.

theorem TrilinearHT.Auto.lintegral_finset_sum_sq_le {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Finset ι) (f : ι → α → ENNReal) (hf : ∀ (i : ι), AEMeasurable (f i) μ) : (∫⁻ (x : α), (∑ i ∈ s, f i x) ^ 2 ∂μ) ^ (1 / 2) ≤ ∑ i ∈ s, (∫⁻ (x : α), f i x ^ 2 ∂μ) ^ (1 / 2)

Minkowski's inequality in L² for finite sums of nonnegative functions.

noncomputable def TrilinearHT.Auto.BlockData.J {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (I : ℤ × ℤ) : Set ℝ

The localization interval of the second sampling error at a cell.

Equations

• D.J I = Set.Icc (D.left I + κ.margin * D.len I - 3 * D.δ) (D.left I + D.len I - κ.margin * D.len I + 3 * D.δ)

theorem TrilinearHT.Auto.BlockData.err2_support {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) {I : ℤ × ℤ} (hI : I ∈ D.cells) (z : ℝ × ℝ) (hz : D.kernel I z - roundSampledKernel D.δ (D.kernel I) z ≠ 0) (j : Fin 4) : realProgressionCoordinate j z ∈ D.J I

theorem TrilinearHT.Auto.BlockData.err2_local {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) {I : ℤ × ℤ} (hI : I ∈ D.cells) (f : Fin 4 → ℝ → ℂ) : D.err2 I f = D.err2 I fun (j : Fin 4) => (D.J I).indicator (f j)

The second sampling error only sees the inputs on J_I.

noncomputable def TrilinearHT.Auto.BlockData.TJ {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (I : ℤ × ℤ) : Finset ℤ

The slow points whose intervals meet J_I.

Equations

• D.TJ I = {m ∈ D.T | (Metric.ball (D.δ * ↑m) (1 / 8 * D.δ) ∩ D.J I).Nonempty}

theorem TrilinearHT.Auto.BlockData.TJ_window_subset {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) {I : ℤ × ℤ} (hI : I ∈ D.cells) {m : ℤ} (hm : m ∈ D.TJ I) (j : Fin 4) : D.window j m ⊆ Set.Icc (D.left I) (D.left I + D.len I)

The windows of the slow points meeting J_I lie in the cell.

theorem TrilinearHT.Auto.BlockData.sum_cells_ab_le {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (a b : Fin 4) (m : Fin 4 → ℝ) (hm : ∀ (j : Fin 4), ∫⁻ (y : ℝ), ENNReal.ofReal (D.Z j y) ^ 2 ≤ ENNReal.ofReal (m j)) (hw : ∑ s ∈ Finset.image Prod.fst D.cells, D.δ / dyadicGridLength D.grid s ≤ 1) : ∑ I ∈ D.cells, ENNReal.ofReal (D.δ / D.len I) * ((∫⁻ (y : ℝ) in Set.Icc (D.left I) (D.left I + D.len I), ENNReal.ofReal (D.Z a y) ^ 2) ^ (1 / 2) * (∫⁻ (y : ℝ) in Set.Icc (D.left I) (D.left I + D.len I), ENNReal.ofReal (D.Z b y) ^ 2) ^ (1 / 2)) ≤ ENNReal.ofReal (m a) ^ (1 / 2) * ENNReal.ofReal (m b) ^ (1 / 2)

The weighted cell sum of eq:shortblock (lines 2309-2312): with local masses Y_j(I) at most the total masses m_j on each depth and Σ_s δ / r_s ≤ 1, Σ_I (δ / r_I) Y_a(I)^{1/2} Y_b(I)^{1/2} ≤ m_a^{1/2} m_b^{1/2}.

noncomputable def TrilinearHT.Auto.BlockData.locMass {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (N : ℕ) (w : Fin 4 → ℤ → ℂ) (I : ℤ × ℤ) (j : Fin 4) (z : (Ω × ℝ) × FastCircle) : ENNReal

The localized squared masses of the comparison inputs at a cell.

Equations

• D.locMass N w I j z = ENNReal.ofReal (D.len I)⁻¹ * ∑ m ∈ D.TJ I, ENNReal.ofReal (D.δ / 4) * ‖D.multWith N w z.1.2 z.1.1 j m z.2‖ₑ ^ 2

theorem TrilinearHT.Auto.BlockData.measurable_locMass {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (N : ℕ) (w : Fin 4 → ℤ → ℂ) (I : ℤ × ℤ) (j : Fin 4) : Measurable (D.locMass N w I j)

theorem TrilinearHT.Auto.BlockData.err2_pointwise {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) {I : ℤ × ℤ} (hI : I ∈ D.cells) (N : ℕ) (w : Fin 4 → ℤ → ℂ) (γ : ℝ) (σ : Ω) (x : FastCircle × FastCircle) : ‖D.err2 I (D.gin N w γ σ x)‖ₑ ≤ ENNReal.ofReal (4 * admissibleLipConst κ * (D.δ / D.len I)) * ∏ j : Fin 4, D.locMass N w I j ((σ, γ), (fastCoord ↑↑j) x) ^ (1 / 2)

Pointwise second sampling error: ‖H_I^{err}(g)‖ ≤ 4 C_κ (δ / r) Π_j X_j^{1/2}.

theorem TrilinearHT.Auto.BlockData.sum_ewin_sq_le_of {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) {I : ℤ × ℤ} (j : Fin 4) (S : Finset ℤ) (hS : ∀ m ∈ S, D.window j m ⊆ Set.Icc (D.left I) (D.left I + D.len I)) : ∑ m ∈ S, D.ewin j m ^ 2 ≤ (ENNReal.ofReal (16 * D.δ))⁻¹ * 8 * ∫⁻ (y : ℝ) in Set.Icc (D.left I) (D.left I + D.len I), ENNReal.ofReal (D.Z j y) ^ 2

The window sum over slow points with windows in the cell.

theorem TrilinearHT.Auto.BlockData.locMass_L2 {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {C4 : ℝ} (hmom : ∀ (j : Fin 4) (y : ℝ), (∫⁻ (σ : Ω), ‖D.z j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ENNReal.ofReal (D.Z j y)) (N : ℕ) (w : Fin 4 → ℤ → ℂ) (hw : ∀ (j : Fin 4) (m : ℤ), ‖w j m‖ₑ ≤ 1) {I : ℤ × ℤ} (hI : I ∈ D.cells) (j : Fin 4) : (∫⁻ (z : (Ω × ℝ) × FastCircle), D.locMass N w I j z ^ 2 ∂(P.prod gammaMeasure).prod fastHaar) ^ (1 / 2) ≤ ENNReal.ofReal (D.len I)⁻¹ * err2Const C4 * ∫⁻ (y : ℝ) in Set.Icc (D.left I) (D.left I + D.len I), ENNReal.ofReal (D.Z j y) ^ 2

The L² size of the localized masses: (E ∫ X_j²)^{1/2} ≤ K r⁻¹ ∫_I Z_j².

theorem TrilinearHT.Auto.BlockData.err2_cell_bound {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {C4 : ℝ} (hmom : ∀ (j : Fin 4) (y : ℝ), (∫⁻ (σ : Ω), ‖D.z j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ENNReal.ofReal (D.Z j y)) (N : ℕ) (w : Fin 4 → ℤ → ℂ) (hw : ∀ (j : Fin 4) (m : ℤ), ‖w j m‖ₑ ≤ 1) {I : ℤ × ℤ} (hI : I ∈ D.cells) {a b : Fin 4} (hab : a ≠ b) (hloc : ∀ (j : Fin 4), ∫⁻ (y : ℝ) in Set.Icc (D.left I) (D.left I + D.len I), ENNReal.ofReal (D.Z j y) ^ 2 ≤ ENNReal.ofReal (D.len I)) : ∫⁻ (σ : Ω), ∫⁻ (γ : ℝ), ∫⁻ (x : FastCircle × FastCircle), ENNReal.ofReal (D.len I) * ‖D.err2 I (D.gin N w γ σ x)‖ₑ ∂fastHaar.prod fastHaar ∂gammaMeasure ∂P ≤ ENNReal.ofReal (4 * admissibleLipConst κ) * err2Const C4 ^ 2 * (ENNReal.ofReal (D.δ / D.len I) * ((∫⁻ (y : ℝ) in Set.Icc (D.left I) (D.left I + D.len I), ENNReal.ofReal (D.Z a y) ^ 2) ^ (1 / 2) * (∫⁻ (y : ℝ) in Set.Icc (D.left I) (D.left I + D.len I), ENNReal.ofReal (D.Z b y) ^ 2) ^ (1 / 2)))

Blueprint lines 2353-2355 (second sampling error, integrated): at one cell, E ∫∫ |I| |H_I^{err}(g)| ≤ 4 C_κ K² (δ / r_I) Y_a^{1/2} Y_b^{1/2}.

theorem TrilinearHT.Auto.BlockData.measurable_err1 {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) {I : ℤ × ℤ} (hI : I ∈ D.cells) : Measurable fun (σ : Ω) => D.err1 I σ

theorem TrilinearHT.Auto.BlockData.sum_ewin_sq_le_total {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (j : Fin 4) (S : Finset ℤ) : ∑ m ∈ S, D.ewin j m ^ 2 ≤ (ENNReal.ofReal (16 * D.δ))⁻¹ * 8 * ∫⁻ (y : ℝ), ENNReal.ofReal (D.Z j y) ^ 2

The total window mass of a slot: Σ_{m ∈ S} e_j(m)² ≤ (16 δ)⁻¹ 8 ∫ Z_j².

theorem TrilinearHT.Auto.BlockData.mixed_ginFam_le {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {C4 : ℝ} (hmom : ∀ (j : Fin 4) (y : ℝ), (∫⁻ (σ : Ω), ‖D.z j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ENNReal.ofReal (D.Z j y)) (N : ℕ) (w : Fin 4 → ℤ → ℂ) (hw : ∀ (j : Fin 4) (m : ℤ), ‖w j m‖ₑ ≤ 1) (j : Fin 4) {p : ℝ} (hp : 2 ≤ p) {B : ENNReal} (hB : ∀ (m : ℤ), ‖w j m‖ₑ ≠ 0 → D.ewin j m ≤ B) {mj : ℝ} (hmj : ∫⁻ (y : ℝ), ENNReal.ofReal (D.Z j y) ^ 2 ≤ ENNReal.ofReal mj) : (ClassicalMaximal.mixedENorm MeasureTheory.volume ((P.prod gammaMeasure).prod fastHaar) p 4 fun (z : ℝ × (Ω × ℝ) × FastCircle) => ‖D.ginFam N w j z‖ₑ) ≤ (1 / 8 * 2 ^ (p / 4) * ENNReal.ofReal C4 ^ p * B ^ (p - 2) * ENNReal.ofReal mj) ^ (1 / p)

Blueprint lines 2364-2366 (window power sums): if every retained window has e_j(m) ≤ B, then ‖g_j‖_{L^p_y L⁴} ≤ ((1/8) 2^{p/4} C₄^p B^{p-2} m_j)^{1/p}.

theorem TrilinearHT.Auto.BlockData.measurable_form_gin {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (r : ℝ) {k : ℝ × ℝ → ℂ} (hk : Measurable k) (N : ℕ) (w : Fin 4 → ℤ → ℂ) : Measurable fun (p : (Ω × ℝ) × FastCircle × FastCircle) => localProgressionForm r k (D.gin N w p.1.2 p.1.1 p.2)

theorem TrilinearHT.Auto.BlockData.measurable_fastFormAt_mult {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (N : ℕ) (w : Fin 4 → ℤ → ℂ) (n : ℤ × ℤ) : Measurable fun (q : Ω × ℝ) => fastFormAt (D.multWith N w q.2 q.1) n

theorem TrilinearHT.Auto.BlockData.measurable_latticeSum_mult {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (ε : ℤ × ℤ → Ω → ℂ) (hε : ∀ (I : ℤ × ℤ), Measurable (ε I)) (N : ℕ) (w : Fin 4 → ℤ → ℂ) : Measurable fun (q : Ω × ℝ) => D.latticeSum ε q.1 (D.multWith N w q.2 q.1)

theorem TrilinearHT.Auto.BlockData.norm_wRet_le (a : Fin 4) (keep : Set ℤ) (j : Fin 4) (m : ℤ) : ‖wRet a keep j m‖ₑ ≤ 1

theorem TrilinearHT.Auto.BlockData.partial_bound {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {C4 E2 : ℝ} (hmom : ∀ (j : Fin 4) (y : ℝ), (∫⁻ (σ : Ω), ‖D.z j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ENNReal.ofReal (D.Z j y)) (ε : ℤ × ℤ → Ω → ℂ) (hε : ∀ (I : ℤ × ℤ), Measurable (ε I)) (hε1 : ∀ (I : ℤ × ℤ) (σ : Ω), ‖ε I σ‖ ≤ 1) {a b : Fin 4} (hab : a ≠ b) (m : Fin 4 → ℝ) (hm : ∀ (j : Fin 4), ∫⁻ (y : ℝ), ENNReal.ofReal (D.Z j y) ^ 2 ≤ ENNReal.ofReal (m j)) (hloc : ∀ I ∈ D.cells, ∀ (j : Fin 4), ∫⁻ (y : ℝ) in Set.Icc (D.left I) (D.left I + D.len I), ENNReal.ofReal (D.Z j y) ^ 2 ≤ ENNReal.ofReal (D.len I)) (hw : ∑ s ∈ Finset.image Prod.fst D.cells, D.δ / dyadicGridLength D.grid s ≤ 1) (hreg : ∀ (j : Fin 4), j ≠ a → ∀ (n : ℤ), D.ewin j n ^ 2 ≤ ENNReal.ofReal E2) {A : ℝ} (hA : 0 < A) {q : ℝ} (hq : 2 ≤ q) {Nd : ℕ} (first : ℤ) (hdepth : ∀ I ∈ D.cells, first ≤ I.1 ∧ I.1 < first + ↑Nd) (p : Fin 4 → ℝ) (hp : ∀ (j : Fin 4), 2 ≤ p j) (hsum : ∑ j : Fin 4, 1 / p j = 1) (Cm : Fin 4 → ENNReal) (hCm : ∀ (j : Fin 4) (f : ℝ × (Ω × ℝ) × FastCircle → ℂ), Measurable f → ClassicalMaximal.mixedENorm MeasureTheory.volume ((P.prod gammaMeasure).prod fastHaar) (p j) 4 (maximalQ q f) ≤ Cm j * ClassicalMaximal.mixedENorm MeasureTheory.volume ((P.prod gammaMeasure).prod fastHaar) (p j) 4 fun (z : ℝ × (Ω × ℝ) × FastCircle) => ‖f z‖ₑ) (B : Fin 4 → ENNReal) (hB : ∀ (j : Fin 4) (n : ℤ), ‖wRet a {m : ℤ | D.ewin a m ≤ ENNReal.ofReal A} j n‖ₑ ≠ 0 → D.ewin j n ≤ B j) (N : ℕ) : ∫⁻ (σ : Ω), ‖D.latticeSum ε σ (D.partialData N σ)‖ₑ ∂P ≤ (4 * ENNReal.ofReal (256 * localKernelSupBound κ) * regConst C4 E2 ^ 3 * ENNReal.ofReal C4 * (ENNReal.ofReal A)⁻¹ * ∑ I ∈ D.cells, ∫⁻ (y : ℝ) in Set.Icc (D.left I) (D.left I + D.len I), ENNReal.ofReal (D.Z a y) ^ 2) + ENNReal.ofReal (256 / (MeasureTheory.volume (offsetPolygon (1 / 8))).toReal) * (ENNReal.ofReal (finiteDepthConstant κ q Nd) * ∏ j : Fin 4, Cm j * (1 / 8 * 2 ^ (p j / 4) * ENNReal.ofReal C4 ^ p j * B j ^ (p j - 2) * ENNReal.ofReal (m j)) ^ (1 / p j) + ENNReal.ofReal (4 * admissibleLipConst κ) * err2Const C4 ^ 2 * (ENNReal.ofReal (m a) ^ (1 / 2) * ENNReal.ofReal (m b) ^ (1 / 2)))

Blueprint lines 2314-2369 for the partial sums S_N: the expected lattice sum is bounded, uniformly in N, by the deletion error, the main term and the second sampling error.

theorem TrilinearHT.Auto.BlockData.rect_bound {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {C4 E2 : ℝ} (hC4 : 0 ≤ C4) (hmom : ∀ (j : Fin 4) (y : ℝ), (∫⁻ (σ : Ω), ‖D.z j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ENNReal.ofReal (D.Z j y)) (ε : ℤ × ℤ → Ω → ℂ) (hε : ∀ (I : ℤ × ℤ), Measurable (ε I)) (hε1 : ∀ (I : ℤ × ℤ) (σ : Ω), ‖ε I σ‖ ≤ 1) {a b : Fin 4} (hab : a ≠ b) (m : Fin 4 → ℝ) (hm : ∀ (j : Fin 4), ∫⁻ (y : ℝ), ENNReal.ofReal (D.Z j y) ^ 2 ≤ ENNReal.ofReal (m j)) (hloc : ∀ I ∈ D.cells, ∀ (j : Fin 4), ∫⁻ (y : ℝ) in Set.Icc (D.left I) (D.left I + D.len I), ENNReal.ofReal (D.Z j y) ^ 2 ≤ ENNReal.ofReal (D.len I)) (hw : ∑ s ∈ Finset.image Prod.fst D.cells, D.δ / dyadicGridLength D.grid s ≤ 1) (hreg : ∀ (j : Fin 4), j ≠ a → ∀ (n : ℤ), D.ewin j n ^ 2 ≤ ENNReal.ofReal E2) {A : ℝ} (hA : 0 < A) {q : ℝ} (hq : 2 ≤ q) {Nd : ℕ} (first : ℤ) (hdepth : ∀ I ∈ D.cells, first ≤ I.1 ∧ I.1 < first + ↑Nd) (p : Fin 4 → ℝ) (hp : ∀ (j : Fin 4), 2 ≤ p j) (hsum : ∑ j : Fin 4, 1 / p j = 1) (Cm : Fin 4 → ENNReal) (hCm : ∀ (j : Fin 4) (f : ℝ × (Ω × ℝ) × FastCircle → ℂ), Measurable f → ClassicalMaximal.mixedENorm MeasureTheory.volume ((P.prod gammaMeasure).prod fastHaar) (p j) 4 (maximalQ q f) ≤ Cm j * ClassicalMaximal.mixedENorm MeasureTheory.volume ((P.prod gammaMeasure).prod fastHaar) (p j) 4 fun (z : ℝ × (Ω × ℝ) × FastCircle) => ‖f z‖ₑ) (B : Fin 4 → ENNReal) (hB : ∀ (j : Fin 4) (n : ℤ), ‖wRet a {m : ℤ | D.ewin a m ≤ ENNReal.ofReal A} j n‖ₑ ≠ 0 → D.ewin j n ≤ B j) : ∫⁻ (σ : Ω), ‖D.total ε σ‖ₑ ∂P ≤ ENNReal.ofReal (4 * admissibleLipConst κ * C4 ^ 4) * ENNReal.ofReal (m a) ^ (1 / 2) * ENNReal.ofReal (m b) ^ (1 / 2) + ((4 * ENNReal.ofReal (256 * localKernelSupBound κ) * regConst C4 E2 ^ 3 * ENNReal.ofReal C4 * (ENNReal.ofReal A)⁻¹ * ∑ I ∈ D.cells, ∫⁻ (y : ℝ) in Set.Icc (D.left I) (D.left I + D.len I), ENNReal.ofReal (D.Z a y) ^ 2) + ENNReal.ofReal (256 / (MeasureTheory.volume (offsetPolygon (1 / 8))).toReal) * (ENNReal.ofReal (finiteDepthConstant κ q Nd) * ∏ j : Fin 4, Cm j * (1 / 8 * 2 ^ (p j / 4) * ENNReal.ofReal C4 ^ p j * B j ^ (p j - 2) * ENNReal.ofReal (m j)) ^ (1 / p j) + ENNReal.ofReal (4 * admissibleLipConst κ) * err2Const C4 ^ 2 * (ENNReal.ofReal (m a) ^ (1 / 2) * ENNReal.ofReal (m b) ^ (1 / 2))))

lem:shortblock at one leaf-depth rectangle (blueprint lines 2298-2369): the expected signed sum is at most the first and second sampling errors (≲ m_a^{1/2} m_b^{1/2}), the deletion error (≲ A⁻¹ Σ_I ∫_I Z_a²) and the main term C_N Π_j C_j (B_j^{p_j - 2} m_j)^{1/p_j}.

theorem TrilinearHT.Auto.DepthRect.side_heavy_le {R : DepthRect} (hv : R.Valid) {x : ℕ} (hx : R.Side R.heavy x) : x ≤ R.sep

The heavy slot has depth at most the separating depth.

theorem TrilinearHT.Auto.DepthRect.sep_le_side {R : DepthRect} {j : Fin 4} (hj : j ≠ R.heavy) {x : ℕ} (hx : R.Side j x) : R.sep ≤ x

All other slots have depth at least the separating depth.

theorem TrilinearHT.Auto.DepthRect.heavy_disjoint {R R' : DepthRect} (hv : R.Valid) (hl : R.level = R'.level) (hne : R ≠ R') {x : ℕ} (h1 : R.Side R.heavy x) (h2 : R'.Side R'.heavy x) : False

Within a level, the heavy masks of distinct positions are disjoint.

theorem TrilinearHT.Auto.DepthRect.desig_disjoint {R R' : DepthRect} (hv : R.Valid) (hl : R.level = R'.level) (hne : R ≠ R') {x : ℕ} (h1 : R.Side R.desig x) (h2 : R'.Side R'.desig x) : False

Within a level, the designated masks of distinct positions are disjoint.

noncomputable def TrilinearHT.Auto.ShortBlockTree.sel {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (R : DepthRect) (j : Fin 4) : Finset (ℤ × ℤ)

The leaves selected by slot j of a rectangle.

Equations

• T.sel R j = {L ∈ T.leaves | R.Side j (T.depth L)}

noncomputable def TrilinearHT.Auto.ShortBlockTree.mask {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (R : DepthRect) (j : Fin 4) : Set ℝ

The leaf mask E_j of slot j in a rectangle.

Equations

• T.mask R j = TrilinearHT.Auto.leafUnion (T.sel R j) (TrilinearHT.Auto.ShortBlockTree.cl G) (TrilinearHT.Auto.ShortBlockTree.cr G)

theorem TrilinearHT.Auto.ShortBlockTree.measurableSet_mask {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (R : DepthRect) (j : Fin 4) : MeasurableSet (T.mask R j)

theorem TrilinearHT.Auto.ShortBlockTree.mask_subset_root {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (R : DepthRect) (j : Fin 4) : T.mask R j ⊆ dyadicGridCell G T.root.1 T.root.2

theorem TrilinearHT.Auto.ShortBlockTree.mem_mask_iff {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) {R : DepthRect} {j : Fin 4} {y : ℝ} (hy : y ∈ dyadicGridCell G T.root.1 T.root.2) : y ∈ T.mask R j ↔ R.Side j (T.dep y)

theorem TrilinearHT.Auto.ShortBlockTree.sel_pairwiseDisjoint {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (R : DepthRect) (j : Fin 4) : (↑(T.sel R j)).PairwiseDisjoint (leafInterval (cl G) (cr G))

theorem TrilinearHT.Auto.DepthRect.pos_lt_of_mem_upTo {m : ℕ} {R : DepthRect} (hR : R ∈ upTo m) : R.pos < 2 ^ m

theorem TrilinearHT.Auto.DepthRect.card_level_fiber_le (m : ℕ) (F : Finset DepthRect) (hF : F ⊆ upTo m) (key : DepthRect) : {R ∈ F | R.level = key}.card ≤ 2 ^ m

At most 2^m positions per level.

theorem TrilinearHT.Auto.DepthRect.card_levels_le (m : ℕ) : (Finset.image level (upTo m)).card ≤ 16 + 64 * m

At most 16 + 64 m levels.

noncomputable def TrilinearHT.Auto.ShortBlockTree.rectData {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (κ : LocalKernelClass) (cells : Finset (ℤ × ℤ)) (hcells : cells ⊆ T.internal) (kernel : ℤ × ℤ → ℝ × ℝ → ℂ) (hker : ∀ I ∈ T.internal, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (kernel I)) {Ω : Type u_1} [MeasurableSpace Ω] {E : Type u_2} [NormedAddCommGroup E] (z : Fin 4 → ℝ → E) (hz : ∀ (j : Fin 4), Measurable fun (y : ℝ) => ‖z j y‖) (zσ : Fin 4 → Ω → ℝ → ℂ) (hzσ : ∀ (j : Fin 4), Measurable (Function.uncurry (zσ j))) (R : DepthRect) : BlockData κ Ω

The comparison data of one leaf-depth rectangle (blueprint lines 2298-2303): the summation cells coarser than the separating depth t, the sampling scale δ = β r_t, and the inputs restricted to the rectangle's leaf masks.

Equations

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

theorem TrilinearHT.Auto.ShortBlockTree.rect_Z_sq {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (κ : LocalKernelClass) (cells : Finset (ℤ × ℤ)) (hcells : cells ⊆ T.internal) (kernel : ℤ × ℤ → ℝ × ℝ → ℂ) (hker : ∀ I ∈ T.internal, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (kernel I)) {Ω : Type u_1} [MeasurableSpace Ω] {E : Type u_2} [NormedAddCommGroup E] (z : Fin 4 → ℝ → E) (hz : ∀ (j : Fin 4), Measurable fun (y : ℝ) => ‖z j y‖) (zσ : Fin 4 → Ω → ℝ → ℂ) (hzσ : ∀ (j : Fin 4), Measurable (Function.uncurry (zσ j))) (R : DepthRect) (j : Fin 4) (y : ℝ) : ENNReal.ofReal ((T.rectData κ cells hcells kernel hker z hz zσ hzσ R).Z j y) ^ 2 = (T.mask R j).indicator (fun (y : ℝ) => ‖↑‖z j y‖‖ₑ ^ 2) y

theorem TrilinearHT.Auto.ShortBlockTree.leafBound_zc {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) {E : Type u_2} [NormedAddCommGroup E] {z : Fin 4 → ℝ → E} (hL : T.LeafBound z) (j : Fin 4) (R : DepthRect) (i : ℤ × ℤ) : i ∈ T.sel R j → ∫⁻ (x : ℝ) in leafInterval (cl G) (cr G) i, ‖↑‖z j x‖‖ₑ ^ 2 ≤ ENNReal.ofReal (cr G i)

theorem TrilinearHT.Auto.ShortBlockTree.rect_mass {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (κ : LocalKernelClass) (cells : Finset (ℤ × ℤ)) (hcells : cells ⊆ T.internal) (kernel : ℤ × ℤ → ℝ × ℝ → ℂ) (hker : ∀ I ∈ T.internal, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (kernel I)) {Ω : Type u_1} [MeasurableSpace Ω] {E : Type u_2} [NormedAddCommGroup E] (z : Fin 4 → ℝ → E) (hz : ∀ (j : Fin 4), Measurable fun (y : ℝ) => ‖z j y‖) (zσ : Fin 4 → Ω → ℝ → ℂ) (hzσ : ∀ (j : Fin 4), Measurable (Function.uncurry (zσ j))) (hL : T.LeafBound z) (R : DepthRect) (j : Fin 4) : ∫⁻ (y : ℝ), ENNReal.ofReal ((T.rectData κ cells hcells kernel hker z hz zσ hzσ R).Z j y) ^ 2 ≤ ENNReal.ofReal (MeasureTheory.volume (T.mask R j)).toReal

The mass hypothesis of the rectangle: ∫ Z_j² ≤ |E_j|.

theorem TrilinearHT.Auto.ShortBlockTree.rect_loc {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (κ : LocalKernelClass) (cells : Finset (ℤ × ℤ)) (hcells : cells ⊆ T.internal) (kernel : ℤ × ℤ → ℝ × ℝ → ℂ) (hker : ∀ I ∈ T.internal, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (kernel I)) {Ω : Type u_1} [MeasurableSpace Ω] {E : Type u_2} [NormedAddCommGroup E] (z : Fin 4 → ℝ → E) (hz : ∀ (j : Fin 4), Measurable fun (y : ℝ) => ‖z j y‖) (zσ : Fin 4 → Ω → ℝ → ℂ) (hzσ : ∀ (j : Fin 4), Measurable (Function.uncurry (zσ j))) (hL : T.LeafBound z) (R : DepthRect) {I : ℤ × ℤ} (hI : I ∈ (T.rectData κ cells hcells kernel hker z hz zσ hzσ R).cells) (j : Fin 4) : ∫⁻ (y : ℝ) in Set.Icc ((T.rectData κ cells hcells kernel hker z hz zσ hzσ R).left I) ((T.rectData κ cells hcells kernel hker z hz zσ hzσ R).left I + (T.rectData κ cells hcells kernel hker z hz zσ hzσ R).len I), ENNReal.ofReal ((T.rectData κ cells hcells kernel hker z hz zσ hzσ R).Z j y) ^ 2 ≤ ENNReal.ofReal ((T.rectData κ cells hcells kernel hker z hz zσ hzσ R).len I)

The local hypothesis of the rectangle: ∫_I Z_j² ≤ |I|.

theorem TrilinearHT.Auto.ShortBlockTree.rect_weights {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (κ : LocalKernelClass) (cells : Finset (ℤ × ℤ)) (hcells : cells ⊆ T.internal) (kernel : ℤ × ℤ → ℝ × ℝ → ℂ) (hker : ∀ I ∈ T.internal, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (kernel I)) {Ω : Type u_1} [MeasurableSpace Ω] {E : Type u_2} [NormedAddCommGroup E] (z : Fin 4 → ℝ → E) (hz : ∀ (j : Fin 4), Measurable fun (y : ℝ) => ‖z j y‖) (zσ : Fin 4 → Ω → ℝ → ℂ) (hzσ : ∀ (j : Fin 4), Measurable (Function.uncurry (zσ j))) (R : DepthRect) : ∑ s ∈ Finset.image Prod.fst (T.rectData κ cells hcells kernel hker z hz zσ hzσ R).cells, (T.rectData κ cells hcells kernel hker z hz zσ hzσ R).δ / dyadicGridLength G s ≤ 1

The sampling weights of the rectangle: Σ_s δ / r_s ≤ 1.

theorem TrilinearHT.Auto.ShortBlockTree.rect_reg {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (κ : LocalKernelClass) (cells : Finset (ℤ × ℤ)) (hcells : cells ⊆ T.internal) (kernel : ℤ × ℤ → ℝ × ℝ → ℂ) (hker : ∀ I ∈ T.internal, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (kernel I)) {Ω : Type u_1} [MeasurableSpace Ω] {E : Type u_2} [NormedAddCommGroup E] (z : Fin 4 → ℝ → E) (hz : ∀ (j : Fin 4), Measurable fun (y : ℝ) => ‖z j y‖) (zσ : Fin 4 → Ω → ℝ → ℂ) (hzσ : ∀ (j : Fin 4), Measurable (Function.uncurry (zσ j))) (hL : T.LeafBound z) (R : DepthRect) {j : Fin 4} (hj : j ≠ R.heavy) (m : ℤ) : (T.rectData κ cells hcells kernel hker z hz zσ hzσ R).ewin j m ^ 2 ≤ ENNReal.ofReal (1 / 2 + 1 / (8 * beta κ))

The regular window bound of the rectangle (blueprint lines 2331-2333): e_j(m)² ≤ 1/2 + 1/(8β) for the slots other than the heavy one.

theorem TrilinearHT.Auto.BlockData.measurable_total {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (ε : ℤ × ℤ → Ω → ℂ) (hε : ∀ (I : ℤ × ℤ), Measurable (ε I)) : Measurable fun (σ : Ω) => D.total ε σ

theorem TrilinearHT.Auto.admissible_coord_mem_cell {κ : LocalKernelClass} {G : RealDyadicGrid} {I : ℤ × ℤ} {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) w) {z : ℝ × ℝ} (hz : w z ≠ 0) (j : Fin 4) : realProgressionCoordinate j z ∈ dyadicGridCell G I.1 I.2

The kernel of an admissible local form vanishes unless all progression coordinates lie in the cell.

theorem TrilinearHT.Auto.localProgressionForm_eq_zero_of_cell {κ : LocalKernelClass} {G : RealDyadicGrid} {I : ℤ × ℤ} {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) w) (f : Fin 4 → ℝ → ℂ) (a : Fin 4) (ha : ∀ y ∈ dyadicGridCell G I.1 I.2, f a y = 0) (r : ℝ) : localProgressionForm r w f = 0

A local form vanishes when one input vanishes on the cell.

theorem TrilinearHT.Auto.ShortBlockTree.heavy_mask_disjoint {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) {R : DepthRect} (hv : R.Valid) {I : ℤ × ℤ} (hI : I ∈ T.internal) (hs : T.first + ↑R.sep ≤ I.1) {y : ℝ} (hyI : y ∈ dyadicGridCell G I.1 I.2) : y ∉ T.mask R R.heavy

Below the separating depth, the heavy mask misses every internal cell.

theorem TrilinearHT.Auto.ShortBlockTree.total_decomp {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (κ : LocalKernelClass) (cells : Finset (ℤ × ℤ)) (hcells : cells ⊆ T.internal) (kernel : ℤ × ℤ → ℝ × ℝ → ℂ) (hker : ∀ I ∈ T.internal, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (kernel I)) {Ω : Type u_1} [MeasurableSpace Ω] {E : Type u_2} [NormedAddCommGroup E] (z : Fin 4 → ℝ → E) (hz : ∀ (j : Fin 4), Measurable fun (y : ℝ) => ‖z j y‖) (zσ : Fin 4 → Ω → ℝ → ℂ) (hzσ : ∀ (j : Fin 4), Measurable (Function.uncurry (zσ j))) {m : ℕ} (hm : K < 2 ^ m) (ε : ℤ × ℤ → Ω → ℂ) (σ : Ω) (hL2 : ∀ (j : Fin 4), MeasureTheory.MemLp ((dyadicGridCell G T.root.1 T.root.2).indicator (zσ j σ)) 2 MeasureTheory.volume) : (∑ I ∈ cells, ↑(dyadicGridLength G I.1) * ε I σ * localProgressionForm (dyadicGridLength G I.1) (kernel I) fun (j : Fin 4) => zσ j σ) = ∑ R ∈ DepthRect.upTo m with DepthRect.Valid R, (T.rectData κ cells hcells kernel hker z hz zσ hzσ R).total ε σ

Blueprint lines 2290-2296 (the rectangle decomposition of the signed sum): for inputs in L² on the root, Σ_I |I| ε_I H_I(z^σ) = Σ_R Σ_{I : depth < t_R} |I| ε_I H_I(z^σ 1_{E_R}).

theorem TrilinearHT.Auto.ShortBlockTree.rect_mom {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (κ : LocalKernelClass) (cells : Finset (ℤ × ℤ)) (hcells : cells ⊆ T.internal) (kernel : ℤ × ℤ → ℝ × ℝ → ℂ) (hker : ∀ I ∈ T.internal, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (kernel I)) {Ω : Type u_1} [MeasurableSpace Ω] {E : Type u_2} [NormedAddCommGroup E] (z : Fin 4 → ℝ → E) (hz : ∀ (j : Fin 4), Measurable fun (y : ℝ) => ‖z j y‖) (zσ : Fin 4 → Ω → ℝ → ℂ) (hzσ : ∀ (j : Fin 4), Measurable (Function.uncurry (zσ j))) (P : MeasureTheory.Measure Ω) {C4 : ℝ} (hmom : ∀ (j : Fin 4) (y : ℝ), (∫⁻ (σ : Ω), ‖zσ j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ‖z j y‖ₑ) (R : DepthRect) (j : Fin 4) (y : ℝ) : (∫⁻ (σ : Ω), ‖(T.rectData κ cells hcells kernel hker z hz zσ hzσ R).z j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ENNReal.ofReal ((T.rectData κ cells hcells kernel hker z hz zσ hzσ R).Z j y)

theorem TrilinearHT.Auto.ShortBlockTree.rect_apply {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (κ : LocalKernelClass) (cells : Finset (ℤ × ℤ)) (hcells : cells ⊆ T.internal) (kernel : ℤ × ℤ → ℝ × ℝ → ℂ) (hker : ∀ I ∈ T.internal, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (kernel I)) {Ω : Type u_1} [MeasurableSpace Ω] {E : Type u_2} [NormedAddCommGroup E] (z : Fin 4 → ℝ → E) (hz : ∀ (j : Fin 4), Measurable fun (y : ℝ) => ‖z j y‖) (zσ : Fin 4 → Ω → ℝ → ℂ) (hzσ : ∀ (j : Fin 4), Measurable (Function.uncurry (zσ j))) (hL : T.LeafBound z) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {C4 : ℝ} (hC4 : 0 ≤ C4) (hmom : ∀ (j : Fin 4) (y : ℝ), (∫⁻ (σ : Ω), ‖zσ j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ‖z j y‖ₑ) (ε : ℤ × ℤ → Ω → ℂ) (hε : ∀ (I : ℤ × ℤ), Measurable (ε I)) (hε1 : ∀ (I : ℤ × ℤ) (σ : Ω), ‖ε I σ‖ ≤ 1) {q : ℝ} (hq : 2 < q) {Nd : ℕ} (d₀ : ℤ) (hwin : ∀ I ∈ cells, d₀ ≤ I.1 ∧ I.1 < d₀ + ↑Nd) (Cs Cd : ENNReal) (hCs : ∀ (f : ℝ × (Ω × ℝ) × FastCircle → ℂ), Measurable f → ClassicalMaximal.mixedENorm MeasureTheory.volume ((P.prod gammaMeasure).prod fastHaar) (pStar q) 4 (maximalQ q f) ≤ Cs * ClassicalMaximal.mixedENorm MeasureTheory.volume ((P.prod gammaMeasure).prod fastHaar) (pStar q) 4 fun (z : ℝ × (Ω × ℝ) × FastCircle) => ‖f z‖ₑ) (hCd : ∀ (f : ℝ × (Ω × ℝ) × FastCircle → ℂ), Measurable f → ClassicalMaximal.mixedENorm MeasureTheory.volume ((P.prod gammaMeasure).prod fastHaar) (pReg q) 4 (maximalQ q f) ≤ Cd * ClassicalMaximal.mixedENorm MeasureTheory.volume ((P.prod gammaMeasure).prod fastHaar) (pReg q) 4 fun (z : ℝ × (Ω × ℝ) × FastCircle) => ‖f z‖ₑ) {R : DepthRect} (hv : R.Valid) : ∫⁻ (σ : Ω), ‖(T.rectData κ cells hcells kernel hker z hz zσ hzσ R).total ε σ‖ₑ ∂P ≤ ENNReal.ofReal (4 * admissibleLipConst κ * C4 ^ 4) * ENNReal.ofReal (MeasureTheory.volume (T.mask R R.heavy)).toReal ^ (1 / 2) * ENNReal.ofReal (MeasureTheory.volume (T.mask R R.desig)).toReal ^ (1 / 2) + ((4 * ENNReal.ofReal (256 * localKernelSupBound κ) * BlockData.regConst C4 (regE2 κ) ^ 3 * ENNReal.ofReal C4 * (ENNReal.ofReal (↑K + 2))⁻¹ * ∑ I ∈ (T.rectData κ cells hcells kernel hker z hz zσ hzσ R).cells, ∫⁻ (y : ℝ) in Set.Icc ((T.rectData κ cells hcells kernel hker z hz zσ hzσ R).left I) ((T.rectData κ cells hcells kernel hker z hz zσ hzσ R).left I + (T.rectData κ cells hcells kernel hker z hz zσ hzσ R).len I), ENNReal.ofReal ((T.rectData κ cells hcells kernel hker z hz zσ hzσ R).Z R.heavy y) ^ 2) + ENNReal.ofReal (256 / (MeasureTheory.volume (offsetPolygon (1 / 8))).toReal) * (ENNReal.ofReal (finiteDepthConstant κ q Nd) * ∏ j : Fin 4, (if j = R.heavy ∨ j = R.desig then Cs else Cd) * (1 / 8 * 2 ^ (pexp q R j / 4) * ENNReal.ofReal C4 ^ pexp q R j * (if j = R.heavy then ENNReal.ofReal (↑K + 2) else ENNReal.ofReal (regE2 κ) ^ (1 / 2)) ^ (pexp q R j - 2) * ENNReal.ofReal (MeasureTheory.volume (T.mask R j)).toReal) ^ (1 / pexp q R j) + ENNReal.ofReal (4 * admissibleLipConst κ) * BlockData.err2Const C4 ^ 2 * (ENNReal.ofReal (MeasureTheory.volume (T.mask R R.heavy)).toReal ^ (1 / 2) * ENNReal.ofReal (MeasureTheory.volume (T.mask R R.desig)).toReal ^ (1 / 2))))

rect_bound instantiated at a leaf-depth rectangle of the tree piece.

theorem TrilinearHT.Auto.ennreal_position_holder {ι : Type u_1} (s : Finset ι) (x y : ι → ENNReal) {p : ℝ} (hp : 2 < p) : ∑ i ∈ s, x i ^ (1 / p) * y i ^ (1 / p) ≤ ↑s.card ^ (1 - 2 / p) * ((∑ i ∈ s, x i) ^ (1 / 2) * (∑ i ∈ s, y i) ^ (1 / 2)) ^ (2 / p)

Hölder over positions in ℝ≥0∞ (blueprint line 2368): for p > 2, Σ_i x_i^{1/p} y_i^{1/p} ≤ J^{1 - 2/p} ((Σ x)^{1/2} (Σ y)^{1/2})^{2/p}.

theorem TrilinearHT.Auto.ShortBlockTree.sum_heavy_mask_le {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (F : Finset DepthRect) (hF : ∀ R ∈ F, R.Valid) (key : DepthRect) : ∑ R ∈ F with R.level = key, MeasureTheory.volume (T.mask R R.heavy) ≤ MeasureTheory.volume (dyadicGridCell G T.root.1 T.root.2)

Within a level, the heavy masks of distinct valid rectangles are disjoint, so their measures add up to at most the root length.

theorem TrilinearHT.Auto.ShortBlockTree.sum_desig_mask_le {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (F : Finset DepthRect) (hF : ∀ R ∈ F, R.Valid) (key : DepthRect) : ∑ R ∈ F with R.level = key, MeasureTheory.volume (T.mask R R.desig) ≤ MeasureTheory.volume (dyadicGridCell G T.root.1 T.root.2)

Within a level, the designated masks are disjoint.

theorem TrilinearHT.Auto.ShortBlockTree.volume_mask_le_root {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (R : DepthRect) (j : Fin 4) : MeasureTheory.volume (T.mask R j) ≤ MeasureTheory.volume (dyadicGridCell G T.root.1 T.root.2)

theorem TrilinearHT.Auto.ShortBlockTree.volume_mask_ne_top {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (R : DepthRect) (j : Fin 4) : MeasureTheory.volume (T.mask R j) ≠ ⊤

theorem TrilinearHT.Auto.BlockData.sum_cells_mass_le {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (j : Fin 4) : ∑ I ∈ D.cells, ∫⁻ (y : ℝ) in Set.Icc (D.left I) (D.left I + D.len I), ENNReal.ofReal (D.Z j y) ^ 2 ≤ ↑(Finset.image Prod.fst D.cells).card * ∫⁻ (y : ℝ), ENNReal.ofReal (D.Z j y) ^ 2

Summing the local masses over the cells costs the number of depths: Σ_I ∫_I Z_j² ≤ #depths · ∫ Z_j².

theorem TrilinearHT.Auto.main_factor_le {p : ℝ} (hp : 2 ≤ p) {Cm Cmax B M C : ENNReal} (hC : Cm ≤ Cmax) : Cm * (1 / 8 * 2 ^ (p / 4) * C ^ p * B ^ (p - 2) * M) ^ (1 / p) ≤ Cmax * (2 ^ (1 / 4) * C) * B ^ ((p - 2) / p) * M ^ (1 / p)

theorem TrilinearHT.Auto.rpow_le_self_of_one_le {E : ENNReal} (hE : 1 ≤ E) {e : ℝ} (he1 : e ≤ 1) : E ^ e ≤ E

theorem TrilinearHT.Auto.main_prod_le {a b : Fin 4} (hab : a ≠ b) (p : Fin 4 → ℝ) {ps pd : ℝ} (hps : 2 ≤ ps) (hpd : 2 ≤ pd) (hpa : p a = ps) (hpb : p b = ps) (hpo : ∀ (j : Fin 4), j ≠ a → j ≠ b → p j = pd) (Cm : Fin 4 → ENNReal) {Cmax : ENNReal} (hCm : ∀ (j : Fin 4), Cm j ≤ Cmax) (B : Fin 4 → ENNReal) {A' E : ENNReal} (hBa : B a = A') (hE : 1 ≤ E) (hBo : ∀ (j : Fin 4), j ≠ a → B j = E) (M : Fin 4 → ENNReal) {Rv : ENNReal} (hM : ∀ (j : Fin 4), M j ≤ Rv) (C : ENNReal) : ∏ j : Fin 4, Cm j * (1 / 8 * 2 ^ (p j / 4) * C ^ p j * B j ^ (p j - 2) * M j) ^ (1 / p j) ≤ (Cmax * (2 ^ (1 / 4) * C)) ^ 4 * (A' ^ ((ps - 2) / ps) * E ^ 3) * (M a ^ (1 / ps) * M b ^ (1 / ps) * (Rv ^ (1 / pd)) ^ 2)

The main-term product of a rectangle (blueprint lines 2362-2368): with exponents p_* in the heavy slot a and designated slot b, p elsewhere, heavy window bound A, regular bound E ≥ 1 and masks of measure at most |R|.

theorem TrilinearHT.Auto.ShortBlockTree.one_le_regE2 (κ : LocalKernelClass) : 1 ≤ regE2 κ

theorem TrilinearHT.Auto.ShortBlockTree.card_rect_depths_le {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (κ : LocalKernelClass) (cells : Finset (ℤ × ℤ)) (hcells : cells ⊆ T.internal) (kernel : ℤ × ℤ → ℝ × ℝ → ℂ) (hker : ∀ I ∈ T.internal, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (kernel I)) {Ω : Type u_1} [MeasurableSpace Ω] {E : Type u_2} [NormedAddCommGroup E] (z : Fin 4 → ℝ → E) (hz : ∀ (j : Fin 4), Measurable fun (y : ℝ) => ‖z j y‖) (zσ : Fin 4 → Ω → ℝ → ℂ) (hzσ : ∀ (j : Fin 4), Measurable (Function.uncurry (zσ j))) (R : DepthRect) : (Finset.image Prod.fst (T.rectData κ cells hcells kernel hker z hz zσ hzσ R).cells).card ≤ K

theorem TrilinearHT.Auto.ShortBlockTree.rect_simplified {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (κ : LocalKernelClass) (cells : Finset (ℤ × ℤ)) (hcells : cells ⊆ T.internal) (kernel : ℤ × ℤ → ℝ × ℝ → ℂ) (hker : ∀ I ∈ T.internal, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (kernel I)) {Ω : Type u_1} [MeasurableSpace Ω] {E : Type u_2} [NormedAddCommGroup E] (z : Fin 4 → ℝ → E) (hz : ∀ (j : Fin 4), Measurable fun (y : ℝ) => ‖z j y‖) (zσ : Fin 4 → Ω → ℝ → ℂ) (hzσ : ∀ (j : Fin 4), Measurable (Function.uncurry (zσ j))) (hL : T.LeafBound z) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {C4 : ℝ} (hC4 : 0 ≤ C4) (hmom : ∀ (j : Fin 4) (y : ℝ), (∫⁻ (σ : Ω), ‖zσ j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ‖z j y‖ₑ) (ε : ℤ × ℤ → Ω → ℂ) (hε : ∀ (I : ℤ × ℤ), Measurable (ε I)) (hε1 : ∀ (I : ℤ × ℤ) (σ : Ω), ‖ε I σ‖ ≤ 1) {q : ℝ} (hq : 2 < q) {Nd : ℕ} (d₀ : ℤ) (hwin : ∀ I ∈ cells, d₀ ≤ I.1 ∧ I.1 < d₀ + ↑Nd) (Cs Cd : ENNReal) (hCs : ∀ (f : ℝ × (Ω × ℝ) × FastCircle → ℂ), Measurable f → ClassicalMaximal.mixedENorm MeasureTheory.volume ((P.prod gammaMeasure).prod fastHaar) (pStar q) 4 (maximalQ q f) ≤ Cs * ClassicalMaximal.mixedENorm MeasureTheory.volume ((P.prod gammaMeasure).prod fastHaar) (pStar q) 4 fun (z : ℝ × (Ω × ℝ) × FastCircle) => ‖f z‖ₑ) (hCd : ∀ (f : ℝ × (Ω × ℝ) × FastCircle → ℂ), Measurable f → ClassicalMaximal.mixedENorm MeasureTheory.volume ((P.prod gammaMeasure).prod fastHaar) (pReg q) 4 (maximalQ q f) ≤ Cd * ClassicalMaximal.mixedENorm MeasureTheory.volume ((P.prod gammaMeasure).prod fastHaar) (pReg q) 4 fun (z : ℝ × (Ω × ℝ) × FastCircle) => ‖f z‖ₑ) {R : DepthRect} (hv : R.Valid) : ∫⁻ (σ : Ω), ‖(T.rectData κ cells hcells kernel hker z hz zσ hzσ R).total ε σ‖ₑ ∂P ≤ (ENNReal.ofReal (4 * admissibleLipConst κ * C4 ^ 4) + ENNReal.ofReal (256 / (MeasureTheory.volume (offsetPolygon (1 / 8))).toReal) * (ENNReal.ofReal (4 * admissibleLipConst κ) * BlockData.err2Const C4 ^ 2)) * (MeasureTheory.volume (T.mask R R.heavy) ^ (1 / 2) * MeasureTheory.volume (T.mask R R.desig) ^ (1 / 2)) + 4 * ENNReal.ofReal (256 * localKernelSupBound κ) * BlockData.regConst C4 (regE2 κ) ^ 3 * ENNReal.ofReal C4 * (ENNReal.ofReal (↑K + 2))⁻¹ * (↑K * MeasureTheory.volume (T.mask R R.heavy)) + ENNReal.ofReal (256 / (MeasureTheory.volume (offsetPolygon (1 / 8))).toReal) * ENNReal.ofReal (finiteDepthConstant κ q Nd) * ((max Cs Cd * (2 ^ (1 / 4) * ENNReal.ofReal C4)) ^ 4 * (ENNReal.ofReal (↑K + 2) ^ ((pStar q - 2) / pStar q) * (ENNReal.ofReal (regE2 κ) ^ (1 / 2)) ^ 3)) * (MeasureTheory.volume (T.mask R R.heavy) ^ (1 / pStar q) * MeasureTheory.volume (T.mask R R.desig) ^ (1 / pStar q) * (MeasureTheory.volume (dyadicGridCell G T.root.1 T.root.2) ^ (1 / pReg q)) ^ 2)

The bound of one leaf-depth rectangle in a form uniform over the rectangles.

theorem TrilinearHT.Auto.ShortBlockTree.sum_rects_le {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (m : ℕ) {p : ℝ} (hp : 2 < p) (X₁ X₂ Y : ENNReal) : ∑ R ∈ DepthRect.upTo m with DepthRect.Valid R, (X₁ * (MeasureTheory.volume (T.mask R R.heavy) ^ (1 / 2) * MeasureTheory.volume (T.mask R R.desig) ^ (1 / 2)) + X₂ * (↑K * MeasureTheory.volume (T.mask R R.heavy)) + Y * (MeasureTheory.volume (T.mask R R.heavy) ^ (1 / p) * MeasureTheory.volume (T.mask R R.desig) ^ (1 / p))) ≤ ↑(Finset.image DepthRect.level (Finset.filter DepthRect.Valid (DepthRect.upTo m))).card * (X₁ * MeasureTheory.volume (dyadicGridCell G T.root.1 T.root.2) + X₂ * (↑K * MeasureTheory.volume (dyadicGridCell G T.root.1 T.root.2)) + Y * ↑(2 ^ m) ^ (1 - 2 / p) * MeasureTheory.volume (dyadicGridCell G T.root.1 T.root.2) ^ (2 / p))

Blueprint lines 2366-2369 (summing the rectangle bounds over positions and levels): with n_L levels and at most 2^m positions per level, designated disjointness gives Σ_R [X₁ (M_a M_b)^{1/2} + X₂ K M_a + Y M_a^{1/p} M_b^{1/p}] ≤ n_L (X₁ |R| + X₂ K |R| + Y (2^m)^{1 - 2/p} |R|^{2/p}).

theorem TrilinearHT.Auto.ShortBlockTree.lintegral_root_lt_top {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) {E : Type u_2} [NormedAddCommGroup E] (z : Fin 4 → ℝ → E) (hL : T.LeafBound z) (j : Fin 4) : ∫⁻ (y : ℝ) in dyadicGridCell G T.root.1 T.root.2, ENNReal.ofReal ‖z j y‖ ^ 2 < ⊤

The root is covered by leaves of finite total mass.

theorem TrilinearHT.Auto.ShortBlockTree.ae_memLp_root {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) {Ω : Type u_1} [MeasurableSpace Ω] {E : Type u_2} [NormedAddCommGroup E] (z : Fin 4 → ℝ → E) (hz : ∀ (j : Fin 4), Measurable fun (y : ℝ) => ‖z j y‖) (zσ : Fin 4 → Ω → ℝ → ℂ) (hzσ : ∀ (j : Fin 4), Measurable (Function.uncurry (zσ j))) (hL : T.LeafBound z) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {C4 : ℝ} (hmom : ∀ (j : Fin 4) (y : ℝ), (∫⁻ (σ : Ω), ‖zσ j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ‖z j y‖ₑ) : ∀ᵐ (σ : Ω) ∂P, ∀ (j : Fin 4), MeasureTheory.MemLp ((dyadicGridCell G T.root.1 T.root.2).indicator (zσ j σ)) 2 MeasureTheory.volume

Almost every random parameter gives inputs in L² of the root.

theorem TrilinearHT.Auto.two_lt_pStar {q : ℝ} (hq : 2 < q) : 2 < pStar q

noncomputable def TrilinearHT.Auto.ShortBlockTree.coreX1 (κ : LocalKernelClass) (C4 : ℝ) : ENNReal

The sampling-error constant of eq:shortblock.

Equations

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

noncomputable def TrilinearHT.Auto.ShortBlockTree.coreX2 (κ : LocalKernelClass) (C4 : ℝ) : ENNReal

The deletion constant of eq:shortblock.

Equations

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

noncomputable def TrilinearHT.Auto.ShortBlockTree.coreX3 (κ : LocalKernelClass) (C4 : ℝ) (Cs Cd : ENNReal) : ENNReal

The main-term constant of eq:shortblock.

Equations

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

noncomputable def TrilinearHT.Auto.ShortBlockTree.numLevels (m : ℕ) : ℕ

The number of levels for depths below 2^m.

Equations

• TrilinearHT.Auto.ShortBlockTree.numLevels m = (Finset.image TrilinearHT.Auto.DepthRect.level (Finset.filter TrilinearHT.Auto.DepthRect.Valid (TrilinearHT.Auto.DepthRect.upTo m))).card

theorem TrilinearHT.Auto.ShortBlockTree.short_block_core {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (κ : LocalKernelClass) (cells : Finset (ℤ × ℤ)) (hcells : cells ⊆ T.internal) (kernel : ℤ × ℤ → ℝ × ℝ → ℂ) (hker : ∀ I ∈ T.internal, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (kernel I)) {Ω : Type u_1} [MeasurableSpace Ω] {E : Type u_2} [NormedAddCommGroup E] (z : Fin 4 → ℝ → E) (hz : ∀ (j : Fin 4), Measurable fun (y : ℝ) => ‖z j y‖) (zσ : Fin 4 → Ω → ℝ → ℂ) (hzσ : ∀ (j : Fin 4), Measurable (Function.uncurry (zσ j))) (hL : T.LeafBound z) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {C4 : ℝ} (hC4 : 0 ≤ C4) (hmom : ∀ (j : Fin 4) (y : ℝ), (∫⁻ (σ : Ω), ‖zσ j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ‖z j y‖ₑ) (ε : ℤ × ℤ → Ω → ℂ) (hε : ∀ (I : ℤ × ℤ), Measurable (ε I)) (hε1 : ∀ (I : ℤ × ℤ) (σ : Ω), ‖ε I σ‖ ≤ 1) {q : ℝ} (hq : 2 < q) {Nd : ℕ} (d₀ : ℤ) (hwin : ∀ I ∈ cells, d₀ ≤ I.1 ∧ I.1 < d₀ + ↑Nd) (Cs Cd : ENNReal) (hCs : ∀ (f : ℝ × (Ω × ℝ) × FastCircle → ℂ), Measurable f → ClassicalMaximal.mixedENorm MeasureTheory.volume ((P.prod gammaMeasure).prod fastHaar) (pStar q) 4 (maximalQ q f) ≤ Cs * ClassicalMaximal.mixedENorm MeasureTheory.volume ((P.prod gammaMeasure).prod fastHaar) (pStar q) 4 fun (z : ℝ × (Ω × ℝ) × FastCircle) => ‖f z‖ₑ) (hCd : ∀ (f : ℝ × (Ω × ℝ) × FastCircle → ℂ), Measurable f → ClassicalMaximal.mixedENorm MeasureTheory.volume ((P.prod gammaMeasure).prod fastHaar) (pReg q) 4 (maximalQ q f) ≤ Cd * ClassicalMaximal.mixedENorm MeasureTheory.volume ((P.prod gammaMeasure).prod fastHaar) (pReg q) 4 fun (z : ℝ × (Ω × ℝ) × FastCircle) => ‖f z‖ₑ) : ∫⁻ (σ : Ω), ‖∑ I ∈ cells, ↑(dyadicGridLength G I.1) * ε I σ * localProgressionForm (dyadicGridLength G I.1) (kernel I) fun (j : Fin 4) => zσ j σ‖ₑ ∂P ≤ ↑(numLevels (Nat.log 2 (K + 1) + 1)) * (coreX1 κ C4 * MeasureTheory.volume (dyadicGridCell G T.root.1 T.root.2) + coreX2 κ C4 * (ENNReal.ofReal (↑K + 2))⁻¹ * (↑K * MeasureTheory.volume (dyadicGridCell G T.root.1 T.root.2)) + ENNReal.ofReal (finiteDepthConstant κ q Nd) * coreX3 κ C4 Cs Cd * ENNReal.ofReal (↑K + 2) ^ ((pStar q - 2) / pStar q) * (MeasureTheory.volume (dyadicGridCell G T.root.1 T.root.2) ^ (1 / pReg q)) ^ 2 * ↑(2 ^ (Nat.log 2 (K + 1) + 1)) ^ (1 - 2 / pStar q) * MeasureTheory.volume (dyadicGridCell G T.root.1 T.root.2) ^ (2 / pStar q))

eq:shortblock for normalized sizes, before the numerical simplification of the constants (blueprint lines 2276-2369).

theorem TrilinearHT.Auto.numLevels_le (m : ℕ) : ShortBlockTree.numLevels m ≤ 16 + 64 * m

theorem TrilinearHT.Auto.numLevels_le_log (K : ℕ) : ↑(ShortBlockTree.numLevels (Nat.log 2 (K + 1) + 1)) ≤ 200 * (1 + Real.log (↑K + 2))

theorem TrilinearHT.Auto.ShortBlockTree.coreX1_ne_top (κ : LocalKernelClass) (C4 : ℝ) : coreX1 κ C4 ≠ ⊤

theorem TrilinearHT.Auto.ShortBlockTree.coreX2_ne_top (κ : LocalKernelClass) (C4 : ℝ) : coreX2 κ C4 ≠ ⊤

theorem TrilinearHT.Auto.ShortBlockTree.coreX3_ne_top (κ : LocalKernelClass) (C4 : ℝ) {Cs Cd : ENNReal} (hs : Cs ≠ ⊤) (hd : Cd ≠ ⊤) : coreX3 κ C4 Cs Cd ≠ ⊤

noncomputable def TrilinearHT.Auto.ShortBlockTree.shortBlockConst (κ : LocalKernelClass) (C4 : ℝ) (Cs Cd : ENNReal) : ℝ

The constant of eq:shortblock.

Equations

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

theorem TrilinearHT.Auto.ShortBlockTree.shortBlockConst_nonneg (κ : LocalKernelClass) (C4 : ℝ) (Cs Cd : ENNReal) : 0 ≤ shortBlockConst κ C4 Cs Cd

theorem TrilinearHT.Auto.ShortBlockTree.core_rhs_le (κ : LocalKernelClass) (C4 : ℝ) {Cs Cd : ENNReal} (hs : Cs ≠ ⊤) (hd : Cd ≠ ⊤) {q : ℝ} (hq : 2 < q) (K : ℕ) {CN L : ℝ} (hCN : 0 ≤ CN) (hL : 0 ≤ L) : ↑(numLevels (Nat.log 2 (K + 1) + 1)) * (coreX1 κ C4 * ENNReal.ofReal L + coreX2 κ C4 * (ENNReal.ofReal (↑K + 2))⁻¹ * (↑K * ENNReal.ofReal L) + ENNReal.ofReal CN * coreX3 κ C4 Cs Cd * ENNReal.ofReal (↑K + 2) ^ ((pStar q - 2) / pStar q) * (ENNReal.ofReal L ^ (1 / pReg q)) ^ 2 * ↑(2 ^ (Nat.log 2 (K + 1) + 1)) ^ (1 - 2 / pStar q) * ENNReal.ofReal L ^ (2 / pStar q)) ≤ ENNReal.ofReal (shortBlockConst κ C4 Cs Cd * (1 + CN) * (1 + Real.log (↑K + 2)) * (↑K + 2) ^ (2 * (q - 2) / (q - 1)) * L)

The numerical form of the core bound.

theorem TrilinearHT.Auto.short_block_comparison (κ : LocalKernelClass) {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) {C4 : ℝ} (hC4 : 0 ≤ C4) : ∃ (Cq : ℝ), 0 ≤ Cq ∧ ∀ (G : RealDyadicGrid) (K Nd : ℕ) (d₀ : ℤ) (T : ShortBlockTree G K) {E : Type u_1} [inst : NormedAddCommGroup E] (z : Fin 4 → ℝ → E), (∀ (j : Fin 4), Measurable fun (y : ℝ) => ‖z j y‖) → ∀ (s : Fin 4 → ℝ), (∀ (j : Fin 4), 0 ≤ s j) → (∀ (j : Fin 4), ∀ L ∈ T.leaves, ∫⁻ (y : ℝ) in dyadicGridCell G L.1 L.2, ‖z j y‖ₑ ^ 2 ≤ ENNReal.ofReal (s j ^ 2 * dyadicGridLength G L.1)) → ∀ {Ω : Type u_2} [inst_1 : MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (zσ : Fin 4 → Ω → ℝ → ℂ), (∀ (j : Fin 4), Measurable (Function.uncurry (zσ j))) → (∀ (j : Fin 4) (y : ℝ), (∫⁻ (σ : Ω), ‖zσ j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ‖z j y‖ₑ) → ∀ (kernel : ℤ × ℤ → ℝ × ℝ → ℂ), (∀ I ∈ T.internal, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (kernel I)) → ∀ cells ⊆ T.internal, (∀ I ∈ cells, d₀ ≤ I.1 ∧ I.1 < d₀ + ↑Nd) → ∀ (ε : ℤ × ℤ → Ω → ℂ), (∀ (I : ℤ × ℤ), Measurable (ε I)) → (∀ (I : ℤ × ℤ) (σ : Ω), ‖ε I σ‖ ≤ 1) → ∫⁻ (σ : Ω), ‖∑ I ∈ cells, ↑(dyadicGridLength G I.1) * ε I σ * localProgressionForm (dyadicGridLength G I.1) (kernel I) fun (j : Fin 4) => zσ j σ‖ₑ ∂P ≤ ENNReal.ofReal (Cq * (1 + finiteDepthConstant κ q Nd) * (1 + Real.log (↑K + 2)) * (↑K + 2) ^ (2 * (q - 2) / (q - 1)) * dyadicGridLength G T.root.1 * ∏ j : Fin 4, s j)

Lemma lem:shortblock (blueprint lines 2276-2283, eq:shortblock). Let a finite dyadic tree piece have root R, internal summation cells in at most K consecutive depths, lying in the original N-depth range [d₀, d₀ + N), and leaves in that block or one depth below. Suppose deterministic inputs z_j satisfy ‖z_j‖_{2,L} ≤ s_j on every leaf, and the scalar randomizations satisfy (E_σ|z_j^σ(y)|⁴)^{1/4} ≤ C₄ ‖z_j(y)‖ (the finite moment used). Then for arbitrary measurable |ε_I(σ)| ≤ 1 and any subcollection of internal cells, E_σ |Σ_I |I| ε_I(σ) H_I(z^σ)| ≤ C_q (1 + C_N) (1 + log(K+2)) (K+2)^{2(q-2)/(q-1)} |R| Π_j s_j, with C_q depending only on the kernel class, q ∈ (2, 3) and C₄.

theorem TrilinearHT.Auto.short_block_comparison_nz (κ : LocalKernelClass) {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) {C4 : ℝ} (hC4 : 0 ≤ C4) : ∃ (Cq : ℝ), 0 ≤ Cq ∧ ∀ (G : RealDyadicGrid) (K Nd : ℕ) (d₀ : ℤ) (T : ShortBlockTree G K) {E : Type u_1} [inst : NormedAddCommGroup E] (z : Fin 4 → ℝ → E), (∀ (j : Fin 4), Measurable fun (y : ℝ) => ‖z j y‖) → ∀ (s : Fin 4 → ℝ), (∀ (j : Fin 4), 0 ≤ s j) → (∀ (j : Fin 4), ∀ L ∈ T.leaves, ∫⁻ (y : ℝ) in dyadicGridCell G L.1 L.2, ‖z j y‖ₑ ^ 2 ≤ ENNReal.ofReal (s j ^ 2 * dyadicGridLength G L.1)) → ∀ {Ω : Type u_2} [inst_1 : MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (zσ : Fin 4 → Ω → ℝ → ℂ), (∀ (j : Fin 4), Measurable (Function.uncurry (zσ j))) → (∀ (j : Fin 4) (y : ℝ), (∫⁻ (σ : Ω), ‖zσ j σ y‖ₑ ^ 4 ∂P) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ‖z j y‖ₑ) → ∀ (kernel : ℤ × ℤ → ℝ × ℝ → ℂ), (∀ I ∈ T.internal, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (kernel I)) → ∀ cells ⊆ T.internal, (∀ I ∈ cells, kernel I ≠ 0 → d₀ ≤ I.1 ∧ I.1 < d₀ + ↑Nd) → ∀ (ε : ℤ × ℤ → Ω → ℂ), (∀ (I : ℤ × ℤ), Measurable (ε I)) → (∀ (I : ℤ × ℤ) (σ : Ω), ‖ε I σ‖ ≤ 1) → ∫⁻ (σ : Ω), ‖∑ I ∈ cells, ↑(dyadicGridLength G I.1) * ε I σ * localProgressionForm (dyadicGridLength G I.1) (kernel I) fun (j : Fin 4) => zσ j σ‖ₑ ∂P ≤ ENNReal.ofReal (Cq * (1 + finiteDepthConstant κ q Nd) * (1 + Real.log (↑K + 2)) * (↑K + 2) ^ (2 * (q - 2) / (q - 1)) * dyadicGridLength G T.root.1 * ∏ j : Fin 4, s j)

lem:shortblock with the depth window imposed only on the summation cells of nonzero kernel: cells with zero kernel contribute nothing (blueprint line 2836, the used cells of the original N depths).

Leaves of a complete search

The localized sum of an attempt (blueprint prop:localize, line 1856)

Far bands: the complement band above the helper band (blueprint lines 2254-2256)

Structure of the transfer steps of a chain pair (blueprint line 2241)

One far band term of a transfer step (blueprint lines 2253-2258)

Sources of the remaining other complement of a transfer step (blueprint line 2254)

The far band terms of one concrete transfer step (blueprint lines 2253-2258)

The far defects of one chain pair (blueprint lines 2253-2258)