Section 14.2, part 2a: lem:shortblock, rectangles, sampling, fourth moment

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 2a: lem:shortblock: rectangles, sampling, fourth moment (lines 2274-2317) of blueprint/formalization_blueprint.tex.

Comparison on a short depth block (lem:shortblock, blueprint lines 2275-2369)

theorem TrilinearHT.Auto.pair_eq_of_sum_sq {m₁ m₂ m₃ m₄ : ℤ} (hs : m₁ + m₂ = m₃ + m₄) (hq : m₁ ^ 2 + m₂ ^ 2 = m₃ ^ 2 + m₄ ^ 2) : m₃ = m₁ ∧ m₄ = m₂ ∨ m₃ = m₂ ∧ m₄ = m₁

Two integer pairs with the same sum and the same sum of squares agree as multisets.

theorem TrilinearHT.Auto.fourth_moment_pairing (s : Finset ℤ) (a : ℤ → ℂ) : ‖∑ m₁ ∈ s, ∑ m₂ ∈ s, ∑ m₃ ∈ s, ∑ m₄ ∈ s, if m₁ + m₂ = m₃ + m₄ ∧ m₁ ^ 2 + m₂ ^ 2 = m₃ ^ 2 + m₄ ^ 2 then a m₁ * a m₂ * (starRingEnd ℂ) (a m₃) * (starRingEnd ℂ) (a m₄) else 0‖ ≤ 2 * (∑ m ∈ s, ‖a m‖ ^ 2) ^ 2

Blueprint eq:fourth-moment (lines 2311-2315), the pairing count: the sum of a(m₁) a(m₂) conj a(m₃) conj a(m₄) over quadruples with equal sums and equal squared sums (what survives integration in w and in γ) is at most 2 (Σ |a|²)².

Leaf-depth rectangles (lem:shortblock, blueprint lines 2290-2296)

inductive TrilinearHT.Auto.DepthRect : Type

The rectangles partitioning four-tuples of leaf depths in the proof of lem:shortblock: rep S v (the minimum v is attained exactly on the slots S, at least two of them) and uniq a S h k (the minimum is attained only at a; at scale 2^(h+1) the depths of slot a and of the slots S share the block k, with a in the lower and S in the upper half; all other slots lie above that block).

• rep (S : Finset (Fin 4)) (v : ℕ) : DepthRect
• uniq (a : Fin 4) (S : Finset (Fin 4)) (h k : ℕ) : DepthRect

def TrilinearHT.Auto.instDecidableEqDepthRect.decEq (x✝ x✝¹ : DepthRect) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• TrilinearHT.Auto.instDecidableEqDepthRect.decEq (TrilinearHT.Auto.DepthRect.rep S v) (TrilinearHT.Auto.DepthRect.uniq a S_1 h k) = isFalse ⋯
• TrilinearHT.Auto.instDecidableEqDepthRect.decEq (TrilinearHT.Auto.DepthRect.uniq a S h k) (TrilinearHT.Auto.DepthRect.rep S_1 v) = isFalse ⋯

@[instance_reducible]

instance TrilinearHT.Auto.instDecidableEqDepthRect : DecidableEq DepthRect

Equations

• TrilinearHT.Auto.instDecidableEqDepthRect = TrilinearHT.Auto.instDecidableEqDepthRect.decEq

def TrilinearHT.Auto.DepthRect.Valid : DepthRect → Prop

Admissible rectangle parameters.

Equations

• (TrilinearHT.Auto.DepthRect.rep S v).Valid = (2 ≤ S.card)
• (TrilinearHT.Auto.DepthRect.uniq a S h k).Valid = (a ∉ S ∧ S.Nonempty)

def TrilinearHT.Auto.DepthRect.Mem : DepthRect → (Fin 4 → ℕ) → Prop

Membership of a depth tuple; it is a product of per-slot conditions.

Equations

• (TrilinearHT.Auto.DepthRect.rep S v).Mem x✝ = ∀ (j : Fin 4), (j ∈ S → x✝ j = v) ∧ (j ∉ S → v < x✝ j)
• (TrilinearHT.Auto.DepthRect.uniq a S h k).Mem x✝ = (x✝ a / 2 ^ h = 2 * k ∧ ∀ (j : Fin 4), j ≠ a → (j ∈ S → x✝ j / 2 ^ h = 2 * k + 1) ∧ (j ∉ S → 2 * k + 2 ≤ x✝ j / 2 ^ h))

def TrilinearHT.Auto.DepthRect.sep : DepthRect → ℕ

The separating depth t: all slots except possibly the heavy slot have depth at least t.

Equations

• (TrilinearHT.Auto.DepthRect.rep S v).sep = v
• (TrilinearHT.Auto.DepthRect.uniq a S h k).sep = (2 * k + 1) * 2 ^ h

theorem TrilinearHT.Auto.DepthRect.div_pow_succ (x h : ℕ) : x / 2 ^ (h + 1) = x / 2 ^ h / 2

theorem TrilinearHT.Auto.DepthRect.div_pow_eq_of_le {x y h h' : ℕ} (hh : h ≤ h') (e : x / 2 ^ h = y / 2 ^ h) : x / 2 ^ h' = y / 2 ^ h'

Agreement of the dyadic blocks persists at coarser scales.

theorem TrilinearHT.Auto.DepthRect.uniq_lt {a : Fin 4} {S : Finset (Fin 4)} {h k : ℕ} {d : Fin 4 → ℕ} (hm : (uniq a S h k).Mem d) {j : Fin 4} (hj : j ≠ a) : d a < d j

In a uniq rectangle the heavy slot is the strict minimum.

theorem TrilinearHT.Auto.DepthRect.exists_mem (d : Fin 4 → ℕ) : ∃ (R : DepthRect), R.Valid ∧ R.Mem d

Every tuple lies in a valid rectangle.

theorem TrilinearHT.Auto.DepthRect.existsUnique_mem (d : Fin 4 → ℕ) : ∃! R : DepthRect, R.Valid ∧ R.Mem d

The rectangles partition the depth tuples: a tuple lies in exactly one valid rectangle.

theorem TrilinearHT.Auto.DepthRect.uniq_bounds {a : Fin 4} {S : Finset (Fin 4)} {h k m : ℕ} {d : Fin 4 → ℕ} (hv : (uniq a S h k).Valid) (hm : (uniq a S h k).Mem d) (hd : ∀ (j : Fin 4), d j < 2 ^ m) : h < m ∧ k < 2 ^ (m - h - 1)

Positions at a level: for depths below 2^m, a uniq rectangle has h < m and k < 2^(m-h-1); a rep rectangle has v < 2^m.

Kernel sampling on the δ-lattice (lem:shortblock, blueprint lines 2298-2312)

noncomputable def TrilinearHT.Auto.admissibleLipConst (κ : LocalKernelClass) : ℝ

The first-order derivative constant of an admissible class.

Equations

• TrilinearHT.Auto.admissibleLipConst κ = (κ.derivativeConstant * (↑1 + 2)) ^ (κ.derivativeConstant * (↑1 + 2))

theorem TrilinearHT.Auto.admissibleLipConst_nonneg (κ : LocalKernelClass) : 0 ≤ admissibleLipConst κ

theorem TrilinearHT.Auto.admissible_kernel_lipschitz {κ : LocalKernelClass} {a r : ℝ} {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a r w) (z z' : ℝ × ℝ) : ‖w z - w z'‖ ≤ admissibleLipConst κ * r⁻¹ * (|z.1 - z'.1| + |z.2 - z'.2|)

An admissible kernel on a cell of length r is Lipschitz with constant C_κ / r in each variable.

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

The kernel sampled on the δ-lattice: with y₀ = x = δ(n₀ + u) and y₁ = x + t = δ(n₁ + v), its value is w(δ n₀, δ(n₁ - n₀)) (blueprint line 2307).

Equations

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

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

theorem TrilinearHT.Auto.latticeSampled_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 - latticeSampledKernel δ w z) f‖ₑ ≤ ENNReal.ofReal (4 * admissibleLipConst κ * (δ / r)) * ∏ i : Fin 4, MeasureTheory.eLpNorm (f i) (p i) (normalizedIntervalMeasure a r)

Blueprint lines 2307-2312 (first kernel-sampling error): for an admissible kernel on a cell of length r and 5δ ≤ μ r, the form with the sampling error kernel w - w^δ is at most 4 C_κ (δ / r) times the product of normalized local norms, at every exponent tuple allowed by eq:absolute.

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

The δ-lattice cell of the integer point n ∈ ℤ².

Equations

• TrilinearHT.Auto.latticeCell δ n = Set.Ico (δ * ↑n.1) (δ * (↑n.1 + 1)) ×ˢ Set.Ico (δ * ↑n.2) (δ * (↑n.2 + 1))

theorem TrilinearHT.Auto.mem_latticeCell_iff {δ : ℝ} (hδ : 0 < δ) (n : ℤ × ℤ) (z : ℝ × ℝ) : z ∈ latticeCell δ n ↔ ⌊z.1 / δ⌋ = n.1 ∧ ⌊z.2 / δ⌋ = n.2

