Section 14.5: Common cuts, hull maxima, and summation

This file was automatically generated by Claude.

Formalization of blueprint Section 14, "The two-side estimate" (sec:sides), subsection 5, "Common cuts, hull maxima, and summation" (lines 2425-2459) of blueprint/formalization_blueprint.tex.

theorem TrilinearHT.Auto.min_le_rpow_mul {η x p : ℝ} (hη : 0 ≤ η) (hx : 0 ≤ x) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : min η x ≤ η ^ (1 - p) * x ^ p

Blueprint eq:min-power (line 2445): min(η, x) ≤ η^{1-p} x^p for x ≥ 0, 0 ≤ p ≤ 1.

theorem TrilinearHT.Auto.hull_maxima_cauchy_schwarz {ι : Type u_1} (s : Finset ι) (ma mb : ι → ℝ) (ha : ∀ i ∈ s, 0 ≤ ma i) (hb : ∀ i ∈ s, 0 ≤ mb i) : ∑ i ∈ s, √(ma i * mb i) ≤ √(∑ i ∈ s, ma i) * √(∑ i ∈ s, mb i)

Blueprint lines 2433-2436: on each remainder the stopping cell gives a_Q b_Q ≤ √(m_a m_b), and pointwise Cauchy–Schwarz over the indices ν gives Σ_ν √(m_{a,ν} m_{b,ν}) ≤ √(Σ_ν m_{a,ν}) √(Σ_ν m_{b,ν}).

Sparse decomposition and summation for the side estimate (blueprint lines 2425-2456)

