Trilinear Hilbert transform: delayData

structure TrilinearHT.Auto.DelayData (G : RealDyadicGrid) (J : ℤ × ℤ) (S : Finset (ℤ × ℤ)) : Type

The scalar data of a delayed replacement on the use cells S below J (blueprint lem:delay, lines 1549–1553): the residuals D_h = (f_a - (P_h F_a)_phys) ψ_a at depth h, their predictor moments μ_h (constant on depth-h cells below every use cell, with the same cell integrals, eq:predictor-moment), energy densities e_h of the successive projection increments (Σ_h ∫_J e_h ≤ E, orthogonality of P_{h+1} - P_h), the private weight ε (the increments of μ cost ε e_h below the use cells), the bound of μ on the use cells of one depth (Σ_I ‖1_I μ_h‖² ≤ ε E), the depth N of the projection family (the predictor is present down to depth N) and the input mass |f_a|² (∫_J |f_a|² ≤ E, and the terminal residual is a contraction of it).

• N : ℤ

  Terminal depth of the delayed approximation.

• D : ℤ → ℝ → ℂ

  Depth-indexed scalar functions being approximated.

• μ : ℤ → ℝ → ℂ

  Delayed approximants at each depth.

• e : ℤ → ℝ → ℝ

  Pointwise error envelopes at each depth.

• ε : ℝ

  Relative error tolerance in the delayed approximation estimates.

• E : ℝ

  Integrated mass budget for the delayed approximation.

• ε_nonneg : 0 ≤ self.ε
• ε_le_one : self.ε ≤ 1
• sub (I : ℤ × ℤ) : I ∈ S → dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G J.1 J.2
• D_meas (h : ℤ) : Measurable (self.D h)
• D_memLp (I : ℤ × ℤ) : I ∈ S → ∀ (h : ℤ), MeasureTheory.MemLp (self.D h) 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))
• μ_memLp (I : ℤ × ℤ) : I ∈ S → ∀ (h : ℤ), MeasureTheory.MemLp (self.μ h) 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))
• μ_const (I : ℤ × ℤ) : I ∈ S → ∀ (j : ℕ), I.1 + ↑j ≤ self.N → ∀ Q ∈ dyadicGeneration G I j, ∀ y ∈ dyadicGridCell G Q.1 Q.2, ∀ z ∈ dyadicGridCell G Q.1 Q.2, self.μ (I.1 + ↑j) y = self.μ (I.1 + ↑j) z
• moment (I : ℤ × ℤ) : I ∈ S → ∀ (j : ℕ), I.1 + ↑j ≤ self.N → ∀ Q ∈ dyadicGeneration G I j, ∫ (y : ℝ) in dyadicGridCell G Q.1 Q.2, self.D (I.1 + ↑j) y = ∫ (y : ℝ) in dyadicGridCell G Q.1 Q.2, self.μ (I.1 + ↑j) y
• e_nonneg (h : ℤ) (y : ℝ) : 0 ≤ self.e h y
• e_int (h : ℤ) : MeasureTheory.IntegrableOn (self.e h) (dyadicGridCell G J.1 J.2) MeasureTheory.volume
• e_D (I : ℤ × ℤ) : I ∈ S → ∀ (h : ℤ), I.1 ≤ h → h < self.N → ∀ᵐ (y : ℝ) ∂MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2), ‖self.D h y - self.D (h + 1) y‖ ^ 2 ≤ self.e h y
• e_μ (I : ℤ × ℤ) : I ∈ S → ∀ (h : ℤ), I.1 ≤ h → h < self.N → ∀ᵐ (y : ℝ) ∂MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2), ‖self.μ (h + 1) y - self.μ h y‖ ^ 2 ≤ self.ε * self.e h y
• energy (Hs : Finset ℤ) : ∑ h ∈ Hs, ∫ (y : ℝ) in dyadicGridCell G J.1 J.2, self.e h y ≤ self.E
• mass : ℝ → ℝ

  Nonnegative integrable envelope controlling the terminal approximation energy.