theorem TrilinearHT.Auto.lattice_integral_decomposition {G : ℝ × ℝ → ℂ} (hG : MeasureTheory.Integrable G MeasureTheory.volume) {δ : ℝ} (hδ : 0 < δ) : ∫ (z : ℝ × ℝ), G z = ↑(δ ^ 2) * ∑' (n : ℤ × ℤ), ∫ (u : ℝ × ℝ) in Set.Ico 0 1 ×ˢ Set.Ico 0 1, G (δ * (↑n.1 + u.1), δ * (↑n.2 + u.2))

Blueprint lines 2298-2305 (substitution y = δ(n + u)): an integrable function on ℝ² is the δ²-weighted sum over n ∈ ℤ² of its integrals over the unit fast cell.

The fast multipliers and the fourth moment (lem:shortblock, blueprint lines 2314-2326)

noncomputable def TrilinearHT.Auto.ePhase (x : ℝ) : ℂ

The additive character e(x) = exp(2πix) of a real phase.

Equations

• TrilinearHT.Auto.ePhase x = Complex.exp (2 * ↑Real.pi * Complex.I * ↑x)

theorem TrilinearHT.Auto.ePhase_add (x y : ℝ) : ePhase x * ePhase y = ePhase (x + y)

theorem TrilinearHT.Auto.ePhase_conj (x : ℝ) : (starRingEnd ℂ) (ePhase x) = ePhase (-x)

theorem TrilinearHT.Auto.norm_ePhase (x : ℝ) : ‖ePhase x‖ = 1

theorem TrilinearHT.Auto.continuous_ePhase : Continuous ePhase

theorem TrilinearHT.Auto.integral_ePhase_int (k : ℤ) {L : ℝ} (hL : 0 < L) : ∫ (x : ℝ) in 0..L, ePhase (↑k * x / L) = if k = 0 then ↑L else 0

∫₀ᴸ e(k x / L) dx = L [k = 0] for an integer frequency k.

noncomputable def TrilinearHT.Auto.fastMultiplied (s : Finset ℤ) (a : ℤ → ℂ) (c : ℤ) (γ w : ℝ) : ℂ

The fast trigonometric polynomial Σ_m a_m e(γ m²/c + m w/16) on the circle of length 16 after the multiplier e(γ m²/c) (blueprint line 2316).

Equations

• TrilinearHT.Auto.fastMultiplied s a c γ w = ∑ m ∈ s, a m * TrilinearHT.Auto.ePhase (γ * ↑m ^ 2 / ↑c + ↑m * w / 16)

theorem TrilinearHT.Auto.fastMultiplied_norm_pow_four (s : Finset ℤ) (a : ℤ → ℂ) (c : ℤ) (γ w : ℝ) : ↑(‖fastMultiplied s a c γ w‖ ^ 4) = ∑ m₁ ∈ s, ∑ m₂ ∈ s, ∑ m₃ ∈ s, ∑ m₄ ∈ s, a m₁ * a m₂ * (starRingEnd ℂ) (a m₃) * (starRingEnd ℂ) (a m₄) * (ePhase (γ * (↑m₁ ^ 2 + ↑m₂ ^ 2 - ↑m₃ ^ 2 - ↑m₄ ^ 2) / ↑c) * ePhase (↑(m₁ + m₂ - m₃ - m₄) * w / 16))

The fourth power expanded into the quadruple sum.

theorem TrilinearHT.Auto.intervalIntegral_quad_sum {x₀ x₁ : ℝ} (s : Finset ℤ) (F : ℤ → ℤ → ℤ → ℤ → ℝ → ℂ) (hF : ∀ (i j k l : ℤ), Continuous (F i j k l)) : ∫ (x : ℝ) in x₀..x₁, ∑ i ∈ s, ∑ j ∈ s, ∑ k ∈ s, ∑ l ∈ s, F i j k l x = ∑ i ∈ s, ∑ j ∈ s, ∑ k ∈ s, ∑ l ∈ s, ∫ (x : ℝ) in x₀..x₁, F i j k l x

Interval integrals commute with quadruple finite sums of continuous functions.

theorem TrilinearHT.Auto.fast_fourth_moment (s : Finset ℤ) (a : ℤ → ℂ) {c : ℤ} (hc0 : c ≠ 0) (hc : c ∣ 3) : 1 / 3 * ∫ (γ : ℝ) in 0..3, 1 / 16 * ∫ (w : ℝ) in 0..16, ‖fastMultiplied s a c γ w‖ ^ 4 ≤ 2 * (∑ m ∈ s, ‖a m‖ ^ 2) ^ 2

Blueprint eq:fourth-moment (lines 2318-2322) for finite Fourier sums: when c ∣ 3, the average over γ ∈ ℝ/3ℤ of the normalized L⁴ norm on the circle of length 16 satisfies E_γ ∫ |U_γ F|⁴ ≤ 2 (Σ |a_m|²)² = 2 ‖F‖₂⁴.

def TrilinearHT.Auto.fastSlotC : Fin 4 → ℤ

The fast multiplier coefficients c = (-1, 3, -3, 1) (blueprint line 2314).

Equations

• TrilinearHT.Auto.fastSlotC = ![-1, 3, -3, 1]

theorem TrilinearHT.Auto.ePhase_prod_four (x : Fin 4 → ℝ) : ∏ j : Fin 4, ePhase (x j) = ePhase (∑ j : Fin 4, x j)

theorem TrilinearHT.Auto.ePhase_zero : ePhase 0 = 1

theorem TrilinearHT.Auto.fast_quadratic_invariance_real (m : Fin 4 → ℝ) (h0 : m 0 + m 1 + m 2 + m 3 = 0) (h1 : m 1 + 2 * m 2 + 3 * m 3 = 0) : ∑ j : Fin 4, m j ^ 2 / ↑(fastSlotC j) = 0

fast_form_quadratic_invariance over ℝ.

theorem TrilinearHT.Auto.fast_slots_product (s : Finset ℤ) (a : Fin 4 → ℤ → ℂ) (γ u v : ℝ) : ∏ j : Fin 4, fastMultiplied s (a j) (fastSlotC j) γ ((1 - ↑↑j) * u + ↑↑j * v) = ∑ p ∈ Fintype.piFinset fun (x : Fin 4) => s, (∏ j : Fin 4, a j (p j)) * (ePhase (γ * ∑ j : Fin 4, ↑(p j) ^ 2 / ↑(fastSlotC j)) * ePhase ((↑(∑ j : Fin 4, (1 - ↑↑j) * p j) * u + ↑(∑ j : Fin 4, ↑↑j * p j) * v) / 16))

The product of the four multiplied slots on the progression w_j = (1-j)u + jv, expanded over frequency tuples.

theorem TrilinearHT.Auto.double_integral_ePhase (A B : ℤ) : ∫ (u : ℝ) (v : ℝ) in 0..16, ePhase ((↑A * u + ↑B * v) / 16) = if A = 0 ∧ B = 0 then 256 else 0

∫₀¹⁶ ∫₀¹⁶ e((A u + B v)/16) dv du = 16² [A = 0][B = 0].

theorem TrilinearHT.Auto.fast_form_eval (s : Finset ℤ) (a : Fin 4 → ℤ → ℂ) (γ : ℝ) : ∫ (u : ℝ) (v : ℝ) in 0..16, ∏ j : Fin 4, fastMultiplied s (a j) (fastSlotC j) γ ((1 - ↑↑j) * u + ↑↑j * v) = 256 * ∑ p ∈ Fintype.piFinset fun (x : Fin 4) => s, if ∑ j : Fin 4, (1 - ↑↑j) * p j = 0 ∧ ∑ j : Fin 4, ↑↑j * p j = 0 then ∏ j : Fin 4, a j (p j) else 0

Blueprint lines 2314-2317: the fast form of the multiplied slots does not depend on γ: its Fourier support has Σ m_j = Σ j m_j = 0, hence Σ m_j² / c_j = 0. The form equals 16² Σ_{Σ m_j = Σ j m_j = 0} Π_j a_j(m_j).

theorem TrilinearHT.Auto.fast_form_invariance (s : Finset ℤ) (a : Fin 4 → ℤ → ℂ) (γ : ℝ) : ∫ (u : ℝ) (v : ℝ) in 0..16, ∏ j : Fin 4, fastMultiplied s (a j) (fastSlotC j) γ ((1 - ↑↑j) * u + ↑↑j * v) = ∫ (u : ℝ) (v : ℝ) in 0..16, ∏ j : Fin 4, fastMultiplied s (a j) (fastSlotC j) 0 ((1 - ↑↑j) * u + ↑↑j * v)

Blueprint lines 2314-2317: the multipliers U_{j,γ} leave the fast form unchanged.

