Trilinear Hilbert transform: replaceTuple

theorem TrilinearHT.Auto.replaceTuple (κ : LocalKernelClass) {G : RealDyadicGrid} {J : ℤ × ℤ} {N c₀ c₁ : ℕ} {H : ℝ} (Xi Xk : LowList G J N J c₀ H) {a i k b : Fin 4} (Bp D : ℝ) (pkga : (K K' : ℤ × ℤ) → (li : Xi.Λ) → (lk : Xk.Λ) → PredictorPackage κ (Xi.chart K li) (Xk.chart K' lk) a i k b Bp D c₁) (pkgb : (K K' : ℤ × ℤ) → (li : Xi.Λ) → (lk : Xk.Λ) → PredictorPackage κ (Xi.chart K li) (Xk.chart K' lk) b i k a Bp D c₁) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε ≤ 1) (hai : a ≠ i) (hak : a ≠ k) (hab : a ≠ b) (hik : i ≠ k) (hib : i ≠ b) (hkb : k ≠ b) (hD1 : 1 ≤ D) (K₀ Ma Mb : ℕ) (f : Fin 4 → ℝ → ℂ) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (q : ℝ) (ka kb c₂ : ℕ) (Ba Bb : ℝ) (hSa : (predAccSetup κ Xi Xk a i k b Bp D pkga hε0 hε1 K₀ Ma (f a) w q ka c₂ Ba).Hyp) (hSb : (predAccSetup κ Xi Xk b i k a Bp D pkgb hε0 hε1 K₀ Mb (f b) w q kb c₂ Bb).Hyp) (hw : ∀ (I : ℤ × ℤ), IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) {Ka Kb : ℤ × ℤ} (hKa : Ka ∈ (predAccSetup κ Xi Xk a i k b Bp D pkga hε0 hε1 K₀ Ma (f a) w q ka c₂ Ba).tree.roots) (hKb : Kb ∈ (predAccSetup κ Xi Xk b i k a Bp D pkgb hε0 hε1 K₀ Mb (f b) w q kb c₂ Bb).tree.roots) {R : ℤ × ℤ} (hR : R ∈ dyadicFiniteTree G J N) (ga gb zga zgb : ℤ × ℤ → ℝ → ℂ) {Cga Cgb : ℝ} (hCga : 0 ≤ Cga) (hCgb : 0 ≤ Cgb) (hgam : ∀ (I : ℤ × ℤ), Measurable (ga I)) (hgbm : ∀ (I : ℤ × ℤ), Measurable (gb I)) (hzga : (∀ (I : ℤ × ℤ), Measurable (zga I) ∧ MeasureTheory.MemLp (zga I) 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) ∧ ∀ J' ∈ dyadicFiniteTree G J N, dyadicGridCell G J'.1 J'.2 ⊆ dyadicGridCell G R.1 R.2 → IsAdmissibleOpponent G J' (f a) zga Cga ∧ HasDepthEnergy G J' (f a) zga 1) (hzgb : (∀ (I : ℤ × ℤ), Measurable (zgb I) ∧ MeasureTheory.MemLp (zgb I) 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) ∧ ∀ J' ∈ dyadicFiniteTree G J N, dyadicGridCell G J'.1 J'.2 ⊆ dyadicGridCell G R.1 R.2 → IsAdmissibleOpponent G J' (f b) zgb Cgb ∧ HasDepthEnergy G J' (f b) zgb 1) (T : Finset (ℤ × ℤ)) (hT : ∀ I ∈ T, I ∈ dyadicFiniteTree G J (predAccSetup κ Xi Xk a i k b Bp D pkga hε0 hε1 K₀ Ma (f a) w q ka c₂ Ba).Nc ∧ (predAccSetup κ Xi Xk a i k b Bp D pkga hε0 hε1 K₀ Ma (f a) w q ka c₂ Ba).tree.seg I = Ka ∧ (predAccSetup κ Xi Xk b i k a Bp D pkgb hε0 hε1 K₀ Mb (f b) w q kb c₂ Bb).tree.seg I = Kb ∧ dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R.1 R.2 ∧ (∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → zga I y = ga I y) ∧ ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → zgb I y = gb I y) : have Sa := predAccSetup κ Xi Xk a i k b Bp D pkga hε0 hε1 K₀ Ma (f a) w q ka c₂ Ba; have Sb := predAccSetup κ Xi Xk b i k a Bp D pkgb hε0 hε1 K₀ Mb (f b) w q kb c₂ Bb; have Ea := 2 * Real.exp (-Bp) * (2 * (compressionOneConst ((Sa.system Ka).rooted R) + ↑K₀) + 1) + D ^ 2 * (delayConst κ * (2⁻¹ ^ K₀ + (1 + ↑K₀) * √ε) * (1 + D) ^ 4); have Eb := 2 * Real.exp (-Bp) * (2 * (compressionOneConst ((Sb.system Kb).rooted R) + ↑K₀) + 1) + D ^ 2 * (delayConst κ * (2⁻¹ ^ K₀ + (1 + ↑K₀) * √ε) * (1 + D) ^ 4); ∑ I ∈ T, dyadicGridLength G I.1 * ‖localProgressionForm (dyadicGridLength G I.1) (w I) (slots4 a i k (f a - ga I) (Xi.val I) (Xk.val I) (f b - gb I)) - localProgressionForm (dyadicGridLength G I.1) (w I) (slots4 a i k (Sa.phys I (Sa.tree.st I).1 (Sa.tree.st I).2 - ga I) (Xi.val I) (Xk.val I) (Sb.phys I (Sb.tree.st I).1 (Sb.tree.st I).2 - gb I))‖ ≤ ↑(Fintype.card Xi.Λ) * ↑(Fintype.card Xk.Λ) * (Ea * (2 * (1 + Cgb) + 4)) * √(∫ (y : ℝ) in dyadicGridCell G R.1 R.2, ‖↑↑Sa.input y‖ ^ 2) * √(∫ (y : ℝ) in dyadicGridCell G R.1 R.2, ‖(dyadicGridCell G J.1 J.2).indicator (f b) y‖ ^ 2) + ↑(Fintype.card Xi.Λ) * ↑(Fintype.card Xk.Λ) * (Eb * (2 * (2 * (compressionOneConst ((Sa.system Ka).rooted R) + ↑K₀) + Cga) + 4)) * √(∫ (y : ℝ) in dyadicGridCell G R.1 R.2, ‖↑↑Sb.input y‖ ^ 2) * √(∫ (y : ℝ) in dyadicGridCell G R.1 R.2, ‖(dyadicGridCell G J.1 J.2).indicator (f a) y‖ ^ 2)

Blueprint prop:base, proof lines 1626-1641 (eq:Y): on the cells of a common root R inside the accurate-fit roots K_a, K_b, the tuple (X_i, X_k, f_a - g_a, f_b - g_b) is replaced by (X_i, X_k, P_a - g_a, P_b - g_b) with the delayed physical projections of the accurate fits, first in slot a (opponent f_b - g_b) and then in slot b (delayed opponent P_a - g_a).

theorem TrilinearHT.Auto.min_sum_le {ι : Type u_1} (s : Finset ι) (a : ι → ℝ) (ha : ∀ j ∈ s, 0 ≤ a j) {η : ℝ} (hη : 0 ≤ η) : min η (∑ j ∈ s, a j) ≤ ∑ j ∈ s, min η (a j)

Blueprint eq:min-subadd (line 1659).

theorem TrilinearHT.Auto.cells_sum_eq_integral (G : RealDyadicGrid) (cells : Finset (ℤ × ℤ)) (f : ℤ × ℤ → ℝ) : ∑ I ∈ cells, dyadicGridLength G I.1 * f I = ∫ (y : ℝ), ∑ I ∈ cells, (dyadicGridCell G I.1 I.2).indicator (fun (x : ℝ) => f I) y

The cell sum weighted by length is the integral over the root of the path sums.

theorem TrilinearHT.Auto.cells_sum_le_of_path (G : RealDyadicGrid) (R : ℤ × ℤ) (cells : Finset (ℤ × ℤ)) (hsub : ∀ I ∈ cells, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R.1 R.2) {f : ℤ × ℤ → ℝ} (hf : ∀ (I : ℤ × ℤ), 0 ≤ f I) {M : ℝ} (hM : ∀ (y : ℝ), ∑ I ∈ cells with y ∈ dyadicGridCell G I.1 I.2, f I ≤ M) : ∑ I ∈ cells, dyadicGridLength G I.1 * f I ≤ dyadicGridLength G R.1 * M

Path bounds integrate to a root bound: if every path through the root collects at most M, the length-weighted cell sum is at most M |R|.

structure TrilinearHT.Auto.ActiveSetup (κ : LocalKernelClass) (c₀ : ℕ) : Type 1

The data of the active-cell reduction (blueprint prop:base, lines 1655-1660): on the cells below a root, the four arguments Y_l = B_l + U_l with U_i = U_j = 0, where the basic arguments B_l are combinations of bounded atoms which, along each path, are fixed quadratic chart atoms of bounded complexity, and every cell has |H_I(Y)| ≤ η.

• G : RealDyadicGrid

  Dyadic grid supporting the active setup.

• R : ℤ × ℤ

  Root cell containing all active-setup cells.

• cells : Finset (ℤ × ℤ)

  Finite collection of cells used in the active reduction.

• sub (I : ℤ × ℤ) : I ∈ self.cells → dyadicGridCell self.G I.1 I.2 ⊆ dyadicGridCell self.G self.R.1 self.R.2
• w : ℤ × ℤ → ℝ × ℝ → ℂ

  Admissible local kernel assigned to each active-setup cell.

• adm (I : ℤ × ℤ) : I ∈ self.cells → IsAdmissibleLocalKernel κ (dyadicGridLeft self.G I.1 I.2) (dyadicGridLength self.G I.1) (self.w I)
• L : Type

  Finite label type for the pathwise quadratic-chart atoms.

• fin : Fintype self.L
• φ : ℤ × ℤ → self.L → ℝ → ℂ

  Bounded measurable scalar atom at each cell and label.

• φ_meas (I : ℤ × ℤ) (v : self.L) : Measurable (self.φ I v)
• φ_bound (I : ℤ × ℤ) (v : self.L) (x : ℝ) : ‖self.φ I v x‖ ≤ 1
• H : ℝ

  Uniform complexity budget for the pathwise charts.

• coef : Fin 4 → ℤ × ℤ → self.L → ℂ

  Coefficient of each chart atom in each slot and cell.

• path_chart (y : ℝ) (v : self.L) : ∃ (d : ℕ) (B : QuadraticChartData d), QuadraticChartComplexity c₀ self.H B ∧ IsBoundedQuadraticChart B ∧ ∀ I ∈ self.cells, y ∈ dyadicGridCell self.G I.1 I.2 → (∃ (l : Fin 4), self.coef l I v ≠ 0) → ∀ x ∈ dyadicGridCell self.G I.1 I.2, self.φ I v x = quadraticChartAtom B x
• nested_chart (I : ℤ × ℤ) : I ∈ self.cells → ∀ (v : self.L), (∃ (l : Fin 4), self.coef l I v ≠ 0) → ∃ (d : ℕ) (B : QuadraticChartData d), QuadraticChartComplexity c₀ self.H B ∧ IsBoundedQuadraticChart B ∧ self.φ I v = quadraticChartAtom B
• nested_cons (I : ℤ × ℤ) : I ∈ self.cells → ∀ I' ∈ self.cells, dyadicGridCell self.G I.1 I.2 ⊆ dyadicGridCell self.G I'.1 I'.2 → ∀ (v : self.L), (∃ (l : Fin 4), self.coef l I v ≠ 0) → (∃ (l : Fin 4), self.coef l I' v ≠ 0) → self.φ I v = self.φ I' v
• Dc : ℝ

  Uniform bound for the chart coefficients.

• Dc_nonneg : 0 ≤ self.Dc
• coef_le (l : Fin 4) (I : ℤ × ℤ) (v : self.L) : ‖self.coef l I v‖ ≤ self.Dc
• a : Fin 4

  First slot allowed to carry an additional L² error term.

• b : Fin 4

  Second slot allowed to carry an additional L² error term.

• hab : self.a ≠ self.b
• U : Fin 4 → ℤ × ℤ → ℝ → ℂ

  Additional measurable L² error terms in the two distinguished slots.

• U_meas (l : Fin 4) (I : ℤ × ℤ) : Measurable (self.U l I)
• S : ℝ

  Uniform normalized L² norm bound for the additional error terms.

• U_L2 (l : Fin 4) (I : ℤ × ℤ) : MeasureTheory.MemLp (self.U l I) 2 (normalizedIntervalMeasure (dyadicGridLeft self.G I.1 I.2) (dyadicGridLength self.G I.1))
• U_le (l : Fin 4) (I : ℤ × ℤ) : (MeasureTheory.eLpNorm (self.U l I) 2 (normalizedIntervalMeasure (dyadicGridLeft self.G I.1 I.2) (dyadicGridLength self.G I.1))).toReal ≤ self.S
• η : ℝ

  Upper bound for the norm of the four-linear local form at each cell.

• small (I : ℤ × ℤ) : I ∈ self.cells → ‖localProgressionForm (dyadicGridLength self.G I.1) (self.w I) fun (l : Fin 4) => (fun (x : ℝ) => ∑ v : self.L, self.coef l I v * self.φ I v x) + if l = self.a ∨ l = self.b then self.U l I else 0‖ ≤ self.η

@[reducible, inline]