• mass_nonneg (y : ℝ) : 0 ≤ self.mass y
• mass_int : MeasureTheory.IntegrableOn self.mass (dyadicGridCell G J.1 J.2) MeasureTheory.volume
• mass_le : ∫ (y : ℝ) in dyadicGridCell G J.1 J.2, self.mass y ≤ self.E
• D_final (I : ℤ × ℤ) : I ∈ S → ∫ (y : ℝ) in dyadicGridCell G I.1 I.2, ‖self.D self.N y‖ ^ 2 ≤ 4 * ∫ (y : ℝ) in dyadicGridCell G I.1 I.2, self.mass y
• μ_energy (S' : Finset (ℤ × ℤ)) : S' ⊆ S → ∀ (s : ℤ), (∀ I ∈ S', I.1 = s) → ∀ (h : ℤ), s ≤ h → h ≤ self.N → ∑ I ∈ S', ∫ (y : ℝ) in dyadicGridCell G I.1 I.2, ‖self.μ h y‖ ^ 2 ≤ self.ε * self.E

theorem TrilinearHT.Auto.DelayData.E_nonneg {G : RealDyadicGrid} {J : ℤ × ℤ} {S : Finset (ℤ × ℤ)} (Δ : DelayData G J S) : 0 ≤ Δ.E

theorem TrilinearHT.Auto.norm_waveRow_sq (G : RealDyadicGrid) (κ : LocalKernelClass) (α ν : ℤ × ℤ → ℝ) (I : ℤ × ℤ) (g : ℝ → ℂ) : ‖∫ (y : ℝ), (starRingEnd ℂ) (waveRowTest G κ id α ν (fun (x : ℝ) => 1) I y) * g y‖ ^ 2 = (dyadicGridLength G I.1)⁻¹ * ‖∫ (y : ℝ) in dyadicGridCell G I.1 I.2, g y * (classWave κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (α I) y * ↑(Real.fourierChar (ν I * y)))‖ ^ 2

The wave row of a cell input as a normalized set integral.

theorem TrilinearHT.Auto.delay_wave_rows (κ : LocalKernelClass) {G : RealDyadicGrid} {J : ℤ × ℤ} {S : Finset (ℤ × ℤ)} (Δ : DelayData G J S) (S' : Finset (ℤ × ℤ)) (hS' : S' ⊆ S) (α ν : ℤ × ℤ → ℝ) {A V : ℝ} (hA : ∀ I ∈ S', 2 * (kernelPlateau κ).K * (1 + 6 * Real.pi * (dyadicGridLength G I.1 * |α I|)) ^ 2 ≤ A) (hV : ∀ I ∈ S', dyadicGridLength G I.1 * |ν I| ≤ V) (hV0 : 0 ≤ V) (hA0 : 0 ≤ A) (K₀ : ℕ) (hN : ∀ I ∈ S', I.1 + ↑K₀ ≤ Δ.N) : ∑ I ∈ S', ‖∫ (y : ℝ), (starRingEnd ℂ) (waveRowTest G κ id α ν (fun (x : ℝ) => 1) I y) * Δ.D (I.1 + ↑K₀) y‖ ^ 2 ≤ 3 * ∑ I ∈ S', (dyadicGridLength G I.1)⁻¹ * ‖∫ (y : ℝ) in dyadicGridCell G I.1 I.2, Δ.μ (I.1 + ↑K₀) y * (classWave κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (α I) y * ↑(Real.fourierChar (ν I * y)))‖ ^ 2 + 3 * (9 * (2 * A + 4 * Real.pi * V + 2) * 2⁻¹ ^ K₀) ^ 2 * Δ.E

The delayed wave rows of a sub-collection: the telescoping part, with the start term left explicit.

noncomputable def TrilinearHT.Auto.depthMultConst : ℝ

The multiplicity constant of a fixed center over distinct depths.

Equations

• TrilinearHT.Auto.depthMultConst = 4 * (2 * Real.pi) ^ 2

theorem TrilinearHT.Auto.depthMultConst_pos : 0 < depthMultConst

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

The constant of the mean-zero part of the delayed replacement.

Equations

• TrilinearHT.Auto.delayZeroConst κ = TrilinearHT.Auto.linearScaleConst κ * TrilinearHT.Auto.depthMultConst * √(27 / (2 * TrilinearHT.Auto.depthMultConst))

theorem TrilinearHT.Auto.delayZeroConst_nonneg (κ : LocalKernelClass) : 0 ≤ delayZeroConst κ

theorem TrilinearHT.Auto.sum_image_const_snd {β : Type u_1} (S : Finset (ℤ × ℤ)) (c : ℝ) (f : ℤ × ℝ → β) [AddCommMonoid β] : ∑ p ∈ Finset.image (fun (I : ℤ × ℤ) => (I.1, c)) S, f p = ∑ s ∈ Finset.image Prod.fst S, f (s, c)

theorem TrilinearHT.Auto.delay_part_zero (κ : LocalKernelClass) {G : RealDyadicGrid} {J : ℤ × ℤ} {S : Finset (ℤ × ℤ)} (Δ : DelayData G J S) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (hw : ∀ I ∈ S, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) {a b : Fin 4} (hab : a ≠ b) {ψb : ℝ → ℂ} (hψbm : Measurable ψb) (hψb : ∀ (y : ℝ), ‖ψb y‖ ≤ 1) {Fb : ℝ → ℂ} {zb : ℤ × ℤ → ℝ → ℂ} {Kb : ℝ} (hKb : 0 ≤ Kb) (hzb : IsAdmissibleOpponent G J Fb zb Kb) (hzbm : ∀ (I : ℤ × ℤ), Measurable (zb I)) (hzbi : ∀ I ∈ S, MeasureTheory.IntegrableOn (zb I) (dyadicGridCell G I.1 I.2) MeasureTheory.volume) (K₀ : ℕ) (hN : ∀ I ∈ S, I.1 + ↑K₀ ≤ Δ.N) : ∑ I ∈ S, dyadicGridLength G I.1 * ‖separatedLocalForm (dyadicGridLength G I.1) (w I) (fun (t : ℝ) => ↑(Real.fourierChar (0 * t))) a b (fun (y : ℝ) => 1 * Δ.D (I.1 + ↑K₀) y) fun (y : ℝ) => ψb y * zb I y‖ ≤ delayZeroConst κ * (↑K₀ * √Δ.ε + 9 * 2⁻¹ ^ K₀) * √Δ.E * Kb * √(∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖Fb y‖ ^ 2)

Blueprint lem:delay, proof lines 1558–1559 with the kernel w_I itself: the mean-zero tensor rows of w_I against the delayed residuals, paired with the opposing Bessel rows, cost C (K₀ √ε + 2^{-K₀}) ‖F_a‖ ‖F_b‖.

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

The constant of the one-depth linear-phase part of the delayed replacement.

Equations

• TrilinearHT.Auto.delayLinConst κ = TrilinearHT.Auto.linearScaleConst κ * (2 * Real.pi) ^ 2 * √(147 / (2 * (2 * Real.pi) ^ 2))

theorem TrilinearHT.Auto.delayLinConst_nonneg (κ : LocalKernelClass) : 0 ≤ delayLinConst κ

theorem TrilinearHT.Auto.delay_linear_xrow (κ : LocalKernelClass) {G : RealDyadicGrid} {J : ℤ × ℤ} {S : Finset (ℤ × ℤ)} (Δ : DelayData G J S) (S' : Finset (ℤ × ℤ)) (hS' : S' ⊆ S) (s : ℤ) (hs : ∀ I ∈ S', I.1 = s) {a b : Fin 4} (hab : a ≠ b) (γ : ℝ) (K₀ : ℕ) (hN : ∀ I ∈ S', I.1 + ↑K₀ ≤ Δ.N) (v : Fin 2 → ℤ) : ∑ I ∈ S', ‖∫ (y : ℝ), (starRingEnd ℂ) (waveRowTest G κ id (fun (I : ℤ × ℤ) => slotPairFreqA a b (dyadicGridLength G (id I).1) v) (fun (x : ℤ × ℤ) => -(γ / (↑↑b - ↑↑a))) (fun (x : ℝ) => 1) I y) * Δ.D ((id I).1 + ↑K₀) y‖ ^ 2 ≤ (√(147 / (2 * (2 * Real.pi) ^ 2)) * (1 + dyadicGridLength G s * |γ|) * (√Δ.ε + 9 * 2⁻¹ ^ K₀) * √Δ.E) ^ 2 * (charWaveConst κ (frequencyLength v) * 1 * √(2 * (2 * Real.pi) ^ 2)) ^ 2 * 1 ^ 2

The delayed residual rows at one depth for a fixed linear phase.

theorem TrilinearHT.Auto.delay_linear_depth (κ : LocalKernelClass) {G : RealDyadicGrid} {J : ℤ × ℤ} {S : Finset (ℤ × ℤ)} (Δ : DelayData G J S) (S' : Finset (ℤ × ℤ)) (hS' : S' ⊆ S) (s : ℤ) (hs : ∀ I ∈ S', I.1 = s) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (hw : ∀ I ∈ S', IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) {a b : Fin 4} (hab : a ≠ b) (γ : ℝ) {ψb : ℝ → ℂ} (hψbm : Measurable ψb) (hψb : ∀ (y : ℝ), ‖ψb y‖ ≤ 1) {Fb : ℝ → ℂ} {zb : ℤ × ℤ → ℝ → ℂ} {Kb : ℝ} (hKb : 0 ≤ Kb) (hzb : IsAdmissibleOpponent G J Fb zb Kb) (hzbm : ∀ (I : ℤ × ℤ), Measurable (zb I)) (hzbi : ∀ I ∈ S', MeasureTheory.IntegrableOn (zb I) (dyadicGridCell G I.1 I.2) MeasureTheory.volume) (K₀ : ℕ) (hN : ∀ I ∈ S', I.1 + ↑K₀ ≤ Δ.N) : ∑ I ∈ S', dyadicGridLength G I.1 * ‖separatedLocalForm (dyadicGridLength G I.1) (w I) (fun (t : ℝ) => ↑(Real.fourierChar (γ * t))) a b (fun (y : ℝ) => 1 * Δ.D (I.1 + ↑K₀) y) fun (y : ℝ) => ψb y * zb I y‖ ≤ delayLinConst κ * (1 + dyadicGridLength G s * |γ|) * (√Δ.ε + 9 * 2⁻¹ ^ K₀) * √Δ.E * Kb * √(∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖Fb y‖ ^ 2)

Blueprint lem:delay, proof lines 1558 and 1562 at one depth: for a fixed linear phase e(γ t) on the use cells of a single depth s, the delayed residual rows (start term ‖1_J μ_H‖ ≤ √ε ‖F_a‖) paired with the opposing Bessel rows cost C (1 + |I_s| |γ|) (√ε + 2^{-K₀}) ‖F_a‖ ‖F_b‖.

noncomputable def TrilinearHT.Auto.chirpBump (χ : ℝ → ℝ) (D u : ℝ) : ℂ

The cut-off chirp (e(D u²) - 1) χ(u), the normalized form of e(λ_* t²) - 1 on a cell of length r with D = λ_* r² (blueprint lem:delay, line 1562).

Equations

• TrilinearHT.Auto.chirpBump χ D u = (↑(Real.fourierChar (D * (u * u))) - 1) * ↑(χ u)

theorem TrilinearHT.Auto.contDiff_fourierChar_comp {φ : ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) : ContDiff ℝ ↑⊤ fun (s : ℝ) => ↑(Real.fourierChar (φ s))

theorem TrilinearHT.Auto.chirpBump_geomBound {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) {Cχ : ℝ} (hCχ : ∀ i ≤ 3, ∀ (x : ℝ), |iteratedDeriv i χ x| ≤ Cχ) (D : ℝ) {u : ℝ} (hu : |u| ≤ 3) : GeomBound (chirpBump χ D) u ((18 * Real.pi * |D| + 2 * Real.pi * (2 * |D| * 3) * 1) * Cχ) (1 + (0 + (0 + 1) + (3 + 1) * (2 * Real.pi) * (max (|D| * (3 * 3)) 1 * (0 + (1 + 1)))) + 1) 3

Geometric derivative bounds of the cut-off chirp with the smallness factor |D|.

noncomputable def TrilinearHT.Auto.freqWeightOne : ℝ

The one-dimensional frequency weight Σ_v (1 + |v|)^{-2}.

Equations

• TrilinearHT.Auto.freqWeightOne = ∑' (v : Fin 1 → ℤ), ((1 + TrilinearHT.Auto.frequencyLength v) ^ 2)⁻¹

theorem TrilinearHT.Auto.summable_freqWeightOne : Summable fun (v : Fin 1 → ℤ) => ((1 + frequencyLength v) ^ 2)⁻¹

theorem TrilinearHT.Auto.freqWeightOne_nonneg : 0 ≤ freqWeightOne

noncomputable def TrilinearHT.Auto.bumpFourierConst : ℝ

The constant of the one-dimensional bump expansion.

Equations

• TrilinearHT.Auto.bumpFourierConst = 8192 * TrilinearHT.Auto.freqWeightOne

theorem TrilinearHT.Auto.bump_fourier_one {φ : ℝ → ℂ} (hφ : ContDiff ℝ (↑⊤) φ) (hsupp : ∀ (u : ℝ), φ u ≠ 0 → |u| ≤ 2) {A0 A3 : ℝ} (hA0 : ∀ (u : ℝ), ‖φ u‖ ≤ A0) (hA3 : ∀ (u : ℝ), ‖iteratedDeriv 3 φ u‖ ≤ A3) : ∃ (q : (Fin 1 → ℤ) → ℂ), (∀ (u : ℝ), |u| ≤ 4 → HasSum (fun (v : Fin 1 → ℤ) => q v * ↑(Real.fourierChar (↑(v 0) * (u / 8)))) (φ u)) ∧ (Summable fun (v : Fin 1 → ℤ) => ‖q v‖ * (1 + frequencyLength v)) ∧ ∑' (v : Fin 1 → ℤ), ‖q v‖ * (1 + frequencyLength v) ≤ bumpFourierConst * (A0 + A3)

A smooth bump on [-2, 2] is, on [-4, 4], the absolutely convergent sum of the linear phases e(v u / 8), with Σ_v |q_v| (1 + |v|) ≤ C (sup |φ| + sup |φ'''|).

theorem TrilinearHT.Auto.chirp_fourier : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (D : ℝ), ∃ (q : (Fin 1 → ℤ) → ℂ), (∀ (u : ℝ), |u| ≤ 1 → HasSum (fun (v : Fin 1 → ℤ) => q v * ↑(Real.fourierChar (↑(v 0) * (u / 8)))) (↑(Real.fourierChar (D * u ^ 2)) - 1)) ∧ (Summable fun (v : Fin 1 → ℤ) => ‖q v‖ * (1 + frequencyLength v)) ∧ ∑' (v : Fin 1 → ℤ), ‖q v‖ * (1 + frequencyLength v) ≤ C * |D| * (1 + |D|) ^ 3

Blueprint lem:delay, line 1562 (smooth expansion of e(λ_* t²) - 1): on |u| ≤ 1, e(D u²) - 1 is an absolutely convergent sum of linear phases e(v u / 8) whose weighted coefficient norm is at most C |D| (1 + |D|)³.

noncomputable def TrilinearHT.Auto.chirpConst : ℝ

The constant of chirp_fourier.

Equations

• TrilinearHT.Auto.chirpConst = Classical.choose TrilinearHT.Auto.chirp_fourier

theorem TrilinearHT.Auto.chirpConst_spec : 0 ≤ chirpConst ∧ ∀ (D : ℝ), ∃ (q : (Fin 1 → ℤ) → ℂ), (∀ (u : ℝ), |u| ≤ 1 → HasSum (fun (v : Fin 1 → ℤ) => q v * ↑(Real.fourierChar (↑(v 0) * (u / 8)))) (↑(Real.fourierChar (D * u ^ 2)) - 1)) ∧ (Summable fun (v : Fin 1 → ℤ) => ‖q v‖ * (1 + frequencyLength v)) ∧ ∑' (v : Fin 1 → ℤ), ‖q v‖ * (1 + frequencyLength v) ≤ chirpConst * |D| * (1 + |D|) ^ 3

theorem TrilinearHT.Auto.delay_chirp_depth (κ : LocalKernelClass) {G : RealDyadicGrid} {J : ℤ × ℤ} {S : Finset (ℤ × ℤ)} (Δ : DelayData G J S) (S' : Finset (ℤ × ℤ)) (hS' : S' ⊆ S) (s : ℤ) (hs : ∀ I ∈ S', I.1 = s) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (hw : ∀ I ∈ S', IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) {a b : Fin 4} (hab : a ≠ b) (lam : ℝ) {ψb : ℝ → ℂ} (hψbm : Measurable ψb) (hψb : ∀ (y : ℝ), ‖ψb y‖ ≤ 1) {Fb : ℝ → ℂ} {zb : ℤ × ℤ → ℝ → ℂ} {Kb : ℝ} (hKb : 0 ≤ Kb) (hzb : IsAdmissibleOpponent G J Fb zb Kb) (hzbm : ∀ (I : ℤ × ℤ), Measurable (zb I)) (hzb2 : ∀ I ∈ S', MeasureTheory.MemLp (zb I) 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) (K₀ : ℕ) (hN : ∀ I ∈ S', I.1 + ↑K₀ ≤ Δ.N) : ∑ I ∈ S', dyadicGridLength G I.1 * ‖separatedLocalForm (dyadicGridLength G I.1) (w I) (fun (t : ℝ) => ↑(Real.fourierChar (lam * t ^ 2)) - 1) a b (fun (y : ℝ) => 1 * Δ.D (I.1 + ↑K₀) y) fun (y : ℝ) => ψb y * zb I y‖ ≤ delayLinConst κ * chirpConst * (|lam * dyadicGridLength G s ^ 2| * (1 + |lam * dyadicGridLength G s ^ 2|) ^ 3) * (√Δ.ε + 9 * 2⁻¹ ^ K₀) * √Δ.E * Kb * √(∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖Fb y‖ ^ 2)

Blueprint lem:delay, proof line 1562 at one depth: the smooth tensor expansion of w_I (e(λ_* t²) - 1) in linear phases costs C |λ_*| r² (1 + |λ_*| r²)³ times the one-depth linear-phase bound.

theorem TrilinearHT.Auto.depth_sq_sum_le (G : RealDyadicGrid) (Ds : Finset ℤ) (hne : Ds.Nonempty) : ∑ s ∈ Ds, dyadicGridLength G s ^ 2 ≤ 2 * dyadicGridLength G (Ds.min' hne) ^ 2

Squared lengths of distinct depths sum to at most twice the largest one.

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

The constant of the delayed replacement.

Equations

• TrilinearHT.Auto.delayConst κ = 9 * TrilinearHT.Auto.delayZeroConst κ + 18 * TrilinearHT.Auto.delayLinConst κ * TrilinearHT.Auto.chirpConst

theorem TrilinearHT.Auto.delayConst_nonneg (κ : LocalKernelClass) : 0 ≤ delayConst κ

theorem TrilinearHT.Auto.delay_error_bound (κ : LocalKernelClass) {G : RealDyadicGrid} {J : ℤ × ℤ} {S : Finset (ℤ × ℤ)} (Δ : DelayData G J S) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (hw : ∀ I ∈ S, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) {a b : Fin 4} (hab : a ≠ b) (lam : ℝ) {Dp : ℝ} (hDp0 : 0 ≤ Dp) (hDp : ∀ I ∈ S, |lam| * dyadicGridLength G I.1 ^ 2 ≤ Dp) {ψb : ℝ → ℂ} (hψbm : Measurable ψb) (hψb : ∀ (y : ℝ), ‖ψb y‖ ≤ 1) {Fb : ℝ → ℂ} {zb : ℤ × ℤ → ℝ → ℂ} {Kb : ℝ} (hKb : 0 ≤ Kb) (hzb : IsAdmissibleOpponent G J Fb zb Kb) (hzbm : ∀ (I : ℤ × ℤ), Measurable (zb I)) (hzb2 : ∀ I ∈ S, MeasureTheory.MemLp (zb I) 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) (K₀ : ℕ) (hN : ∀ I ∈ S, I.1 + ↑K₀ ≤ Δ.N) : ∑ I ∈ S, dyadicGridLength G I.1 * ‖separatedLocalForm (dyadicGridLength G I.1) (w I) (fun (t : ℝ) => ↑(Real.fourierChar (lam * t ^ 2))) a b (Δ.D (I.1 + ↑K₀)) fun (y : ℝ) => ψb y * zb I y‖ ≤ delayConst κ * (2⁻¹ ^ K₀ + (1 + ↑K₀) * √Δ.ε) * (1 + Dp) ^ 4 * √Δ.E * Kb * √(∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖Fb y‖ ^ 2)

Blueprint lem:delay, eq:delay-error: replacing the position-a input at each use cell of depth s by its projection at depth s + K₀ changes the length-weighted scale sum of a fixed predictor term w_I(x,t) e(λ_* t²) (with |λ_*| |I|² ≤ D_pred) against an admissible opponent by at most C (2^{-K₀} + (1 + K₀) √ε) (1 + D_pred)⁴ ‖F_a‖ ‖F_b‖; here the delayed residual D_{s+K₀} carries the multiplier ψ_a, E = ‖1_J F_a‖² bounds the projection energies and K_b is the opponent's transfer constant.

The position-a projection family

structure TrilinearHT.Auto.ColumnDepthFamily (V : Type u_1) [Fintype V] : Type u_1

A column tree that is complete down to depth N below its root, with a fixed inherited mask: the nested depth projections P_h of blueprint lem:delay (line 1549), on the direct-sum partitions of the root into its depth-h cells.

• D : ColumnTreeData V

  Column-tree data used by the depth-indexed family.

• A : InheritedColumnMask self.D

  Inherited column mask on the depth-indexed tree.

• N : ℤ

  Last depth represented by the column family.

• root_le : self.D.root.1 ≤ self.N
• complete (c : ℤ × ℤ) : dyadicGridCell self.D.grid c.1 c.2 ⊆ dyadicGridCell self.D.grid self.D.root.1 self.D.root.2 → c.1 ≤ self.N → c ∈ self.D.cells

def TrilinearHT.Auto.ColumnDepthFamily.depth {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (h : ℤ) : ℤ

The depth used at level h: h clamped to [root, N].

Equations

• Ψ.depth h = max Ψ.D.root.1 (min h Ψ.N)

theorem TrilinearHT.Auto.ColumnDepthFamily.root_le_depth {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (h : ℤ) : Ψ.D.root.1 ≤ Ψ.depth h

theorem TrilinearHT.Auto.ColumnDepthFamily.depth_le {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (h : ℤ) : Ψ.depth h ≤ Ψ.N

theorem TrilinearHT.Auto.ColumnDepthFamily.depth_eq {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) {h : ℤ} (h1 : Ψ.D.root.1 ≤ h) (h2 : h ≤ Ψ.N) : Ψ.depth h = h

theorem TrilinearHT.Auto.ColumnDepthFamily.depth_mono {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) {h h' : ℤ} (hh : h ≤ h') : Ψ.depth h ≤ Ψ.depth h'

noncomputable def TrilinearHT.Auto.ColumnDepthFamily.partition {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (h : ℤ) : ColumnStoppingPartition Ψ.D

The partition of the root into its cells of depth depth h.

Equations

• Ψ.partition h = { cells := TrilinearHT.Auto.dyadicGeneration Ψ.D.grid Ψ.D.root (Ψ.depth h - Ψ.D.root.1).toNat, subset := ⋯, disjoint := ⋯, cover := ⋯ }

theorem TrilinearHT.Auto.ColumnDepthFamily.mem_partition {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (h : ℤ) (c : ℤ × ℤ) : c ∈ (Ψ.partition h).cells ↔ c.1 = Ψ.depth h ∧ dyadicGridCell Ψ.D.grid c.1 c.2 ⊆ dyadicGridCell Ψ.D.grid Ψ.D.root.1 Ψ.D.root.2

noncomputable def TrilinearHT.Auto.ColumnDepthFamily.proj {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (h : ℤ) : ↥(ColumnL2 V) →L[ℂ] ↥(ColumnL2 V)

The depth projection P_h.

Equations

• Ψ.proj h = TrilinearHT.Auto.partitionColumnProjection Ψ.D Ψ.A (Ψ.partition h)

theorem TrilinearHT.Auto.ColumnDepthFamily.isStarProjection_proj {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (h : ℤ) : IsStarProjection (Ψ.proj h)

theorem TrilinearHT.Auto.ancestor_below_root (G : RealDyadicGrid) (J c : ℤ × ℤ) (hc : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G J.1 J.2) {k : ℤ} (hJk : J.1 ≤ k) (hkc : k ≤ c.1) : ∃ (m : ℤ), dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G k m ∧ dyadicGridCell G k m ⊆ dyadicGridCell G J.1 J.2

Cells below the root of depth at least the root's are contained in the root's cell along with their ancestors.

theorem TrilinearHT.Auto.ColumnDepthFamily.proj_nested {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) {h h' : ℤ} (hh : h ≤ h') : Ψ.proj h ∘SL Ψ.proj h' = Ψ.proj h

The depth projections are nested.

theorem TrilinearHT.Auto.ColumnDepthFamily.proj_ae_cell {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (h : ℤ) (z : ↥(ColumnL2 V)) {Q : ℤ × ℤ} (hQ : Q ∈ (Ψ.partition h).cells) : ↑↑((Ψ.proj h) z) =ᵐ[MeasureTheory.volume.restrict (dyadicGridCell Ψ.D.grid Q.1 Q.2)] ↑↑((cellColumnProjection Ψ.D Ψ.A ⋯) z)

On a cell of the depth-h partition, P_h z agrees a.e. with the cell projection.

theorem TrilinearHT.Auto.ColumnDepthFamily.depth_of_mem {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) {h : ℤ} (h1 : Ψ.D.root.1 ≤ h) (h2 : h ≤ Ψ.N) {Q : ℤ × ℤ} (hQ1 : Q.1 = h) (hQ : dyadicGridCell Ψ.D.grid Q.1 Q.2 ⊆ dyadicGridCell Ψ.D.grid Ψ.D.root.1 Ψ.D.root.2) : Q ∈ (Ψ.partition h).cells

theorem TrilinearHT.Auto.ColumnDepthFamily.proj_ae_combination {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (h : ℤ) (z : ↥(ColumnL2 V)) {Q : ℤ × ℤ} (hQ : Q ∈ (Ψ.partition h).cells) : ∀ᵐ (y : ℝ) ∂MeasureTheory.volume.restrict (dyadicGridCell Ψ.D.grid Q.1 Q.2), ↑↑((Ψ.proj h) z) y = columnCombination Ψ.D Ψ.A Q (cellProjectionCoefficients Ψ.D Ψ.A ⋯ z) y

On a partition cell, P_h z is a.e. the constant-coefficient column combination.

noncomputable def TrilinearHT.Auto.ColumnDepthFamily.resid {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (ψa : ℝ → ℂ) (h : ℤ) (y : ℝ) : ℂ

The delayed residual D_h = (f - (P_h F)_phys) ψ_a of a physical input.

Equations

• Ψ.resid f ψa h y = (↑↑f y - (↑↑((Ψ.proj h) (TrilinearHT.Auto.physicalColumnInput f)) y).ofLp none) * ψa y

theorem TrilinearHT.Auto.ColumnDepthFamily.integral_resid {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) {ψa : ℝ → ℂ} {p : V} (hscal : ∀ (y : ℝ), Ψ.D.scalar p y = star (ψa y)) (h : ℤ) {Q : ℤ × ℤ} (hQ : Q ∈ (Ψ.partition h).cells) (hp : p ∈ Ψ.A.labels Q) : ↑(dyadicGridLength Ψ.D.grid Q.1)⁻¹ * ∫ (y : ℝ) in dyadicGridCell Ψ.D.grid Q.1 Q.2, Ψ.resid f ψa h y = ↑(Ψ.D.privateWeight p) * (cellProjectionCoefficients Ψ.D Ψ.A ⋯ (physicalColumnInput f)).ofLp ⟨p, hp⟩

The predictor moment on a partition cell (eq:predictor-moment): if the predictor (ψBar_a, √ε e_p) is available on Q, the cell average of the residual is ε times the predictor's coefficient.

theorem TrilinearHT.Auto.ColumnDepthFamily.proj_private_ae {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (h : ℤ) (z : ↥(ColumnL2 V)) {Q : ℤ × ℤ} (hQ : Q ∈ (Ψ.partition h).cells) {p : V} (hp : p ∈ Ψ.A.labels Q) : ∀ᵐ (y : ℝ) ∂MeasureTheory.volume.restrict (dyadicGridCell Ψ.D.grid Q.1 Q.2), (↑↑((Ψ.proj h) z) y).ofLp (some p) = (cellProjectionCoefficients Ψ.D Ψ.A ⋯ z).ofLp ⟨p, hp⟩ * ↑√(Ψ.D.privateWeight p)

The private coordinate of P_h F on a partition cell.

theorem TrilinearHT.Auto.ColumnDepthFamily.moment_ae {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) {ψa : ℝ → ℂ} {p : V} (hscal : ∀ (y : ℝ), Ψ.D.scalar p y = star (ψa y)) {I : ℤ × ℤ} (hI : dyadicGridCell Ψ.D.grid I.1 I.2 ⊆ dyadicGridCell Ψ.D.grid Ψ.D.root.1 Ψ.D.root.2) (havail : ∀ c ∈ Ψ.D.cells, dyadicGridCell Ψ.D.grid c.1 c.2 ⊆ dyadicGridCell Ψ.D.grid I.1 I.2 → p ∈ Ψ.A.labels c) {h : ℤ} (hIh : I.1 ≤ h) (hhN : h ≤ Ψ.N) : ∀ᵐ (y : ℝ) ∂MeasureTheory.volume.restrict (dyadicGridCell Ψ.D.grid I.1 I.2), depthExpectation Ψ.D.grid h (Ψ.resid f ψa h) y = ↑√(Ψ.D.privateWeight p) * (↑↑((Ψ.proj h) (physicalColumnInput f)) y).ofLp (some p)

Blueprint lem:delay, line 1550: below a use cell carrying the predictor, the conditional expectation of the residual at depth h is √ε times the private coordinate, μ_h = E_h D_h = ε a_{h,p}.

theorem TrilinearHT.Auto.physicalColumnInput_ae {V : Type u_1} [Fintype V] (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ∀ᵐ (y : ℝ), ‖↑↑(physicalColumnInput f) y‖ = ‖↑↑f y‖ ∧ (↑↑(physicalColumnInput f) y).ofLp none = ↑↑f y

theorem TrilinearHT.Auto.ColumnDepthFamily.proj_restrict_root {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (h : ℤ) (z : ↥(ColumnL2 V)) : (Ψ.proj h) ((columnL2Restriction (dyadicGridCell Ψ.D.grid Ψ.D.root.1 Ψ.D.root.2) ⋯) z) = (Ψ.proj h) z

The depth projections only see the input on the root.

theorem TrilinearHT.Auto.setIntegral_cell_eq_sum_generation_real (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

Integrals over a cell split along its depth-(s+n) generation (real-valued version).

theorem TrilinearHT.Auto.integrableOn_norm_sq_Lp {V : Type u_1} [Fintype V] (z : ↥(ColumnL2 V)) (s : Set ℝ) : MeasureTheory.IntegrableOn (fun (y : ℝ) => ‖↑↑z y‖ ^ 2) s MeasureTheory.volume

theorem TrilinearHT.Auto.ColumnDepthFamily.setIntegral_proj_le {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (h : ℤ) (z : ↥(ColumnL2 V)) {I : ℤ × ℤ} (hI : dyadicGridCell Ψ.D.grid I.1 I.2 ⊆ dyadicGridCell Ψ.D.grid Ψ.D.root.1 Ψ.D.root.2) (hIh : I.1 ≤ Ψ.depth h) : ∫ (y : ℝ) in dyadicGridCell Ψ.D.grid I.1 I.2, ‖↑↑((Ψ.proj h) z) y‖ ^ 2 ≤ ∫ (y : ℝ) in dyadicGridCell Ψ.D.grid I.1 I.2, ‖↑↑z y‖ ^ 2

Local contraction: on a cell I of depth at most the depth of P_h, ‖1_I P_h z‖ ≤ ‖1_I z‖.

theorem TrilinearHT.Auto.ColumnDepthFamily.proj_eq_of_depth {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) {h h' : ℤ} (hd : Ψ.depth h = Ψ.depth h') : Ψ.proj h = Ψ.proj h'

theorem TrilinearHT.Auto.ColumnDepthFamily.increment_energy {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (z : ↥(ColumnL2 V)) (Hs : Finset ℤ) : ∑ h ∈ Hs, ∫ (y : ℝ) in dyadicGridCell Ψ.D.grid Ψ.D.root.1 Ψ.D.root.2, ‖↑↑((Ψ.proj (h + 1)) z) y - ↑↑((Ψ.proj h) z) y‖ ^ 2 ≤ ∫ (y : ℝ) in dyadicGridCell Ψ.D.grid Ψ.D.root.1 Ψ.D.root.2, ‖↑↑z y‖ ^ 2

Blueprint lem:delay, line 1558 (orthogonality of P_{h+1} - P_h): the successive increments of the depth projections have total energy at most ‖1_J z‖².

theorem TrilinearHT.Auto.measurable_column_coord {V : Type u_1} [Fintype V] (z : ↥(ColumnL2 V)) (i : Option V) : Measurable fun (y : ℝ) => (↑↑z y).ofLp i

theorem TrilinearHT.Auto.memLp_column_coord {V : Type u_1} [Fintype V] (z : ↥(ColumnL2 V)) (i : Option V) : MeasureTheory.MemLp (fun (y : ℝ) => (↑↑z y).ofLp i) 2 MeasureTheory.volume

theorem TrilinearHT.Auto.ColumnDepthFamily.measurable_resid {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) {ψa : ℝ → ℂ} (hψm : Measurable ψa) (h : ℤ) : Measurable (Ψ.resid f ψa h)

theorem TrilinearHT.Auto.ColumnDepthFamily.memLp_resid {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) {ψa : ℝ → ℂ} (hψm : Measurable ψa) (hψ : ∀ (y : ℝ), ‖ψa y‖ ≤ 1) (h : ℤ) : MeasureTheory.MemLp (Ψ.resid f ψa h) 2 MeasureTheory.volume

theorem TrilinearHT.Auto.norm_depthExpectation_le_L2 (G : RealDyadicGrid) (h : ℤ) {g : ℝ → ℂ} (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) (y : ℝ) : ‖depthExpectation G h g y‖ ≤ (√(dyadicGridLength G h))⁻¹ * √(∫ (x : ℝ), ‖g x‖ ^ 2)

|E_h g| ≤ |I_h|^{-1/2} ‖g‖₂ pointwise.

theorem TrilinearHT.Auto.memLp_depthExpectation (G : RealDyadicGrid) (h : ℤ) {g : ℝ → ℂ} (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) (s : Set ℝ) (hs : MeasureTheory.volume s < ⊤) : MeasureTheory.MemLp (depthExpectation G h g) 2 (MeasureTheory.volume.restrict s)

theorem TrilinearHT.Auto.norm_coord_le {V : Type u_1} [Fintype V] (x : ColumnHilbert V) (i : Option V) : ‖x.ofLp i‖ ≤ ‖x‖

theorem TrilinearHT.Auto.ColumnDepthFamily.resid_sub_le {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) {ψa : ℝ → ℂ} (hψ : ∀ (y : ℝ), ‖ψa y‖ ≤ 1) (h : ℤ) (y : ℝ) : ‖Ψ.resid f ψa h y - Ψ.resid f ψa (h + 1) y‖ ^ 2 ≤ ‖↑↑((Ψ.proj (h + 1)) (physicalColumnInput f)) y - ↑↑((Ψ.proj h) (physicalColumnInput f)) y‖ ^ 2

theorem TrilinearHT.Auto.ColumnDepthFamily.moment_sub_ae {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) {ψa : ℝ → ℂ} {p : V} (hscal : ∀ (y : ℝ), Ψ.D.scalar p y = star (ψa y)) {I : ℤ × ℤ} (hI : dyadicGridCell Ψ.D.grid I.1 I.2 ⊆ dyadicGridCell Ψ.D.grid Ψ.D.root.1 Ψ.D.root.2) (havail : ∀ c ∈ Ψ.D.cells, dyadicGridCell Ψ.D.grid c.1 c.2 ⊆ dyadicGridCell Ψ.D.grid I.1 I.2 → p ∈ Ψ.A.labels c) {h : ℤ} (hIh : I.1 ≤ h) (hhN : h < Ψ.N) : ∀ᵐ (y : ℝ) ∂MeasureTheory.volume.restrict (dyadicGridCell Ψ.D.grid I.1 I.2), ‖depthExpectation Ψ.D.grid (h + 1) (Ψ.resid f ψa (h + 1)) y - depthExpectation Ψ.D.grid h (Ψ.resid f ψa h) y‖ ^ 2 ≤ Ψ.D.privateWeight p * ‖↑↑((Ψ.proj (h + 1)) (physicalColumnInput f)) y - ↑↑((Ψ.proj h) (physicalColumnInput f)) y‖ ^ 2

theorem TrilinearHT.Auto.integral_physical_sq {V : Type u_1} [Fintype V] (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (s : Set ℝ) : ∫ (y : ℝ) in s, ‖↑↑(physicalColumnInput f) y‖ ^ 2 = ∫ (y : ℝ) in s, ‖↑↑f y‖ ^ 2

noncomputable def TrilinearHT.Auto.ColumnDepthFamily.delayData {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) {ψa : ℝ → ℂ} (hψm : Measurable ψa) (hψ : ∀ (y : ℝ), ‖ψa y‖ ≤ 1) {p : V} (hscal : ∀ (y : ℝ), Ψ.D.scalar p y = star (ψa y)) (hε1 : Ψ.D.privateWeight p ≤ 1) (S : Finset (ℤ × ℤ)) (hS : ∀ I ∈ S, dyadicGridCell Ψ.D.grid I.1 I.2 ⊆ dyadicGridCell Ψ.D.grid Ψ.D.root.1 Ψ.D.root.2) (hSN : ∀ I ∈ S, I.1 ≤ Ψ.N) (havail : ∀ I ∈ S, ∀ c ∈ Ψ.D.cells, dyadicGridCell Ψ.D.grid c.1 c.2 ⊆ dyadicGridCell Ψ.D.grid I.1 I.2 → p ∈ Ψ.A.labels c) : DelayData Ψ.D.grid Ψ.D.root S

Blueprint lem:delay, lines 1549–1553: a position-a projection family carrying the predictor (ψBar_a, √ε e_p) on every use cell and its descendants, down to the depth N, gives the scalar delay data: the residuals (f_a - (P_h F_a)_phys) ψ_a, their dyadic conditional expectations, and the energies of the projection increments.

Equations

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

theorem TrilinearHT.Auto.separatedLocalForm_sub_left {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {a b : Fin 4} (hab : a ≠ b) {Q : ℝ → ℂ} (hQ : Measurable Q) {C : ℝ} (hQb : ∀ (t : ℝ), ‖Q t‖ ≤ C) {Fa₁ Fa₂ Fb : ℝ → ℂ} (hF₁m : Measurable Fa₁) (hF₂m : Measurable Fa₂) (hFbm : Measurable Fb) (hF₁ : MeasureTheory.MemLp Fa₁ 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) (hF₂ : MeasureTheory.MemLp Fa₂ 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) (hFb : MeasureTheory.MemLp Fb 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) : separatedLocalForm r w Q a b (fun (y : ℝ) => Fa₁ y - Fa₂ y) Fb = separatedLocalForm r w Q a b Fa₁ Fb - separatedLocalForm r w Q a b Fa₂ Fb

The separated form is additive (subtractive) in the position-a input.

theorem TrilinearHT.Auto.delayedPredictorReplacement {V : Type u_1} [Fintype V] (κ : LocalKernelClass) (Ψ : ColumnDepthFamily V) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) {ψa : ℝ → ℂ} (hψm : Measurable ψa) (hψ : ∀ (y : ℝ), ‖ψa y‖ ≤ 1) {p : V} (hscal : ∀ (y : ℝ), Ψ.D.scalar p y = star (ψa y)) (hε1 : Ψ.D.privateWeight p ≤ 1) (S : Finset (ℤ × ℤ)) (hS : ∀ I ∈ S, dyadicGridCell Ψ.D.grid I.1 I.2 ⊆ dyadicGridCell Ψ.D.grid Ψ.D.root.1 Ψ.D.root.2) (havail : ∀ I ∈ S, ∀ c ∈ Ψ.D.cells, dyadicGridCell Ψ.D.grid c.1 c.2 ⊆ dyadicGridCell Ψ.D.grid I.1 I.2 → p ∈ Ψ.A.labels c) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (hw : ∀ I ∈ S, IsAdmissibleLocalKernel κ (dyadicGridLeft Ψ.D.grid I.1 I.2) (dyadicGridLength Ψ.D.grid I.1) (w I)) {a b : Fin 4} (hab : a ≠ b) (lam : ℝ) {Dp : ℝ} (hDp0 : 0 ≤ Dp) (hDp : ∀ I ∈ S, |lam| * dyadicGridLength Ψ.D.grid I.1 ^ 2 ≤ Dp) {ψb : ℝ → ℂ} (hψbm : Measurable ψb) (hψb : ∀ (y : ℝ), ‖ψb y‖ ≤ 1) {Fb : ℝ → ℂ} {zb : ℤ × ℤ → ℝ → ℂ} {Kb : ℝ} (hKb : 0 ≤ Kb) (hzb : IsAdmissibleOpponent Ψ.D.grid Ψ.D.root Fb zb Kb) (hzbm : ∀ (I : ℤ × ℤ), Measurable (zb I)) (hzb2 : ∀ I ∈ S, MeasureTheory.MemLp (zb I) 2 (MeasureTheory.volume.restrict (dyadicGridCell Ψ.D.grid I.1 I.2))) (K₀ : ℕ) (hN : ∀ I ∈ S, I.1 + ↑K₀ ≤ Ψ.N) : ∑ I ∈ S, dyadicGridLength Ψ.D.grid I.1 * ‖(separatedLocalForm (dyadicGridLength Ψ.D.grid I.1) (w I) (fun (t : ℝ) => ↑(Real.fourierChar (lam * t ^ 2))) a b (fun (y : ℝ) => ↑↑f y * ψa y) fun (y : ℝ) => ψb y * zb I y) - separatedLocalForm (dyadicGridLength Ψ.D.grid I.1) (w I) (fun (t : ℝ) => ↑(Real.fourierChar (lam * t ^ 2))) a b (fun (y : ℝ) => (↑↑((Ψ.proj (I.1 + ↑K₀)) (physicalColumnInput f)) y).ofLp none * ψa y) fun (y : ℝ) => ψb y * zb I y‖ ≤ delayConst κ * (2⁻¹ ^ K₀ + (1 + ↑K₀) * √(Ψ.D.privateWeight p)) * (1 + Dp) ^ 4 * √(∫ (y : ℝ) in dyadicGridCell Ψ.D.grid Ψ.D.root.1 Ψ.D.root.2, ‖↑↑f y‖ ^ 2) * Kb * √(∫ (y : ℝ) in dyadicGridCell Ψ.D.grid Ψ.D.root.1 Ψ.D.root.2, ‖Fb y‖ ^ 2)

Blueprint lem:delay (Declaration delay, line 1566), eq:delay-error: let the position-a projection family P_h (nested direct-sum projections on the depth-h partitions of the root J, complete down to depth N) contain the predictor (ψBar_a, √ε e_p) on every use cell and its descendants. Replacing the input f_a ψ_a at each use cell I of depth s by (P_{s+K₀} F_a)_phys ψ_a changes the length-weighted scale sum of a fixed predictor term w_I(x,t) e(λ_* t²), |λ_*| |I|² ≤ D_pred, against an admissible opponent by at most C (2^{-K₀} + (1 + K₀) √ε) (1 + D_pred)⁴ K_b ‖1_J F_a‖ ‖1_J F_b‖ (the transfer constant K_b of the opponent carries the polynomial in log(2 D_h) and 1 + L).

theorem TrilinearHT.Auto.ColumnDepthFamily.rolling_energy {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (z : ↥(ColumnL2 V)) (K₀ : ℕ) (S : Finset (ℤ × ℤ)) (hS : ∀ I ∈ S, dyadicGridCell Ψ.D.grid I.1 I.2 ⊆ dyadicGridCell Ψ.D.grid Ψ.D.root.1 Ψ.D.root.2) : ∑ I ∈ S, ∫ (y : ℝ) in dyadicGridCell Ψ.D.grid I.1 I.2, ‖↑↑((Ψ.proj (I.1 + ↑K₀)) z) y - ↑↑((Ψ.proj I.1) z) y‖ ^ 2 ≤ ↑K₀ ^ 2 * ∫ (y : ℝ) in dyadicGridCell Ψ.D.grid Ψ.D.root.1 Ψ.D.root.2, ‖↑↑z y‖ ^ 2

Blueprint lem:delay, lines 1563–1565 (sequential replacement): the rolling differences (P_{s+K₀} - P_s) F restricted to the cells I of depth s have square energy at most K₀² ‖1_J F‖² (each increment is counted at most K₀ times), so they form an admissible square-energy opponent with transfer constant K₀.

Current projections as admissible opponents

noncomputable def TrilinearHT.Auto.ColumnDepthFamily.anc {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (I : ℤ × ℤ) : ℤ × ℤ

The tree cell used for a row cell I: its ancestor at depth min I.1 N.

Equations

• Ψ.anc I = (min I.1 Ψ.N, TrilinearHT.Auto.dyadicIndex Ψ.D.grid (min I.1 Ψ.N) (TrilinearHT.Auto.dyadicGridLeft Ψ.D.grid I.1 I.2))

theorem TrilinearHT.Auto.ColumnDepthFamily.cell_sub_anc {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (I : ℤ × ℤ) : dyadicGridCell Ψ.D.grid I.1 I.2 ⊆ dyadicGridCell Ψ.D.grid (Ψ.anc I).1 (Ψ.anc I).2

theorem TrilinearHT.Auto.ColumnDepthFamily.cell_sub_anc_root {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) {I : ℤ × ℤ} (hI : dyadicGridCell Ψ.D.grid I.1 I.2 ⊆ dyadicGridCell Ψ.D.grid Ψ.D.root.1 Ψ.D.root.2) : dyadicGridCell Ψ.D.grid (Ψ.anc I).1 (Ψ.anc I).2 ⊆ dyadicGridCell Ψ.D.grid Ψ.D.root.1 Ψ.D.root.2

theorem TrilinearHT.Auto.ColumnDepthFamily.anc_mem {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) {I : ℤ × ℤ} (hI : dyadicGridCell Ψ.D.grid I.1 I.2 ⊆ dyadicGridCell Ψ.D.grid Ψ.D.root.1 Ψ.D.root.2) : Ψ.anc I ∈ Ψ.D.cells

noncomputable def TrilinearHT.Auto.ColumnDepthFamily.current {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (I : ℤ × ℤ) (y : ℝ) : ℂ

The current projection opponent z_I = (P_{u(I)} F)_phys (blueprint sec:base, line 1482; lem:predictors, line 1532), with u(I) the tree cell above I.

Equations

• Ψ.current f I y = if h : Ψ.anc I ∈ Ψ.D.cells then (↑↑((TrilinearHT.Auto.cellColumnProjection Ψ.D Ψ.A h) (TrilinearHT.Auto.physicalColumnInput f)) y).ofLp none else 0

noncomputable def TrilinearHT.Auto.physicalCoordLp (V : Type u_2) [Fintype V] : ↥(ColumnL2 V) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

The physical coordinate as a contraction L²(ℝ; ℂ ⊕ ℓ²(V)) → L²(ℝ).

Equations

• TrilinearHT.Auto.physicalCoordLp V = ContinuousLinearMap.compLpL 2 MeasureTheory.volume (EuclideanSpace.proj none)

theorem TrilinearHT.Auto.physicalCoordLp_coeFn {V : Type u_1} [Fintype V] (w : ↥(ColumnL2 V)) : ↑↑((physicalCoordLp V) w) =ᵐ[MeasureTheory.volume] fun (y : ℝ) => (↑↑w y).ofLp none

theorem TrilinearHT.Auto.norm_physicalCoordLp_le {V : Type u_1} [Fintype V] (w : ↥(ColumnL2 V)) : ‖(physicalCoordLp V) w‖ ≤ ‖w‖

theorem TrilinearHT.Auto.cellRow_inner {V : Type u_1} [Fintype V] {G : RealDyadicGrid} {ι : Type} (R : CellRowFamily G ι) (i : ι) (w : ↥(ColumnL2 V)) : inner ℂ (MeasureTheory.MemLp.toLp (R.test i) ⋯) ((physicalCoordLp V) w) = ∫ (y : ℝ), (starRingEnd ℂ) (R.test i y) * (↑↑w y).ofLp none

The value of a row on a column input.

noncomputable def TrilinearHT.Auto.compressionOneConst {V : Type u_1} [Fintype V] (D : ColumnTreeData V) : ℝ

The compression constant of lem:compression with one projection layer.

Equations

• TrilinearHT.Auto.compressionOneConst D = (512 * (↑1 + 1) ^ 512 * Real.log (2 * D.budget)) ^ (512 * (1 + 1))

theorem TrilinearHT.Auto.ColumnDepthFamily.current_admissible {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : IsAdmissibleOpponent Ψ.D.grid Ψ.D.root (↑↑f) (Ψ.current f) (compressionOneConst Ψ.D)

Blueprint lem:predictors, proof line 1532, and sec:base, line 1482: the current projection z_I = (P_{u(I)} F)_phys is an admissible opponent: every local Bessel row family over cells of the root, applied to the current projections at the row cells, is controlled by the compression constant of lem:compression (eq:compression with m = 1, a polynomial in log(2 D)).

def TrilinearHT.Auto.IsAttemptData (c₂ : ℕ) (B : ℝ) (G : RealDyadicGrid) (J : ℤ × ℤ) (N M : ℕ) (roots : Finset (ℤ × ℤ)) (seg : ℤ × ℤ → ℤ × ℤ) (n : ℤ × ℤ → ℕ) (a : ℤ × ℤ → ℕ → ℝ → ℂ) (cnt : ℤ × ℤ → ℤ × ℤ → ℕ) (atm : ℤ × ℤ → ℤ × ℤ → ℕ → ℝ → ℂ) : Prop

The attempt-level data of an adaptive fit (blueprint sec:reduction, line 429: an inherited column family continues below a cut by retaining its columns): for each attempt root K, counts cnt K c and atoms atm K c on the whole tree below K, extending along paths, given by bounded charts, and agreeing with the segment lists on the segment cells.

Equations

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

Pair norms and the staggered replacement estimate

def TrilinearHT.Auto.slotPair (z : Fin 4 → ℝ → ℂ) (p p' : Fin 4) (X Y : ℝ → ℂ) : Fin 4 → ℝ → ℂ

Inputs X in slot p and Y in slot p', spectators z elsewhere.

Equations

• TrilinearHT.Auto.slotPair z p p' X Y = Function.update (Function.update z p X) p' Y

theorem TrilinearHT.Auto.slotPair_left {z : Fin 4 → ℝ → ℂ} {p p' : Fin 4} (h : p ≠ p') (X Y : ℝ → ℂ) : slotPair z p p' X Y p = X

theorem TrilinearHT.Auto.slotPair_right (z : Fin 4 → ℝ → ℂ) (p p' : Fin 4) (X Y : ℝ → ℂ) : slotPair z p p' X Y p' = Y

theorem TrilinearHT.Auto.slotPair_other {z : Fin 4 → ℝ → ℂ} {p p' l : Fin 4} (hl : l ≠ p) (hl' : l ≠ p') (X Y : ℝ → ℂ) : slotPair z p p' X Y l = z l

theorem TrilinearHT.Auto.slotPair_comm (z : Fin 4 → ℝ → ℂ) {p p' : Fin 4} (h : p ≠ p') (X Y : ℝ → ℂ) : slotPair z p p' X Y = slotPair z p' p Y X

noncomputable def TrilinearHT.Auto.ColumnDepthFamily.delayed {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (K₀ : ℕ) (I : ℤ × ℤ) (y : ℝ) : ℂ

The delayed opponent z_I = (P_{I + K₀} F)_phys (blueprint lem:delay, line 1565).

Equations

• Ψ.delayed f K₀ I y = (↑↑((Ψ.proj (I.1 + ↑K₀)) (TrilinearHT.Auto.physicalColumnInput f)) y).ofLp none

theorem TrilinearHT.Auto.ColumnDepthFamily.memLp_coord_restrict {V : Type u_1} [Fintype V] (z : ↥(ColumnL2 V)) (s : Set ℝ) : MeasureTheory.MemLp (fun (y : ℝ) => (↑↑z y).ofLp none) 2 (MeasureTheory.volume.restrict s)

theorem TrilinearHT.Auto.ColumnDepthFamily.delayed_depthEnergy {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (K₀ : ℕ) : HasDepthEnergy Ψ.D.grid Ψ.D.root (↑↑f) (Ψ.delayed f K₀) 1

Delayed opponents have depth energy with constant one.

The replacement of both high inputs on a common root

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

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