Trilinear Hilbert transform: predictor_list_param

theorem TrilinearHT.Auto.predictor_list_param (c₀ : ℕ) (hc : 1 ≤ c₀) (κ : LocalKernelClass) : ∃ (c₁ : ℕ) (Ds : ℕ) (Cr : ℕ) (Dc : ℕ) (J1 : ℕ), 1 ≤ c₁ ∧ ∀ {d e : ℕ} (H B : ℝ) (A : QuadraticChartData d) (A' : QuadraticChartData e), 1 ≤ d → 1 ≤ e → QuadraticChartComplexity c₀ H A → QuadraticChartComplexity c₀ H A' → IsBoundedQuadraticChart A → IsBoundedQuadraticChart A' → 1 ≤ B → ∀ {a i k b : Fin 4}, a ≠ i → a ≠ k → a ≠ b → i ≠ k → i ≠ b → k ≠ b → ∃ (ι : Type) (L : Finset ι) (ψa : ι → QuadraticChartData (d + e)) (ψb : ι → QuadraticChartData (d + e)) (lam : ι → ℝ) (coef : ι → ℝ → ℂ), ↑L.card ≤ pdCard κ (d + e) Dc J1 Ds Cr H B ∧ (∀ ℓ ∈ L, IsBoundedQuadraticChart (ψa ℓ) ∧ IsBoundedQuadraticChart (ψb ℓ) ∧ QuadraticChartComplexity c₁ (pdH0 Ds Cr H B) (ψa ℓ) ∧ QuadraticChartComplexity c₁ (pdH0 Ds Cr H B) (ψb ℓ)) ∧ (∀ (r : ℝ), ∑ ℓ ∈ L, ‖coef ℓ r‖ ≤ 4 * pdEs Ds H * pdE Dc Ds Cr H B) ∧ (∀ (ℓ : ι) (r : ℝ), coef ℓ r ≠ 0 → |lam ℓ| * r ^ 2 ≤ pdE Dc Ds Cr H B) ∧ ∀ (G : RealDyadicGrid) (J : ℤ × ℤ) (S : Finset (ℤ × ℤ)), (∀ I ∈ S, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G J.1 J.2) → ∀ (w : ℤ × ℤ → ℝ × ℝ → ℂ), (∀ I ∈ S, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) → ∀ {Fa Fb : ℝ → ℂ} {za zb : ℤ × ℤ → ℝ → ℂ} {Ka Kb : ℝ}, 0 ≤ Ka → 0 ≤ Kb → IsAdmissibleOpponent G J Fa za Ka → IsAdmissibleOpponent G J Fb zb Kb → HasDepthEnergy G J Fa za Ka → HasDepthEnergy G J Fb zb Kb → (∀ (I : ℤ × ℤ), Measurable (za I)) → (∀ (I : ℤ × ℤ), Measurable (zb I)) → ⋯

Blueprint lem:predictors, eq:predictors with explicit parameters: the product of two fixed bounded atoms in slots i, k of the local form is replaced by a finite list of terms ψ_a(y_a) ψ_b(y_b) w_I(x,t) e(λ_* t²) with scale-dependent coefficients, with absolute length-weighted error at most e^{-B} K_a K_b ‖1_J F_a‖ ‖1_J F_b‖.

The quasipolynomial size of the predictor budget

theorem TrilinearHT.Auto.qple_poly {Y a : ℝ} {K : ℕ} (h : a ≤ ↑K * Y ^ K) : QPLe Y K a

theorem TrilinearHT.Auto.qple_exp {Y x : ℝ} {K : ℕ} (h : x ≤ ↑K * Y ^ K) : QPLe Y K (Real.exp x)

theorem TrilinearHT.Auto.qple_add {Y a b : ℝ} {K : ℕ} (hY : 1 ≤ Y) (ha : QPLe Y K a) (hb : QPLe Y K b) : QPLe Y (K + 1) (a + b)

theorem TrilinearHT.Auto.qple_add_one {Y a : ℝ} {K : ℕ} (hY : 1 ≤ Y) (ha : QPLe Y K a) : QPLe Y (K + 1) (a + 1)

theorem TrilinearHT.Auto.qple_pow_var {Y a : ℝ} {K m j n : ℕ} (hY : 1 ≤ Y) (ha0 : 0 ≤ a) (ha : QPLe Y K a) (hn : ↑n ≤ ↑m * Y ^ j) : QPLe Y (m * K + K + j) (a ^ n)

Variable powers a^n with n ≤ m Y^j.

theorem TrilinearHT.Auto.poly_add_le {Y x c : ℝ} {K n : ℕ} (hY : 1 ≤ Y) (hx : x ≤ ↑K * Y ^ K) (hc : c ≤ ↑n) : c + x ≤ ↑(K + n) * Y ^ (K + n)

A polynomial c + x with x ≤ K Y^K and c ≤ n.

theorem TrilinearHT.Auto.qp_pdX {Y H : ℝ} (hH : 1 ≤ H) (hHY : 1 + Real.log H ≤ Y) : 1 ≤ pdX H ∧ pdX H ≤ Y

theorem TrilinearHT.Auto.qp_pdEs {Y H : ℝ} (Ds : ℕ) (hH : 1 ≤ H) (hHY : 1 + Real.log H ≤ Y) : QPLe Y Ds (pdEs Ds H)

theorem TrilinearHT.Auto.qp_pdA0 {Y H : ℝ} (Ds : ℕ) (hH : 1 ≤ H) (hHY : 1 + Real.log H ≤ Y) : QPLe Y (8 * Ds + 2) (pdA0 Ds H)

theorem TrilinearHT.Auto.qp_expB {Y B : ℝ} (hBY : B ≤ Y) : QPLe Y 1 (Real.exp B)

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

theorem TrilinearHT.Auto.qp_pdT0 (Ds Cr : ℕ) : ∃ (K : ℕ), ∀ {Y H B : ℝ}, 1 ≤ H → B ≤ Y → 1 + Real.log H ≤ Y → QPLe Y K (pdT0 Ds Cr H B)

theorem TrilinearHT.Auto.qple_add' {Y a b : ℝ} {K L : ℕ} (hY : 1 ≤ Y) (ha : QPLe Y K a) (hb : QPLe Y L b) : QPLe Y (K + L + 1) (a + b)

theorem TrilinearHT.Auto.qple_max' {Y a b : ℝ} {K L : ℕ} (hY : 1 ≤ Y) (ha : QPLe Y K a) (hb : QPLe Y L b) : QPLe Y (K + L) (max a b)

theorem TrilinearHT.Auto.ceil_two_log_le {Y B z : ℝ} {K : ℕ} (hY : 1 ≤ Y) (hB0 : 0 ≤ B) (hBY : B ≤ Y) (hz : QPLe Y K z) (hz1 : 1 ≤ z) : ↑⌈2 * (B + Real.log z)⌉₊ ≤ ↑(2 * K + 3) * Y ^ (2 * K + 3)

theorem TrilinearHT.Auto.qple_exp_LE {Y h M : ℝ} {K1 K2 : ℕ} (D : ℕ) (hY : 1 ≤ Y) (hh1 : 1 ≤ h) (hh : QPLe Y K1 h) (hM0 : 0 ≤ M) (hM : M ≤ ↑K2 * Y ^ K2) : QPLe Y (D * (1 + (1 + K1 + K2)) ^ D + (1 + K1 + K2) * D) (Real.exp (↑D * (2 + Real.log h + M) ^ D))

theorem TrilinearHT.Auto.two_pow_ceil_logb_le {z : ℝ} (hz : 0 ≤ z) : 2 ^ ⌈Real.logb 2 z⌉₊ ≤ 2 * z + 1

theorem TrilinearHT.Auto.qp_pdH0 (Ds Cr : ℕ) : ∃ (K : ℕ), ∀ {Y H B : ℝ}, 1 ≤ H → B ≤ Y → 1 + Real.log H ≤ Y → QPLe Y K (pdH0 Ds Cr H B)

theorem TrilinearHT.Auto.qp_pdM0 (Ds Cr : ℕ) : ∃ (K : ℕ), ∀ {Y H B : ℝ}, 1 ≤ H → 0 ≤ B → B ≤ Y → 1 + Real.log H ≤ Y → ↑(pdM0 Ds Cr H B) ≤ ↑K * Y ^ K

theorem TrilinearHT.Auto.qp_pdLE_exp (Ds Cr D : ℕ) : ∃ (K : ℕ), ∀ {Y H B : ℝ}, 1 ≤ H → 0 ≤ B → B ≤ Y → 1 + Real.log H ≤ Y → QPLe Y K (Real.exp (↑D * pdLE Ds Cr H B ^ D))

theorem TrilinearHT.Auto.qp_tailCT (κ : LocalKernelClass) (KE : ℕ) : ∃ (K : ℕ), ∀ {Y E : ℝ} {d : ℕ}, 1 ≤ Y → ↑d ≤ 2 * Y → 1 ≤ E → QPLe Y KE E → QPLe Y K (tailCT κ d E)

theorem TrilinearHT.Auto.qp_pdK0 (κ : LocalKernelClass) (Dc J1 Ds Cr : ℕ) : ∃ (K : ℕ), ∀ {Y H B : ℝ} {d' : ℕ}, 1 ≤ H → 0 ≤ B → B ≤ Y → 1 + Real.log H ≤ Y → ↑d' ≤ 2 * Y → QPLe Y K (2 ^ pdK0 κ d' Dc J1 Ds Cr H B)

theorem TrilinearHT.Auto.qp_pdCard (κ : LocalKernelClass) (Dc J1 Ds Cr : ℕ) : ∃ (K : ℕ), ∀ {Y H B : ℝ} {d' : ℕ}, 1 ≤ H → 0 ≤ B → B ≤ Y → 1 + Real.log H ≤ Y → ↑d' ≤ 2 * Y → QPLe Y K (pdCard κ d' Dc J1 Ds Cr H B)

theorem TrilinearHT.Auto.finitePredictorList (c₀ : ℕ) (hc : 1 ≤ c₀) (κ : LocalKernelClass) : ∃ (c₁ : ℕ) (C : ℕ), 1 ≤ c₁ ∧ ∀ {d e : ℕ} (H B : ℝ) (A : QuadraticChartData d) (A' : QuadraticChartData e), 1 ≤ d → 1 ≤ e → QuadraticChartComplexity c₀ H A → QuadraticChartComplexity c₀ H A' → IsBoundedQuadraticChart A → IsBoundedQuadraticChart A' → 1 ≤ B → ∀ {a i k b : Fin 4}, a ≠ i → a ≠ k → a ≠ b → i ≠ k → i ≠ b → k ≠ b → ∃ (ι : Type) (L : Finset ι) (ψa : ι → QuadraticChartData (d + e)) (ψb : ι → QuadraticChartData (d + e)) (lam : ι → ℝ) (coef : ι → ℝ → ℂ), ↑L.card ≤ Real.exp (↑C * (1 + B + Real.log H) ^ C) ∧ (∀ ℓ ∈ L, IsBoundedQuadraticChart (ψa ℓ) ∧ IsBoundedQuadraticChart (ψb ℓ) ∧ QuadraticChartComplexity c₁ (Real.exp (↑C * (1 + B + Real.log H) ^ C)) (ψa ℓ) ∧ QuadraticChartComplexity c₁ (Real.exp (↑C * (1 + B + Real.log H) ^ C)) (ψb ℓ)) ∧ (∀ (r : ℝ), ∑ ℓ ∈ L, ‖coef ℓ r‖ ≤ Real.exp (↑C * (1 + B + Real.log H) ^ C)) ∧ (∀ (ℓ : ι) (r : ℝ), coef ℓ r ≠ 0 → |lam ℓ| * r ^ 2 ≤ Real.exp (↑C * (1 + B + Real.log H) ^ C)) ∧ ∀ (G : RealDyadicGrid) (J : ℤ × ℤ) (S : Finset (ℤ × ℤ)), (∀ I ∈ S, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G J.1 J.2) → ∀ (w : ℤ × ℤ → ℝ × ℝ → ℂ), (∀ I ∈ S, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) → ∀ {Fa Fb : ℝ → ℂ} {za zb : ℤ × ℤ → ℝ → ℂ} {Ka Kb : ℝ}, 0 ≤ Ka → 0 ≤ Kb → IsAdmissibleOpponent G J Fa za Ka → IsAdmissibleOpponent G J Fb zb Kb → HasDepthEnergy G J Fa za Ka → HasDepthEnergy G J Fb zb Kb → (∀ (I : ℤ × ℤ), Measurable (za I)) → (∀ (I : ℤ × ℤ), Measurable (zb I)) → (∀ (I : ℤ × ℤ), MeasureTheory.MemLp (za I) 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) → (∀ (I : ℤ × ℤ), ⋯) → ∀ (f : ℤ × ℤ → Fin 4 → ℝ → ℂ), ⋯

Blueprint lem:predictors, eq:predictors (Declaration predictors, line 1536): for two fixed bounded original atoms of complexity H in slots i, k and B ≥ 1, their product in the local form is replaced by a finite list of terms ψ_a(y_a) ψ_b(y_b) w_I(x,t) e(λ_* t²) with |λ_*| |I|² ≤ D_pred, scale-dependent scalar coefficients, bounded atoms ψ_a, ψ_b fixed on J, and absolute length-weighted error at most e^{-B} K_a K_b ‖1_J F_a‖ ‖1_J F_b‖ against admissible opponents with depth energy (the opponent constants K_a, K_b carry the polynomial in log(2 D_h) and 1 + L). The list size, the coefficient norm, the multiplier complexities and D_pred are at most D_pred = exp(C (1 + B + log H)^C), i.e. log D_pred ≤ poly(1 + B, log H).

Dyadic conditional expectations

noncomputable def TrilinearHT.Auto.dyadicIndex (G : RealDyadicGrid) (h : ℤ) (y : ℝ) : ℤ

The position of the depth-h cell containing y.

Equations

• TrilinearHT.Auto.dyadicIndex G h y = Classical.choose ⋯

theorem TrilinearHT.Auto.mem_dyadicIndex (G : RealDyadicGrid) (h : ℤ) (y : ℝ) : y ∈ dyadicGridCell G h (dyadicIndex G h y)

theorem TrilinearHT.Auto.dyadicIndex_eq {G : RealDyadicGrid} {h m : ℤ} {y : ℝ} (hy : y ∈ dyadicGridCell G h m) : dyadicIndex G h y = m

noncomputable def TrilinearHT.Auto.cellAverage (G : RealDyadicGrid) (h m : ℤ) (F : ℝ → ℂ) : ℂ

The normalized integral of F over the depth-h cell at position m.

Equations

• TrilinearHT.Auto.cellAverage G h m F = ↑(TrilinearHT.Auto.dyadicGridLength G h)⁻¹ * ∫ (y : ℝ) in TrilinearHT.Auto.dyadicGridCell G h m, F y

noncomputable def TrilinearHT.Auto.depthExpectation (G : RealDyadicGrid) (h : ℤ) (F : ℝ → ℂ) (y : ℝ) : ℂ

The dyadic conditional expectation E_h at depth h.

Equations

• TrilinearHT.Auto.depthExpectation G h F y = TrilinearHT.Auto.cellAverage G h (TrilinearHT.Auto.dyadicIndex G h y) F

theorem TrilinearHT.Auto.depthExpectation_of_mem {G : RealDyadicGrid} {h m : ℤ} {y : ℝ} (hy : y ∈ dyadicGridCell G h m) (F : ℝ → ℂ) : depthExpectation G h F y = cellAverage G h m F

def TrilinearHT.Auto.DepthConst (G : RealDyadicGrid) (h : ℤ) (g : ℝ → ℂ) : Prop

Functions that are constant on every depth-h cell.

Equations

• TrilinearHT.Auto.DepthConst G h g = ∀ (m : ℤ), ∀ y ∈ TrilinearHT.Auto.dyadicGridCell G h m, ∀ z ∈ TrilinearHT.Auto.dyadicGridCell G h m, g y = g z

theorem TrilinearHT.Auto.depthConst_depthExpectation (G : RealDyadicGrid) (h : ℤ) (F : ℝ → ℂ) : DepthConst G h (depthExpectation G h F)

theorem TrilinearHT.Auto.DepthConst.mono {G : RealDyadicGrid} {h k : ℤ} (hhk : h ≤ k) {g : ℝ → ℂ} (hg : DepthConst G h g) : DepthConst G k g

Constancy passes to deeper cells.

theorem TrilinearHT.Auto.setIntegral_cell_eq_sum_generation (G : RealDyadicGrid) (I : ℤ × ℤ) (n : ℕ) {F : ℝ → ℂ} (hF : MeasureTheory.IntegrableOn F (dyadicGridCell G I.1 I.2) MeasureTheory.volume) : ∫ (y : ℝ) in dyadicGridCell G I.1 I.2, F y = ∑ Q ∈ dyadicGeneration G I n, ∫ (y : ℝ) in dyadicGridCell G Q.1 Q.2, F y

The integral over a cell splits over its depth-(s+n) generation.

theorem TrilinearHT.Auto.setIntegral_mul_const_cell {G : RealDyadicGrid} {Q : ℤ × ℤ} {g : ℝ → ℂ} {c : ℂ} (hg : ∀ y ∈ dyadicGridCell G Q.1 Q.2, g y = c) (F : ℝ → ℂ) : ∫ (y : ℝ) in dyadicGridCell G Q.1 Q.2, F y * g y = (∫ (y : ℝ) in dyadicGridCell G Q.1 Q.2, F y) * c

theorem TrilinearHT.Auto.setIntegral_depthExpectation (G : RealDyadicGrid) (I : ℤ × ℤ) (n : ℕ) {F : ℝ → ℂ} (hF : MeasureTheory.IntegrableOn F (dyadicGridCell G I.1 I.2) MeasureTheory.volume) : ∫ (y : ℝ) in dyadicGridCell G I.1 I.2, depthExpectation G (I.1 + ↑n) F y = ∫ (y : ℝ) in dyadicGridCell G I.1 I.2, F y

∫_Q E_k F = ∫_Q F on cells of depth at most k.

theorem TrilinearHT.Auto.dyadicIndex_eq_floor (G : RealDyadicGrid) (h : ℤ) (y : ℝ) : dyadicIndex G h y = ⌊(y - G.origin h) / dyadicGridLength G h⌋

theorem TrilinearHT.Auto.measurable_depthExpectation (G : RealDyadicGrid) (h : ℤ) (F : ℝ → ℂ) : Measurable (depthExpectation G h F)

theorem TrilinearHT.Auto.volume_real_cell (G : RealDyadicGrid) (s m : ℤ) : MeasureTheory.volume.real (dyadicGridCell G s m) = dyadicGridLength G s

theorem TrilinearHT.Auto.cell_isFiniteMeasure (G : RealDyadicGrid) (s m : ℤ) : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (dyadicGridCell G s m))

theorem TrilinearHT.Auto.dyadicGridLength_add_nat (G : RealDyadicGrid) (s : ℤ) (j : ℕ) : dyadicGridLength G (s + ↑j) = dyadicGridLength G s * 2⁻¹ ^ j

theorem TrilinearHT.Auto.norm_cellAverage_sub_le {G : RealDyadicGrid} {h m : ℤ} {F : ℝ → ℂ} {c : ℂ} {B : ℝ} (hF : MeasureTheory.IntegrableOn F (dyadicGridCell G h m) MeasureTheory.volume) (hB : ∀ z ∈ dyadicGridCell G h m, ‖F z - c‖ ≤ B) : ‖cellAverage G h m F - c‖ ≤ B

theorem TrilinearHT.Auto.integrableOn_cell_of_continuous (G : RealDyadicGrid) (s m : ℤ) {θ : ℝ → ℂ} (hθ : Continuous θ) : MeasureTheory.IntegrableOn θ (dyadicGridCell G s m) MeasureTheory.volume

theorem TrilinearHT.Auto.norm_depthExpectation_le (G : RealDyadicGrid) (h : ℤ) {θ : ℝ → ℂ} {L : ℝ} (hθc : Continuous θ) (hθb : ∀ (y : ℝ), ‖θ y‖ ≤ L) (y : ℝ) : ‖depthExpectation G h θ y‖ ≤ L

theorem TrilinearHT.Auto.norm_sub_depthExpectation_le (G : RealDyadicGrid) (h : ℤ) {θ : ℝ → ℂ} {Lip : ℝ} (hLip0 : 0 ≤ Lip) (hθc : Continuous θ) (hLip : ∀ (y z : ℝ), ‖θ y - θ z‖ ≤ Lip * |y - z|) (y : ℝ) : ‖θ y - depthExpectation G h θ y‖ ≤ Lip * dyadicGridLength G h

theorem TrilinearHT.Auto.norm_depthExpectation_succ_sub_le (G : RealDyadicGrid) (h : ℤ) {θ : ℝ → ℂ} {Lip : ℝ} (hLip0 : 0 ≤ Lip) (hθc : Continuous θ) (hLip : ∀ (y z : ℝ), ‖θ y - θ z‖ ≤ Lip * |y - z|) (y : ℝ) : ‖depthExpectation G (h + 1) θ y - depthExpectation G h θ y‖ ≤ 2 * Lip * dyadicGridLength G h

theorem TrilinearHT.Auto.integrableOn_cell_mul_bdd {G : RealDyadicGrid} {I : ℤ × ℤ} {u v : ℝ → ℂ} {B : ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) (hv : Measurable v) (hvb : ∀ (y : ℝ), ‖v y‖ ≤ B) : MeasureTheory.IntegrableOn (fun (y : ℝ) => u y * v y) (dyadicGridCell G I.1 I.2) MeasureTheory.volume

theorem TrilinearHT.Auto.norm_setIntegral_cell_mul_le {G : RealDyadicGrid} {I : ℤ × ℤ} {u v : ℝ → ℂ} {B : ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) (hB : 0 ≤ B) (hvb : ∀ (y : ℝ), ‖v y‖ ≤ B) : ‖∫ (y : ℝ) in dyadicGridCell G I.1 I.2, u y * v y‖ ≤ B * √(dyadicGridLength G I.1) * √(∫ (y : ℝ) in dyadicGridCell G I.1 I.2, ‖u y‖ ^ 2)

theorem TrilinearHT.Auto.setIntegral_mul_locConst (G : RealDyadicGrid) (I : ℤ × ℤ) (n : ℕ) {D μ g : ℝ → ℂ} (hg : ∀ Q ∈ dyadicGeneration G I n, ∀ y ∈ dyadicGridCell G Q.1 Q.2, ∀ z ∈ dyadicGridCell G Q.1 Q.2, g y = g z) (hD : MeasureTheory.IntegrableOn D (dyadicGridCell G I.1 I.2) MeasureTheory.volume) (hμ : MeasureTheory.IntegrableOn μ (dyadicGridCell G I.1 I.2) MeasureTheory.volume) (hDμ : ∀ Q ∈ dyadicGeneration G I n, ∫ (y : ℝ) in dyadicGridCell G Q.1 Q.2, D y = ∫ (y : ℝ) in dyadicGridCell G Q.1 Q.2, μ y) : ∫ (y : ℝ) in dyadicGridCell G I.1 I.2, D y * g y = ∫ (y : ℝ) in dyadicGridCell G I.1 I.2, μ y * g y

The swap principle with constancy only on the depth-(s+n) cells of I.

theorem TrilinearHT.Auto.depthConst_locConst {G : RealDyadicGrid} {I : ℤ × ℤ} {n : ℕ} {k : ℤ} (hk : k ≤ I.1 + ↑n) {g : ℝ → ℂ} (hg : DepthConst G k g) (Q : ℤ × ℤ) : Q ∈ dyadicGeneration G I n → ∀ y ∈ dyadicGridCell G Q.1 Q.2, ∀ z ∈ dyadicGridCell G Q.1 Q.2, g y = g z

theorem TrilinearHT.Auto.setIntegral_depthExpectation_of_le (G : RealDyadicGrid) (Q : ℤ × ℤ) {k : ℤ} (hk : Q.1 ≤ k) {F : ℝ → ℂ} (hF : MeasureTheory.IntegrableOn F (dyadicGridCell G Q.1 Q.2) MeasureTheory.volume) : ∫ (y : ℝ) in dyadicGridCell G Q.1 Q.2, depthExpectation G k F y = ∫ (y : ℝ) in dyadicGridCell G Q.1 Q.2, F y

∫_Q E_k F = ∫_Q F on cells Q of depth at most k.

theorem TrilinearHT.Auto.cellRow_memLp {G : RealDyadicGrid} {ι : Type} (R : CellRowFamily G ι) (i : ι) : MeasureTheory.MemLp (R.test i) 2 MeasureTheory.volume

A bounded measurable cell-supported test as an L² class.

theorem TrilinearHT.Auto.cellRow_inner_Lp {G : RealDyadicGrid} {ι : Type} (R : CellRowFamily G ι) (i : ι) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : inner ℂ (MeasureTheory.MemLp.toLp (R.test i) ⋯) g = ∫ (y : ℝ), (starRingEnd ℂ) (R.test i y) * ↑↑g y

Path-uniform column systems

structure TrilinearHT.Auto.PathColumnSystem (G : RealDyadicGrid) (J : ℤ × ℤ) (N : ℕ) (V : Type) [Fintype V] : Type

A path-uniform column system on the complete finite tree of depth N below J: labels reused across disjoint branches, inherited cellwise availability, cellwise bounded scalars that agree along paths, and private weights in (0, 1] (blueprint sec:columns, lines 470-483, in the form used by prop:base).

• avail : ℤ × ℤ → Finset V

  Available column labels at each point of a dyadic path.

• scalarAt : ℤ × ℤ → V → ℝ → ℂ

  Scalar column function at each cell and label.

• weight : V → ℝ

  Normalization weight of a path column label.

• weight_pos (v : V) : 0 < self.weight v
• weight_le (v : V) : self.weight v ≤ 1
• scalar_meas (c : ℤ × ℤ) (v : V) : Measurable (self.scalarAt c v)
• scalar_bound (c : ℤ × ℤ) (v : V) (y : ℝ) : ‖self.scalarAt c v y‖ ≤ 1
• avail_mono (c d : ℤ × ℤ) : c ∈ dyadicFiniteTree G J N → d ∈ dyadicFiniteTree G J N → dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2 → self.avail d ⊆ self.avail c
• consistent (c d : ℤ × ℤ) : c ∈ dyadicFiniteTree G J N → d ∈ dyadicFiniteTree G J N → dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2 → ∀ v ∈ self.avail d, ∀ y ∈ dyadicGridCell G c.1 c.2, self.scalarAt c v y = self.scalarAt d v y

noncomputable def TrilinearHT.Auto.pathLeaf (G : RealDyadicGrid) (J : ℤ × ℤ) (N : ℕ) (y : ℝ) : ℤ × ℤ

The leaf of the tree of depth N below J containing y.

Equations

• TrilinearHT.Auto.pathLeaf G J N y = (J.1 + ↑N, TrilinearHT.Auto.dyadicIndex G (J.1 + ↑N) y)

noncomputable def TrilinearHT.Auto.pathBelow (G : RealDyadicGrid) (J : ℤ × ℤ) (N : ℕ) (R : ℤ × ℤ) : Finset (ℤ × ℤ)

The part below R of the tree of depth N below J.

Equations

• TrilinearHT.Auto.pathBelow G J N R = TrilinearHT.Auto.dyadicFiniteTree G R (TrilinearHT.Auto.dyadicRemainingDepth J N R)

noncomputable def TrilinearHT.Auto.PathColumnSystem.scalar {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) (R : ℤ × ℤ) (v : V) (y : ℝ) : ℂ

The scalar of label v, read off at the leaf below y (and at R outside R).

Equations

• P.scalar R v y = if y ∈ TrilinearHT.Auto.dyadicGridCell G R.1 R.2 then P.scalarAt (TrilinearHT.Auto.pathLeaf G J N y) v y else P.scalarAt R v y

theorem TrilinearHT.Auto.PathColumnSystem.scalar_bound' {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) (R : ℤ × ℤ) (v : V) (y : ℝ) : ‖P.scalar R v y‖ ≤ 1

theorem TrilinearHT.Auto.PathColumnSystem.below_mem_iff {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {R : ℤ × ℤ} (hR : R ∈ dyadicFiniteTree G J N) (c : ℤ × ℤ) : c ∈ pathBelow G J N R ↔ c ∈ dyadicFiniteTree G J N ∧ dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G R.1 R.2

theorem TrilinearHT.Auto.PathColumnSystem.leaf_mem {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} (y : ℝ) : y ∈ dyadicGridCell G (pathLeaf G J N y).1 (pathLeaf G J N y).2

noncomputable def TrilinearHT.Auto.PathColumnSystem.budget {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) : ℝ

The budget of the system.

Equations

• P.budget = 2 + ↑(Fintype.card V) + ∑ v : V, (√(P.weight v))⁻¹

theorem TrilinearHT.Auto.PathColumnSystem.two_le_budget {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) : 2 ≤ P.budget

Opponent algebra and delayed opponents

theorem TrilinearHT.Auto.IsAdmissibleOpponent.congr_cell {G : RealDyadicGrid} {J : ℤ × ℤ} {F : ℝ → ℂ} {z z' : ℤ × ℤ → ℝ → ℂ} {K : ℝ} (h : IsAdmissibleOpponent G J F z K) (hz : ∀ (I : ℤ × ℤ), dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G J.1 J.2 → ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → z' I y = z I y) : IsAdmissibleOpponent G J F z' K

Admissibility only sees each opponent on its own cell.

theorem TrilinearHT.Auto.cellRow_integrable {G : RealDyadicGrid} {ι : Type} (R : CellRowFamily G ι) (i : ι) {z : ℝ → ℂ} (hz : MeasureTheory.MemLp z 2 (MeasureTheory.volume.restrict (dyadicGridCell G (R.cell i).1 (R.cell i).2))) : MeasureTheory.Integrable (fun (y : ℝ) => (starRingEnd ℂ) (R.test i y) * z y) MeasureTheory.volume

theorem TrilinearHT.Auto.norm_add_sq_le_two (a b : ℂ) : ‖a + b‖ ^ 2 ≤ 2 * ‖a‖ ^ 2 + 2 * ‖b‖ ^ 2

theorem TrilinearHT.Auto.IsAdmissibleOpponent.add {G : RealDyadicGrid} {J : ℤ × ℤ} {F : ℝ → ℂ} {z₁ z₂ : ℤ × ℤ → ℝ → ℂ} {K₁ K₂ : ℝ} (hK₁ : 0 ≤ K₁) (hK₂ : 0 ≤ K₂) (h₁ : IsAdmissibleOpponent G J F z₁ K₁) (h₂ : IsAdmissibleOpponent G J F z₂ K₂) (hm₁ : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (z₁ I) 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) (hm₂ : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (z₂ I) 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) : IsAdmissibleOpponent G J F (fun (I : ℤ × ℤ) (y : ℝ) => z₁ I y + z₂ I y) (2 * (K₁ + K₂))

Sums of admissible opponents are admissible.

theorem TrilinearHT.Auto.HasDepthEnergy.add {G : RealDyadicGrid} {J : ℤ × ℤ} {F : ℝ → ℂ} {z₁ z₂ : ℤ × ℤ → ℝ → ℂ} {K₁ K₂ : ℝ} (hK₁ : 0 ≤ K₁) (hK₂ : 0 ≤ K₂) (h₁ : HasDepthEnergy G J F z₁ K₁) (h₂ : HasDepthEnergy G J F z₂ K₂) (hm₁ : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (z₁ I) 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) (hm₂ : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (z₂ I) 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) : HasDepthEnergy G J F (fun (I : ℤ × ℤ) (y : ℝ) => z₁ I y + z₂ I y) (2 * (K₁ + K₂))

Sums of opponents with depth energy have depth energy.

Predictor approximation and delayed replacement for one low pair

def TrilinearHT.Auto.PredictorApprox (κ : LocalKernelClass) {d e : ℕ} (A : QuadraticChartData d) (A' : QuadraticChartData e) (a i k b : Fin 4) (B : ℝ) {ι : Type} (L : Finset ι) (ψa ψb : ι → QuadraticChartData (d + e)) (lam : ι → ℝ) (coef : ι → ℝ → ℂ) : Prop

The approximation property eq:predictors of a predictor list for the chart pair (A, A') in slots i, k, against admissible opponents in slots a, b.

Equations

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

theorem TrilinearHT.Auto.finitePredictorList_approx (c₀ : ℕ) (hc : 1 ≤ c₀) (κ : LocalKernelClass) : ∃ (c₁ : ℕ) (C : ℕ), 1 ≤ c₁ ∧ ∀ {d e : ℕ} (H B : ℝ) (A : QuadraticChartData d) (A' : QuadraticChartData e), 1 ≤ d → 1 ≤ e → QuadraticChartComplexity c₀ H A → QuadraticChartComplexity c₀ H A' → IsBoundedQuadraticChart A → IsBoundedQuadraticChart A' → 1 ≤ B → ∀ {a i k b : Fin 4}, a ≠ i → a ≠ k → a ≠ b → i ≠ k → i ≠ b → k ≠ b → ∃ (ι : Type) (L : Finset ι) (ψa : ι → QuadraticChartData (d + e)) (ψb : ι → QuadraticChartData (d + e)) (lam : ι → ℝ) (coef : ι → ℝ → ℂ), ↑L.card ≤ Real.exp (↑C * (1 + B + Real.log H) ^ C) ∧ (∀ ℓ ∈ L, IsBoundedQuadraticChart (ψa ℓ) ∧ IsBoundedQuadraticChart (ψb ℓ) ∧ QuadraticChartComplexity c₁ (Real.exp (↑C * (1 + B + Real.log H) ^ C)) (ψa ℓ) ∧ QuadraticChartComplexity c₁ (Real.exp (↑C * (1 + B + Real.log H) ^ C)) (ψb ℓ)) ∧ (∀ (r : ℝ), ∑ ℓ ∈ L, ‖coef ℓ r‖ ≤ Real.exp (↑C * (1 + B + Real.log H) ^ C)) ∧ (∀ (ℓ : ι) (r : ℝ), coef ℓ r ≠ 0 → |lam ℓ| * r ^ 2 ≤ Real.exp (↑C * (1 + B + Real.log H) ^ C)) ∧ PredictorApprox κ A A' a i k b B L ψa ψb lam coef

Blueprint lem:predictors (THT.Base.finitePredictorList) in the packaged form used by prop:base.

noncomputable def TrilinearHT.Auto.slots4 (a i k : Fin 4) (za φ φ' zb : ℝ → ℂ) : Fin 4 → ℝ → ℂ

The four inputs (z_a, φ, φ', z_b) placed in the slots a, i, k, b.

Equations

• TrilinearHT.Auto.slots4 a i k za φ φ' zb l = if l = a then za else if l = i then φ else if l = k then φ' else zb

theorem TrilinearHT.Auto.slots4_a {a i k : Fin 4} (za φ φ' zb : ℝ → ℂ) : slots4 a i k za φ φ' zb a = za

theorem TrilinearHT.Auto.slots4_i {a i k : Fin 4} (hai : a ≠ i) (za φ φ' zb : ℝ → ℂ) : slots4 a i k za φ φ' zb i = φ

theorem TrilinearHT.Auto.slots4_k {a i k : Fin 4} (hak : a ≠ k) (hik : i ≠ k) (za φ φ' zb : ℝ → ℂ) : slots4 a i k za φ φ' zb k = φ'

theorem TrilinearHT.Auto.slots4_b {a i k b : Fin 4} (hab : a ≠ b) (hib : i ≠ b) (hkb : k ≠ b) (za φ φ' zb : ℝ → ℂ) : slots4 a i k za φ φ' zb b = zb

theorem TrilinearHT.Auto.IsAdmissibleOpponent.mono {G : RealDyadicGrid} {J : ℤ × ℤ} {F : ℝ → ℂ} {z : ℤ × ℤ → ℝ → ℂ} {K K' : ℝ} (h : IsAdmissibleOpponent G J F z K) (hK : 0 ≤ K) (hKK : K ≤ K') : IsAdmissibleOpponent G J F z K'

theorem TrilinearHT.Auto.HasDepthEnergy.mono {G : RealDyadicGrid} {J : ℤ × ℤ} {F : ℝ → ℂ} {z : ℤ × ℤ → ℝ → ℂ} {K K' : ℝ} (h : HasDepthEnergy G J F z K) (hK : 0 ≤ K) (hKK : K ≤ K') : HasDepthEnergy G J F z K'

The predictor high system

structure TrilinearHT.Auto.PredictorPackage (κ : LocalKernelClass) {d e : ℕ} (A : QuadraticChartData d) (A' : QuadraticChartData e) (a i k b : Fin 4) (B D : ℝ) (c₁ : ℕ) : Type 1

A predictor list for a chart pair with budget D (blueprint lem:predictors).

• ι : Type

  Index type for the finite family of predictors.

• L : Finset self.ι

  Finite set of predictor indices used by the package.

• ψa : self.ι → QuadraticChartData (d + e)

  First chart factor of each separated predictor.

• ψb : self.ι → QuadraticChartData (d + e)

  Second chart factor of each separated predictor.

• lam : self.ι → ℝ

  Scalar quadratic phase coefficient of each predictor.

• coef : self.ι → ℝ → ℂ

  Scale-dependent coefficient of each predictor.

• card_le : ↑self.L.card ≤ D
• bdd (ℓ : self.ι) : ℓ ∈ self.L → IsBoundedQuadraticChart (self.ψa ℓ) ∧ IsBoundedQuadraticChart (self.ψb ℓ) ∧ QuadraticChartComplexity c₁ D (self.ψa ℓ) ∧ QuadraticChartComplexity c₁ D (self.ψb ℓ)
• coef_le (r : ℝ) : ∑ ℓ ∈ self.L, ‖self.coef ℓ r‖ ≤ D
• lam_le (ℓ : self.ι) (r : ℝ) : self.coef ℓ r ≠ 0 → |self.lam ℓ| * r ^ 2 ≤ D
• approx : PredictorApprox κ A A' a i k b B self.L self.ψa self.ψb self.lam self.coef

theorem TrilinearHT.Auto.predictorPackage_nonempty (c₀ : ℕ) (hc : 1 ≤ c₀) (κ : LocalKernelClass) : ∃ (c₁ : ℕ) (C : ℕ), 1 ≤ c₁ ∧ ∀ {d e : ℕ} (H B : ℝ) (A : QuadraticChartData d) (A' : QuadraticChartData e), 1 ≤ d → 1 ≤ e → QuadraticChartComplexity c₀ H A → QuadraticChartComplexity c₀ H A' → IsBoundedQuadraticChart A → IsBoundedQuadraticChart A' → 1 ≤ B → ∀ {a i k b : Fin 4}, a ≠ i → a ≠ k → a ≠ b → i ≠ k → i ≠ b → k ≠ b → Nonempty (PredictorPackage κ A A' a i k b B (Real.exp (↑C * (1 + B + Real.log H) ^ C)) c₁)

lem:predictors provides packages for all admissible chart pairs.

Bridges for the replacement

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