Section 14.4: Fixed stacks for the two varying sides

This file was automatically generated by Claude.

Formalization of blueprint Section 14, "The two-side estimate" (sec:sides), subsection 4, "Fixed stacks for the two varying sides" (lines 2392-2424) of blueprint/formalization_blueprint.tex.

theorem TrilinearHT.Auto.sum_sqrt_mul_le_ennreal {ι : Type u_1} (s : Finset ι) (x y : ι → ENNReal) : ∑ i ∈ s, (x i * y i) ^ (1 / 2) ≤ (∑ i ∈ s, x i) ^ (1 / 2) * (∑ i ∈ s, y i) ^ (1 / 2)

Pointwise Cauchy–Schwarz for hull maxima in ℝ≥0∞: Σ_ν √(m_{a,ν} m_{b,ν}) ≤ √(Σ_ν m_{a,ν}) √(Σ_ν m_{b,ν}).

Rademacher randomization of the stacks (blueprint lines 2421-2423)

@[reducible, inline]

abbrev TrilinearHT.Auto.SignPattern {ι : Type u_1} (s : Finset ι) : Type u_1

The sign patterns on a finite set.

Equations

• TrilinearHT.Auto.SignPattern s = ↥s.powerset

@[instance_reducible]

instance TrilinearHT.Auto.instMeasurableSpaceSignPattern {ι : Type u_1} (s : Finset ι) : MeasurableSpace (SignPattern s)

Equations

• TrilinearHT.Auto.instMeasurableSpaceSignPattern s = ⊤

instance TrilinearHT.Auto.instMeasurableSingletonClassSignPattern {ι : Type u_1} (s : Finset ι) : MeasurableSingletonClass (SignPattern s)

noncomputable def TrilinearHT.Auto.unifMeasure (Ω : Type u_1) [Fintype Ω] [MeasurableSpace Ω] : MeasureTheory.Measure Ω

The uniform probability on a finite type with the discrete σ-algebra.

Equations

• TrilinearHT.Auto.unifMeasure Ω = (↑(Fintype.card Ω))⁻¹ • MeasureTheory.Measure.count

theorem TrilinearHT.Auto.lintegral_unifMeasure {Ω : Type u_1} [Fintype Ω] [MeasurableSpace Ω] [MeasurableSingletonClass Ω] (f : Ω → ENNReal) : ∫⁻ (ω : Ω), f ω ∂unifMeasure Ω = (↑(Fintype.card Ω))⁻¹ * ∑ ω : Ω, f ω

instance TrilinearHT.Auto.instIsProbabilityMeasureUnifMeasureOfNonemptyOfMeasurableSingletonClass {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] [MeasurableSpace Ω] [MeasurableSingletonClass Ω] : MeasureTheory.IsProbabilityMeasure (unifMeasure Ω)

theorem TrilinearHT.Auto.piece_random_bound (κ : LocalKernelClass) {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) {C4 : ℝ} (hC4 : 0 ≤ C4) : ∃ (Cq : ℝ), 0 ≤ Cq ∧ ∀ (G : RealDyadicGrid) (K Nd : ℕ) (d₀ : ℤ) (T : ShortBlockTree G K) (z : Fin 4 → ℝ → ℝ), (∀ (j : Fin 4), Measurable (z j)) → ∀ (sv : Fin 4 → ℝ), (∀ (j : Fin 4), 0 ≤ sv j) → (∀ (j : Fin 4), ∀ L ∈ T.leaves, ∫⁻ (y : ℝ) in dyadicGridCell G L.1 L.2, ‖z j y‖ₑ ^ 2 ≤ ENNReal.ofReal (sv j ^ 2 * dyadicGridLength G L.1)) → ∀ {Ω : Type} [inst : Fintype Ω] [Nonempty Ω] [inst_2 : MeasurableSpace Ω] [MeasurableSingletonClass Ω] (zσ : Fin 4 → Ω → ℝ → ℂ), (∀ (j : Fin 4) (ω : Ω), Measurable (zσ j ω)) → (∀ (j : Fin 4) (y : ℝ), ((↑(Fintype.card Ω))⁻¹ * ∑ ω : Ω, ‖zσ j ω y‖ₑ ^ 4) ^ (1 / 4) ≤ ENNReal.ofReal C4 * ‖z j y‖ₑ) → ∀ (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 : ℤ × ℤ) (ω : Ω), ‖ε I ω‖ ≤ 1) → ∀ (Tc : ℤ × ℤ → ℂ), (∀ I ∈ cells, ((↑(Fintype.card Ω))⁻¹ * ∑ ω : Ω, ε I ω * localProgressionForm (dyadicGridLength G I.1) (kernel I) fun (j : Fin 4) => zσ j ω) = Tc I) → ‖∑ I ∈ cells, ↑(dyadicGridLength G I.1) * Tc 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: on a short-block piece, any randomization on a finite uniform probability space with fourth moments bounded by C₄ times deterministic sizes, and signed expectations equal to given cell quantities T_I, bounds Σ_I |I| T_I by the short-block constant.