noncomputable abbrev TrilinearHT.Auto.ActiveSetup.μ {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (I : ℤ × ℤ) : MeasureTheory.Measure ℝ

The normalized measure of a cell.

Equations

• A.μ I = TrilinearHT.Auto.normalizedIntervalMeasure (TrilinearHT.Auto.dyadicGridLeft A.G I.1 I.2) (TrilinearHT.Auto.dyadicGridLength A.G I.1)

@[reducible, inline]

noncomputable abbrev TrilinearHT.Auto.ActiveSetup.Hf {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (I : ℤ × ℤ) (F : Fin 4 → ℝ → ℂ) : ℂ

The local form on a cell.

Equations

• A.Hf I F = TrilinearHT.Auto.localProgressionForm (TrilinearHT.Auto.dyadicGridLength A.G I.1) (A.w I) F

noncomputable def TrilinearHT.Auto.ActiveSetup.B {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (l : Fin 4) (I : ℤ × ℤ) : ℝ → ℂ

The basic arguments.

Equations

• A.B l I x = ∑ v : A.L, A.coef l I v * A.φ I v x

noncomputable def TrilinearHT.Auto.ActiveSetup.z {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (p : Fin 4) (I : ℤ × ℤ) : Fin 4 → ℝ → ℂ

The patterns: 0 all basic, 1 the side U_a, 2 the side U_b, 3 both sides.

Equations

• A.z 0 I = fun (l : Fin 4) => A.B l I
• A.z 1 I = Function.update (fun (l : Fin 4) => A.B l I) A.a (A.U A.a I)
• A.z 2 I = Function.update (fun (l : Fin 4) => A.B l I) A.b (A.U A.b I)
• A.z 3 I = Function.update (Function.update (fun (l : Fin 4) => A.B l I) A.a (A.U A.a I)) A.b (A.U A.b I)

def TrilinearHT.Auto.ActiveSetup.mslot {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (p : Fin 3) : Fin 4

The slot carrying the possibly non-basic argument of the patterns 0, 1, 2.

Equations

• A.mslot p = if p = 2 then A.b else A.a

theorem TrilinearHT.Auto.ActiveSetup.B_meas {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (l : Fin 4) (I : ℤ × ℤ) : Measurable (A.B l I)

theorem TrilinearHT.Auto.ActiveSetup.B_bound {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (l : Fin 4) (I : ℤ × ℤ) (x : ℝ) : ‖A.B l I x‖ ≤ ↑(Fintype.card A.L) * A.Dc

theorem TrilinearHT.Auto.ActiveSetup.B_memLp {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (l : Fin 4) (I : ℤ × ℤ) : MeasureTheory.MemLp (A.B l I) 2 (A.μ I)

theorem TrilinearHT.Auto.ActiveSetup.B_eLpNorm_le {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (l : Fin 4) (I : ℤ × ℤ) : (MeasureTheory.eLpNorm (A.B l I) 2 (A.μ I)).toReal ≤ ↑(Fintype.card A.L) * A.Dc

noncomputable def TrilinearHT.Auto.ActiveSetup.Y {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (I : ℤ × ℤ) : Fin 4 → ℝ → ℂ

The replaced tuple Y_l = B_l + U_l with U_i = U_j = 0.

Equations

• A.Y I l = A.B l I + if l = A.a ∨ l = A.b then A.U l I else 0

noncomputable def TrilinearHT.Auto.ActiveSetup.tnorm {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (I : ℤ × ℤ) (m : Fin 4) (v₀ v₁ v₂ : A.L) : ℝ

The transpose norm of an atom triple in the slots other than m.

Equations

• A.tnorm I m v₀ v₁ v₂ = TrilinearHT.Auto.transposeNorm (TrilinearHT.Auto.dyadicGridLength A.G I.1) (A.w I) m (TrilinearHT.Auto.tripleSlots 0 m ![A.φ I v₀, A.φ I v₁, A.φ I v₂])

theorem TrilinearHT.Auto.ActiveSetup.tnorm_nonneg {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (I : ℤ × ℤ) (m : Fin 4) (v₀ v₁ v₂ : A.L) : 0 ≤ A.tnorm I m v₀ v₁ v₂

theorem TrilinearHT.Auto.ActiveSetup.Y_eq {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (I : ℤ × ℤ) : A.Y I = Function.update (Function.update (fun (l : Fin 4) => A.B l I) A.a (A.B A.a I + A.U A.a I)) A.b (A.B A.b I + A.U A.b I)

theorem TrilinearHT.Auto.ActiveSetup.H_Y_eq {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) {I : ℤ × ℤ} (hI : I ∈ A.cells) : A.Hf I (A.Y I) = ∑ p : Fin 4, A.Hf I (A.z p I)

Multilinearity: H(Y) = Σ_p H(z_p) over the four patterns.

theorem TrilinearHT.Auto.ActiveSetup.S_nonneg {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) : 0 ≤ A.S

theorem TrilinearHT.Auto.ActiveSetup.z_zero {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (I : ℤ × ℤ) : A.z (Fin.castSucc 0) I = fun (l : Fin 4) => A.B l I

theorem TrilinearHT.Auto.ActiveSetup.z_one {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (I : ℤ × ℤ) : A.z (Fin.castSucc 1) I = Function.update (fun (l : Fin 4) => A.B l I) A.a (A.U A.a I)

theorem TrilinearHT.Auto.ActiveSetup.z_two {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (I : ℤ × ℤ) : A.z (Fin.castSucc 2) I = Function.update (fun (l : Fin 4) => A.B l I) A.b (A.U A.b I)

theorem TrilinearHT.Auto.ActiveSetup.pattern_data {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (I : ℤ × ℤ) (p : Fin 3) : (∀ (j : Fin 4), Measurable (A.z p.castSucc I j)) ∧ MeasureTheory.MemLp (A.z p.castSucc I (A.mslot p)) 2 (A.μ I) ∧ (MeasureTheory.eLpNorm (A.z p.castSucc I (A.mslot p)) 2 (A.μ I)).toReal ≤ A.S + ↑(Fintype.card A.L) * A.Dc ∧ ∀ (i : Fin 3), A.z p.castSucc I ((A.mslot p).succAbove i) = A.B ((A.mslot p).succAbove i) I

def TrilinearHT.Auto.ActiveSetup.avail3 {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (I : ℤ × ℤ) (m : Fin 4) (v₀ v₁ v₂ : A.L) : Prop

The atom triple is available at the cell: nonzero coefficients in the three slots other than m.

Equations

• A.avail3 I m v₀ v₁ v₂ = (A.coef (m.succAbove 0) I v₀ ≠ 0 ∧ A.coef (m.succAbove 1) I v₁ ≠ 0 ∧ A.coef (m.succAbove 2) I v₂ ≠ 0)

theorem TrilinearHT.Auto.ActiveSetup.pattern_le {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) {I : ℤ × ℤ} (hI : I ∈ A.cells) (p : Fin 3) : ‖A.Hf I (A.z p.castSucc I)‖ ≤ A.Dc ^ 3 * (A.S + ↑(Fintype.card A.L) * A.Dc) * ∑ v₀ : A.L, ∑ v₁ : A.L, ∑ v₂ : A.L, if A.avail3 I (A.mslot p) v₀ v₁ v₂ then A.tnorm I (A.mslot p) v₀ v₁ v₂ else 0

Blueprint prop:base, line 1657: a pattern with at least three basic arguments is bounded by the coefficient products times the transpose norms of the available triples.

def TrilinearHT.Auto.ActiveSetup.active {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (δ : ℝ) (I : ℤ × ℤ) : Prop

A cell is active at threshold δ when some available atom triple has transpose norm above δ (blueprint prop:base, line 1655).

Equations

• A.active δ I = ∃ (m : Fin 4) (v₀ : A.L) (v₁ : A.L) (v₂ : A.L), A.avail3 I m v₀ v₁ v₂ ∧ δ < A.tnorm I m v₀ v₁ v₂

theorem TrilinearHT.Auto.ActiveSetup.exists_path_charts {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (hc : 1 ≤ c₀) : ∃ (d : ℝ → A.L → ℕ) (Q : (y : ℝ) → (v : A.L) → QuadraticChartData (d y v)), ∀ (y : ℝ) (v : A.L), QuadraticChartComplexity c₀ (chartTranslationBudget A.H) (Q y v) ∧ IsBoundedQuadraticChart (Q y v) ∧ ∀ I ∈ A.cells, y ∈ dyadicGridCell A.G I.1 I.2 → (∃ (l : Fin 4), A.coef l I v ≠ 0) → ∀ x ∈ dyadicGridCell A.G I.1 I.2, A.φ I v x = quadraticChartAtom (Q y v) (x - y)

The translated path charts: near the path through y, the atom of label v is u ↦ Q_{y,v}(u - y) with Q_{y,v} of complexity chartTranslationBudget H.

theorem TrilinearHT.Auto.ActiveSetup.avail3_vec {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) {I : ℤ × ℤ} {m : Fin 4} {v₀ v₁ v₂ : A.L} (h : A.avail3 I m v₀ v₁ v₂) (i : Fin 3) : ∃ (l : Fin 4), A.coef l I (![v₀, v₁, v₂] i) ≠ 0

theorem TrilinearHT.Auto.ActiveSetup.tripleSlots_vec {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (I : ℤ × ℤ) (m : Fin 4) (v₀ v₁ v₂ : A.L) (i : Fin 3) : tripleSlots 0 m ![A.φ I v₀, A.φ I v₁, A.φ I v₂] (m.succAbove i) = A.φ I (![v₀, v₁, v₂] i)

theorem TrilinearHT.Auto.ActiveSetup.inactive_sum (κ : LocalKernelClass) (c₀ : ℕ) (hc : 1 ≤ c₀) : ∃ (C : ℕ) (Cr : ℝ), 0 ≤ Cr ∧ ∀ (A : ActiveSetup κ c₀) (δ : ℝ), 0 < δ → δ ≤ 1 → ∀ (m : Fin 4) (v₀ v₁ v₂ : A.L), (∑ I ∈ A.cells, dyadicGridLength A.G I.1 * if A.avail3 I m v₀ v₁ v₂ ∧ A.tnorm I m v₀ v₁ v₂ ≤ δ then A.tnorm I m v₀ v₁ v₂ else 0) ≤ dyadicGridLength A.G A.R.1 * (δ * Cr * (Real.log (chartTranslationBudget A.H) + Real.log δ⁻¹ + 1) ^ C)

Blueprint prop:base, lines 1656-1657: the inactive contributions of one available atom triple, summed over the cells below the root, are at most δ poly(log H, log δ⁻¹) times the root length (eq:triple-tail and eq:path).

theorem TrilinearHT.Auto.ActiveSetup.active_count (κ : LocalKernelClass) (c₀ : ℕ) (hc : 1 ≤ c₀) : ∃ (C : ℕ), 1 ≤ C ∧ ∀ (A : ActiveSetup κ c₀) (δ : ℝ), 0 < δ → δ ≤ 1 → ∀ (y : ℝ), ↑{I ∈ A.cells | y ∈ dyadicGridCell A.G I.1 I.2 ∧ A.active δ I}.card ≤ 4 * ↑(Fintype.card A.L) ^ 3 * (↑C * (216 * Real.log (chartTranslationBudget A.H) + Real.log (sliceConst κ) + 2 * Real.log δ⁻¹) ^ C)

Blueprint prop:base, line 1655: the active collection has path multiplicity at most 4 |L|³ poly(log H, log δ⁻¹).

theorem TrilinearHT.Auto.ActiveSetup.reduction (κ : LocalKernelClass) (c₀ : ℕ) (hc : 1 ≤ c₀) : ∃ (C : ℕ) (Cr : ℝ), 0 ≤ Cr ∧ ∀ (A : ActiveSetup κ c₀) (δ : ℝ), 0 < δ → δ ≤ 1 → 0 ≤ A.η → ∑ I ∈ A.cells, dyadicGridLength A.G I.1 * ‖A.Hf I (A.Y I)‖ ≤ ∑ p : Fin 3, ∑ I ∈ A.cells with A.active δ I, dyadicGridLength A.G I.1 * min A.η ‖A.Hf I (A.z p.castSucc I)‖ + ∑ I ∈ A.cells, dyadicGridLength A.G I.1 * ‖A.Hf I (A.z 3 I)‖ + 3 * ↑(Fintype.card A.L) ^ 3 * (A.Dc ^ 3 * (A.S + ↑(Fintype.card A.L) * A.Dc)) * (dyadicGridLength A.G A.R.1 * (δ * Cr * (Real.log (chartTranslationBudget A.H) + Real.log δ⁻¹ + 1) ^ C))

Blueprint prop:base, proof lines 1655-1660 (active cells, eq:min-subadd): the length-weighted sum of |H_I(Y)| is at most the active minima of the three patterns with at least three basic arguments, plus the two-U term, plus the inactive error δ poly(log H, log δ⁻¹) |R| times the coefficient and size bounds and the triple count.

Path charts of labelled cell functions

def TrilinearHT.Auto.PathCharts (G : RealDyadicGrid) (cells : Finset (ℤ × ℤ)) {Λ : Type u_1} (φ : ℤ × ℤ → Λ → ℝ → ℂ) (av : ℤ × ℤ → Λ → Prop) (c₀ : ℕ) (H : ℝ) : Prop

Charts of labelled cell functions that are nested along the tree (blueprint prop:base, line 1645, and sec:localization, line 1677: each available label is one fixed bounded quadratic chart atom, and the functions of a label agree on nested cells where it is available). In particular, along every path each available label is one chart atom (PathCharts.path).

Equations

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

theorem TrilinearHT.Auto.PathCharts.of_nested {G : RealDyadicGrid} {cells : Finset (ℤ × ℤ)} {Λ : Type u_1} {φ : ℤ × ℤ → Λ → ℝ → ℂ} {av : ℤ × ℤ → Λ → Prop} {c₀ : ℕ} {H : ℝ} (hchart : ∀ I ∈ cells, ∀ (v : Λ), av I v → ∃ (d : ℕ) (B : QuadraticChartData d), QuadraticChartComplexity c₀ H B ∧ IsBoundedQuadraticChart B ∧ φ I v = quadraticChartAtom B) (hcons : ∀ I ∈ cells, ∀ I' ∈ cells, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G I'.1 I'.2 → ∀ (v : Λ), av I v → av I' v → φ I v = φ I' v) : PathCharts G cells φ av c₀ H

Path charts from charts at the available cells that agree along nested available cells.

theorem TrilinearHT.Auto.PathCharts.path {G : RealDyadicGrid} {cells : Finset (ℤ × ℤ)} {Λ : Type u_1} {φ : ℤ × ℤ → Λ → ℝ → ℂ} {av : ℤ × ℤ → Λ → Prop} {c₀ : ℕ} {H : ℝ} (h : PathCharts G cells φ av c₀ H) (hdef : ∃ (d : ℕ) (B : QuadraticChartData d), QuadraticChartComplexity c₀ H B ∧ IsBoundedQuadraticChart B) (y : ℝ) (v : Λ) : ∃ (d : ℕ) (B : QuadraticChartData d), QuadraticChartComplexity c₀ H B ∧ IsBoundedQuadraticChart B ∧ ∀ I ∈ cells, y ∈ dyadicGridCell G I.1 I.2 → av I v → ∀ x ∈ dyadicGridCell G I.1 I.2, φ I v x = quadraticChartAtom B x

Along every path, each available label is one fixed bounded quadratic chart atom on the cells through the path (blueprint prop:base, line 1645: "after recentering at this fixed y, all unscaled oscillation parameters are fixed along the path").

theorem TrilinearHT.Auto.PathCharts.mono_c {G : RealDyadicGrid} {cells : Finset (ℤ × ℤ)} {Λ : Type u_1} {φ : ℤ × ℤ → Λ → ℝ → ℂ} {av : ℤ × ℤ → Λ → Prop} {c₀ c₁ : ℕ} {H : ℝ} (h : PathCharts G cells φ av c₀ H) (hc : c₀ ≤ c₁) : PathCharts G cells φ av c₁ H

theorem TrilinearHT.Auto.PathCharts.mono {G : RealDyadicGrid} {cells : Finset (ℤ × ℤ)} {Λ : Type u_1} {φ : ℤ × ℤ → Λ → ℝ → ℂ} {av av' : ℤ × ℤ → Λ → Prop} {c₀ : ℕ} {H H' : ℝ} (h : PathCharts G cells φ av c₀ H) (hav : ∀ (I : ℤ × ℤ) (v : Λ), av' I v → av I v) (hH : H ≤ H') : PathCharts G cells φ av' c₀ H'

theorem TrilinearHT.Auto.PathCharts.sum {G : RealDyadicGrid} {cells : Finset (ℤ × ℤ)} {Λ₁ : Type u_1} {Λ₂ : Type u_2} {φ₁ : ℤ × ℤ → Λ₁ → ℝ → ℂ} {φ₂ : ℤ × ℤ → Λ₂ → ℝ → ℂ} {av₁ : ℤ × ℤ → Λ₁ → Prop} {av₂ : ℤ × ℤ → Λ₂ → Prop} {c₀ : ℕ} {H : ℝ} (h₁ : PathCharts G cells φ₁ av₁ c₀ H) (h₂ : PathCharts G cells φ₂ av₂ c₀ H) : PathCharts G cells (fun (I : ℤ × ℤ) => Sum.elim (φ₁ I) (φ₂ I)) (fun (I : ℤ × ℤ) => Sum.elim (av₁ I) (av₂ I)) c₀ H

Path charts of two label families combine.

theorem TrilinearHT.Auto.LowList.pathCharts {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {R : ℤ × ℤ} {c₀ : ℕ} {H : ℝ} (X : LowList G J N R c₀ H) (cells : Finset (ℤ × ℤ)) : PathCharts G cells (fun (I : ℤ × ℤ) (l : X.Λ) => X.atom I l) (fun (I : ℤ × ℤ) (l : X.Λ) => X.coef I l ≠ 0) c₀ H

The low lists have path charts: births are canonical along paths.

theorem TrilinearHT.Auto.AccSetup.Hyp.atoms_good {S : AccSetup} (h : S.Hyp) (d : ℕ) (c : ℤ × ℤ) (i : ℕ) : i < (fitState S.G S.M S.P S.O d c).2 → ∃ (p : (d : ℕ) × QuadraticChartData d), QuadraticChartComplexity S.c₂ S.B p.snd ∧ IsBoundedQuadraticChart p.snd ∧ (fitState S.G S.M S.P S.O d c).1 i = quadraticChartAtom p.snd

The accurate-fit atoms are detection charts.

theorem TrilinearHT.Auto.AccSetup.Hyp.system_pathCharts {S : AccSetup} (h : S.Hyp) (K : ℤ × ℤ) (cells : Finset (ℤ × ℤ)) {c₀ : ℕ} {H : ℝ} (hP₀ : PathCharts S.G cells (fun (c : ℤ × ℤ) (v : S.V₀) => S.P₀.scalarAt c v) (fun (c : ℤ × ℤ) (v : S.V₀) => v ∈ S.P₀.avail c) c₀ H) (hc₀ : S.c₂ ≤ c₀) (hBH : S.B ≤ H) : PathCharts S.G cells (fun (c : ℤ × ℤ) (v : S.W) => (S.system K).scalarAt c v) (fun (c : ℤ × ℤ) (v : S.W) => v ∈ (S.system K).avail c) c₀ H

The scalars of the accurate-fit system have path charts, given path charts of the predictor system.

theorem TrilinearHT.Auto.predSystem_pathCharts (κ : LocalKernelClass) {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {R : ℤ × ℤ} {c₀ c₁ : ℕ} {H : ℝ} (Xi Xk : LowList G J N R c₀ H) (a i k b : Fin 4) (B D : ℝ) (pkg : (K K' : ℤ × ℤ) → (li : Xi.Λ) → (lk : Xk.Λ) → PredictorPackage κ (Xi.chart K li) (Xk.chart K' lk) a i k b B D c₁) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε ≤ 1) (cells : Finset (ℤ × ℤ)) (hcells : ∀ I ∈ cells, I ∈ dyadicFiniteTree G J N) : PathCharts G cells (fun (c : ℤ × ℤ) (v : Xi.Λ × Xk.Λ × Fin ⌊D⌋₊) => (predSystem κ Xi Xk a i k b B D pkg hε0 hε1).scalarAt c v) (fun (c : ℤ × ℤ) (v : Xi.Λ × Xk.Λ × Fin ⌊D⌋₊) => v ∈ (predSystem κ Xi Xk a i k b B D pkg hε0 hε1).avail c) c₁ D

The predictor system has path charts: its scalars are conjugate predictor charts, fixed along paths by the canonical births of the low labels.

Coefficients of the current projections of a path-uniform system

theorem TrilinearHT.Auto.PathColumnSystem.colData {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) (c : ℤ × ℤ) : ColData (P.scalarAt c) P.weight

theorem TrilinearHT.Auto.PathColumnSystem.colOK {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) (c : ℤ × ℤ) (v : V) : ColOK (dyadicGridCell G c.1 c.2) (P.scalarAt c) P.weight v

theorem TrilinearHT.Auto.PathColumnSystem.range_eq_colRange {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) (c : ℤ × ℤ) : P.range c = colRange (dyadicGridCell G c.1 c.2) (P.scalarAt c) P.weight (P.avail c)

The cell projection of the system is the column-range projection of its available labels.

noncomputable def TrilinearHT.Auto.PathColumnSystem.coef {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) (c : ℤ × ℤ) (z : ↥(ColumnL2 V)) (v : V) : ℂ

The coefficients of the current projection at a cell (zero off the available labels).

Equations

• P.coef c z v = if v ∈ P.avail c then TrilinearHT.Auto.colCoeff (TrilinearHT.Auto.dyadicGridCell G c.1 c.2) (P.scalarAt c) P.weight (P.avail c) z v else 0

theorem TrilinearHT.Auto.PathColumnSystem.proj_none_ae {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) (c : ℤ × ℤ) (z : ↥(ColumnL2 V)) : ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G c.1 c.2 → (↑↑((P.proj c) z) y).ofLp none = ∑ v : V, P.coef c z v * P.scalarAt c v y

The physical part of the cell projection is the combination of the scalars with the coefficients.

theorem TrilinearHT.Auto.PathColumnSystem.coef_sq_le {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) (c : ℤ × ℤ) (z : ↥(ColumnL2 V)) (v : V) : ‖P.coef c z v‖ ^ 2 * P.weight v * dyadicGridLength G c.1 ≤ ∫ (y : ℝ) in dyadicGridCell G c.1 c.2, ‖↑↑z y‖ ^ 2

Private-coordinate recovery: the coefficients are bounded by the inverse square root of the private weight times the normalized L² norm of the input on the cell.

Basic projections (blueprint prop:base, lines 1611-1613; line 1859)

noncomputable def TrilinearHT.Auto.ColumnDepthFamily.currentZ {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (Z : ↥(ColumnL2 V)) (I : ℤ × ℤ) (y : ℝ) : ℂ

The physical part (P_{u(I)} Z)_phys of the current projection of an augmented input, with u(I) the tree cell above I (zero outside the tree).

Equations

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

structure TrilinearHT.Auto.BasicProjection (G : RealDyadicGrid) (R : ℤ × ℤ) (CF : ℝ) : Type 1

A basic projection below the root R: an inherited column depth family on the grid of R whose root contains R, and an augmented input Z of energy at most CF |R| on R; its value at a cell I is the physical part of the current projection (P_I Z)_phys (blueprint prop:base, line 1611: "each B_l is a difference of at most two current basic projections").

• V : Type

  Finite label type of the basic column projection system.

• fin : Fintype self.V
• Ψ : ColumnDepthFamily self.V

  Depth-indexed column family defining the basic projections.

• Z : ↥(ColumnL2 self.V)

  Column L² input whose projections generate the basic components.

• grid : self.Ψ.D.grid = G
• root_sub : dyadicGridCell G R.1 R.2 ⊆ dyadicGridCell G self.Ψ.D.root.1 self.Ψ.D.root.2
• energy : ∫ (y : ℝ) in dyadicGridCell G R.1 R.2, ‖↑↑self.Z y‖ ^ 2 ≤ CF * dyadicGridLength G R.1

noncomputable def TrilinearHT.Auto.BasicProjection.val {G : RealDyadicGrid} {R : ℤ × ℤ} {CF : ℝ} (P : BasicProjection G R CF) (I : ℤ × ℤ) (y : ℝ) : ℂ

The value of a basic projection at a cell.

Equations

• P.val I y = P.Ψ.currentZ P.Z I y

noncomputable def TrilinearHT.Auto.BasicProjection.zero {G : RealDyadicGrid} {R : ℤ × ℤ} {CF : ℝ} (P : BasicProjection G R CF) (hCF : 0 ≤ CF) : BasicProjection G R CF

The zero input on the family of another basic projection.

Equations

• P.zero hCF = { V := P.V, fin := P.fin, Ψ := P.Ψ, Z := 0, grid := ⋯, root_sub := ⋯, energy := ⋯ }

theorem TrilinearHT.Auto.BasicProjection.zero_val {G : RealDyadicGrid} {R : ℤ × ℤ} {CF : ℝ} (P : BasicProjection G R CF) (hCF : 0 ≤ CF) (I : ℤ × ℤ) : ∀ᵐ (y : ℝ), (P.zero hCF).val I y = 0

theorem TrilinearHT.Auto.BasicProjection.inv_privateWeight_le {G : RealDyadicGrid} {R : ℤ × ℤ} {CF : ℝ} (P : BasicProjection G R CF) {X : ℝ} (hX : P.Ψ.D.budget ≤ X) (v : P.V) : (P.Ψ.D.privateWeight v)⁻¹ ≤ X ^ 2

A column budget X bounds the inverse private weights of a basic projection by X² (eq:columnbudget, budget⁻¹ ≤ √ε_v).

def TrilinearHT.Auto.BasicProjection.HasChartsOn {G : RealDyadicGrid} {R : ℤ × ℤ} {CF : ℝ} (P : BasicProjection G R CF) (S : Set (ℤ × ℤ)) (c₀ : ℕ) (H : ℝ) : Prop

The cells of S are decision cells of the family of a basic projection, not deeper than its leaf depth, and the columns available there are bounded quadratic chart atoms of order c₀ and complexity at most H on those cells (blueprint prop:base, line 1607: the complexities of the basic data; line 1676: the tags of the original basic columns).

Equations

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

theorem TrilinearHT.Auto.BasicProjection.HasChartsOn.mono {G : RealDyadicGrid} {R : ℤ × ℤ} {CF : ℝ} {P : BasicProjection G R CF} {S S' : Set (ℤ × ℤ)} {c₀ c₀' : ℕ} {H H' : ℝ} (h : P.HasChartsOn S c₀ H) (hS : S' ⊆ S) (hc : c₀ ≤ c₀') (hH : H ≤ H') : P.HasChartsOn S' c₀' H'

def TrilinearHT.Auto.BasicProjection.CellEnergyOn {G : RealDyadicGrid} {R : ℤ × ℤ} {CF : ℝ} (P : BasicProjection G R CF) (S : Set (ℤ × ℤ)) : Prop

The input of a basic projection has energy at most CF |c| on every cell c of S (blueprint prop:base, lines 1607-1608: the basic inputs keep bounded normalized L² sizes on the cells, the original inputs being normalized on every cell of the tree).

Equations

• P.CellEnergyOn S = ∀ c ∈ S, ∫ (y : ℝ) in TrilinearHT.Auto.dyadicGridCell G c.1 c.2, ‖↑↑P.Z y‖ ^ 2 ≤ CF * TrilinearHT.Auto.dyadicGridLength G c.1

theorem TrilinearHT.Auto.BasicProjection.CellEnergyOn.mono {G : RealDyadicGrid} {R : ℤ × ℤ} {CF : ℝ} {P : BasicProjection G R CF} {S S' : Set (ℤ × ℤ)} (h : P.CellEnergyOn S) (hS : S' ⊆ S) : P.CellEnergyOn S'

theorem TrilinearHT.Auto.BasicProjection.zero_cellEnergyOn {G : RealDyadicGrid} {R : ℤ × ℤ} {CF : ℝ} (P : BasicProjection G R CF) (hCF : 0 ≤ CF) (S : Set (ℤ × ℤ)) : (P.zero hCF).CellEnergyOn S

noncomputable def TrilinearHT.Auto.ActiveSetup.colBudget {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) : ℝ

The column budget of an active setup, 2 + |L| (1 + D_c), from its label count and coefficient bound. The basic projections of its column representation have column budgets at most this (blueprint prop:base, line 1607: counts, complexities and inverse private weights are exp(k^{O(1)})); a column budget X bounds the inverse private weights by X² (BasicProjection.inv_privateWeight_le).

Equations

• A.colBudget = 2 + ↑(Fintype.card A.L) * (1 + A.Dc)

def TrilinearHT.Auto.ActiveSetup.HasColumnRep {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (CF : ℝ) : Prop

The column representation of the basic arguments of an active setup (blueprint prop:base, lines 1607 and 1611-1613): on every cell of the setup each basic argument B_l is, almost everywhere on the cell, the difference of two current basic projections below the root, with inputs of energy at most CF |R| on the root and at most CF |I| on every cell I of the setup, column budgets at most A.colBudget, and columns that are charts of order c₀ and complexity at most A.H on the cells of the setup.

Equations

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

def TrilinearHT.Auto.ActiveSetup.ColumnRepBelow {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (R' : ℤ × ℤ) (CF : ℝ) : Prop

The column representation below a sub-root R': on every cell of the setup below R' each basic argument is the difference of two current basic projections below R' with column budgets at most A.colBudget and columns that are charts of order c₀ and complexity at most A.H on those cells (blueprint prop:normalized, lines 2840-2842: restarts keep the basic arguments).

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.hasColumnRep_of_below {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) {CF : ℝ} (h : A.ColumnRepBelow A.R CF) : A.HasColumnRep CF

def TrilinearHT.Auto.ActiveSetup.SubRootProps {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (η₀ E : ℝ) : Prop

The sub-root properties of an active setup (blueprint prop:base, lines 1611-1622, asserted on every normalized restart root): below every dyadic sub-root R' of the root, the basic-side energies are at most E |R'|, the two-U term is at most η₀ E |R'|, and the basic arguments have a column representation below R'.

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.SubRootProps.mono {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {η₀ E E' : ℝ} (h : A.SubRootProps η₀ E) (hη₀ : 0 ≤ η₀) (hE : E ≤ E') : A.SubRootProps η₀ E'

theorem TrilinearHT.Auto.PathColumnSystem.family_currentZ_ae {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) {R I : ℤ × ℤ} (hR : R ∈ dyadicFiniteTree G J N) (hI : I ∈ dyadicFiniteTree G J N) (hIR : dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R.1 R.2) (z : ↥(ColumnL2 V)) : ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → (P.family R hR).currentZ z I y = ∑ v : V, P.coef I z v * P.scalarAt I v y

On a tree cell below R the current projection of the system rooted at R is the cell projection of the system.

noncomputable def TrilinearHT.Auto.PathColumnSystem.basicProjection {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) {R : ℤ × ℤ} (hR : R ∈ dyadicFiniteTree G J N) (z : ↥(ColumnL2 V)) {CF : ℝ} (hz : ∫ (y : ℝ) in dyadicGridCell G R.1 R.2, ‖↑↑z y‖ ^ 2 ≤ CF * dyadicGridLength G R.1) : BasicProjection G R CF

The current projections of the system rooted at R applied to an input of energy at most CF |R| on R, as a basic projection.

Equations

• P.basicProjection hR z hz = { V := V, fin := inst✝, Ψ := P.family R hR, Z := z, grid := ⋯, root_sub := ⋯, energy := hz }

theorem TrilinearHT.Auto.PathColumnSystem.basicProjection_val_ae {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) {R I : ℤ × ℤ} (hR : R ∈ dyadicFiniteTree G J N) (hI : I ∈ dyadicFiniteTree G J N) (hIR : dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R.1 R.2) (z : ↥(ColumnL2 V)) {CF : ℝ} (hz : ∫ (y : ℝ) in dyadicGridCell G R.1 R.2, ‖↑↑z y‖ ^ 2 ≤ CF * dyadicGridLength G R.1) : ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → (P.basicProjection hR z hz).val I y = ∑ v : V, P.coef I z v * P.scalarAt I v y

theorem TrilinearHT.Auto.PathColumnSystem.budget_le {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) {ε : ℝ} (hε : 0 < ε) (hw : ∀ (v : V), ε ≤ P.weight v) : P.budget ≤ 2 + ↑(Fintype.card V) + ↑(Fintype.card V) * (√ε)⁻¹

The budget of a path-uniform system with private weights at least ε.

The active setup of the base data

@[reducible, inline]

abbrev TrilinearHT.Auto.BaseLabel {G : RealDyadicGrid} {J : ℤ × ℤ} {N c₀ : ℕ} {H : ℝ} (Xi Xk : LowList G J N J c₀ H) {Wa Wb Ga Gb : Type} : Type

The labels of the base data: the two low lists, and for each high slot the labels of its system and of its previous fit.

Equations

• TrilinearHT.Auto.BaseLabel Xi Xk = (Xi.Λ ⊕ Xk.Λ ⊕ (Wa ⊕ Ga) ⊕ Wb ⊕ Gb)

noncomputable def TrilinearHT.Auto.baseCoef {G : RealDyadicGrid} {J : ℤ × ℤ} {N c₀ : ℕ} {H : ℝ} (Xi Xk : LowList G J N J c₀ H) {Wa Wb : Type} [Fintype Wa] [Fintype Wb] (Pa : PathColumnSystem G J N Wa) (Pb : PathColumnSystem G J N Wb) (Za : ↥(ColumnL2 Wa)) (Zb : ↥(ColumnL2 Wb)) {Ga Gb : Type} (cga : ℤ × ℤ → Ga → ℂ) (cgb : ℤ × ℤ → Gb → ℂ) (i k a b l : Fin 4) (I : ℤ × ℤ) : BaseLabel Xi Xk → ℂ

The coefficients of the basic arguments.

Equations

• TrilinearHT.Auto.baseCoef Xi Xk Pa Pb Za Zb cga cgb i k a b l I (Sum.inl li) = if l = i then Xi.coef I li else 0
• TrilinearHT.Auto.baseCoef Xi Xk Pa Pb Za Zb cga cgb i k a b l I (Sum.inr (Sum.inl lk)) = if l = k then Xk.coef I lk else 0
• TrilinearHT.Auto.baseCoef Xi Xk Pa Pb Za Zb cga cgb i k a b l I (Sum.inr (Sum.inr (Sum.inl (Sum.inl v)))) = if l = a then Pa.coef I Za v else 0
• TrilinearHT.Auto.baseCoef Xi Xk Pa Pb Za Zb cga cgb i k a b l I (Sum.inr (Sum.inr (Sum.inl (Sum.inr m)))) = if l = a then -cga I m else 0
• TrilinearHT.Auto.baseCoef Xi Xk Pa Pb Za Zb cga cgb i k a b l I (Sum.inr (Sum.inr (Sum.inr (Sum.inl v)))) = if l = b then Pb.coef I Zb v else 0
• TrilinearHT.Auto.baseCoef Xi Xk Pa Pb Za Zb cga cgb i k a b l I (Sum.inr (Sum.inr (Sum.inr (Sum.inr m)))) = if l = b then -cgb I m else 0

noncomputable def TrilinearHT.Auto.baseAtom {G : RealDyadicGrid} {J : ℤ × ℤ} {N c₀ : ℕ} {H : ℝ} (Xi Xk : LowList G J N J c₀ H) {Wa Wb : Type} [Fintype Wa] [Fintype Wb] (Pa : PathColumnSystem G J N Wa) (Pb : PathColumnSystem G J N Wb) {Ga Gb : Type} (aga : ℤ × ℤ → Ga → ℝ → ℂ) (agb : ℤ × ℤ → Gb → ℝ → ℂ) (I : ℤ × ℤ) : BaseLabel Xi Xk → ℝ → ℂ

The atoms of the basic arguments.

Equations

• TrilinearHT.Auto.baseAtom Xi Xk Pa Pb aga agb I (Sum.inl li) = Xi.atom I li
• TrilinearHT.Auto.baseAtom Xi Xk Pa Pb aga agb I (Sum.inr (Sum.inl lk)) = Xk.atom I lk
• TrilinearHT.Auto.baseAtom Xi Xk Pa Pb aga agb I (Sum.inr (Sum.inr (Sum.inl (Sum.inl v)))) = Pa.scalarAt I v
• TrilinearHT.Auto.baseAtom Xi Xk Pa Pb aga agb I (Sum.inr (Sum.inr (Sum.inl (Sum.inr m)))) = aga I m
• TrilinearHT.Auto.baseAtom Xi Xk Pa Pb aga agb I (Sum.inr (Sum.inr (Sum.inr (Sum.inl v)))) = Pb.scalarAt I v
• TrilinearHT.Auto.baseAtom Xi Xk Pa Pb aga agb I (Sum.inr (Sum.inr (Sum.inr (Sum.inr m)))) = agb I m

theorem TrilinearHT.Auto.baseB_i {G : RealDyadicGrid} {J : ℤ × ℤ} {N c₀ : ℕ} {H : ℝ} (Xi Xk : LowList G J N J c₀ H) {Wa Wb : Type} [Fintype Wa] [Fintype Wb] (Pa : PathColumnSystem G J N Wa) (Pb : PathColumnSystem G J N Wb) (Za : ↥(ColumnL2 Wa)) (Zb : ↥(ColumnL2 Wb)) {Ga Gb : Type} [Fintype Ga] [Fintype Gb] (cga : ℤ × ℤ → Ga → ℂ) (aga : ℤ × ℤ → Ga → ℝ → ℂ) (cgb : ℤ × ℤ → Gb → ℂ) (agb : ℤ × ℤ → Gb → ℝ → ℂ) (i k a b : Fin 4) (hik : i ≠ k) (hia : i ≠ a) (hib : i ≠ b) (I : ℤ × ℤ) (y : ℝ) : ∑ v : BaseLabel Xi Xk, baseCoef Xi Xk Pa Pb Za Zb cga cgb i k a b i I v * baseAtom Xi Xk Pa Pb aga agb I v y = Xi.val I y

theorem TrilinearHT.Auto.baseB_k {G : RealDyadicGrid} {J : ℤ × ℤ} {N c₀ : ℕ} {H : ℝ} (Xi Xk : LowList G J N J c₀ H) {Wa Wb : Type} [Fintype Wa] [Fintype Wb] (Pa : PathColumnSystem G J N Wa) (Pb : PathColumnSystem G J N Wb) (Za : ↥(ColumnL2 Wa)) (Zb : ↥(ColumnL2 Wb)) {Ga Gb : Type} [Fintype Ga] [Fintype Gb] (cga : ℤ × ℤ → Ga → ℂ) (aga : ℤ × ℤ → Ga → ℝ → ℂ) (cgb : ℤ × ℤ → Gb → ℂ) (agb : ℤ × ℤ → Gb → ℝ → ℂ) (i k a b : Fin 4) (hik : i ≠ k) (hka : k ≠ a) (hkb : k ≠ b) (I : ℤ × ℤ) (y : ℝ) : ∑ v : BaseLabel Xi Xk, baseCoef Xi Xk Pa Pb Za Zb cga cgb i k a b k I v * baseAtom Xi Xk Pa Pb aga agb I v y = Xk.val I y

theorem TrilinearHT.Auto.baseB_a {G : RealDyadicGrid} {J : ℤ × ℤ} {N c₀ : ℕ} {H : ℝ} (Xi Xk : LowList G J N J c₀ H) {Wa Wb : Type} [Fintype Wa] [Fintype Wb] (Pa : PathColumnSystem G J N Wa) (Pb : PathColumnSystem G J N Wb) (Za : ↥(ColumnL2 Wa)) (Zb : ↥(ColumnL2 Wb)) {Ga Gb : Type} [Fintype Ga] [Fintype Gb] (cga : ℤ × ℤ → Ga → ℂ) (aga : ℤ × ℤ → Ga → ℝ → ℂ) (cgb : ℤ × ℤ → Gb → ℂ) (agb : ℤ × ℤ → Gb → ℝ → ℂ) (i k a b : Fin 4) (hia : i ≠ a) (hka : k ≠ a) (hab : a ≠ b) (I : ℤ × ℤ) (y : ℝ) : ∑ v : BaseLabel Xi Xk, baseCoef Xi Xk Pa Pb Za Zb cga cgb i k a b a I v * baseAtom Xi Xk Pa Pb aga agb I v y = ∑ v : Wa, Pa.coef I Za v * Pa.scalarAt I v y - ∑ m : Ga, cga I m * aga I m y

theorem TrilinearHT.Auto.baseB_b {G : RealDyadicGrid} {J : ℤ × ℤ} {N c₀ : ℕ} {H : ℝ} (Xi Xk : LowList G J N J c₀ H) {Wa Wb : Type} [Fintype Wa] [Fintype Wb] (Pa : PathColumnSystem G J N Wa) (Pb : PathColumnSystem G J N Wb) (Za : ↥(ColumnL2 Wa)) (Zb : ↥(ColumnL2 Wb)) {Ga Gb : Type} [Fintype Ga] [Fintype Gb] (cga : ℤ × ℤ → Ga → ℂ) (aga : ℤ × ℤ → Ga → ℝ → ℂ) (cgb : ℤ × ℤ → Gb → ℂ) (agb : ℤ × ℤ → Gb → ℝ → ℂ) (i k a b : Fin 4) (hib : i ≠ b) (hkb : k ≠ b) (hab : a ≠ b) (I : ℤ × ℤ) (y : ℝ) : ∑ v : BaseLabel Xi Xk, baseCoef Xi Xk Pa Pb Za Zb cga cgb i k a b b I v * baseAtom Xi Xk Pa Pb aga agb I v y = ∑ v : Wb, Pb.coef I Zb v * Pb.scalarAt I v y - ∑ m : Gb, cgb I m * agb I m y

theorem TrilinearHT.Auto.base_av {G : RealDyadicGrid} {J : ℤ × ℤ} {N c₀ : ℕ} {H : ℝ} (Xi Xk : LowList G J N J c₀ H) {Wa Wb : Type} [Fintype Wa] [Fintype Wb] (Pa : PathColumnSystem G J N Wa) (Pb : PathColumnSystem G J N Wb) (Za : ↥(ColumnL2 Wa)) (Zb : ↥(ColumnL2 Wb)) {Ga Gb : Type} (cga : ℤ × ℤ → Ga → ℂ) (cgb : ℤ × ℤ → Gb → ℂ) (i k a b : Fin 4) {I : ℤ × ℤ} {v : BaseLabel Xi Xk} (h : ∃ (l : Fin 4), baseCoef Xi Xk Pa Pb Za Zb cga cgb i k a b l I v ≠ 0) : match v, h with | Sum.inl li, h => Xi.coef I li ≠ 0 | Sum.inr (Sum.inl lk), h => Xk.coef I lk ≠ 0 | Sum.inr (Sum.inr (Sum.inl (Sum.inl w))), h => w ∈ Pa.avail I | Sum.inr (Sum.inr (Sum.inl (Sum.inr m))), h => cga I m ≠ 0 | Sum.inr (Sum.inr (Sum.inr (Sum.inl w))), h => w ∈ Pb.avail I | Sum.inr (Sum.inr (Sum.inr (Sum.inr m))), h => cgb I m ≠ 0

A nonzero base coefficient of a label means availability in its family.

theorem TrilinearHT.Auto.base_pathCharts {G : RealDyadicGrid} {J : ℤ × ℤ} {N c₀ : ℕ} {H : ℝ} (Xi Xk : LowList G J N J c₀ H) {Wa Wb : Type} [Fintype Wa] [Fintype Wb] (Pa : PathColumnSystem G J N Wa) (Pb : PathColumnSystem G J N Wb) (Za : ↥(ColumnL2 Wa)) (Zb : ↥(ColumnL2 Wb)) {Ga Gb : Type} (cga : ℤ × ℤ → Ga → ℂ) (aga : ℤ × ℤ → Ga → ℝ → ℂ) (cgb : ℤ × ℤ → Gb → ℂ) (agb : ℤ × ℤ → Gb → ℝ → ℂ) (i k a b : Fin 4) (cells : Finset (ℤ × ℤ)) {c₀' : ℕ} {H' : ℝ} (hXi : PathCharts G cells (fun (I : ℤ × ℤ) (l : Xi.Λ) => Xi.atom I l) (fun (I : ℤ × ℤ) (l : Xi.Λ) => Xi.coef I l ≠ 0) c₀' H') (hXk : PathCharts G cells (fun (I : ℤ × ℤ) (l : Xk.Λ) => Xk.atom I l) (fun (I : ℤ × ℤ) (l : Xk.Λ) => Xk.coef I l ≠ 0) c₀' H') (hPa : PathCharts G cells (fun (I : ℤ × ℤ) (v : Wa) => Pa.scalarAt I v) (fun (I : ℤ × ℤ) (v : Wa) => v ∈ Pa.avail I) c₀' H') (hPb : PathCharts G cells (fun (I : ℤ × ℤ) (v : Wb) => Pb.scalarAt I v) (fun (I : ℤ × ℤ) (v : Wb) => v ∈ Pb.avail I) c₀' H') (hga : PathCharts G cells aga (fun (I : ℤ × ℤ) (m : Ga) => cga I m ≠ 0) c₀' H') (hgb : PathCharts G cells agb (fun (I : ℤ × ℤ) (m : Gb) => cgb I m ≠ 0) c₀' H') : PathCharts G cells (baseAtom Xi Xk Pa Pb aga agb) (fun (I : ℤ × ℤ) (v : BaseLabel Xi Xk) => ∃ (l : Fin 4), baseCoef Xi Xk Pa Pb Za Zb cga cgb i k a b l I v ≠ 0) c₀' H'

Nested charts of the base labels from those of the four families.

noncomputable def TrilinearHT.Auto.baseHighB {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {Wa : Type} [Fintype Wa] (Pa : PathColumnSystem G J N Wa) (Za : ↥(ColumnL2 Wa)) {Ga : Type} [Fintype Ga] (cga : ℤ × ℤ → Ga → ℂ) (aga : ℤ × ℤ → Ga → ℝ → ℂ) (I : ℤ × ℤ) (y : ℝ) : ℂ

The basic argument in a high slot: the current projection of the high system minus the previous fit.

Equations

• TrilinearHT.Auto.baseHighB Pa Za cga aga I y = ∑ v : Wa, Pa.coef I Za v * Pa.scalarAt I v y - ∑ m : Ga, cga I m * aga I m y

noncomputable def TrilinearHT.Auto.baseActiveSetup (κ : LocalKernelClass) {G : RealDyadicGrid} {J : ℤ × ℤ} {N c₀ : ℕ} {H : ℝ} (Xi Xk : LowList G J N J c₀ H) {Wa Wb : Type} [Fintype Wa] [Fintype Wb] (Pa : PathColumnSystem G J N Wa) (Pb : PathColumnSystem G J N Wb) (Za : ↥(ColumnL2 Wa)) (Zb : ↥(ColumnL2 Wb)) {Ga Gb : Type} [Fintype Ga] [Fintype Gb] (cga : ℤ × ℤ → Ga → ℂ) (aga : ℤ × ℤ → Ga → ℝ → ℂ) (cgb : ℤ × ℤ → Gb → ℂ) (agb : ℤ × ℤ → Gb → ℝ → ℂ) {i k a b : Fin 4} {c₀' : ℕ} (R : ℤ × ℤ) (cells : Finset (ℤ × ℤ)) (hsub : ∀ I ∈ cells, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R.1 R.2) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (hw : ∀ I ∈ cells, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) (hik : i ≠ k) (hia : i ≠ a) (hib : i ≠ b) (hka : k ≠ a) (hkb : k ≠ b) (hab : a ≠ b) (hagm : ∀ (I : ℤ × ℤ) (m : Ga), Measurable (aga I m)) (hagb : ∀ (I : ℤ × ℤ) (m : Ga) (y : ℝ), ‖aga I m y‖ ≤ 1) (hbgm : ∀ (I : ℤ × ℤ) (m : Gb), Measurable (agb I m)) (hbgb : ∀ (I : ℤ × ℤ) (m : Gb) (y : ℝ), ‖agb I m y‖ ≤ 1) (H' : ℝ) (hXi : PathCharts G cells (fun (I : ℤ × ℤ) (l : Xi.Λ) => Xi.atom I l) (fun (I : ℤ × ℤ) (l : Xi.Λ) => Xi.coef I l ≠ 0) c₀' H') (hXk : PathCharts G cells (fun (I : ℤ × ℤ) (l : Xk.Λ) => Xk.atom I l) (fun (I : ℤ × ℤ) (l : Xk.Λ) => Xk.coef I l ≠ 0) c₀' H') (hPa : PathCharts G cells (fun (I : ℤ × ℤ) (v : Wa) => Pa.scalarAt I v) (fun (I : ℤ × ℤ) (v : Wa) => v ∈ Pa.avail I) c₀' H') (hPb : PathCharts G cells (fun (I : ℤ × ℤ) (v : Wb) => Pb.scalarAt I v) (fun (I : ℤ × ℤ) (v : Wb) => v ∈ Pb.avail I) c₀' H') (hga : PathCharts G cells aga (fun (I : ℤ × ℤ) (m : Ga) => cga I m ≠ 0) c₀' H') (hgb : PathCharts G cells agb (fun (I : ℤ × ℤ) (m : Gb) => cgb I m ≠ 0) c₀' H') (hdef : ∃ (d : ℕ) (B : QuadraticChartData d), QuadraticChartComplexity c₀' H' B ∧ IsBoundedQuadraticChart B) (Dc : ℝ) (hDc : 1 ≤ Dc) (hPac : ∀ I ∈ cells, ∀ (v : Wa), ‖Pa.coef I Za v‖ ≤ Dc) (hPbc : ∀ I ∈ cells, ∀ (v : Wb), ‖Pb.coef I Zb v‖ ≤ Dc) (hcga : ∀ (I : ℤ × ℤ) (m : Ga), ‖cga I m‖ ≤ 1) (hcgb : ∀ (I : ℤ × ℤ) (m : Gb), ‖cgb I m‖ ≤ 1) (Ya Yb : ℤ × ℤ → ℝ → ℂ) (hYam : ∀ (I : ℤ × ℤ), Measurable (Ya I)) (hYbm : ∀ (I : ℤ × ℤ), Measurable (Yb I)) (S : ℝ) (hS : 0 ≤ S) (hUa : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (Ya I - baseHighB Pa Za cga aga I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))) (hUb : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (Yb I - baseHighB Pb Zb cgb agb I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))) (hUa' : ∀ (I : ℤ × ℤ), (MeasureTheory.eLpNorm (Ya I - baseHighB Pa Za cga aga I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))).toReal ≤ S) (hUb' : ∀ (I : ℤ × ℤ), (MeasureTheory.eLpNorm (Yb I - baseHighB Pb Zb cgb agb I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))).toReal ≤ S) (η : ℝ) (hsmall : ∀ I ∈ cells, ‖localProgressionForm (dyadicGridLength G I.1) (w I) (slots4 a i k (Ya I) (Xi.val I) (Xk.val I) (Yb I))‖ ≤ η) : ActiveSetup κ c₀'

The active setup of the base data on the cells of a root (blueprint prop:base, eq:Y and lines 1641-1660): basic arguments from the low lists and the current high projections minus the previous fits, basic sides U_e = Y_e - B_e.

Equations

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

Current projections and basic sides of a path-uniform system

theorem TrilinearHT.Auto.PathColumnSystem.mem_partition_self {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) {R I : ℤ × ℤ} (hR : R ∈ dyadicFiniteTree G J N) (hIR : I ∈ pathBelow G J N R) : I ∈ ((P.family R hR).partition I.1).cells

theorem TrilinearHT.Auto.PathColumnSystem.cur_ae {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) {R I : ℤ × ℤ} (hR : R ∈ dyadicFiniteTree G J N) (hIR : I ∈ pathBelow G J N R) (z : ↥(ColumnL2 V)) : ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → (↑↑(((P.family R hR).proj I.1) z) y).ofLp none = ∑ v : V, P.coef I z v * P.scalarAt I v y

The physical part of the current projection of a rooted family on a cell is the combination of the cell scalars with the cell coefficients.

theorem TrilinearHT.Auto.PathColumnSystem.cur_measurable {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) (I : ℤ × ℤ) (z : ↥(ColumnL2 V)) : Measurable fun (y : ℝ) => ∑ v : V, P.coef I z v * P.scalarAt I v y

theorem TrilinearHT.Auto.PathColumnSystem.cur_sq_le {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) {R I : ℤ × ℤ} (hR : R ∈ dyadicFiniteTree G J N) (hIR : I ∈ pathBelow G J N R) (z : ↥(ColumnL2 V)) : ∫ (y : ℝ) in dyadicGridCell G I.1 I.2, ‖∑ v : V, P.coef I z v * P.scalarAt I v y‖ ^ 2 ≤ ∫ (y : ℝ) in dyadicGridCell G I.1 I.2, ‖↑↑z y‖ ^ 2

Local contraction of the current projection.

theorem TrilinearHT.Auto.PathColumnSystem.rolling_cells {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) {R : ℤ × ℤ} (hR : R ∈ dyadicFiniteTree G J N) (z : ↥(ColumnL2 V)) (K₀ : ℕ) (T : Finset (ℤ × ℤ)) (hT : ∀ I ∈ T, I ∈ pathBelow G J N R) : ∑ I ∈ T, ∫ (y : ℝ) in dyadicGridCell G I.1 I.2, ‖(↑↑(((P.family R hR).proj (I.1 + ↑K₀)) z) y).ofLp none - ∑ v : V, P.coef I z v * P.scalarAt I v y‖ ^ 2 ≤ ↑K₀ ^ 2 * ∫ (y : ℝ) in dyadicGridCell G R.1 R.2, ‖↑↑z y‖ ^ 2

The rolling increments (P_{s+K₀} - P_s) F on cells below a root have square energy at most K₀² times the input energy on the root (blueprint prop:base, eq:basic-side).

theorem TrilinearHT.Auto.eLpNorm_normalized_toReal_sq {a r : ℝ} (hr : 0 < r) {g : ℝ → ℂ} (hm : MeasureTheory.MemLp g 2 (normalizedIntervalMeasure a r)) : (MeasureTheory.eLpNorm g 2 (normalizedIntervalMeasure a r)).toReal ^ 2 = r⁻¹ * ∫ (y : ℝ) in Set.Ico a (a + r), ‖g y‖ ^ 2

noncomputable def TrilinearHT.Auto.AccSetup.cur (S : AccSetup) (K I : ℤ × ℤ) (y : ℝ) : ℂ

The current physical projection of the attempt system rooted at K on a cell.

Equations

• S.cur K I y = ∑ v : S.W, (S.system K).coef I S.Z v * (S.system K).scalarAt I v y

theorem TrilinearHT.Auto.AccSetup.Hyp.phys_st_ae {S : AccSetup} (h : S.Hyp) {K R I : ℤ × ℤ} (hR : R ∈ dyadicFiniteTree S.G S.J S.N) (hIc : I ∈ dyadicFiniteTree S.G S.J S.Nc) (hseg : S.tree.seg I = K) (hIR : S.cell I ⊆ S.cell R) : ∀ᵐ (y : ℝ), y ∈ S.cell I → S.phys I (S.tree.st I).1 (S.tree.st I).2 y = (↑↑((((S.system K).family R hR).proj (I.1 + ↑S.K₀)) S.Z) y).ofLp none

The final fine projections of a coarse cell are the delayed projections of the attempt system rooted at its segment.

theorem TrilinearHT.Auto.AccSetup.cur_measurable (S : AccSetup) (K I : ℤ × ℤ) : Measurable (S.cur K I)

theorem TrilinearHT.Auto.AccSetup.cur_bound (S : AccSetup) (K I : ℤ × ℤ) : ∃ (C : ℝ), ∀ (y : ℝ), ‖S.cur K I y‖ ≤ C

theorem TrilinearHT.Auto.AccSetup.integrableOn_sq_of_bound {s : Set ℝ} (hs : MeasureTheory.volume s < ⊤) {g : ℝ → ℂ} (hg : Measurable g) {C : ℝ} (hC : ∀ (y : ℝ), ‖g y‖ ≤ C) : MeasureTheory.IntegrableOn (fun (y : ℝ) => ‖g y‖ ^ 2) s MeasureTheory.volume

theorem TrilinearHT.Auto.AccSetup.Hyp.basicSide {S : AccSetup} (h : S.Hyp) {K R : ℤ × ℤ} (hR : R ∈ dyadicFiniteTree S.G S.J S.N) (hRT : kernelHull S.G S.J S.N S.w R) (T : Finset (ℤ × ℤ)) (hT : ∀ I ∈ T, I ∈ dyadicFiniteTree S.G S.J S.Nc ∧ S.tree.seg I = K ∧ S.cell I ⊆ S.cell R) : ∑ I ∈ T, ∫ (y : ℝ) in S.cell I, ‖S.phys I (S.tree.st I).1 (S.tree.st I).2 y - S.cur K I y‖ ^ 2 ≤ ↑S.K₀ ^ 2 * dyadicGridLength S.G R.1

Blueprint prop:base, eq:basic-side: the basic sides U_{e,I} = (P_{s+K₀} - P_s) F_e on the coarse cells of one segment below a common root R have square energy at most K₀² |R|.

theorem TrilinearHT.Auto.AccSetup.Hyp.U_sq_le {S : AccSetup} (h : S.Hyp) {K I : ℤ × ℤ} (hIc : I ∈ dyadicFiniteTree S.G S.J S.Nc) (hIH : kernelHull S.G S.J S.N S.w I) : ∫ (y : ℝ) in S.cell I, ‖S.phys I (S.tree.st I).1 (S.tree.st I).2 y - S.cur K I y‖ ^ 2 ≤ 4 * dyadicGridLength S.G I.1

The basic side on one coarse cell has L²(I) energy at most 4 |I|.

theorem TrilinearHT.Auto.AccSetup.Hyp.coef_le {S : AccSetup} (h : S.Hyp) {K I : ℤ × ℤ} (hIT : I ∈ dyadicFiniteTree S.G S.J S.N) (hIH : kernelHull S.G S.J S.N S.w I) {ε : ℝ} (hε : 0 < ε) (hw : ∀ (v : S.W), ε ≤ S.wt v) (v : S.W) : ‖(S.system K).coef I S.Z v‖ ≤ √ε⁻¹

Coefficient bound from private-coordinate recovery: |c_v| ≤ ε^{-1/2}.

Pair smallness of the replaced tuple on one cell

theorem TrilinearHT.Auto.slots4_pairSmall {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {q : ℝ} (hq : 2 ≤ q) {a i k b : Fin 4} (hai : a ≠ i) (hak : a ≠ k) (hab : a ≠ b) (hik : i ≠ k) (hib : i ≠ b) (hkb : k ≠ b) {f : Fin 4 → ℝ → ℂ} (hfm : ∀ (l : Fin 4), Measurable (f l)) (hfq : ∀ (l : Fin 4), MeasureTheory.eLpNorm (f l) (ENNReal.ofReal q) (normalizedIntervalMeasure a₀ r) ≤ 1) {φ φ' ga gb Pa Pb : ℝ → ℂ} (hφ : Measurable φ) (hφ' : Measurable φ') (hga : Measurable ga) (hgb : Measurable gb) (hPa : Measurable Pa) (hPb : Measurable Pb) {S Sa Sb η₀ δa δb : ℝ} (hS : 0 < S) (hSa : 0 < Sa) (hφS : ∀ (y : ℝ), ‖φ y‖ ≤ S) (hφ'S : ∀ (y : ℝ), ‖φ' y‖ ≤ S) (hgaS : ∀ (y : ℝ), ‖ga y‖ ≤ S) (hgbS : ∀ (y : ℝ), ‖gb y‖ ≤ S) (hPaS : ∀ (y : ℝ), ‖Pa y‖ ≤ Sa) (hPbS : ∀ (y : ℝ), ‖Pb y‖ ≤ Sb) (hδa : 0 ≤ δa) (hδb : 0 ≤ δb) (hsa : FormSmall a₀ r w a q (f a - Pa) δa) (hsb : FormSmall a₀ r w b q (f b - Pb) δb) (hpairs : ∀ (s s' : Fin 4), s ≠ s' → PairSmall a₀ r w s s' (slots4 a i k (f a - ga) φ φ' (f b - gb) s) (slots4 a i k (f a - ga) φ φ' (f b - gb) s') η₀) (s s' : Fin 4) : s ≠ s' → PairSmall a₀ r w s s' (slots4 a i k (Pa - ga) φ φ' (Pb - gb) s) (slots4 a i k (Pa - ga) φ φ' (Pb - gb) s') (η₀ + (2 + 2 * S) * (δa + δb) + (1 + Sa) * δb)

Blueprint prop:base, proof lines 1641-1642 (one cell): if every pair of the tuple (f_a - g_a, φ, φ', f_b - g_b) in the slots a, i, k, b is η₀-small and the residuals f_e - P_e are δ_e-small, then every pair of the replaced tuple (P_a - g_a, φ, φ', P_b - g_b) is η₀ + (2 + 2S)(δ_a + δ_b) + (1 + S_a) δ_b-small.

theorem TrilinearHT.Auto.baseActiveSetup_U_a (κ : LocalKernelClass) {G : RealDyadicGrid} {J : ℤ × ℤ} {N c₀ : ℕ} {H : ℝ} (Xi Xk : LowList G J N J c₀ H) {Wa Wb : Type} [Fintype Wa] [Fintype Wb] (Pa : PathColumnSystem G J N Wa) (Pb : PathColumnSystem G J N Wb) (Za : ↥(ColumnL2 Wa)) (Zb : ↥(ColumnL2 Wb)) {Ga Gb : Type} [Fintype Ga] [Fintype Gb] (cga : ℤ × ℤ → Ga → ℂ) (aga : ℤ × ℤ → Ga → ℝ → ℂ) (cgb : ℤ × ℤ → Gb → ℂ) (agb : ℤ × ℤ → Gb → ℝ → ℂ) {i k a b : Fin 4} {c₀' : ℕ} (R : ℤ × ℤ) (cells : Finset (ℤ × ℤ)) (hsub : ∀ I ∈ cells, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R.1 R.2) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (hw : ∀ I ∈ cells, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) (hik : i ≠ k) (hia : i ≠ a) (hib : i ≠ b) (hka : k ≠ a) (hkb : k ≠ b) (hab : a ≠ b) (hagm : ∀ (I : ℤ × ℤ) (m : Ga), Measurable (aga I m)) (hagb : ∀ (I : ℤ × ℤ) (m : Ga) (y : ℝ), ‖aga I m y‖ ≤ 1) (hbgm : ∀ (I : ℤ × ℤ) (m : Gb), Measurable (agb I m)) (hbgb : ∀ (I : ℤ × ℤ) (m : Gb) (y : ℝ), ‖agb I m y‖ ≤ 1) (H' : ℝ) (hXi : PathCharts G cells (fun (I : ℤ × ℤ) (l : Xi.Λ) => Xi.atom I l) (fun (I : ℤ × ℤ) (l : Xi.Λ) => Xi.coef I l ≠ 0) c₀' H') (hXk : PathCharts G cells (fun (I : ℤ × ℤ) (l : Xk.Λ) => Xk.atom I l) (fun (I : ℤ × ℤ) (l : Xk.Λ) => Xk.coef I l ≠ 0) c₀' H') (hPa : PathCharts G cells (fun (I : ℤ × ℤ) (v : Wa) => Pa.scalarAt I v) (fun (I : ℤ × ℤ) (v : Wa) => v ∈ Pa.avail I) c₀' H') (hPb : PathCharts G cells (fun (I : ℤ × ℤ) (v : Wb) => Pb.scalarAt I v) (fun (I : ℤ × ℤ) (v : Wb) => v ∈ Pb.avail I) c₀' H') (hga : PathCharts G cells aga (fun (I : ℤ × ℤ) (m : Ga) => cga I m ≠ 0) c₀' H') (hgb : PathCharts G cells agb (fun (I : ℤ × ℤ) (m : Gb) => cgb I m ≠ 0) c₀' H') (hdef : ∃ (d : ℕ) (B : QuadraticChartData d), QuadraticChartComplexity c₀' H' B ∧ IsBoundedQuadraticChart B) (Dc : ℝ) (hDc : 1 ≤ Dc) (hPac : ∀ I ∈ cells, ∀ (v : Wa), ‖Pa.coef I Za v‖ ≤ Dc) (hPbc : ∀ I ∈ cells, ∀ (v : Wb), ‖Pb.coef I Zb v‖ ≤ Dc) (hcga : ∀ (I : ℤ × ℤ) (m : Ga), ‖cga I m‖ ≤ 1) (hcgb : ∀ (I : ℤ × ℤ) (m : Gb), ‖cgb I m‖ ≤ 1) (Ya Yb : ℤ × ℤ → ℝ → ℂ) (hYam : ∀ (I : ℤ × ℤ), Measurable (Ya I)) (hYbm : ∀ (I : ℤ × ℤ), Measurable (Yb I)) (S : ℝ) (hS : 0 ≤ S) (hUa : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (Ya I - baseHighB Pa Za cga aga I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))) (hUb : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (Yb I - baseHighB Pb Zb cgb agb I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))) (hUa' : ∀ (I : ℤ × ℤ), (MeasureTheory.eLpNorm (Ya I - baseHighB Pa Za cga aga I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))).toReal ≤ S) (hUb' : ∀ (I : ℤ × ℤ), (MeasureTheory.eLpNorm (Yb I - baseHighB Pb Zb cgb agb I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))).toReal ≤ S) (η : ℝ) (hsmall : ∀ I ∈ cells, ‖localProgressionForm (dyadicGridLength G I.1) (w I) (slots4 a i k (Ya I) (Xi.val I) (Xk.val I) (Yb I))‖ ≤ η) (I : ℤ × ℤ) : (baseActiveSetup κ Xi Xk Pa Pb Za Zb cga aga cgb agb R cells hsub w hw hik hia hib hka hkb hab hagm hagb hbgm hbgb H' hXi hXk hPa hPb hga hgb hdef Dc hDc hPac hPbc hcga hcgb Ya Yb hYam hYbm S hS hUa hUb hUa' hUb' η hsmall).U a I = Ya I - baseHighB Pa Za cga aga I

theorem TrilinearHT.Auto.baseActiveSetup_U_b (κ : LocalKernelClass) {G : RealDyadicGrid} {J : ℤ × ℤ} {N c₀ : ℕ} {H : ℝ} (Xi Xk : LowList G J N J c₀ H) {Wa Wb : Type} [Fintype Wa] [Fintype Wb] (Pa : PathColumnSystem G J N Wa) (Pb : PathColumnSystem G J N Wb) (Za : ↥(ColumnL2 Wa)) (Zb : ↥(ColumnL2 Wb)) {Ga Gb : Type} [Fintype Ga] [Fintype Gb] (cga : ℤ × ℤ → Ga → ℂ) (aga : ℤ × ℤ → Ga → ℝ → ℂ) (cgb : ℤ × ℤ → Gb → ℂ) (agb : ℤ × ℤ → Gb → ℝ → ℂ) {i k a b : Fin 4} {c₀' : ℕ} (R : ℤ × ℤ) (cells : Finset (ℤ × ℤ)) (hsub : ∀ I ∈ cells, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R.1 R.2) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (hw : ∀ I ∈ cells, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) (hik : i ≠ k) (hia : i ≠ a) (hib : i ≠ b) (hka : k ≠ a) (hkb : k ≠ b) (hab : a ≠ b) (hagm : ∀ (I : ℤ × ℤ) (m : Ga), Measurable (aga I m)) (hagb : ∀ (I : ℤ × ℤ) (m : Ga) (y : ℝ), ‖aga I m y‖ ≤ 1) (hbgm : ∀ (I : ℤ × ℤ) (m : Gb), Measurable (agb I m)) (hbgb : ∀ (I : ℤ × ℤ) (m : Gb) (y : ℝ), ‖agb I m y‖ ≤ 1) (H' : ℝ) (hXi : PathCharts G cells (fun (I : ℤ × ℤ) (l : Xi.Λ) => Xi.atom I l) (fun (I : ℤ × ℤ) (l : Xi.Λ) => Xi.coef I l ≠ 0) c₀' H') (hXk : PathCharts G cells (fun (I : ℤ × ℤ) (l : Xk.Λ) => Xk.atom I l) (fun (I : ℤ × ℤ) (l : Xk.Λ) => Xk.coef I l ≠ 0) c₀' H') (hPa : PathCharts G cells (fun (I : ℤ × ℤ) (v : Wa) => Pa.scalarAt I v) (fun (I : ℤ × ℤ) (v : Wa) => v ∈ Pa.avail I) c₀' H') (hPb : PathCharts G cells (fun (I : ℤ × ℤ) (v : Wb) => Pb.scalarAt I v) (fun (I : ℤ × ℤ) (v : Wb) => v ∈ Pb.avail I) c₀' H') (hga : PathCharts G cells aga (fun (I : ℤ × ℤ) (m : Ga) => cga I m ≠ 0) c₀' H') (hgb : PathCharts G cells agb (fun (I : ℤ × ℤ) (m : Gb) => cgb I m ≠ 0) c₀' H') (hdef : ∃ (d : ℕ) (B : QuadraticChartData d), QuadraticChartComplexity c₀' H' B ∧ IsBoundedQuadraticChart B) (Dc : ℝ) (hDc : 1 ≤ Dc) (hPac : ∀ I ∈ cells, ∀ (v : Wa), ‖Pa.coef I Za v‖ ≤ Dc) (hPbc : ∀ I ∈ cells, ∀ (v : Wb), ‖Pb.coef I Zb v‖ ≤ Dc) (hcga : ∀ (I : ℤ × ℤ) (m : Ga), ‖cga I m‖ ≤ 1) (hcgb : ∀ (I : ℤ × ℤ) (m : Gb), ‖cgb I m‖ ≤ 1) (Ya Yb : ℤ × ℤ → ℝ → ℂ) (hYam : ∀ (I : ℤ × ℤ), Measurable (Ya I)) (hYbm : ∀ (I : ℤ × ℤ), Measurable (Yb I)) (S : ℝ) (hS : 0 ≤ S) (hUa : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (Ya I - baseHighB Pa Za cga aga I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))) (hUb : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (Yb I - baseHighB Pb Zb cgb agb I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))) (hUa' : ∀ (I : ℤ × ℤ), (MeasureTheory.eLpNorm (Ya I - baseHighB Pa Za cga aga I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))).toReal ≤ S) (hUb' : ∀ (I : ℤ × ℤ), (MeasureTheory.eLpNorm (Yb I - baseHighB Pb Zb cgb agb I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))).toReal ≤ S) (η : ℝ) (hsmall : ∀ I ∈ cells, ‖localProgressionForm (dyadicGridLength G I.1) (w I) (slots4 a i k (Ya I) (Xi.val I) (Xk.val I) (Yb I))‖ ≤ η) (I : ℤ × ℤ) : (baseActiveSetup κ Xi Xk Pa Pb Za Zb cga aga cgb agb R cells hsub w hw hik hia hib hka hkb hab hagm hagb hbgm hbgb H' hXi hXk hPa hPb hga hgb hdef Dc hDc hPac hPbc hcga hcgb Ya Yb hYam hYbm S hS hUa hUb hUa' hUb' η hsmall).U b I = Yb I - baseHighB Pb Zb cgb agb I

theorem TrilinearHT.Auto.baseActiveSetup_B (κ : LocalKernelClass) {G : RealDyadicGrid} {J : ℤ × ℤ} {N c₀ : ℕ} {H : ℝ} (Xi Xk : LowList G J N J c₀ H) {Wa Wb : Type} [Fintype Wa] [Fintype Wb] (Pa : PathColumnSystem G J N Wa) (Pb : PathColumnSystem G J N Wb) (Za : ↥(ColumnL2 Wa)) (Zb : ↥(ColumnL2 Wb)) {Ga Gb : Type} [Fintype Ga] [Fintype Gb] (cga : ℤ × ℤ → Ga → ℂ) (aga : ℤ × ℤ → Ga → ℝ → ℂ) (cgb : ℤ × ℤ → Gb → ℂ) (agb : ℤ × ℤ → Gb → ℝ → ℂ) {i k a b : Fin 4} {c₀' : ℕ} (R : ℤ × ℤ) (cells : Finset (ℤ × ℤ)) (hsub : ∀ I ∈ cells, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R.1 R.2) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (hw : ∀ I ∈ cells, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) (hik : i ≠ k) (hia : i ≠ a) (hib : i ≠ b) (hka : k ≠ a) (hkb : k ≠ b) (hab : a ≠ b) (hagm : ∀ (I : ℤ × ℤ) (m : Ga), Measurable (aga I m)) (hagb : ∀ (I : ℤ × ℤ) (m : Ga) (y : ℝ), ‖aga I m y‖ ≤ 1) (hbgm : ∀ (I : ℤ × ℤ) (m : Gb), Measurable (agb I m)) (hbgb : ∀ (I : ℤ × ℤ) (m : Gb) (y : ℝ), ‖agb I m y‖ ≤ 1) (H' : ℝ) (hXi : PathCharts G cells (fun (I : ℤ × ℤ) (l : Xi.Λ) => Xi.atom I l) (fun (I : ℤ × ℤ) (l : Xi.Λ) => Xi.coef I l ≠ 0) c₀' H') (hXk : PathCharts G cells (fun (I : ℤ × ℤ) (l : Xk.Λ) => Xk.atom I l) (fun (I : ℤ × ℤ) (l : Xk.Λ) => Xk.coef I l ≠ 0) c₀' H') (hPa : PathCharts G cells (fun (I : ℤ × ℤ) (v : Wa) => Pa.scalarAt I v) (fun (I : ℤ × ℤ) (v : Wa) => v ∈ Pa.avail I) c₀' H') (hPb : PathCharts G cells (fun (I : ℤ × ℤ) (v : Wb) => Pb.scalarAt I v) (fun (I : ℤ × ℤ) (v : Wb) => v ∈ Pb.avail I) c₀' H') (hga : PathCharts G cells aga (fun (I : ℤ × ℤ) (m : Ga) => cga I m ≠ 0) c₀' H') (hgb : PathCharts G cells agb (fun (I : ℤ × ℤ) (m : Gb) => cgb I m ≠ 0) c₀' H') (hdef : ∃ (d : ℕ) (B : QuadraticChartData d), QuadraticChartComplexity c₀' H' B ∧ IsBoundedQuadraticChart B) (Dc : ℝ) (hDc : 1 ≤ Dc) (hPac : ∀ I ∈ cells, ∀ (v : Wa), ‖Pa.coef I Za v‖ ≤ Dc) (hPbc : ∀ I ∈ cells, ∀ (v : Wb), ‖Pb.coef I Zb v‖ ≤ Dc) (hcga : ∀ (I : ℤ × ℤ) (m : Ga), ‖cga I m‖ ≤ 1) (hcgb : ∀ (I : ℤ × ℤ) (m : Gb), ‖cgb I m‖ ≤ 1) (Ya Yb : ℤ × ℤ → ℝ → ℂ) (hYam : ∀ (I : ℤ × ℤ), Measurable (Ya I)) (hYbm : ∀ (I : ℤ × ℤ), Measurable (Yb I)) (S : ℝ) (hS : 0 ≤ S) (hUa : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (Ya I - baseHighB Pa Za cga aga I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))) (hUb : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (Yb I - baseHighB Pb Zb cgb agb I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))) (hUa' : ∀ (I : ℤ × ℤ), (MeasureTheory.eLpNorm (Ya I - baseHighB Pa Za cga aga I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))).toReal ≤ S) (hUb' : ∀ (I : ℤ × ℤ), (MeasureTheory.eLpNorm (Yb I - baseHighB Pb Zb cgb agb I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))).toReal ≤ S) (η : ℝ) (hsmall : ∀ I ∈ cells, ‖localProgressionForm (dyadicGridLength G I.1) (w I) (slots4 a i k (Ya I) (Xi.val I) (Xk.val I) (Yb I))‖ ≤ η) {I : ℤ × ℤ} (hI : I ∈ cells) (l : Fin 4) : (baseActiveSetup κ Xi Xk Pa Pb Za Zb cga aga cgb agb R cells hsub w hw hik hia hib hka hkb hab hagm hagb hbgm hbgb H' hXi hXk hPa hPb hga hgb hdef Dc hDc hPac hPbc hcga hcgb Ya Yb hYam hYbm S hS hUa hUb hUa' hUb' η hsmall).B l I = fun (x : ℝ) => ∑ v : BaseLabel Xi Xk, baseCoef Xi Xk Pa Pb Za Zb cga cgb i k a b l I v * baseAtom Xi Xk Pa Pb aga agb I v x

theorem TrilinearHT.Auto.baseActiveSetup_Y (κ : LocalKernelClass) {G : RealDyadicGrid} {J : ℤ × ℤ} {N c₀ : ℕ} {H : ℝ} (Xi Xk : LowList G J N J c₀ H) {Wa Wb : Type} [Fintype Wa] [Fintype Wb] (Pa : PathColumnSystem G J N Wa) (Pb : PathColumnSystem G J N Wb) (Za : ↥(ColumnL2 Wa)) (Zb : ↥(ColumnL2 Wb)) {Ga Gb : Type} [Fintype Ga] [Fintype Gb] (cga : ℤ × ℤ → Ga → ℂ) (aga : ℤ × ℤ → Ga → ℝ → ℂ) (cgb : ℤ × ℤ → Gb → ℂ) (agb : ℤ × ℤ → Gb → ℝ → ℂ) {i k a b : Fin 4} {c₀' : ℕ} (R : ℤ × ℤ) (cells : Finset (ℤ × ℤ)) (hsub : ∀ I ∈ cells, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R.1 R.2) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (hw : ∀ I ∈ cells, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) (hik : i ≠ k) (hia : i ≠ a) (hib : i ≠ b) (hka : k ≠ a) (hkb : k ≠ b) (hab : a ≠ b) (hagm : ∀ (I : ℤ × ℤ) (m : Ga), Measurable (aga I m)) (hagb : ∀ (I : ℤ × ℤ) (m : Ga) (y : ℝ), ‖aga I m y‖ ≤ 1) (hbgm : ∀ (I : ℤ × ℤ) (m : Gb), Measurable (agb I m)) (hbgb : ∀ (I : ℤ × ℤ) (m : Gb) (y : ℝ), ‖agb I m y‖ ≤ 1) (H' : ℝ) (hXi : PathCharts G cells (fun (I : ℤ × ℤ) (l : Xi.Λ) => Xi.atom I l) (fun (I : ℤ × ℤ) (l : Xi.Λ) => Xi.coef I l ≠ 0) c₀' H') (hXk : PathCharts G cells (fun (I : ℤ × ℤ) (l : Xk.Λ) => Xk.atom I l) (fun (I : ℤ × ℤ) (l : Xk.Λ) => Xk.coef I l ≠ 0) c₀' H') (hPa : PathCharts G cells (fun (I : ℤ × ℤ) (v : Wa) => Pa.scalarAt I v) (fun (I : ℤ × ℤ) (v : Wa) => v ∈ Pa.avail I) c₀' H') (hPb : PathCharts G cells (fun (I : ℤ × ℤ) (v : Wb) => Pb.scalarAt I v) (fun (I : ℤ × ℤ) (v : Wb) => v ∈ Pb.avail I) c₀' H') (hga : PathCharts G cells aga (fun (I : ℤ × ℤ) (m : Ga) => cga I m ≠ 0) c₀' H') (hgb : PathCharts G cells agb (fun (I : ℤ × ℤ) (m : Gb) => cgb I m ≠ 0) c₀' H') (hdef : ∃ (d : ℕ) (B : QuadraticChartData d), QuadraticChartComplexity c₀' H' B ∧ IsBoundedQuadraticChart B) (Dc : ℝ) (hDc : 1 ≤ Dc) (hPac : ∀ I ∈ cells, ∀ (v : Wa), ‖Pa.coef I Za v‖ ≤ Dc) (hPbc : ∀ I ∈ cells, ∀ (v : Wb), ‖Pb.coef I Zb v‖ ≤ Dc) (hcga : ∀ (I : ℤ × ℤ) (m : Ga), ‖cga I m‖ ≤ 1) (hcgb : ∀ (I : ℤ × ℤ) (m : Gb), ‖cgb I m‖ ≤ 1) (Ya Yb : ℤ × ℤ → ℝ → ℂ) (hYam : ∀ (I : ℤ × ℤ), Measurable (Ya I)) (hYbm : ∀ (I : ℤ × ℤ), Measurable (Yb I)) (S : ℝ) (hS : 0 ≤ S) (hUa : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (Ya I - baseHighB Pa Za cga aga I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))) (hUb : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (Yb I - baseHighB Pb Zb cgb agb I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))) (hUa' : ∀ (I : ℤ × ℤ), (MeasureTheory.eLpNorm (Ya I - baseHighB Pa Za cga aga I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))).toReal ≤ S) (hUb' : ∀ (I : ℤ × ℤ), (MeasureTheory.eLpNorm (Yb I - baseHighB Pb Zb cgb agb I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))).toReal ≤ S) (η : ℝ) (hsmall : ∀ I ∈ cells, ‖localProgressionForm (dyadicGridLength G I.1) (w I) (slots4 a i k (Ya I) (Xi.val I) (Xk.val I) (Yb I))‖ ≤ η) {I : ℤ × ℤ} (hI : I ∈ cells) : (baseActiveSetup κ Xi Xk Pa Pb Za Zb cga aga cgb agb R cells hsub w hw hik hia hib hka hkb hab hagm hagb hbgm hbgb H' hXi hXk hPa hPb hga hgb hdef Dc hDc hPac hPbc hcga hcgb Ya Yb hYam hYbm S hS hUa hUb hUa' hUb' η hsmall).Y I = slots4 a i k (Ya I) (Xi.val I) (Xk.val I) (Yb I)

theorem TrilinearHT.Auto.baseActiveSetup_z3 (κ : LocalKernelClass) {G : RealDyadicGrid} {J : ℤ × ℤ} {N c₀ : ℕ} {H : ℝ} (Xi Xk : LowList G J N J c₀ H) {Wa Wb : Type} [Fintype Wa] [Fintype Wb] (Pa : PathColumnSystem G J N Wa) (Pb : PathColumnSystem G J N Wb) (Za : ↥(ColumnL2 Wa)) (Zb : ↥(ColumnL2 Wb)) {Ga Gb : Type} [Fintype Ga] [Fintype Gb] (cga : ℤ × ℤ → Ga → ℂ) (aga : ℤ × ℤ → Ga → ℝ → ℂ) (cgb : ℤ × ℤ → Gb → ℂ) (agb : ℤ × ℤ → Gb → ℝ → ℂ) {i k a b : Fin 4} {c₀' : ℕ} (R : ℤ × ℤ) (cells : Finset (ℤ × ℤ)) (hsub : ∀ I ∈ cells, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R.1 R.2) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (hw : ∀ I ∈ cells, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) (hik : i ≠ k) (hia : i ≠ a) (hib : i ≠ b) (hka : k ≠ a) (hkb : k ≠ b) (hab : a ≠ b) (hagm : ∀ (I : ℤ × ℤ) (m : Ga), Measurable (aga I m)) (hagb : ∀ (I : ℤ × ℤ) (m : Ga) (y : ℝ), ‖aga I m y‖ ≤ 1) (hbgm : ∀ (I : ℤ × ℤ) (m : Gb), Measurable (agb I m)) (hbgb : ∀ (I : ℤ × ℤ) (m : Gb) (y : ℝ), ‖agb I m y‖ ≤ 1) (H' : ℝ) (hXi : PathCharts G cells (fun (I : ℤ × ℤ) (l : Xi.Λ) => Xi.atom I l) (fun (I : ℤ × ℤ) (l : Xi.Λ) => Xi.coef I l ≠ 0) c₀' H') (hXk : PathCharts G cells (fun (I : ℤ × ℤ) (l : Xk.Λ) => Xk.atom I l) (fun (I : ℤ × ℤ) (l : Xk.Λ) => Xk.coef I l ≠ 0) c₀' H') (hPa : PathCharts G cells (fun (I : ℤ × ℤ) (v : Wa) => Pa.scalarAt I v) (fun (I : ℤ × ℤ) (v : Wa) => v ∈ Pa.avail I) c₀' H') (hPb : PathCharts G cells (fun (I : ℤ × ℤ) (v : Wb) => Pb.scalarAt I v) (fun (I : ℤ × ℤ) (v : Wb) => v ∈ Pb.avail I) c₀' H') (hga : PathCharts G cells aga (fun (I : ℤ × ℤ) (m : Ga) => cga I m ≠ 0) c₀' H') (hgb : PathCharts G cells agb (fun (I : ℤ × ℤ) (m : Gb) => cgb I m ≠ 0) c₀' H') (hdef : ∃ (d : ℕ) (B : QuadraticChartData d), QuadraticChartComplexity c₀' H' B ∧ IsBoundedQuadraticChart B) (Dc : ℝ) (hDc : 1 ≤ Dc) (hPac : ∀ I ∈ cells, ∀ (v : Wa), ‖Pa.coef I Za v‖ ≤ Dc) (hPbc : ∀ I ∈ cells, ∀ (v : Wb), ‖Pb.coef I Zb v‖ ≤ Dc) (hcga : ∀ (I : ℤ × ℤ) (m : Ga), ‖cga I m‖ ≤ 1) (hcgb : ∀ (I : ℤ × ℤ) (m : Gb), ‖cgb I m‖ ≤ 1) (Ya Yb : ℤ × ℤ → ℝ → ℂ) (hYam : ∀ (I : ℤ × ℤ), Measurable (Ya I)) (hYbm : ∀ (I : ℤ × ℤ), Measurable (Yb I)) (S : ℝ) (hS : 0 ≤ S) (hUa : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (Ya I - baseHighB Pa Za cga aga I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))) (hUb : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (Yb I - baseHighB Pb Zb cgb agb I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))) (hUa' : ∀ (I : ℤ × ℤ), (MeasureTheory.eLpNorm (Ya I - baseHighB Pa Za cga aga I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))).toReal ≤ S) (hUb' : ∀ (I : ℤ × ℤ), (MeasureTheory.eLpNorm (Yb I - baseHighB Pb Zb cgb agb I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))).toReal ≤ S) (η : ℝ) (hsmall : ∀ I ∈ cells, ‖localProgressionForm (dyadicGridLength G I.1) (w I) (slots4 a i k (Ya I) (Xi.val I) (Xk.val I) (Yb I))‖ ≤ η) {I : ℤ × ℤ} (hI : I ∈ cells) : (baseActiveSetup κ Xi Xk Pa Pb Za Zb cga aga cgb agb R cells hsub w hw hik hia hib hka hkb hab hagm hagb hbgm hbgb H' hXi hXk hPa hPb hga hgb hdef Dc hDc hPac hPbc hcga hcgb Ya Yb hYam hYbm S hS hUa hUb hUa' hUb' η hsmall).z 3 I = slots4 a i k (Ya I - baseHighB Pa Za cga aga I) (Xi.val I) (Xk.val I) (Yb I - baseHighB Pb Zb cgb agb I)

theorem TrilinearHT.Auto.baseActiveSetup_columnRepBelow (κ : LocalKernelClass) {G : RealDyadicGrid} {J : ℤ × ℤ} {N c₀ : ℕ} {H : ℝ} (Xi Xk : LowList G J N J c₀ H) {Wa Wb : Type} [Fintype Wa] [Fintype Wb] (Pa : PathColumnSystem G J N Wa) (Pb : PathColumnSystem G J N Wb) (Za : ↥(ColumnL2 Wa)) (Zb : ↥(ColumnL2 Wb)) {Ga Gb : Type} [Fintype Ga] [Fintype Gb] (cga : ℤ × ℤ → Ga → ℂ) (aga : ℤ × ℤ → Ga → ℝ → ℂ) (cgb : ℤ × ℤ → Gb → ℂ) (agb : ℤ × ℤ → Gb → ℝ → ℂ) {i k a b : Fin 4} {c₀' : ℕ} (R : ℤ × ℤ) (cells : Finset (ℤ × ℤ)) (hsub : ∀ I ∈ cells, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R.1 R.2) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (hw : ∀ I ∈ cells, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) (hik : i ≠ k) (hia : i ≠ a) (hib : i ≠ b) (hka : k ≠ a) (hkb : k ≠ b) (hab : a ≠ b) (hagm : ∀ (I : ℤ × ℤ) (m : Ga), Measurable (aga I m)) (hagb : ∀ (I : ℤ × ℤ) (m : Ga) (y : ℝ), ‖aga I m y‖ ≤ 1) (hbgm : ∀ (I : ℤ × ℤ) (m : Gb), Measurable (agb I m)) (hbgb : ∀ (I : ℤ × ℤ) (m : Gb) (y : ℝ), ‖agb I m y‖ ≤ 1) (H' : ℝ) (hXi : PathCharts G cells (fun (I : ℤ × ℤ) (l : Xi.Λ) => Xi.atom I l) (fun (I : ℤ × ℤ) (l : Xi.Λ) => Xi.coef I l ≠ 0) c₀' H') (hXk : PathCharts G cells (fun (I : ℤ × ℤ) (l : Xk.Λ) => Xk.atom I l) (fun (I : ℤ × ℤ) (l : Xk.Λ) => Xk.coef I l ≠ 0) c₀' H') (hPa : PathCharts G cells (fun (I : ℤ × ℤ) (v : Wa) => Pa.scalarAt I v) (fun (I : ℤ × ℤ) (v : Wa) => v ∈ Pa.avail I) c₀' H') (hPb : PathCharts G cells (fun (I : ℤ × ℤ) (v : Wb) => Pb.scalarAt I v) (fun (I : ℤ × ℤ) (v : Wb) => v ∈ Pb.avail I) c₀' H') (hga : PathCharts G cells aga (fun (I : ℤ × ℤ) (m : Ga) => cga I m ≠ 0) c₀' H') (hgb : PathCharts G cells agb (fun (I : ℤ × ℤ) (m : Gb) => cgb I m ≠ 0) c₀' H') (hdef : ∃ (d : ℕ) (B : QuadraticChartData d), QuadraticChartComplexity c₀' H' B ∧ IsBoundedQuadraticChart B) (Dc : ℝ) (hDc : 1 ≤ Dc) (hPac : ∀ I ∈ cells, ∀ (v : Wa), ‖Pa.coef I Za v‖ ≤ Dc) (hPbc : ∀ I ∈ cells, ∀ (v : Wb), ‖Pb.coef I Zb v‖ ≤ Dc) (hcga : ∀ (I : ℤ × ℤ) (m : Ga), ‖cga I m‖ ≤ 1) (hcgb : ∀ (I : ℤ × ℤ) (m : Gb), ‖cgb I m‖ ≤ 1) (Ya Yb : ℤ × ℤ → ℝ → ℂ) (hYam : ∀ (I : ℤ × ℤ), Measurable (Ya I)) (hYbm : ∀ (I : ℤ × ℤ), Measurable (Yb I)) (S : ℝ) (hS : 0 ≤ S) (hUa : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (Ya I - baseHighB Pa Za cga aga I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))) (hUb : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (Yb I - baseHighB Pb Zb cgb agb I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))) (hUa' : ∀ (I : ℤ × ℤ), (MeasureTheory.eLpNorm (Ya I - baseHighB Pa Za cga aga I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))).toReal ≤ S) (hUb' : ∀ (I : ℤ × ℤ), (MeasureTheory.eLpNorm (Yb I - baseHighB Pb Zb cgb agb I) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))).toReal ≤ S) (η : ℝ) (hsmall : ∀ I ∈ cells, ‖localProgressionForm (dyadicGridLength G I.1) (w I) (slots4 a i k (Ya I) (Xi.val I) (Xk.val I) (Yb I))‖ ≤ η) {CF X : ℝ} (R' : ℤ × ℤ) (hX : X ≤ 2 + ↑(Fintype.card Xi.Λ + Fintype.card Xk.Λ + (Fintype.card Wa + Fintype.card Ga) + (Fintype.card Wb + Fintype.card Gb)) * (1 + Dc)) (hri : ∃ (P₁ : BasicProjection G R' CF) (P₂ : BasicProjection G R' CF), P₁.Ψ.D.budget ≤ X ∧ P₂.Ψ.D.budget ≤ X ∧ P₁.HasChartsOn {I : ℤ × ℤ | I ∈ cells ∧ dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R'.1 R'.2} c₀' H' ∧ P₂.HasChartsOn {I : ℤ × ℤ | I ∈ cells ∧ dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R'.1 R'.2} c₀' H' ∧ P₁.CellEnergyOn {I : ℤ × ℤ | I ∈ cells ∧ dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R'.1 R'.2} ∧ P₂.CellEnergyOn {I : ℤ × ℤ | I ∈ cells ∧ dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R'.1 R'.2} ∧ ∀ I ∈ cells, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R'.1 R'.2 → ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → Xi.val I y = P₁.val I y - P₂.val I y) (hrk : ∃ (P₁ : BasicProjection G R' CF) (P₂ : BasicProjection G R' CF), P₁.Ψ.D.budget ≤ X ∧ P₂.Ψ.D.budget ≤ X ∧ P₁.HasChartsOn {I : ℤ × ℤ | I ∈ cells ∧ dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R'.1 R'.2} c₀' H' ∧ P₂.HasChartsOn {I : ℤ × ℤ | I ∈ cells ∧ dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R'.1 R'.2} c₀' H' ∧ P₁.CellEnergyOn {I : ℤ × ℤ | I ∈ cells ∧ dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R'.1 R'.2} ∧ P₂.CellEnergyOn {I : ℤ × ℤ | I ∈ cells ∧ dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R'.1 R'.2} ∧ ∀ I ∈ cells, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R'.1 R'.2 → ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → Xk.val I y = P₁.val I y - P₂.val I y) (hra : ∃ (P₁ : BasicProjection G R' CF) (P₂ : BasicProjection G R' CF), P₁.Ψ.D.budget ≤ X ∧ P₂.Ψ.D.budget ≤ X ∧ P₁.HasChartsOn {I : ℤ × ℤ | I ∈ cells ∧ dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R'.1 R'.2} c₀' H' ∧ P₂.HasChartsOn {I : ℤ × ℤ | I ∈ cells ∧ dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R'.1 R'.2} c₀' H' ∧ P₁.CellEnergyOn {I : ℤ × ℤ | I ∈ cells ∧ dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R'.1 R'.2} ∧ P₂.CellEnergyOn {I : ℤ × ℤ | I ∈ cells ∧ dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R'.1 R'.2} ∧ ∀ I ∈ cells, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R'.1 R'.2 → ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → ∑ v : Wa, Pa.coef I Za v * Pa.scalarAt I v y - ∑ m : Ga, cga I m * aga I m y = P₁.val I y - P₂.val I y) (hrb : ∃ (P₁ : BasicProjection G R' CF) (P₂ : BasicProjection G R' CF), P₁.Ψ.D.budget ≤ X ∧ P₂.Ψ.D.budget ≤ X ∧ P₁.HasChartsOn {I : ℤ × ℤ | I ∈ cells ∧ dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R'.1 R'.2} c₀' H' ∧ P₂.HasChartsOn {I : ℤ × ℤ | I ∈ cells ∧ dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R'.1 R'.2} c₀' H' ∧ P₁.CellEnergyOn {I : ℤ × ℤ | I ∈ cells ∧ dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R'.1 R'.2} ∧ P₂.CellEnergyOn {I : ℤ × ℤ | I ∈ cells ∧ dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R'.1 R'.2} ∧ ∀ I ∈ cells, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R'.1 R'.2 → ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → ∑ v : Wb, Pb.coef I Zb v * Pb.scalarAt I v y - ∑ m : Gb, cgb I m * agb I m y = P₁.val I y - P₂.val I y) : (baseActiveSetup κ Xi Xk Pa Pb Za Zb cga aga cgb agb R cells hsub w hw hik hia hib hka hkb hab hagm hagb hbgm hbgb H' hXi hXk hPa hPb hga hgb hdef Dc hDc hPac hPbc hcga hcgb Ya Yb hYam hYbm S hS hUa hUb hUa' hUb' η hsmall).ColumnRepBelow R' CF

The column representation below a sub-root R' of the base active setup from the representations of its four basic arguments below R' (blueprint prop:base, lines 1611-1613).

theorem TrilinearHT.Auto.AccSetup.memLp_normalized_of_bound {a r : ℝ} (hr : 0 < r) {g : ℝ → ℂ} (hg : Measurable g) {C : ℝ} (hC : ∀ (y : ℝ), ‖g y‖ ≤ C) : MeasureTheory.MemLp g 2 (normalizedIntervalMeasure a r)

theorem TrilinearHT.Auto.AccSetup.U_measurable (S : AccSetup) (K I : ℤ × ℤ) : Measurable fun (y : ℝ) => S.phys I (S.tree.st I).1 (S.tree.st I).2 y - S.cur K I y

theorem TrilinearHT.Auto.AccSetup.U_bound (S : AccSetup) (K I : ℤ × ℤ) : ∃ (C : ℝ), ∀ (y : ℝ), ‖S.phys I (S.tree.st I).1 (S.tree.st I).2 y - S.cur K I y‖ ≤ C

theorem TrilinearHT.Auto.AccSetup.U_memLp (S : AccSetup) (K I : ℤ × ℤ) : MeasureTheory.MemLp (fun (y : ℝ) => S.phys I (S.tree.st I).1 (S.tree.st I).2 y - S.cur K I y) 2 (normalizedIntervalMeasure (dyadicGridLeft S.G I.1 I.2) (dyadicGridLength S.G I.1))

theorem TrilinearHT.Auto.AccSetup.U_sq_eq (S : AccSetup) (K I : ℤ × ℤ) : dyadicGridLength S.G I.1 * (MeasureTheory.eLpNorm (fun (y : ℝ) => S.phys I (S.tree.st I).1 (S.tree.st I).2 y - S.cur K I y) 2 (normalizedIntervalMeasure (dyadicGridLeft S.G I.1 I.2) (dyadicGridLength S.G I.1))).toReal ^ 2 = ∫ (y : ℝ) in S.cell I, ‖S.phys I (S.tree.st I).1 (S.tree.st I).2 y - S.cur K I y‖ ^ 2

The length-weighted squared normalized norm of a basic side is its L²(I) energy.

theorem TrilinearHT.Auto.AccSetup.Hyp.U_eLpNorm_le {S : AccSetup} (h : S.Hyp) {K I : ℤ × ℤ} (hIc : I ∈ dyadicFiniteTree S.G S.J S.Nc) (hIH : kernelHull S.G S.J S.N S.w I) : (MeasureTheory.eLpNorm (fun (y : ℝ) => S.phys I (S.tree.st I).1 (S.tree.st I).2 y - S.cur K I y) 2 (normalizedIntervalMeasure (dyadicGridLeft S.G I.1 I.2) (dyadicGridLength S.G I.1))).toReal ≤ 2

theorem TrilinearHT.Auto.AccSetup.Hyp.phys_eLpNorm_le {S : AccSetup} (h : S.Hyp) {I : ℤ × ℤ} (hIc : I ∈ dyadicFiniteTree S.G S.J S.Nc) (hIH : kernelHull S.G S.J S.N S.w I) (a : ℕ → ℝ → ℂ) (n : ℕ) : MeasureTheory.eLpNorm (S.phys I a n) 2 (normalizedIntervalMeasure (dyadicGridLeft S.G I.1 I.2) (dyadicGridLength S.G I.1)) ≤ ENNReal.ofReal 1

The fine projections have normalized L² norm at most one on a coarse cell.

The base data on one root

def TrilinearHT.Auto.IsBasicOn (G : RealDyadicGrid) (J : ℤ × ℤ) (N : ℕ) (CF Bd : ℝ) (c : ℕ) (Hc : ℝ) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (z : ℤ × ℤ → ℝ → ℂ) : Prop

A family of cell functions that is a basic projection below every tree cell: the physical part of the current projections of one column depth family whose root contains J, whose column budget is at most Bd and whose columns available on tree cells are charts of order c and complexity at most Hc there, applied to an augmented input of energy at most CF |R| on every tree cell R.

Equations

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

theorem TrilinearHT.Auto.kernelHull_below_iff {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {w : ℤ × ℤ → ℝ × ℝ → ℂ} {R : ℤ × ℤ} (hR : R ∈ dyadicFiniteTree G J N) {c : ℤ × ℤ} (hc : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G R.1 R.2) : kernelHull G R (dyadicRemainingDepth J N R) w c ↔ kernelHull G J N w c

The kernel hull of a subtree is the kernel hull of the tree restricted to the subtree.

theorem TrilinearHT.Auto.IsBasicOn.basicProjection {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {CF Bd : ℝ} {c : ℕ} {Hc : ℝ} {w : ℤ × ℤ → ℝ × ℝ → ℂ} {z : ℤ × ℤ → ℝ → ℂ} (h : IsBasicOn G J N CF Bd c Hc w z) {R : ℤ × ℤ} (hR : R ∈ dyadicFiniteTree G J N) (hRH : kernelHull G J N w R) : ∃ (P : BasicProjection G R CF), P.Ψ.D.budget ≤ Bd ∧ P.HasChartsOn {c' : ℤ × ℤ | c' ∈ dyadicFiniteTree G J N} c Hc ∧ P.CellEnergyOn {c' : ℤ × ℤ | c' ∈ dyadicFiniteTree G J N ∧ kernelHull G J N w c'} ∧ ∀ (I : ℤ × ℤ), z I = P.val I

theorem TrilinearHT.Auto.IsBasicOn.mono_budget {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {CF Bd Bd' : ℝ} {c : ℕ} {Hc : ℝ} {w : ℤ × ℤ → ℝ × ℝ → ℂ} {z : ℤ × ℤ → ℝ → ℂ} (h : IsBasicOn G J N CF Bd c Hc w z) (hB : Bd ≤ Bd') : IsBasicOn G J N CF Bd' c Hc w z

Enlarging the column budget of a basic family.

theorem TrilinearHT.Auto.IsBasicOn.mono_chart {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {CF Bd : ℝ} {c c' : ℕ} {Hc Hc' : ℝ} {w : ℤ × ℤ → ℝ × ℝ → ℂ} {z : ℤ × ℤ → ℝ → ℂ} (h : IsBasicOn G J N CF Bd c Hc w z) (hc : c ≤ c') (hH : Hc ≤ Hc') : IsBasicOn G J N CF Bd c' Hc' w z

Enlarging the chart order and complexity of a basic family.

theorem TrilinearHT.Auto.IsBasicOn.zeroProjection {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {CF Bd : ℝ} {c : ℕ} {Hc : ℝ} {w : ℤ × ℤ → ℝ × ℝ → ℂ} {z : ℤ × ℤ → ℝ → ℂ} (h : IsBasicOn G J N CF Bd c Hc w z) (hCF : 0 ≤ CF) {R : ℤ × ℤ} (hR : dyadicGridCell G R.1 R.2 ⊆ dyadicGridCell G J.1 J.2) : ∃ (P : BasicProjection G R CF), P.Ψ.D.budget ≤ Bd ∧ P.HasChartsOn {c' : ℤ × ℤ | c' ∈ dyadicFiniteTree G J N} c Hc

A basic projection with zero input below any sub-cell of the root of a basic family.