Trilinear Hilbert transform: bandStack_block

theorem TrilinearHT.Auto.ActiveSetup.bandStack_block {κ' : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ' c₀) (hanc : A.AncClosed) {V : Type u_1} [Fintype V] (Zg : ℤ → ↥(ColumnL2 V)) {K N : ℕ} (hKN : K ≤ 2 ^ N) (k : Fin (N + 1)) (hk : ↑k ≠ N) (β : ℕ) (Ug : Finset (ℤ × ℤ)) (off : ℤ × ℤ → ℕ) (hoff : ∀ (J : ℤ × ℤ), ∀ m < K, J.1 = A.R.1 + ↑(K * β + m) → off J = m) (hU : ∀ I ∈ Ug, I ∈ A.cells ∧ I.1 = A.R.1 + ↑(K * β + off I) ∧ off I < K) {P : ℕ} (Ah : ℕ → ℤ → ↥(ColumnL2 V) →L[ℂ] ↥(ColumnL2 V)) (hbes : ∀ (h : ℤ) (y : ↥(ColumnL2 V)), ∑ p ∈ Finset.range (P + 1), ‖(Ah (p + 1) h - Ah p h) y‖ ^ 2 ≤ ‖y‖ ^ 2) (hcomm : ∀ (n : ℕ) (h : ℤ) (J : ℤ × ℤ), J.1 ≤ h → J.1 ≤ A.R.1 + ↑A.treeDepth → columnL2Restriction (dyadicGridCell A.G J.1 J.2) ⋯ ∘SL Ah n h = Ah n h ∘SL columnL2Restriction (dyadicGridCell A.G J.1 J.2) ⋯) {Cj : ℝ} (hCj : 0 ≤ Cj) (hJ : ∀ (n : ℕ) {ι : Type} [inst : Fintype ι] (r t : ι → ℕ), (∀ (i : ι), r i ≤ t i) → (∀ (i i' : ι), i ≠ i' → Disjoint (Finset.Ioc (r i) (t i)) (Finset.Ioc (r i') (t i'))) → ∀ (Ec : ι → Finset (ℤ × ℤ)), (∀ (i : ι), ∀ J ∈ Ec i, J ∈ A.cells) → ∀ (x : ↥(ColumnL2 V)), ∑ i : ι, ‖(columnL2Restriction (⋃ J ∈ Ec i, dyadicGridCell A.G J.1 J.2) ⋯) ((Ah n (A.R.1 + ↑(t i)) - Ah n (A.R.1 + ↑(r i))) x)‖ ^ 2 ≤ Cj * ‖x‖ ^ 2) (Wg : ↥(ColumnL2 V)) (Sa : ℤ → ↥(ColumnL2 V)) (hSa : ∀ (h : ℤ), Sa h = Zg h - Zg (A.R.1 + ↑(K * β)) + Wg) : ∑ q ∈ Finset.image (fun (I : ℤ × ℤ) => off I / 2 ^ (↑k + 1)) ({I ∈ Ug | posAct N k (off I)}), ∑ p ∈ Finset.range (P + 1), ‖gluedStack A.G ({I ∈ Ug | posAct N k (off I)}) (fun (I : ℤ × ℤ) => off I / 2 ^ (↑k + 1)) (fun (q : ℕ) => posVal (fun (n : ℕ) => (Ah (p + 1) (A.R.1 + ↑(K * β + n)) - Ah p (A.R.1 + ↑(K * β + n))) (Sa (A.R.1 + ↑(K * β + n)))) N k q) q‖ ^ 2 ≤ 2 * ∑ q ∈ Finset.image (fun (I : ℤ × ℤ) => off I / 2 ^ (↑k + 1)) ({I ∈ Ug | posAct N k (off I)}), ‖(columnL2Restriction (⋃ J ∈ A.posEc ({I ∈ Ug | posAct N k (off I)}) off (↑k) (K * β) q, dyadicGridCell A.G J.1 J.2) ⋯) (Zg (A.R.1 + ↑(K * β + (q * 2 ^ (↑k + 1) + 2 ^ ↑k))) - Zg (A.R.1 + ↑(K * β + q * 2 ^ (↑k + 1))))‖ ^ 2 + 16 * (↑P + 2) * (Cj * ‖(columnL2Restriction (⋃ J ∈ Finset.image (fun (I : ℤ × ℤ) => ancAt A.G I (A.R.1 + ↑(K * β))) ({I ∈ Ug | posAct N k (off I)}), dyadicGridCell A.G J.1 J.2) ⋯) Wg‖ ^ 2) + 16 * (↑P + 2) * (↑N * (Cj * ∑ k' : Fin N, ∑ q' ∈ Finset.image (fun (J : ℤ × ℤ) => off J / 2 ^ (↑k' + 1)) ({J ∈ A.posLeft ({I ∈ Ug | posAct N k (off I)}) off (↑k) (K * β) | posAct N k'.castSucc (off J)}), ‖(columnL2Restriction (⋃ J ∈ A.posEc ({J ∈ A.posLeft ({I ∈ Ug | posAct N k (off I)}) off (↑k) (K * β) | posAct N k'.castSucc (off J)}) off (↑k') (K * β) q', dyadicGridCell A.G J.1 J.2) ⋯) (Zg (A.R.1 + ↑(K * β + (q' * 2 ^ (↑k' + 1) + 2 ^ ↑k'))) - Zg (A.R.1 + ↑(K * β + q' * 2 ^ (↑k' + 1))))‖ ^ 2))

band_block for the uses of one group in one block, with the ancestor unions of the positions and the inner positions of the pseudo-uses posLeft.