Aligned binary prefix positions (blueprint lines 2400-2404)

def TrilinearHT.Auto.bitPrefix (n k : ℕ) : ℕ

The prefix of n above the bit k (the bits below k cleared).

Equations

• TrilinearHT.Auto.bitPrefix n k = n / 2 ^ k * 2 ^ k

def TrilinearHT.Auto.posInt (n k : ℕ) : ℕ × ℕ

The position of level k of the prefix [0, n]: the aligned interval [bitPrefix n (k+1), bitPrefix n (k+1) + 2^k] (used when the bit k of n is set).

Equations

• TrilinearHT.Auto.posInt n k = (TrilinearHT.Auto.bitPrefix n (k + 1), TrilinearHT.Auto.bitPrefix n (k + 1) + 2 ^ k)

theorem TrilinearHT.Auto.bitPrefix_zero (n : ℕ) : bitPrefix n 0 = n

theorem TrilinearHT.Auto.bitPrefix_of_lt {n N : ℕ} (h : n < 2 ^ N) : bitPrefix n N = 0

theorem TrilinearHT.Auto.bitPrefix_succ (n k : ℕ) : bitPrefix n k = bitPrefix n (k + 1) + if n.testBit k = true then 2 ^ k else 0

Consecutive prefixes differ by the bit k times 2^k.

theorem TrilinearHT.Auto.prefix_telescope {M : Type u_1} [AddCommGroup M] (W : ℕ → M) (b n N : ℕ) (hn : n < 2 ^ N) : W (b + n) = W b + ∑ k ∈ Finset.range N, if n.testBit k = true then W (b + (posInt n k).2) - W (b + (posInt n k).1) else 0

Blueprint lines 2400-2402: W_{b+n} = W_b + Σ_k [bit k] (W_{b+t_k} - W_{b+r_k}) over the aligned positions of the levels k < N (for n < 2^N), at most one interval at each length.

theorem TrilinearHT.Auto.posInt_le {n k : ℕ} (hk : n.testBit k = true) : (posInt n k).1 ≤ (posInt n k).2 ∧ (posInt n k).2 ≤ n

The positions lie inside the prefix [0, n] when the bit is set.

Configurations of positions (blueprint lines 2402-2404, 2423)

def TrilinearHT.Auto.posComp {M : Type u_1} [AddCommGroup M] (W : ℕ → M) (b n N : ℕ) (k : Fin (N + 1)) : M

The component of level k ≤ N of W_{b+n}: the base W_b at level N, otherwise the jump over the aligned position of level k when the bit k of n is set.

Equations

• TrilinearHT.Auto.posComp W b n N k = if ↑k = N then W b else if n.testBit ↑k = true then W (b + (TrilinearHT.Auto.posInt n ↑k).2) - W (b + (TrilinearHT.Auto.posInt n ↑k).1) else 0

theorem TrilinearHT.Auto.sum_posComp {M : Type u_1} [AddCommGroup M] (W : ℕ → M) (b n N : ℕ) (hn : n < 2 ^ N) : ∑ k : Fin (N + 1), posComp W b n N k = W (b + n)

Blueprint lines 2400-2402: the components of all levels sum to W_{b+n} (for n < 2^N).

Glued stacks (blueprint lines 2409-2411)

noncomputable def TrilinearHT.Auto.selUnion (G : RealDyadicGrid) {ι : Type u_2} (U : Finset (ℤ × ℤ)) (sel : ℤ × ℤ → ι) (i : ι) : Set ℝ

