Section 14.3: Power costs and frozen complements

This file was automatically generated by Claude.

Formalization of blueprint Section 14, "The two-side estimate" (sec:sides), subsection 3, "Power costs and frozen complements" (lines 2372-2391) of blueprint/formalization_blueprint.tex.

Power costs, fixed stacks and the exported side estimate (blueprint lines 2372-2457)

theorem TrilinearHT.Auto.sum_rpow_le_sum_sq_rpow {ι : Type u_1} (s : Finset ι) (a : ι → ℝ) (ha : ∀ i ∈ s, 0 ≤ a i) {r : ℝ} (hr : 2 ≤ r) : ∑ i ∈ s, a i ^ r ≤ (∑ i ∈ s, a i ^ 2) ^ (r / 2)

ℓ^r ⊆ ℓ² for r ≥ 2: Σ a_i^r ≤ (Σ a_i²)^{r/2} for nonnegative a.

theorem TrilinearHT.Auto.three_sides_power {ι : Type u_1} (s : Finset ι) (a b c : ι → ℝ) (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) (hc : ∀ i ∈ s, 0 ≤ c i) {p : ℝ} (hp : 2 / 3 < p) : ∑ i ∈ s, (a i * b i * c i) ^ p ≤ (∑ i ∈ s, a i ^ 2) ^ (p / 2) * (∑ i ∈ s, b i ^ 2) ^ (p / 2) * (∑ i ∈ s, c i ^ 2) ^ (p / 2)

Blueprint eq:three-sides (line 2380): for 2/3 < p ≤ 1 and nonnegative group sizes, Σ_s (a_s b_s c_s)^p ≤ Π_{x = a,b,c} (Σ_s x_s²)^{p/2}.

noncomputable def TrilinearHT.Auto.patternCount (σ : Fin 4 → Fin 3) (j : Fin 3) : ℕ

The number of slots of a pattern carrying a given part.

Equations

• TrilinearHT.Auto.patternCount σ j = {l : Fin 4 | σ l = j}.card

Power costs of three strong factors (side-estimate, blueprint lines 2370-2378)

theorem TrilinearHT.Auto.power_cost_bound (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a b c : ℤ × ℤ → ℝ) (ha : ∀ I ∈ S, 0 ≤ a I) (hb : ∀ I ∈ S, 0 ≤ b I) (hc : ∀ I ∈ S, 0 ≤ c I) (root : ℤ × ℤ) (hR : ∀ I ∈ S, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G root.1 root.2) {Ca Cb Cc : ℝ} (hCa : ∀ (x : ℝ), ∑ I ∈ S with x ∈ dyadicGridCell G I.1 I.2, a I ^ 2 ≤ Ca) (hCb : ∀ (x : ℝ), ∑ I ∈ S with x ∈ dyadicGridCell G I.1 I.2, b I ^ 2 ≤ Cb) (hCc : ∀ (x : ℝ), ∑ I ∈ S with x ∈ dyadicGridCell G I.1 I.2, c I ^ 2 ≤ Cc) {p : ℝ} (hp : 2 / 3 < p) : ∑ I ∈ S, dyadicGridLength G I.1 * (a I * b I * c I) ^ p ≤ Ca ^ (p / 2) * Cb ^ (p / 2) * Cc ^ (p / 2) * dyadicGridLength G root.1

Blueprint lines 2373-2378 (eq:three-sides integrated along paths): cell weights a, b, c ≥ 0 whose squares have retained path sums at most C_a, C_b, C_c everywhere satisfy Σ_I |I| (a_I b_I c_I)^p ≤ (C_a C_b C_c)^{p/2} |R| for 2/3 < p.

theorem TrilinearHT.Auto.prod_four_le_of_three (f : Fin 4 → ℝ) (hf0 : ∀ (l : Fin 4), 0 ≤ f l) {B w : ℝ} (hB : ∀ (l : Fin 4), f l ≤ B) (Sd : Finset (Fin 4)) (hS : 3 ≤ Sd.card) (hw : ∀ l ∈ Sd, f l ≤ √w) : ∏ l : Fin 4, f l ≤ B * (w * √w)

Four factors bounded by B, of which at least three are bounded by √w, have product at most B w √w.

theorem TrilinearHT.Auto.sum_mul_sqrt_le {γ : Type u_2} (s : Finset γ) (w : γ → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) : ∑ i ∈ s, w i * √(w i) ≤ (∑ i ∈ s, w i) * √(∑ i ∈ s, w i)

Σ w_i √w_i ≤ (Σ w_i) √(Σ w_i) for nonnegative w.