theorem TrilinearHT.Auto.ActiveSetup.bandStack_energy {κ' : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ' c₀) (hanc : A.AncClosed) {γ : Type u_1} {V : Type u_2} [Fintype V] (Gs : Finset γ) (Z : γ → ℤ → ↥(ColumnL2 V)) (ok : γ → ℤ × ℤ → Prop) {B : ℝ} (hcap : A.VarCap Gs Z ok B) {K N : ℕ} (hKN : K ≤ 2 ^ N) (k : Fin (N + 1)) (hk : ↑k ≠ N) (Bs : Finset ℕ) (U : γ → ℕ → Finset (ℤ × ℤ)) (off : ℤ × ℤ → ℕ) (hoff : ∀ (J : ℤ × ℤ) (β m : ℕ), m < K → J.1 = A.R.1 + ↑(K * β + m) → off J = m) (hU : ∀ (g : γ) (β : ℕ), ∀ I ∈ U g β, I ∈ A.cells ∧ I.1 = A.R.1 + ↑(K * β + off I) ∧ off I < K) (hok : ∀ g ∈ Gs, ∀ (β : ℕ), ∀ I ∈ U g β, ∀ J ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G J.1 J.2 → ok g J) {P : ℕ} (Ah : γ → ℕ → ℤ → ↥(ColumnL2 V) →L[ℂ] ↥(ColumnL2 V)) (hbes : ∀ (g : γ) (h : ℤ) (y : ↥(ColumnL2 V)), ∑ p ∈ Finset.range (P + 1), ‖(Ah g (p + 1) h - Ah g p h) y‖ ^ 2 ≤ ‖y‖ ^ 2) (hcomm : ∀ (g : γ) (n : ℕ) (h : ℤ) (J : ℤ × ℤ), J.1 ≤ h → J.1 ≤ A.R.1 + ↑A.treeDepth → columnL2Restriction (dyadicGridCell A.G J.1 J.2) ⋯ ∘SL Ah g n h = Ah g n h ∘SL columnL2Restriction (dyadicGridCell A.G J.1 J.2) ⋯) {Cj : ℝ} (hCj : 0 ≤ Cj) (hJ : ∀ g ∈ Gs, ∀ (n : ℕ) {ι : Type} [inst : Fintype ι] (r t : ι → ℕ), (∀ (i : ι), r i ≤ t i) → (∀ (i i' : ι), i ≠ i' → Disjoint (Finset.Ioc (r i) (t i)) (Finset.Ioc (r i') (t i'))) → ∀ (Ec : ι → Finset (ℤ × ℤ)), (∀ (i : ι), ∀ J ∈ Ec i, J ∈ A.cells) → ∀ (x : ↥(ColumnL2 V)), ∑ i : ι, ‖(columnL2Restriction (⋃ J ∈ Ec i, dyadicGridCell A.G J.1 J.2) ⋯) ((Ah g n (A.R.1 + ↑(t i)) - Ah g n (A.R.1 + ↑(r i))) x)‖ ^ 2 ≤ Cj * ‖x‖ ^ 2) (W : γ → ℕ → ↥(ColumnL2 V)) {EW : ℝ} (hEW : ∑ g ∈ Gs, ∑ β ∈ Bs, ‖(columnL2Restriction (⋃ J ∈ Finset.image (fun (I : ℤ × ℤ) => ancAt A.G I (A.R.1 + ↑(K * β))) ({I ∈ U g β | posAct N k (off I)}), dyadicGridCell A.G J.1 J.2) ⋯) (W g β)‖ ^ 2 ≤ EW) (Sa : γ → ℕ → ℤ → ↥(ColumnL2 V)) (hSa : ∀ (g : γ) (β : ℕ) (h : ℤ), Sa g β h = Z g h - Z g (A.R.1 + ↑(K * β)) + W g β) : ∑ g ∈ Gs, ∑ β ∈ Bs, ∑ q ∈ Finset.image (fun (I : ℤ × ℤ) => off I / 2 ^ (↑k + 1)) ({I ∈ U g β | posAct N k (off I)}), ∑ p ∈ Finset.range (P + 1), ‖gluedStack A.G ({I ∈ U g β | posAct N k (off I)}) (fun (I : ℤ × ℤ) => off I / 2 ^ (↑k + 1)) (fun (q : ℕ) => posVal (fun (n : ℕ) => (Ah g (p + 1) (A.R.1 + ↑(K * β + n)) - Ah g p (A.R.1 + ↑(K * β + n))) (Sa g β (A.R.1 + ↑(K * β + n)))) N k q) q‖ ^ 2 ≤ 2 * B + 16 * (↑P + 2) * (Cj * EW) + 16 * (↑P + 2) * (↑N * (Cj * (↑N * B)))

Blueprint lines 2408-2423 (eq:stack-energy for the banded transferred side, one level k < N): for a family Z_g of variation capacity B, a side S = Z_h - Z_b + W in each block, and pad families A_n (n ≤ P + 1) with Bessel bands, local at their depths and with fixed-input jumps bounded by C_j, the glued position stacks of the bands (A_{p+1} - A_p) S over the uses of all groups and blocks have total square at most 2 B + 16 (P + 2) C_j E_W + 16 (P + 2) N C_j (N B), with E_W the energy of the block inputs W restricted to the block-start ancestors of the uses.

theorem TrilinearHT.Auto.ActiveSetup.baseStack_energy {κ' : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ' c₀) {γ : Type u_1} {V : Type u_2} [Fintype V] (Gs : Finset γ) {K N : ℕ} (hKN : K ≤ 2 ^ N) (Bs : Finset ℕ) (U : γ → ℕ → Finset (ℤ × ℤ)) (off : ℤ × ℤ → ℕ) (hU : ∀ (g : γ) (β : ℕ), ∀ I ∈ U g β, I ∈ A.cells ∧ I.1 = A.R.1 + ↑(K * β + off I) ∧ off I < K) {P : ℕ} (Ah : γ → ℕ → ℤ → ↥(ColumnL2 V) →L[ℂ] ↥(ColumnL2 V)) (hbes : ∀ (g : γ) (h : ℤ) (y : ↥(ColumnL2 V)), ∑ p ∈ Finset.range (P + 1), ‖(Ah g (p + 1) h - Ah g p h) y‖ ^ 2 ≤ ‖y‖ ^ 2) (hcomm : ∀ (g : γ) (n : ℕ) (h : ℤ) (J : ℤ × ℤ), J.1 ≤ h → J.1 ≤ A.R.1 + ↑A.treeDepth → columnL2Restriction (dyadicGridCell A.G J.1 J.2) ⋯ ∘SL Ah g n h = Ah g n h ∘SL columnL2Restriction (dyadicGridCell A.G J.1 J.2) ⋯) (W : γ → ℕ → ↥(ColumnL2 V)) {EW : ℝ} (hEW : ∑ g ∈ Gs, ∑ β ∈ Bs, ‖(columnL2Restriction (⋃ J ∈ Finset.image (fun (I : ℤ × ℤ) => ancAt A.G I (A.R.1 + ↑(K * β))) (U g β), dyadicGridCell A.G J.1 J.2) ⋯) (W g β)‖ ^ 2 ≤ EW) (Sa : γ → ℕ → ℤ → ↥(ColumnL2 V)) (hSa : ∀ (g : γ) (β : ℕ), Sa g β (A.R.1 + ↑(K * β)) = W g β) : ∑ g ∈ Gs, ∑ β ∈ Bs, ∑ q ∈ Finset.image (fun (I : ℤ × ℤ) => off I / 2 ^ (N + 1)) ({I ∈ U g β | posAct N (Fin.last N) (off I)}), ∑ p ∈ Finset.range (P + 1), ‖gluedStack A.G ({I ∈ U g β | posAct N (Fin.last N) (off I)}) (fun (I : ℤ × ℤ) => off I / 2 ^ (N + 1)) (fun (q : ℕ) => posVal (fun (n : ℕ) => (Ah g (p + 1) (A.R.1 + ↑(K * β + n)) - Ah g p (A.R.1 + ↑(K * β + n))) (Sa g β (A.R.1 + ↑(K * β + n)))) N (Fin.last N) q) q‖ ^ 2 ≤ EW

Blueprint lines 2408-2409 and 2420 (the base terms of eq:stack-energy): the glued base stacks (level N) of the bands (A_{p+1} - A_p) S at the block starts, where S_b = W, have total square at most the energy E_W of the block inputs restricted to the block-start ancestors of the uses (Bessel bands, local pads).

Depth stacks of a basic U side (blueprint lines 2407-2408)

noncomputable def TrilinearHT.Auto.depthStack (G : RealDyadicGrid) {V : Type u_1} [Fintype V] (U : Finset (ℤ × ℤ)) (sel : ℤ × ℤ → ℕ) (v : ℤ × ℤ → ↥(ColumnL2 V)) (m : ℕ) : ↥(ColumnL2 V)

Blueprint line 2407 ("for a basic U side use each depth directly as a position"): the depth stack of local values v_I on the cells of U of selection m: the sum of their restrictions to the cells.

Equations

• TrilinearHT.Auto.depthStack G U sel v m = ∑ J ∈ U with sel J = m, (TrilinearHT.Auto.columnL2Restriction (TrilinearHT.Auto.dyadicGridCell G J.1 J.2) ⋯) (v J)

theorem TrilinearHT.Auto.helpPre_append {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (P : ℕ) (l : List (TransferStep E)) (st : TransferStep E) (x : E) : helpPre P (l ++ [st]) x = (filterAvg P st.2.1) (helpPre P l x)

Global sides of a leaf (blueprint lines 2161-2162, 2414-2420)

theorem TrilinearHT.Auto.fin4_last (a b c d l : Fin 4) : a ≠ b → a ≠ c → a ≠ d → b ≠ c → b ≠ d → c ≠ d → l ≠ a → l ≠ c → l ≠ d → l = b

In four slots, a slot distinct from three of four distinct slots is the fourth.

theorem TrilinearHT.Auto.ActiveSetup.bandStack_all {κ' : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ' c₀) (hanc : A.AncClosed) {γ : Type u_1} {V : Type u_2} [Fintype V] (Gs : Finset γ) (Z : γ → ℤ → ↥(ColumnL2 V)) (ok : γ → ℤ × ℤ → Prop) {B : ℝ} (hcap : A.VarCap Gs Z ok B) {K N : ℕ} (hKN : K ≤ 2 ^ N) (Bs : Finset ℕ) (U : γ → ℕ → Finset (ℤ × ℤ)) (off : ℤ × ℤ → ℕ) (hoff : ∀ (J : ℤ × ℤ) (β m : ℕ), m < K → J.1 = A.R.1 + ↑(K * β + m) → off J = m) (hU : ∀ (g : γ) (β : ℕ), ∀ I ∈ U g β, I ∈ A.cells ∧ I.1 = A.R.1 + ↑(K * β + off I) ∧ off I < K) (hok : ∀ g ∈ Gs, ∀ (β : ℕ), ∀ I ∈ U g β, ∀ J ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G J.1 J.2 → ok g J) {P : ℕ} (Ah : γ → ℕ → ℤ → ↥(ColumnL2 V) →L[ℂ] ↥(ColumnL2 V)) (hbes : ∀ (g : γ) (h : ℤ) (y : ↥(ColumnL2 V)), ∑ p ∈ Finset.range (P + 1), ‖(Ah g (p + 1) h - Ah g p h) y‖ ^ 2 ≤ ‖y‖ ^ 2) (hcomm : ∀ (g : γ) (n : ℕ) (h : ℤ) (J : ℤ × ℤ), J.1 ≤ h → J.1 ≤ A.R.1 + ↑A.treeDepth → columnL2Restriction (dyadicGridCell A.G J.1 J.2) ⋯ ∘SL Ah g n h = Ah g n h ∘SL columnL2Restriction (dyadicGridCell A.G J.1 J.2) ⋯) {Cj : ℝ} (hCj : 0 ≤ Cj) (hJ : ∀ g ∈ Gs, ∀ (n : ℕ) {ι : Type} [inst : Fintype ι] (r t : ι → ℕ), (∀ (i : ι), r i ≤ t i) → (∀ (i i' : ι), i ≠ i' → Disjoint (Finset.Ioc (r i) (t i)) (Finset.Ioc (r i') (t i'))) → ∀ (Ec : ι → Finset (ℤ × ℤ)), (∀ (i : ι), ∀ J ∈ Ec i, J ∈ A.cells) → ∀ (x : ↥(ColumnL2 V)), ∑ i : ι, ‖(columnL2Restriction (⋃ J ∈ Ec i, dyadicGridCell A.G J.1 J.2) ⋯) ((Ah g n (A.R.1 + ↑(t i)) - Ah g n (A.R.1 + ↑(r i))) x)‖ ^ 2 ≤ Cj * ‖x‖ ^ 2) (W : γ → ℕ → ↥(ColumnL2 V)) {EW : ℝ} (hEW : ∑ g ∈ Gs, ∑ β ∈ Bs, ‖(columnL2Restriction (⋃ J ∈ Finset.image (fun (I : ℤ × ℤ) => ancAt A.G I (A.R.1 + ↑(K * β))) (U g β), dyadicGridCell A.G J.1 J.2) ⋯) (W g β)‖ ^ 2 ≤ EW) (Sa : γ → ℕ → ℤ → ↥(ColumnL2 V)) (hSa : ∀ (g : γ) (β : ℕ) (h : ℤ), Sa g β h = Z g h - Z g (A.R.1 + ↑(K * β)) + W g β) : ∑ k : Fin (N + 1), ∑ g ∈ Gs, ∑ β ∈ Bs, ∑ q ∈ Finset.image (fun (I : ℤ × ℤ) => off I / 2 ^ (↑k + 1)) ({I ∈ U g β | posAct N k (off I)}), ∑ p ∈ Finset.range (P + 1), ‖gluedStack A.G ({I ∈ U g β | posAct N k (off I)}) (fun (I : ℤ × ℤ) => off I / 2 ^ (↑k + 1)) (fun (q : ℕ) => posVal (fun (n : ℕ) => (Ah g (p + 1) (A.R.1 + ↑(K * β + n)) - Ah g p (A.R.1 + ↑(K * β + n))) (Sa g β (A.R.1 + ↑(K * β + n)))) N k q) q‖ ^ 2 ≤ ↑N * (2 * B + 16 * (↑P + 2) * (Cj * EW) + 16 * (↑P + 2) * (↑N * (Cj * (↑N * B)))) + EW

Blueprint eq:stack-energy for the banded side of one transfer step over all levels: the bandStack_energy of the levels k < N plus the baseStack_energy of the base level.

theorem TrilinearHT.Auto.ActiveSetup.posStack_all {κ' : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ' c₀) (hanc : A.AncClosed) {γ : Type u_1} {V : Type u_2} [Fintype V] (Gs : Finset γ) (Z : γ → ℤ → ↥(ColumnL2 V)) (ok : γ → ℤ × ℤ → Prop) {B : ℝ} (hcap : A.VarCap Gs Z ok B) {K N : ℕ} (hKN : K ≤ 2 ^ N) (Bs : Finset ℕ) (U : γ → ℕ → Finset (ℤ × ℤ)) (off : ℤ × ℤ → ℕ) (hU : ∀ (g : γ) (β : ℕ), ∀ I ∈ U g β, I ∈ A.cells ∧ I.1 = A.R.1 + ↑(K * β + off I) ∧ off I < K) (hok : ∀ g ∈ Gs, ∀ (β : ℕ), ∀ I ∈ U g β, ∀ J ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G J.1 J.2 → ok g J) (Sb : γ → ℕ → ℤ → ↥(ColumnL2 V)) (hSb : ∀ (g : γ) (β : ℕ) (h h' : ℤ), Sb g β h - Sb g β h' = Z g h - Z g h') {EW : ℝ} (hEW : ∑ g ∈ Gs, ∑ β ∈ Bs, ‖(columnL2Restriction (⋃ J ∈ Finset.image (fun (I : ℤ × ℤ) => ancAt A.G I (A.R.1 + ↑(K * β))) (U g β), dyadicGridCell A.G J.1 J.2) ⋯) (Sb g β (A.R.1 + ↑(K * β)))‖ ^ 2 ≤ EW) : ∑ k : Fin (N + 1), ∑ g ∈ Gs, ∑ β ∈ Bs, ∑ q ∈ Finset.image (fun (I : ℤ × ℤ) => off I / 2 ^ (↑k + 1)) ({I ∈ U g β | posAct N k (off I)}), ‖gluedStack A.G ({I ∈ U g β | posAct N k (off I)}) (fun (I : ℤ × ℤ) => off I / 2 ^ (↑k + 1)) (fun (q : ℕ) => posVal (fun (n : ℕ) => Sb g β (A.R.1 + ↑(K * β + n))) N k q) q‖ ^ 2 ≤ ↑N * B + EW

Blueprint eq:stack-energy for the untouched side over all levels: the position levels by posStack_energy and the base level by the block-start energy.

theorem TrilinearHT.Auto.path_cap_integral (Gd : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (root : ℤ × ℤ) (hroot : ∀ I ∈ S, dyadicGridCell Gd I.1 I.2 ⊆ dyadicGridCell Gd root.1 root.2) (f : ℤ × ℤ → ℝ) {T : ℝ} (hT : ∀ (x : ℝ), ∑ I ∈ S with x ∈ dyadicGridCell Gd I.1 I.2, f I ≤ T) : ∑ I ∈ S, dyadicGridLength Gd I.1 * f I ≤ T * dyadicGridLength Gd root.1

Integrating a pointwise path cap: if the path sums of f are at most T everywhere, the length-weighted sum of f over cells inside a root is at most T times the root length.

theorem TrilinearHT.Auto.list_map_sum_range {α : Type u_1} (L : List α) (d : α) (f : α → ℝ) : (List.map f L).sum = ∑ i ∈ Finset.range L.length, f (L.getD i d)

A list sum of a map as a sum over the index range with getD.

theorem TrilinearHT.Auto.sq_sum_le_of_card {ι : Type u_1} (s : Finset ι) (f : ι → ℝ) {n : ℝ} (hs : ↑s.card ≤ n) : (∑ i ∈ s, f i) ^ 2 ≤ n * ∑ i ∈ s, f i ^ 2

Cauchy-Schwarz for a sum over a finset of size at most n.

theorem TrilinearHT.Auto.add_sq_le_two (a b : ℝ) : (a + b) ^ 2 ≤ 2 * a ^ 2 + 2 * b ^ 2

(a + b)² ≤ 2 a² + 2 b².

theorem TrilinearHT.Auto.sq_sum2_le (s : Finset ℕ) (t : ℕ → Finset ℕ) (f : ℕ → ℕ → ℝ) {n m : ℝ} (hs : ↑s.card ≤ n) (ht : ∀ (i : ℕ), ↑(t i).card ≤ m) (hn : 0 ≤ n) : (∑ i ∈ s, ∑ j ∈ t i, f i j) ^ 2 ≤ n * m * ∑ i ∈ s, ∑ j ∈ t i, f i j ^ 2

Cauchy-Schwarz for a double sum over ranges of sizes at most n and m.

theorem TrilinearHT.Auto.pair_sq_le {L a Aa D : ℝ} (J O : Finset ℕ) (y Bt : ℕ → ℕ → ℝ) {Jm : ℕ} (hL : 0 < L) (hJ : J.card ≤ Jm) (hO : O.card = 5) (ha : L * a ^ 2 ≤ Aa) (hy : ∀ (j o : ℕ), L * y j o ^ 2 ≤ D * Bt j o) (hD : 0 ≤ D) (hAa : 0 ≤ Aa) (hBt : ∀ (j o : ℕ), 0 ≤ Bt j o) : L * (a + ∑ j ∈ J, ∑ o ∈ O, y j o) ^ 2 ≤ 2 * (1 + 5 * ↑Jm) * (Aa + D * ∑ j ∈ J, ∑ o ∈ O, Bt j o)

The per-pair bound of the third strong factor: L (a + Σ_{j,o} y)² ≤ 2 (1 + 5 J) (A + D Σ B).

theorem TrilinearHT.Auto.pairs_sq_le {L Lp K A D : ℝ} (s : Finset ℕ) (t : ℕ → Finset ℕ) (X B : ℕ → ℕ → ℝ) (hL : 0 ≤ L) (hK : 0 ≤ K) (hA : 0 ≤ A) (hD : 0 ≤ D) (hLp : 0 ≤ Lp) (hs : ↑s.card ≤ Lp) (ht : ∀ (i : ℕ), ↑(t i).card ≤ Lp) (hX : ∀ i ∈ s, ∀ j ∈ t i, L * X i j ^ 2 ≤ K * (A + D * B i j)) (hB : ∀ (i j : ℕ), 0 ≤ B i j) : L * (∑ i ∈ s, ∑ j ∈ t i, X i j) ^ 2 ≤ Lp ^ 2 * K * (Lp ^ 2 * A + D * ∑ i ∈ s, ∑ j ∈ t i, B i j)

Assembling the per-pair bounds over the pairs of positive chains by Cauchy-Schwarz.

theorem TrilinearHT.Auto.sq_sum_fin4_4 (f : Fin 4 → Fin 4 → Fin 4 → Fin 4 → ℝ) : (∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, f a b c d) ^ 2 ≤ 256 * ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, f a b c d ^ 2

Cauchy-Schwarz over four slot indices.

theorem TrilinearHT.Auto.disjoint_subcells_length_le (Gd : RealDyadicGrid) (C : Finset (ℤ × ℤ)) (J : ℤ × ℤ) (hC : (↑C).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell Gd c.1 c.2) (hsub : ∀ c ∈ C, dyadicGridCell Gd c.1 c.2 ⊆ dyadicGridCell Gd J.1 J.2) : ∑ c ∈ C, dyadicGridLength Gd c.1 ≤ dyadicGridLength Gd J.1

Pairwise disjoint cells inside a cell have total length at most its length.

theorem TrilinearHT.Auto.depth_window_length_le (Gd : RealDyadicGrid) (X : Finset (ℤ × ℤ)) (J : ℤ × ℤ) (K : ℕ) (hsub : ∀ I ∈ X, dyadicGridCell Gd I.1 I.2 ⊆ dyadicGridCell Gd J.1 J.2) (hdep : ∀ I ∈ X, J.1 ≤ I.1 ∧ I.1 < J.1 + ↑K) : ∑ I ∈ X, dyadicGridLength Gd I.1 ≤ ↑K * dyadicGridLength Gd J.1

Cells of a finite family inside a cell J, at depths of a window of K depths starting at J, have total length at most K |J|.

theorem TrilinearHT.Auto.block_ioc_disjoint {K n : ℕ} (hn : n < K) {β β' : ℕ} (hne : β ≠ β') : Disjoint (Finset.Ioc (K * β) (K * β + n)) (Finset.Ioc (K * β') (K * β' + n))

Distinct blocks give disjoint depth intervals of a fixed offset n < K.

Global helper projections in the main column space (blueprint lines 2393-2420)

theorem TrilinearHT.Auto.colRelabel_physEmbed {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] (f : V → W) {U : Type u_3} [Fintype U] (x : ↥(ColumnL2 U)) : (colRelabel f) ((physEmbed U V) x) = (physEmbed U W) x

Relabeling a physical vector keeps it physical.

theorem TrilinearHT.Auto.isStarProjection_conj {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] {f : V → W} (hf : Function.Injective f) {T : ↥(ColumnL2 V) →L[ℂ] ↥(ColumnL2 V)} (hT : IsStarProjection T) : IsStarProjection (colRelabel f ∘SL T ∘SL ContinuousLinearMap.adjoint (colRelabel f))

A conjugated projection by an isometric relabeling is a projection.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gProjC {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (M : InheritedColumnMask (bf.mainTree fp.Mc s mb)) (h : ℤ) : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)) →L[ℂ] ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))

A global depth projection of the main base of the catalog s with an inherited mask at the depth h, conjugated to the main column space by the relabeling of the relevant labels.

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gProjC_isStarProjection {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (M : InheritedColumnMask (bf.mainTree fp.Mc s mb)) (h : ℤ) : IsStarProjection (fp.gProjC s mb M h)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gProjC_comp {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (M M' : InheritedColumnMask (bf.mainTree fp.Mc s mb)) (h h' : ℤ) : fp.gProjC s mb M h ∘SL fp.gProjC s mb M' h' = colRelabel (bf.rv fp.Mc s) ∘SL (((bf.mainBase fp.Mc s mb).withMask M).proj h ∘SL ((bf.mainBase fp.Mc s mb).withMask M').proj h') ∘SL ContinuousLinearMap.adjoint (colRelabel (bf.rv fp.Mc s))

Conjugation preserves the composition of global projections.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gProjC_mask_nested {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) {M M' : InheritedColumnMask (bf.mainTree fp.Mc s mb)} (hM : ∀ c ∈ (bf.mainTree fp.Mc s mb).cells, M.labels c ⊆ M'.labels c) (h : ℤ) : fp.gProjC s mb M h ∘SL fp.gProjC s mb M' h = fp.gProjC s mb M h

Global projections with nested masks at one depth are nested.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gProjC_commute {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (M : InheritedColumnMask (bf.mainTree fp.Mc s mb)) (h : ℤ) {Q : ℤ × ℤ} (hQ : Q.1 ≤ (bf.mainBase fp.Mc s mb).depth h) : columnL2Restriction (dyadicGridCell A.G Q.1 Q.2) ⋯ ∘SL fp.gProjC s mb M h = fp.gProjC s mb M h ∘SL columnL2Restriction (dyadicGridCell A.G Q.1 Q.2) ⋯

The global projections commute with the restriction to every cell of depth at most the clamped depth.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.physMain_mem_range {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (s : List (CatCol bf.Vtx)) {U : Type u_1} [Fintype U] (x : ↥(ColumnL2 U)) : (fp.physMain U) x ∈ (↑(colRelabel (bf.rv fp.Mc s))).range

Physical vectors lie in the range of the relabeling.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.mainMaskT_labels_mono {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (l : Fin 4) (Mc : ℕ) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (r : ℕ) {M M' : ℤ × ℤ → bf.Vtx → Prop} (hM : ∀ c ∈ A.cells, ∀ d ∈ A.cells, dyadicGridCell A.G c.1 c.2 ⊆ dyadicGridCell A.G d.1 d.2 → ∀ (x : bf.Vtx), M d x → M c x) (hM' : ∀ c ∈ A.cells, ∀ d ∈ A.cells, dyadicGridCell A.G c.1 c.2 ⊆ dyadicGridCell A.G d.1 d.2 → ∀ (x : bf.Vtx), M' d x → M' c x) (hMM : ∀ (c : ℤ × ℤ) (x : bf.Vtx), M c x → M' c x) (c : ℤ × ℤ) : c ∈ (bf.mainTree Mc s mb).cells → (bf.mainMaskT l Mc s mb r M hM).labels c ⊆ (bf.mainMaskT l Mc s mb r M' hM').labels c

The inherited main masks are monotone in the vertex masks.

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.slotDescM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (j : ℕ) (t : List ℕ) : List (ℕ × Option ℕ)

The cell-independent descriptors of the positive filters of a slot along a positive chain: the ball filter of the level j, then the cumulative layers, each with its rank.

Equations

• fp.slotDescM j t = (fp.brank j, none) :: List.map (fun (m : ℕ) => (fp.crank m, some m)) t

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.stepMaskM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (G : bf.Grp) (j : ℕ) : Option ℕ → Fin fp.P → ℤ × ℤ → bf.Vtx → Prop

The pad mask of a descriptor at a cell: the ball mask of the group or the cumulative mask.

Equations

• fp.stepMaskM G j none x✝¹ x✝ = fp.bmask x✝ G j (↑x✝¹ + 1)
• fp.stepMaskM G j (some m) x✝¹ x✝ = fp.cmask x✝ m (↑x✝¹ + 1)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.stepMaskM_mono {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (G : bf.Grp) (j : ℕ) (o : Option ℕ) (p : Fin fp.P) (c : ℤ × ℤ) : c ∈ A.cells → ∀ d ∈ A.cells, dyadicGridCell A.G c.1 c.2 ⊆ dyadicGridCell A.G d.1 d.2 → ∀ (x : bf.Vtx), fp.stepMaskM G j o p d x → fp.stepMaskM G j o p c x

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.stepMaskM_pad_mono {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (G : bf.Grp) (j : ℕ) (o : Option ℕ) {p p' : Fin fp.P} (hpp : p ≤ p') (I : ℤ × ℤ) (x : bf.Vtx) : fp.stepMaskM G j o p I x → fp.stepMaskM G j o p' I x

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.slotFiltM_eq {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (G : bf.Grp) (j : ℕ) (I : ℤ × ℤ) (t : List ℕ) : fp.slotFiltM G j I t = List.map (fun (e : ℕ × Option ℕ) => (e.1, fun (p : Fin fp.P) => fp.stepMaskM G j e.2 p I)) (fp.slotDescM j t)

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.mergeDescM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (jc jd : ℕ) (t t' : List ℕ) : List (Bool × ℕ × Option ℕ)

The merged descriptors of a pair of positive chains of the complement slots.

Equations

• fp.mergeDescM jc jd t t' = TrilinearHT.Auto.rankMerge Prod.fst (fp.slotDescM jc t) (fp.slotDescM jd t')

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.rankMerge_slotFiltM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (G : bf.Grp) (jc jd : ℕ) (I : ℤ × ℤ) (t t' : List ℕ) : rankMerge Prod.fst (fp.slotFiltM G jc I t) (fp.slotFiltM G jd I t') = List.map (fun (e : Bool × ℕ × Option ℕ) => (e.1, e.2.1, fun (p : Fin fp.P) => fp.stepMaskM G (if e.1 = true then jc else jd) e.2.2 p I)) (fp.mergeDescM jc jd t t')

The rank merge of the slot filters of a cell is the list of the merged descriptors with their cell masks.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.hMaskM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (a : Fin 4) (sA : List (CatCol bf.Vtx)) (mbA : bf.MainBudget sA) (G : bf.Grp) (jc jd : ℕ) (e : Bool × ℕ × Option ℕ) (p : Fin fp.P) : InheritedColumnMask (bf.mainTree fp.Mc sA mbA)

The inherited helper mask (rank L + 5) of a descriptor at a pad, on the main tree of the side slot a with its catalog s_a.

Equations

• fp.hMaskM a sA mbA G jc jd e p = bf.mainMaskT a fp.Mc sA mbA (fp.Lc + 5) (fun (c : ℤ × ℤ) => fp.stepMaskM G (if e.1 = true then jc else jd) e.2.2 p c) ⋯

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.lsOf (n : ℕ) : List (ℕ × Bool)

The layers (0, false), …, (n - 1, false).

Equations

• TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.lsOf n = List.map (fun (k : ℕ) => (k, false)) (List.range n)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.lsOf_length (n : ℕ) : (lsOf n).length = n

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.lsOf_succ (n : ℕ) : lsOf (n + 1) = lsOf n ++ [(n, false)]

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gPreR {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (a : Fin 4) (sA : List (CatCol bf.Vtx)) (mbA : bf.MainBudget sA) (G : bf.Grp) (jc jd : ℕ) (D : List (Bool × ℕ × Option ℕ)) (h : ℤ) : ↥(ColumnL2 (bf.RLab fp.Mc sA)) →L[ℂ] ↥(ColumnL2 (bf.RLab fp.Mc sA))

The global helper prefix of the descriptors D at the depth h on the relevant labels of the side slot: the averaged global helper projections of the steps, in step order.

Equations

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

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gBandR {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (a : Fin 4) (sA : List (CatCol bf.Vtx)) (mbA : bf.MainBudget sA) (G : bf.Grp) (jc jd : ℕ) (e : Bool × ℕ × Option ℕ) (D : List (Bool × ℕ × Option ℕ)) (n : ℕ) (h : ℤ) : ↥(ColumnL2 (bf.RLab fp.Mc sA)) →L[ℂ] ↥(ColumnL2 (bf.RLab fp.Mc sA))

The global band pad family of the step e after the prefix D, on the relevant labels.

Equations

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

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gBandC {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (a : Fin 4) (sA : List (CatCol bf.Vtx)) (mbA : bf.MainBudget sA) (G : bf.Grp) (jc jd : ℕ) (e : Bool × ℕ × Option ℕ) (D : List (Bool × ℕ × Option ℕ)) (n : ℕ) (h : ℤ) : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)) →L[ℂ] ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))

The global band pad family of a step after its prefix, conjugated to the main column space (the operators A_{p} of the banded side, blueprint line 2411).

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gBandC_bessel {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (a : Fin 4) (sA : List (CatCol bf.Vtx)) (mbA : bf.MainBudget sA) (G : bf.Grp) (jc jd : ℕ) (e : Bool × ℕ × Option ℕ) (D : List (Bool × ℕ × Option ℕ)) (h : ℤ) (y : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : ∑ p ∈ Finset.range (fp.P + 1), ‖(fp.gBandC a sA mbA G jc jd e D (p + 1) h - fp.gBandC a sA mbA G jc jd e D p h) y‖ ^ 2 ≤ ‖y‖ ^ 2

Blueprint lines 2411-2413 ("on the banded side pay at most P + 1 indices"): the bands of the global pad family after the prefix are Bessel.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gBandC_commute {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (a : Fin 4) (sA : List (CatCol bf.Vtx)) (mbA : bf.MainBudget sA) (G : bf.Grp) (jc jd : ℕ) (e : Bool × ℕ × Option ℕ) (D : List (Bool × ℕ × Option ℕ)) (n : ℕ) (h : ℤ) {Q : ℤ × ℤ} (hQ : Q.1 ≤ (bf.mainBase fp.Mc sA mbA).depth h) : columnL2Restriction (dyadicGridCell A.G Q.1 Q.2) ⋯ ∘SL fp.gBandC a sA mbA G jc jd e D n h = fp.gBandC a sA mbA G jc jd e D n h ∘SL columnL2Restriction (dyadicGridCell A.G Q.1 Q.2) ⋯

The global band pad family commutes with the restriction to every cell of depth at most the clamped depth.

theorem TrilinearHT.Auto.layerOp_congr {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {C C' : ℕ → H →L[ℂ] H} (ls : List (ℕ × Bool)) : (∀ x ∈ ls, C x.1 = C' x.1) → layerOp C ls = layerOp C' ls

A layer product depends only on the layers used.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.mem_lsOf {n : ℕ} {x : ℕ × Bool} (hx : x ∈ lsOf n) : x.1 < n ∧ x.2 = false

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.bandJumpM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (n : ℕ) : ℝ

The jump constant of a helper product with one more layer.

Equations

• fp.bandJumpM s mb n = (↑n + 1) * ∑ m ∈ Finset.range (n + 1), TrilinearHT.Auto.compressionC (bf.mainTree fp.Mc s mb) m ^ 2

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.bandJumpM_nonneg {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (n : ℕ) : 0 ≤ fp.bandJumpM s mb n

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gBandC_jump {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (a : Fin 4) (sA : List (CatCol bf.Vtx)) (mbA : bf.MainBudget sA) (G : bf.Grp) (jc jd : ℕ) (e : Bool × ℕ × Option ℕ) (D : List (Bool × ℕ × Option ℕ)) (n : ℕ) {ι : Type u_1} [Fintype ι] (r t : ι → ℕ) (hrt : ∀ (i : ι), r i ≤ t i) (hdis : ∀ (i i' : ι), i ≠ i' → Disjoint (Finset.Ioc (r i) (t i)) (Finset.Ioc (r i') (t i'))) (E : ι → Set ℝ) (hE : ∀ (i : ι), MeasurableSet (E i)) (x : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : ∑ i : ι, ‖(columnL2Restriction (E i) ⋯) ((fp.gBandC a sA mbA G jc jd e D n (A.R.1 + ↑(t i)) - fp.gBandC a sA mbA G jc jd e D n (A.R.1 + ↑(r i))) x)‖ ^ 2 ≤ fp.bandJumpM sA mbA D.length * ‖x‖ ^ 2

Blueprint lines 2411-2413 (the outer bands of a fixed input under the subsequent product, lem:prefix): over disjoint depth intervals, the jumps of the global band pad family of a step after its prefix, on any restrictions, have total square at most (|D| + 1) Σ_{m ≤ |D|} C_m² times the square of the fixed input.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.varCap_basicOut {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (hT : ∀ e ∈ s, ∃ R ∈ residueBox (bf.vtag e.tag).dim 9, ∃ (γ : ℝ), e = templateCol (bf.vtag e.tag) l R γ e.birth e.rank e.tag) (htag : ∀ e ∈ s, bf.occAvail (↑e.tag.2) e.tag.1) (d : bf.Vtx) (mb : bf.MainBudget s) (hanc : A.AncClosed) (hne : A.cells.Nonempty) (Gs : Finset bf.Grp) (k j : ℕ) (hPH : fp.bbase j + fp.P ≤ fp.Hmax) (ls : List (ℕ × Bool)) {ra rb : ℝ} (hroot : ∀ I ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ Set.Icc ra rb) {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ ≤ 1) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ⁻¹) ^ A.Dg) ≤ fp.Hed) {N : ℕ} (hN : ∀ (y : ℝ), {q : ↥Gs × (bf.Lab ⊕ Fin fp.Mc) | ∃ I ∈ A.cells, (∃ (k' : ℕ), fp.Cert k' (↑q.1) I) ∧ ∃ (p : Fin fp.P), y ∈ dyadicGridCell A.G I.1 I.2 ∧ q.2 ∈ mainLabelsM A.G fp.Mc (bf.origCols l) s I (fp.brank j) (fp.bmask I (↑q.1) j (↑p + 1)) d}.card ≤ N) (hτN : τ * ↑N * A.colBudget ^ 2 ≤ 1) (c : ℕ) (hc : 1 ≤ c) {kk : ℝ} (hk : 1 ≤ kk) (hDm : Real.log (2 * mb.B) ≤ kk ^ c) (hDb : Real.log (2 * A.colBudget) ≤ kk ^ c) (hn : ↑ls.length ≤ ↑c * (Real.log kk + 1)) : A.VarCap Gs (fun (G : bf.Grp) (h : ℤ) => (fp.physMain (bf.Lab ⊕ Fin fp.Mc)) (fp.basicOut l s mb G j ls h)) (fun (G : bf.Grp) (J : ℤ × ℤ) => fp.Cert k G J) (Real.exp ((4096 * (↑c + 1) * (1024 * (↑c + 1) + ↑c + 7) + ↑c ^ 2 + 3) * (1 + Real.log (2 * kk)) ^ 2) * (4 * dyadicGridLength A.G A.R.1))

Blueprint lem:variation as a variation capacity (VarCap) of the physical global coarse outputs of a basic slot for a set of groups of one color: over any disjoint depth intervals and unions of certified active cells at the right endpoints, the restricted jumps have total square at most G₀ · 4 |R|.

The number of configurations (blueprint line 2419)