The union of the cells of U selecting the index i.

Equations

• TrilinearHT.Auto.selUnion G U sel i = ⋃ I ∈ U, ⋃ (_ : sel I = i), TrilinearHT.Auto.dyadicGridCell G I.1 I.2

theorem TrilinearHT.Auto.selUnion_measurable (G : RealDyadicGrid) {ι : Type u_2} (U : Finset (ℤ × ℤ)) (sel : ℤ × ℤ → ι) (i : ι) : MeasurableSet (selUnion G U sel i)

noncomputable def TrilinearHT.Auto.gluedStack (G : RealDyadicGrid) {V : Type u_1} [Fintype V] {ι : Type u_2} (U : Finset (ℤ × ℤ)) (sel : ℤ × ℤ → ι) (val : ι → ↥(ColumnL2 V)) (i : ι) : ↥(ColumnL2 V)

Blueprint line 2410 ("a fixed stack component may be restricted to the union of use cells selecting it"): the glued stack of the values val i, each restricted to the union of the cells selecting i.

Equations

• TrilinearHT.Auto.gluedStack G U sel val i = (TrilinearHT.Auto.columnL2Restriction (TrilinearHT.Auto.selUnion G U sel i) ⋯) (val i)

theorem TrilinearHT.Auto.cell_sub_selUnion (G : RealDyadicGrid) {ι : Type u_2} {U : Finset (ℤ × ℤ)} (sel : ℤ × ℤ → ι) {I : ℤ × ℤ} (hI : I ∈ U) : dyadicGridCell G I.1 I.2 ⊆ selUnion G U sel (sel I)

theorem TrilinearHT.Auto.gluedStack_restrict (G : RealDyadicGrid) {V : Type u_1} [Fintype V] {ι : Type u_2} {U : Finset (ℤ × ℤ)} (sel : ℤ × ℤ → ι) (val : ι → ↥(ColumnL2 V)) {I : ℤ × ℤ} (hI : I ∈ U) : (columnL2Restriction (dyadicGridCell G I.1 I.2) ⋯) (gluedStack G U sel val (sel I)) = (columnL2Restriction (dyadicGridCell G I.1 I.2) ⋯) (val (sel I))

Blueprint line 2410 ("which preserves its value there"): on a cell of U the glued stack at its selected index is the selected value.

theorem TrilinearHT.Auto.gluedStack_norm_sq_le (G : RealDyadicGrid) {V : Type u_1} [Fintype V] {ι : Type u_2} (U : Finset (ℤ × ℤ)) (sel : ℤ × ℤ → ι) (val : ι → ↥(ColumnL2 V)) (i : ι) {Ω : Set ℝ} (hΩ : MeasurableSet Ω) (hsub : selUnion G U sel i ⊆ Ω) : ‖gluedStack G U sel val i‖ ^ 2 ≤ ‖(columnL2Restriction Ω hΩ) (val i)‖ ^ 2

Blueprint line 2410 ("and decreases its norm"): the glued stack is bounded by its value on any larger set.

Expanding the two varying sides over positions (blueprint lines 2400-2404, 2423)

theorem TrilinearHT.Auto.multilinear_update_two_finsum {E : Type u_1} [AddCommGroup E] [Module ℂ E] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => E) ℂ) {a b : Fin 4} (hab : a ≠ b) (x : Fin 4 → E) {α : Type u_2} {β : Type u_3} (sa : Finset α) (sb : Finset β) (f : α → E) (g : β → E) : Λ (Function.update (Function.update x a (∑ i ∈ sa, f i)) b (∑ j ∈ sb, g j)) = ∑ i ∈ sa, ∑ j ∈ sb, Λ (Function.update (Function.update x a (f i)) b (g j))

A multilinear form is biadditive over finite sums in two distinct slots.

Binary position configurations of a varying side (blueprint lines 2400-2411)

def TrilinearHT.Auto.posVal {E : Type u_1} [AddCommGroup E] (W : ℕ → E) (N : ℕ) (k : Fin (N + 1)) (q : ℕ) : E

The component of level k ≤ N at the position index q of a sequence on offsets: the base value at level N, otherwise the jump over the aligned interval [q 2^(k+1), q 2^(k+1) + 2^k].

Equations