theorem TrilinearHT.Auto.latticeSampled_form_lift {w : ℝ × ℝ → ℂ} {δ : ℝ} (hδ : 0 < δ) (f : Fin 4 → ℝ → ℂ) (hF : MeasureTheory.Integrable (fun (z : ℝ × ℝ) => latticeSampledKernel δ w z * ∏ j : Fin 4, f j (realProgressionCoordinate j z)) MeasureTheory.volume) : ∫ (z : ℝ × ℝ), latticeSampledKernel δ w z * ∏ j : Fin 4, f j (realProgressionCoordinate j z) = ↑(δ ^ 2) * ∑' (n : ℤ × ℤ), w (δ * ↑n.1, δ * ↑n.2 - δ * ↑n.1) * ∫ (u : ℝ × ℝ) in Set.Ico 0 1 ×ˢ Set.Ico 0 1, ∏ j : Fin 4, f j (δ * ((1 - ↑↑j) * ↑n.1 + ↑↑j * ↑n.2 + ((1 - ↑↑j) * u.1 + ↑↑j * u.2)))

Blueprint lines 2302-2307 (lift to the fast variables): with y₀ = x = δ(n₀ + u) and y₁ = x + t = δ(n₁ + v), the form with the lattice-sampled kernel is the δ²-weighted sum over n ∈ ℤ² of w(δ n₀, δ(n₁ - n₀)) times the fast integral over the unit cell of the inputs at δ(n_j + w_j), n_j = (1-j)n₀ + j n₁, w_j = (1-j)u + j v.

Window masses (lem:shortblock, blueprint lines 2328-2332)

def TrilinearHT.Auto.leafInterval {ι : Type u_1} (aL lL : ι → ℝ) (i : ι) : Set ℝ

The leaf interval [a_i, a_i + l_i).

Equations

• TrilinearHT.Auto.leafInterval aL lL i = Set.Ico (aL i) (aL i + lL i)

def TrilinearHT.Auto.leafUnion {ι : Type u_1} (S : Finset ι) (aL lL : ι → ℝ) : Set ℝ

The selected leaf union E = ⋃_{i ∈ S} L_i.

Equations

• TrilinearHT.Auto.leafUnion S aL lL = ⋃ i ∈ S, TrilinearHT.Auto.leafInterval aL lL i

theorem TrilinearHT.Auto.leaf_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)) (W : Set ℝ) : ∫⁻ (x : ℝ) in W ∩ leafUnion S aL lL, ‖z x‖ₑ ^ 2 ≤ MeasureTheory.volume (⋃ i ∈ {i ∈ S | (W ∩ leafInterval aL lL i).Nonempty}, leafInterval aL lL i)

The mass of z on the leaves meeting a set W is at most the total length of those leaves.

The mixed lattice-torus absolute estimate (lem:shortblock, blueprint lines 2307-2340)

@[reducible, inline]

abbrev TrilinearHT.Auto.FastCircle : Type

The fast circle T₀ = ℝ / 16ℤ of blueprint line 2303.

Equations

• TrilinearHT.Auto.FastCircle = AddCircle 16

instance TrilinearHT.Auto.instFactLtRealOfNat_leanPool_1 : Fact (0 < 16)

@[reducible, inline]

noncomputable abbrev TrilinearHT.Auto.fastHaar : MeasureTheory.Measure FastCircle

Normalized Haar measure on the fast circle.

Equations

• TrilinearHT.Auto.fastHaar = AddCircle.haarAddCircle

def TrilinearHT.Auto.fastCoord (j : ℤ) : FastCircle × FastCircle →+ FastCircle

The progression coordinate w_j = (1 - j) u + j v as a homomorphism T₀² → T₀.

Equations

• TrilinearHT.Auto.fastCoord j = { toFun := fun (x : TrilinearHT.Auto.FastCircle × TrilinearHT.Auto.FastCircle) => (1 - j) • x.1 + j • x.2, map_zero' := ⋯, map_add' := ⋯ }

theorem TrilinearHT.Auto.continuous_fastCoord (j : ℤ) : Continuous ⇑(fastCoord j)

theorem TrilinearHT.Auto.fastCoord_surjective (j : ℤ) : Function.Surjective ⇑(fastCoord j)

def TrilinearHT.Auto.fastPair (i j : ℤ) : FastCircle × FastCircle →+ FastCircle × FastCircle

Two distinct progression coordinates (w_i, w_j) as a homomorphism T₀² → T₀².

Equations

• TrilinearHT.Auto.fastPair i j = (TrilinearHT.Auto.fastCoord i).prod (TrilinearHT.Auto.fastCoord j)

theorem TrilinearHT.Auto.fastPair_surjective {i j : ℤ} (hij : i ≠ j) : Function.Surjective ⇑(fastPair i j)

instance TrilinearHT.Auto.instIsProbabilityMeasureProdFastCircleProdFastHaar : MeasureTheory.IsProbabilityMeasure (fastHaar.prod fastHaar)

theorem TrilinearHT.Auto.map_fastCoord {j : ℤ} : MeasureTheory.Measure.map (⇑(fastCoord j)) (fastHaar.prod fastHaar) = fastHaar

theorem TrilinearHT.Auto.map_fastPair {i j : ℤ} (hij : i ≠ j) : MeasureTheory.Measure.map (⇑(fastPair i j)) (fastHaar.prod fastHaar) = fastHaar.prod fastHaar

theorem TrilinearHT.Auto.lintegral_fastCoord (j : ℤ) {f : FastCircle → ENNReal} (hf : Measurable f) : ∫⁻ (x : FastCircle × FastCircle), f ((fastCoord j) x) ∂fastHaar.prod fastHaar = ∫⁻ (t : FastCircle), f t ∂fastHaar

The single progression coordinate pushes Haar measure on T₀² to Haar measure on T₀.

theorem TrilinearHT.Auto.lintegral_fastPair {i j : ℤ} (hij : i ≠ j) {f g : FastCircle → ENNReal} (hf : Measurable f) (hg : Measurable g) : ∫⁻ (x : FastCircle × FastCircle), f ((fastCoord i) x) * g ((fastCoord j) x) ∂fastHaar.prod fastHaar = (∫⁻ (t : FastCircle), f t ∂fastHaar) * ∫⁻ (t : FastCircle), g t ∂fastHaar

Blueprint line 394 (torus pair endpoint): two distinct progression coordinates are independent: ∫∫ f(w_i) g(w_j) = ∫ f ∫ g.

def TrilinearHT.Auto.latticeCoord (j : ℤ) (n : ℤ × ℤ) : ℤ

The slow progression coordinate n_j = (1 - j) n₀ + j n₁.

Equations

• TrilinearHT.Auto.latticeCoord j n = (1 - j) * n.1 + j * n.2

theorem TrilinearHT.Auto.latticeCoord_pair_injective {i j : ℤ} (hij : i ≠ j) : Function.Injective fun (n : ℤ × ℤ) => (latticeCoord i n, latticeCoord j n)

noncomputable def TrilinearHT.Auto.latticeTorusMeasure (B : Finset (ℤ × ℤ)) (ε : ENNReal) : MeasureTheory.Measure ((ℤ × ℤ) × FastCircle × FastCircle)

The mixed measure: weight ε² on the slow pairs in B, normalized Haar measure on T₀².

Equations

• TrilinearHT.Auto.latticeTorusMeasure B ε = (∑ n ∈ B, ε ^ 2 • MeasureTheory.Measure.dirac n).prod (TrilinearHT.Auto.fastHaar.prod TrilinearHT.Auto.fastHaar)

noncomputable def TrilinearHT.Auto.latticeCircleMeasure (ε : ENNReal) : MeasureTheory.Measure (ℤ × FastCircle)

The target measure: weight ε on each slow point, normalized Haar measure on T₀.

Equations

• TrilinearHT.Auto.latticeCircleMeasure ε = (ε • MeasureTheory.Measure.count).prod TrilinearHT.Auto.fastHaar

def TrilinearHT.Auto.latticeTorusProj (j : ℤ) (x : (ℤ × ℤ) × FastCircle × FastCircle) : ℤ × FastCircle

The progression map (n, u, v) ↦ (n_j, w_j).

Equations

• TrilinearHT.Auto.latticeTorusProj j x = (TrilinearHT.Auto.latticeCoord j x.1, (TrilinearHT.Auto.fastCoord j) x.2)

theorem TrilinearHT.Auto.measurable_latticeTorusProj (j : ℤ) : Measurable (latticeTorusProj j)

theorem TrilinearHT.Auto.lintegral_latticeTorusMeasure (B : Finset (ℤ × ℤ)) (ε : ENNReal) {F : (ℤ × ℤ) × FastCircle × FastCircle → ENNReal} (hF : Measurable F) : ∫⁻ (x : (ℤ × ℤ) × FastCircle × FastCircle), F x ∂latticeTorusMeasure B ε = ∑ n ∈ B, ε ^ 2 * ∫⁻ (w : FastCircle × FastCircle), F (n, w) ∂fastHaar.prod fastHaar

theorem TrilinearHT.Auto.lintegral_latticeCircleMeasure (ε : ENNReal) {f : ℤ × FastCircle → ENNReal} (hf : Measurable f) : ∫⁻ (y : ℤ × FastCircle), f y ∂latticeCircleMeasure ε = ε * ∑' (m : ℤ), ∫⁻ (t : FastCircle), f (m, t) ∂fastHaar

