Rademacher–Menshov estimates and nested projection products

This file was automatically generated by Codex.

The finite Rademacher–Menshov argument decomposes variable prefixes into dyadic blocks and combines orthogonal block energy with the triangle inequality. We develop its Hilbert-space row formulation, for finite families of bounded linear maps whose squared output norms sum to at most the squared input norm. The intended applications are noncommuting products of nested orthogonal projections and their disjoint-interval jumps, as in blueprint lem:prefix. All statements and local definitions are independent of the column construction.

The classical logarithmic maximal inequality is recorded in Terence Tao, 247A Lecture Notes 2, page 31, exercises Q14–Q15: https://www.math.ucla.edu/~tao/247a.1.06f/notes2.pdf. The exact row/product formulation and constants follow blueprint/formalization_blueprint.tex, lines 508–535. The explicit logarithmic horizon and numerical restart bounds implement lem:compression, lines 567 and 579, for arbitrary real budgets and layer counts.

noncomputable def TrilinearHT.Auto.finiteRowNorm {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] (f : ι → F) : ℝ

The Hilbertian norm of a finite family of outputs, also for normed outputs.

Equations

• TrilinearHT.Auto.finiteRowNorm f = ‖WithLp.toLp 2 f‖

theorem TrilinearHT.Auto.finiteRowNorm_nonneg {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] (f : ι → F) : 0 ≤ finiteRowNorm f

theorem TrilinearHT.Auto.finiteRowNorm_sq {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] (f : ι → F) : finiteRowNorm f ^ 2 = ∑ i : ι, ‖f i‖ ^ 2

theorem TrilinearHT.Auto.finiteRowNorm_add_le {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] (f g : ι → F) : finiteRowNorm (f + g) ≤ finiteRowNorm f + finiteRowNorm g