• TrilinearHT.Auto.posVal W N k q = if ↑k = N then W 0 else W (q * 2 ^ (↑k + 1) + 2 ^ ↑k) - W (q * 2 ^ (↑k + 1))

def TrilinearHT.Auto.posAct (N : ℕ) (k : Fin (N + 1)) (n : ℕ) : Prop

The level k is active at the offset n: the base level, or the bit k of n is set.

Equations

• TrilinearHT.Auto.posAct N k n = (↑k = N ∨ n.testBit ↑k = true)

@[instance_reducible]

instance TrilinearHT.Auto.instDecidablePosAct (N : ℕ) (k : Fin (N + 1)) (n : ℕ) : Decidable (posAct N k n)

Equations

• TrilinearHT.Auto.instDecidablePosAct N k n = id inferInstance

theorem TrilinearHT.Auto.posComp_eq {E : Type u_1} [AddCommGroup E] (W : ℕ → E) (n N : ℕ) (k : Fin (N + 1)) : posComp W 0 n N k = if posAct N k n then posVal W N k (n / 2 ^ (↑k + 1)) else 0

theorem TrilinearHT.Auto.pos_rep {E : Type u_1} [AddCommGroup E] (W : ℕ → E) {n N : ℕ} (hn : n < 2 ^ N) : W n = ∑ k : Fin (N + 1) with posAct N k n, posVal W N k (n / 2 ^ (↑k + 1))

Blueprint lines 2400-2402: a sequence at an offset n < 2^N is the sum of the components of its active levels at their position indices.

theorem TrilinearHT.Auto.posEnd_le {n N : ℕ} {k : Fin (N + 1)} (hk : ↑k ≠ N) (ha : posAct N k n) : n / 2 ^ (↑k + 1) * 2 ^ (↑k + 1) + 2 ^ ↑k ≤ n

The right end of the position of an active level below the base lies at or before the offset.

theorem TrilinearHT.Auto.selUnion_sub_anc (G : RealDyadicGrid) {ι : Type u_1} [DecidableEq ι] (U : Finset (ℤ × ℤ)) (sel : ℤ × ℤ → ι) (d : ι → ℤ) (hd : ∀ I ∈ U, d (sel I) ≤ I.1) (q : ι) : selUnion G U sel q ⊆ ⋃ J ∈ Finset.image (fun (I : ℤ × ℤ) => ancAt G I (d q)) ({I ∈ U | sel I = q}), dyadicGridCell G J.1 J.2

The union of the cells selecting an index lies in the union of their ancestors at any depth at most theirs.

Variation capacities and the energies of position stacks (blueprint lines 2408-2411)

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

A family of global sequences Z_g (g ∈ Gs) has variation capacity B over certified cells when, for any family of disjoint depth intervals (r_i, t_i] below the root and any families of certified active cells at the right endpoints, the restricted jumps have total square at most B (blueprint lem:variation).

Equations

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

theorem TrilinearHT.Auto.posIoc_disjoint {k q q' : ℕ} (hqq : q ≠ q') : Disjoint (Finset.Ioc (q * 2 ^ (k + 1)) (q * 2 ^ (k + 1) + 2 ^ k)) (Finset.Ioc (q' * 2 ^ (k + 1)) (q' * 2 ^ (k + 1) + 2 ^ k))

The intervals of the positions of one level are disjoint.

noncomputable def TrilinearHT.Auto.ActiveSetup.posEc {κ' : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ' c₀) (U' : Finset (ℤ × ℤ)) (off : ℤ × ℤ → ℕ) (k bo q : ℕ) : Finset (ℤ × ℤ)

The ancestors at the right end of the position q of level k (block offset bo) of the cells of U' selecting it.

Equations

• A.posEc U' off k bo q = Finset.image (fun (I : ℤ × ℤ) => TrilinearHT.Auto.ancAt A.G I (A.R.1 + ↑(bo + (q * 2 ^ (k + 1) + 2 ^ k)))) ({I ∈ U' | off I / 2 ^ (k + 1) = q})