theorem TrilinearHT.Auto.bands_bessel {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (Q : ℕ → H →L[ℂ] H) (T : ℕ) (hQ : ∀ n ≤ T, IsStarProjection (Q n)) (hnest : ∀ i ≤ T, ∀ j ≤ T, i ≤ j → Q i ∘SL Q j = Q i) (x : H) : ∑ q ∈ Finset.range T, ‖(Q (q + 1) - Q q) x‖ ^ 2 ≤ ‖x‖ ^ 2

Blueprint line 2388 ("pad bands are orthogonal at one cell"): the bands Q_{q+1} - Q_q of a nested family of star projections are Bessel: Σ_q ‖(Q_{q+1} - Q_q) x‖² ≤ ‖x‖².

theorem TrilinearHT.Auto.three_side_pattern_cell {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℂ W] (Gd : RealDyadicGrid) {γ : Type u_2} (I : ℤ × ℤ) (Gs : Finset γ) (Λ : MultilinearMap ℂ (fun (x : Fin 4) => W) ℂ) {C Bs : ℝ} (hC : 0 ≤ C) (hΛ : ∀ (x : Fin 4 → W), ‖Λ x‖ ≤ C * ∏ l : Fin 4, ‖x l‖ / √(dyadicGridLength Gd I.1)) (a s e : γ → Fin 4 → W) (hsize : ∀ G ∈ Gs, ∀ (l : Fin 4), ‖a G l‖ ≤ Bs * √(dyadicGridLength Gd I.1) ∧ ‖s G l‖ ≤ Bs * √(dyadicGridLength Gd I.1)) {σ : Fin 4 → Fin 3} (hσ : (∀ (l : Fin 4), σ l ≠ 2) ∧ 3 ≤ patternCount σ 1) : ‖∑ G ∈ Gs, Λ (patternPiece (a G) (s G) (e G) σ)‖ ≤ C * Bs * ((∑ G ∈ Gs, ∑ l : Fin 4, ‖s G l‖ ^ 2 / dyadicGridLength Gd I.1) * √(∑ G ∈ Gs, ∑ l : Fin 4, ‖s G l‖ ^ 2 / dyadicGridLength Gd I.1))

One error-free pattern with at least three sides at one cell, summed over the groups: ‖Σ_G Λ(pattern)‖ ≤ C B u √u with u = Σ_{G,l} ‖S_{G,l}‖² / |I| (blueprint eq:three-sides, Cauchy-Schwarz in the groups).

The pair-small restored main term (blueprint lines 2261-2262, 2385-2386)

Locality of the cell forms (blueprint line 2410, "which preserves its value there")

theorem TrilinearHT.Auto.rankMerge_map {α : Type u_1} {β : Type u_2} (key : α → ℕ) (key' : β → ℕ) (f g : α → β) (hf : ∀ (x : α), key' (f x) = key x) (hg : ∀ (x : α), key' (g x) = key x) (xs ys : List α) : rankMerge key' (List.map f xs) (List.map g ys) = List.map (fun (e : Bool × α) => (e.1, if e.1 = true then f e.2 else g e.2)) (rankMerge key xs ys)

Mapping both lists by key-preserving maps commutes with the rank merge.

theorem TrilinearHT.Auto.padFam_intertwine {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {P : ℕ} (r : E →L[ℂ] E) (Qg Ql : Fin P → E →L[ℂ] E) (h : ∀ (p : Fin P), r ∘SL Qg p = Ql p ∘SL r) (n : ℕ) (y : E) : r ((padFam Qg n) y) = (padFam Ql n) (r y)

theorem TrilinearHT.Auto.filterAvg_intertwine {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {P : ℕ} (r : E →L[ℂ] E) (Qg Ql : Fin P → E →L[ℂ] E) (h : ∀ (p : Fin P), r ∘SL Qg p = Ql p ∘SL r) (y : E) : r ((filterAvg P (padFam Qg)) y) = (filterAvg P (padFam Ql)) (r y)

theorem TrilinearHT.Auto.chainVal_intertwine {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {P : ℕ} (r : E →L[ℂ] E) (v : Bool) (gs ls : List (Bool × (Fin P → E →L[ℂ] E) × (Fin P → E →L[ℂ] E))) : List.Forall₂ (StepRel r) gs ls → ∀ (y : E), r (chainVal P v (List.map padStep gs) y) = chainVal P v (List.map padStep ls) (r y)

The complement values of intertwined step lists are intertwined.

noncomputable def TrilinearHT.Auto.helpPre {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (P : ℕ) : List (TransferStep E) → E → E

The helper prefix of a step list: the helper averages applied in step order.

Equations

• TrilinearHT.Auto.helpPre P [] x✝ = x✝
• TrilinearHT.Auto.helpPre P (st :: rest) x✝ = TrilinearHT.Auto.helpPre P rest ((TrilinearHT.Auto.filterAvg P st.2.1) x✝)

theorem TrilinearHT.Auto.helpPre_intertwine {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {P : ℕ} (r : E →L[ℂ] E) (gs ls : List (Bool × (Fin P → E →L[ℂ] E) × (Fin P → E →L[ℂ] E))) : List.Forall₂ (StepRel r) gs ls → ∀ (x : E), r (helpPre P (List.map padStep gs) x) = helpPre P (List.map padStep ls) (r x)

The band defects as a sum over the steps (blueprint lines 2252-2258)

noncomputable def TrilinearHT.Auto.defTerm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => E) ℂ) (P : ℕ) (a c d : Fin 4) (x : Fin 4 → E) (yc yd : E) (sel : ℕ → ℕ → Prop) [DecidableRel sel] (st : TransferStep E) (rest : List (TransferStep E)) (xa : E) : ℂ

The selected band defect of one step st, with the later steps rest and the helper input xa of the step.

Equations

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

theorem TrilinearHT.Auto.chainDefectSel_eq_sum {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => E) ℂ) (P : ℕ) (a c d : Fin 4) (x : Fin 4 → E) (yc yd : E) (sel : ℕ → ℕ → Prop) [DecidableRel sel] (steps : List (TransferStep E)) (xa : E) : chainDefectSel Λ P a c d x yc yd sel steps xa = ∑ j : Fin steps.length, defTerm Λ P a c d x yc yd sel steps[j] (List.drop (↑j + 1) steps) (helpPre P (List.take (↑j) steps) xa)

The selected band defects are the sum over the steps of their defects at the helper prefix of the earlier steps.

Global transfer steps of a pair of positive chains (blueprint lines 2386-2391)

theorem TrilinearHT.Auto.defTerm_intertwine {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => E) ℂ) {P : ℕ} (r : E →L[ℂ] E) (hr2 : ∀ (y : E), r (r y) = r y) (hloc : ∀ (x y : Fin 4 → E), (∀ (l : Fin 4), r (x l) = r (y l)) → Λ x = Λ y) {a c d : Fin 4} (sel : ℕ → ℕ → Prop) [DecidableRel sel] (sg sl : Bool × (Fin P → E →L[ℂ] E) × (Fin P → E →L[ℂ] E)) (hs : StepRel r sg sl) (gr lr gp lp : List (Bool × (Fin P → E →L[ℂ] E) × (Fin P → E →L[ℂ] E))) (hrr : List.Forall₂ (StepRel r) gr lr) (hpp : List.Forall₂ (StepRel r) gp lp) (xg xl : Fin 4 → E) (hx : ∀ (l : Fin 4), l ≠ a → l ≠ c → l ≠ d → r (xg l) = r (xl l)) (yc yd xa : E) : defTerm Λ P a c d xl (r yc) (r yd) sel (padStep sl) (List.map padStep lr) (helpPre P (List.map padStep lp) (r xa)) = defTerm Λ P a c d xg yc yd sel (padStep sg) (List.map padStep gr) (helpPre P (List.map padStep gp) xa)

A selected band defect of cell steps on restricted global inputs is the defect of the global steps, for a form that sees only the restrictions.

Nested pads of one depth (blueprint line 2388, "pad bands are orthogonal at one cell")

theorem TrilinearHT.Auto.cellColumnRange_mono_mask {V : Type u_1} [Fintype V] (D : ColumnTreeData V) {A₁ A₂ : InheritedColumnMask D} {c : ℤ × ℤ} (hc : c ∈ D.cells) (hA : A₁.labels c ⊆ A₂.labels c) : cellColumnRange D A₁ hc ≤ cellColumnRange D A₂ hc

The cell column ranges are monotone in the mask labels.

theorem TrilinearHT.Auto.partitionColumnRange_mono_mask {V : Type u_1} [Fintype V] (D : ColumnTreeData V) {A₁ A₂ : InheritedColumnMask D} (π : ColumnStoppingPartition D) (hA : ∀ c ∈ D.cells, A₁.labels c ⊆ A₂.labels c) : partitionColumnRange D A₁ π ≤ partitionColumnRange D A₂ π

The partition column ranges are monotone in the mask labels.

theorem TrilinearHT.Auto.ColumnDepthFamily.proj_mask_nested {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) {A₁ A₂ : InheritedColumnMask Ψ.D} (hA : ∀ c ∈ Ψ.D.cells, A₁.labels c ⊆ A₂.labels c) (h : ℤ) : (Ψ.withMask A₁).proj h ∘SL (Ψ.withMask A₂).proj h = (Ψ.withMask A₁).proj h

The depth projections with nested masks are nested.

The pad families of a band step after its helper prefix (blueprint lines 2408-2420)

noncomputable def TrilinearHT.Auto.padFamC {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {P : ℕ} (Q : Fin P → E →L[ℂ] E) (n : ℕ) : E →L[ℂ] E

The pad family Q_0 = 0, Q_p for 1 ≤ p ≤ P, Q_p = 1 beyond, as continuous maps.

Equations

• TrilinearHT.Auto.padFamC Q n = if n = 0 then 0 else if h : n - 1 < P then Q ⟨n - 1, h⟩ else ContinuousLinearMap.id ℂ E

theorem TrilinearHT.Auto.padFam_apply_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {P : ℕ} (Q : Fin P → E →L[ℂ] E) (n : ℕ) (y : E) : (padFam Q n) y = (padFamC Q n) y

theorem TrilinearHT.Auto.padFamC_bessel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {P : ℕ} (Q : Fin P → E →L[ℂ] E) (hQ : ∀ (p : Fin P), IsStarProjection (Q p)) (hnest : ∀ (p p' : Fin P), p ≤ p' → Q p ∘SL Q p' = Q p) (y : E) : ∑ p ∈ Finset.range (P + 1), ‖(padFamC Q (p + 1) - padFamC Q p) y‖ ^ 2 ≤ ‖y‖ ^ 2

The pad family of nested star projections is a nested family of star projections, so its bands are Bessel.

Frozen complements (blueprint lines 2386-2394)

theorem TrilinearHT.Auto.freeze_four {E : Type u_1} [AddCommGroup E] [Module ℂ E] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => E) ℂ) {e f : Fin 4} (hef : e ≠ f) (x : Fin 4 → E) (Yc Yb Fc Fb : E) : Λ (Function.update (Function.update x e Yc) f Fc) = Λ (Function.update (Function.update x e Yb) f Fb) + Λ (Function.update (Function.update x e (Yc - Yb)) f Fc) + Λ (Function.update (Function.update x e Yc) f (Fc - Fb)) - Λ (Function.update (Function.update x e (Yc - Yb)) f (Fc - Fb))

Blueprint lines 2388-2393 (freezing both complements and splitting the unbounded frozen one): Λ(Y, F) = Λ(Y_b, F_b) + Λ(Y - Y_b, F) + Λ(Y, F - F_b) - Λ(Y - Y_b, F - F_b) in two slots.

theorem TrilinearHT.Auto.sum_mul_le_sqrt_mul_sqrt {β : Type u_1} (u : Finset β) (a b : β → ℝ) : ∑ p ∈ u, a p * b p ≤ √(∑ p ∈ u, a p ^ 2) * √(∑ p ∈ u, b p ^ 2)

Cauchy-Schwarz for a finite sum of products of norms.

theorem TrilinearHT.Auto.prod_fin4_distinct {a b e f : Fin 4} (hab : a ≠ b) (hae : a ≠ e) (haf : a ≠ f) (hbe : b ≠ e) (hbf : b ≠ f) (hef : e ≠ f) (g : Fin 4 → ℝ) : ∏ l : Fin 4, g l = g a * g b * g e * g f

A product over the four slots, for four distinct slots.

theorem TrilinearHT.Auto.chainDefectSel_eq_sum_range {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => E) ℂ) (P : ℕ) (a c d : Fin 4) (x : Fin 4 → E) (yc yd : E) (sel : ℕ → ℕ → Prop) [DecidableRel sel] (steps : List (TransferStep E)) (xa : E) (dflt : TransferStep E) : chainDefectSel Λ P a c d x yc yd sel steps xa = ∑ j ∈ Finset.range steps.length, defTerm Λ P a c d x yc yd sel (steps.getD j dflt) (List.drop (j + 1) steps) (helpPre P (List.take j steps) xa)

chainDefectSel_eq_sum with the steps indexed by range and getD.

Power costs of three strong factors with group sums (blueprint lines 2372-2384)

theorem TrilinearHT.Auto.rpow_finsetSum_le {ι : Type u_1} (s : Finset ι) (t : ι → ℝ) (ht : ∀ i ∈ s, 0 ≤ t i) {p : ℝ} (hp : 0 < p) (hp1 : p ≤ 1) : (∑ i ∈ s, t i) ^ p ≤ ∑ i ∈ s, t i ^ p

(Σ t)^p ≤ Σ t^p for nonnegative terms and 0 ≤ p ≤ 1.

Budgets to caps (blueprint line 2373)

The transferred main term and the restoration errors on the main columns (lines 2382-2384)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.norm_Λc_le_sizes {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) (x : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (n : Fin 4 → ℝ) (hn0 : ∀ (j : Fin 4), 0 ≤ n j) (hn : ∀ (j : Fin 4), MeasureTheory.eLpNorm (augPhys (x j)) 2 (normalizedIntervalMeasure (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1)) ≤ ENNReal.ofReal (n j)) : ‖(fp.Λc I) x‖ ≤ localFormUniformConstant κ * (n 0 * n 1 * n 2 * n 3)

The cell form on the main columns is bounded by the product of the normalized L² sizes of the physical parts (localFormUniformConstant; zero off the active cells).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.Λc_pair_smallM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {I : ℤ × ℤ} (hI : I ∈ A.cells) {c d a b : Fin 4} (hcd : c ≠ d) (hca : c ≠ a) (hcb : c ≠ b) (hda : d ≠ a) (hdb : d ≠ b) (hab : a ≠ b) (X : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {Yc Yd : ℝ → ℂ} {τ : ℝ} (hτ : 0 ≤ τ) (hpair : PairSmall (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1) (A.w I) c d Yc Yd τ) (hXc : ∀ᵐ (y : ℝ), y ∈ dyadicGridCell A.G I.1 I.2 → augPhys (X c) y = Yc y) (hXd : ∀ᵐ (y : ℝ), y ∈ dyadicGridCell A.G I.1 I.2 → augPhys (X d) y = Yd y) {Sa Sb : ℝ} (hSa : 0 ≤ Sa) (hSb : 0 ≤ Sb) (hXa : MeasureTheory.eLpNorm (augPhys (X a)) 2 (normalizedIntervalMeasure (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1)) ≤ ENNReal.ofReal Sa) (hXb : MeasureTheory.eLpNorm (augPhys (X b)) 2 (normalizedIntervalMeasure (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1)) ≤ ENNReal.ofReal Sb) : ‖(fp.Λc I) X‖ ≤ τ * Sa * Sb

Blueprint line 2384 ("by pair-smallness"), at one cell on the main columns: with the physical parts of a pair-small pair in the slots c, d and inputs of normalized sizes at most S_a, S_b in the other slots, the cell form is at most τ S_a S_b.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.main_restoredM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {I : ℤ × ℤ} (hI : I ∈ A.cells) {a b c d : Fin 4} (hab : a ≠ b) (hac : a ≠ c) (had : a ≠ d) (hbc : b ≠ c) (hbd : b ≠ d) (hcd : c ≠ d) (x : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (D : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {η : ℝ} (hη : 0 ≤ η) (hpair : PairSmall (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1) (A.w I) c d (A.Y I c) (A.Y I d) η) {Sa Sb : ℝ} (hDa : ‖D‖ / √(dyadicGridLength A.G I.1) ≤ Sa) (hxb : ‖x b‖ / √(dyadicGridLength A.G I.1) ≤ Sb) : ‖(fp.Λc I) (Function.update (Function.update (Function.update x a D) c (bf.basicIn fp.Mc c I + bf.Ucol fp.Mc c I)) d (bf.basicIn fp.Mc d I + bf.Ucol fp.Mc d I))‖ ≤ η * Sa * Sb

Blueprint line 2384 ("the main term eq:transferred-main, with complements restored to their full Y arguments, costs η ... by pair-smallness, contractions"), at one cell, group and chain pair: the transferred main term with the full arguments Y_c = B_c + U_c, Y_d = B_d + U_d is at most η S_a S_b, where (Y_c, Y_d) is η-pair-small and S_a, S_b bound the normalized sizes of the transferred side and of the other side.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.restore_corrM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) {a b c d : Fin 4} (hab : a ≠ b) (hac : a ≠ c) (had : a ≠ d) (hbc : b ≠ c) (hbd : b ≠ d) (hcd : c ≠ d) (x : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (D u v : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {Sa Sb Su Sv : ℝ} (hDa : ‖D‖ / √(dyadicGridLength A.G I.1) ≤ Sa) (hxb : ‖x b‖ / √(dyadicGridLength A.G I.1) ≤ Sb) (hu : ‖u‖ / √(dyadicGridLength A.G I.1) ≤ Su) (hv : ‖v‖ / √(dyadicGridLength A.G I.1) ≤ Sv) : ‖(fp.Λc I) (Function.update (Function.update (Function.update x a D) c u) d v)‖ ≤ localFormUniformConstant κ * (Sa * Sb * (Su * Sv))

Blueprint line 2384 ("restoration errors have a third basic side"), at one cell, group and chain pair: a restoration correction with values u, v in the slots c, d is at most C_κ S_a S_b S_u S_v (one of u, v is a basic side U).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.norm_chainSide_mergeStepsM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (a c d : Fin 4) (rH : ℕ) (I : ℤ × ℤ) (xs ys : List (ℕ × (Fin fp.P → bf.Vtx → Prop))) (x : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : ‖chainSide fp.P (fp.mergeStepsM cat a c d rH I xs ys) x‖ ≤ ‖x‖

The side value after merged steps is a contraction of the side.

Certified variation of single masked outputs (blueprint lem:variation, lines 1871, 2386)

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

The global output of a single outer main projection with the inherited mask M after the shared history ls at the depth h (an individual pad choice of a filter, blueprint line 1871: "couple individual pad choices across times").

Equations

• fp.gOutM l s mb M ls h = ((bf.mainBase fp.Mc s mb).withMask M).proj h ∘SL fp.gHist l s mb ls h

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

The single masked global outputs at depth h commute with the restriction to every dyadic cell of depth at most the clamped depth h.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gOutM_rows_blk {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (M : InheritedColumnMask (bf.mainTree fp.Mc s mb)) (ls : List (ℕ × Bool)) {hr ht : ℤ} (hrt : hr ≤ ht) (htd : ht ≤ A.R.1 + ↑A.treeDepth) (E : Finset (ℤ × ℤ)) (hE : ∀ I ∈ E, I ∈ A.cells) {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (hΨG : Ψ.D.grid = A.G) (hΨR : dyadicGridCell A.G A.R.1 A.R.2 ⊆ dyadicGridCell A.G Ψ.D.root.1 Ψ.D.root.2) (hΨr : Ψ.D.root.1 ≤ A.R.1) (hRr : A.R.1 ≤ hr) (x : ↥(ColumnL2 (bf.RLab fp.Mc s))) : ‖(columnL2Restriction (⋃ I ∈ E, dyadicGridCell A.G I.1 I.2) ⋯ ∘SL (fp.gOutM l s mb M ls ht - fp.gOutM l s mb M ls hr)) x‖ ^ 2 = ∑ Q : ↥(Ψ.partition hr).cells, ‖(columnL2Restriction (⋃ I ∈ E, dyadicGridCell A.G I.1 I.2) ⋯ ∘SL (fp.gOutM l s mb M ls ht - fp.gOutM l s mb M ls hr)) ((columnL2Restriction (dyadicGridCell Ψ.D.grid (↑Q).1 (↑Q).2) ⋯) x)‖ ^ 2

The restricted jump rows of the single masked global outputs between two depths split orthogonally over the depth partition of a basic family at the left depth.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.main_blkM {κ : 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)) {hr ht : ℤ} (hrt : hr ≤ ht) (Ec : Finset (ℤ × ℤ)) (hEc : ∀ I ∈ Ec, I ∈ A.cells) (x : ↥(ColumnL2 (bf.RLab fp.Mc s))) : ‖(columnL2Restriction (⋃ I ∈ Ec, dyadicGridCell A.G I.1 I.2) ⋯ ∘SL (((bf.mainBase fp.Mc s mb).withMask M).proj ht - ((bf.mainBase fp.Mc s mb).withMask M).proj hr)) x‖ ^ 2 = ∑ Q : ↥((bf.mainBase fp.Mc s mb).partition hr).cells, ‖(columnL2Restriction (⋃ I ∈ Ec, dyadicGridCell A.G I.1 I.2) ⋯ ∘SL (((bf.mainBase fp.Mc s mb).withMask M).proj ht - ((bf.mainBase fp.Mc s mb).withMask M).proj hr)) ((columnL2Restriction (dyadicGridCell A.G (↑Q).1 (↑Q).2) ⋯) x)‖ ^ 2

The restricted jump rows of a single masked main depth family split orthogonally over the main partition at the left depth (main_blk for any inherited mask).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.main_variationM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] (Mk : ι → InheritedColumnMask (bf.mainTree fp.Mc s mb)) (ls : List (ℕ × Bool)) (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'))) (Ec : ι → ι' → Finset (ℤ × ℤ)) (hEc : ∀ (G : ι) (i : ι'), ∀ I ∈ Ec G i, I ∈ A.cells) {Cw : ℝ} (hCw : 0 ≤ Cw) (hwr1 : ∀ (x : ι × ι' → ↥(ColumnL2 (bf.RLab fp.Mc s))), ‖∑ q : ι × ι', (ContinuousLinearMap.adjoint (columnL2Restriction (⋃ I ∈ Ec q.1 q.2, dyadicGridCell A.G I.1 I.2) ⋯ ∘SL (((bf.mainBase fp.Mc s mb).withMask (Mk q.1)).proj (A.R.1 + ↑(t q.2)) - ((bf.mainBase fp.Mc s mb).withMask (Mk q.1)).proj (A.R.1 + ↑(r q.2))))) (x q)‖ ^ 2 ≤ Cw * ∑ G : ι, ‖∑ q : ι × ι' with q.1 = G, (ContinuousLinearMap.adjoint (columnL2Restriction (⋃ I ∈ Ec q.1 q.2, dyadicGridCell A.G I.1 I.2) ⋯ ∘SL (((bf.mainBase fp.Mc s mb).withMask (Mk q.1)).proj (A.R.1 + ↑(t q.2)) - ((bf.mainBase fp.Mc s mb).withMask (Mk q.1)).proj (A.R.1 + ↑(r q.2))))) (x q)‖ ^ 2) (hwr2 : ∀ (i : ι') (x : ι → ↥(ColumnL2 (bf.RLab fp.Mc s))), ‖∑ G : ι, (ContinuousLinearMap.adjoint (columnL2Restriction (⋃ I ∈ Ec G i, dyadicGridCell A.G I.1 I.2) ⋯ ∘SL ((bf.mainBase fp.Mc s mb).withMask (Mk G)).proj (A.R.1 + ↑(t i)))) (x G)‖ ^ 2 ≤ Cw * ∑ G : ι, ‖∑ G' : ι with G' = G, (ContinuousLinearMap.adjoint (columnL2Restriction (⋃ I ∈ Ec G' i, dyadicGridCell A.G I.1 I.2) ⋯ ∘SL ((bf.mainBase fp.Mc s mb).withMask (Mk G')).proj (A.R.1 + ↑(t i)))) (x G')‖ ^ 2) (z : ↥(ColumnL2 (bf.RLab fp.Mc s))) : ∑ q : ι × ι', ‖(columnL2Restriction (⋃ I ∈ Ec q.1 q.2, dyadicGridCell A.G I.1 I.2) ⋯) ((fp.gOutM l s mb (Mk q.1) ls (A.R.1 + ↑(t q.2))) z - (fp.gOutM l s mb (Mk q.1) ls (A.R.1 + ↑(r q.2))) z)‖ ^ 2 ≤ 2 * Cw * (compressionC (bf.mainTree fp.Mc s mb) ls.length ^ 2 * ‖z‖ ^ 2 + (↑ls.length * ∑ m ∈ Finset.range ls.length, compressionC (bf.mainTree fp.Mc s mb) m ^ 2) * ‖z‖ ^ 2)

Blueprint lem:variation (lines 1871-1877) for single masked outputs with a common input z: if the restricted interval rows of the outer masks M_G are jointly Bessel with constant C_w across groups (hwr1, hwr2: the whole-range conditions), the outputs M_{G,s} B'_s z have square-summable certified variation over disjoint depth intervals, Σ ‖1_E (Z_{G,t} - Z_{G,r})‖² ≤ 2 C_w (C_{|ls|}² + |ls| Σ_m C_m²) ‖z‖².

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.main_jointM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) {ι : Type u_1} [Fintype ι] (Mk : ι → InheritedColumnMask (bf.mainTree fp.Mc s mb)) (ls : List (ℕ × Bool)) (ht : ℤ) (Ec : ι → Finset (ℤ × ℤ)) {Cw : ℝ} (hCw : 0 ≤ Cw) (hwr2 : ∀ (x : ι → ↥(ColumnL2 (bf.RLab fp.Mc s))), ‖∑ G : ι, (ContinuousLinearMap.adjoint (columnL2Restriction (⋃ I ∈ Ec G, dyadicGridCell A.G I.1 I.2) ⋯ ∘SL ((bf.mainBase fp.Mc s mb).withMask (Mk G)).proj ht)) (x G)‖ ^ 2 ≤ Cw * ∑ G : ι, ‖∑ G' : ι with G' = G, (ContinuousLinearMap.adjoint (columnL2Restriction (⋃ I ∈ Ec G', dyadicGridCell A.G I.1 I.2) ⋯ ∘SL ((bf.mainBase fp.Mc s mb).withMask (Mk G')).proj ht)) (x G')‖ ^ 2) (w : ↥(ColumnL2 (bf.RLab fp.Mc s))) : ∑ G : ι, ‖(columnL2Restriction (⋃ I ∈ Ec G, dyadicGridCell A.G I.1 I.2) ⋯) ((fp.gOutM l s mb (Mk G) ls ht) w)‖ ^ 2 ≤ Cw * ‖w‖ ^ 2

eq:whole-ranges for single masked outputs at one depth: with the whole-range condition the outputs of the groups on unions of cells of that depth are jointly Bessel with constant C_w.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.main_variation_basicM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] (Mk : ι → InheritedColumnMask (bf.mainTree fp.Mc s mb)) (ls : List (ℕ × Bool)) (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'))) (htd : ∀ (i : ι'), t i ≤ A.treeDepth) (Ec : ι → ι' → Finset (ℤ × ℤ)) (hEc : ∀ (G : ι) (i : ι'), ∀ I ∈ Ec G i, I ∈ A.cells) {Cw : ℝ} (hCw : 0 ≤ Cw) (hwr1 : ∀ (x : ι × ι' → ↥(ColumnL2 (bf.RLab fp.Mc s))), ‖∑ q : ι × ι', (ContinuousLinearMap.adjoint (columnL2Restriction (⋃ I ∈ Ec q.1 q.2, dyadicGridCell A.G I.1 I.2) ⋯ ∘SL (((bf.mainBase fp.Mc s mb).withMask (Mk q.1)).proj (A.R.1 + ↑(t q.2)) - ((bf.mainBase fp.Mc s mb).withMask (Mk q.1)).proj (A.R.1 + ↑(r q.2))))) (x q)‖ ^ 2 ≤ Cw * ∑ G : ι, ‖∑ q : ι × ι' with q.1 = G, (ContinuousLinearMap.adjoint (columnL2Restriction (⋃ I ∈ Ec q.1 q.2, dyadicGridCell A.G I.1 I.2) ⋯ ∘SL (((bf.mainBase fp.Mc s mb).withMask (Mk q.1)).proj (A.R.1 + ↑(t q.2)) - ((bf.mainBase fp.Mc s mb).withMask (Mk q.1)).proj (A.R.1 + ↑(r q.2))))) (x q)‖ ^ 2) (hwr2 : ∀ (i : ι') (x : ι → ↥(ColumnL2 (bf.RLab fp.Mc s))), ‖∑ G : ι, (ContinuousLinearMap.adjoint (columnL2Restriction (⋃ I ∈ Ec G i, dyadicGridCell A.G I.1 I.2) ⋯ ∘SL ((bf.mainBase fp.Mc s mb).withMask (Mk G)).proj (A.R.1 + ↑(t i)))) (x G)‖ ^ 2 ≤ Cw * ∑ G : ι, ‖∑ G' : ι with G' = G, (ContinuousLinearMap.adjoint (columnL2Restriction (⋃ I ∈ Ec G' i, dyadicGridCell A.G I.1 I.2) ⋯ ∘SL ((bf.mainBase fp.Mc s mb).withMask (Mk G')).proj (A.R.1 + ↑(t i)))) (x G')‖ ^ 2) (jb : Fin 2) (Z : ↥(ColumnL2 (bf.P l jb).V)) : ∑ q : ι × ι', ‖(columnL2Restriction (⋃ I ∈ Ec q.1 q.2, dyadicGridCell A.G I.1 I.2) ⋯) ((fp.gOutM l s mb (Mk q.1) ls (A.R.1 + ↑(t q.2))) ((bf.famEmbR fp.Mc s l jb) (((bf.P l jb).Ψ.proj (A.R.1 + ↑(t q.2))) Z)) - (fp.gOutM l s mb (Mk q.1) ls (A.R.1 + ↑(r q.2))) ((bf.famEmbR fp.Mc s l jb) (((bf.P l jb).Ψ.proj (A.R.1 + ↑(r q.2))) Z)))‖ ^ 2 ≤ 2 * (2 * Cw * (compressionC (bf.mainTree fp.Mc s mb) ls.length ^ 2 + ↑ls.length * ∑ m ∈ Finset.range ls.length, compressionC (bf.mainTree fp.Mc s mb) m ^ 2) * compressionC (bf.P l jb).Ψ.D 1 ^ 2 * ‖Z‖ ^ 2) + 2 * (Cw * ‖Z‖ ^ 2)

Blueprint lem:variation (lines 1861-1877) for single masked outputs of a basic slot and one of its basic families j_b: the histories act on the basic depth projection P_{l,j_b,h} F, and the certified variation over disjoint depth intervals is at most 2 (B C₁² ‖F‖²) + 2 C_w ‖F‖², with B the constant of main_variationM.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.basicOutM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (M : InheritedColumnMask (bf.mainTree fp.Mc s mb)) (ls : List (ℕ × Bool)) (h : ℤ) : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))

The global single masked output of a basic slot: the outer main projection with mask M after the shared history ls, acting on the global basic input at the depth h.

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.basicOutM_eq {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (M : InheritedColumnMask (bf.mainTree fp.Mc s mb)) (ls : List (ℕ × Bool)) (h : ℤ) : fp.basicOutM l s mb M ls h = (colRelabel (bf.rv fp.Mc s)) ((fp.gOutM l s mb M ls h) ((bf.famEmbR fp.Mc s l 0) (((bf.P l 0).Ψ.proj h) (bf.P l 0).Z)) - (fp.gOutM l s mb M ls h) ((bf.famEmbR fp.Mc s l 1) (((bf.P l 1).Ψ.proj h) (bf.P l 1).Z)))

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.out_restrictRM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (hne : A.cells.Nonempty) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (M : InheritedColumnMask (bf.mainTree fp.Mc s mb)) (ls : List (ℕ × Bool)) (jb : Fin 2) {h : ℤ} (hRh : A.R.1 ≤ h) (E : Finset (ℤ × ℤ)) (hE : ∀ I ∈ E, I ∈ A.cells) (Z : ↥(ColumnL2 (bf.P l jb).V)) : (columnL2Restriction (⋃ I ∈ E, dyadicGridCell A.G I.1 I.2) ⋯) ((fp.gOutM l s mb M ls h) ((bf.famEmbR fp.Mc s l jb) (((bf.P l jb).Ψ.proj h) Z))) = (columnL2Restriction (⋃ I ∈ E, dyadicGridCell A.G I.1 I.2) ⋯) ((fp.gOutM l s mb M ls h) ((bf.famEmbR fp.Mc s l jb) (((bf.P l jb).Ψ.proj h) ((columnL2Restriction (dyadicGridCell A.G A.R.1 A.R.2) ⋯) Z))))

On unions of active cells, the single masked outputs of a basic family depend only on the restriction of the family input to the attempt root.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.basic_variationM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (hne : A.cells.Nonempty) {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] (Mk : ι → InheritedColumnMask (bf.mainTree fp.Mc s mb)) (ls : List (ℕ × Bool)) (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'))) (htd : ∀ (i : ι'), t i ≤ A.treeDepth) (Ec : ι → ι' → Finset (ℤ × ℤ)) (hEc : ∀ (G : ι) (i : ι'), ∀ I ∈ Ec G i, I ∈ A.cells) {Cw : ℝ} (hCw : 0 ≤ Cw) (hwr1 : ∀ (x : ι × ι' → ↥(ColumnL2 (bf.RLab fp.Mc s))), ‖∑ q : ι × ι', (ContinuousLinearMap.adjoint (columnL2Restriction (⋃ I ∈ Ec q.1 q.2, dyadicGridCell A.G I.1 I.2) ⋯ ∘SL (((bf.mainBase fp.Mc s mb).withMask (Mk q.1)).proj (A.R.1 + ↑(t q.2)) - ((bf.mainBase fp.Mc s mb).withMask (Mk q.1)).proj (A.R.1 + ↑(r q.2))))) (x q)‖ ^ 2 ≤ Cw * ∑ G : ι, ‖∑ q : ι × ι' with q.1 = G, (ContinuousLinearMap.adjoint (columnL2Restriction (⋃ I ∈ Ec q.1 q.2, dyadicGridCell A.G I.1 I.2) ⋯ ∘SL (((bf.mainBase fp.Mc s mb).withMask (Mk q.1)).proj (A.R.1 + ↑(t q.2)) - ((bf.mainBase fp.Mc s mb).withMask (Mk q.1)).proj (A.R.1 + ↑(r q.2))))) (x q)‖ ^ 2) (hwr2 : ∀ (i : ι') (x : ι → ↥(ColumnL2 (bf.RLab fp.Mc s))), ‖∑ G : ι, (ContinuousLinearMap.adjoint (columnL2Restriction (⋃ I ∈ Ec G i, dyadicGridCell A.G I.1 I.2) ⋯ ∘SL ((bf.mainBase fp.Mc s mb).withMask (Mk G)).proj (A.R.1 + ↑(t i)))) (x G)‖ ^ 2 ≤ Cw * ∑ G : ι, ‖∑ G' : ι with G' = G, (ContinuousLinearMap.adjoint (columnL2Restriction (⋃ I ∈ Ec G' i, dyadicGridCell A.G I.1 I.2) ⋯ ∘SL ((bf.mainBase fp.Mc s mb).withMask (Mk G')).proj (A.R.1 + ↑(t i)))) (x G')‖ ^ 2) : ∑ q : ι × ι', ‖(columnL2Restriction (⋃ I ∈ Ec q.1 q.2, dyadicGridCell A.G I.1 I.2) ⋯) (fp.basicOutM l s mb (Mk q.1) ls (A.R.1 + ↑(t q.2)) - fp.basicOutM l s mb (Mk q.1) ls (A.R.1 + ↑(r q.2)))‖ ^ 2 ≤ ∑ jb : Fin 2, 2 * (2 * (2 * Cw * (compressionC (bf.mainTree fp.Mc s mb) ls.length ^ 2 + ↑ls.length * ∑ m ∈ Finset.range ls.length, compressionC (bf.mainTree fp.Mc s mb) m ^ 2) * compressionC (bf.P l jb).Ψ.D 1 ^ 2) + 2 * Cw) * ‖(columnL2Restriction (dyadicGridCell A.G A.R.1 A.R.2) ⋯) (bf.P l jb).Z‖ ^ 2

Blueprint lem:variation (eq:variation) for single masked basic outputs: with the whole-range conditions at constant C_w, Σ_{G,i} ‖1_E (Z_{G,t_i} - Z_{G,r_i})‖² ≤ Σ_{j_b} 2 V_{j_b} ‖1_R F_{l,j_b}‖², V_{j_b} = 2 (2 C_w S) C_{1,j_b}² + 2 C_w.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.basic_variationM_le {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (ls : List (ℕ × Bool)) {Cw : ℝ} (hCw : Cw ≤ 2) (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)) : ∑ jb : Fin 2, 2 * (2 * (2 * Cw * (compressionC (bf.mainTree fp.Mc s mb) ls.length ^ 2 + ↑ls.length * ∑ m ∈ Finset.range ls.length, compressionC (bf.mainTree fp.Mc s mb) m ^ 2) * compressionC (bf.P l jb).Ψ.D 1 ^ 2) + 2 * Cw) * ‖(columnL2Restriction (dyadicGridCell A.G A.R.1 A.R.2) ⋯) (bf.P l jb).Z‖ ^ 2 ≤ 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)

The variation constants of basic_variationM with C_w ≤ 2 are at most the compression loss G₀ (blueprint line 1877), giving the bound G₀ · 4 |R|.

Frozen complements on the main columns (blueprint line 2386)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.basic_variation_ballP {κ : 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) {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] (grp : ι → bf.Grp) (hgrp : Function.Injective grp) (k j : ℕ) (hPH : fp.bbase j + fp.P ≤ fp.Hmax) (ls : List (ℕ × Bool)) (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'))) (htd : ∀ (i : ι'), t i ≤ A.treeDepth) (Ec : ι → ι' → Finset (ℤ × ℤ)) (hEc : ∀ (G : ι) (i : ι'), ∀ I ∈ Ec G i, I ∈ A.cells ∧ I.1 = A.R.1 + ↑(t i)) (hcert : ∀ (G : ι) (i : ι'), ∀ I ∈ Ec G i, fp.Cert k (grp G) I) {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 : ι × (bf.Lab ⊕ Fin fp.Mc) | ∃ I ∈ A.cells, (∃ (k' : ℕ), fp.Cert k' (grp 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 (grp 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)) (p : Fin fp.P) : ∑ q : ι × ι', ‖(columnL2Restriction (⋃ I ∈ Ec q.1 q.2, dyadicGridCell A.G I.1 I.2) ⋯) (fp.basicOutM l s mb (fp.ballMaskT l s mb (grp q.1) j p) ls (A.R.1 + ↑(t q.2)) - fp.basicOutM l s mb (fp.ballMaskT l s mb (grp q.1) j p) ls (A.R.1 + ↑(r q.2)))‖ ^ 2 ≤ 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 lines 1861-1877 and 2386 for an individual pad of a ball filter ("joint group budgets for positive ball ranges"): the global outputs of the pad-p ball projections of the groups after the shared history of the basic input have certified variation at most G₀ · 4 |R| over disjoint depth intervals.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.basic_variation_cumP {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (hne : A.cells.Nonempty) {ι' : Type u_1} [Fintype ι'] (m : ℕ) (p : Fin fp.P) (ls : List (ℕ × Bool)) (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'))) (htd : ∀ (i : ι'), t i ≤ A.treeDepth) (Ec : ι' → Finset (ℤ × ℤ)) (hEc : ∀ (i : ι'), ∀ I ∈ Ec i, I ∈ A.cells) (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)) : ∑ i : ι', ‖(columnL2Restriction (⋃ I ∈ Ec i, dyadicGridCell A.G I.1 I.2) ⋯) (fp.basicOutM l s mb (fp.cumMaskT l s mb m p) ls (A.R.1 + ↑(t i)) - fp.basicOutM l s mb (fp.cumMaskT l s mb m p) ls (A.R.1 + ↑(r i)))‖ ^ 2 ≤ 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 lines 1868 and 2386 for an individual pad of a cumulative filter ("shared budgets for group-independent histories"): the global outputs of the pad-p cumulative projection of the split m after the shared history of the basic input have certified variation at most G₀ · 4 |R| over disjoint depth intervals, without a sum over groups.

Flags of large frozen complements (blueprint line 2388)