theorem TrilinearHT.Auto.latticeTorus_empty (B : Finset (ℤ × ℤ)) {ε C : ENNReal} (hB : ε ^ 2 * ↑B.card ≤ C) : (latticeTorusMeasure B ε) Set.univ ≤ C

Total mass of the mixed lattice-torus measure.

theorem TrilinearHT.Auto.latticeTorus_single (B : Finset (ℤ × ℤ)) {ε M C : ENNReal} (hM : ε * M ≤ C) (hfib : ∀ (j : Fin 4) (m : ℤ), ↑{n ∈ B | latticeCoord (↑↑j) n = m}.card ≤ M) (i : Fin 4) (g : ℤ × FastCircle → ENNReal) (hg : Measurable g) : ∫⁻ (x : (ℤ × ℤ) × FastCircle × FastCircle), g (latticeTorusProj (↑↑i) x) ∂latticeTorusMeasure B ε ≤ C * ∫⁻ (y : ℤ × FastCircle), g y ∂latticeCircleMeasure ε

The single-coordinate endpoint of the mixed absolute estimate.

theorem TrilinearHT.Auto.latticeTorus_pair (B : Finset (ℤ × ℤ)) {ε C : ENNReal} (hC1 : 1 ≤ C) (i j : Fin 4) (hij : i ≠ j) (g h : ℤ × FastCircle → ENNReal) (hg : Measurable g) (hh : Measurable h) : ∫⁻ (x : (ℤ × ℤ) × FastCircle × FastCircle), g (latticeTorusProj (↑↑i) x) * h (latticeTorusProj (↑↑j) x) ∂latticeTorusMeasure B ε ≤ (C * ∫⁻ (y : ℤ × FastCircle), g y ∂latticeCircleMeasure ε) * ∫⁻ (y : ℤ × FastCircle), h y ∂latticeCircleMeasure ε

The pair endpoint of the mixed absolute estimate.

theorem TrilinearHT.Auto.latticeTorus_eLpNorm_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) (f : Fin 4 → ℤ × FastCircle → ENNReal) (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) : ∫⁻ (x : (ℤ × ℤ) × FastCircle × FastCircle), ∏ i : Fin 4, f i (latticeTorusProj (↑↑i) x) ∂latticeTorusMeasure B ε ≤ C * ∏ i : Fin 4, MeasureTheory.eLpNorm (f i) (p i) (latticeCircleMeasure ε)

eq:absolute on local counting measure times Haar measure, in normed form: for exponents p_j ≥ 1 with Σ 1/p_j ≤ 2, the positive form is at most C Π_j ‖f_j‖_{L^{p_j}}.

noncomputable def TrilinearHT.Auto.gammaMeasure : MeasureTheory.Measure ℝ

The uniform probability on γ ∈ [0, 3) (blueprint line 2316, γ ∈ ℝ/3ℤ).

Equations

• TrilinearHT.Auto.gammaMeasure = ENNReal.ofReal (1 / 3) • MeasureTheory.volume.restrict (Set.Ioc 0 3)

instance TrilinearHT.Auto.instIsProbabilityMeasureRealGammaMeasure : MeasureTheory.IsProbabilityMeasure gammaMeasure

noncomputable def TrilinearHT.Auto.fastMass {Ω : Type u_1} (s : Finset ℤ) (A : Ω → ℤ → ℤ → ℂ) (ω : Ω) (m : ℤ) : ℝ

The squared window mass e(ω, m)² = Σ_k |A(ω, m, k)|².

Equations

• TrilinearHT.Auto.fastMass s A ω m = ∑ k ∈ s, ‖A ω m k‖ ^ 2

instance TrilinearHT.Auto.instSFiniteProdIntFastCircleLatticeCircleMeasure (ε : ENNReal) : MeasureTheory.SFinite (latticeCircleMeasure ε)

theorem TrilinearHT.Auto.fastSlotC_ne_zero (j : Fin 4) : fastSlotC j ≠ 0

theorem TrilinearHT.Auto.fastSlotC_dvd (j : Fin 4) : fastSlotC j ∣ 3

Continuous comparison (lem:shortblock, blueprint lines 2345-2357)

theorem TrilinearHT.Auto.interval_centers_progression {δ c : ℝ} (hδ : 0 < δ) (hc : c < 1 / 7) (n : Fin 4 → ℤ) (z : ℝ × ℝ) (hn : ∀ (j : Fin 4), |realProgressionCoordinate j z - δ * ↑(n j)| < c * δ) (j : Fin 4) : n j = latticeCoord ↑↑j (n 0, n 1)

Blueprint lines 2347-2349: if the four intervals |y - δ n_j| < c δ with c < 1/7 meet a real progression y_j = x + j t, the integer centers form a lattice progression: n_j = (1 - j) n₀ + j n₁.

Mixed Hölder and the block factor (lem:shortblock, blueprint lines 2357-2369)

theorem TrilinearHT.Auto.lintegral_fastCoord_prod {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) (j : ℤ) {g : Ω × FastCircle → ENNReal} (hg : Measurable g) : ∫⁻ (q : Ω × FastCircle × FastCircle), g (q.1, (fastCoord j) q.2) ∂P.prod (fastHaar.prod fastHaar) = ∫⁻ (z : Ω × FastCircle), g z ∂P.prod fastHaar

The progression coordinate on the fast factor pushes P ⊗ Haar(T₀²) to P ⊗ Haar(T₀).

Fourier partial sums of the fast windows (limiting route of lem:shortblock)

theorem TrilinearHT.Auto.fast_partial_sums_tendsto (f : ↥(MeasureTheory.Lp ℂ 2 fastHaar)) : Filter.Tendsto (fun (N : ℕ) => ∑ m ∈ Finset.Icc (-↑N) ↑N, fourierCoeff (↑↑f) m • fourierLp 2 m) Filter.atTop (nhds f)

The symmetric Fourier partial sums of an L² function on the fast circle converge to it in L² (Mathlib hasSum_fourier_series_L2).

theorem TrilinearHT.Auto.fast_bessel (f : ↥(MeasureTheory.Lp ℂ 2 fastHaar)) (s : Finset ℤ) : ∑ m ∈ s, ‖fourierCoeff (↑↑f) m‖ ^ 2 ≤ ∫ (t : FastCircle), ‖↑↑f t‖ ^ 2 ∂fastHaar

Bessel's inequality for finite sets of frequencies: Σ_{m ∈ s} |f̂(m)|² ≤ ‖f‖₂².

The fast lift (lem:shortblock, blueprint lines 2302-2306)

noncomputable def TrilinearHT.Auto.fastLiftLeft (j : Fin 4) : ℝ

Left endpoints of the fast lift intervals: [0, 1) in slots 0, 1 and [-4, 4) in slots 2, 3 (blueprint line 2303: "restricted to [0,1) in slots 0,1 and to fixed lift intervals in [-4,4] containing all needed w_j in slots 2,3").

Equations

• TrilinearHT.Auto.fastLiftLeft j = if ↑j < 2 then 0 else -4

noncomputable def TrilinearHT.Auto.fastLiftLen (j : Fin 4) : ℝ

Lengths of the fast lift intervals.

Equations

• TrilinearHT.Auto.fastLiftLen j = if ↑j < 2 then 1 else 8

noncomputable def TrilinearHT.Auto.fastRep (j : Fin 4) (t : FastCircle) : ℝ

The representative of a fast point in [ℓ_j, ℓ_j + 16).

Equations

• TrilinearHT.Auto.fastRep j t = ↑((AddCircle.equivIco 16 (TrilinearHT.Auto.fastLiftLeft j)) t)

theorem TrilinearHT.Auto.measurable_fastRep (j : Fin 4) : Measurable (fastRep j)

theorem TrilinearHT.Auto.fastRep_coe {j : Fin 4} {x : ℝ} (hx : x ∈ Set.Ico (fastLiftLeft j) (fastLiftLeft j + 16)) : fastRep j ↑x = x

noncomputable def TrilinearHT.Auto.fastLift (j : Fin 4) (φ : ℝ → ℂ) (t : FastCircle) : ℂ

The lift of a function on the lift interval of slot j to the fast circle, zero elsewhere.

Equations

• TrilinearHT.Auto.fastLift j φ t = if TrilinearHT.Auto.fastRep j t < TrilinearHT.Auto.fastLiftLeft j + TrilinearHT.Auto.fastLiftLen j then φ (TrilinearHT.Auto.fastRep j t) else 0

theorem TrilinearHT.Auto.measurable_fastLift (j : Fin 4) {φ : ℝ → ℂ} (hφ : Measurable φ) : Measurable (fastLift j φ)

theorem TrilinearHT.Auto.integral_fastHaar_prod {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : FastCircle × FastCircle → E) (hh : MeasureTheory.AEStronglyMeasurable h (fastHaar.prod fastHaar)) : ∫ (x : FastCircle × FastCircle), h x ∂fastHaar.prod fastHaar = (1 / 256) • ∫ (x : ℝ × ℝ) in Set.Ico 0 16 ×ˢ Set.Ico 0 16, h (↑x.1, ↑x.2)

Normalized Haar measure on T₀² is 1/256 times Lebesgue measure on [0, 16)².