theorem TrilinearHT.Auto.ActiveSetup.posAnc_energy {κ' : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ' c₀) (hanc : A.AncClosed) {γ : Type u_1} {V : Type u_2} [Fintype V] (Gs : Finset γ) (Z : γ → ℤ → ↥(ColumnL2 V)) (ok : γ → ℤ × ℤ → Prop) {B : ℝ} (hcap : A.VarCap Gs Z ok B) {K N : ℕ} (k : Fin (N + 1)) (hk : ↑k ≠ 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) : ∑ g ∈ Gs, ∑ β ∈ Bs, ∑ q ∈ Finset.image (fun (I : ℤ × ℤ) => off I / 2 ^ (↑k + 1)) ({I ∈ U g β | posAct N k (off I)}), ‖(columnL2Restriction (⋃ J ∈ A.posEc ({I ∈ U g β | posAct N k (off I)}) off (↑k) (K * β) q, dyadicGridCell A.G J.1 J.2) ⋯) (Z g (A.R.1 + ↑(K * β + (q * 2 ^ (↑k + 1) + 2 ^ ↑k))) - Z g (A.R.1 + ↑(K * β + q * 2 ^ (↑k + 1))))‖ ^ 2 ≤ B

Blueprint lines 2408-2411 (eq:stack-energy for the positions of one level below the base, on the ancestors at the right ends): if the family Z_g has variation capacity B, the jumps of Z_g over the positions of a level k < N used by the cells of all groups and blocks, restricted to the ancestors at the right ends of the cells selecting them, have total square at most B.