theorem TrilinearHT.Auto.stopping_cells_volume_le (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (root : ℤ × ℤ) (hS : ∀ c ∈ S, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G root.1 root.2) (g : ℝ → ENNReal) {lam : ENNReal} (hlam : lam ≠ 0) : MeasureTheory.volume (⋃ c ∈ {c ∈ S | lam < dyadicEnergyAverage G g c}, dyadicGridCell G c.1 c.2) ≤ (∫⁻ (x : ℝ) in dyadicGridCell G root.1 root.2, g x) / lam

Blueprint lines 2430-2431: in a finite family of cells inside a root, the cells whose average of a fixed energy g exceeds λ cover total length at most (∫_root g) / λ; the bound is realized by the disjoint maximal stopping cells.

theorem TrilinearHT.Auto.sparse_two_stacks_volume_le (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (root : ℤ × ℤ) (hS : ∀ c ∈ S, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G root.1 root.2) (ga gb : ℝ → ENNReal) : MeasureTheory.volume (⋃ c ∈ {c ∈ S | 16 * dyadicEnergyAverage G ga root < dyadicEnergyAverage G ga c ∨ 16 * dyadicEnergyAverage G gb root < dyadicEnergyAverage G gb c}, dyadicGridCell G c.1 c.2) ≤ MeasureTheory.volume (dyadicGridCell G root.1 root.2) / 8

Blueprint lines 2430-2431: stopping at the first descendants where either squared stack average exceeds sixteen times its root average, the next roots have total length at most |Q|/8; a zero root size gives no stopping cell.

def TrilinearHT.Auto.patternSign {ι : Type u_1} [DecidableEq ι] (u : Finset ι) (i : ι) : ℝ

The sign ε_i = ±1 of the sign pattern u (+1 on u).

Equations

• TrilinearHT.Auto.patternSign u i = if i ∈ u then 1 else -1

theorem TrilinearHT.Auto.rademacherSum_eq_sign {ι : Type u_1} {E : Type u_2} [DecidableEq ι] [AddCommGroup E] [Module ℝ E] (s u : Finset ι) (v : ι → E) : rademacherSum s u v = ∑ i ∈ s, patternSign u i • v i

theorem TrilinearHT.Auto.sum_patternSign_mul {ι : Type u_1} [DecidableEq ι] (s : Finset ι) {a i : ι} (ha : a ∈ s) (hi : i ∈ s) : ∑ u ∈ s.powerset, patternSign u a * patternSign u i = if a = i then 2 ^ s.card else 0

Sign orthogonality: Σ_{u ⊆ s} ε_a(u) ε_i(u) = 2^{|s|} [a = i] for a, i ∈ s.

theorem TrilinearHT.Auto.near_band_summation {N : Type u_1} {ι : Type u_2} (Ns : Finset N) (Qs : N → Finset ι) (len a b : ι → ENNReal) (E : ι → Set ℝ) (hEm : ∀ (Q : ι), MeasurableSet (E Q)) {R : Set ℝ} (hRm : MeasurableSet R) (hdis : ∀ ν ∈ Ns, (↑(Qs ν)).PairwiseDisjoint E) (hER : ∀ ν ∈ Ns, ∀ Q ∈ Qs ν, E Q ⊆ R) (hvol : ∀ ν ∈ Ns, ∀ Q ∈ Qs ν, 7 * len Q ≤ 8 * MeasureTheory.volume (E Q)) (ma mb : N → ℝ → ENNReal) (hab : ∀ ν ∈ Ns, ∀ Q ∈ Qs ν, ∀ x ∈ E Q, a Q * b Q ≤ (ma ν x * mb ν x) ^ (1 / 2)) {A B : ENNReal} (hA : ∀ x ∈ R, ∑ ν ∈ Ns, ma ν x ≤ A) (hB : ∀ x ∈ R, ∑ ν ∈ Ns, mb ν x ≤ B) : 7 * ∑ ν ∈ Ns, ∑ Q ∈ Qs ν, len Q * (a Q * b Q) ≤ 8 * ((A * B) ^ (1 / 2) * MeasureTheory.volume R)

Blueprint lines 2433-2440 (summation for eq:near-band): for each index ν the sparse pieces Q have disjoint remainders E_Q ⊆ R with |E_Q| ≥ 7|Q|/8; on E_Q the root sizes obey a_Q b_Q ≤ √(m_{a,ν} m_{b,ν}); and the hull maxima satisfy the joint caps Σ_ν m_{a,ν} ≤ A, Σ_ν m_{b,ν} ≤ B on R. Then Σ_{ν,Q} |Q| a_Q b_Q ≤ (8/7) √(AB) |R|.

theorem TrilinearHT.Auto.near_band_total {N : Type u_1} {ι : Type u_2} (Ns : Finset N) (Qs : N → Finset ι) (len a b : ι → ENNReal) (E : ι → Set ℝ) (hEm : ∀ (Q : ι), MeasurableSet (E Q)) {R : Set ℝ} (hRm : MeasurableSet R) (hdis : ∀ ν ∈ Ns, (↑(Qs ν)).PairwiseDisjoint E) (hER : ∀ ν ∈ Ns, ∀ Q ∈ Qs ν, E Q ⊆ R) (hvol : ∀ ν ∈ Ns, ∀ Q ∈ Qs ν, 7 * len Q ≤ 8 * MeasureTheory.volume (E Q)) (ma mb : N → ℝ → ENNReal) (hab : ∀ ν ∈ Ns, ∀ Q ∈ Qs ν, ∀ x ∈ E Q, a Q * b Q ≤ (ma ν x * mb ν x) ^ (1 / 2)) {A B : ENNReal} (hA : ∀ x ∈ R, ∑ ν ∈ Ns, ma ν x ≤ A) (hB : ∀ x ∈ R, ∑ ν ∈ Ns, mb ν x ≤ B) (term : ι → ENNReal) (C : ENNReal) (hterm : ∀ ν ∈ Ns, ∀ Q ∈ Qs ν, term Q ≤ C * (len Q * (a Q * b Q))) : 7 * ∑ ν ∈ Ns, ∑ Q ∈ Qs ν, term Q ≤ 8 * C * ((A * B) ^ (1 / 2) * MeasureTheory.volume R)

Blueprint lines 2433-2442 (eq:near-band assembly): if every sparse piece Q of every index ν contributes at most C |Q| a_Q b_Q (the short-block comparison on the piece), the remainders satisfy the hypotheses of near_band_summation and the hull maxima the joint caps A, B, then the total is at most (8/7) C √(AB) |R|.

theorem TrilinearHT.Auto.card_signPattern {ι : Type u_1} (s : Finset ι) : Fintype.card (SignPattern s) = 2 ^ s.card

Joint hull caps for the two stacks (blueprint lines 2425-2433)

theorem TrilinearHT.Auto.dyadicHullMax_mono (G : RealDyadicGrid) {S T : Finset (ℤ × ℤ)} (hST : S ⊆ T) (g : ℝ → ENNReal) (x : ℝ) : dyadicHullMax G S g x ≤ dyadicHullMax G T g x

The coupled-band estimate (eq:near-band, blueprint lines 2433-2445)

theorem TrilinearHT.Auto.energyAverage_le_hullMax (G : RealDyadicGrid) {S : Finset (ℤ × ℤ)} {c : ℤ × ℤ} (hc : c ∈ S) (g : ℝ → ENNReal) {x : ℝ} (hx : x ∈ dyadicGridCell G c.1 c.2) : dyadicEnergyAverage G g c ≤ dyadicHullMax G S g x

theorem TrilinearHT.Auto.near_band_estimate (G : RealDyadicGrid) {N : Type u_1} (Ns : Finset N) (Hs Qs : N → Finset (ℤ × ℤ)) (hQH : ∀ ν ∈ Ns, Qs ν ⊆ Hs ν) (E : N → ℤ × ℤ → Set ℝ) (hEm : ∀ (ν : N) (Q : ℤ × ℤ), MeasurableSet (E ν Q)) {R : Set ℝ} (hRm : MeasurableSet R) (hdis : ∀ ν ∈ Ns, (↑(Qs ν)).PairwiseDisjoint (E ν)) (hEQ : ∀ ν ∈ Ns, ∀ Q ∈ Qs ν, E ν Q ⊆ dyadicGridCell G Q.1 Q.2 ∩ R) (hvol : ∀ ν ∈ Ns, ∀ Q ∈ Qs ν, 7 * ENNReal.ofReal (dyadicGridLength G Q.1) ≤ 8 * MeasureTheory.volume (E ν Q)) (ga gb : N → ℝ → ENNReal) {A B : ENNReal} (hA : ∀ x ∈ R, ∑ ν ∈ Ns, dyadicHullMax G (Hs ν) (ga ν) x ≤ A) (hB : ∀ x ∈ R, ∑ ν ∈ Ns, dyadicHullMax G (Hs ν) (gb ν) x ≤ B) (term : N → ℤ × ℤ → ENNReal) (C : ENNReal) (hterm : ∀ ν ∈ Ns, ∀ Q ∈ Qs ν, term ν Q ≤ C * (ENNReal.ofReal (dyadicGridLength G Q.1) * (dyadicEnergyAverage G (ga ν) Q ^ (1 / 2) * dyadicEnergyAverage G (gb ν) Q ^ (1 / 2)))) : 7 * ∑ ν ∈ Ns, ∑ Q ∈ Qs ν, term ν Q ≤ 8 * C * ((A * B) ^ (1 / 2) * MeasureTheory.volume R)

Blueprint lines 2433-2445 (eq:near-band): for each index ν, sparse pieces Q lying in the retained hull H_ν, with disjoint remainders E_Q ⊆ Q ∩ R of length at least 7|Q|/8, and terms bounded by C |Q| a_Q b_Q with the root sizes a_Q² = ⨍_Q g_a, b_Q² = ⨍_Q g_b (from lem:shortblock on the pieces), sum to at most (8/7) C √(AB) |R| when the hull maxima have the joint caps Σ_ν m_{a,ν} ≤ A, Σ_ν m_{b,ν} ≤ B on R.

Sparse pieces as short-block trees (blueprint lines 2433-2437)

noncomputable def TrilinearHT.Auto.pieceInternal (G : RealDyadicGrid) (Q : ℤ × ℤ) (C : Finset (ℤ × ℤ)) : Finset (ℤ × ℤ)

The internal cells of a piece: the root and all cells between it and the summation cells.

Equations

• TrilinearHT.Auto.pieceInternal G Q C = insert Q (C.biUnion fun (c : ℤ × ℤ) => Finset.image (fun (n : ℕ) => TrilinearHT.Auto.ancAt G c (Q.1 + ↑n)) (Finset.range ((c.1 - Q.1).toNat + 1)))

noncomputable def TrilinearHT.Auto.pieceLeaves (G : RealDyadicGrid) (Q : ℤ × ℤ) (C : Finset (ℤ × ℤ)) : Finset (ℤ × ℤ)

The leaves of a piece: children of internal cells that are not internal.

Equations

• TrilinearHT.Auto.pieceLeaves G Q C = {d ∈ (TrilinearHT.Auto.pieceInternal G Q C).biUnion (TrilinearHT.Auto.dyadicChildren G) | d ∉ TrilinearHT.Auto.pieceInternal G Q C}

theorem TrilinearHT.Auto.mem_pieceInternal {G : RealDyadicGrid} {Q : ℤ × ℤ} {C : Finset (ℤ × ℤ)} (hC : ∀ c ∈ C, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G Q.1 Q.2) {d : ℤ × ℤ} : d ∈ pieceInternal G Q C ↔ d = Q ∨ ∃ c ∈ C, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2 ∧ dyadicGridCell G d.1 d.2 ⊆ dyadicGridCell G Q.1 Q.2

theorem TrilinearHT.Auto.pieceInternal_anc {G : RealDyadicGrid} {Q : ℤ × ℤ} {C : Finset (ℤ × ℤ)} (hC : ∀ c ∈ C, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G Q.1 Q.2) {d e : ℤ × ℤ} (hd : d ∈ pieceInternal G Q C) (hde : dyadicGridCell G d.1 d.2 ⊆ dyadicGridCell G e.1 e.2) (heQ : dyadicGridCell G e.1 e.2 ⊆ dyadicGridCell G Q.1 Q.2) : e ∈ pieceInternal G Q C

Internal cells are closed under ancestors below the root.

theorem TrilinearHT.Auto.pieceInternal_sub {G : RealDyadicGrid} {Q : ℤ × ℤ} {C : Finset (ℤ × ℤ)} (hC : ∀ c ∈ C, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G Q.1 Q.2) {d : ℤ × ℤ} (hd : d ∈ pieceInternal G Q C) : dyadicGridCell G d.1 d.2 ⊆ dyadicGridCell G Q.1 Q.2

theorem TrilinearHT.Auto.mem_pieceLeaves {G : RealDyadicGrid} {Q : ℤ × ℤ} {C : Finset (ℤ × ℤ)} {L : ℤ × ℤ} : L ∈ pieceLeaves G Q C ↔ L ∉ pieceInternal G Q C ∧ ∃ d ∈ pieceInternal G Q C, L ∈ dyadicChildren G d

noncomputable def TrilinearHT.Auto.pieceTree {G : RealDyadicGrid} (Q : ℤ × ℤ) (C : Finset (ℤ × ℤ)) (hC : ∀ c ∈ C, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G Q.1 Q.2) {K : ℕ} (hK : 1 ≤ K) (hdepth : ∀ c ∈ C, c.1 < Q.1 + ↑K) : ShortBlockTree G K

Blueprint lines 2433-2437 ("complete pieces by children immediately below their included cells, including missing branches ... each piece has at most K internal depths and leaves at most one step below"): a root Q with summation cells C inside it, at most K depths below, forms a short-block tree.

Equations

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

theorem TrilinearHT.Auto.pieceTree_internal_sup {G : RealDyadicGrid} {Q : ℤ × ℤ} {C : Finset (ℤ × ℤ)} (hC : ∀ c ∈ C, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G Q.1 Q.2) {K : ℕ} (hK : 1 ≤ K) (hdepth : ∀ c ∈ C, c.1 < Q.1 + ↑K) : C ⊆ (pieceTree Q C hC hK hdepth).internal

theorem TrilinearHT.Auto.child_lintegral_le (G : RealDyadicGrid) {p L : ℤ × ℤ} (hL : L ∈ dyadicChildren G p) (g : ℝ → ENNReal) : ∫⁻ (x : ℝ) in dyadicGridCell G L.1 L.2, g x ≤ 2 * ENNReal.ofReal (dyadicGridLength G L.1) * dyadicEnergyAverage G g p

Blueprint line 2436 ("a child's squared average is at most twice its parent's"): ∫_L g ≤ 2 |L| ⨍_p g for a child L of p.

theorem TrilinearHT.Auto.power_min_sum_le (Gd : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (root : ℤ × ℤ) (hroot : ∀ I ∈ S, dyadicGridCell Gd I.1 I.2 ⊆ dyadicGridCell Gd root.1 root.2) (x u : ℤ × ℤ → ℝ) (hx : ∀ I ∈ S, 0 ≤ x I) (hu : ∀ (I : ℤ × ℤ), 0 ≤ u I) {K T : ℝ} (hK : 0 ≤ K) (hxu : ∀ I ∈ S, x I ≤ K * (u I * √(u I))) (hT : ∀ (y : ℝ), ∑ I ∈ S with y ∈ dyadicGridCell Gd I.1 I.2, u I ≤ T) {η p : ℝ} (hη : 0 ≤ η) (hp : 2 / 3 < p) (hp1 : p ≤ 1) : ∑ I ∈ S, dyadicGridLength Gd I.1 * min η (x I) ≤ η ^ (1 - p) * K ^ p * (T ^ (p / 2) * T ^ (p / 2) * T ^ (p / 2) * dyadicGridLength Gd root.1)

Blueprint eq:min-power with eq:three-sides integrated over paths: cell quantities bounded by K u_I √u_I, where the weights u_I have path sums at most T, contribute to the active minimum at most η^{1-p} K^p T^{3p/2} |R|.

theorem TrilinearHT.Auto.sign_select_two {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [DecidableEq κ] (s : Finset ι) (t : Finset κ) {a i : ι} {b j : κ} (ha : a ∈ s) (hi : i ∈ s) (hb : b ∈ t) (hj : j ∈ t) : (2 ^ s.card)⁻¹ * ∑ u ∈ s.powerset, (2 ^ t.card)⁻¹ * ∑ v ∈ t.powerset, patternSign u a * patternSign v b * (patternSign u i * patternSign v j) = if a = i ∧ b = j then 1 else 0

The double sign selection: averaging ε_a η_b ε_i η_j over two independent sign families gives δ_{ai} δ_{bj}.

theorem TrilinearHT.Auto.rademacherSum_complex {ι : Type u_1} [DecidableEq ι] (s u : Finset ι) (v : ι → ℂ) : rademacherSum s u v = ∑ i ∈ s, ↑(patternSign u i) * v i

theorem TrilinearHT.Auto.dyadicRootLength_eq_volume (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (hS : (↑S).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2) : dyadicRootLength G S = (MeasureTheory.volume (⋃ c ∈ S, dyadicGridCell G c.1 c.2)).toReal

The total length of a pairwise disjoint finite family of dyadic cells is the measure of their union.

noncomputable def TrilinearHT.Auto.sparseStops (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (ga gb : ℝ → ENNReal) (Q : ℤ × ℤ) : Finset (ℤ × ℤ)

The stopping cells below a root Q (blueprint lines 2430-2431): the maximal cells of the hull strictly below Q where either squared stack average exceeds sixteen times its value at Q.

Equations

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

theorem TrilinearHT.Auto.sparseStops_sub (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (ga gb : ℝ → ENNReal) (Q : ℤ × ℤ) {c : ℤ × ℤ} (hc : c ∈ sparseStops G H ga gb Q) : c ∈ H ∧ dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G Q.1 Q.2 ∧ c ≠ Q ∧ (16 * dyadicEnergyAverage G ga Q < dyadicEnergyAverage G ga c ∨ 16 * dyadicEnergyAverage G gb Q < dyadicEnergyAverage G gb c)

theorem TrilinearHT.Auto.sparseStops_depth (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (ga gb : ℝ → ENNReal) (Q : ℤ × ℤ) {c : ℤ × ℤ} (hc : c ∈ sparseStops G H ga gb Q) : Q.1 < c.1

theorem TrilinearHT.Auto.sparseStops_disjoint (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (ga gb : ℝ → ENNReal) (Q : ℤ × ℤ) : (↑(sparseStops G H ga gb Q)).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2

theorem TrilinearHT.Auto.sparseStops_length_le (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (ga gb : ℝ → ENNReal) (Q : ℤ × ℤ) : dyadicRootLength G (sparseStops G H ga gb Q) ≤ dyadicGridLength G Q.1 / 8

Blueprint line 2431: the stopping cells of a root have total length at most |Q|/8.

noncomputable def TrilinearHT.Auto.sparseGen (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (ga gb : ℝ → ENNReal) (Q₀ : ℤ × ℤ) : ℕ → Finset (ℤ × ℤ)

The generations of the sparse decomposition of a root Q₀.

Equations

• TrilinearHT.Auto.sparseGen G H ga gb Q₀ 0 = {Q₀}
• TrilinearHT.Auto.sparseGen G H ga gb Q₀ k.succ = (TrilinearHT.Auto.sparseGen G H ga gb Q₀ k).biUnion (TrilinearHT.Auto.sparseStops G H ga gb)

theorem TrilinearHT.Auto.sparseGen_sub (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (ga gb : ℝ → ENNReal) (Q₀ : ℤ × ℤ) (k : ℕ) (Q : ℤ × ℤ) : Q ∈ sparseGen G H ga gb Q₀ k → dyadicGridCell G Q.1 Q.2 ⊆ dyadicGridCell G Q₀.1 Q₀.2 ∧ Q₀.1 + ↑k ≤ Q.1

theorem TrilinearHT.Auto.sparseGen_disjoint (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (ga gb : ℝ → ENNReal) (Q₀ : ℤ × ℤ) (k : ℕ) : (↑(sparseGen G H ga gb Q₀ k)).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2

The cells of one generation are pairwise disjoint.

theorem TrilinearHT.Auto.sparseGen_later (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (ga gb : ℝ → ENNReal) (Q₀ : ℤ × ℤ) (j k : ℕ) : j < k → ∀ Q ∈ sparseGen G H ga gb Q₀ k, ∀ Q' ∈ sparseGen G H ga gb Q₀ j, (∃ c ∈ sparseStops G H ga gb Q', dyadicGridCell G Q.1 Q.2 ⊆ dyadicGridCell G c.1 c.2) ∨ Disjoint (dyadicGridCell G Q.1 Q.2) (dyadicGridCell G Q'.1 Q'.2)

A root of a later generation lies in a stopping cell of the unique root of an earlier generation containing it, and is disjoint from the other roots of that generation.

noncomputable def TrilinearHT.Auto.sparseRoots (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (ga gb : ℝ → ENNReal) (Q₀ : ℤ × ℤ) (D : ℕ) : Finset (ℤ × ℤ)

The roots of the sparse decomposition of Q₀ up to D generations.

Equations

• TrilinearHT.Auto.sparseRoots G H ga gb Q₀ D = (Finset.range (D + 1)).biUnion (TrilinearHT.Auto.sparseGen G H ga gb Q₀)

noncomputable def TrilinearHT.Auto.sparseRem (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (ga gb : ℝ → ENNReal) (Q : ℤ × ℤ) : Set ℝ

The remainder of a root: the root minus its stopping cells.

Equations

• TrilinearHT.Auto.sparseRem G H ga gb Q = TrilinearHT.Auto.dyadicGridCell G Q.1 Q.2 \ ⋃ c ∈ TrilinearHT.Auto.sparseStops G H ga gb Q, TrilinearHT.Auto.dyadicGridCell G c.1 c.2

theorem TrilinearHT.Auto.sparseRem_measurable (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (ga gb : ℝ → ENNReal) (Q : ℤ × ℤ) : MeasurableSet (sparseRem G H ga gb Q)

theorem TrilinearHT.Auto.sparseRem_sub (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (ga gb : ℝ → ENNReal) (Q : ℤ × ℤ) : sparseRem G H ga gb Q ⊆ dyadicGridCell G Q.1 Q.2

theorem TrilinearHT.Auto.sparseRem_volume (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (ga gb : ℝ → ENNReal) (Q : ℤ × ℤ) : 7 * ENNReal.ofReal (dyadicGridLength G Q.1) ≤ 8 * MeasureTheory.volume (sparseRem G H ga gb Q)

Blueprint line 2431: the remainder has measure at least 7|Q|/8.

theorem TrilinearHT.Auto.sparseRem_disjoint (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (ga gb : ℝ → ENNReal) (Q₀ : ℤ × ℤ) (D : ℕ) : (↑(sparseRoots G H ga gb Q₀ D)).PairwiseDisjoint (sparseRem G H ga gb)

Distinct roots have disjoint remainders.

theorem TrilinearHT.Auto.sparse_owner (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (ga gb : ℝ → ENNReal) (Q₀ : ℤ × ℤ) (D : ℕ) {c : ℤ × ℤ} (hcH : c ∈ H) (hcQ : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G Q₀.1 Q₀.2) (hcD : c.1 ≤ Q₀.1 + ↑D) : ∃ Q ∈ sparseRoots G H ga gb Q₀ D, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G Q.1 Q.2 ∧ (∀ s ∈ sparseStops G H ga gb Q, ¬dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G s.1 s.2) ∧ dyadicEnergyAverage G ga c ≤ 16 * dyadicEnergyAverage G ga Q ∧ dyadicEnergyAverage G gb c ≤ 16 * dyadicEnergyAverage G gb Q

Blueprint line 2432 ("a child's squared average is at most twice its parent's; hence side leaf norms are bounded multiples of the root sizes"): every hull cell below Q₀ within D depths is owned by a root containing it but no stopping cell of it, where both stack averages are at most sixteen times those of the root.

theorem TrilinearHT.Auto.piece_internal_avg_le (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (ga gb : ℝ → ENNReal) (Q : ℤ × ℤ) (C : Finset (ℤ × ℤ)) (hC : ∀ c ∈ C, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G Q.1 Q.2) (hown : ∀ c ∈ C, ∀ s ∈ sparseStops G H ga gb Q, ¬dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G s.1 s.2) (hhull : ∀ c ∈ C, ∀ (d : ℤ × ℤ), dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2 → dyadicGridCell G d.1 d.2 ⊆ dyadicGridCell G Q.1 Q.2 → d ∈ H) {d : ℤ × ℤ} (hd : d ∈ pieceInternal G Q C) : dyadicEnergyAverage G ga d ≤ 16 * dyadicEnergyAverage G ga Q ∧ dyadicEnergyAverage G gb d ≤ 16 * dyadicEnergyAverage G gb Q

Blueprint lines 2432-2435: on the internal cells of the piece of a sparse root (the owned cells and their ancestors below the root, all in the hull), both stack averages are at most sixteen times those of the root.

theorem TrilinearHT.Auto.piece_leaf_energy (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (ga gb : ℝ → ENNReal) (Q : ℤ × ℤ) (C : Finset (ℤ × ℤ)) (hC : ∀ c ∈ C, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G Q.1 Q.2) (hown : ∀ c ∈ C, ∀ s ∈ sparseStops G H ga gb Q, ¬dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G s.1 s.2) (hhull : ∀ c ∈ C, ∀ (d : ℤ × ℤ), dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2 → dyadicGridCell G d.1 d.2 ⊆ dyadicGridCell G Q.1 Q.2 → d ∈ H) {L : ℤ × ℤ} (hL : L ∈ pieceLeaves G Q C) : ∫⁻ (x : ℝ) in dyadicGridCell G L.1 L.2, ga x ≤ 32 * ENNReal.ofReal (dyadicGridLength G L.1) * dyadicEnergyAverage G ga Q ∧ ∫⁻ (x : ℝ) in dyadicGridCell G L.1 L.2, gb x ≤ 32 * ENNReal.ofReal (dyadicGridLength G L.1) * dyadicEnergyAverage G gb Q

Blueprint line 2436: the leaves of the piece of a sparse root carry stack energy at most 32 |L| times the root average.

theorem TrilinearHT.Auto.khintchine_four {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (a : ι → ℂ) : (rademacherMean s fun (u : Finset ι) => ‖rademacherSum s u a‖ ^ 4) ≤ 256 * (∑ i ∈ s, ‖a i‖ ^ 2) ^ 2

Khintchine at the fourth moment: E|Σ ε_i a_i|⁴ ≤ 256 (Σ |a_i|²)².

theorem TrilinearHT.Auto.rademacherMean_sum_sq_le {κ : Type u_1} {ι : Type u_2} (u : Finset κ) (s : Finset ι) (g : ι → Finset κ → ℝ) : (rademacherMean u fun (w : Finset κ) => (∑ i ∈ s, g i w) ^ 2) ≤ (∑ i ∈ s, √(rademacherMean u fun (w : Finset κ) => g i w ^ 2)) ^ 2

Minkowski for nonnegative finite sums in L² of a finite average: E (Σ_i g_i)² ≤ (Σ_i (E g_i²)^{1/2})².

theorem TrilinearHT.Auto.double_khintchine {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [DecidableEq κ] (s : Finset ι) (u : Finset κ) (x : ι → κ → ℂ) : (rademacherMean u fun (w : Finset κ) => rademacherMean s fun (v : Finset ι) => ‖∑ i ∈ s, ∑ p ∈ u, ↑(patternSign v i) * ↑(patternSign w p) * x i p‖ ^ 4) ≤ 16 ^ 4 * (∑ i ∈ s, ∑ p ∈ u, ‖x i p‖ ^ 2) ^ 2

Blueprint lines 2421-2423 ("two applications of Khintchine give the pointwise moment hypothesis"): the product chaos Σ_{i,p} ε_i ζ_p x_{ip} has fourth moment at most 16⁴ (Σ |x_{ip}|²)².

theorem TrilinearHT.Auto.avg_three_families {ι : Type u_1} {κ : Type u_2} {ν : Type u_3} {M : Type u_4} [AddCommGroup M] [Module ℂ M] (s : Finset ι) (t : Finset κ) (u : Finset ν) (g : Finset ι → Finset κ → Finset ν → M) : (↑(Fintype.card (SignPattern s × SignPattern t × SignPattern u)))⁻¹ • ∑ ω : SignPattern s × SignPattern t × SignPattern u, g ↑ω.1 ↑ω.2.1 ↑ω.2.2 = (2 ^ s.card)⁻¹ • ∑ v₁ ∈ s.powerset, (2 ^ t.card)⁻¹ • ∑ v₂ ∈ t.powerset, (2 ^ u.card)⁻¹ • ∑ v₃ ∈ u.powerset, g v₁ v₂ v₃

The uniform average over three sign families as a nested average.

theorem TrilinearHT.Auto.sign_select_three {ι : Type u_1} {κ : Type u_2} {ν : Type u_3} [DecidableEq ι] [DecidableEq κ] [DecidableEq ν] (s : Finset ι) (t : Finset κ) (u : Finset ν) {i₀ i : ι} {j₀ j : κ} {p p' : ν} (hi₀ : i₀ ∈ s) (hi : i ∈ s) (hj₀ : j₀ ∈ t) (hj : j ∈ t) (hp : p ∈ u) (hp' : p' ∈ u) : (2 ^ s.card)⁻¹ * ∑ v₁ ∈ s.powerset, (2 ^ t.card)⁻¹ * ∑ v₂ ∈ t.powerset, (2 ^ u.card)⁻¹ * ∑ v₃ ∈ u.powerset, patternSign v₁ i₀ * patternSign v₂ j₀ * (patternSign v₁ i * patternSign v₂ j * (patternSign v₃ p * patternSign v₃ p')) = if i₀ = i ∧ j₀ = j ∧ p = p' then 1 else 0

The triple sign selection: averaging ε_{i₀} η_{j₀} ε_i η_j ζ_p ζ_{p'} over three independent families gives δ_{i₀ i} δ_{j₀ j} δ_{p p'}.

theorem TrilinearHT.Auto.avg_three_families_real {ι : Type u_1} {κ : Type u_2} {ν : Type u_3} (s : Finset ι) (t : Finset κ) (u : Finset ν) (g : Finset ι → Finset κ → Finset ν → ℝ) : (↑(Fintype.card (SignPattern s × SignPattern t × SignPattern u)))⁻¹ * ∑ ω : SignPattern s × SignPattern t × SignPattern u, g ↑ω.1 ↑ω.2.1 ↑ω.2.2 = (2 ^ s.card)⁻¹ * ∑ v₁ ∈ s.powerset, (2 ^ t.card)⁻¹ * ∑ v₂ ∈ t.powerset, (2 ^ u.card)⁻¹ * ∑ v₃ ∈ u.powerset, g v₁ v₂ v₃

The uniform average over three sign families as a nested average (real values).

theorem TrilinearHT.Auto.enorm_avg_rpow {Ω : Type u_4} [Fintype Ω] [Nonempty Ω] (g : Ω → ℂ) : ((↑(Fintype.card Ω))⁻¹ * ∑ ω : Ω, ‖g ω‖ₑ ^ 4) ^ (1 / 4) = ENNReal.ofReal (((↑(Fintype.card Ω))⁻¹ * ∑ ω : Ω, ‖g ω‖ ^ 4) ^ (1 / 4))

The fourth moment of an average of norms in ℝ≥0∞ is that of the real average.

theorem TrilinearHT.Auto.root4_le {A c S : ℝ} (hA : 0 ≤ A) (hc : 0 ≤ c) (hS : 0 ≤ S) (h : A ≤ c ^ 4 * S ^ 2) : A ^ (1 / 4) ≤ c * √S

instance TrilinearHT.Auto.signPattern_nonempty {α : Type u_4} (s : Finset α) : Nonempty (SignPattern s)

theorem TrilinearHT.Auto.moment_three_a {ι : Type u_1} {κ : Type u_2} {ν : Type u_3} [DecidableEq ι] [DecidableEq ν] (s : Finset ι) (t : Finset κ) (u : Finset ν) (x : ι → ν → ℂ) : ((↑(Fintype.card (SignPattern s × SignPattern t × SignPattern u)))⁻¹ * ∑ ω : SignPattern s × SignPattern t × SignPattern u, ‖∑ i ∈ s, ∑ p ∈ u, ↑(patternSign (↑ω.1) i) * ↑(patternSign (↑ω.2.2) p) * x i p‖ₑ ^ 4) ^ (1 / 4) ≤ ENNReal.ofReal 16 * ENNReal.ofReal √(∑ i ∈ s, ∑ p ∈ u, ‖x i p‖ ^ 2)

The moment of the side slot Σ_{i,p} ε_i ζ_p x_{ip} on three families.

noncomputable def TrilinearHT.Auto.randTuple3 {ι : Type u_1} {κ : Type u_2} {ν : Type u_3} [DecidableEq ι] [DecidableEq κ] [DecidableEq ν] (a b c : Fin 4) (f : Fin 4 → ℝ → ℂ) (s : Finset ι) (t : Finset κ) (u : Finset ν) (x : ι → ν → ℝ → ℂ) (w : κ → ℝ → ℂ) (y : ν → ℝ → ℂ) (v₁ : Finset ι) (v₂ : Finset κ) (v₃ : Finset ν) : Fin 4 → ℝ → ℂ

The randomized tuple of a band defect: slot a carries Σ_{i,p} ε_i ζ_p x_{ip}, slot b carries Σ_j η_j w_j, slot c carries Σ_p ζ_p y_p.

Equations

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

theorem TrilinearHT.Auto.update_measurable_fin {f : Fin 4 → ℝ → ℂ} (hf : ∀ (j : Fin 4), Measurable (f j)) (k : Fin 4) {g : ℝ → ℂ} (hg : Measurable g) (j : Fin 4) : Measurable (Function.update f k g j)

theorem TrilinearHT.Auto.update_fin_fin {μ : MeasureTheory.Measure ℝ} {f : Fin 4 → ℝ → ℂ} (hf : ∀ (j : Fin 4), MeasureTheory.eLpNorm (f j) 2 μ ≠ ⊤) (k : Fin 4) {g : ℝ → ℂ} (hg : MeasureTheory.eLpNorm g 2 μ ≠ ⊤) (j : Fin 4) : MeasureTheory.eLpNorm (Function.update f k g j) 2 μ ≠ ⊤

theorem TrilinearHT.Auto.sum_eLpNorm_ne_top {μ : MeasureTheory.Measure ℝ} {α : Type u_4} (s : Finset α) (c : α → ℂ) (g : α → ℝ → ℂ) (hg : ∀ (i : α), MeasureTheory.eLpNorm (g i) 2 μ ≠ ⊤) : MeasureTheory.eLpNorm (fun (z : ℝ) => ∑ i ∈ s, c i * g i z) 2 μ ≠ ⊤

theorem TrilinearHT.Auto.sum_swap_three_four {ι : Type u_1} {κ : Type u_2} {ν : Type u_3} {A : Type u_4} {B : Type u_5} {C : Type u_6} (VA : Finset A) (VB : Finset B) (VC : Finset C) (s : Finset ι) (u : Finset ν) (t : Finset κ) (g : A → B → C → ι → ν → κ → ν → ℂ) : ∑ a ∈ VA, ∑ b ∈ VB, ∑ c ∈ VC, ∑ i ∈ s, ∑ p ∈ u, ∑ j ∈ t, ∑ p' ∈ u, g a b c i p j p' = ∑ i ∈ s, ∑ p ∈ u, ∑ j ∈ t, ∑ p' ∈ u, ∑ a ∈ VA, ∑ b ∈ VB, ∑ c ∈ VC, g a b c i p j p'

Interchanging three outer sums with four inner sums.

theorem TrilinearHT.Auto.form_sign_avg3 {ι : Type u_1} {κ : Type u_2} {ν : Type u_3} [DecidableEq ι] [DecidableEq κ] [DecidableEq ν] {κ' : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w₀ : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ' a₀ r w₀) {a b c : Fin 4} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (f : Fin 4 → ℝ → ℂ) (hf : ∀ (j : Fin 4), Measurable (f j)) (hfin : ∀ (j : Fin 4), MeasureTheory.eLpNorm (f j) 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (s : Finset ι) (t : Finset κ) (u : Finset ν) (x : ι → ν → ℝ → ℂ) (w : κ → ℝ → ℂ) (y : ν → ℝ → ℂ) (hx : ∀ (i : ι) (p : ν), Measurable (x i p)) (hxf : ∀ (i : ι) (p : ν), MeasureTheory.eLpNorm (x i p) 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hwm : ∀ (j : κ), Measurable (w j)) (hwf : ∀ (j : κ), MeasureTheory.eLpNorm (w j) 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hym : ∀ (p : ν), Measurable (y p)) (hyf : ∀ (p : ν), MeasureTheory.eLpNorm (y p) 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) {i₀ : ι} {j₀ : κ} (hi₀ : i₀ ∈ s) (hj₀ : j₀ ∈ t) : (2 ^ s.card)⁻¹ * ∑ v₁ ∈ s.powerset, (2 ^ t.card)⁻¹ * ∑ v₂ ∈ t.powerset, (2 ^ u.card)⁻¹ * ∑ v₃ ∈ u.powerset, ↑(patternSign v₁ i₀) * ↑(patternSign v₂ j₀) * localProgressionForm r w₀ (randTuple3 a b c f s t u x w y v₁ v₂ v₃) = ∑ p ∈ u, localProgressionForm r w₀ (Function.update (Function.update (Function.update f a (x i₀ p)) b (w j₀)) c (y p))

Blueprint lines 2421-2423 with the band family: averaging ε_{i₀} η_{j₀} times the form of the randomized band tuple over three independent sign families gives the matched band sum Σ_p H(x_{i₀ p}, w_{j₀}, y_p).

theorem TrilinearHT.Auto.moment_three_b {ι : Type u_1} {κ : Type u_2} {ν : Type u_3} [DecidableEq κ] (s : Finset ι) (t : Finset κ) (u : Finset ν) (w : κ → ℂ) : ((↑(Fintype.card (SignPattern s × SignPattern t × SignPattern u)))⁻¹ * ∑ ω : SignPattern s × SignPattern t × SignPattern u, ‖∑ j ∈ t, ↑(patternSign (↑ω.2.1) j) * w j‖ₑ ^ 4) ^ (1 / 4) ≤ ENNReal.ofReal 16 * ENNReal.ofReal √(∑ j ∈ t, ‖w j‖ ^ 2)

The moment of the slot Σ_j η_j w_j on three families.

theorem TrilinearHT.Auto.moment_three_c {ι : Type u_1} {κ : Type u_2} {ν : Type u_3} [DecidableEq ν] (s : Finset ι) (t : Finset κ) (u : Finset ν) (y : ν → ℂ) : ((↑(Fintype.card (SignPattern s × SignPattern t × SignPattern u)))⁻¹ * ∑ ω : SignPattern s × SignPattern t × SignPattern u, ‖∑ p ∈ u, ↑(patternSign (↑ω.2.2) p) * y p‖ₑ ^ 4) ^ (1 / 4) ≤ ENNReal.ofReal 16 * ENNReal.ofReal √(∑ p ∈ u, ‖y p‖ ^ 2)

The moment of the band slot Σ_p ζ_p y_p on three families.

theorem TrilinearHT.Auto.piece_band_bound (κ : LocalKernelClass) {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) : ∃ (Cq : ℝ), 0 ≤ Cq ∧ ∀ (G : RealDyadicGrid) (K Nd : ℕ) (d₀ : ℤ) (T : ShortBlockTree G K) {ι κ' ν : Type} [DecidableEq ι] [DecidableEq κ'] [DecidableEq ν] (s : Finset ι) (t : Finset κ') (u : Finset ν) {a b c : Fin 4}, a ≠ b → a ≠ c → b ≠ c → ∀ (f : Fin 4 → ℝ → ℂ) (x : ι → ν → ℝ → ℂ) (w : κ' → ℝ → ℂ) (y : ν → ℝ → ℂ), (∀ (j : Fin 4), Measurable (f j)) → (∀ (i : ι) (p : ν), Measurable (x i p)) → (∀ (k : κ'), Measurable (w k)) → (∀ (p : ν), Measurable (y p)) → ∀ (kernel : ℤ × ℤ → ℝ × ℝ → ℂ), (∀ I ∈ T.internal, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (kernel I)) → ∀ cells ⊆ T.internal, (∀ I ∈ cells, kernel I ≠ 0 → d₀ ≤ I.1 ∧ I.1 < d₀ + ↑Nd) → (∀ I ∈ cells, ∀ (j : Fin 4), MeasureTheory.eLpNorm (f j) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≠ ⊤) → (∀ I ∈ cells, ∀ (i : ι) (p : ν), MeasureTheory.eLpNorm (x i p) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≠ ⊤) → (∀ I ∈ cells, ∀ (k : κ'), MeasureTheory.eLpNorm (w k) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≠ ⊤) → (∀ I ∈ cells, ∀ (p : ν), MeasureTheory.eLpNorm (y p) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≠ ⊤) → ∀ (sv : Fin 4 → ℝ), (∀ (j : Fin 4), 0 ≤ sv j) → (∀ L ∈ T.leaves, ∫⁻ (z : ℝ) in dyadicGridCell G L.1 L.2, ENNReal.ofReal (∑ i ∈ s, ∑ p ∈ u, ‖x i p z‖ ^ 2) ≤ ENNReal.ofReal (sv a ^ 2 * dyadicGridLength G L.1)) → (∀ L ∈ T.leaves, ∫⁻ (z : ℝ) in dyadicGridCell G L.1 L.2, ENNReal.ofReal (∑ k ∈ t, ‖w k z‖ ^ 2) ≤ ENNReal.ofReal (sv b ^ 2 * dyadicGridLength G L.1)) → (∀ L ∈ T.leaves, ∫⁻ (z : ℝ) in dyadicGridCell G L.1 L.2, ENNReal.ofReal (∑ p ∈ u, ‖y p z‖ ^ 2) ≤ ENNReal.ofReal (sv c ^ 2 * dyadicGridLength G L.1)) → (∀ (j : Fin 4), j ≠ a → j ≠ b → j ≠ c → ∀ L ∈ T.leaves, ∫⁻ (z : ℝ) in dyadicGridCell G L.1 L.2, ‖f j z‖ₑ ^ 2 ≤ ENNReal.ofReal (sv j ^ 2 * dyadicGridLength G L.1)) → ∀ (sa : ℤ × ℤ → ι) (sb : ℤ × ℤ → κ'), (∀ I ∈ cells, sa I ∈ s) → (∀ I ∈ cells, sb I ∈ t) → ∀ (sg : ℤ × ℤ → ℂ), (∀ (I : ℤ × ℤ), ‖sg I‖ ≤ 1) → ‖∑ I ∈ cells, ↑(dyadicGridLength G I.1) * (sg I * ⋯)‖ ≤ Cq * (1 + finiteDepthConstant κ q Nd) * (1 + Real.log (↑K + 2)) * (↑K + 2) ^ (2 * (q - 2) / (q - 1)) * dyadicGridLength G T.root.1 * ∏ j : Fin 4, sv j

Blueprint lines 2421-2445 (eq:near-band on one short-block piece): with the first side stack indexed by positions and bands, the second side stack by positions and the complementary band stack by bands, the cell sum of the matched band forms (positions selected at each use, arbitrary signs) is bounded by the short-block constant times the stack sizes.

theorem TrilinearHT.Auto.prod_fin4_slots {a b c : Fin 4} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (α β γ δ : ℝ) : (∏ j : Fin 4, if j = a then α else if j = b then β else if j = c then γ else δ) = α * β * γ * δ

theorem TrilinearHT.Auto.avg_sqrt_eq {A : ENNReal} (hA : A ≠ ⊤) : A ^ (1 / 2) = ENNReal.ofReal √A.toReal

theorem TrilinearHT.Auto.child_lintegral_le_sq (G : RealDyadicGrid) {p L : ℤ × ℤ} (hL : L ∈ dyadicChildren G p) (g : ℝ → ENNReal) {B : ℝ} (hB : dyadicEnergyAverage G g p ≤ ENNReal.ofReal (B ^ 2)) : ∫⁻ (x : ℝ) in dyadicGridCell G L.1 L.2, g x ≤ ENNReal.ofReal ((√2 * B) ^ 2 * dyadicGridLength G L.1)

∫_L g ≤ 2 |L| B² for a child L of a cell p on which g has average at most B².

theorem TrilinearHT.Auto.sparse_piece_bound (κ : LocalKernelClass) {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) : ∃ (Cq : ℝ), 0 ≤ Cq ∧ ∀ (G : RealDyadicGrid) (K Nd : ℕ) (d₀ : ℤ), 1 ≤ K → ∀ (H : Finset (ℤ × ℤ)) (Q : ℤ × ℤ) (C : Finset (ℤ × ℤ)), (∀ c ∈ C, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G Q.1 Q.2) → (∀ c ∈ C, c.1 < Q.1 + ↑K) → ∀ {ι κ' ν : Type} [DecidableEq ι] [DecidableEq κ'] [DecidableEq ν] (s : Finset ι) (t : Finset κ') (u : Finset ν) {a b c : Fin 4}, a ≠ b → a ≠ c → b ≠ c → ∀ (f : Fin 4 → ℝ → ℂ) (x : ι → ν → ℝ → ℂ) (w : κ' → ℝ → ℂ) (y : ν → ℝ → ℂ), (∀ (j : Fin 4), Measurable (f j)) → (∀ (i : ι) (p : ν), Measurable (x i p)) → (∀ (k : κ'), Measurable (w k)) → (∀ (p : ν), Measurable (y p)) → (∀ c' ∈ C, ∀ s' ∈ sparseStops G H (fun (z : ℝ) => ENNReal.ofReal (∑ i ∈ s, ∑ p ∈ u, ‖x i p z‖ ^ 2)) (fun (z : ℝ) => ENNReal.ofReal (∑ k ∈ t, ‖w k z‖ ^ 2)) Q, ¬dyadicGridCell G c'.1 c'.2 ⊆ dyadicGridCell G s'.1 s'.2) → (∀ c' ∈ C, ∀ (d : ℤ × ℤ), dyadicGridCell G c'.1 c'.2 ⊆ dyadicGridCell G d.1 d.2 → dyadicGridCell G d.1 d.2 ⊆ dyadicGridCell G Q.1 Q.2 → d ∈ H) → dyadicEnergyAverage G (fun (z : ℝ) => ENNReal.ofReal (∑ i ∈ s, ∑ p ∈ u, ‖x i p z‖ ^ 2)) Q ≠ ⊤ → dyadicEnergyAverage G (fun (z : ℝ) => ENNReal.ofReal (∑ k ∈ t, ‖w k z‖ ^ 2)) Q ≠ ⊤ → ∀ (kernel : ℤ × ℤ → ℝ × ℝ → ℂ), (∀ I ∈ pieceInternal G Q C, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (kernel I)) → (∀ I ∈ C, kernel I ≠ 0 → d₀ ≤ I.1 ∧ I.1 < d₀ + ↑Nd) → (∀ I ∈ C, ∀ (j : Fin 4), MeasureTheory.eLpNorm (f j) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≠ ⊤) → (∀ I ∈ C, ∀ (i : ι) (p : ν), MeasureTheory.eLpNorm (x i p) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≠ ⊤) → (∀ I ∈ C, ∀ (k : κ'), MeasureTheory.eLpNorm (w k) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≠ ⊤) → (∀ I ∈ C, ∀ (p : ν), MeasureTheory.eLpNorm (y p) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≠ ⊤) → ∀ {Bc Bd : ℝ}, 0 ≤ Bc → 0 ≤ Bd → (∀ d ∈ pieceInternal G Q C, dyadicEnergyAverage G (fun (z : ℝ) => ENNReal.ofReal (∑ p ∈ u, ‖y p z‖ ^ 2)) d ≤ ENNReal.ofReal (Bc ^ 2)) → (∀ (j : Fin 4), j ≠ a → j ≠ b → j ≠ c → ∀ (d : ℤ × ℤ), ⋯) → ∀ (sa : ℤ × ℤ → ι) (sb : ℤ × ℤ → κ'), (∀ I ∈ C, sa I ∈ s) → (∀ I ∈ C, sb I ∈ t) → ∀ (sg : ℤ × ℤ → ℂ), ⋯

Blueprint lines 2432-2437 (lem:shortblock on one sparse piece): for a sparse root Q of the two side stacks g_a = Σ_{i,p} |x_{ip}|², g_b = Σ_k |w_k|² and summation cells C owned by Q, with the frozen complementary stack and the remaining input of averages at most B_c², B_d² on the internal cells, the selected matched band forms over C (arbitrary signs) are at most a short-block constant times |Q| a_Q b_Q B_c B_d.

theorem TrilinearHT.Auto.sparseRoots_sub (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (ga gb : ℝ → ENNReal) (Q₀ : ℤ × ℤ) (hQ₀ : Q₀ ∈ H) (D : ℕ) {Q : ℤ × ℤ} (hQ : Q ∈ sparseRoots G H ga gb Q₀ D) : Q ∈ H ∧ dyadicGridCell G Q.1 Q.2 ⊆ dyadicGridCell G Q₀.1 Q₀.2

The roots of the sparse decomposition lie in the hull and below the initial root.

def TrilinearHT.Auto.SparseOwner (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (ga gb : ℝ → ENNReal) (Rt : Finset (ℤ × ℤ)) (K : ℕ) (c Q : ℤ × ℤ) : Prop

The owner property of a use cell c: a sparse root Q of one of the hull roots r ∈ Rt containing c but no stopping cell of Q containing c.

Equations

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

theorem TrilinearHT.Auto.sparse_root_sum (G : RealDyadicGrid) {N : Type u_1} (Ns : Finset N) (K : ℕ) (H Rt U : N → Finset (ℤ × ℤ)) (ga gb : N → ℝ → ENNReal) {R : Set ℝ} (hRm : MeasurableSet R) (hRtH : ∀ ν ∈ Ns, Rt ν ⊆ H ν) (hRtdis : ∀ ν ∈ Ns, (↑(Rt ν)).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2) (hRtR : ∀ ν ∈ Ns, ∀ r ∈ Rt ν, dyadicGridCell G r.1 r.2 ⊆ R) (hUH : ∀ ν ∈ Ns, U ν ⊆ H ν) (hUr : ∀ ν ∈ Ns, ∀ c ∈ U ν, ∃ r ∈ Rt ν, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G r.1 r.2) (hdep : ∀ ν ∈ Ns, ∀ c ∈ U ν, ∀ r ∈ Rt ν, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G r.1 r.2 → c.1 < r.1 + ↑K) (hclos : ∀ ν ∈ Ns, ∀ c ∈ U ν, ∀ r ∈ Rt ν, ∀ (d : ℤ × ℤ), dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2 → dyadicGridCell G d.1 d.2 ⊆ dyadicGridCell G r.1 r.2 → d ∈ H ν) {A B : ENNReal} (hA : ∀ x ∈ R, ∑ ν ∈ Ns, dyadicHullMax G (H ν) (ga ν) x ≤ A) (hB : ∀ x ∈ R, ∑ ν ∈ Ns, dyadicHullMax G (H ν) (gb ν) x ≤ B) (F : N → ℤ × ℤ → ℂ) (c₀ : ENNReal) (hpiece : ∀ ν ∈ Ns, ∀ (Q : ℤ × ℤ) (C : Finset (ℤ × ℤ)), Q ∈ H ν → C ⊆ U ν → (∀ c ∈ C, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G Q.1 Q.2) → (∀ c ∈ C, c.1 < Q.1 + ↑K) → (∀ c ∈ C, ∀ s ∈ sparseStops G (H ν) (ga ν) (gb ν) Q, ¬dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G s.1 s.2) → (∀ c ∈ C, ∀ (d : ℤ × ℤ), dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2 → dyadicGridCell G d.1 d.2 ⊆ dyadicGridCell G Q.1 Q.2 → d ∈ H ν) → ‖∑ I ∈ C, F ν I‖ₑ ≤ c₀ * (ENNReal.ofReal (dyadicGridLength G Q.1) * (dyadicEnergyAverage G (ga ν) Q ^ (1 / 2) * dyadicEnergyAverage G (gb ν) Q ^ (1 / 2)))) : 7 * ∑ ν ∈ Ns, ‖∑ I ∈ U ν, F ν I‖ₑ ≤ 8 * c₀ * ((A * B) ^ (1 / 2) * MeasureTheory.volume R)

Blueprint lines 2430-2445 (summation of the sparse pieces, eq:near-band): for each index ν with retained hull H_ν, disjoint hull roots Rt_ν ⊆ H_ν inside R, and use cells U_ν within K depths of their root, decompose each root sparsely for the two stack energies and assign each use to its owning sparse root. If every piece (owned summation cells of one sparse root) contributes at most c₀ |Q| a_Q b_Q, then the total of the absolute index sums is at most (8/7) c₀ √(AB) |R| under the joint hull caps Σ_ν m_{a,ν} ≤ A, Σ_ν m_{b,ν} ≤ B on R.

theorem TrilinearHT.Auto.pieceInternal_sub_hull {G : RealDyadicGrid} {H : Finset (ℤ × ℤ)} {Q : ℤ × ℤ} {C : Finset (ℤ × ℤ)} (hQ : Q ∈ H) (hC : ∀ c ∈ C, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G Q.1 Q.2) (hhull : ∀ c ∈ C, ∀ (d : ℤ × ℤ), dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2 → dyadicGridCell G d.1 d.2 ⊆ dyadicGridCell G Q.1 Q.2 → d ∈ H) : pieceInternal G Q C ⊆ H

theorem TrilinearHT.Auto.near_band_bound (κ : LocalKernelClass) {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) : ∃ (Cq : ℝ), 0 ≤ Cq ∧ ∀ (G : RealDyadicGrid) (K Nd : ℕ), 1 ≤ K → ∀ {N : Type u_1} (Ns : Finset N) (H Rt U : N → Finset (ℤ × ℤ)) {R : Set ℝ}, MeasurableSet R → (∀ n ∈ Ns, Rt n ⊆ H n) → (∀ n ∈ Ns, (↑(Rt n)).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2) → (∀ n ∈ Ns, ∀ r ∈ Rt n, dyadicGridCell G r.1 r.2 ⊆ R) → (∀ n ∈ Ns, U n ⊆ H n) → (∀ n ∈ Ns, ∀ c ∈ U n, ∃ r ∈ Rt n, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G r.1 r.2) → (∀ n ∈ Ns, ∀ c ∈ U n, ∀ r ∈ Rt n, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G r.1 r.2 → c.1 < r.1 + ↑K) → (∀ n ∈ Ns, ∀ c ∈ U n, ∀ r ∈ Rt n, ∀ (d : ℤ × ℤ), dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2 → dyadicGridCell G d.1 d.2 ⊆ dyadicGridCell G r.1 r.2 → d ∈ H n) → ∀ {ι κ' β : Type} [DecidableEq ι] [DecidableEq κ'] [DecidableEq β] (s : N → Finset ι) (t : N → Finset κ') (u : N → Finset β) {a b c : Fin 4}, a ≠ b → a ≠ c → b ≠ c → ∀ (f : N → Fin 4 → ℝ → ℂ) (x : N → ι → β → ℝ → ℂ) (w : N → κ' → ℝ → ℂ) (y : N → β → ℝ → ℂ), (∀ (n : N) (j : Fin 4), Measurable (f n j)) → (∀ (n : N) (i : ι) (p : β), Measurable (x n i p)) → (∀ (n : N) (k : κ'), Measurable (w n k)) → (∀ (n : N) (p : β), Measurable (y n p)) → ∀ {A B : ENNReal}, (∀ z ∈ R, ∑ n ∈ Ns, dyadicHullMax G (H n) (fun (r : ℝ) => ENNReal.ofReal (∑ i ∈ s n, ∑ p ∈ u n, ‖x n i p r‖ ^ 2)) z ≤ A) → (∀ z ∈ R, ∑ n ∈ Ns, dyadicHullMax G (H n) (fun (r : ℝ) => ENNReal.ofReal (∑ k ∈ t n, ‖w n k r‖ ^ 2)) z ≤ B) → (∀ n ∈ Ns, ∀ d ∈ H n, dyadicEnergyAverage G (fun (r : ℝ) => ENNReal.ofReal (∑ i ∈ s n, ∑ p ∈ u n, ‖x n i p r‖ ^ 2)) d ≠ ⊤) → (∀ n ∈ Ns, ∀ d ∈ H n, dyadicEnergyAverage G (fun (r : ℝ) => ENNReal.ofReal (∑ k ∈ t n, ‖w n k r‖ ^ 2)) d ≠ ⊤) → ∀ (kernel : N → ℤ × ℤ → ℝ × ℝ → ℂ), (∀ n ∈ Ns, ∀ I ∈ H n, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (kernel n I)) → (∀ n ∈ Ns, ∀ (Q : ℤ × ℤ), ∃ (d₀ : ℤ), ∀ I ∈ U n, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G Q.1 Q.2 → I.1 < Q.1 + ↑K → kernel n I ≠ 0 → d₀ ≤ I.1 ∧ I.1 < d₀ + ↑Nd) → (∀ n ∈ Ns, ∀ I ∈ U n, ∀ (j : Fin 4), ⋯ ≠ ⊤) → (∀ n ∈ Ns, ∀ I ∈ U n, ∀ (i : ι), ⋯) → (∀ n ∈ Ns, ∀ I ∈ U n, ⋯) → (∀ n ∈ Ns, ∀ (I : ℤ × ℤ), ⋯) → ∀ {Bc Bd : ℝ}, 0 ≤ Bc → 0 ≤ Bd → ⋯

Blueprint lines 2421-2445 (eq:near-band before the transfer coefficient): for indices n with retained hulls H_n, disjoint hull roots Rt_n ⊆ H_n in R, use cells U_n within K depths of their roots, randomized side stacks x_n (positions and bands), w_n (positions) and the frozen complementary band stack y_n of averages at most B_c² on the hulls, the selected matched band sums with arbitrary signs satisfy 7 Σ_n |Σ_{I ∈ U_n} |I| ε_I Σ_p Λ_I(…)| ≤ 8 C (1+C_N) log K K^{2(q-2)/(q-1)} B_c B_d √(AB) |R| under the joint hull caps Σ_n m_{a,n} ≤ A, Σ_n m_{b,n} ≤ B on R.

theorem TrilinearHT.Auto.physEmbed_coeFn_none {V : Type u_1} {W : Type u_3} [Fintype V] [Fintype W] (x : ↥(ColumnL2 V)) : ∀ᵐ (y : ℝ), (↑↑((physEmbed V W) x) y).ofLp none = (↑↑x y).ofLp none

The physical value of the physical embedding.

noncomputable def TrilinearHT.Auto.packetW (dmax : ℕ) (y : ℝ) : ℝ

The packet width of lem:height at height y for coefficient vectors of dimension at most 2 d_max + 1, in base-two units: 16 (2 d_max + 1)^3 log(2 max(2, y)) (from the natural-log width 8 (d+1)^3 log(2B) of rational_logarithmic_cover_nat).

Equations

• TrilinearHT.Auto.packetW dmax y = 16 * (2 * ↑dmax + 1) ^ 3 * Real.log (2 * max 2 y)

theorem TrilinearHT.Auto.packetW_nonneg (dmax : ℕ) (y : ℝ) : 0 ≤ packetW dmax y

theorem TrilinearHT.Auto.exists_attempt_schedule (Cj CA CT CK : ℕ) {δs : ℝ} (hδs : 0 < δs) (hδs1 : δs ≤ 1) : ∃ (M : ℝ), 0 < M ∧ ∀ (dmax : ℕ) (Dstar Bstar Dm : ℝ) (Q0 : ℕ), 2 ≤ dmax → 2 ≤ Dstar → 2 ≤ Bstar → 2 ≤ Dm → 1 ≤ Q0 → have Λ := ↑dmax + Real.log Dstar + Real.log Bstar + Real.log Dm + Real.log ↑Q0 + 1; ∃ (S : ModeSchedule), S.dmax = dmax ∧ S.Dstar = Dstar ∧ S.Bstar = Bstar ∧ S.Dm = Dm ∧ S.Q0 = Q0 ∧ S.Valid Cj CA CT CK δs (packetW dmax S.H) ∧ Real.log S.H ≤ M * Λ ^ 12 ∧ Real.log S.T ≤ M * Λ ^ 16 ∧ ↑S.K ≤ M * Λ ^ 16

Blueprint mode-schedule (lines 1944-1966) with K chosen last at the packet width of the chosen height: there is a schedule with eq:mode-parameters, side parameters read off it, and log H ≤ M Λ^{12}, log T ≤ M Λ^{16}, K ≤ M Λ^{16}.

theorem TrilinearHT.Auto.sum_families_eq {ι : Type u_1} {α : Type u_2} [DecidableEq α] (V : Finset ι) (U : ι → Finset α) (g : α → ℝ) : ∑ ν ∈ V, ∑ c ∈ U ν, g c = ∑ c ∈ V.biUnion U, g c * ↑{ν ∈ V | c ∈ U ν}.card

Double counting over a finite union of families: Σ_ν Σ_{c ∈ U_ν} g c = Σ_{c ∈ ⋃ U} g c · #{ν : c ∈ U_ν}.

theorem TrilinearHT.Auto.hull_mass_le (G : RealDyadicGrid) {ι : Type u_1} (V : Finset ι) (H U : ι → Finset (ℤ × ℤ)) (hmax : ∀ ν ∈ V, maximalDyadicCells G (H ν) ⊆ U ν) (root : ℤ × ℤ) (hU : ∀ ν ∈ V, ∀ c ∈ U ν, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G root.1 root.2) {M : ℝ} (hM : ∀ (y : ℝ), ↑(∑ ν ∈ V, {c ∈ U ν | y ∈ dyadicGridCell G c.1 c.2}.card) ≤ M) : ∑ ν ∈ V, MeasureTheory.volume (⋃ c ∈ maximalDyadicCells G (H ν), dyadicGridCell G c.1 c.2) ≤ ENNReal.ofReal (M * dyadicGridLength G root.1)

Blueprint lines 2426-2427 (Σ_ν |Ω_ν| ≤ M₀ |R| "by active multiplicity, the main group count, and the number of configurations"): if the maximal cells of each hull are use cells of ν and every point lies in at most M use cells counted over all ν, the hull roots have total measure at most M |R|.

theorem TrilinearHT.Auto.augPhys_normalized_ne_top {V : Type u_1} [Fintype V] (G : RealDyadicGrid) (I : ℤ × ℤ) (x : ↥(ColumnL2 V)) : MeasureTheory.eLpNorm (augPhys x) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≠ ⊤

The normalized size of the physical part of a column on a cell is finite.

def TrilinearHT.Auto.ActiveSetup.DepthWin {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (Nd : ℕ) : Prop

Blueprint line 2836 and the depth hypothesis of prop:normalized: the cells of the setup with nonzero kernel lie in N_d consecutive depths [d₀, d₀ + N_d) of the original range.

Equations

• A.DepthWin Nd = ∃ (d₀ : ℤ), ∀ I ∈ A.cells, A.w I ≠ 0 → d₀ ≤ I.1 ∧ I.1 < d₀ + ↑Nd

theorem TrilinearHT.Auto.three_side_patterns_sum_le {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℂ W] (Gd : RealDyadicGrid) {γ : Type u_2} (S : Finset (ℤ × ℤ)) (root : ℤ × ℤ) (hroot : ∀ I ∈ S, dyadicGridCell Gd I.1 I.2 ⊆ dyadicGridCell Gd root.1 root.2) (Gs : ℤ × ℤ → Finset γ) (Λ : ℤ × ℤ → MultilinearMap ℂ (fun (x : Fin 4) => W) ℂ) {C Bs : ℝ} (hC : 0 ≤ C) (hBs : 0 ≤ Bs) (hΛ : ∀ I ∈ S, ∀ (x : Fin 4 → W), ‖(Λ I) x‖ ≤ C * ∏ l : Fin 4, ‖x l‖ / √(dyadicGridLength Gd I.1)) (a s e : ℤ × ℤ → γ → Fin 4 → W) (hsize : ∀ I ∈ S, ∀ G ∈ Gs I, ∀ (l : Fin 4), ‖a I G l‖ ≤ Bs * √(dyadicGridLength Gd I.1) ∧ ‖s I G l‖ ≤ Bs * √(dyadicGridLength Gd I.1)) {T : ℝ} (hT : ∀ (x : ℝ), ∑ I ∈ S with x ∈ dyadicGridCell Gd I.1 I.2, ∑ G ∈ Gs I, ∑ l : Fin 4, ‖s I G l‖ ^ 2 / dyadicGridLength Gd I.1 ≤ T) {η p : ℝ} (hη : 0 ≤ η) (hp : 2 / 3 < p) (hp1 : p ≤ 1) : ∑ I ∈ S, dyadicGridLength Gd I.1 * min η (∑ σ : Fin 4 → Fin 3 with (∀ (l : Fin 4), σ l ≠ 2) ∧ 3 ≤ patternCount σ 1, ‖∑ G ∈ Gs I, (Λ I) (patternPiece (a I G) (s I G) (e I G) σ)‖) ≤ η ^ (1 - p) * (81 * C * Bs) ^ p * (T ^ (p / 2) * T ^ (p / 2) * T ^ (p / 2) * dyadicGridLength Gd root.1)

Blueprint eq:three-sides with eq:min-power, for the sum of the norms of the error-free patterns with at least three sides: their contribution to the active minimum is at most η^{1-p} (81 C B)^p T^{3p/2} |R|.

The near-band estimate after the common hull cuts (blueprint lines 2425-2444)

theorem TrilinearHT.Auto.lintegral_augPhys_sq_le {V : Type u_1} [Fintype V] (x : ↥(ColumnL2 V)) : ∫⁻ (y : ℝ), ENNReal.ofReal (‖augPhys x y‖ ^ 2) ≤ ENNReal.ofReal (‖x‖ ^ 2)

The physical part of a column has integrated square at most its square norm.

The near band pairs by offsets (blueprint line 2425, "fix a near offset q - p")

theorem TrilinearHT.Auto.near_pairs_offsets {M : Type u_1} [AddCommMonoid M] [Module ℂ M] (P : ℕ) (f : ℕ → ℕ → M) : ∑ p ∈ Finset.range (P + 1), ∑ q ∈ Finset.range (P + 1) with ¬(q + 2 < p ∨ p + 2 < q), ((↑p - ↑q) / ↑P) • f p q = ∑ o ∈ Finset.range 5, ((2 - ↑o) / ↑P) • ∑ p ∈ Finset.range (P + 1) with 2 ≤ p + o ∧ p + o - 2 ≤ P, f p (p + o - 2)

Blueprint line 2425: the near band pairs |p - q| ≤ 2 of 0..P are the pairs (p, p + o - 2) over the five offsets o < 5, with the coefficient (p - q)/P = (2 - o)/P of each offset constant.

theorem TrilinearHT.Auto.defTerm_near {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) (st : TransferStep E) (rest : List (TransferStep E)) (xa : E) : defTerm Λ P a c d x yc yd (fun (p q : ℕ) => ¬(q + 2 < p ∨ p + 2 < q)) st rest xa = ∑ o ∈ Finset.range 5, (2 - ↑o) / ↑P * ∑ p ∈ Finset.range (P + 1) with 2 ≤ p + o ∧ p + o - 2 ≤ P, Λ (Function.update (Function.update (Function.update (Function.update x c (chainVal P true rest yc)) d (chainVal P false rest yd)) a ((st.2.1 (p + 1)) xa - (st.2.1 p) xa)) (if st.1 = true then c else d) ((st.2.2 (p + o - 2 + 1)) (chainVal P st.1 rest (if st.1 = true then yc else yd)) - (st.2.2 (p + o - 2)) (chainVal P st.1 rest (if st.1 = true then yc else yd))))

The near band defect of one step, by offsets: the sum over the five offsets o of (2 - o)/P times the band sums with the paired bands p and p + o - 2.

theorem TrilinearHT.Auto.posExpand_coef (ls : List (ℕ × Bool)) (t : ℤ × List ℕ) : t ∈ posExpand ls → ‖↑t.1‖ ≤ 1

theorem TrilinearHT.Auto.norm_list_map_sum_le {α : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] (L : List α) (f : α → E) : ‖(List.map f L).sum‖ ≤ (List.map (fun (x : α) => ‖f x‖) L).sum

theorem TrilinearHT.Auto.list_map_sum_le {α : Type u_1} (L : List α) {f g : α → ℝ} (h : ∀ x ∈ L, f x ≤ g x) : (List.map f L).sum ≤ (List.map g L).sum

theorem TrilinearHT.Auto.min_three_strong (Gd : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (root : ℤ × ℤ) (hroot : ∀ I ∈ S, dyadicGridCell Gd I.1 I.2 ⊆ dyadicGridCell Gd root.1 root.2) {ω : Type u_1} {γ : Type u_2} (Os : Finset ω) (gs : ℤ × ℤ → Finset γ) (fa fb fc : ω → ℤ × ℤ → γ → ℝ) (ha : ∀ (o : ω) (I : ℤ × ℤ) (G : γ), 0 ≤ fa o I G) (hb : ∀ (o : ω) (I : ℤ × ℤ) (G : γ), 0 ≤ fb o I G) (Ca Cb Cc : ω → ℝ) (hCa : ∀ o ∈ Os, ∀ (x : ℝ), ∑ I ∈ S with x ∈ dyadicGridCell Gd I.1 I.2, ∑ G ∈ gs I, fa o I G ^ 2 ≤ Ca o) (hCb : ∀ o ∈ Os, ∀ (x : ℝ), ∑ I ∈ S with x ∈ dyadicGridCell Gd I.1 I.2, ∑ G ∈ gs I, fb o I G ^ 2 ≤ Cb o) (hCc : ∀ o ∈ Os, ∀ (x : ℝ), ∑ I ∈ S with x ∈ dyadicGridCell Gd I.1 I.2, ∑ G ∈ gs I, fc o I G ^ 2 ≤ Cc o) (hval : ℤ × ℤ → ℝ) (hh : ∀ I ∈ S, hval I ≤ ∑ o ∈ Os, ∑ G ∈ gs I, fa o I G * fb o I G * fc o I G) {η p : ℝ} (hη : 0 ≤ η) (hp : 2 / 3 < p) (hp1 : p ≤ 1) : ∑ I ∈ S, dyadicGridLength Gd I.1 * min η (hval I) ≤ η ^ (1 - p) * ∑ o ∈ Os, Ca o ^ (p / 2) * Cb o ^ (p / 2) * Cc o ^ (p / 2) * dyadicGridLength Gd root.1

Blueprint lines 2372-2384 and 2447-2449 (eq:three-sides, eq:min-power): if the cell values h_I are bounded by sums over terms o and groups G ∈ gs I of products of three nonnegative strong factors, whose group-summed squares have path caps C_a o, C_b o, C_c o, then Σ_I |I| min(η, ‖h_I‖) ≤ η^{1-p} Σ_o (C_a C_b C_c)^{p/2} |R| for 2/3 < p ≤ 1.

theorem TrilinearHT.Auto.two_two_tuple (σ : Fin 4 → Fin 3) : (∀ (l : Fin 4), σ l ≠ 2) ∧ {l : Fin 4 | σ l = 0}.card = 2 ∧ {l : Fin 4 | σ l = 1}.card = 2 → ∀ (u : Fin 4), ∃ (a : Fin 4) (b : Fin 4) (c : Fin 4) (d : Fin 4), a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d ∧ σ c = 0 ∧ σ d = 0 ∧ σ a = 1 ∧ σ b = 1 ∧ a ≠ u

The 2+2 patterns: two cores and two sides, no error.

theorem TrilinearHT.Auto.card_two_two : {σ : Fin 4 → Fin 3 | (∀ (l : Fin 4), σ l ≠ 2) ∧ {l : Fin 4 | σ l = 0}.card = 2 ∧ {l : Fin 4 | σ l = 1}.card = 2}.card = 6

theorem TrilinearHT.Auto.exceptional_roots_le (G : RealDyadicGrid) {ι : Type u_1} (T : Finset ι) (F : ι → Finset (ℤ × ℤ)) (ρs : ι → ℝ) (root : ℤ × ℤ) (hF : ∀ i ∈ T, dyadicRootLength G (F i) ≤ ρs i * dyadicGridLength G root.1) {ρ : ℝ} (hρ : ∑ i ∈ T, ρs i ≤ ρ) : dyadicRootLength G (maximalDyadicCells G (T.biUnion F)) ≤ ρ * dyadicGridLength G root.1

Blueprint lines 2839-2840 ("choose their thresholds so the union of exceptional roots has length at most |R|/4") with path-packing line 429 ("for several rules take maximal cells in their union and add their length bounds"): finitely many cut families of lengths at most ρ_i |R| with Σ ρ_i ≤ ρ have maximal union cells of total length at most ρ |R|.

theorem TrilinearHT.Auto.two_hull_caps {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup F] (V : Finset ι) (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (H : ι → Finset (ℤ × ℤ)) (fa fb : ι → ℝ → F) (hfa : ∀ ν ∈ V, MeasureTheory.AEStronglyMeasurable (fa ν) MeasureTheory.volume) (hfb : ∀ ν ∈ V, MeasureTheory.AEStronglyMeasurable (fb ν) MeasureTheory.volume) (root : ℤ × ℤ) (hHS : ∀ ν ∈ V, H ν ⊆ S) (hS : ∀ c ∈ S, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G root.1 root.2) {Ea Eb M ρ : ℝ} (hEa : 0 ≤ Ea) (hEb : 0 ≤ Eb) (hM0 : 0 ≤ M) (hρ : 0 < ρ) (hρ1 : ρ < 1) (hea : ∑ ν ∈ V, MeasureTheory.eLpNorm (fa ν) 2 MeasureTheory.volume ^ 2 ≤ ENNReal.ofReal (Ea * dyadicGridLength G root.1)) (heb : ∑ ν ∈ V, MeasureTheory.eLpNorm (fb ν) 2 MeasureTheory.volume ^ 2 ≤ ENNReal.ofReal (Eb * dyadicGridLength G root.1)) (hM : ∑ ν ∈ V, MeasureTheory.volume (⋃ c ∈ maximalDyadicCells G (H ν), dyadicGridCell G c.1 c.2) ≤ ENNReal.ofReal (M * dyadicGridLength G root.1)) : ∃ C ⊆ S, dyadicRootLength G (maximalDyadicCells G C) ≤ ρ * dyadicGridLength G root.1 ∧ (∀ (x : ℝ), ∑ ν ∈ V, dyadicHullMax G ({c ∈ H ν | ¬∃ d ∈ C, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2}) (fun (y : ℝ) => ‖fa ν y‖ₑ ^ 2) x ≤ ENNReal.ofReal (hullCutConstant (ρ / 2) * Ea * (1 + Real.log (2 + M)))) ∧ ∀ (x : ℝ), ∑ ν ∈ V, dyadicHullMax G ({c ∈ H ν | ¬∃ d ∈ C, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2}) (fun (y : ℝ) => ‖fb ν y‖ₑ ^ 2) x ≤ ENNReal.ofReal (hullCutConstant (ρ / 2) * Eb * (1 + Real.log (2 + M)))

Blueprint lines 2428-2431 ("apply the hull part of lem:cuts to the two energies in eq:stack-energy ... combine these cuts"): two families of fixed functions with total square energies E_a |R|, E_b |R| on hulls of total support M |R| admit one family of cut cells of total length at most ρ |R| after which the squared hull maxima on the retained hulls have the joint caps C_{ρ/2} E_a (1 + log(2+M)) and C_{ρ/2} E_b (1 + log(2+M)) everywhere.

The hull mass of the stacks (blueprint line 2426)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.hull_mult_le {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {γ : Type u_1} (Gs : Finset bf.Grp) (Cs : Finset γ) (Bs : Finset ℕ) (k : ℕ) (Act : Finset (ℤ × ℤ)) (U : bf.Grp → γ → ℕ → Finset (ℤ × ℤ)) (hU : ∀ (G : bf.Grp) (x : γ) (b : ℕ), ∀ c ∈ U G x b, c ∈ Act ∧ G ∈ fp.groupsAt c k) (hblk : ∀ (G : bf.Grp) (x : γ) (b b' : ℕ), ∀ c ∈ U G x b, c ∈ U G x b' → b = b') {Mp : ℝ} (hMp : ∀ (y : ℝ), ↑{c ∈ Act | y ∈ dyadicGridCell A.G c.1 c.2}.card ≤ Mp) (y : ℝ) : ∑ G ∈ Gs, ∑ x ∈ Cs, ∑ b ∈ Bs, ↑{c ∈ U G x b | y ∈ dyadicGridCell A.G c.1 c.2}.card ≤ ↑Cs.card * Mp * ↑A.famVtxBound

Blueprint line 2426 ("Σ_ν |Ω_ν| ≤ M₀ |R| with M₀ ≤ exp(k^{O(1)}), by active multiplicity, the main group count, and the number of configurations"), pointwise: if the use cells of the indices ν = (G, configuration, block) are cells of a set Act (the active cells) where G is a current group of the color k, each cell lies in the uses of at most one block for fixed (G, configuration), and every point lies in at most M_p cells of Act, then every point lies in at most |configurations| M_p D use cells counted over all ν (D the vertex bound). With hull_mass_le this gives Σ_ν |Ω_ν| ≤ |configurations| M_p D |R|.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.near_use_multiplicity {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (K : ℕ) (hK : 1 ≤ K) {Ω : Type u_1} (Os : Finset Ω) (Gs : Finset bf.Grp) (Bs : Finset ℕ) (k : ℕ) (Act : Finset (ℤ × ℤ)) (U : bf.Grp → ℕ → Finset (ℤ × ℤ)) (off : ℤ × ℤ → ℕ) (hdepth : ∀ (g : bf.Grp) (β : ℕ), ∀ I ∈ U g β, I.1 = A.R.1 + ↑(K * β + off I)) (hUact : ∀ (g : bf.Grp) (β : ℕ), ∀ I ∈ U g β, I ∈ Act ∧ g ∈ fp.groupsAt I k) {Mp : ℝ} (hMp : ∀ (y : ℝ), ↑{c ∈ Act | y ∈ dyadicGridCell A.G c.1 c.2}.card ≤ Mp) (Ms : Finset (Ω × bf.Grp × ℕ)) (hMs : Ms ⊆ Os ×ˢ Gs ×ˢ Bs) (Um : Ω × bf.Grp × ℕ → Finset (ℤ × ℤ)) (hUm : ∀ m ∈ Ms, Um m ⊆ U m.2.1 m.2.2) (y : ℝ) : ↑(∑ m ∈ Ms, {c ∈ Um m | y ∈ dyadicGridCell A.G c.1 c.2}.card) ≤ ↑Os.card * Mp * ↑A.famVtxBound

Near-band subfamilies inherit the active-cell multiplicity bound, uniformly over blocks.

Stack densities, use hulls and outer stack energies (blueprint lines 2410-2430)

theorem TrilinearHT.Auto.lintegral_augPhys_sum_le {V : Type u_1} [Fintype V] {ι : Type u_2} {β : Type u_3} (s : Finset ι) (u : Finset β) (X : ι → β → ↥(ColumnL2 V)) : ∫⁻ (y : ℝ), ENNReal.ofReal (∑ i ∈ s, ∑ p ∈ u, ‖augPhys (X i p) y‖ ^ 2) ≤ ENNReal.ofReal (∑ i ∈ s, ∑ p ∈ u, ‖X i p‖ ^ 2)

A finite double sum of physical squares has integral at most the sum of the square norms.

noncomputable def TrilinearHT.Auto.stackDens {V : Type u_1} [Fintype V] {ι : Type u_2} {β : Type u_3} (s : Finset ι) (u : Finset β) (X : ι → β → ↥(ColumnL2 V)) (y : ℝ) : ℝ

The square root of a finite double sum of physical squares, as a stack density.

Equations

• TrilinearHT.Auto.stackDens s u X y = √(∑ i ∈ s, ∑ p ∈ u, ‖TrilinearHT.Auto.augPhys (X i p) y‖ ^ 2)

theorem TrilinearHT.Auto.stackDens_measurable {V : Type u_1} [Fintype V] {ι : Type u_2} {β : Type u_3} (s : Finset ι) (u : Finset β) (X : ι → β → ↥(ColumnL2 V)) : Measurable (stackDens s u X)

theorem TrilinearHT.Auto.stackDens_enorm_sq {V : Type u_1} [Fintype V] {ι : Type u_2} {β : Type u_3} (s : Finset ι) (u : Finset β) (X : ι → β → ↥(ColumnL2 V)) (y : ℝ) : ‖stackDens s u X y‖ₑ ^ 2 = ENNReal.ofReal (∑ i ∈ s, ∑ p ∈ u, ‖augPhys (X i p) y‖ ^ 2)

theorem TrilinearHT.Auto.stackDens_eLpNorm_sq {V : Type u_1} [Fintype V] {ι : Type u_2} {β : Type u_3} (s : Finset ι) (u : Finset β) (X : ι → β → ↥(ColumnL2 V)) : MeasureTheory.eLpNorm (stackDens s u X) 2 MeasureTheory.volume ^ 2 ≤ ENNReal.ofReal (∑ i ∈ s, ∑ p ∈ u, ‖X i p‖ ^ 2)

theorem TrilinearHT.Auto.energyAverage_augPhys_ne_top {V : Type u_1} [Fintype V] (G : RealDyadicGrid) {ι : Type u_2} {β : Type u_3} (s : Finset ι) (u : Finset β) (X : ι → β → ↥(ColumnL2 V)) (d : ℤ × ℤ) : dyadicEnergyAverage G (fun (y : ℝ) => ENNReal.ofReal (∑ i ∈ s, ∑ p ∈ u, ‖augPhys (X i p) y‖ ^ 2)) d ≠ ⊤

The energy average of a physical square sum on a cell is finite.

noncomputable def TrilinearHT.Auto.ActiveSetup.useHull {κ' : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ' c₀) (U : Finset (ℤ × ℤ)) : Finset (ℤ × ℤ)

The hull of a family of use cells: the active cells between two of its cells.

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.useHull_sub {κ' : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ' c₀) (U : Finset (ℤ × ℤ)) : A.useHull U ⊆ A.cells

theorem TrilinearHT.Auto.ActiveSetup.mem_useHull {κ' : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ' c₀) {U : Finset (ℤ × ℤ)} (hU : U ⊆ A.cells) {c : ℤ × ℤ} (hc : c ∈ U) : c ∈ A.useHull U

noncomputable def TrilinearHT.Auto.unPhase (z : ℂ) : ℂ

The unimodular phase undoing the argument of a complex number (zero at zero).

Equations

• TrilinearHT.Auto.unPhase z = if z = 0 then 0 else (starRingEnd ℂ) z / ↑‖z‖

theorem TrilinearHT.Auto.norm_unPhase_le (z : ℂ) : ‖unPhase z‖ ≤ 1

theorem TrilinearHT.Auto.unPhase_mul (z : ℂ) : unPhase z * z = ↑‖z‖

theorem TrilinearHT.Auto.sum_enorm_eq_unPhase {α : Type u_1} (s : Finset α) (x : α → ℂ) : ∑ i ∈ s, ‖x i‖ₑ = ‖∑ i ∈ s, unPhase (x i) * x i‖ₑ

A finite sum of moduli is the modulus of the sum with the undoing phases.

theorem TrilinearHT.Auto.gluedStack_norm_sq_mono (G : RealDyadicGrid) {V : Type u_1} [Fintype V] {ι : Type u_2} {U U' : Finset (ℤ × ℤ)} (hUU : U' ⊆ U) (sel : ℤ × ℤ → ι) (val : ι → ↥(ColumnL2 V)) (i : ι) : ‖gluedStack G U' sel val i‖ ^ 2 ≤ ‖gluedStack G U sel val i‖ ^ 2

The glued stack over a smaller family of cells is smaller.

theorem TrilinearHT.Auto.restrict_restrict_disjoint (G : RealDyadicGrid) {V : Type u_1} [Fintype V] {I J : ℤ × ℤ} (h : Disjoint (dyadicGridCell G I.1 I.2) (dyadicGridCell G J.1 J.2)) (x : ↥(ColumnL2 V)) : (columnL2Restriction (dyadicGridCell G I.1 I.2) ⋯) ((columnL2Restriction (dyadicGridCell G J.1 J.2) ⋯) x) = 0

The restriction to one cell of the restriction to a disjoint cell vanishes.

theorem TrilinearHT.Auto.depthStack_restrict (G : RealDyadicGrid) {V : Type u_1} [Fintype V] (U : Finset (ℤ × ℤ)) (sel : ℤ × ℤ → ℕ) (hdis : ∀ I ∈ U, ∀ J ∈ U, sel I = sel J → I ≠ J → Disjoint (dyadicGridCell G I.1 I.2) (dyadicGridCell G J.1 J.2)) (v : ℤ × ℤ → ↥(ColumnL2 V)) {I : ℤ × ℤ} (hI : I ∈ U) : (columnL2Restriction (dyadicGridCell G I.1 I.2) ⋯) (depthStack G U sel v (sel I)) = (columnL2Restriction (dyadicGridCell G I.1 I.2) ⋯) (v I)

On a cell of U, the depth stack at its selection is its local value, if the cells of one selection are pairwise disjoint.

theorem TrilinearHT.Auto.depthStack_norm_sq (G : RealDyadicGrid) {V : Type u_1} [Fintype V] (U : Finset (ℤ × ℤ)) (sel : ℤ × ℤ → ℕ) (hdis : ∀ I ∈ U, ∀ J ∈ U, sel I = sel J → I ≠ J → Disjoint (dyadicGridCell G I.1 I.2) (dyadicGridCell G J.1 J.2)) (v : ℤ × ℤ → ↥(ColumnL2 V)) (m : ℕ) : ‖depthStack G U sel v m‖ ^ 2 = ∑ J ∈ U with sel J = m, ‖(columnL2Restriction (dyadicGridCell G J.1 J.2) ⋯) (v J)‖ ^ 2

The square norm of a depth stack is the sum of the square norms of the restricted local values of its cells (disjoint supports).

theorem TrilinearHT.Auto.energyAverage_band_le (G : RealDyadicGrid) {V : Type u_1} [Fintype V] {β : Type u_2} (u : Finset β) (Y : β → ↥(ColumnL2 V)) (d : ℤ × ℤ) : dyadicEnergyAverage G (fun (r : ℝ) => ENNReal.ofReal (∑ p ∈ u, ‖augPhys (Y p) r‖ ^ 2)) d ≤ ENNReal.ofReal ((∑ p ∈ u, ‖(columnL2Restriction (dyadicGridCell G d.1 d.2) ⋯) (Y p)‖ ^ 2) / dyadicGridLength G d.1)

The energy average of a physical square sum on a cell is at most the restricted square norms divided by the length.

theorem TrilinearHT.Auto.energyAverage_single_le (G : RealDyadicGrid) {V : Type u_1} [Fintype V] (F : ↥(ColumnL2 V)) (d : ℤ × ℤ) : dyadicEnergyAverage G (fun (r : ℝ) => ‖augPhys F r‖ₑ ^ 2) d ≤ ENNReal.ofReal (‖(columnL2Restriction (dyadicGridCell G d.1 d.2) ⋯) F‖ ^ 2 / dyadicGridLength G d.1)

The energy average of one physical square on a cell is at most the restricted square norm divided by the length.

theorem TrilinearHT.Auto.gluedStack_sum_mono (G : RealDyadicGrid) {V : Type u_1} [Fintype V] {ι : Type u_2} {β : Type u_3} [DecidableEq ι] {U U' : Finset (ℤ × ℤ)} (hUU : U' ⊆ U) (sel : ℤ × ℤ → ι) {u u' : Finset β} (huu : u' ⊆ u) (val : β → ι → ↥(ColumnL2 V)) : ∑ i ∈ Finset.image sel U', ∑ p ∈ u', ‖gluedStack G U' sel (val p) i‖ ^ 2 ≤ ∑ i ∈ Finset.image sel U, ∑ p ∈ u, ‖gluedStack G U sel (val p) i‖ ^ 2

Glued stacks over smaller families of cells and band ranges have smaller total energies.

theorem TrilinearHT.Auto.ActiveSetup.bandStack_outer {κ' : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ' c₀) (hanc : A.AncClosed) {Ω : Type u_1} {γ : Type u_2} {V : Type u_3} [Fintype V] (Os : Finset Ω) (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 β) (Ms : Finset (Ω × γ × ℕ)) (hMs : Ms ⊆ Os ×ˢ Gs ×ˢ Bs) (Um : Ω × γ × ℕ → Finset (ℤ × ℤ)) (hUm : ∀ m ∈ Ms, Um m ⊆ U m.2.1 m.2.2) (u : Ω × γ × ℕ → Finset ℕ) (hu : ∀ m ∈ Ms, u m ⊆ Finset.range (P + 1)) : ∑ m ∈ Ms, ∑ k : Fin (N + 1), ∑ i ∈ Finset.image (fun (I : ℤ × ℤ) => off I / 2 ^ (↑k + 1)) ({I ∈ Um m | posAct N k (off I)}), ∑ p ∈ u m, ‖gluedStack A.G ({I ∈ Um m | posAct N k (off I)}) (fun (I : ℤ × ℤ) => off I / 2 ^ (↑k + 1)) (fun (i : ℕ) => posVal (fun (n : ℕ) => (Ah m.1 m.2.1 (p + 1) (A.R.1 + ↑(K * m.2.2) + ↑n) - Ah m.1 m.2.1 p (A.R.1 + ↑(K * m.2.2) + ↑n)) (Sa m.2.1 m.2.2 (A.R.1 + ↑(K * m.2.2) + ↑n))) N k i) i‖ ^ 2 ≤ ∑ ω ∈ Os, (↑N * (2 * B + 16 * (↑P + 2) * (Cj ω * EW) + 16 * (↑P + 2) * (↑N * (Cj ω * (↑N * B)))) + EW)

The banded stack energies over indices m = (ω, g, β) with use sets inside the uses of the group and block, band ranges inside 0..P and band values (A_{ω,g,p+1} - A_{ω,g,p}) S_{g,β}: the sum over the outer indices ω of bandStack_all.

theorem TrilinearHT.Auto.ActiveSetup.posStack_outer {κ' : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ' c₀) (hanc : A.AncClosed) {Ω : Type u_1} {γ : Type u_2} {V : Type u_3} [Fintype V] (Os : Finset Ω) (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) (Ms : Finset (Ω × γ × ℕ)) (hMs : Ms ⊆ Os ×ˢ Gs ×ˢ Bs) (Um : Ω × γ × ℕ → Finset (ℤ × ℤ)) (hUm : ∀ m ∈ Ms, Um m ⊆ U m.2.1 m.2.2) : ∑ m ∈ Ms, ∑ k : Fin (N + 1), ∑ i ∈ Finset.image (fun (I : ℤ × ℤ) => off I / 2 ^ (↑k + 1)) ({I ∈ Um m | posAct N k (off I)}), ‖gluedStack A.G ({I ∈ Um m | posAct N k (off I)}) (fun (I : ℤ × ℤ) => off I / 2 ^ (↑k + 1)) (fun (i : ℕ) => posVal (fun (n : ℕ) => Sb m.2.1 m.2.2 (A.R.1 + ↑(K * m.2.2) + ↑n)) N k i) i‖ ^ 2 ≤ ∑ _ω ∈ Os, (↑N * B + EW)

The untouched-side position stack energies over indices m = (ω, g, β) with use sets inside the uses of the group and block: #Ω times posStack_all.

theorem TrilinearHT.Auto.near_real {M : Type u_1} {ι : Type u_2} (Ms : Finset M) (U : M → Finset ι) (L : ι → ℝ) (hL : ∀ (i : ι), 0 ≤ L i) (v : M → ι → ℂ) {X Y₁ Y₂ R : ℝ} (hX : 0 ≤ X) (hY₁ : 0 ≤ Y₁) (hY₂ : 0 ≤ Y₂) (hR : 0 ≤ R) (h : 7 * ∑ m ∈ Ms, ∑ i ∈ U m, ‖↑(L i) * v m i‖ₑ ≤ 8 * ENNReal.ofReal X * ((ENNReal.ofReal Y₁ * ENNReal.ofReal Y₂) ^ (1 / 2) * ENNReal.ofReal R)) : ∑ m ∈ Ms, ∑ i ∈ U m, L i * ‖v m i‖ ≤ 8 / 7 * X * √(Y₁ * Y₂) * R

The real form of the extended-norm conclusion of near_band_positions.

Near bands on the main columns (blueprint lines 2426-2443)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.Λc_congr_restrictM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) {x y : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))} (h : ∀ (l : Fin 4), (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (x l) = (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (y l)) : (fp.Λc I) x = (fp.Λc I) y

The cell form on the main columns sees only the restrictions of its inputs to the cell.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.Λc_stacks_expandM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {I : ℤ × ℤ} {a b : Fin 4} (hab : a ≠ b) (x : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (va vb : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {Ka : Type u_1} {Kb : Type u_2} (Sa : Finset Ka) (Sb : Finset Kb) (fa : Ka → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (fb : Kb → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (ga gb : Ka → Kb → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (hga : ∀ k ∈ Sa, ∀ k' ∈ Sb, (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (ga k k') = (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (fa k)) (hgb : ∀ k ∈ Sa, ∀ k' ∈ Sb, (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (gb k k') = (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (fb k')) (hva : (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) va = ∑ k ∈ Sa, (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (fa k)) (hvb : (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) vb = ∑ k ∈ Sb, (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (fb k)) : (fp.Λc I) (Function.update (Function.update x a va) b vb) = ∑ ka ∈ Sa, ∑ kb ∈ Sb, (fp.Λc I) (Function.update (Function.update x a (ga ka kb)) b (gb ka kb))

Blueprint lines 2400-2411 and 2423 at one use, on the main columns: if the restrictions of the two varying sides to the use are the sums of the selected components of their active configurations, the cell form is the sum over the pairs of active configurations of the forms of the glued stacks.

theorem TrilinearHT.Auto.ActiveSetup.useHull_max_sub {κ' : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ' c₀) {U : Finset (ℤ × ℤ)} (hU : U ⊆ A.cells) : maximalDyadicCells A.G (A.useHull U) ⊆ U

The maximal cells of the hull of a family of active cells are cells of the family (blueprint line 2426: "its maximal cells are disjoint roots").

theorem TrilinearHT.Auto.augPhys_update3V {V : Type u_1} [Fintype V] (F : Fin 4 → ↥(ColumnL2 V)) (a b c : Fin 4) (xa xb xc : ↥(ColumnL2 V)) : (fun (l : Fin 4) => augPhys (Function.update (Function.update (Function.update F a xa) b xb) c xc l)) = Function.update (Function.update (Function.update (fun (l : Fin 4) => augPhys (F l)) a (augPhys xa)) b (augPhys xb)) c (augPhys xc)

The physical parts of a triple slot update.

theorem TrilinearHT.Auto.leaf_near_bandM (κ : LocalKernelClass) {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) : ∃ (Cq : ℝ), 0 ≤ Cq ∧ ∀ {c₀ : ℕ} (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) (fp : bf.FamParams) (K Nd : ℕ), A.DepthWin Nd → 1 ≤ K → ∀ {N : Type u_1} (Ns : Finset N) (H Rt U : N → Finset (ℤ × ℤ)) {R : Set ℝ}, MeasurableSet R → (∀ n ∈ Ns, Rt n ⊆ H n) → (∀ n ∈ Ns, (↑(Rt n)).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell A.G c.1 c.2) → (∀ n ∈ Ns, ∀ r ∈ Rt n, dyadicGridCell A.G r.1 r.2 ⊆ R) → (∀ n ∈ Ns, U n ⊆ H n) → (∀ n ∈ Ns, ∀ c ∈ U n, ∃ r ∈ Rt n, dyadicGridCell A.G c.1 c.2 ⊆ dyadicGridCell A.G r.1 r.2) → (∀ n ∈ Ns, ∀ c ∈ U n, ∀ r ∈ Rt n, dyadicGridCell A.G c.1 c.2 ⊆ dyadicGridCell A.G r.1 r.2 → c.1 < r.1 + ↑K) → (∀ n ∈ Ns, ∀ c ∈ U n, ∀ r ∈ Rt n, ∀ (d : ℤ × ℤ), dyadicGridCell A.G c.1 c.2 ⊆ dyadicGridCell A.G d.1 d.2 → dyadicGridCell A.G d.1 d.2 ⊆ dyadicGridCell A.G r.1 r.2 → d ∈ H n) → (∀ n ∈ Ns, H n ⊆ A.cells) → ∀ {ι κ' β : Type} [DecidableEq ι] [DecidableEq κ'] [DecidableEq β] (s : N → Finset ι) (t : N → Finset κ') (u : N → Finset β) {a b c : Fin 4}, a ≠ b → a ≠ c → b ≠ c → ∀ (F : N → Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (X : N → ι → β → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (W : N → κ' → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (Y : N → β → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {Aa Bb : ENNReal}, (∀ z ∈ R, ∑ n ∈ Ns, dyadicHullMax A.G (H n) (fun (r : ℝ) => ENNReal.ofReal (∑ i ∈ s n, ∑ p ∈ u n, ‖augPhys (X n i p) r‖ ^ 2)) z ≤ Aa) → (∀ z ∈ R, ∑ n ∈ Ns, dyadicHullMax A.G (H n) (fun (r : ℝ) => ENNReal.ofReal (∑ k ∈ t n, ‖augPhys (W n k) r‖ ^ 2)) z ≤ Bb) → (∀ n ∈ Ns, ∀ d ∈ H n, dyadicEnergyAverage A.G (fun (r : ℝ) => ENNReal.ofReal (∑ i ∈ s n, ∑ p ∈ u n, ⋯)) d ≠ ⊤) → (∀ n ∈ Ns, ∀ d ∈ H n, dyadicEnergyAverage A.G (fun (r : ℝ) => ENNReal.ofReal (∑ k ∈ t n, ⋯)) d ≠ ⊤) → ∀ {Bc Bd : ℝ}, 0 ≤ Bc → 0 ≤ Bd → (∀ n ∈ Ns, ∀ d ∈ H n, ⋯ ≤ ENNReal.ofReal (Bc ^ 2)) → (∀ n ∈ Ns, ∀ (j : Fin 4), j ≠ a → ⋯) → ∀ (sa : N → ℤ × ℤ → ι) (sb : N → ℤ × ℤ → κ'), (∀ (n : N), ⋯) → ⋯ → ⋯

Blueprint lines 2430-2444 (eq:near-band) on the main column stacks: the near-band bound of near_band_bound for the cell forms Λ_c on the main columns, applied to fixed column inputs F, the first side stack X (positions and bands), the second side stack W and the frozen band stack Y, on hulls of active cells.

theorem TrilinearHT.Auto.near_band_cutM (κ : LocalKernelClass) {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) : ∃ (Cq : ℝ), 0 ≤ Cq ∧ ∀ {c₀ : ℕ} (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) (fp : bf.FamParams) (K Nd : ℕ), A.DepthWin Nd → 1 ≤ K → A.AncClosed → ∀ {N : Type u_1} (Ns : Finset N) (U : N → Finset (ℤ × ℤ)) (bs : N → ℤ), (∀ n ∈ Ns, U n ⊆ A.cells) → (∀ n ∈ Ns, ∀ c ∈ U n, bs n ≤ c.1 ∧ c.1 < bs n + ↑K) → ∀ {ι κ' β : Type} [DecidableEq ι] [DecidableEq κ'] [DecidableEq β] (s : N → Finset ι) (t : N → Finset κ') (u : N → Finset β) {a b c : Fin 4}, a ≠ b → a ≠ c → b ≠ c → ∀ (F : N → Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (X : N → ι → β → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (W : N → κ' → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (Y : N → β → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {Ea Eb ρ Mu : ℝ}, 0 ≤ Ea → 0 ≤ Eb → 0 ≤ Mu → 0 < ρ → ρ < 1 → ∑ n ∈ Ns, ∑ i ∈ s n, ∑ p ∈ u n, ‖X n i p‖ ^ 2 ≤ Ea * dyadicGridLength A.G A.R.1 → ∑ n ∈ Ns, ∑ k ∈ t n, ∑ _p ∈ {()}, ‖W n k‖ ^ 2 ≤ Eb * dyadicGridLength A.G A.R.1 → (∀ (y : ℝ), ↑(∑ n ∈ Ns, {c ∈ U n | y ∈ dyadicGridCell A.G c.1 c.2}.card) ≤ Mu) → ∀ {Bc Bd : ℝ}, 0 ≤ Bc → 0 ≤ Bd → (∀ n ∈ Ns, ∀ c' ∈ U n, ∀ d ∈ A.cells, dyadicGridCell A.G c'.1 c'.2 ⊆ dyadicGridCell A.G d.1 d.2 → ⋯) → (∀ n ∈ Ns, ∀ (j : Fin 4), j ≠ a → j ≠ b → j ≠ c → ⋯) → ∀ (sa : N → ℤ × ℤ → ι) (sb : N → ℤ × ℤ → κ'), (∀ n ∈ Ns, ∀ I ∈ U n, sa n I ∈ s n) → (∀ n ∈ Ns, ∀ I ∈ U n, sb n I ∈ t n) → ∃ C ⊆ A.cells, ⋯

Blueprint lines 2426-2444 on the main columns: for indices n with use cells U n in one depth block [b_n, b_n + K) and point multiplicity Σ_n #{I ∈ U n : y ∈ I} ≤ M_u (so the hull roots have total measure Σ_n |Ω_n| ≤ M_u |R|, line 2426), fixed stacks of total energies E_a |R|, E_b |R|, and frozen complements bounded on the active ancestors of the uses within their blocks, there are common cut cells of total length at most ρ |R| after which the squared hull maxima have the joint caps C_{ρ/2} E (1 + log(2 + M_u)) of two_hull_caps (line 2428) and the near-band sums over the uses below no cut cell obey eq:near-band.

theorem TrilinearHT.Auto.near_band_stacksM (κ : LocalKernelClass) {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) : ∃ (Cq : ℝ), 0 ≤ Cq ∧ ∀ {c₀ : ℕ} (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) (fp : bf.FamParams) (K Nd : ℕ), A.DepthWin Nd → 1 ≤ K → A.AncClosed → ∀ {M : Type u_1} (Ms : Finset M) (U : M → Finset (ℤ × ℤ)) (bs : M → ℤ), (∀ m ∈ Ms, U m ⊆ A.cells) → (∀ m ∈ Ms, ∀ c ∈ U m, bs m ≤ c.1 ∧ c.1 < bs m + ↑K) → ∀ {Ka Kb : Type} [inst : Fintype Ka] [inst_1 : Fintype Kb] {ι κ' β : Type} (u : M → Finset β) {a b c : Fin 4}, a ≠ b → a ≠ c → b ≠ c → ∀ (F : M → Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (Y : M → β → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (va : M → ℤ × ℤ → β → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (vb : M → ℤ × ℤ → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (actA : Ka → ℤ × ℤ → Prop) (selA : Ka → ℤ × ℤ → ι) (valA : M → Ka → ι → β → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (actB : Kb → ℤ × ℤ → Prop) (selB : Kb → ℤ × ℤ → κ') (valB : M → Kb → κ' → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))), (∀ m ∈ Ms, ∀ I ∈ U m, ∀ p ∈ u m, (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (va m I p) = ∑ k : Ka with actA k I, (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (valA m k (selA k I) p)) → (∀ m ∈ Ms, ∀ I ∈ U m, (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (vb m I) = ∑ k : Kb with actB k I, (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (valB m k (selB k I))) → ∀ {Ea Eb ρ Mu : ℝ}, 0 ≤ Ea → 0 ≤ Eb → 0 ≤ Mu → 0 < ρ → ρ < 1 → ∑ m ∈ Ms, ∑ k : Ka, ∑ i ∈ Finset.image (selA k) (Finset.filter (actA k) (U m)), ∑ p ∈ u m, ‖⋯‖ ^ 2 ≤ Ea * dyadicGridLength A.G A.R.1 → ∑ m ∈ Ms, ∑ k : Kb, ∑ i ∈ Finset.image (selB k) (Finset.filter (actB k) (U m)), ‖⋯‖ ^ 2 ≤ Eb * dyadicGridLength A.G A.R.1 → (∀ (y : ℝ), ↑(∑ m ∈ Ms, ⋯.card) ≤ Mu) → ∀ {Bc Bd : ℝ}, 0 ≤ Bc → 0 ≤ Bd → (∀ (m : M), ⋯) → ⋯ → ⋯

Blueprint lines 2392-2444 on the main columns (fixed stacks, common cuts, hull maxima and summation): for indices m with use cells U m in one depth block and point multiplicity M_u, varying sides v_a, v_b whose restrictions to each use are the sums of the selected components of their active configurations, and frozen complements bounded on the active ancestors of the uses within their blocks, there are common cut cells of total length at most ρ |R| after which the absolute near-band sums over the uses below no cut cell obey eq:near-band, with the stack energies E_a, E_b of the configurations of each side (paid with the number of configurations of the other side) and the hull mass |K_a| |K_b| M_u |R| of the indices (m, k_a, k_b).

theorem TrilinearHT.Auto.near_band_positionsM (κ : LocalKernelClass) {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) : ∃ (Cq : ℝ), 0 ≤ Cq ∧ ∀ {c₀ : ℕ} (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) (fp : bf.FamParams) (K Nd N : ℕ), A.DepthWin Nd → 1 ≤ K → K ≤ 2 ^ N → A.AncClosed → ∀ {M : Type} (Ms : Finset M) (U : M → Finset (ℤ × ℤ)) (bs : M → ℤ) (off : ℤ × ℤ → ℕ), (∀ m ∈ Ms, U m ⊆ A.cells) → (∀ m ∈ Ms, ∀ I ∈ U m, I.1 = bs m + ↑(off I) ∧ off I < K) → ∀ {β : Type} (u : M → Finset β) {a b c : Fin 4}, a ≠ b → a ≠ c → b ≠ c → ∀ (F : M → Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (Y : M → β → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (Xs : M → β → ℤ → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (Ws : M → ℤ → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {Ea Eb ρ Mu : ℝ}, 0 ≤ Ea → 0 ≤ Eb → 0 ≤ Mu → 0 < ρ → ρ < 1 → ∑ m ∈ Ms, ∑ k : Fin (N + 1), ∑ i ∈ Finset.image (fun (I : ℤ × ℤ) => off I / 2 ^ (↑k + 1)) ({I ∈ U m | posAct N k (off I)}), ∑ p ∈ u m, ‖gluedStack A.G ({I ∈ U m | posAct N k (off I)}) (fun (I : ℤ × ℤ) => off I / 2 ^ (↑k + 1)) (fun (i : ℕ) => posVal (fun (n : ℕ) => Xs m p (bs m + ↑n)) N k i) i‖ ^ 2 ≤ Ea * dyadicGridLength A.G A.R.1 → ∑ m ∈ Ms, ∑ k : Fin (N + 1), ∑ i ∈ Finset.image (fun (I : ℤ × ℤ) => off I / 2 ^ (↑k + 1)) ({I ∈ U m | posAct N k (off I)}), ‖gluedStack A.G ({I ∈ U m | posAct N k (off I)}) (fun (I : ℤ × ℤ) => off I / 2 ^ (↑k + 1)) (fun (i : ℕ) => posVal (fun (n : ℕ) => Ws m (bs m + ↑n)) N k i) i‖ ^ 2 ≤ Eb * dyadicGridLength A.G A.R.1 → (∀ (y : ℝ), ↑(∑ m ∈ Ms, {c ∈ U m | y ∈ dyadicGridCell A.G c.1 c.2}.card) ≤ Mu) → ∀ {Bc Bd : ℝ}, 0 ≤ Bc → 0 ≤ Bd → (∀ m ∈ Ms, ∀ c' ∈ U m, ∀ d ∈ A.cells, dyadicGridCell A.G c'.1 c'.2 ⊆ dyadicGridCell A.G d.1 d.2 → bs m ≤ d.1 → dyadicEnergyAverage A.G ⋯ d ≤ ENNReal.ofReal (Bc ^ 2)) → (∀ m ∈ Ms, ∀ (j : Fin 4), j ≠ a → j ≠ b → j ≠ c → ∀ c' ∈ U m, ∀ (d : ℤ × ℤ), ⋯) → ∃ C ⊆ A.cells, dyadicRootLength A.G (maximalDyadicCells A.G C) ≤ ρ * dyadicGridLength A.G A.R.1 ∧ 7 * ∑ m ∈ Ms, ∑ I ∈ U m with ¬∃ e ∈ C, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G e.1 e.2, ‖↑(dyadicGridLength A.G I.1) * ⋯‖ₑ ≤ 8 * ENNReal.ofReal (Cq * (1 + finiteDepthConstant κ q Nd) * (1 + Real.log (↑K + 2)) * ⋯ * (64 * Bc * Bd)) * ((ENNReal.ofReal ⋯ * ENNReal.ofReal ⋯) ^ (1 / 2) * ENNReal.ofReal (dyadicGridLength A.G A.R.1))

near_band_stacksM with the binary position configurations of two varying sides given by global sequences X_{m,p}(h), W_m(h) on the depths of the uses (offsets off I < K ≤ 2^N from the block starts).

theorem TrilinearHT.Auto.near_band_positions_UM (κ : LocalKernelClass) {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) : ∃ (Cq : ℝ), 0 ≤ Cq ∧ ∀ {c₀ : ℕ} (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) (fp : bf.FamParams) (K Nd N : ℕ), A.DepthWin Nd → 1 ≤ K → K ≤ 2 ^ N → A.AncClosed → ∀ {M : Type} (Ms : Finset M) (U : M → Finset (ℤ × ℤ)) (bs : M → ℤ) (off : ℤ × ℤ → ℕ), (∀ m ∈ Ms, U m ⊆ A.cells) → (∀ m ∈ Ms, ∀ I ∈ U m, I.1 = bs m + ↑(off I) ∧ off I < K) → ∀ {β : Type} (u : M → Finset β) {a b c : Fin 4}, a ≠ b → a ≠ c → b ≠ c → ∀ (F : M → Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (Y : M → β → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (Xs : M → β → ℤ → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (Wv : M → ℤ × ℤ → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {Ea Eb ρ Mu : ℝ}, 0 ≤ Ea → 0 ≤ Eb → 0 ≤ Mu → 0 < ρ → ρ < 1 → ∑ m ∈ Ms, ∑ k : Fin (N + 1), ∑ i ∈ Finset.image (fun (I : ℤ × ℤ) => off I / 2 ^ (↑k + 1)) ({I ∈ U m | posAct N k (off I)}), ∑ p ∈ u m, ‖gluedStack A.G ({I ∈ U m | posAct N k (off I)}) (fun (I : ℤ × ℤ) => off I / 2 ^ (↑k + 1)) (fun (i : ℕ) => posVal (fun (n : ℕ) => Xs m p (bs m + ↑n)) N k i) i‖ ^ 2 ≤ Ea * dyadicGridLength A.G A.R.1 → ∑ m ∈ Ms, ∑ I ∈ U m, ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (Wv m I)‖ ^ 2 ≤ Eb * dyadicGridLength A.G A.R.1 → (∀ (y : ℝ), ↑(∑ m ∈ Ms, {c ∈ U m | y ∈ dyadicGridCell A.G c.1 c.2}.card) ≤ Mu) → ∀ {Bc Bd : ℝ}, 0 ≤ Bc → 0 ≤ Bd → (∀ m ∈ Ms, ∀ c' ∈ U m, ∀ d ∈ A.cells, dyadicGridCell A.G c'.1 c'.2 ⊆ dyadicGridCell A.G d.1 d.2 → bs m ≤ d.1 → dyadicEnergyAverage A.G ⋯ d ≤ ENNReal.ofReal (Bc ^ 2)) → (∀ m ∈ Ms, ∀ (j : Fin 4), j ≠ a → j ≠ b → j ≠ c → ∀ c' ∈ U m, ∀ (d : ℤ × ℤ), ⋯) → ∃ C ⊆ A.cells, dyadicRootLength A.G (maximalDyadicCells A.G C) ≤ ρ * dyadicGridLength A.G A.R.1 ∧ 7 * ∑ m ∈ Ms, ∑ I ∈ U m with ¬∃ e ∈ C, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G e.1 e.2, ‖↑(dyadicGridLength A.G I.1) * ⋯‖ₑ ≤ 8 * ENNReal.ofReal (Cq * (1 + finiteDepthConstant κ q Nd) * (1 + Real.log (↑K + 2)) * ⋯ * (64 * Bc * Bd)) * ((ENNReal.ofReal ⋯ * ENNReal.ofReal ⋯) ^ (1 / 2) * ENNReal.ofReal (dyadicGridLength A.G A.R.1))

near_band_stacksM with the binary position configurations of the banded side given by global sequences X_{m,p}(h) and the depth stacks of local values v_m(I) of a basic U side (the cells of one offset in one block are distinct cells of one depth).

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.stackEA {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {Ω : Type u_1} (Os : Finset Ω) (sA : List (CatCol bf.Vtx)) (mbA : bf.MainBudget sA) (D : Ω → List (Bool × ℕ × Option ℕ)) (N : ℕ) (B EW : ℝ) : ℝ

The stack energy of the banded side over the outer configurations (bandStack_outer).

Equations

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

theorem TrilinearHT.Auto.near_band_actualM (κ : LocalKernelClass) {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) : ∃ (Cq : ℝ), 0 ≤ Cq ∧ ∀ {c₀ : ℕ} (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) (fp : bf.FamParams) (K Nd N : ℕ), A.DepthWin Nd → 1 ≤ K → K ≤ 2 ^ N → A.AncClosed → ∀ {Ω : Type} (Os : Finset Ω) (Gs : Finset bf.Grp) (Bs : Finset ℕ) (k : ℕ) (Act : Finset (ℤ × ℤ)) (U : bf.Grp → ℕ → Finset (ℤ × ℤ)) (off : ℤ × ℤ → ℕ), (∀ (J : ℤ × ℤ) (β m : ℕ), m < K → J.1 = A.R.1 + ↑(K * β + m) → off J = m) → (∀ (g : bf.Grp) (β : ℕ), ∀ I ∈ U g β, I ∈ A.cells ∧ I.1 = A.R.1 + ↑(K * β + off I) ∧ off I < K) → (∀ (g : bf.Grp) (β : ℕ), ∀ I ∈ U g β, I ∈ Act ∧ g ∈ fp.groupsAt I k) → ∀ {Mp : ℝ}, (∀ (y : ℝ), ↑{c ∈ Act | y ∈ dyadicGridCell A.G c.1 c.2}.card ≤ Mp) → ∀ {a b c : Fin 4}, a ≠ b → a ≠ c → b ≠ c → ∀ (sA : List (CatCol bf.Vtx)) (mbA : bf.MainBudget sA) (jc jd : Ω → ℕ) (e : Ω → Bool × ℕ × Option ℕ) (D : Ω → List (Bool × ℕ × Option ℕ)) (Za Zb : bf.Grp → ℤ → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (okA okB : bf.Grp → ℤ × ℤ → Prop) {BA BB : ℝ}, A.VarCap Gs Za okA BA → A.VarCap Gs Zb okB BB → (∀ g ∈ Gs, ∀ (β : ℕ), ∀ I ∈ U g β, ∀ J ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G J.1 J.2 → okA g J ∧ okB g J) → ∀ (Wa : bf.Grp → ℕ → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {EWa : ℝ}, ∑ g ∈ Gs, ∑ β ∈ Bs, ‖(columnL2Restriction (⋃ (J : ℤ × ℤ), ⋃ (_ : ⋯), dyadicGridCell A.G J.1 J.2) ⋯) (Wa g β)‖ ^ 2 ≤ EWa → ∀ (Sa Sb : bf.Grp → ℕ → ℤ → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))), (∀ (g : bf.Grp) (β : ℕ) (h : ℤ), Sa g β h = Za g h - Za g (A.R.1 + ↑(K * β)) + Wa g β) → (∀ (g : bf.Grp) (β : ℕ) (h h' : ℤ), Sb g β h - Sb g β h' = Zb g h - Zb g h') → ∀ {EWb : ℝ}, ∑ g ∈ Gs, ∑ β ∈ Bs, ⋯ ^ 2 ≤ EWb → ∀ Ms ⊆ Os ×ˢ Gs ×ˢ Bs, ∀ (Um : Ω × bf.Grp × ℕ → Finset (ℤ × ℤ)), ⋯ → ⋯

Blueprint lines 2392-2444 for the actual stacks on the main columns (eq:stack-energy, the hull mass of line 2426, the joint caps of line 2428 and the near-band summation): for outer configurations ω (step descriptors e_ω, D_ω and ball levels), groups G and blocks β with uses in a set Act of active cells of multiplicity M_p carrying the group, the banded side (A_{p+1} - A_p) S_a with the global helper bands gBandC of the step after its helper prefix and the rolling side S_a = Z_a - Z_a(b) + W_a, and the untouched side S_b, there is one cut family of root fraction ρ after which the near-band sums over the retained uses are at most the bound of near_band_positionsM with the stack energies stackEA (banded, ≈ P G₀ |R|) and |Ω| (N B_b + E_{W,b}) (untouched, ≈ G₀ |R|), paid with the N + 1 levels of the other side, and the hull mass (N + 1)² |Ω| M_p D |R| (active multiplicity, group count, configurations).

theorem TrilinearHT.Auto.ActiveSetup.VarCap.nonneg {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {γ : Type u_1} {V : Type u_2} [Fintype V] {Gs : Finset γ} {Z : γ → ℤ → ↥(ColumnL2 V)} {ok : γ → ℤ × ℤ → Prop} {B : ℝ} (h : A.VarCap Gs Z ok B) : 0 ≤ B

A variation capacity is nonnegative (the empty family of intervals).

theorem TrilinearHT.Auto.near_coeff_le {P Ea Eb Γa Γb Z c : ℝ} (hP : 1 ≤ P) (hEa0 : 0 ≤ Ea) (hEb0 : 0 ≤ Eb) (hEa : Ea ≤ (P + 2) * Γa) (hEb : Eb ≤ Γb) (hZ : 0 ≤ Z) (hc : 0 ≤ c) : 2 / P * (8 / 7 * Z * √(c * Ea * (c * Eb))) ≤ 4 * Z * c * √(Γa * Γb) / √P

Blueprint line 2438 ("multiplying by the O(P^{-1}) transfer coefficient"): for P ≥ 1, a banded energy at most (P + 2) Γ_a and an untouched energy at most Γ_b, the coefficient 2/P times (8/7) Z √(c E_a · c E_b) is at most 4 Z c √(Γ_a Γ_b) / √P.

theorem TrilinearHT.Auto.near_band_criticalM (κ : LocalKernelClass) {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) : ∃ (Cq : ℝ), 0 ≤ Cq ∧ ∀ {c₀ : ℕ} (A : ActiveSetup κ c₀) (bf : A.BasicFamilies) (fp : bf.FamParams) (K Nd N : ℕ), A.DepthWin Nd → 1 ≤ K → K ≤ 2 ^ N → A.AncClosed → ∀ {Ω : Type} (Os : Finset Ω) (Gs : Finset bf.Grp) (Bs : Finset ℕ) (k : ℕ) (Act : Finset (ℤ × ℤ)) (U : bf.Grp → ℕ → Finset (ℤ × ℤ)) (off : ℤ × ℤ → ℕ), (∀ (J : ℤ × ℤ) (β m : ℕ), m < K → J.1 = A.R.1 + ↑(K * β + m) → off J = m) → (∀ (g : bf.Grp) (β : ℕ), ∀ I ∈ U g β, I ∈ A.cells ∧ I.1 = A.R.1 + ↑(K * β + off I) ∧ off I < K) → (∀ (g : bf.Grp) (β : ℕ), ∀ I ∈ U g β, I ∈ Act ∧ g ∈ fp.groupsAt I k) → ∀ {Mp : ℝ}, (∀ (y : ℝ), ↑{c ∈ Act | y ∈ dyadicGridCell A.G c.1 c.2}.card ≤ Mp) → ∀ {a b c : Fin 4}, a ≠ b → a ≠ c → b ≠ c → ∀ (sA : List (CatCol bf.Vtx)) (mbA : bf.MainBudget sA) (jc jd : Ω → ℕ) (e : Ω → Bool × ℕ × Option ℕ) (D : Ω → List (Bool × ℕ × Option ℕ)) (Za Zb : bf.Grp → ℤ → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (okA okB : bf.Grp → ℤ × ℤ → Prop) {BA BB : ℝ}, A.VarCap Gs Za okA BA → A.VarCap Gs Zb okB BB → (∀ g ∈ Gs, ∀ (β : ℕ), ∀ I ∈ U g β, ∀ J ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G J.1 J.2 → okA g J ∧ okB g J) → ∀ (Wa : bf.Grp → ℕ → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {EWa : ℝ}, ∑ g ∈ Gs, ∑ β ∈ Bs, ‖(columnL2Restriction (⋃ (J : ℤ × ℤ), ⋃ (_ : ⋯), dyadicGridCell A.G J.1 J.2) ⋯) (Wa g β)‖ ^ 2 ≤ EWa → ∀ (Sa Sb : bf.Grp → ℕ → ℤ → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))), (∀ (g : bf.Grp) (β : ℕ) (h : ℤ), Sa g β h = Za g h - Za g (A.R.1 + ↑(K * β)) + Wa g β) → (∀ (g : bf.Grp) (β : ℕ) (h h' : ℤ), Sb g β h - Sb g β h' = Zb g h - Zb g h') → ∀ {EWb : ℝ}, ∑ g ∈ Gs, ∑ β ∈ Bs, ⋯ ^ 2 ≤ EWb → ∀ Ms ⊆ Os ×ˢ Gs ×ˢ Bs, ∀ (Um : Ω × bf.Grp × ℕ → Finset (ℤ × ℤ)), ⋯ → ⋯

Blueprint eq:near-band (lines 2426-2443) for the actual stacks on the main columns: for a fixed near offset o (|o| ≤ 2), the transfer coefficient o/P of the matched bands times the near-band sums of near_band_actualM has, off one cut family of root fraction ρ, the critical absolute bound 4 C_q (1 + C_N) log K (K+2)^{2(q-2)/(q-1)} (64 B_c B_d) G₀ P^{-1/2} |R|, where the banded stack energy is at most (P + 2) Γ_a |R| and the untouched one at most Γ_b |R| (eq:stack-energy), and G₀ = C_{ρ/2} (N + 1) (1 + log(2 + (N+1)² |Ω| M_p D)) √(Γ_a Γ_b) collects the logarithms and the configurations.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.stackEA_le {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {Ω : Type u_1} (Os : Finset Ω) (sA : List (CatCol bf.Vtx)) (mbA : bf.MainBudget sA) (D : Ω → List (Bool × ℕ × Option ℕ)) (N : ℕ) {B EW Cj : ℝ} (hB : 0 ≤ B) (hEW : 0 ≤ EW) (hCj : ∀ ω ∈ Os, fp.bandJumpM sA mbA (D ω).length ≤ Cj) : fp.stackEA Os sA mbA D N B EW ≤ (↑fp.P + 2) * (↑Os.card * (↑N * (2 * B + 16 * (Cj * EW) + 16 * (↑N * (Cj * (↑N * B)))) + EW))

Blueprint eq:stack-energy (line 2397, "Σ ‖stack_a‖² ≤ P G₀ |R|"): the banded stack energy over the outer configurations is P + 2 times a quantity free of P, given a common bound C_j on the product-jump constants of the helper prefixes.

Global transfer steps on the main columns (blueprint lines 2386-2391)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.mainCol_mem_range {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (l : Fin 4) (Mc : ℕ) (s : List (CatCol bf.Vtx)) {I : ℤ × ℤ} {x : bf.Lab ⊕ Fin Mc} (hx : bf.Relevant s x) (hmem : MeasureTheory.MemLp ((dyadicGridCell A.G I.1 I.2).indicator (privateColumnValue (mainScalar Mc (bf.origCols l) s) (mainWeight Mc (bf.origCols l)) x)) 2 MeasureTheory.volume) (hmeas : Measurable (mainScalar Mc (bf.origCols l) s x)) : mainCol A.G Mc (bf.origCols l) s I x ∈ (↑(colRelabel (bf.rv Mc s))).range

On an active cell every main column of a relevant label lies in the range of the relabeling of the relevant labels.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.mainRange_le_range {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (l : Fin 4) (Mc : ℕ) (s : List (CatCol bf.Vtx)) {I : ℤ × ℤ} (hI : I ∈ A.cells) (r : ℕ) (M : bf.Vtx → Prop) : mainRange A.G Mc (bf.origCols l) s I r M ≤ (↑(colRelabel (bf.rv Mc s))).range

On an active cell the main range of a slot lies in the range of the relabeling of the relevant labels of its catalog.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.mainProj_relabel_range {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (l : Fin 4) (Mc : ℕ) (s : List (CatCol bf.Vtx)) {I : ℤ × ℤ} (hI : I ∈ A.cells) (r : ℕ) (M : bf.Vtx → Prop) (z : ↥(ColumnL2 (bf.Lab ⊕ Fin Mc))) : (mainProj A.G Mc (bf.origCols l) s I r M) ((colRelabel (bf.rv Mc s)) ((ContinuousLinearMap.adjoint (colRelabel (bf.rv Mc s))) z)) = (mainProj A.G Mc (bf.origCols l) s I r M) z

On an active cell the main projection does not see the complement of the range of the relabeling: Q = Q ∘ (C C^*).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gProjC_restrict {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (r : ℕ) (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) {I : ℤ × ℤ} (hI : I ∈ A.cells) : columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯ ∘SL fp.gProjC s mb (bf.mainMaskT l fp.Mc s mb r M hM) I.1 = mainProj A.G fp.Mc (bf.origCols l) s I r (M I) ∘SL columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯

On an active cell of the depth, the conjugated global projection with the inherited mask of a main mask is intertwined with the cell main projection by the restriction to the cell (on all inputs).

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

The global transfer step of a descriptor e at the depth h on the main columns: the conjugated global helper pads (rank r_H) on the catalog of the side slot a and the conjugated global pads of the complement slot of the descriptor on its catalog.

Equations

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

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.cellDescM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (G : bf.Grp) (jc jd : ℕ) (I : ℤ × ℤ) (e : Bool × ℕ × Option ℕ) : Bool × ℕ × (Fin fp.P → bf.Vtx → Prop)

The cell masks of a descriptor at a cell.

Equations

• fp.cellDescM G jc jd I e = (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)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gStepM_rel {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (a c d : Fin 4) (rH : ℕ) (G : bf.Grp) (jc jd : ℕ) (e : Bool × ℕ × Option ℕ) {I : ℤ × ℤ} (hI : I ∈ A.cells) : StepRel (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (fp.gStepM cat mbs a c d rH G jc jd e I.1) (fp.toStepM cat a c d rH I (fp.cellDescM G jc jd I e))

On an active cell the global step at its depth is intertwined with the cell step.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gStepsM_rel {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (a c d : Fin 4) (rH : ℕ) (G : bf.Grp) (jc jd : ℕ) (D : List (Bool × ℕ × Option ℕ)) {I : ℤ × ℤ} (hI : I ∈ A.cells) : List.Forall₂ (StepRel (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯)) (List.map (fun (e : Bool × ℕ × Option ℕ) => fp.gStepM cat mbs a c d rH G jc jd e I.1) D) (List.map (fun (e : Bool × ℕ × Option ℕ) => fp.toStepM cat a c d rH I (fp.cellDescM G jc jd I e)) D)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.mergeStepsM_eq_desc {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (a c d : Fin 4) (rH : ℕ) (G : bf.Grp) (jc jd : ℕ) (I : ℤ × ℤ) (t t' : List ℕ) : fp.mergeStepsM cat a c d rH I (fp.slotFiltM G jc I t) (fp.slotFiltM G jd I t') = List.map padStep (List.map (fun (e : Bool × ℕ × Option ℕ) => fp.toStepM cat a c d rH I (fp.cellDescM G jc jd I e)) (fp.mergeDescM jc jd t t'))

The merged transfer steps of the slot filters of a pair of positive chains at a cell are the pad steps of the cell steps of the merged descriptors.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.defects_globalM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (a c d : Fin 4) (rH : ℕ) (G : bf.Grp) (jc jd : ℕ) (t t' : List ℕ) (sel : ℕ → ℕ → Prop) [DecidableRel sel] {I : ℤ × ℤ} (hI : I ∈ A.cells) (x xg : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (hx : ∀ (l : Fin 4), l ≠ a → l ≠ c → l ≠ d → (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (xg l) = (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (x l)) (xa : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (hxa : x a = (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) xa) (e₀ : Bool × ℕ × Option ℕ) : chainDefectSel (fp.Λc I) fp.P a c d x (bf.basicIn fp.Mc c I) (bf.basicIn fp.Mc d I) sel (fp.mergeStepsM cat a c d rH I (fp.slotFiltM G jc I t) (fp.slotFiltM G jd I t')) (x a) = ∑ j ∈ Finset.range (fp.mergeDescM jc jd t t').length, defTerm (fp.Λc I) fp.P a c d xg (bf.gBasic fp.Mc c I.1) (bf.gBasic fp.Mc d I.1) sel (padStep (fp.gStepM cat mbs a c d rH G jc jd ((fp.mergeDescM jc jd t t').getD j e₀) I.1)) (List.map padStep (List.map (fun (e : Bool × ℕ × Option ℕ) => fp.gStepM cat mbs a c d rH G jc jd e I.1) (List.drop (j + 1) (fp.mergeDescM jc jd t t')))) (helpPre fp.P (List.map padStep (List.map (fun (e : Bool × ℕ × Option ℕ) => fp.gStepM cat mbs a c d rH G jc jd e I.1) (List.take j (fp.mergeDescM jc jd t t')))) xa)

Blueprint lines 2386-2391 at one cell, on the main columns: the selected band defects of the transfer steps of a pair of positive chains at an active cell (basic inputs in the two complement slots) are the defect terms of the global steps at the depth of the cell, with the global basic inputs and global values of the side and the spectators restricting to the cell values.

Near band forms on the main columns (blueprint lines 2386-2394)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.norm_Λc_leM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) (x : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : ‖(fp.Λc I) x‖ ≤ localFormUniformConstant κ' * ∏ l : Fin 4, ‖x l‖ / √(dyadicGridLength A.G I.1)

The cell form on the main columns is bounded by the normalized sizes of its inputs.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.norm_Λc_le_restrictM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) (x : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : ‖(fp.Λc I) x‖ ≤ localFormUniformConstant κ' * ∏ l : Fin 4, ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (x l)‖ / √(dyadicGridLength A.G I.1)

The cell form of four slot values is bounded by the normalized sizes of their restrictions to the cell.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.band_sum_leM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) {a b e f : Fin 4} (hab : a ≠ b) (hae : a ≠ e) (haf : a ≠ f) (hbe : b ≠ e) (hbf : b ≠ f) (hef : e ≠ f) (x : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {β : Type u_1} (u : Finset β) (X Y : β → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (W F : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : ‖∑ p ∈ u, (fp.Λc I) (Function.update (Function.update (Function.update (Function.update x f F) a (X p)) b W) e (Y p))‖ ≤ localFormUniformConstant κ' * (‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) F‖ / √(dyadicGridLength A.G I.1) * (‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) W‖ / √(dyadicGridLength A.G I.1)) * (√(∑ p ∈ u, ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (X p)‖ ^ 2) / √(dyadicGridLength A.G I.1)) * (√(∑ p ∈ u, ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (Y p)‖ ^ 2) / √(dyadicGridLength A.G I.1)))

Blueprint lines 2386-2394 at one use: a band sum of the cell form with the paired bands X_p, Y_p in two slots and single values W, F in the other two is bounded by the product of the normalized sizes of F, W and the band families.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.nearFormM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) (a b e f : Fin 4) (z : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {β : Type u_1} (u : Finset β) (X Y : β → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (W F : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : ℂ

The near band form at a use: the band sum of the cell form with the band families X, Y in the slots a, e, the side W in the slot b and the complement F in the slot f.

Equations

• fp.nearFormM I a b e f z u X Y W F = ∑ p ∈ u, (fp.Λc I) (Function.update (Function.update (Function.update (Function.update z f F) a (X p)) b W) e (Y p))

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.nearForm_freezeM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) {a b e f : Fin 4} (_hae : a ≠ e) (_hbe : b ≠ e) (hef : e ≠ f) (haf : a ≠ f) (hbf : b ≠ f) (z : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {β : Type u_1} (u : Finset β) (X Yc Yb : β → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (W Fc Fb : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : fp.nearFormM I a b e f z u X Yc W Fc = fp.nearFormM I a b e f z u X Yb W Fb + fp.nearFormM I a b e f z u X (Yc - Yb) W Fc + fp.nearFormM I a b e f z u X Yc W (Fc - Fb) - fp.nearFormM I a b e f z u X (Yc - Yb) W (Fc - Fb)

The near band form is additive in the band family Y and the complement F.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.nearForm_unflaggedM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) {a b e f : Fin 4} (hab : a ≠ b) (hae : a ≠ e) (haf : a ≠ f) (hbe : b ≠ e) (hbf : b ≠ f) (hef : e ≠ f) (z : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {β : Type u_1} (u : Finset β) (X Yc Yb : β → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (W Fc Fb : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {C₀ SA : ℝ} (hC₀ : 0 ≤ C₀) (hX : √(∑ p ∈ u, ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (X p)‖ ^ 2) / √(dyadicGridLength A.G I.1) ≤ SA) (hFc : ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) Fc‖ / √(dyadicGridLength A.G I.1) ≤ C₀) (hFb : ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) Fb‖ / √(dyadicGridLength A.G I.1) ≤ 2 * C₀) (hYc : √(∑ p ∈ u, ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (Yc p)‖ ^ 2) / √(dyadicGridLength A.G I.1) ≤ C₀) : ‖fp.nearFormM I a b e f z u X Yc W Fc‖ ≤ ‖fp.nearFormM I a b e f z u X Yb W Fb‖ + localFormUniformConstant κ' * (‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) W‖ / √(dyadicGridLength A.G I.1) * SA * (4 * C₀ * (√(∑ p ∈ u, ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (Yc p - Yb p)‖ ^ 2) / √(dyadicGridLength A.G I.1)) + C₀ * (‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (Fc - Fb)‖ / √(dyadicGridLength A.G I.1))))

Blueprint lines 2386-2394 at an unflagged use: the near band form with the current complements is at most the frozen one plus C_κ (‖W‖/s) S_a (4 C₀ δ_Y + C₀ δ_F), where S_a bounds the band family X, C₀ the current complements and 2 C₀ the frozen complement F_b (all normalized on the cell), and δ_Y, δ_F are the normalized freeze differences.

Frozen complements on the main columns (blueprint lines 2386-2389)

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.uoM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (o : ℕ) : Finset ℕ

The offsets' band index sets: the bands p with p + o - 2 in 0..P.

Equations

• fp.uoM o = {p ∈ Finset.range (fp.P + 1) | 2 ≤ p + o ∧ p + o - 2 ≤ fp.P}

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gStM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (a c d : Fin 4) (rH : ℕ) (G : bf.Grp) (jc jd : ℕ) (D : List (Bool × ℕ × Option ℕ)) (j : ℕ) (h : ℤ) : TransferStep ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))

The global transfer step j of the descriptors D at the depth h.

Equations

• fp.gStM cat mbs a c d rH G jc jd D j h = TrilinearHT.Auto.padStep (fp.gStepM cat mbs a c d rH G jc jd (D.getD j (true, 0, none)) h)

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gRestM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (a c d : Fin 4) (rH : ℕ) (G : bf.Grp) (jc jd : ℕ) (D : List (Bool × ℕ × Option ℕ)) (j : ℕ) (h : ℤ) : List (TransferStep ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)))

The global transfer steps after the step j of the descriptors D at the depth h.

Equations

• fp.gRestM cat mbs a c d rH G jc jd D j h = List.map TrilinearHT.Auto.padStep (List.map (fun (e : Bool × ℕ × Option ℕ) => fp.gStepM cat mbs a c d rH G jc jd e h) (List.drop (j + 1) D))

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.YfrM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (a c d : Fin 4) (rH : ℕ) (G : bf.Grp) (jc jd : ℕ) (D : List (Bool × ℕ × Option ℕ)) (j o : ℕ) (h₀ : ℤ) (p : ℕ) : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))

The complement band family of the step j at the offset o with the global steps and global basic inputs at the depth h₀ (current at the depth of a use, frozen at the block start).

Equations

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

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.FfrM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (a c d : Fin 4) (rH : ℕ) (G : bf.Grp) (jc jd : ℕ) (D : List (Bool × ℕ × Option ℕ)) (j : ℕ) (h₀ : ℤ) : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))

The other complement of the step j with the global steps and global basic inputs at the depth h₀.

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.norm_chainVal_cellM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (a c d : Fin 4) (rH : ℕ) (G : bf.Grp) (jc jd : ℕ) (I : ℤ × ℤ) (v : Bool) (D : List (Bool × ℕ × Option ℕ)) (y : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : ‖chainVal fp.P v (List.map padStep (List.map (fun (e : Bool × ℕ × Option ℕ) => fp.toStepM cat a c d rH I (fp.cellDescM G jc jd I e)) D)) y‖ ≤ ‖y‖

The complement value after cell transfer steps is a contraction.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.compBand_besselM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (r : ℕ) (G : bf.Grp) (j : ℕ) (o : Option ℕ) (h : ℤ) (J : ℤ × ℤ) (hJ : J.1 ≤ h) (hJN : J.1 ≤ A.R.1 + ↑A.treeDepth) (y : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : ∑ n ∈ Finset.range (fp.P + 1), ‖(columnL2Restriction (dyadicGridCell A.G J.1 J.2) ⋯) ((padFamC (fun (p : Fin fp.P) => fp.gProjC s mb (bf.mainMaskT l fp.Mc s mb r (fun (c' : ℤ × ℤ) => fp.stepMaskM G j o p c') ⋯) h) (n + 1) - padFamC (fun (p : Fin fp.P) => fp.gProjC s mb (bf.mainMaskT l fp.Mc s mb r (fun (c' : ℤ × ℤ) => fp.stepMaskM G j o p c') ⋯) h) n) y)‖ ^ 2 ≤ ‖(columnL2Restriction (dyadicGridCell A.G J.1 J.2) ⋯) y‖ ^ 2

The bands of the global complement pads of a descriptor at the depth h, restricted to a cell at most that deep, are Bessel.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.sum_uoM_le {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (o : ℕ) (g : ℕ → ℝ) (hg : ∀ (n : ℕ), 0 ≤ g n) : ∑ p ∈ fp.uoM o, g (p + o - 2) ≤ ∑ n ∈ Finset.range (fp.P + 1), g n

Reindexing the offset bands into all bands.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.cur_boundsM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (a c d : Fin 4) (rH : ℕ) (G : bf.Grp) (jc jd : ℕ) (D : List (Bool × ℕ × Option ℕ)) (j o : ℕ) {J : ℤ × ℤ} (hJ : J ∈ A.cells) {C : ℝ} (hsc : ‖bf.basicIn fp.Mc c J‖ ≤ C * √(dyadicGridLength A.G J.1)) (hsd : ‖bf.basicIn fp.Mc d J‖ ≤ C * √(dyadicGridLength A.G J.1)) : ∑ p ∈ fp.uoM o, ‖(columnL2Restriction (dyadicGridCell A.G J.1 J.2) ⋯) (fp.YfrM cat mbs a c d rH G jc jd D j o J.1 p)‖ ^ 2 ≤ C ^ 2 * dyadicGridLength A.G J.1 ∧ ‖(columnL2Restriction (dyadicGridCell A.G J.1 J.2) ⋯) (fp.FfrM cat mbs a c d rH G jc jd D j J.1)‖ ^ 2 ≤ C ^ 2 * dyadicGridLength A.G J.1

Blueprint lines 2388-2389 ("their current local L² norms are bounded: pad bands are orthogonal at one cell, and all inner histories are contractions on bounded basic inputs"), on the main columns: at an active cell where the basic inputs of the two complement slots have normalized size at most C, the current complement bands of every step and offset and the current other complement have restricted squares at most C² |J|.

The global near terms of a use on the main columns (blueprint lines 2386-2394)

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gPreM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (a c d : Fin 4) (rH : ℕ) (G : bf.Grp) (jc jd : ℕ) (D : List (Bool × ℕ × Option ℕ)) (j : ℕ) (h : ℤ) : List (TransferStep ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)))

The global helper prefix: the global steps before the step j.

Equations

• fp.gPreM cat mbs a c d rH G jc jd D j h = List.map TrilinearHT.Auto.padStep (List.map (fun (e : Bool × ℕ × Option ℕ) => fp.gStepM cat mbs a c d rH G jc jd e h) (List.take j D))

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.opAvg_conj_apply {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] {f : V → W} (hf : Function.Injective f) {P : ℕ} (Q : Fin P → ↥(ColumnL2 V) →L[ℂ] ↥(ColumnL2 V)) (z : ↥(ColumnL2 V)) : (opAvg fun (p : Fin P) => colRelabel f ∘SL Q p ∘SL ContinuousLinearMap.adjoint (colRelabel f)) ((colRelabel f) z) = (colRelabel f) ((opAvg Q) z)

An average of conjugated operators on a relabeled vector is the relabeled average.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.padFam_conj_apply {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] {f : V → W} (hf : Function.Injective f) {P : ℕ} (Q : Fin P → ↥(ColumnL2 V) →L[ℂ] ↥(ColumnL2 V)) (n : ℕ) (w : ↥(ColumnL2 V)) : (padFam (fun (p : Fin P) => colRelabel f ∘SL Q p ∘SL ContinuousLinearMap.adjoint (colRelabel f)) n) ((colRelabel f) w) = (colRelabel f) ((padFamC Q n) w)

A pad family of conjugated operators on a relabeled vector is the relabeled pad family.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.helpPre_gPreM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (a c d : Fin 4) (G : bf.Grp) (jc jd : ℕ) (D : List (Bool × ℕ × Option ℕ)) (h : ℤ) (j : ℕ) : j ≤ D.length → ∀ (z : ↥(ColumnL2 (bf.RLab fp.Mc (cat a)))), helpPre fp.P (fp.gPreM cat mbs a c d (fp.Lc + 5) G jc jd D j h) ((colRelabel (bf.rv fp.Mc (cat a))) z) = (colRelabel (bf.rv fp.Mc (cat a))) ((globHist (bf.mainBase fp.Mc (cat a) (mbs a)) (fun (k : ℕ) (p : Fin fp.P) => fp.hMaskM a (cat a) (mbs a) G jc jd (D.getD k (true, 0, none)) p) (lsOf j) h) z)

The global helper prefix of the first j steps on a relabeled vector is the relabeled global history of their helper masks (rank L + 5).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gStM_help_band {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (a c d : Fin 4) (G : bf.Grp) (jc jd : ℕ) (D : List (Bool × ℕ × Option ℕ)) {j : ℕ} (hj : j < D.length) (h : ℤ) (n : ℕ) (z : ↥(ColumnL2 (bf.RLab fp.Mc (cat a)))) : ((fp.gStM cat mbs a c d (fp.Lc + 5) G jc jd D j h).2.1 n) (helpPre fp.P (fp.gPreM cat mbs a c d (fp.Lc + 5) G jc jd D j h) ((colRelabel (bf.rv fp.Mc (cat a))) z)) = (fp.gBandC a (cat a) (mbs a) G jc jd (D.getD j (true, 0, none)) (List.take j D) n h) ((colRelabel (bf.rv fp.Mc (cat a))) z)

The helper bands of the step j after its global helper prefix, on a relabeled vector, are the global helper bands gBandC of the step after its prefix descriptors.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.help_bands_besselM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (a c d : Fin 4) (G : bf.Grp) (jc jd : ℕ) (D : List (Bool × ℕ × Option ℕ)) {j : ℕ} (hj : j < D.length) {I : ℤ × ℤ} (hI : I ∈ A.cells) (xa : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (hxa : xa ∈ (↑(colRelabel (bf.rv fp.Mc (cat a)))).range) (u : Finset ℕ) (hu : u ⊆ Finset.range (fp.P + 1)) : ∑ p ∈ u, ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (((fp.gStM cat mbs a c d (fp.Lc + 5) G jc jd D j I.1).2.1 (p + 1)) (helpPre fp.P (fp.gPreM cat mbs a c d (fp.Lc + 5) G jc jd D j I.1) xa) - ((fp.gStM cat mbs a c d (fp.Lc + 5) G jc jd D j I.1).2.1 p) (helpPre fp.P (fp.gPreM cat mbs a c d (fp.Lc + 5) G jc jd D j I.1) xa))‖ ^ 2 ≤ ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) xa‖ ^ 2

At an active cell of the depth, the helper bands of a relabeled side value after the global helper prefix have total restricted square at most the restricted square of the side value.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.nearTermGM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (rH : ℕ) (a c d : Fin 4) (G : bf.Grp) (jc jd : ℕ) (D : List (Bool × ℕ × Option ℕ)) (I : ℤ × ℤ) (h : ℤ) (xg : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (xa : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (j o : ℕ) : ℂ

The near band sum of the step j at the offset o of a descriptor list, with the global steps, basic inputs and spectators at the depth h, in the cell form of I.

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.nearTermGM_eq {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (rH : ℕ) {a b c d : Fin 4} (hab : a ≠ b) (hac : a ≠ c) (had : a ≠ d) (hbc' : b ≠ c) (hbd : b ≠ d) (hcd : c ≠ d) (G : bf.Grp) (jc jd : ℕ) (D : List (Bool × ℕ × Option ℕ)) (I : ℤ × ℤ) (h : ℤ) (xg : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (xa : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (j o : ℕ) (z : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : fp.nearTermGM cat mbs rH a c d G jc jd D I h xg xa j o = fp.nearFormM I a b (if (fp.gStM cat mbs a c d rH G jc jd D j h).1 = true then c else d) (if (fp.gStM cat mbs a c d rH G jc jd D j h).1 = true then d else c) z (fp.uoM o) (fun (p : ℕ) => ((fp.gStM cat mbs a c d rH G jc jd D j h).2.1 (p + 1)) (helpPre fp.P (fp.gPreM cat mbs a c d rH G jc jd D j h) xa) - ((fp.gStM cat mbs a c d rH G jc jd D j h).2.1 p) (helpPre fp.P (fp.gPreM cat mbs a c d rH G jc jd D j h) xa)) (fun (p : ℕ) => fp.YfrM cat mbs a c d rH G jc jd D j o h p) (xg b) (fp.FfrM cat mbs a c d rH G jc jd D j h)

The global near band sum of the step j at the offset o is the near band form with the slots e (the complement slot of the step) and f (the other complement slot), the helper bands of the side, the complement band family Y and the other complement F at the depth h.

Freezing at one use on the main columns (blueprint lines 2386-2394)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.nearForm_current_leM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) {a b e f : Fin 4} (hab : a ≠ b) (hae : a ≠ e) (haf : a ≠ f) (hbe : b ≠ e) (hbf : b ≠ f) (hef : e ≠ f) (z : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {β : Type u_1} (u : Finset β) (X Yc : β → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (W Fc : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {C₀ SA : ℝ} (hC₀ : 0 ≤ C₀) (hX : √(∑ p ∈ u, ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (X p)‖ ^ 2) / √(dyadicGridLength A.G I.1) ≤ SA) (hFc : ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) Fc‖ / √(dyadicGridLength A.G I.1) ≤ C₀) (hYc : √(∑ p ∈ u, ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (Yc p)‖ ^ 2) / √(dyadicGridLength A.G I.1) ≤ C₀) : ‖fp.nearFormM I a b e f z u X Yc W Fc‖ ≤ localFormUniformConstant κ' * (‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) W‖ / √(dyadicGridLength A.G I.1) * SA * C₀ ^ 2)

Blueprint line 2393 at a flagged use, on the main columns: the near band form with the current complements is at most C_κ (‖W‖/s) S_a C₀².

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.near_useM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) {a b c d : Fin 4} (hab : a ≠ b) (hac : a ≠ c) (had : a ≠ d) (hbc' : b ≠ c) (hbd : b ≠ d) (hcd : c ≠ d) (G : bf.Grp) (jc jd : ℕ) (D : List (Bool × ℕ × Option ℕ)) {I : ℤ × ℤ} (hI : I ∈ A.cells) (xg : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (xa : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (hxa : xa ∈ (↑(colRelabel (bf.rv fp.Mc (cat a)))).range) {j : ℕ} (hj : j < D.length) (o : ℕ) (z : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (Yb : ℕ → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (Fb : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (Unfl : Prop) {C₀ : ℝ} (hC₀ : 0 ≤ C₀) (hFc : ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (fp.FfrM cat mbs a c d (fp.Lc + 5) G jc jd D j I.1)‖ / √(dyadicGridLength A.G I.1) ≤ C₀) (hYc : √(∑ p ∈ fp.uoM o, ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (fp.YfrM cat mbs a c d (fp.Lc + 5) G jc jd D j o I.1 p)‖ ^ 2) / √(dyadicGridLength A.G I.1) ≤ C₀) (hFb : Unfl → ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) Fb‖ / √(dyadicGridLength A.G I.1) ≤ 2 * C₀) : ‖fp.nearTermGM cat mbs (fp.Lc + 5) a c d G jc jd D I I.1 xg xa j o‖ ≤ (if Unfl then ‖fp.nearFormM I a b (if (fp.gStM cat mbs a c d (fp.Lc + 5) G jc jd D j I.1).1 = true then c else d) (if (fp.gStM cat mbs a c d (fp.Lc + 5) G jc jd D j I.1).1 = true then d else c) z (fp.uoM o) (fun (p : ℕ) => ((fp.gStM cat mbs a c d (fp.Lc + 5) G jc jd D j I.1).2.1 (p + 1)) (helpPre fp.P (fp.gPreM cat mbs a c d (fp.Lc + 5) G jc jd D j I.1) xa) - ((fp.gStM cat mbs a c d (fp.Lc + 5) G jc jd D j I.1).2.1 p) (helpPre fp.P (fp.gPreM cat mbs a c d (fp.Lc + 5) G jc jd D j I.1) xa)) Yb (xg b) Fb‖ else 0) + localFormUniformConstant κ' * (‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (xg b)‖ / √(dyadicGridLength A.G I.1) * (‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) xa‖ / √(dyadicGridLength A.G I.1)) * (4 * C₀ * (√(∑ p ∈ fp.uoM o, ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (fp.YfrM cat mbs a c d (fp.Lc + 5) G jc jd D j o I.1 p - Yb p)‖ ^ 2) / √(dyadicGridLength A.G I.1)) + C₀ * (‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (fp.FfrM cat mbs a c d (fp.Lc + 5) G jc jd D j I.1 - Fb)‖ / √(dyadicGridLength A.G I.1)) + if Unfl then 0 else C₀ ^ 2))

Blueprint lines 2386-2394 at one use, on the main columns: the global near band sum of the step j at the offset o (helper bands after the global helper prefix, rank L + 5) is at most, if the use is unflagged, the near band form with the frozen band family Y_b and frozen complement F_b, plus C_κ (‖W‖/s)(‖x_a‖/s)(4 C₀ δ_Y + C₀ δ_F + [flagged] C₀²), where the current complement bands and other complement have normalized sizes at most C₀ and the frozen other complement at most 2 C₀ on unflagged uses.