theorem TrilinearHT.Auto.fastLift_coe {j : Fin 4} (φ : ℝ → ℂ) {y : ℝ} (hy : y ∈ Set.Ico (fastLiftLeft j) (fastLiftLeft j + 16)) : fastLift j φ ↑y = if y < fastLiftLeft j + fastLiftLen j then φ y else 0

theorem TrilinearHT.Auto.fastCoord_coe (j : ℤ) (a b : ℝ) : (fastCoord j) (↑a, ↑b) = ↑((1 - ↑j) * a + ↑j * b)

theorem TrilinearHT.Auto.fast_lift_form (φ : Fin 4 → ℝ → ℂ) (hφ : ∀ (j : Fin 4), Measurable (φ j)) : ∫ (x : FastCircle × FastCircle), ∏ j : Fin 4, fastLift j (φ j) ((fastCoord ↑↑j) x) ∂fastHaar.prod fastHaar = (1 / 256) • ∫ (u : ℝ × ℝ) in Set.Ico 0 1 ×ˢ Set.Ico 0 1, ∏ j : Fin 4, φ j ((1 - ↑↑j) * u.1 + ↑↑j * u.2)

Blueprint lines 2302-2306 ("with fixed Haar constants the fast progression integral reproduces the original integral without wraparound"): lifting the slot functions to T₀ on the lift intervals, the fast progression integral over T₀² is 1/256 times the integral over the unit cell [0, 1)².

theorem TrilinearHT.Auto.fast_form_L2_le (h : Fin 4 → FastCircle → ENNReal) (hh : ∀ (j : Fin 4), Measurable (h j)) : ∫⁻ (x : FastCircle × FastCircle), ∏ j : Fin 4, h j ((fastCoord ↑↑j) x) ∂fastHaar.prod fastHaar ≤ ∏ j : Fin 4, (∫⁻ (t : FastCircle), h j t ^ 2 ∂fastHaar) ^ (1 / 2)

The all-L² case of eq:absolute on T₀² for one slow tuple: pairing the slots (0, 1) and (2, 3) and using independence of two coordinates, ∫∫ Π_j h_j(w_j) ≤ Π_j ‖h_j‖₂.

theorem TrilinearHT.Auto.enorm_prod_four (f : Fin 4 → ℂ) : ‖∏ j : Fin 4, f j‖ₑ = ∏ j : Fin 4, ‖f j‖ₑ

theorem TrilinearHT.Auto.eLpNorm_two_eq {g : FastCircle → ℂ} (hg : MeasureTheory.AEStronglyMeasurable g fastHaar) : MeasureTheory.eLpNorm g 2 fastHaar = (∫⁻ (t : FastCircle), ‖g t‖ₑ ^ 2 ∂fastHaar) ^ (1 / 2)

theorem TrilinearHT.Auto.lintegral_fast_form_le (g : Fin 4 → FastCircle → ℂ) (hg : ∀ (j : Fin 4), Measurable (g j)) : ∫⁻ (x : FastCircle × FastCircle), ∏ j : Fin 4, ‖g j ((fastCoord ↑↑j) x)‖ₑ ∂fastHaar.prod fastHaar ≤ ∏ j : Fin 4, MeasureTheory.eLpNorm (g j) 2 fastHaar

∫∫ Π_j |g_j(w_j)| ≤ Π_j ‖g_j‖₂ for complex slot functions.

theorem TrilinearHT.Auto.fast_form_integrable (g : Fin 4 → FastCircle → ℂ) (hg : ∀ (j : Fin 4), Measurable (g j)) (hL : ∀ (j : Fin 4), MeasureTheory.MemLp (g j) 2 fastHaar) : MeasureTheory.Integrable (fun (x : FastCircle × FastCircle) => ∏ j : Fin 4, g j ((fastCoord ↑↑j) x)) (fastHaar.prod fastHaar)

theorem TrilinearHT.Auto.norm_fast_form_le (g : Fin 4 → FastCircle → ℂ) (hg : ∀ (j : Fin 4), Measurable (g j)) (hL : ∀ (j : Fin 4), MeasureTheory.MemLp (g j) 2 fastHaar) : ‖∫ (x : FastCircle × FastCircle), ∏ j : Fin 4, g j ((fastCoord ↑↑j) x) ∂fastHaar.prod fastHaar‖ ≤ ∏ j : Fin 4, (MeasureTheory.eLpNorm (g j) 2 fastHaar).toReal

theorem TrilinearHT.Auto.fast_prod_four (f : Fin 4 → FastCircle → ℂ) (x : FastCircle × FastCircle) : ∏ j : Fin 4, f j ((fastCoord ↑↑j) x) = f 0 ((fastCoord 0) x) * f 1 ((fastCoord 1) x) * f 2 ((fastCoord 2) x) * f 3 ((fastCoord 3) x)

theorem TrilinearHT.Auto.fast_form_integrable4 {g0 g1 g2 g3 : FastCircle → ℂ} (m0 : Measurable g0) (m1 : Measurable g1) (m2 : Measurable g2) (m3 : Measurable g3) (l0 : MeasureTheory.MemLp g0 2 fastHaar) (l1 : MeasureTheory.MemLp g1 2 fastHaar) (l2 : MeasureTheory.MemLp g2 2 fastHaar) (l3 : MeasureTheory.MemLp g3 2 fastHaar) : MeasureTheory.Integrable (fun (x : FastCircle × FastCircle) => g0 ((fastCoord 0) x) * g1 ((fastCoord 1) x) * g2 ((fastCoord 2) x) * g3 ((fastCoord 3) x)) (fastHaar.prod fastHaar)

theorem TrilinearHT.Auto.norm_fast_form_le4 {g0 g1 g2 g3 : FastCircle → ℂ} (m0 : Measurable g0) (m1 : Measurable g1) (m2 : Measurable g2) (m3 : Measurable g3) (l0 : MeasureTheory.MemLp g0 2 fastHaar) (l1 : MeasureTheory.MemLp g1 2 fastHaar) (l2 : MeasureTheory.MemLp g2 2 fastHaar) (l3 : MeasureTheory.MemLp g3 2 fastHaar) : ‖∫ (x : FastCircle × FastCircle), g0 ((fastCoord 0) x) * g1 ((fastCoord 1) x) * g2 ((fastCoord 2) x) * g3 ((fastCoord 3) x) ∂fastHaar.prod fastHaar‖ ≤ (MeasureTheory.eLpNorm g0 2 fastHaar).toReal * (MeasureTheory.eLpNorm g1 2 fastHaar).toReal * (MeasureTheory.eLpNorm g2 2 fastHaar).toReal * (MeasureTheory.eLpNorm g3 2 fastHaar).toReal

The sampled form as a lattice sum of fast forms (lem:shortblock, lines 2298-2307)

noncomputable def TrilinearHT.Auto.slotLift (δ : ℝ) (f : Fin 4 → ℝ → ℂ) (j : Fin 4) (m : ℤ) : FastCircle → ℂ

The fast slot functions F_j(m, w) = f_j(δ(m + w)) on the lift interval of slot j (blueprint line 2303).

Equations

• TrilinearHT.Auto.slotLift δ f j m = TrilinearHT.Auto.fastLift j fun (x : ℝ) => f j (δ * (↑m + x))

noncomputable def TrilinearHT.Auto.fastFormAt (F : Fin 4 → ℤ → FastCircle → ℂ) (n : ℤ × ℤ) : ℂ

The fast progression form of one slow pair n = (n₀, n₁): ∫∫_{T₀²} Π_j F_j(n_j, w_j) with n_j = (1-j) n₀ + j n₁, w_j = (1-j) u + j v.

Equations

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

theorem TrilinearHT.Auto.measurable_slotLift {δ : ℝ} {f : Fin 4 → ℝ → ℂ} (hf : ∀ (j : Fin 4), Measurable (f j)) (j : Fin 4) (m : ℤ) : Measurable (slotLift δ f j m)

theorem TrilinearHT.Auto.unit_cell_eq_fastFormAt {δ : ℝ} {f : Fin 4 → ℝ → ℂ} (hf : ∀ (j : Fin 4), Measurable (f j)) (n : ℤ × ℤ) : ∫ (u : ℝ × ℝ) in Set.Ico 0 1 ×ˢ Set.Ico 0 1, ∏ j : Fin 4, f j (δ * ((1 - ↑↑j) * ↑n.1 + ↑↑j * ↑n.2 + ((1 - ↑↑j) * u.1 + ↑↑j * u.2))) = 256 * fastFormAt (slotLift δ f) n

The unit-cell integral of the progression inputs is 256 times the fast form.

theorem TrilinearHT.Auto.latticeSampled_support {w : ℝ × ℝ → ℂ} {a r δ : ℝ} (hδ : 0 < δ) (hw : HasLocalProgressionSupport a r w) : HasLocalProgressionSupport (a - 5 * δ) (r + 10 * δ) (latticeSampledKernel δ w)

The lattice-sampled kernel of a kernel with local progression support on [a, a + r] has local progression support on [a - 5δ, a + r + 5δ].

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