theorem TrilinearHT.Auto.rowSquareBound_restrict {𝕜 : Type u_1} {H : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (B : ι → H →L[𝕜] F) (C : ℝ) (hB : ∀ (h : H), ∑ i : ι, ‖(B i) h‖ ^ 2 ≤ C ^ 2 * ‖h‖ ^ 2) (p : ι → Prop) [DecidablePred p] (h : H) : ∑ i : ι, ‖(if p i then B i else 0) h‖ ^ 2 ≤ C ^ 2 * ‖h‖ ^ 2

Removing rows preserves their square-sum contraction estimate.

theorem TrilinearHT.Auto.orthogonalBlock_energy {𝕜 : Type u_1} {H : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (s : Finset ι) (v : ι → H) (hv : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → inner 𝕜 (v i) (v j) = 0) : ‖∑ i ∈ s, v i‖ ^ 2 = ∑ i ∈ s, ‖v i‖ ^ 2

Finite Pythagoras for the orthogonal vectors used in dyadic blocks.

theorem TrilinearHT.Auto.finiteRowNorm_le_of_sq_le {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] (f : ι → F) {C : ℝ} (hC : 0 ≤ C) (h : ∑ i : ι, ‖f i‖ ^ 2 ≤ C ^ 2) : finiteRowNorm f ≤ C

theorem TrilinearHT.Auto.finiteRowNorm_disjoint_sq {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] (f g : ι → F) (h : ∀ (i : ι), f i = 0 ∨ g i = 0) : finiteRowNorm (f + g) ^ 2 = finiteRowNorm f ^ 2 + finiteRowNorm g ^ 2

theorem TrilinearHT.Auto.finiteRowNorm_binary_step {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] (f g w : ι → F) {C E₀ E₁ : ℝ} (hC : 0 ≤ C) (hE₀ : 0 ≤ E₀) (hE₁ : 0 ≤ E₁) (hd : ∀ (i : ι), f i = 0 ∨ g i = 0) (hf : finiteRowNorm f ≤ C * √E₀) (hg : finiteRowNorm g ≤ C * √E₁) (hw : finiteRowNorm w ≤ √E₀) : finiteRowNorm (f + g + w) ≤ (C + 1) * √(E₀ + E₁)

The two half-prefixes occupy disjoint rows; completing the left half costs one additional unit of the dyadic logarithmic bound.

theorem TrilinearHT.Auto.prefix_binary_split {H : Type u_1} [AddCommMonoid H] (v : ℕ → H) (M n : ℕ) : ∑ j ∈ Finset.range n, v j = (if n ≤ M then ∑ j ∈ Finset.range n, v j else ∑ j ∈ Finset.range (n - M), v (M + j)) + if n ≤ M then 0 else ∑ j ∈ Finset.range M, v j

Binary splitting is the recursive form of one dyadic block at each length.

theorem TrilinearHT.Auto.prefixRowBound_pow_two {𝕜 : Type u_1} {H : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (k : ℕ) (v : ℕ → H) (hv : ∀ i < 2 ^ k, ∀ j < 2 ^ k, i ≠ j → inner 𝕜 (v i) (v j) = 0) (B : ι → H →L[𝕜] F) (hB : ∀ (h : H), ∑ i : ι, ‖(B i) h‖ ^ 2 ≤ ‖h‖ ^ 2) (n : ι → ℕ) (hn : ∀ (i : ι), n i ≤ 2 ^ k) : (finiteRowNorm fun (i : ι) => (B i) (∑ j ∈ Finset.range (n i), v j)) ≤ (↑k + 1) * √(∑ j ∈ Finset.range (2 ^ k), ‖v j‖ ^ 2)

The finite row version of Rademacher–Menshov for a power-of-two horizon. The binary induction implements the dyadic decomposition in lem:prefix.

theorem TrilinearHT.Auto.prefixRowBound {𝕜 : Type u_1} {H : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (N : ℕ) (v : ℕ → H) (hv : ∀ i < N, ∀ j < N, i ≠ j → inner 𝕜 (v i) (v j) = 0) (B : ι → H →L[𝕜] F) (hB : ∀ (h : H), ∑ i : ι, ‖(B i) h‖ ^ 2 ≤ ‖h‖ ^ 2) (n : ι → ℕ) (hn : ∀ (i : ι), n i ≤ N) : (finiteRowNorm fun (i : ι) => (B i) (∑ j ∈ Finset.range (n i), v j)) ≤ (↑(Nat.clog 2 N) + 1) * √(∑ j ∈ Finset.range N, ‖v j‖ ^ 2)

Arbitrary finite prefixes have the exact dyadic logarithmic row bound. Zero-padding to the next power of two leaves every relevant vector and energy unchanged.

theorem TrilinearHT.Auto.prefixRowLog_eq_ceil (N : ℕ) : ↑(Nat.clog 2 N) + 1 = ↑⌈Real.logb 2 ↑N⌉₊ + 1

Exact identification of the dyadic depth with the ceiling logarithm used for L_T in blueprint lem:prefix.

theorem TrilinearHT.Auto.nestedProjection_comp_reverse {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (P Q : H →L[𝕜] H) (hP : IsStarProjection P) (hQ : IsStarProjection Q) (hPQ : P ∘SL Q = P) : Q ∘SL P = P

theorem TrilinearHT.Auto.starProjection_norm_apply_le {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (P : H →L[𝕜] H) (hP : IsStarProjection P) (g : H) : ‖P g‖ ≤ ‖g‖

noncomputable def TrilinearHT.Auto.projectionIncrement {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (P : ℕ → H →L[𝕜] H) : ℕ → H →L[𝕜] H

The initial projection followed by successive projection differences.

Equations

• TrilinearHT.Auto.projectionIncrement P 0 = P 0
• TrilinearHT.Auto.projectionIncrement P n.succ = P (n + 1) - P n

theorem TrilinearHT.Auto.sum_projectionIncrement {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (P : ℕ → H →L[𝕜] H) (n : ℕ) : ∑ j ∈ Finset.range (n + 1), projectionIncrement P j = P n

theorem TrilinearHT.Auto.sum_projectionIncrement_apply {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (P : ℕ → H →L[𝕜] H) (n : ℕ) (g : H) : ∑ j ∈ Finset.range (n + 1), (projectionIncrement P j) g = (P n) g

theorem TrilinearHT.Auto.projectionIncrement_fixed {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (P : ℕ → H →L[𝕜] H) (T : ℕ) (hP : ∀ n ≤ T, IsStarProjection (P n)) (hnest : ∀ i ≤ T, ∀ j ≤ T, i ≤ j → P i ∘SL P j = P i) {n m : ℕ} (hnm : n ≤ m) (hm : m ≤ T) : P m ∘SL projectionIncrement P n = projectionIncrement P n

theorem TrilinearHT.Auto.projectionIncrement_inner_eq_zero_of_lt {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (P : ℕ → H →L[𝕜] H) (T : ℕ) (hP : ∀ n ≤ T, IsStarProjection (P n)) (hnest : ∀ i ≤ T, ∀ j ≤ T, i ≤ j → P i ∘SL P j = P i) {i j : ℕ} (hij : i < j) (hj : j ≤ T) (g h : H) : inner 𝕜 ((projectionIncrement P i) g) ((projectionIncrement P j) h) = 0

theorem TrilinearHT.Auto.projectionIncrement_orthogonal {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (P : ℕ → H →L[𝕜] H) (T : ℕ) (hP : ∀ n ≤ T, IsStarProjection (P n)) (hnest : ∀ i ≤ T, ∀ j ≤ T, i ≤ j → P i ∘SL P j = P i) (g : H) (i : ℕ) : i < T + 1 → ∀ j < T + 1, i ≠ j → inner 𝕜 ((projectionIncrement P i) g) ((projectionIncrement P j) g) = 0

theorem TrilinearHT.Auto.projectionIncrement_energy_le {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (P : ℕ → H →L[𝕜] H) (T : ℕ) (hP : ∀ n ≤ T, IsStarProjection (P n)) (hnest : ∀ i ≤ T, ∀ j ≤ T, i ≤ j → P i ∘SL P j = P i) (g : H) : ∑ j ∈ Finset.range (T + 1), ‖(projectionIncrement P j) g‖ ^ 2 ≤ ‖g‖ ^ 2

noncomputable def TrilinearHT.Auto.projectionPrefixConstant (T : ℕ) : ℝ

The exact constant L_T = 1 + ceil(log₂(T+1)) in the source.

Equations

• TrilinearHT.Auto.projectionPrefixConstant T = ↑(Nat.clog 2 (T + 1)) + 1

theorem TrilinearHT.Auto.projectionPrefixConstant_one_le (T : ℕ) : 1 ≤ projectionPrefixConstant T

theorem TrilinearHT.Auto.projectionPrefixConstant_eq_ceil (T : ℕ) : projectionPrefixConstant T = 1 + ↑⌈Real.logb 2 (↑T + 1)⌉₊

theorem TrilinearHT.Auto.nestedProjection_prefix_rows {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] {F : Type u_3} {ι : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (P : ℕ → H →L[𝕜] H) (T : ℕ) (hP : ∀ n ≤ T, IsStarProjection (P n)) (hnest : ∀ i ≤ T, ∀ j ≤ T, i ≤ j → P i ∘SL P j = P i) (B : ι → H →L[𝕜] F) (hB : ∀ (h : H), ∑ i : ι, ‖(B i) h‖ ^ 2 ≤ ‖h‖ ^ 2) (n : ι → ℕ) (hn : ∀ (i : ι), n i ≤ T) (g : H) : (finiteRowNorm fun (i : ι) => (B i) ((P (n i)) g)) ≤ projectionPrefixConstant T * ‖g‖

The single-layer nested-projection row estimate with arbitrary row times, the first case of blueprint eq:prefix, lines 508–514.

theorem TrilinearHT.Auto.finiteRowNorm_smul {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_3} {ι : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (c : 𝕜) (f : ι → F) : (finiteRowNorm fun (i : ι) => c • f i) = ‖c‖ * finiteRowNorm f

noncomputable def TrilinearHT.Auto.nestedProjectionProduct {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (P : ℕ → ℕ → H →L[𝕜] H) : ℕ → ℕ → H →L[𝕜] H

Products are ordered with layer zero on the right; different layers need not commute.

Equations

• TrilinearHT.Auto.nestedProjectionProduct P 0 x✝ = ContinuousLinearMap.id 𝕜 H
• TrilinearHT.Auto.nestedProjectionProduct P m.succ x✝ = P m x✝ ∘SL TrilinearHT.Auto.nestedProjectionProduct P m x✝

theorem TrilinearHT.Auto.nestedProjectionProduct_prefix_rows {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] {F : Type u_3} {ι : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (P : ℕ → ℕ → H →L[𝕜] H) (T m : ℕ) (hP : ∀ l < m, ∀ n ≤ T, IsStarProjection (P l n)) (hnest : ∀ l < m, ∀ i ≤ T, ∀ j ≤ T, i ≤ j → P l i ∘SL P l j = P l i) (B : ι → H →L[𝕜] F) (hB : ∀ (h : H), ∑ i : ι, ‖(B i) h‖ ^ 2 ≤ ‖h‖ ^ 2) (n : ι → ℕ) (hn : ∀ (i : ι), n i ≤ T) (g : H) : (finiteRowNorm fun (i : ι) => (B i) ((nestedProjectionProduct P m (n i)) g)) ≤ projectionPrefixConstant T ^ m * ‖g‖

Blueprint eq:prefix: the logarithmic row estimate for arbitrary noncommuting products of nested orthogonal projection layers.

theorem TrilinearHT.Auto.nestedProjectionProduct_prefix_rows_sq {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] {F : Type u_3} {ι : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [Fintype ι] (P : ℕ → ℕ → H →L[𝕜] H) (T m : ℕ) (hP : ∀ l < m, ∀ n ≤ T, IsStarProjection (P l n)) (hnest : ∀ l < m, ∀ i ≤ T, ∀ j ≤ T, i ≤ j → P l i ∘SL P l j = P l i) (B : ι → H →L[𝕜] F) (hB : ∀ (h : H), ∑ i : ι, ‖(B i) h‖ ^ 2 ≤ ‖h‖ ^ 2) (n : ι → ℕ) (hn : ∀ (i : ι), n i ≤ T) (g : H) : ∑ i : ι, ‖(B i) ((nestedProjectionProduct P m (n i)) g)‖ ^ 2 ≤ projectionPrefixConstant T ^ (2 * m) * ‖g‖ ^ 2

theorem TrilinearHT.Auto.finiteRowNorm_mono {F : Type u_3} {ι : Type u_4} [NormedAddCommGroup F] [Fintype ι] (f g : ι → F) (h : ∀ (i : ι), ‖f i‖ ≤ ‖g i‖) : finiteRowNorm f ≤ finiteRowNorm g

theorem TrilinearHT.Auto.nestedProjectionProduct_jump_split {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (P : ℕ → ℕ → H →L[𝕜] H) (m r t : ℕ) (g : H) : (nestedProjectionProduct P (m + 1) t) g - (nestedProjectionProduct P (m + 1) r) g = (P m t) ((nestedProjectionProduct P m t) g - (nestedProjectionProduct P m r) g) + (P m t - P m r) ((nestedProjectionProduct P m r) g)

theorem TrilinearHT.Auto.nestedProjectionProduct_jump_rows_of_bessel {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] {ι : Type u_3} [Fintype ι] (P : ℕ → ℕ → H →L[𝕜] H) (T m : ℕ) (hP : ∀ l < m, ∀ n ≤ T, IsStarProjection (P l n)) (hnest : ∀ l < m, ∀ i ≤ T, ∀ j ≤ T, i ≤ j → P l i ∘SL P l j = P l i) (r t : ι → ℕ) (hr : ∀ (i : ι), r i ≤ T) (ht : ∀ (i : ι), t i ≤ T) (hB : ∀ l < m, ∀ (h : H), ∑ i : ι, ‖(P l (t i) - P l (r i)) h‖ ^ 2 ≤ ‖h‖ ^ 2) (g : H) : (finiteRowNorm fun (i : ι) => (nestedProjectionProduct P m (t i)) g - (nestedProjectionProduct P m (r i)) g) ≤ (∑ l ∈ Finset.range m, projectionPrefixConstant T ^ l) * ‖g‖

Product telescoping with Bessel difference rows. The dyadic prefix estimate controls each right-hand product; left-hand factors are contractions.

theorem TrilinearHT.Auto.projectionPrefixConstant_sum_pow_le (T m : ℕ) : ∑ l ∈ Finset.range m, projectionPrefixConstant T ^ l ≤ ↑m * projectionPrefixConstant T ^ (m - 1)

theorem TrilinearHT.Auto.nestedProjectionProduct_jump_rows_sq_of_bessel {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] {ι : Type u_3} [Fintype ι] (P : ℕ → ℕ → H →L[𝕜] H) (T m : ℕ) (hP : ∀ l < m, ∀ n ≤ T, IsStarProjection (P l n)) (hnest : ∀ l < m, ∀ i ≤ T, ∀ j ≤ T, i ≤ j → P l i ∘SL P l j = P l i) (r t : ι → ℕ) (hr : ∀ (i : ι), r i ≤ T) (ht : ∀ (i : ι), t i ≤ T) (hB : ∀ l < m, ∀ (h : H), ∑ i : ι, ‖(P l (t i) - P l (r i)) h‖ ^ 2 ≤ ‖h‖ ^ 2) (g : H) : ∑ i : ι, ‖(nestedProjectionProduct P m (t i)) g - (nestedProjectionProduct P m (r i)) g‖ ^ 2 ≤ ↑m ^ 2 * projectionPrefixConstant T ^ (2 * (m - 1)) * ‖g‖ ^ 2

The exact square-sum jump constant once the layer differences are Bessel rows.

theorem TrilinearHT.Auto.projection_successive_differences_bessel {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (P : ℕ → H →L[𝕜] H) (T : ℕ) (hP : ∀ n ≤ T, IsStarProjection (P n)) (hnest : ∀ i ≤ T, ∀ j ≤ T, i ≤ j → P i ∘SL P j = P i) (h : H) : ∑ n : Fin T, ‖(P (↑n + 1) - P ↑n) h‖ ^ 2 ≤ ‖h‖ ^ 2

Successive differences of a nested orthogonal projection family are Bessel rows.

theorem TrilinearHT.Auto.nestedProjectionProduct_successive_jumps {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (P : ℕ → ℕ → H →L[𝕜] H) (T m : ℕ) (hP : ∀ l < m, ∀ n ≤ T, IsStarProjection (P l n)) (hnest : ∀ l < m, ∀ i ≤ T, ∀ j ≤ T, i ≤ j → P l i ∘SL P l j = P l i) (g : H) : ∑ n : Fin T, ‖(nestedProjectionProduct P m (↑n + 1)) g - (nestedProjectionProduct P m ↑n) g‖ ^ 2 ≤ ↑m ^ 2 * projectionPrefixConstant T ^ (2 * (m - 1)) * ‖g‖ ^ 2

Blueprint eq:product-jump, lines 515–519: the square sum of successive product jumps is at most m² L_T^(2(m-1)) times the input energy.

theorem TrilinearHT.Auto.orthogonalIndexedBlocks_energy_le {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {α : Type u_3} {ι : Type u_4} [Fintype ι] (s : Finset α) (v : α → H) (hv : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → inner 𝕜 (v i) (v j) = 0) (A : ι → Finset α) (hdis : ∀ (i j : ι), i ≠ j → Disjoint (A i) (A j)) (hsub : ∀ (i : ι), A i ⊆ s) : ∑ i : ι, ‖∑ j ∈ A i, v j‖ ^ 2 ≤ ∑ j ∈ s, ‖v j‖ ^ 2

theorem TrilinearHT.Auto.sum_projectionIncrement_Ioc {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (P : ℕ → H →L[𝕜] H) {r t : ℕ} (hrt : r ≤ t) (g : H) : ∑ j ∈ Finset.Ioc r t, (projectionIncrement P j) g = (P t) g - (P r) g

theorem TrilinearHT.Auto.projection_interval_differences_bessel {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] {ι : Type u_3} [Fintype ι] (P : ℕ → H →L[𝕜] H) (T : ℕ) (hP : ∀ n ≤ T, IsStarProjection (P n)) (hnest : ∀ i ≤ T, ∀ j ≤ T, i ≤ j → P i ∘SL P j = P i) (r t : ι → ℕ) (hrt : ∀ (i : ι), r i ≤ t i) (ht : ∀ (i : ι), t i ≤ T) (hdis : ∀ (i j : ι), i ≠ j → Disjoint (Finset.Ioc (r i) (t i)) (Finset.Ioc (r j) (t j))) (g : H) : ∑ i : ι, ‖(P (t i) - P (r i)) g‖ ^ 2 ≤ ‖g‖ ^ 2

Differences over disjoint index intervals are Bessel rows, including empty intervals.

theorem TrilinearHT.Auto.projectionPrefixConstant_ceil_pow_le {b : ℝ} (hb : 2 ≤ b) {p : ℕ} (hp : 1 ≤ p) : projectionPrefixConstant ⌈b ^ p⌉₊ ≤ ↑p * Real.logb 2 b + 3

A power-sized transition count has a logarithmic prefix constant, with explicit allowance for both ceiling operations.

noncomputable def TrilinearHT.Auto.projectionRestartTime (D : ℝ) (m : ℕ) : ℕ

The source transition horizon for a real column budget and a natural number of projection layers (lem:compression, lines 567 and 579).

Equations

• TrilinearHT.Auto.projectionRestartTime D m = ⌈(2 * D * (↑m + 1)) ^ (128 * (m + 1) ^ 2)⌉₊

theorem TrilinearHT.Auto.projectionRestartTime_prefix_le {D : ℝ} (hD : 2 ≤ D) {m : ℕ} (hm : 1 ≤ m) : projectionPrefixConstant (projectionRestartTime D m) ≤ 129 * (↑m + 1) ^ 2 * Real.logb 2 (2 * D * (↑m + 1))

The first explicit bound in the source's numerical contraction check.

theorem TrilinearHT.Auto.logb_two_le_half {b : ℝ} (hb : 4 ≤ b) : Real.logb 2 b ≤ b / 2

A convenient elementary bound for binary logarithms above four.

theorem TrilinearHT.Auto.projectionRestartTime_prefix_le_fourth {D : ℝ} (hD : 2 ≤ D) {m : ℕ} (hm : 1 ≤ m) : projectionPrefixConstant (projectionRestartTime D m) ≤ (2 * D * (↑m + 1)) ^ 4

The source logarithmic prefix bound is dominated by the fourth power of b = 2 D (m+1), uniformly for every nonempty product.

theorem TrilinearHT.Auto.projectionRestartTime_factor_lt_half {D : ℝ} (hD : 2 ≤ D) {m : ℕ} (hm : 1 ≤ m) : 16 * D ^ 32 * ↑m ^ 2 * projectionPrefixConstant (projectionRestartTime D m) ^ (2 * m) / ↑(projectionRestartTime D m) < 1 / 2

Blueprint lem:compression, line 579: the prescribed transition horizon makes the common restart contraction factor strictly less than one half.

theorem TrilinearHT.Auto.projectionRestartTime_prefix_polynomial {D : ℝ} {m : ℕ} (hD : 2 ≤ D) (hm : 1 ≤ m) : projectionPrefixConstant (projectionRestartTime D m) ≤ 258 * (↑m + 1) ^ 3 * Real.log (2 * D)

Blueprint lem:compression, line 597: the exact restart horizon has prefix constant at most a cubic layer-count factor times log (2D).

noncomputable def TrilinearHT.Auto.operatorSubproduct {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] (P : ℕ → H →L[𝕜] H) (σ : ℕ → Bool) : ℕ → H →L[𝕜] H

An ordered subproduct, omitting the factors selected as false.

Equations

• TrilinearHT.Auto.operatorSubproduct P σ 0 = ContinuousLinearMap.id 𝕜 H
• TrilinearHT.Auto.operatorSubproduct P σ n.succ = if σ n = true then P n ∘SL TrilinearHT.Auto.operatorSubproduct P σ n else TrilinearHT.Auto.operatorSubproduct P σ n

noncomputable def TrilinearHT.Auto.operatorComplementProduct {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] (P : ℕ → H →L[𝕜] H) (θ : ℕ → Bool) : ℕ → H →L[𝕜] H

An ordered product with any designated factors replaced by their complements.

Equations

• TrilinearHT.Auto.operatorComplementProduct P θ 0 = ContinuousLinearMap.id 𝕜 H
• TrilinearHT.Auto.operatorComplementProduct P θ n.succ = (if θ n = true then ContinuousLinearMap.id 𝕜 H - P n else P n) ∘SL TrilinearHT.Auto.operatorComplementProduct P θ n

theorem TrilinearHT.Auto.operatorSubproduct_congr {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] (P : ℕ → H →L[𝕜] H) (n : ℕ) {σ τ : ℕ → Bool} (h : ∀ j < n, σ j = τ j) : operatorSubproduct P σ n = operatorSubproduct P τ n

theorem TrilinearHT.Auto.operatorSubproduct_update_prefix {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] (P : ℕ → H →L[𝕜] H) (σ : ℕ → Bool) (n : ℕ) (b : Bool) : operatorSubproduct P (Function.update σ n b) n = operatorSubproduct P σ n

theorem TrilinearHT.Auto.operatorSubproduct_succ_update {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] (P : ℕ → H →L[𝕜] H) (σ : ℕ → Bool) (n : ℕ) (b : Bool) : operatorSubproduct P (Function.update σ n b) (n + 1) = if b = true then P n ∘SL operatorSubproduct P σ n else operatorSubproduct P σ n

theorem TrilinearHT.Auto.finiteRowNorm_sub_le {ι : Type u_3} {F : Type u_4} [Fintype ι] [NormedAddCommGroup F] (f g : ι → F) : finiteRowNorm (f - g) ≤ finiteRowNorm f + finiteRowNorm g

theorem TrilinearHT.Auto.operatorComplementProduct_rows_bound {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] {ι : Type u_3} {F : Type u_4} [Fintype ι] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (P : ι → ℕ → H →L[𝕜] H) (θ : ℕ → Bool) (m : ℕ) (z : H) (B : ι → H →L[𝕜] F) {M : ℝ} (hM : 0 ≤ M) (hsub : ∀ (σ : ℕ → Bool), (finiteRowNorm fun (i : ι) => (B i) ((operatorSubproduct (P i) σ m) z)) ≤ M) : (finiteRowNorm fun (i : ι) => (B i) ((operatorComplementProduct (P i) θ m) z)) ≤ 2 ^ m * M

Blueprint lem:compression, line 597: expanding complements costs at most 2^m in the finite row norm. Only a uniform bound for all ordered subproducts is required; no commutation of the factors is assumed.