theorem TrilinearHT.Auto.ActiveSetup.posStack_energy {κ' : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ' c₀) (hanc : A.AncClosed) {γ : Type u_1} {V : Type u_2} [Fintype V] (Gs : Finset γ) (Z : γ → ℤ → ↥(ColumnL2 V)) (ok : γ → ℤ × ℤ → Prop) {B : ℝ} (hcap : A.VarCap Gs Z ok B) {K N : ℕ} (k : Fin (N + 1)) (hk : ↑k ≠ 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') : ∑ g ∈ Gs, ∑ β ∈ Bs, ∑ q ∈ Finset.image (fun (I : ℤ × ℤ) => off I / 2 ^ (↑k + 1)) ({I ∈ U g β | posAct N k (off I)}), ‖gluedStack A.G ({I ∈ U g β | posAct N k (off I)}) (fun (I : ℤ × ℤ) => off I / 2 ^ (↑k + 1)) (fun (q : ℕ) => posVal (fun (n : ℕ) => Sb g β (A.R.1 + ↑(K * β + n))) N k q) q‖ ^ 2 ≤ B

Blueprint lines 2408-2411 (eq:stack-energy for the positions of one level below the base): if the side values of block β have the jumps of a family Z_g of variation capacity B, the glued position stacks of a level k < N over the uses of all groups and blocks have total square at most B (the positions of one level are disjoint depth intervals, also across the blocks).

theorem TrilinearHT.Auto.norm_sub_sq_le_two_mul {E : Type u_1} [SeminormedAddCommGroup E] (a b : E) : ‖a - b‖ ^ 2 ≤ 2 * ‖a‖ ^ 2 + 2 * ‖b‖ ^ 2

‖a - b‖² ≤ 2 ‖a‖² + 2 ‖b‖².

theorem TrilinearHT.Auto.norm_add_sq_le_two_mul {E : Type u_1} [SeminormedAddCommGroup E] (a b : E) : ‖a + b‖ ^ 2 ≤ 2 * ‖a‖ ^ 2 + 2 * ‖b‖ ^ 2

‖a + b‖² ≤ 2 ‖a‖² + 2 ‖b‖².

Banded stacks of the transferred side (blueprint lines 2408-2409, 2414-2423)

theorem TrilinearHT.Auto.band_split {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {P : ℕ} (At Ar : ℕ → E →L[ℂ] E) (Er : E →L[ℂ] E) (hbes : ∀ (y : E), ∑ p ∈ Finset.range (P + 1), ‖(At (p + 1) - At p) y‖ ^ 2 ≤ ‖y‖ ^ 2) (hcomm : ∀ (n : ℕ), Er ∘SL At n = At n ∘SL Er) (St Sr : E) : ∑ p ∈ Finset.range (P + 1), ‖Er ((At (p + 1) - At p) St - (Ar (p + 1) - Ar p) Sr)‖ ^ 2 ≤ 2 * ‖Er (St - Sr)‖ ^ 2 + 8 * ∑ n ∈ Finset.range (P + 2), ‖Er ((At n - Ar n) Sr)‖ ^ 2

Blueprint lines 2408-2409 ("on the banded side pay at most P + 1 indices"): with pad families A_n at the two depths t, r, Bessel bands at t, and a restriction E commuting with the operators at t, the band jumps of a side S split into the side jump and the pad jumps on the left value: Σ_p ‖E(B_p(t) S_t - B_p(r) S_r)‖² ≤ 2 ‖E(S_t - S_r)‖² + 8 Σ_{n ≤ P+1} ‖E((A_n(t) - A_n(r)) S_r)‖².

theorem TrilinearHT.Auto.rows_fixed_inputs {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {Q : Type u_2} {Q' : Type u_3} [DecidableEq Q'] (Qs : Finset Q) (F : Q → E →L[ℂ] E) (used : Q → Prop) [DecidablePred used] (π : Q → Q') (Y : Q → E) (X : Q' → E) (hloc : ∀ q ∈ Qs, used q → (F q) (Y q) = (F q) (X (π q))) {Cj : ℝ} (hJ : ∀ s ⊆ Qs, ∀ (x : E), ∑ q ∈ s, ‖(F q) x‖ ^ 2 ≤ Cj * ‖x‖ ^ 2) : ∑ q ∈ Qs with used q, ‖(F q) (Y q)‖ ^ 2 ≤ Cj * ∑ q' ∈ Finset.image π (Finset.filter used Qs), ‖X q'‖ ^ 2

Blueprint lines 2420-2423 (one fixed inner interval for all outer positions using it): if each used outer row acts on its inner jump as on a common fixed input X_{π q}, and the rows of any subfamily are Bessel with constant C_j, the used rows have total square at most C_j Σ_{q'} ‖X_{q'}‖².

theorem TrilinearHT.Auto.band_block {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {P : ℕ} (Qs : Finset ℕ) (Eq : ℕ → E →L[ℂ] E) (At Ar : ℕ → ℕ → E →L[ℂ] E) (hbes : ∀ q ∈ Qs, ∀ (y : E), ∑ p ∈ Finset.range (P + 1), ‖(At q (p + 1) - At q p) y‖ ^ 2 ≤ ‖y‖ ^ 2) (hcomm : ∀ q ∈ Qs, ∀ (n : ℕ), Eq q ∘SL At q n = At q n ∘SL Eq q) {Cj : ℝ} (hJ : ∀ (n : ℕ), ∀ s ⊆ Qs, ∀ (x : E), ∑ q ∈ s, ‖(Eq q) ((At q n - Ar q n) x)‖ ^ 2 ≤ Cj * ‖x‖ ^ 2) (St Sr Dz : ℕ → E) (W W' : E) (hSr : ∀ q ∈ Qs, Sr q = Dz q + W) (hW : ∀ q ∈ Qs, ∀ (n : ℕ), (Eq q) ((At q n - Ar q n) W) = (Eq q) ((At q n - Ar q n) W')) {Nl : ℕ} (Y : ℕ → ℕ → E) (hY : ∀ q ∈ Qs, Dz q = ∑ k' ∈ Finset.range Nl, Y q k') (used : ℕ → ℕ → Prop) [(k' : ℕ) → DecidablePred (used k')] (hYu : ∀ (q k' : ℕ), ¬used k' q → Y q k' = 0) (π : ℕ → ℕ → ℕ) (X : ℕ → ℕ → E) (hloc : ∀ (k' q : ℕ), q ∈ Qs → used k' q → ∀ (n : ℕ), (Eq q) ((At q n - Ar q n) (Y q k')) = (Eq q) ((At q n - Ar q n) (X k' (π k' q)))) : ∑ q ∈ Qs, ∑ p ∈ Finset.range (P + 1), ‖(Eq q) ((At q (p + 1) - At q p) (St q) - (Ar q (p + 1) - Ar q p) (Sr q))‖ ^ 2 ≤ 2 * ∑ q ∈ Qs, ‖(Eq q) (St q - Sr q)‖ ^ 2 + 16 * (↑P + 2) * (Cj * ‖W'‖ ^ 2) + 16 * (↑P + 2) * (↑Nl * (Cj * ∑ k' ∈ Finset.range Nl, ∑ q' ∈ Finset.image (π k') (Finset.filter (used k') Qs), ‖X k' q'‖ ^ 2))

Blueprint lines 2414-2423 in one block: the banded position jumps of the transferred side S_h = Z_h - Z_b + W over the positions q of one level are bounded by the side jumps, the jumps of the P + 2 pad families on the fixed block input W' (equal to W under the rows), and the jumps on the fixed inner inputs X_{k',q'} of the binary expansion of Z_{r_q} - Z_b.

theorem TrilinearHT.Auto.union_commute {V : Type u_1} [Fintype V] (G : RealDyadicGrid) (Ec : Finset (ℤ × ℤ)) {d : ℤ} (hd : ∀ J ∈ Ec, J.1 = d) (T : ↥(ColumnL2 V) →L[ℂ] ↥(ColumnL2 V)) (hT : ∀ J ∈ Ec, columnL2Restriction (dyadicGridCell G J.1 J.2) ⋯ ∘SL T = T ∘SL columnL2Restriction (dyadicGridCell G J.1 J.2) ⋯) : columnL2Restriction (⋃ J ∈ Ec, dyadicGridCell G J.1 J.2) ⋯ ∘SL T = T ∘SL columnL2Restriction (⋃ J ∈ Ec, dyadicGridCell G J.1 J.2) ⋯

An operator commuting with the restrictions to the cells of a family of one depth commutes with the restriction to their union.

theorem TrilinearHT.Auto.restrict_sandwich {V : Type u_1} [Fintype V] {Ω C D : Set ℝ} (hΩ : MeasurableSet Ω) (hC : MeasurableSet C) (hD : MeasurableSet D) (hΩC : Ω ⊆ C) (hCD : C ⊆ D) (T : ↥(ColumnL2 V) →L[ℂ] ↥(ColumnL2 V)) (hT : columnL2Restriction C hC ∘SL T = T ∘SL columnL2Restriction C hC) (y : ↥(ColumnL2 V)) : (columnL2Restriction Ω hΩ) (T y) = (columnL2Restriction Ω hΩ) (T ((columnL2Restriction D hD) y))

For Ω ⊆ C ⊆ D and an operator commuting with the restriction to C, the restriction to Ω of the output does not see the input outside D.

theorem TrilinearHT.Auto.ancAt_mono (G : RealDyadicGrid) (I : ℤ × ℤ) {d₁ d₂ : ℤ} (h₂₁ : d₂ ≤ d₁) (h₁ : d₁ ≤ I.1) : dyadicGridCell G (ancAt G I d₁).1 (ancAt G I d₁).2 ⊆ dyadicGridCell G (ancAt G I d₂).1 (ancAt G I d₂).2

Ancestors of one cell at nested depths are nested.

theorem TrilinearHT.Auto.posIoc_disjoint_shift (c : ℕ) {k q q' : ℕ} (hqq : q ≠ q') : Disjoint (Finset.Ioc (c + q * 2 ^ (k + 1)) (c + (q * 2 ^ (k + 1) + 2 ^ k))) (Finset.Ioc (c + q' * 2 ^ (k + 1)) (c + (q' * 2 ^ (k + 1) + 2 ^ k)))

The position intervals of one level, shifted by a block offset, are disjoint.

theorem TrilinearHT.Auto.ActiveSetup.mem_posEc {κ' : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ' c₀) {U' : Finset (ℤ × ℤ)} {off : ℤ × ℤ → ℕ} {k bo q : ℕ} {J : ℤ × ℤ} : J ∈ A.posEc U' off k bo q ↔ ∃ I ∈ U', off I / 2 ^ (k + 1) = q ∧ J = ancAt A.G I (A.R.1 + ↑(bo + (q * 2 ^ (k + 1) + 2 ^ k)))

noncomputable def TrilinearHT.Auto.ActiveSetup.posLeft {κ' : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ' c₀) (U' : Finset (ℤ × ℤ)) (off : ℤ × ℤ → ℕ) (k bo : ℕ) : Finset (ℤ × ℤ)

The pseudo-uses of a level: the ancestors of the uses at the left ends of their positions.

Equations

• A.posLeft U' off k bo = Finset.image (fun (I : ℤ × ℤ) => TrilinearHT.Auto.ancAt A.G I (A.R.1 + ↑(bo + off I / 2 ^ (k + 1) * 2 ^ (k + 1)))) U'