theorem TrilinearHT.Auto.eLpNorm_normalized_lt_top {f : ℝ → ℂ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (a r : ℝ) : MeasureTheory.eLpNorm f 2 (normalizedIntervalMeasure a r) < ⊤

theorem TrilinearHT.Auto.progression_integrable {w : ℝ × ℝ → ℂ} {a r W : ℝ} (hr : 0 < r) (hw : HasLocalProgressionSupport a r w) (hwm : Measurable w) (hW : ∀ (z : ℝ × ℝ), ‖w z‖ ≤ W) (f : Fin 4 → ℝ → ℂ) (hf : ∀ (j : Fin 4), Measurable (f j)) (hL : ∀ (j : Fin 4), MeasureTheory.MemLp (f j) 2 MeasureTheory.volume) : MeasureTheory.Integrable (fun (z : ℝ × ℝ) => w z * ∏ j : Fin 4, f j (realProgressionCoordinate j z)) MeasureTheory.volume

A bounded measurable kernel with local progression support against four L² inputs gives an integrable progression integrand (all-L² case of eq:absolute).

theorem TrilinearHT.Auto.sampled_form_eq_fast {w : ℝ × ℝ → ℂ} {a r δ W : ℝ} (hr : 0 < r) (hδ : 0 < δ) (hw : HasLocalProgressionSupport a r w) (hwm : Measurable w) (hW : ∀ (z : ℝ × ℝ), ‖w z‖ ≤ W) (f : Fin 4 → ℝ → ℂ) (hf : ∀ (j : Fin 4), Measurable (f j)) (hL : ∀ (j : Fin 4), MeasureTheory.MemLp (f j) 2 MeasureTheory.volume) (B : Finset (ℤ × ℤ)) (hB : ∀ (n : ℤ × ℤ), w (δ * ↑n.1, δ * ↑n.2 - δ * ↑n.1) ≠ 0 → n ∈ B) : localProgressionForm r (latticeSampledKernel δ w) f = (↑r)⁻¹ ^ 2 * ↑(δ ^ 2) * 256 * ∑ n ∈ B, w (δ * ↑n.1, δ * ↑n.2 - δ * ↑n.1) * fastFormAt (slotLift δ f) n

Blueprint lines 2302-2307: the form with the lattice-sampled kernel is r⁻² δ² 256 Σ_n w(δ n₀, δ(n₁ - n₀)) Φ_n(F), the sum over the finitely many slow pairs where the sampled kernel is nonzero, with Φ_n the fast form of the lifted inputs.

Window masses of the fast slots (lem:shortblock, blueprint lines 2328-2331)

theorem TrilinearHT.Auto.fastLiftLen_le (j : Fin 4) : fastLiftLen j ≤ 8

theorem TrilinearHT.Auto.fastLiftLen_pos (j : Fin 4) : 0 < fastLiftLen j

theorem TrilinearHT.Auto.fastLiftLeft_bounds (j : Fin 4) : -4 ≤ fastLiftLeft j ∧ fastLiftLeft j ≤ 0

noncomputable def TrilinearHT.Auto.fastLiftLenNat (j : Fin 4) : ℕ

The fast lift lengths are natural numbers (1 or 8).

Equations

• TrilinearHT.Auto.fastLiftLenNat j = if ↑j < 2 then 1 else 8

theorem TrilinearHT.Auto.fastLiftLenNat_cast (j : Fin 4) : ↑(fastLiftLenNat j) = fastLiftLen j

theorem TrilinearHT.Auto.lintegral_fastLift_enorm (j : Fin 4) (φ : ℝ → ℂ) (hφ : Measurable φ) (p : ℝ) (hp : 0 < p) : ∫⁻ (t : FastCircle), ‖fastLift j φ t‖ₑ ^ p ∂fastHaar = 1 / 16 * ∫⁻ (x : ℝ) in Set.Ico (fastLiftLeft j) (fastLiftLeft j + fastLiftLen j), ‖φ x‖ₑ ^ p

Haar integrals of lifted functions: ∫_{T₀} φTilde = (1/16) ∫_{[ℓ_j, ℓ_j + L_j)} φ.

theorem TrilinearHT.Auto.lintegral_slotLift (δ : ℝ) (hδ : 0 < δ) (f : Fin 4 → ℝ → ℂ) (hf : ∀ (j : Fin 4), Measurable (f j)) (j : Fin 4) (m : ℤ) (p : ℝ) (hp : 0 < p) : ∫⁻ (t : FastCircle), ‖slotLift δ f j m t‖ₑ ^ p ∂fastHaar = (ENNReal.ofReal (16 * δ))⁻¹ * ∫⁻ (y : ℝ) in Set.Ico (δ * (↑m + fastLiftLeft j)) (δ * (↑m + fastLiftLeft j + fastLiftLen j)), ‖f j y‖ₑ ^ p

The squared fast mass of a slot window: ∫_{T₀} |F_j(m, ·)|^p = (16 δ)⁻¹ ∫_{window} |f_j|^p, the window being [δ(m + ℓ_j), δ(m + ℓ_j + L_j)).

The comparison at one leaf-depth rectangle (lem:shortblock, lines 2298-2369)

structure TrilinearHT.Auto.BlockData (κ : LocalKernelClass) (Ω : Type u_1) [MeasurableSpace Ω] : Type u_1

The data of the comparison at one leaf-depth rectangle of lem:shortblock, after normalization: finitely many summation cells with admissible kernels, the sampling scale δ, random inputs z^σ with deterministic sizes Z_j, the inputs supported in [lo, hi].

• grid : RealDyadicGrid

  Dyadic grid supporting the short-block local forms.

• cells : Finset (ℤ × ℤ)

  Finite collection of cells in the short block.

• kernel : ℤ × ℤ → ℝ × ℝ → ℂ

  Admissible local kernel assigned to each short-block cell.

• admissible (I : ℤ × ℤ) : I ∈ self.cells → IsAdmissibleLocalKernel κ (dyadicGridLeft self.grid I.1 I.2) (dyadicGridLength self.grid I.1) (self.kernel I)
• δ : ℝ

  Positive smoothing scale small relative to each cell length and kernel margin.

• δ_pos : 0 < self.δ
• δ_small (I : ℤ × ℤ) : I ∈ self.cells → 8 * self.δ ≤ κ.margin * dyadicGridLength self.grid I.1
• δ_le_len (I : ℤ × ℤ) : I ∈ self.cells → 8 * self.δ ≤ dyadicGridLength self.grid I.1
• z : Fin 4 → Ω → ℝ → ℂ

  Measurable parameter-dependent input tuple for the block forms.

• z_meas (j : Fin 4) : Measurable (Function.uncurry (self.z j))
• Z : Fin 4 → ℝ → ℝ

  Nonnegative measurable envelopes controlling the parameter-dependent inputs.

• Z_meas (j : Fin 4) : Measurable (self.Z j)
• Z_nonneg (j : Fin 4) (y : ℝ) : 0 ≤ self.Z j y
• lo : ℝ

  Left endpoint of the common compact support interval for the inputs.

• hi : ℝ

  Right endpoint of the common compact support interval for the inputs.

• z_supp (j : Fin 4) (σ : Ω) (y : ℝ) : y ∉ Set.Icc self.lo self.hi → self.z j σ y = 0

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

The length r_I of a cell.

Equations

• D.len I = TrilinearHT.Auto.dyadicGridLength D.grid I.1

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

The left endpoint of a cell.

Equations

• D.left I = TrilinearHT.Auto.dyadicGridLeft D.grid I.1 I.2

def TrilinearHT.Auto.BlockData.inp {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (σ : Ω) : Fin 4 → ℝ → ℂ

The inputs at the random parameter σ.

Equations

• D.inp σ j = D.z j σ

theorem TrilinearHT.Auto.BlockData.len_pos {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (I : ℤ × ℤ) : 0 < D.len I

theorem TrilinearHT.Auto.BlockData.measurable_inp {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (σ : Ω) (j : Fin 4) : Measurable (D.inp σ j)

noncomputable def TrilinearHT.Auto.BlockData.total {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (ε : ℤ × ℤ → Ω → ℂ) (σ : Ω) : ℂ

The signed sum Σ_I |I| ε_I(σ) H_I(z^σ) of eq:shortblock.

Equations

• D.total ε σ = ∑ I ∈ D.cells, ↑(D.len I) * ε I σ * TrilinearHT.Auto.localProgressionForm (D.len I) (D.kernel I) (D.inp σ)

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

The first kernel-sampling error at a cell.

Equations

• D.err1 I σ = TrilinearHT.Auto.localProgressionForm (D.len I) (fun (w : ℝ × ℝ) => D.kernel I w - TrilinearHT.Auto.latticeSampledKernel D.δ (D.kernel I) w) (D.inp σ)

theorem TrilinearHT.Auto.lintegral_prod_four_le {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) (X : Fin 4 → Ω → ENNReal) (hX : ∀ (j : Fin 4), AEMeasurable (X j) P) : ∫⁻ (σ : Ω), ∏ j : Fin 4, X j σ ∂P ≤ ∏ j : Fin 4, (∫⁻ (σ : Ω), X j σ ^ 4 ∂P) ^ (1 / 4)

Hölder in the random parameter with four L⁴ factors.

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

The slow pairs n whose sampled kernel value at the cell I can be nonzero.

Equations

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

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

noncomputable def TrilinearHT.Auto.BlockData.latticeSum {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (ε : ℤ × ℤ → Ω → ℂ) (σ : Ω) (F : Fin 4 → ℤ → FastCircle → ℂ) : ℂ

The lattice sum Σ_I |I| ε_I r_I⁻² δ² 256 Σ_n w_I(δ n₀, δ(n₁ - n₀)) Φ_n(F) for fast data F.

Equations

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

theorem TrilinearHT.Auto.BlockData.total_eq {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (ε : ℤ × ℤ → Ω → ℂ) (σ : Ω) (hL : ∀ (j : Fin 4), MeasureTheory.MemLp (D.inp σ j) 2 MeasureTheory.volume) : D.total ε σ = ∑ I ∈ D.cells, ↑(D.len I) * ε I σ * D.err1 I σ + D.latticeSum ε σ (slotLift D.δ (D.inp σ))

Blueprint lines 2307-2312: for inputs in L², the signed sum splits into the first sampling errors and the lattice sum of the fast forms of the lifted inputs.

theorem TrilinearHT.Auto.memLp_slotLift {δ : ℝ} (hδ : 0 < δ) {f : Fin 4 → ℝ → ℂ} (hf : ∀ (j : Fin 4), Measurable (f j)) (hL : ∀ (j : Fin 4), MeasureTheory.MemLp (f j) 2 MeasureTheory.volume) (j : Fin 4) (m : ℤ) : MeasureTheory.MemLp (slotLift δ f j m) 2 fastHaar

theorem TrilinearHT.Auto.measurable_slotLift_joint {Ω : Type u_1} [MeasurableSpace Ω] {δ : ℝ} {z : Fin 4 → Ω → ℝ → ℂ} (hz : ∀ (j : Fin 4), Measurable (Function.uncurry (z j))) (j : Fin 4) (m : ℤ) : Measurable fun (p : Ω × FastCircle) => slotLift δ (fun (i : Fin 4) => z i p.1) j m p.2

Joint measurability of the lifted random slots.

theorem TrilinearHT.Auto.measurable_fourierCoeff_slotLift {Ω : Type u_1} [MeasurableSpace Ω] {δ : ℝ} {z : Fin 4 → Ω → ℝ → ℂ} (hz : ∀ (j : Fin 4), Measurable (Function.uncurry (z j))) (j : Fin 4) (m k : ℤ) : Measurable fun (σ : Ω) => fourierCoeff (slotLift δ (fun (i : Fin 4) => z i σ) j m) k

theorem TrilinearHT.Auto.fastFormAt_add_slot (F G H : Fin 4 → ℤ → FastCircle → ℂ) (a : Fin 4) (hF : ∀ (j : Fin 4), j ≠ a → F j = G j) (hH : ∀ (j : Fin 4), j ≠ a → H j = G j) (hsum : ∀ (m : ℤ) (t : FastCircle), G a m t = F a m t + H a m t) (cF : ∀ (j : Fin 4) (m : ℤ), Continuous (F j m)) (cH : ∀ (j : Fin 4) (m : ℤ), Continuous (H j m)) (n : ℤ × ℤ) : fastFormAt G n = fastFormAt F n + fastFormAt H n

The fast form is additive in one slot.

noncomputable def TrilinearHT.Auto.BlockData.wRet (a : Fin 4) (keep : Set ℤ) : Fin 4 → ℤ → ℂ

The retained weights: the heavy slot keeps exactly the slow points in keep.

Equations

• TrilinearHT.Auto.BlockData.wRet a keep j m = if j = a ∧ m ∉ keep then 0 else 1

noncomputable def TrilinearHT.Auto.BlockData.wDel (a : Fin 4) (keep : Set ℤ) : Fin 4 → ℤ → ℂ

The deleted weights: the heavy slot keeps exactly the slow points outside keep.

Equations

• TrilinearHT.Auto.BlockData.wDel a keep j m = if j = a ∧ m ∈ keep then 0 else 1

theorem TrilinearHT.Auto.BlockData.latticeSum_add {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (ε : ℤ × ℤ → Ω → ℂ) (σ : Ω) (F G H : Fin 4 → ℤ → FastCircle → ℂ) (h : ∀ (n : ℤ × ℤ), fastFormAt G n = fastFormAt F n + fastFormAt H n) : D.latticeSum ε σ G = D.latticeSum ε σ F + D.latticeSum ε σ H

theorem TrilinearHT.Auto.enorm_ofReal_of_nonneg {x : ℝ} (hx : 0 ≤ x) : ‖↑x‖ₑ = ENNReal.ofReal x

theorem TrilinearHT.Auto.fastLift_right_le (j : Fin 4) : fastLiftLeft j + fastLiftLen j ≤ 4

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

The deterministic sizes as complex functions.

Equations

• D.Zc j y = ↑(D.Z j y)

theorem TrilinearHT.Auto.BlockData.measurable_Zc {κ : LocalKernelClass} {Ω : Type u_1} [MeasurableSpace Ω] (D : BlockData κ Ω) (j : Fin 4) : Measurable (D.Zc j)

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

The constant of the second sampling error.

Equations

• TrilinearHT.Auto.BlockData.err2Const C4 = 2 ^ (1 / 2) * ENNReal.ofReal C4 ^ 2 / 8

Assembly of eq:shortblock (lem:shortblock, blueprint lines 2272-2369)

noncomputable def TrilinearHT.Auto.DepthRect.heavy : DepthRect → Fin 4

The heavy slot a of a rectangle (for rep, the least attaining slot).

Equations

• (TrilinearHT.Auto.DepthRect.rep S v).heavy = if h : S.Nonempty then S.min' h else 0
• (TrilinearHT.Auto.DepthRect.uniq a S h k).heavy = a

noncomputable def TrilinearHT.Auto.DepthRect.desig : DepthRect → Fin 4

The designated slot b of a rectangle (blueprint line 2292).

Equations

• (TrilinearHT.Auto.DepthRect.rep S v).desig = if h : (S.erase (if h : S.Nonempty then S.min' h else 0)).Nonempty then (S.erase (if h : S.Nonempty then S.min' h else 0)).min' h else 0
• (TrilinearHT.Auto.DepthRect.uniq a S h k).desig = if h : S.Nonempty then S.min' h else 0

theorem TrilinearHT.Auto.DepthRect.heavy_mem_rep {S : Finset (Fin 4)} {v : ℕ} (hv : (rep S v).Valid) : (rep S v).heavy ∈ S

theorem TrilinearHT.Auto.DepthRect.desig_mem_rep {S : Finset (Fin 4)} {v : ℕ} (hv : (rep S v).Valid) : (rep S v).desig ∈ S ∧ (rep S v).desig ≠ (rep S v).heavy

theorem TrilinearHT.Auto.DepthRect.desig_mem_uniq {a : Fin 4} {S : Finset (Fin 4)} {h k : ℕ} (hv : (uniq a S h k).Valid) : (uniq a S h k).desig ∈ S ∧ (uniq a S h k).desig ≠ (uniq a S h k).heavy

theorem TrilinearHT.Auto.DepthRect.desig_ne_heavy {R : DepthRect} (hv : R.Valid) : R.desig ≠ R.heavy

def TrilinearHT.Auto.DepthRect.level : DepthRect → DepthRect

The level of a rectangle: its slot assignment and scale, forgetting the position.

Equations

• (TrilinearHT.Auto.DepthRect.rep S v).level = TrilinearHT.Auto.DepthRect.rep S 0
• (TrilinearHT.Auto.DepthRect.uniq a S h k).level = TrilinearHT.Auto.DepthRect.uniq a S h 0

structure TrilinearHT.Auto.ShortBlockTree (G : RealDyadicGrid) (K : ℕ) : Type

A finite dyadic tree piece of lem:shortblock (blueprint line 2276): a root cell, internal summation cells in the K consecutive depths starting at first, and leaves in that block or one depth below; the leaves are disjoint cells inside the root covering it, and an internal cell meeting a leaf is strictly coarser.

• root : ℤ × ℤ

  Root cell of the short-block tree.

• first : ℤ

  First integer depth in the short block.

• internal : Finset (ℤ × ℤ)

  Internal cells at which the short-block expansion continues.

• leaves : Finset (ℤ × ℤ)

  Leaf cells at which the short-block expansion stops.

• internal_depth (I : ℤ × ℤ) : I ∈ self.internal → self.first ≤ I.1 ∧ I.1 < self.first + ↑K
• leaf_depth (L : ℤ × ℤ) : L ∈ self.leaves → self.first ≤ L.1 ∧ L.1 ≤ self.first + ↑K
• internal_subset (I : ℤ × ℤ) : I ∈ self.internal → dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G self.root.1 self.root.2
• leaf_subset (L : ℤ × ℤ) : L ∈ self.leaves → dyadicGridCell G L.1 L.2 ⊆ dyadicGridCell G self.root.1 self.root.2
• leaf_disjoint : (↑self.leaves).PairwiseDisjoint fun (L : ℤ × ℤ) => dyadicGridCell G L.1 L.2
• leaf_cover : dyadicGridCell G self.root.1 self.root.2 ⊆ ⋃ L ∈ self.leaves, dyadicGridCell G L.1 L.2
• internal_leaf (I : ℤ × ℤ) : I ∈ self.internal → ∀ L ∈ self.leaves, (dyadicGridCell G I.1 I.2 ∩ dyadicGridCell G L.1 L.2).Nonempty → I.1 < L.1

noncomputable def TrilinearHT.Auto.ShortBlockTree.cl (G : RealDyadicGrid) (c : ℤ × ℤ) : ℝ

Left endpoints and lengths of cells.

Equations

• TrilinearHT.Auto.ShortBlockTree.cl G c = TrilinearHT.Auto.dyadicGridLeft G c.1 c.2

noncomputable def TrilinearHT.Auto.ShortBlockTree.cr (G : RealDyadicGrid) (c : ℤ × ℤ) : ℝ

Length of the dyadic cell indexed by c.

Equations

• TrilinearHT.Auto.ShortBlockTree.cr G c = TrilinearHT.Auto.dyadicGridLength G c.1

theorem TrilinearHT.Auto.ShortBlockTree.leafInterval_eq {G : RealDyadicGrid} (c : ℤ × ℤ) : leafInterval (cl G) (cr G) c = dyadicGridCell G c.1 c.2

theorem TrilinearHT.Auto.ShortBlockTree.leaf_subset_internal {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) {I L : ℤ × ℤ} (hI : I ∈ T.internal) (hL : L ∈ T.leaves) (h : (dyadicGridCell G I.1 I.2 ∩ dyadicGridCell G L.1 L.2).Nonempty) : dyadicGridCell G L.1 L.2 ⊆ dyadicGridCell G I.1 I.2

Every leaf meeting an internal cell lies inside it.

def TrilinearHT.Auto.ShortBlockTree.depth {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (L : ℤ × ℤ) : ℕ

The padded depth of a leaf.

Equations

• T.depth L = (L.1 - T.first).toNat

theorem TrilinearHT.Auto.ShortBlockTree.depth_le {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) {L : ℤ × ℤ} (hL : L ∈ T.leaves) : T.depth L ≤ K

noncomputable def TrilinearHT.Auto.ShortBlockTree.dep {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) (y : ℝ) : ℕ

The leaf-depth labelling of points (zero outside the leaves).

Equations

• T.dep y = ∑ L ∈ T.leaves, (TrilinearHT.Auto.dyadicGridCell G L.1 L.2).indicator (fun (x : ℝ) => T.depth L) y

theorem TrilinearHT.Auto.ShortBlockTree.dep_eq {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) {L : ℤ × ℤ} (hL : L ∈ T.leaves) {y : ℝ} (hy : y ∈ dyadicGridCell G L.1 L.2) : T.dep y = T.depth L

theorem TrilinearHT.Auto.ShortBlockTree.measurable_dep {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) : Measurable T.dep

theorem TrilinearHT.Auto.ShortBlockTree.dep_lt {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) {m : ℕ} (hm : K < 2 ^ m) (y : ℝ) : T.dep y < 2 ^ m

def TrilinearHT.Auto.DepthRect.pos : DepthRect → ℕ

The position of a rectangle within its level.

Equations

• (TrilinearHT.Auto.DepthRect.rep S v).pos = v
• (TrilinearHT.Auto.DepthRect.uniq a S h k).pos = k

theorem TrilinearHT.Auto.DepthRect.eq_of_level_pos {R R' : DepthRect} (hl : R.level = R'.level) (hp : R.pos = R'.pos) : R = R'

theorem TrilinearHT.Auto.ennreal_sum_sqrt_mul_le {ι : Type u_1} (s : Finset ι) (f g : ι → ENNReal) : ∑ i ∈ s, f i ^ (1 / 2) * g i ^ (1 / 2) ≤ (∑ i ∈ s, f i) ^ (1 / 2) * (∑ i ∈ s, g i) ^ (1 / 2)

Cauchy–Schwarz for finite sums in ℝ≥0∞.

theorem TrilinearHT.Auto.dyadicGridLength_mul_two_pow (G : RealDyadicGrid) (s : ℤ) (n : ℕ) : dyadicGridLength G s = dyadicGridLength G (s + ↑n) * 2 ^ n

theorem TrilinearHT.Auto.two_mul_dyadicGridLength_le (G : RealDyadicGrid) {s t : ℤ} (h : s < t) : 2 * dyadicGridLength G t ≤ dyadicGridLength G s

theorem TrilinearHT.Auto.sum_length_ratio_le (G : RealDyadicGrid) (S : Finset ℤ) {t : ℤ} (hS : ∀ s ∈ S, s < t) : ∑ s ∈ S, dyadicGridLength G t / dyadicGridLength G s ≤ 1

The sampling weights of the coarser depths: Σ_{s ∈ S} r_t / r_s ≤ 1 for distinct s < t.

noncomputable def TrilinearHT.Auto.ShortBlockTree.beta (κ : LocalKernelClass) : ℝ

The sampling ratio β.

Equations

• TrilinearHT.Auto.ShortBlockTree.beta κ = min κ.margin 1 / 16

theorem TrilinearHT.Auto.ShortBlockTree.beta_pos (κ : LocalKernelClass) : 0 < beta κ

def TrilinearHT.Auto.ShortBlockTree.LeafBound {G : RealDyadicGrid} {K : ℕ} (T : ShortBlockTree G K) {E : Type u_2} [NormedAddCommGroup E] (z : Fin 4 → ℝ → E) : Prop

The leaf bound in the normalized form.

Equations

• T.LeafBound z = ∀ (j : Fin 4), ∀ L ∈ T.leaves, ∫⁻ (y : ℝ) in TrilinearHT.Auto.dyadicGridCell G L.1 L.2, ‖z j y‖ₑ ^ 2 ≤ ENNReal.ofReal (TrilinearHT.Auto.dyadicGridLength G L.1)

def TrilinearHT.Auto.pStar (q : ℝ) : ℝ

The heavy exponent p_* = 2q - 2.

Equations

• TrilinearHT.Auto.pStar q = 2 * q - 2

noncomputable def TrilinearHT.Auto.pReg (q : ℝ) : ℝ

The regular exponent p = 2 p_* / (p_* - 2) = (2q - 2) / (q - 2).

Equations

• TrilinearHT.Auto.pReg q = (2 * q - 2) / (q - 2)

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

theorem TrilinearHT.Auto.two_le_pReg {q : ℝ} (hq : 2 < q) : 2 ≤ pReg q

theorem TrilinearHT.Auto.pStar_pReg_sum {q : ℝ} (hq : 2 < q) : 2 / pStar q + 2 / pReg q = 1

noncomputable def TrilinearHT.Auto.ShortBlockTree.pexp (q : ℝ) (R : DepthRect) (j : Fin 4) : ℝ

The exponents of a rectangle: p_* in the heavy and designated slots, p elsewhere.

Equations

• TrilinearHT.Auto.ShortBlockTree.pexp q R j = if j = R.heavy ∨ j = R.desig then TrilinearHT.Auto.pStar q else TrilinearHT.Auto.pReg q

theorem TrilinearHT.Auto.ShortBlockTree.sum_inv_pexp {q : ℝ} (hq : 2 < q) {R : DepthRect} (hv : R.Valid) : ∑ j : Fin 4, 1 / pexp q R j = 1

noncomputable def TrilinearHT.Auto.ShortBlockTree.regE2 (κ : LocalKernelClass) : ℝ

The regular window constant E₂ = 1/2 + 1/(8β).

Equations

• TrilinearHT.Auto.ShortBlockTree.regE2 κ = 1 / 2 + 1 / (8 * TrilinearHT.Auto.ShortBlockTree.beta κ)

theorem TrilinearHT.Auto.natLog_le_two_log (K : ℕ) : ↑(Nat.log 2 (K + 1)) ≤ 2 * Real.log (↑K + 2)

theorem TrilinearHT.Auto.two_pow_succ_log_le (K : ℕ) : ↑(2 ^ (Nat.log 2 (K + 1) + 1)) ≤ 2 * (↑K + 2)

theorem TrilinearHT.Auto.pStar_exponent {q : ℝ} (hq : 2 < q) : (pStar q - 2) / pStar q = (q - 2) / (q - 1) ∧ 1 - 2 / pStar q = (q - 2) / (q - 1)

theorem TrilinearHT.Auto.localProgressionForm_mul_const (r : ℝ) (w : ℝ × ℝ → ℂ) (f : Fin 4 → ℝ → ℂ) (c : Fin 4 → ℂ) : (localProgressionForm r w fun (j : Fin 4) (y : ℝ) => f j y * c j) = (∏ j : Fin 4, c j) * localProgressionForm r w f

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

theorem TrilinearHT.Auto.q_lt_pReg {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) : q < pReg q

Fixed stacks for the two varying sides (blueprint lines 2400-2423)