Section 4: Column projections and bounded-height frequencies

This file was automatically generated by Claude.

Formalization of blueprint Section 4, "Column projections and bounded-height frequencies" (sec:columns, lines 469-623) of blueprint/formalization_blueprint.tex.

@[reducible, inline]

abbrev TrilinearHT.Auto.ColumnHilbert (V : Type u_1) : Type u_1

The source Hilbert space has one physical coordinate and one distinct private coordinate for each label (column-data, lines 470–474).

Equations

• TrilinearHT.Auto.ColumnHilbert V = EuclideanSpace ℂ (Option V)

@[reducible, inline]

noncomputable abbrev TrilinearHT.Auto.ColumnL2 (V : Type u_1) [Fintype V] : AddSubgroup (ℝ →ₘ[MeasureTheory.volume] ColumnHilbert V)

Global L2 space in which cell-supported column projections act.

Equations

• TrilinearHT.Auto.ColumnL2 V = MeasureTheory.Lp (TrilinearHT.Auto.ColumnHilbert V) 2 MeasureTheory.volume

noncomputable def TrilinearHT.Auto.privateColumnValue {V : Type u_1} (φ : V → ℝ → ℂ) (ε : V → ℝ) (v : V) (y : ℝ) : ColumnHilbert V

The augmented column (φᵥ(y), sqrt(εᵥ) eᵥ) from blueprint line 473.

Equations

• TrilinearHT.Auto.privateColumnValue φ ε v y = φ v y • EuclideanSpace.single none 1 + ↑√(ε v) • EuclideanSpace.single (some v) 1

theorem TrilinearHT.Auto.privateColumnValue_physical {V : Type u_1} (φ : V → ℝ → ℂ) (ε : V → ℝ) (v : V) (y : ℝ) : (privateColumnValue φ ε v y).ofLp none = φ v y

theorem TrilinearHT.Auto.privateColumnValue_private {V : Type u_1} (φ : V → ℝ → ℂ) (ε : V → ℝ) (v w : V) (y : ℝ) : (privateColumnValue φ ε v y).ofLp (some w) = if w = v then ↑√(ε v) else 0

theorem TrilinearHT.Auto.privateColumnValue_measurable {V : Type u_1} [Finite V] (φ : V → ℝ → ℂ) (ε : V → ℝ) (v : V) (hφ : Measurable (φ v)) : Measurable (privateColumnValue φ ε v)

structure TrilinearHT.Auto.ColumnTreeData (V : Type u_1) [Fintype V] : Type u_1

Finite column data from eq:columnbudget and column-data, lines 470–483. The budget counts available labels at each point, without bounding the total number of labels on disjoint branches.

• grid : RealDyadicGrid

  Dyadic grid underlying the column tree.

• cells : Finset (ℤ × ℤ)

  Finite collection of cells carrying the column tree.

• root : ℤ × ℤ

  Root cell containing every cell of the tree.

• below_root (c : ℤ × ℤ) : c ∈ self.cells → dyadicGridCell self.grid c.1 c.2 ⊆ dyadicGridCell self.grid self.root.1 self.root.2
• birth : V → ℤ × ℤ

  Birth cell assigned to each column label.

• birth_mem (v : V) : self.birth v ∈ self.cells
• scalar : V → ℝ → ℂ

  Scalar function represented by each column.

• scalar_measurable (v : V) : Measurable (self.scalar v)
• privateWeight : V → ℝ

  Positive normalization weight assigned to each column label.

• privateWeight_pos (v : V) : 0 < self.privateWeight v
• budget : ℝ

  Uniform budget controlling normalized columns and their private weights.

• two_le_budget : 2 ≤ self.budget
• private_lower (v : V) : self.budget⁻¹ ≤ √(self.privateWeight v)
• column_bound (v : V) : ∀ᵐ (y : ℝ) ∂MeasureTheory.volume.restrict (dyadicGridCell self.grid (self.birth v).1 (self.birth v).2), ‖privateColumnValue self.scalar self.privateWeight v y‖ ≤ self.budget
• path_count (y : ℝ) : ↑{v : V | y ∈ dyadicGridCell self.grid (self.birth v).1 (self.birth v).2}.card ≤ self.budget

structure TrilinearHT.Auto.InheritedColumnMask {V : Type u_1} [Fintype V] (D : ColumnTreeData V) : Type u_1

A fixed inherited mask: available birth cells contain the decision cell, and every old label remains available on each descendant in the tree.

• labels : ℤ × ℤ → Finset V

  Available column labels at each cell, inherited from its ancestors.

• available (c : ℤ × ℤ) : c ∈ D.cells → ∀ v ∈ self.labels c, dyadicGridCell D.grid c.1 c.2 ⊆ dyadicGridCell D.grid (D.birth v).1 (D.birth v).2
• inherited (c : ℤ × ℤ) : c ∈ D.cells → ∀ d ∈ D.cells, dyadicGridCell D.grid c.1 c.2 ⊆ dyadicGridCell D.grid d.1 d.2 → self.labels d ⊆ self.labels c

theorem TrilinearHT.Auto.InheritedColumnMask_card_le {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) : ↑(A.labels c).card ≤ D.budget

Each decision-cell mask has at most the path budget many columns, although labels on other branches need not be bounded in number.

theorem TrilinearHT.Auto.InheritedColumnMask_ae_column_bound {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) {v : V} (hv : v ∈ A.labels c) : ∀ᵐ (y : ℝ) ∂MeasureTheory.volume.restrict (dyadicGridCell D.grid c.1 c.2), ‖privateColumnValue D.scalar D.privateWeight v y‖ ≤ D.budget

The birth-cell essential bound passes to every decision cell on which the fixed mask makes the label available.

theorem TrilinearHT.Auto.cellColumn_memLp {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) {v : V} (hv : v ∈ A.labels c) : MeasureTheory.MemLp ((dyadicGridCell D.grid c.1 c.2).indicator (privateColumnValue D.scalar D.privateWeight v)) 2 MeasureTheory.volume

Available columns, restricted to a decision cell and extended by zero, belong to L2 by the source essential bound and the finite cell measure.

noncomputable def TrilinearHT.Auto.cellColumnLp {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (v : ↥(A.labels c)) : ↥(ColumnL2 V)

The cell-supported L2 column, with its exact original representative.

Equations

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

theorem TrilinearHT.Auto.cellColumnLp_coeFn {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (v : ↥(A.labels c)) : ↑↑(cellColumnLp D A hc v) =ᵐ[MeasureTheory.volume] (dyadicGridCell D.grid c.1 c.2).indicator (privateColumnValue D.scalar D.privateWeight ↑v)

noncomputable def TrilinearHT.Auto.cellColumnRange {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) : Submodule ℂ ↥(ColumnL2 V)

The source projection range is the span of constant-coefficient combinations of the restricted available columns (column-data, line 483).

Equations

• TrilinearHT.Auto.cellColumnRange D A hc = Submodule.span ℂ (Set.range (TrilinearHT.Auto.cellColumnLp D A hc))

instance TrilinearHT.Auto.cellColumnRange_finiteDimensional {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) : FiniteDimensional ℂ ↥(cellColumnRange D A hc)

noncomputable def TrilinearHT.Auto.cellColumnProjection {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) : ↥(ColumnL2 V) →L[ℂ] ↥(ColumnL2 V)

Orthogonal projection onto the finite-dimensional column range. No basis-selection algorithm is part of this definition.

Equations

• TrilinearHT.Auto.cellColumnProjection D A hc = (TrilinearHT.Auto.cellColumnRange D A hc).starProjection

theorem TrilinearHT.Auto.cellColumnProjection_mem {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (z : ↥(ColumnL2 V)) : (cellColumnProjection D A hc) z ∈ cellColumnRange D A hc

theorem TrilinearHT.Auto.cellColumnRange_mem_iff {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (z : ↥(ColumnL2 V)) : z ∈ cellColumnRange D A hc ↔ ∃ (a : ↥(A.labels c) → ℂ), ∑ v : ↥(A.labels c), a v • cellColumnLp D A hc v = z

Membership in the projection range is exactly a constant-coefficient combination of the available restricted columns.

noncomputable def TrilinearHT.Auto.columnL2Indicator {V : Type u_1} [Fintype V] (s : Set ℝ) (hs : MeasurableSet s) (z : ↥(ColumnL2 V)) : ↥(ColumnL2 V)

Multiplication of an L2 column-space vector by a measurable decision set, retaining its original values on the set and zero elsewhere.

Equations

• TrilinearHT.Auto.columnL2Indicator s hs z = MeasureTheory.MemLp.toLp (s.indicator ↑↑z) ⋯

theorem TrilinearHT.Auto.columnL2Indicator_coeFn {V : Type u_1} [Fintype V] (s : Set ℝ) (hs : MeasurableSet s) (z : ↥(ColumnL2 V)) : ↑↑(columnL2Indicator s hs z) =ᵐ[MeasureTheory.volume] s.indicator ↑↑z

theorem TrilinearHT.Auto.columnL2Indicator_add {V : Type u_1} [Fintype V] (s : Set ℝ) (hs : MeasurableSet s) (z w : ↥(ColumnL2 V)) : columnL2Indicator s hs (z + w) = columnL2Indicator s hs z + columnL2Indicator s hs w

theorem TrilinearHT.Auto.columnL2Indicator_smul {V : Type u_1} [Fintype V] (s : Set ℝ) (hs : MeasurableSet s) (a : ℂ) (z : ↥(ColumnL2 V)) : columnL2Indicator s hs (a • z) = a • columnL2Indicator s hs z

theorem TrilinearHT.Auto.columnL2Indicator_norm_le {V : Type u_1} [Fintype V] (s : Set ℝ) (hs : MeasurableSet s) (z : ↥(ColumnL2 V)) : ‖columnL2Indicator s hs z‖ ≤ ‖z‖

noncomputable def TrilinearHT.Auto.columnL2Restriction {V : Type u_1} [Fintype V] (s : Set ℝ) (hs : MeasurableSet s) : ↥(ColumnL2 V) →L[ℂ] ↥(ColumnL2 V)

The bounded linear decision-set restriction operator.

Equations

• TrilinearHT.Auto.columnL2Restriction s hs = { toFun := TrilinearHT.Auto.columnL2Indicator s hs, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

theorem TrilinearHT.Auto.cellColumn_restrict_descendant {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c d : ℤ × ℤ} (hc : c ∈ D.cells) (hd : d ∈ D.cells) (hcd : dyadicGridCell D.grid c.1 c.2 ⊆ dyadicGridCell D.grid d.1 d.2) (v : ↥(A.labels d)) : (columnL2Restriction (dyadicGridCell D.grid c.1 c.2) ⋯) (cellColumnLp D A hd v) = cellColumnLp D A hc ⟨↑v, ⋯⟩

Restricting an old column to a descendant gives exactly the same label's descendant column, using the inherited-mask inclusion.

theorem TrilinearHT.Auto.cellColumnRange_restrict_descendant {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c d : ℤ × ℤ} (hc : c ∈ D.cells) (hd : d ∈ D.cells) (hcd : dyadicGridCell D.grid c.1 c.2 ⊆ dyadicGridCell D.grid d.1 d.2) {z : ↥(ColumnL2 V)} (hz : z ∈ cellColumnRange D A hd) : (columnL2Restriction (dyadicGridCell D.grid c.1 c.2) ⋯) z ∈ cellColumnRange D A hc

Blueprint column-data, lines 480–483: restriction to a descendant preserves the range of old constant-coefficient column combinations.

theorem TrilinearHT.Auto.cellColumnRange_fixed_restriction {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) {z : ↥(ColumnL2 V)} (hz : z ∈ cellColumnRange D A hc) : (columnL2Restriction (dyadicGridCell D.grid c.1 c.2) ⋯) z = z

Every vector in a cell's column range is fixed by restriction to that cell, making the zero extension in the source projection explicit.

theorem TrilinearHT.Auto.cellColumnRange_ae_zero_off {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) {z : ↥(ColumnL2 V)} (hz : z ∈ cellColumnRange D A hc) : ∀ᵐ (y : ℝ), y ∉ dyadicGridCell D.grid c.1 c.2 → ↑↑z y = 0

Column-range vectors vanish almost everywhere off their decision cell.

theorem TrilinearHT.Auto.cellColumnRange_inner_eq_zero_of_disjoint {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c d : ℤ × ℤ} (hc : c ∈ D.cells) (hd : d ∈ D.cells) (hdis : Disjoint (dyadicGridCell D.grid c.1 c.2) (dyadicGridCell D.grid d.1 d.2)) {z w : ↥(ColumnL2 V)} (hz : z ∈ cellColumnRange D A hc) (hw : w ∈ cellColumnRange D A hd) : inner ℂ z w = 0

The ranges of columns on disjoint decision cells are orthogonal, justifying the source's direct sums on stopping partitions.

structure TrilinearHT.Auto.ColumnStoppingPartition {V : Type u_1} [Fintype V] (D : ColumnTreeData V) : Type

A finite stopping partition of the source root, using cells of the fixed column tree. Half-open cells make the disjoint cover exact.

• cells : Finset (ℤ × ℤ)

  Disjoint stopping cells covering the original column-tree region.

• subset : self.cells ⊆ D.cells
• disjoint : (↑self.cells).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell D.grid c.1 c.2
• cover : ⋃ c ∈ self.cells, dyadicGridCell D.grid c.1 c.2 = dyadicGridCell D.grid D.root.1 D.root.2

noncomputable def TrilinearHT.Auto.partitionColumnRange {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (π : ColumnStoppingPartition D) : Submodule ℂ ↥(ColumnL2 V)

Orthogonal direct sum of the cell column ranges on a stopping partition.

Equations

• TrilinearHT.Auto.partitionColumnRange D A π = ⨆ (c : ↥π.cells), TrilinearHT.Auto.cellColumnRange D A ⋯

instance TrilinearHT.Auto.partitionColumnRange_finiteDimensional {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (π : ColumnStoppingPartition D) : FiniteDimensional ℂ ↥(partitionColumnRange D A π)

noncomputable def TrilinearHT.Auto.partitionColumnProjection {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (π : ColumnStoppingPartition D) : ↥(ColumnL2 V) →L[ℂ] ↥(ColumnL2 V)

The source stopping-partition projection, defined from its range.

Equations

• TrilinearHT.Auto.partitionColumnProjection D A π = (TrilinearHT.Auto.partitionColumnRange D A π).starProjection

theorem TrilinearHT.Auto.partitionColumnRange_orthogonalFamily {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (π : ColumnStoppingPartition D) : OrthogonalFamily ℂ (fun (c : ↥π.cells) => ↥(cellColumnRange D A ⋯)) fun (c : ↥π.cells) => (cellColumnRange D A ⋯).subtypeₗᵢ

theorem TrilinearHT.Auto.partitionColumnProjection_eq_sum {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (π : ColumnStoppingPartition D) (z : ↥(ColumnL2 V)) : (partitionColumnProjection D A π) z = ∑ c : ↥π.cells, (cellColumnProjection D A ⋯) z

Blueprint column-data, line 480: the partition projection equals the finite direct sum of its cell projections.

theorem TrilinearHT.Auto.cellColumnRange_restrict_superset {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) {s : Set ℝ} (hs : MeasurableSet s) (hcs : dyadicGridCell D.grid c.1 c.2 ⊆ s) {z : ↥(ColumnL2 V)} (hz : z ∈ cellColumnRange D A hc) : (columnL2Restriction s hs) z = z

theorem TrilinearHT.Auto.cellColumnRange_restrict_disjoint {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) {s : Set ℝ} (hs : MeasurableSet s) (hdis : Disjoint s (dyadicGridCell D.grid c.1 c.2)) {z : ↥(ColumnL2 V)} (hz : z ∈ cellColumnRange D A hc) : (columnL2Restriction s hs) z = 0

theorem TrilinearHT.Auto.columnPartition_restriction_sum {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (π : ColumnStoppingPartition D) (z : ↥(ColumnL2 V)) : ∑ c : ↥π.cells, (columnL2Restriction (dyadicGridCell D.grid (↑c).1 (↑c).2) ⋯) z = (columnL2Restriction (dyadicGridCell D.grid D.root.1 D.root.2) ⋯) z

The decision-cell restriction operators on a stopping partition sum to restriction to the root, an exact L2 identity.

def TrilinearHT.Auto.ColumnPartitionRefines {V : Type u_1} [Fintype V] {D : ColumnTreeData V} (σ π : ColumnStoppingPartition D) : Prop

Every fine stopping cell is contained in one old stopping cell.

Equations

• TrilinearHT.Auto.ColumnPartitionRefines σ π = ∀ c ∈ σ.cells, ∃ d ∈ π.cells, TrilinearHT.Auto.dyadicGridCell D.grid c.1 c.2 ⊆ TrilinearHT.Auto.dyadicGridCell D.grid d.1 d.2

theorem TrilinearHT.Auto.partitionColumnRange_mono {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {σ π : ColumnStoppingPartition D} (href : ColumnPartitionRefines σ π) : partitionColumnRange D A π ≤ partitionColumnRange D A σ

Blueprint column-data, lines 480–483: inherited masks make the old partition range a subspace of every refining stopping-partition range.

theorem TrilinearHT.Auto.columnL2Restriction_inner {V : Type u_1} [Fintype V] (s : Set ℝ) (hs : MeasurableSet s) (z w : ↥(ColumnL2 V)) : inner ℂ ((columnL2Restriction s hs) z) w = inner ℂ z ((columnL2Restriction s hs) w)

Restriction to a measurable decision set is self-adjoint on the column L2 space.

theorem TrilinearHT.Auto.cellColumnProjection_input_locality {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) : cellColumnProjection D A hc ∘SL columnL2Restriction (dyadicGridCell D.grid c.1 c.2) ⋯ = cellColumnProjection D A hc

Blueprint column-data, line 483: the cell projection is unchanged by right multiplication by its decision-cell indicator.

structure TrilinearHT.Auto.ColumnRowFamily {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (ι : Type u_2) (F : Type u_3) [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] : Type (max (max u_1 u_2) u_3)

Fixed row-family interface in blueprint column-data, line 483. The square-sum bound and exact input-cell equation remain explicit data when later constructions assemble and compose row families.

• decision : ι → ℤ × ℤ

  Decision cell at which each row is localized.

• decision_mem (i : ι) : self.decision i ∈ D.cells
• row : ι → ↥(ColumnL2 V) →L[ℂ] F

  Continuous linear operator associated with each row.

• bound : ℝ

  Uniform square-sum bound for the row operators.

• bound_nonneg : 0 ≤ self.bound
• square_sum (z : ↥(ColumnL2 V)) : ∑ i : ι, ‖(self.row i) z‖ ^ 2 ≤ self.bound ^ 2 * ‖z‖ ^ 2
• input_locality (i : ι) : self.row i ∘SL columnL2Restriction (dyadicGridCell D.grid (self.decision i).1 (self.decision i).2) ⋯ = self.row i

@[reducible, inline]

abbrev TrilinearHT.Auto.CellCoefficients {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (c : ℤ × ℤ) : Type u_1

Euclidean coefficient space for the labels available on a decision cell.

Equations

• TrilinearHT.Auto.CellCoefficients D A c = EuclideanSpace ℂ ↥(A.labels c)

noncomputable def TrilinearHT.Auto.columnCombination {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (c : ℤ × ℤ) (a : CellCoefficients D A c) (y : ℝ) : ColumnHilbert V

Evaluation of a constant-coefficient combination of available columns.

Equations

• TrilinearHT.Auto.columnCombination D A c a y = ∑ v : ↥(A.labels c), a.ofLp v • TrilinearHT.Auto.privateColumnValue D.scalar D.privateWeight (↑v) y

theorem TrilinearHT.Auto.columnCombination_private {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (c : ℤ × ℤ) (a : CellCoefficients D A c) (y : ℝ) (w : ↥(A.labels c)) : (columnCombination D A c a y).ofLp (some ↑w) = a.ofLp w * ↑√(D.privateWeight ↑w)

theorem TrilinearHT.Auto.columnCombination_lower {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (c : ℤ × ℤ) (a : CellCoefficients D A c) (y : ℝ) : D.budget⁻¹ * ‖a‖ ≤ ‖columnCombination D A c a y‖

The private coordinates alone control the coefficient norm, the lower bound in blueprint lem:coeff, lines 487–491.

theorem TrilinearHT.Auto.columnCombination_upper_of_bound {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (a : CellCoefficients D A c) (y : ℝ) (hcol : ∀ (v : ↥(A.labels c)), ‖privateColumnValue D.scalar D.privateWeight (↑v) y‖ ≤ D.budget) : ‖columnCombination D A c a y‖ ≤ D.budget * √D.budget * ‖a‖

theorem TrilinearHT.Auto.columnBudget_rpow_three_halves {V : Type u_1} [Fintype V] (D : ColumnTreeData V) : D.budget ^ (3 / 2) = D.budget * √D.budget

theorem TrilinearHT.Auto.columnCombination_bounds {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) : ∀ᵐ (y : ℝ) ∂MeasureTheory.volume.restrict (dyadicGridCell D.grid c.1 c.2), ∀ (a : CellCoefficients D A c), D.budget⁻¹ * ‖a‖ ≤ ‖columnCombination D A c a y‖ ∧ ‖columnCombination D A c a y‖ ≤ D.budget ^ (3 / 2) * ‖a‖

Blueprint lem:coeff, lines 487–491: the two-sided coefficient norm bound holds uniformly in all coefficients on a common full-measure subset of the decision cell, using the source essential-supremum convention.

noncomputable def TrilinearHT.Auto.cellColumnSynthesis {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) : CellCoefficients D A c →L[ℂ] ↥(ColumnL2 V)

The cell synthesis map used to form the averaged Gram operator in blueprint lem:coeff, line 503.

Equations

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

theorem TrilinearHT.Auto.cellColumnSynthesis_coeFn {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (a : CellCoefficients D A c) : ↑↑((cellColumnSynthesis D A hc) a) =ᵐ[MeasureTheory.volume] (dyadicGridCell D.grid c.1 c.2).indicator (columnCombination D A c a)

noncomputable def TrilinearHT.Auto.cellColumnGram {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) : CellCoefficients D A c →L[ℂ] CellCoefficients D A c

The normalized Gram operator is the adjoint-square of cell synthesis, divided by the cell length. This is the averaged Gram operator of lem:coeff.

Equations

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

theorem TrilinearHT.Auto.cellColumnGram_inner {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (a b : CellCoefficients D A c) : inner ℂ a ((cellColumnGram D A hc) b) = (dyadicGridLength D.grid c.1)⁻¹ • inner ℂ ((cellColumnSynthesis D A hc) a) ((cellColumnSynthesis D A hc) b)

theorem TrilinearHT.Auto.cellColumnSynthesis_inner_integral {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (a b : CellCoefficients D A c) : inner ℂ ((cellColumnSynthesis D A hc) a) ((cellColumnSynthesis D A hc) b) = ∫ (y : ℝ) in dyadicGridCell D.grid c.1 c.2, inner ℂ (columnCombination D A c a y) (columnCombination D A c b y)

theorem TrilinearHT.Auto.cellColumnSynthesis_norm_sq_integral {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (a : CellCoefficients D A c) : ‖(cellColumnSynthesis D A hc) a‖ ^ 2 = ∫ (y : ℝ) in dyadicGridCell D.grid c.1 c.2, ‖columnCombination D A c a y‖ ^ 2

theorem TrilinearHT.Auto.columnCombination_memLp {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (a : CellCoefficients D A c) : MeasureTheory.MemLp (columnCombination D A c a) 2 (MeasureTheory.volume.restrict (dyadicGridCell D.grid c.1 c.2))

theorem TrilinearHT.Auto.cellColumnSynthesis_lower_sq {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (a : CellCoefficients D A c) : dyadicGridLength D.grid c.1 * (D.budget⁻¹ * ‖a‖) ^ 2 ≤ ‖(cellColumnSynthesis D A hc) a‖ ^ 2

theorem TrilinearHT.Auto.cellColumnGram_coercive {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (a : CellCoefficients D A c) : D.budget⁻¹ ^ 2 * ‖a‖ ^ 2 ≤ (inner ℂ a ((cellColumnGram D A hc) a)).re

Coercivity of the averaged Gram form, with the source constant D⁻².

theorem TrilinearHT.Auto.cellColumnGram_bounded_below {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (a : CellCoefficients D A c) : D.budget⁻¹ ^ 2 * ‖a‖ ≤ ‖(cellColumnGram D A hc) a‖

theorem TrilinearHT.Auto.cellColumnGram_injective {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) : Function.Injective ⇑(cellColumnGram D A hc)

noncomputable def TrilinearHT.Auto.cellColumnGramEquiv {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) : CellCoefficients D A c ≃L[ℂ] CellCoefficients D A c

The positive averaged Gram operator is invertible, including an empty mask.

Equations

• TrilinearHT.Auto.cellColumnGramEquiv D A hc = (LinearEquiv.ofBijective ↑(TrilinearHT.Auto.cellColumnGram D A hc) ⋯).toContinuousLinearEquiv

theorem TrilinearHT.Auto.cellColumnGramEquiv_symm_norm_le {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) : ‖↑(cellColumnGramEquiv D A hc).symm‖ ≤ D.budget ^ 2

theorem TrilinearHT.Auto.cellColumnSynthesis_range {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) : (↑(cellColumnSynthesis D A hc)).range = cellColumnRange D A hc

noncomputable def TrilinearHT.Auto.cellProjectionCoefficients {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (z : ↥(ColumnL2 V)) : CellCoefficients D A c

The coefficient vector in the source projection kernel formula.

Equations

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

theorem TrilinearHT.Auto.cellProjectionCoefficients_normal {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (z : ↥(ColumnL2 V)) : (ContinuousLinearMap.adjoint (cellColumnSynthesis D A hc)) ((cellColumnSynthesis D A hc) (cellProjectionCoefficients D A hc z)) = (ContinuousLinearMap.adjoint (cellColumnSynthesis D A hc)) z

theorem TrilinearHT.Auto.cellColumnProjection_eq_synthesis {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (z : ↥(ColumnL2 V)) : (cellColumnProjection D A hc) z = (cellColumnSynthesis D A hc) (cellProjectionCoefficients D A hc z)

Blueprint lem:coeff, line 503: the inverse-Gram formula agrees with the orthogonal projection defined from the column range.

theorem TrilinearHT.Auto.cellColumnProjection_coeFn {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (z : ↥(ColumnL2 V)) : ↑↑((cellColumnProjection D A hc) z) =ᵐ[MeasureTheory.volume] (dyadicGridCell D.grid c.1 c.2).indicator (columnCombination D A c (cellProjectionCoefficients D A hc z))

noncomputable def TrilinearHT.Auto.columnEvaluation {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (c : ℤ × ℤ) (y : ℝ) : CellCoefficients D A c →L[ℂ] ColumnHilbert V

Pointwise column evaluation, denoted E_y in blueprint lem:coeff.

Equations

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

theorem TrilinearHT.Auto.columnEvaluation_apply {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (c : ℤ × ℤ) (y : ℝ) (a : CellCoefficients D A c) : (columnEvaluation D A c y) a = columnCombination D A c a y

theorem TrilinearHT.Auto.columnEvaluation_measurable {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (c : ℤ × ℤ) : Measurable (columnEvaluation D A c)

theorem TrilinearHT.Auto.columnEvaluation_ae_norm_le {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) : ∀ᵐ (y : ℝ) ∂MeasureTheory.volume.restrict (dyadicGridCell D.grid c.1 c.2), ‖columnEvaluation D A c y‖ ≤ D.budget * √D.budget

noncomputable def TrilinearHT.Auto.cellProjectionKernel {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (y t : ℝ) : ColumnHilbert V →L[ℂ] ColumnHilbert V

The kernel relative to normalized integration on the decision cell.

Equations

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

theorem TrilinearHT.Auto.cellProjectionKernel_norm_le {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (y t : ℝ) (hy : ‖columnEvaluation D A c y‖ ≤ D.budget * √D.budget) (ht : ‖columnEvaluation D A c t‖ ≤ D.budget * √D.budget) : ‖cellProjectionKernel D A hc y t‖ ≤ D.budget ^ 5

theorem TrilinearHT.Auto.columnEvaluation_adjoint_integrable {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (z : ↥(ColumnL2 V)) : MeasureTheory.Integrable (fun (t : ℝ) => (ContinuousLinearMap.adjoint (columnEvaluation D A c t)) (↑↑z t)) (MeasureTheory.volume.restrict (dyadicGridCell D.grid c.1 c.2))

theorem TrilinearHT.Auto.cellColumnSynthesis_adjoint_integral {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (z : ↥(ColumnL2 V)) : (ContinuousLinearMap.adjoint (cellColumnSynthesis D A hc)) z = ∫ (t : ℝ) in dyadicGridCell D.grid c.1 c.2, (ContinuousLinearMap.adjoint (columnEvaluation D A c t)) (↑↑z t)

theorem TrilinearHT.Auto.cellProjectionKernel_integral {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (z : ↥(ColumnL2 V)) (y : ℝ) : columnCombination D A c (cellProjectionCoefficients D A hc z) y = ↑(dyadicGridLength D.grid c.1)⁻¹ • ∫ (t : ℝ) in dyadicGridCell D.grid c.1 c.2, (cellProjectionKernel D A hc y t) (↑↑z t)

theorem TrilinearHT.Auto.cellColumnProjection_kernel {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (z : ↥(ColumnL2 V)) : ↑↑((cellColumnProjection D A hc) z) =ᵐ[MeasureTheory.volume] (dyadicGridCell D.grid c.1 c.2).indicator fun (y : ℝ) => ↑(dyadicGridLength D.grid c.1)⁻¹ • ∫ (t : ℝ) in dyadicGridCell D.grid c.1 c.2, (cellProjectionKernel D A hc y t) (↑↑z t)

Blueprint lem:coeff, line 503: the orthogonal projection is given by the normalized integral kernel E_y G⁻¹ E_t*, on a common almost-everywhere representative.

theorem TrilinearHT.Auto.cellProjectionKernel_ae_norm_le {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) : ∀ᵐ (y : ℝ) (t : ℝ) ∂MeasureTheory.volume.restrict (dyadicGridCell D.grid c.1 c.2), ‖cellProjectionKernel D A hc y t‖ ≤ D.budget ^ 5

The normalized projection kernel has the exact D⁵ bound from the source.

theorem TrilinearHT.Auto.cellColumnProjection_ae_bound {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (z : ↥(ColumnL2 V)) : ∀ᵐ (y : ℝ) ∂MeasureTheory.volume.restrict (dyadicGridCell D.grid c.1 c.2), ‖↑↑((cellColumnProjection D A hc) z) y‖ ≤ D.budget ^ 5 * ((∫ (t : ℝ) in dyadicGridCell D.grid c.1 c.2, ‖↑↑z t‖) / dyadicGridLength D.grid c.1)

The pointwise form of the source average-to-supremum projection bound.

noncomputable def TrilinearHT.Auto.physicalColumnInput {V : Type u_1} [Fintype V] (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↥(ColumnL2 V)

The physical input (f,0) in the column Hilbert space.

Equations

• TrilinearHT.Auto.physicalColumnInput f = (ContinuousLinearMap.toSpanSingleton ℂ (EuclideanSpace.single none 1)).compLp f

theorem TrilinearHT.Auto.physicalColumnInput_coeFn {V : Type u_1} [Fintype V] (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↑↑(physicalColumnInput f) =ᵐ[MeasureTheory.volume] fun (y : ℝ) => ↑↑f y • EuclideanSpace.single none 1

theorem TrilinearHT.Auto.privateColumnValue_inner {V : Type u_1} [Fintype V] (φ : V → ℝ → ℂ) (ε : V → ℝ) (v : V) (y : ℝ) (z : ColumnHilbert V) : inner ℂ (privateColumnValue φ ε v y) z = star (φ v y) * z.ofLp none + ↑√(ε v) * z.ofLp (some v)

theorem TrilinearHT.Auto.privateColumnValue_inner_residual {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (c : ℤ × ℤ) (a : CellCoefficients D A c) (v : ↥(A.labels c)) (y : ℝ) (f : ℂ) : inner ℂ (privateColumnValue D.scalar D.privateWeight (↑v) y) (f • EuclideanSpace.single none 1 - columnCombination D A c a y) = (f - (columnCombination D A c a y).ofLp none) * star (D.scalar (↑v) y) - ↑(D.privateWeight ↑v) * a.ofLp v

theorem TrilinearHT.Auto.cellColumn_residual_integral_zero {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (z : ↥(ColumnL2 V)) (v : ↥(A.labels c)) : ∫ (y : ℝ) in dyadicGridCell D.grid c.1 c.2, inner ℂ (privateColumnValue D.scalar D.privateWeight (↑v) y) (↑↑z y - ↑↑((cellColumnProjection D A hc) z) y) = 0

theorem TrilinearHT.Auto.cellColumnProjection_predictor_moment {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (v : ↥(A.labels c)) : ↑(dyadicGridLength D.grid c.1)⁻¹ * ∫ (y : ℝ) in dyadicGridCell D.grid c.1 c.2, (↑↑f y - (↑↑((cellColumnProjection D A hc) (physicalColumnInput f)) y).ofLp none) * star (D.scalar (↑v) y) = ↑(D.privateWeight ↑v) * (cellProjectionCoefficients D A hc (physicalColumnInput f)).ofLp v

Blueprint eq:predictor-moment, lines 496–503: for the physical input (f,0), the averaged scalar prediction error against each column equals its private weight times its unique projection coefficient.

def TrilinearHT.Auto.enlargedColumnTree {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (S : Finset (ℤ × ℤ)) (hDS : D.cells ⊆ S) (hS : ∀ c ∈ S, dyadicGridCell D.grid c.1 c.2 ⊆ dyadicGridCell D.grid D.root.1 D.root.2) : ColumnTreeData V

Enlarge the finite cell set without changing any columns or their budget. This supplies the completion in lem:compression, line 553.

Equations

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

noncomputable def TrilinearHT.Auto.extendedColumnLabels {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (c : ℤ × ℤ) : Finset V

Extend a mask by taking the union of labels on original ancestor cells. Inheritance makes this extension agree with the mask on every original cell.

Equations

• TrilinearHT.Auto.extendedColumnLabels D A c = {d ∈ D.cells | TrilinearHT.Auto.dyadicGridCell D.grid c.1 c.2 ⊆ TrilinearHT.Auto.dyadicGridCell D.grid d.1 d.2}.biUnion A.labels

theorem TrilinearHT.Auto.extendedColumnLabels_eq {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) : extendedColumnLabels D A c = A.labels c

noncomputable def TrilinearHT.Auto.extendedColumnMask {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (S : Finset (ℤ × ℤ)) (hDS : D.cells ⊆ S) (hS : ∀ c ∈ S, dyadicGridCell D.grid c.1 c.2 ⊆ dyadicGridCell D.grid D.root.1 D.root.2) : InheritedColumnMask (enlargedColumnTree D S hDS hS)

Extend an inherited mask to an enlarged cell collection.

Equations

• TrilinearHT.Auto.extendedColumnMask D A S hDS hS = { labels := TrilinearHT.Auto.extendedColumnLabels D A, available := ⋯, inherited := ⋯ }

theorem TrilinearHT.Auto.extendedColumnMask_range_eq {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (S : Finset (ℤ × ℤ)) (hDS : D.cells ⊆ S) (hS : ∀ c ∈ S, dyadicGridCell D.grid c.1 c.2 ⊆ dyadicGridCell D.grid D.root.1 D.root.2) {c : ℤ × ℤ} (hc : c ∈ D.cells) : cellColumnRange (enlargedColumnTree D S hDS hS) (extendedColumnMask D A S hDS hS) ⋯ = cellColumnRange D A hc

Completing the tree preserves exactly the column range on every original cell; no extra columns have been introduced there (lem:compression, line 553).

theorem TrilinearHT.Auto.extendedColumnMask_projection_eq {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (S : Finset (ℤ × ℤ)) (hDS : D.cells ⊆ S) (hS : ∀ c ∈ S, dyadicGridCell D.grid c.1 c.2 ⊆ dyadicGridCell D.grid D.root.1 D.root.2) {c : ℤ × ℤ} (hc : c ∈ D.cells) : cellColumnProjection (enlargedColumnTree D S hDS hS) (extendedColumnMask D A S hDS hS) ⋯ = cellColumnProjection D A hc

The actual orthogonal projections are unchanged on original cells, so completion does not alter any row input in spatial compression.

def TrilinearHT.Auto.enlargedColumnRows {V : Type u_1} {ι : Type u_2} {F : Type u_3} [Fintype V] [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (D : ColumnTreeData V) (B : ColumnRowFamily D ι F) (S : Finset (ℤ × ℤ)) (hDS : D.cells ⊆ S) (hS : ∀ c ∈ S, dyadicGridCell D.grid c.1 c.2 ⊆ dyadicGridCell D.grid D.root.1 D.root.2) : ColumnRowFamily (enlargedColumnTree D S hDS hS) ι F

Original local rows retain their operators, bounds and exact input locality after completing the tree (lem:compression, lines 553 and 569).

Equations

• TrilinearHT.Auto.enlargedColumnRows D B S hDS hS = { decision := B.decision, decision_mem := ⋯, row := B.row, bound := B.bound, bound_nonneg := ⋯, square_sum := ⋯, input_locality := ⋯ }

noncomputable def TrilinearHT.Auto.columnCompletionDepth {V : Type u_1} [Fintype V] (D : ColumnTreeData V) : ℕ

A complete finite horizon strictly below every original column-tree cell.

Equations

• TrilinearHT.Auto.columnCompletionDepth D = Classical.choose ⋯

theorem TrilinearHT.Auto.columnCompletion_contains {V : Type u_1} [Fintype V] (D : ColumnTreeData V) : D.cells ⊆ dyadicFiniteTree D.grid D.root (columnCompletionDepth D)

theorem TrilinearHT.Auto.columnCompletion_extra_generation {V : Type u_1} [Fintype V] (D : ColumnTreeData V) {c : ℤ × ℤ} (hc : c ∈ D.cells) : c.1 < D.root.1 + ↑(columnCompletionDepth D)

noncomputable def TrilinearHT.Auto.completedColumnTree {V : Type u_1} [Fintype V] (D : ColumnTreeData V) : ColumnTreeData V

Complete the source tree while preserving its original column data.

Equations

• TrilinearHT.Auto.completedColumnTree D = TrilinearHT.Auto.enlargedColumnTree D (TrilinearHT.Auto.dyadicFiniteTree D.grid D.root (TrilinearHT.Auto.columnCompletionDepth D)) ⋯ ⋯

noncomputable def TrilinearHT.Auto.completedColumnMask {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) : InheritedColumnMask (completedColumnTree D)

Inherited mask on the completed finite dyadic tree.

Equations

• TrilinearHT.Auto.completedColumnMask D A = TrilinearHT.Auto.extendedColumnMask D A (TrilinearHT.Auto.dyadicFiniteTree D.grid D.root (TrilinearHT.Auto.columnCompletionDepth D)) ⋯ ⋯

theorem TrilinearHT.Auto.completedColumnMask_projection_eq {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) : cellColumnProjection (completedColumnTree D) (completedColumnMask D A) ⋯ = cellColumnProjection D A hc

noncomputable def TrilinearHT.Auto.completedColumnRows {V : Type u_1} {ι : Type u_2} {F : Type u_3} [Fintype V] [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (D : ColumnTreeData V) (B : ColumnRowFamily D ι F) : ColumnRowFamily (completedColumnTree D) ι F

The original row operators viewed on the completed column tree.

Equations

• TrilinearHT.Auto.completedColumnRows D B = TrilinearHT.Auto.enlargedColumnRows D B (TrilinearHT.Auto.dyadicFiniteTree D.grid D.root (TrilinearHT.Auto.columnCompletionDepth D)) ⋯ ⋯

noncomputable def TrilinearHT.Auto.columnCellAverage {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (z : ↥(ColumnL2 V)) (c : ℤ × ℤ) : ℝ

The size used for the source stopping decomposition is the average of the actual Hilbert-valued L2 input's norm.

Equations

• TrilinearHT.Auto.columnCellAverage D z c = TrilinearHT.Auto.dyadicCellAverage D.grid (fun (y : ℝ) => ‖↑↑z y‖) c

theorem TrilinearHT.Auto.columnCellAverage_nonneg {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (z : ↥(ColumnL2 V)) (c : ℤ × ℤ) : 0 ≤ columnCellAverage D z c

theorem TrilinearHT.Auto.columnInput_norm_integrableOn {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (z : ↥(ColumnL2 V)) (c : ℤ × ℤ) : MeasureTheory.IntegrableOn (fun (y : ℝ) => ‖↑↑z y‖) (dyadicGridCell D.grid c.1 c.2) MeasureTheory.volume

noncomputable def TrilinearHT.Auto.columnSizeRoots {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (z : ↥(ColumnL2 V)) : Finset (ℤ × ℤ)

Size-stopping roots for the cell averages of the column input.

Equations

• TrilinearHT.Auto.columnSizeRoots D z = TrilinearHT.Auto.dyadicSizeRoots D.grid D.root (TrilinearHT.Auto.columnCompletionDepth D) (TrilinearHT.Auto.columnCellAverage D z)

noncomputable def TrilinearHT.Auto.columnSizeSegment {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (z : ↥(ColumnL2 V)) (K : ℤ × ℤ) : Finset (ℤ × ℤ)

Cells in the size segment beginning at the stopping root K.

Equations

• TrilinearHT.Auto.columnSizeSegment D z K = TrilinearHT.Auto.dyadicSizeSegment D.grid (TrilinearHT.Auto.completedColumnTree D).cells (TrilinearHT.Auto.columnCellAverage D z) K

noncomputable def TrilinearHT.Auto.columnSizeCuts {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (z : ↥(ColumnL2 V)) (K : ℤ × ℤ) : Finset (ℤ × ℤ)

Cuts delimiting the size segment beginning at K.

Equations

• TrilinearHT.Auto.columnSizeCuts D z K = TrilinearHT.Auto.dyadicSizeSegmentCuts D.grid D.root (TrilinearHT.Auto.columnCompletionDepth D) (TrilinearHT.Auto.columnCellAverage D z) K

theorem TrilinearHT.Auto.columnSizeRoots_subset {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (z : ↥(ColumnL2 V)) : columnSizeRoots D z ⊆ (completedColumnTree D).cells

theorem TrilinearHT.Auto.columnSizeRoot_assignment {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (z : ↥(ColumnL2 V)) {u : ℤ × ℤ} (hu : u ∈ D.cells) : ∃ K ∈ columnSizeRoots D z, u ∈ columnSizeSegment D z K ∧ ∀ L ∈ columnSizeRoots D z, dyadicGridCell D.grid u.1 u.2 ⊆ dyadicGridCell D.grid L.1 L.2 → L.1 ≤ K.1

Every original decision cell has a deepest doubling-average root and belongs to its segment (lem:compression, line 553).

theorem TrilinearHT.Auto.columnSizeCuts_subset {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (z : ↥(ColumnL2 V)) {K : ℤ × ℤ} (hK : K ∈ columnSizeRoots D z) : columnSizeCuts D z K ⊆ (completedColumnTree D).cells

theorem TrilinearHT.Auto.columnSizeCuts_pairwiseDisjoint {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (z : ↥(ColumnL2 V)) (K : ℤ × ℤ) : (↑(columnSizeCuts D z K)).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell D.grid c.1 c.2

theorem TrilinearHT.Auto.columnSizeCuts_union {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (z : ↥(ColumnL2 V)) (K : ℤ × ℤ) : ⋃ c ∈ columnSizeCuts D z K, dyadicGridCell D.grid c.1 c.2 = dyadicGridCell D.grid K.1 K.2

theorem TrilinearHT.Auto.columnSizeCuts_union_below {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (z : ↥(ColumnL2 V)) {K u : ℤ × ℤ} (hK : K ∈ columnSizeRoots D z) (hu : u ∈ columnSizeSegment D z K) : ⋃ c ∈ {c ∈ columnSizeCuts D z K | dyadicGridCell D.grid c.1 c.2 ⊆ dyadicGridCell D.grid u.1 u.2}, dyadicGridCell D.grid c.1 c.2 = dyadicGridCell D.grid u.1 u.2

theorem TrilinearHT.Auto.columnSizeCuts_average_le {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (z : ↥(ColumnL2 V)) (K : ℤ × ℤ) {c : ℤ × ℤ} (hc : c ∈ columnSizeCuts D z K) : columnCellAverage D z c ≤ 4 * columnCellAverage D z K

Blueprint lem:compression, line 553: every cut-cell average of the input norm is at most four times the segment-root average.

noncomputable def TrilinearHT.Auto.columnAncestorMask {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (S : Finset (ℤ × ℤ)) (hS : S ⊆ D.cells) : InheritedColumnMask D

On each cut retain exactly the columns used by its ancestors in the selected segment (eq:moment-representative, lines 555–556).

Equations

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

theorem TrilinearHT.Auto.columnAncestorMask_labels_eq {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (S : Finset (ℤ × ℤ)) (hS : S ⊆ D.cells) {c : ℤ × ℤ} (hc : c ∈ S) : (columnAncestorMask D A S hS).labels c = A.labels c

noncomputable def TrilinearHT.Auto.cutColumnRange {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (C : Finset (ℤ × ℤ)) (hC : C ⊆ D.cells) : Submodule ℂ ↥(ColumnL2 V)

The orthogonal sum of column ranges on any finite disjoint cut family. Unlike a root stopping partition, it can be supported inside a segment root.

Equations

• TrilinearHT.Auto.cutColumnRange D A C hC = ⨆ (c : ↥C), TrilinearHT.Auto.cellColumnRange D A ⋯

instance TrilinearHT.Auto.cutColumnRange_finiteDimensional {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (C : Finset (ℤ × ℤ)) (hC : C ⊆ D.cells) : FiniteDimensional ℂ ↥(cutColumnRange D A C hC)

noncomputable def TrilinearHT.Auto.cutColumnProjection {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (C : Finset (ℤ × ℤ)) (hC : C ⊆ D.cells) : ↥(ColumnL2 V) →L[ℂ] ↥(ColumnL2 V)

Orthogonal projection onto the column range retained after the specified cuts.

Equations

• TrilinearHT.Auto.cutColumnProjection D A C hC = (TrilinearHT.Auto.cutColumnRange D A C hC).starProjection

theorem TrilinearHT.Auto.cutColumnRange_orthogonalFamily {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (C : Finset (ℤ × ℤ)) (hC : C ⊆ D.cells) (hdis : (↑C).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell D.grid c.1 c.2) : OrthogonalFamily ℂ (fun (c : ↥C) => ↥(cellColumnRange D A ⋯)) fun (c : ↥C) => (cellColumnRange D A ⋯).subtypeₗᵢ

theorem TrilinearHT.Auto.cutColumnProjection_eq_sum {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (C : Finset (ℤ × ℤ)) (hC : C ⊆ D.cells) (hdis : (↑C).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell D.grid c.1 c.2) (z : ↥(ColumnL2 V)) : (cutColumnProjection D A C hC) z = ∑ c : ↥C, (cellColumnProjection D A ⋯) z

noncomputable def TrilinearHT.Auto.columnSegmentMask {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (z : ↥(ColumnL2 V)) (K : ℤ × ℤ) : InheritedColumnMask (completedColumnTree D)

Ancestor mask restricted to the size segment beginning at K.

Equations

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

noncomputable def TrilinearHT.Auto.columnMomentRepresentative {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (z : ↥(ColumnL2 V)) {K : ℤ × ℤ} (hK : K ∈ columnSizeRoots D z) : ↥(ColumnL2 V)

The source moment representative is the orthogonal projection onto the segment-ancestor columns on each cut cell, extended by zero off the segment root.

Equations

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

theorem TrilinearHT.Auto.columnMomentRepresentative_eq_sum {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (z : ↥(ColumnL2 V)) {K : ℤ × ℤ} (hK : K ∈ columnSizeRoots D z) : columnMomentRepresentative D A z hK = ∑ c : ↥(columnSizeCuts D z K), (cellColumnProjection (completedColumnTree D) (columnSegmentMask D A z K) ⋯) z

theorem TrilinearHT.Auto.columnMomentRepresentative_ae_zero_off {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (z : ↥(ColumnL2 V)) {K : ℤ × ℤ} (hK : K ∈ columnSizeRoots D z) : ∀ᵐ (y : ℝ), y ∉ dyadicGridCell D.grid K.1 K.2 → ↑↑(columnMomentRepresentative D A z hK) y = 0

theorem TrilinearHT.Auto.columnMomentRepresentative_ae_bound {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (z : ↥(ColumnL2 V)) {K : ℤ × ℤ} (hK : K ∈ columnSizeRoots D z) : ∀ᵐ (y : ℝ), ‖↑↑(columnMomentRepresentative D A z hK) y‖ ≤ 4 * D.budget ^ 5 * columnCellAverage D z K

Blueprint eq:moment-representative, line 558: the representative has global essential bound 4 D^5 a_K, with no cost for the number of cut cells.

theorem TrilinearHT.Auto.columnMomentRepresentative_inner {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (z : ↥(ColumnL2 V)) {K : ℤ × ℤ} (hK : K ∈ columnSizeRoots D z) : inner ℂ z (columnMomentRepresentative D A z hK) = ↑(‖columnMomentRepresentative D A z hK‖ ^ 2)

Blueprint eq:moment-representative, line 559: the representative's squared L2 norm is exactly its pairing with the original input.

theorem TrilinearHT.Auto.columnMomentRepresentative_norm_sq {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (z : ↥(ColumnL2 V)) {K : ℤ × ℤ} (hK : K ∈ columnSizeRoots D z) : ‖columnMomentRepresentative D A z hK‖ ^ 2 = (inner ℂ z (columnMomentRepresentative D A z hK)).re

theorem TrilinearHT.Auto.cellColumnRange_congr_labels {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A B : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (h : A.labels c = B.labels c) : cellColumnRange D A hc = cellColumnRange D B hc

theorem TrilinearHT.Auto.cellColumnProjection_congr_labels {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A B : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (h : A.labels c = B.labels c) : cellColumnProjection D A hc = cellColumnProjection D B hc

theorem TrilinearHT.Auto.cutColumn_restriction_sum {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (C : Finset (ℤ × ℤ)) (hdis : (↑C).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell D.grid c.1 c.2) (u : ℤ × ℤ) (hcover : ⋃ c ∈ C, dyadicGridCell D.grid c.1 c.2 = dyadicGridCell D.grid u.1 u.2) (z : ↥(ColumnL2 V)) : ∑ c : ↥C, (columnL2Restriction (dyadicGridCell D.grid (↑c).1 (↑c).2) ⋯) z = (columnL2Restriction (dyadicGridCell D.grid u.1 u.2) ⋯) z

Restriction to a cell is the sum of restrictions to an exact finite disjoint partition of that cell, without requiring it to be the tree root.

theorem TrilinearHT.Auto.cellColumnRange_le_cutColumnRange {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (C : Finset (ℤ × ℤ)) (hC : C ⊆ D.cells) (hdis : (↑C).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell D.grid c.1 c.2) {u : ℤ × ℤ} (hu : u ∈ D.cells) (hcover : ⋃ c ∈ C, dyadicGridCell D.grid c.1 c.2 = dyadicGridCell D.grid u.1 u.2) : cellColumnRange D A hu ≤ cutColumnRange D A C hC

theorem TrilinearHT.Auto.cutColumnRange_mono {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (C E : Finset (ℤ × ℤ)) (hC : C ⊆ D.cells) (hE : E ⊆ D.cells) (hCE : C ⊆ E) : cutColumnRange D A C hC ≤ cutColumnRange D A E hE

theorem TrilinearHT.Auto.columnMomentRepresentative_preserves_completed {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (z : ↥(ColumnL2 V)) {K u : ℤ × ℤ} (hK : K ∈ columnSizeRoots D z) (hu : u ∈ columnSizeSegment D z K) : (cellColumnProjection (completedColumnTree D) (completedColumnMask D A) ⋯) (columnMomentRepresentative D A z hK) = (cellColumnProjection (completedColumnTree D) (completedColumnMask D A) ⋯) z

theorem TrilinearHT.Auto.columnMomentRepresentative_preserves_projection {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (z : ↥(ColumnL2 V)) {K u : ℤ × ℤ} (hK : K ∈ columnSizeRoots D z) (hu : u ∈ D.cells) (hsegment : u ∈ columnSizeSegment D z K) : (cellColumnProjection D A hu) (columnMomentRepresentative D A z hK) = (cellColumnProjection D A hu) z

Blueprint eq:moment-representative, lines 559–561: every original first-layer projection in the segment has exactly the same value on g_K and z.

theorem TrilinearHT.Auto.columnInput_norm_sq_integral {V : Type u_1} [Fintype V] (z : ↥(ColumnL2 V)) : ‖z‖ ^ 2 = ∫ (y : ℝ), ‖↑↑z y‖ ^ 2

noncomputable def TrilinearHT.Auto.columnDyadicMax {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (z : ↥(ColumnL2 V)) : ℝ → ℝ

The finite dyadic maximal function used in the source stopping-energy estimate, on the same completed tree as the moment representatives.

Equations

• TrilinearHT.Auto.columnDyadicMax D z = TrilinearHT.Auto.dyadicRealMax D.grid (TrilinearHT.Auto.completedColumnTree D).cells fun (y : ℝ) => ‖↑↑z y‖

theorem TrilinearHT.Auto.columnDyadicMax_nonneg {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (z : ↥(ColumnL2 V)) (x : ℝ) : 0 ≤ columnDyadicMax D z x

theorem TrilinearHT.Auto.columnDyadicMax_memLp {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (z : ↥(ColumnL2 V)) : MeasureTheory.MemLp (columnDyadicMax D z) 2 MeasureTheory.volume

theorem TrilinearHT.Auto.columnDyadicMax_energy_le {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (z : ↥(ColumnL2 V)) : ∫ (x : ℝ), columnDyadicMax D z x ^ 2 ≤ 4 * ‖z‖ ^ 2

The sharp dyadic maximal estimate has norm constant two, squared here.

theorem TrilinearHT.Auto.columnSizeRoots_square_path_le {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (z : ↥(ColumnL2 V)) (x : ℝ) : dyadicRealPathSum D.grid (columnSizeRoots D z) (fun (K : ℤ × ℤ) => columnCellAverage D z K ^ 2) x ≤ 4 / 3 * columnDyadicMax D z x ^ 2

theorem TrilinearHT.Auto.columnSizeRoots_energy_le_maximal {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (z : ↥(ColumnL2 V)) : ∑ K ∈ columnSizeRoots D z, columnCellAverage D z K ^ 2 * dyadicGridLength D.grid K.1 ≤ 4 / 3 * ∫ (x : ℝ), columnDyadicMax D z x ^ 2

Blueprint lem:compression, lines 561–564: integrating the geometric path estimate gives the exact four-thirds maximal-energy bound.

theorem TrilinearHT.Auto.columnSizeRoots_energy_le {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (z : ↥(ColumnL2 V)) : ∑ K ∈ columnSizeRoots D z, columnCellAverage D z K ^ 2 * dyadicGridLength D.grid K.1 ≤ 16 / 3 * ‖z‖ ^ 2

The total squared stopping-average energy is bounded independently of spatial depth and label count (lem:compression, lines 561–564).

noncomputable def TrilinearHT.Auto.columnMomentFamily {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (z : ↥(ColumnL2 V)) (K : ℤ × ℤ) : ↥(ColumnL2 V)

The finite moment family, with zero assigned to indices outside the stopping roots so it can be used in ordinary finite sums.

Equations

• TrilinearHT.Auto.columnMomentFamily D A z K = if hK : K ∈ TrilinearHT.Auto.columnSizeRoots D z then TrilinearHT.Auto.columnMomentRepresentative D A z hK else 0

theorem TrilinearHT.Auto.columnMomentFamily_of_mem {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (z : ↥(ColumnL2 V)) {K : ℤ × ℤ} (hK : K ∈ columnSizeRoots D z) : columnMomentFamily D A z K = columnMomentRepresentative D A z hK

noncomputable def TrilinearHT.Auto.columnMomentEnergy {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (z : ↥(ColumnL2 V)) : ℝ

Sum of squared moment-family norms over the size-stopping roots.

Equations

• TrilinearHT.Auto.columnMomentEnergy D A z = ∑ K ∈ TrilinearHT.Auto.columnSizeRoots D z, ‖TrilinearHT.Auto.columnMomentFamily D A z K‖ ^ 2

theorem TrilinearHT.Auto.columnMomentEnergy_nonneg {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (z : ↥(ColumnL2 V)) : 0 ≤ columnMomentEnergy D A z

noncomputable def TrilinearHT.Auto.columnMomentLogCount {V : Type u_1} [Fintype V] (D : ColumnTreeData V) : ℕ

Here 4 D^7 = (4 D^5) D², the source ratio G D².

Equations

• TrilinearHT.Auto.columnMomentLogCount D = TrilinearHT.Auto.dyadicLogSizeCount (4 * D.budget ^ 7)

theorem TrilinearHT.Auto.columnMoment_ratio_one_le {V : Type u_1} [Fintype V] (D : ColumnTreeData V) : 1 ≤ 4 * D.budget ^ 7

theorem TrilinearHT.Auto.columnMomentEnergy_quadratic {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (z : ↥(ColumnL2 V)) : columnMomentEnergy D A z ≤ 4 * D.budget⁻¹ ^ 2 * ‖z‖ ^ 2 + √↑(columnMomentLogCount D) * ‖z‖ * √(columnMomentEnergy D A z)

Blueprint lem:compression, line 565: the exact quadratic inequality for the aggregate moment energy, with the source logarithmic overlap count.

theorem TrilinearHT.Auto.columnMomentEnergy_le_count {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (z : ↥(ColumnL2 V)) : columnMomentEnergy D A z ≤ (8 * D.budget⁻¹ ^ 2 + ↑(columnMomentLogCount D)) * ‖z‖ ^ 2

theorem TrilinearHT.Auto.columnMomentLogCount_le {V : Type u_1} [Fintype V] (D : ColumnTreeData V) : ↑(columnMomentLogCount D) ≤ 5 + 7 * Real.logb 2 D.budget

The source overlap count grows only logarithmically in the column budget.

theorem TrilinearHT.Auto.columnMomentEnergy_logarithmic {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (z : ↥(ColumnL2 V)) : columnMomentEnergy D A z ≤ 7 / Real.log 2 * Real.log (2 * D.budget) * ‖z‖ ^ 2

Blueprint lem:compression, line 565: the total moment energy has an absolute logarithmic bound, independent of depth and total label count.

noncomputable def TrilinearHT.Auto.extendCellCoefficients {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (c : ℤ × ℤ) (a : CellCoefficients D A c) : EuclideanSpace ℂ V

Coefficients on one mask extended by zero to the common label space, as required for comparing different anchors (lem:compression, line 567).

Equations

• TrilinearHT.Auto.extendCellCoefficients D A c a = WithLp.toLp 2 fun (v : V) => if hv : v ∈ A.labels c then a.ofLp ⟨v, hv⟩ else 0

theorem TrilinearHT.Auto.columnCombination_private_all {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (c : ℤ × ℤ) (a : CellCoefficients D A c) (y : ℝ) (v : V) : (columnCombination D A c a y).ofLp (some v) = (extendCellCoefficients D A c a).ofLp v * ↑√(D.privateWeight v)

noncomputable def TrilinearHT.Auto.cellColumnProduct {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) : ℕ → ↥(ColumnL2 V) →L[ℂ] ↥(ColumnL2 V)

Products use the source order: layer zero acts first, and the last layer provides the coefficient vector used by the stopping rule.

Equations

• TrilinearHT.Auto.cellColumnProduct D A hc 0 = ContinuousLinearMap.id ℂ ↥(TrilinearHT.Auto.ColumnL2 V)
• TrilinearHT.Auto.cellColumnProduct D A hc m.succ = TrilinearHT.Auto.cellColumnProjection D (A m) hc ∘SL TrilinearHT.Auto.cellColumnProduct D A hc m

noncomputable def TrilinearHT.Auto.cellProductCoefficients {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (m : ℕ) (g : ↥(ColumnL2 V)) : EuclideanSpace ℂ V

The last-layer coefficient vector of a nonempty product, extended to all labels. This definition includes changing masks at different cells.

Equations

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

theorem TrilinearHT.Auto.cellColumnProduct_coeFn {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (m : ℕ) (g : ↥(ColumnL2 V)) : ↑↑((cellColumnProduct D A hc (m + 1)) g) =ᵐ[MeasureTheory.volume] (dyadicGridCell D.grid c.1 c.2).indicator (columnCombination D (A m) c (cellProjectionCoefficients D (A m) hc ((cellColumnProduct D A hc m) g)))

The cell product is represented by the last layer's constant coefficients.

theorem TrilinearHT.Auto.privateCoordinates_lower {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (a : EuclideanSpace ℂ V) (w : ColumnHilbert V) (hw : ∀ (v : V), w.ofLp (some v) = a.ofLp v * ↑√(D.privateWeight v)) : D.budget⁻¹ * ‖a‖ ≤ ‖w‖

Private coordinates recover arbitrary coefficient differences, even when the two anchors have different masks (lem:compression, line 569).

noncomputable def TrilinearHT.Auto.columnAnchorTolerance {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (a : ℝ) : ℝ

The source coefficient tolerance; a zero segment average causes no division by zero in the anchor construction.

Equations

• TrilinearHT.Auto.columnAnchorTolerance D a = D.budget⁻¹ ^ 10 * a

theorem TrilinearHT.Auto.columnAnchorTolerance_nonneg {V : Type u_1} [Fintype V] (D : ColumnTreeData V) {a : ℝ} (ha : 0 ≤ a) : 0 ≤ columnAnchorTolerance D a

noncomputable def TrilinearHT.Auto.columnRestartCount {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (m : ℕ) : ℕ

Blueprint lem:compression, line 567: the number of transitions in one attempt for a product with m layers.

Equations

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

theorem TrilinearHT.Auto.columnRestartCount_pos {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (m : ℕ) : 0 < columnRestartCount D m

noncomputable def TrilinearHT.Auto.columnCoefficientField {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (c : ℤ × ℤ) : EuclideanSpace ℂ V

A total coefficient field on cell indices. The zero extension outside the given finite tree is never used by its anchor generations.

Equations

• TrilinearHT.Auto.columnCoefficientField D A m g c = if hc : c ∈ D.cells then TrilinearHT.Auto.cellProductCoefficients D A hc m g else 0

theorem TrilinearHT.Auto.columnCoefficientField_of_mem {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) {c : ℤ × ℤ} (hc : c ∈ D.cells) : columnCoefficientField D A m g c = cellProductCoefficients D A hc m g

noncomputable def TrilinearHT.Auto.columnAnchors {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) (R : ℤ × ℤ) (n : ℕ) : Finset (ℤ × ℤ)

Anchors for an (m+1)-layer product, counting coefficient transitions.

Equations

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

noncomputable def TrilinearHT.Auto.columnAttempts {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) (R : ℤ × ℤ) (n : ℕ) : Finset (ℤ × ℤ)

Attempts restart every source-prescribed T coefficient transitions, using exactly the same input g and size a.

Equations

• TrilinearHT.Auto.columnAttempts D A m g a R n = TrilinearHT.Auto.columnAnchors D A m g a R (n * TrilinearHT.Auto.columnRestartCount D (m + 1))

theorem TrilinearHT.Auto.columnAttempts_succ {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) (R : ℤ × ℤ) (n : ℕ) : columnAttempts D A m g a R (n + 1) = (columnAttempts D A m g a R n).biUnion fun (K : ℤ × ℤ) => columnAnchors D A m g a K (columnRestartCount D (m + 1))

theorem TrilinearHT.Auto.columnAnchors_subset {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) {R : ℤ × ℤ} (hR : R ∈ D.cells) (n : ℕ) : columnAnchors D A m g a R n ⊆ D.cells

theorem TrilinearHT.Auto.columnAnchors_pairwiseDisjoint {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) (R : ℤ × ℤ) (n : ℕ) : (↑(columnAnchors D A m g a R n)).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell D.grid c.1 c.2

theorem TrilinearHT.Auto.columnAttempts_eq_empty {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) {a : ℝ} (ha : 0 ≤ a) {R : ℤ × ℤ} (hR : R ∈ D.cells) (n : ℕ) (hn : columnCompletionDepth D < n) : columnAttempts D A m g a R n = ∅

Finite physical depth terminates all restart attempts, even if the source transition count is much larger than that depth.

theorem TrilinearHT.Auto.cutColumnRange_le_of_refines {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (B C : Finset (ℤ × ℤ)) (hB : B ⊆ D.cells) (hC : C ⊆ D.cells) (hBd : (↑B).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell D.grid c.1 c.2) (hCd : (↑C).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell D.grid c.1 c.2) (hcover : ⋃ c ∈ C, dyadicGridCell D.grid c.1 c.2 = ⋃ b ∈ B, dyadicGridCell D.grid b.1 b.2) (href : ∀ c ∈ C, ∃ b ∈ B, dyadicGridCell D.grid c.1 c.2 ⊆ dyadicGridCell D.grid b.1 b.2) : cutColumnRange D A B hB ≤ cutColumnRange D A C hC

Refining a local cut partition enlarges the inherited column range, even when the partition root is a proper subcell of the original tree.

theorem TrilinearHT.Auto.cutColumnProjection_restrict_atom {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (C : Finset (ℤ × ℤ)) (hC : C ⊆ D.cells) (hdis : (↑C).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell D.grid c.1 c.2) {c : ℤ × ℤ} (hc : c ∈ C) (g : ↥(ColumnL2 V)) : (columnL2Restriction (dyadicGridCell D.grid c.1 c.2) ⋯) ((cutColumnProjection D A C hC) g) = (cellColumnProjection D A ⋯) g

Restricting a cut projection to one atom gives exactly the atom's original cell projection. This includes the refitted terminal atoms.

theorem TrilinearHT.Auto.cellColumnProduct_input_locality {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (m : ℕ) (g : ↥(ColumnL2 V)) : (cellColumnProduct D A hc (m + 1)) ((columnL2Restriction (dyadicGridCell D.grid c.1 c.2) ⋯) g) = (cellColumnProduct D A hc (m + 1)) g

A nonempty cell product depends only on the input on its own cell.

theorem TrilinearHT.Auto.cellColumnProduct_private {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (m : ℕ) (g : ↥(ColumnL2 V)) : ∀ᵐ (y : ℝ), y ∈ dyadicGridCell D.grid c.1 c.2 → ∀ (v : V), (↑↑((cellColumnProduct D A hc (m + 1)) g) y).ofLp (some v) = (cellProductCoefficients D A hc m g).ofLp v * ↑√(D.privateWeight v)

Each private coordinate of a cell product is its zero-extended last-layer coefficient times the fixed private weight.

theorem TrilinearHT.Auto.cellColumnProduct_difference_lower {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) {c b : ℤ × ℤ} (hc : c ∈ D.cells) (hb : b ∈ D.cells) (hcb : dyadicGridCell D.grid c.1 c.2 ⊆ dyadicGridCell D.grid b.1 b.2) (m : ℕ) (g : ↥(ColumnL2 V)) : ∀ᵐ (y : ℝ), y ∈ dyadicGridCell D.grid c.1 c.2 → D.budget⁻¹ * ‖cellProductCoefficients D A hc m g - cellProductCoefficients D A hb m g‖ ≤ ‖↑↑((cellColumnProduct D A hc (m + 1)) g) y - ↑↑((cellColumnProduct D A hb (m + 1)) g) y‖

The source private-coordinate recovery applies to the difference of products on nested anchor cells, despite their different masks.

noncomputable def TrilinearHT.Auto.columnAnchorCutDepth {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (R : ℤ × ℤ) : ℕ

Remaining physical depth at an attempt root in the completed tree.

Equations

• TrilinearHT.Auto.columnAnchorCutDepth D R = TrilinearHT.Auto.dyadicRemainingDepth D.root (TrilinearHT.Auto.columnCompletionDepth D) R

theorem TrilinearHT.Auto.columnAnchorCutDepth_bound {V : Type u_1} [Fintype V] (D : ColumnTreeData V) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (c : ℤ × ℤ) : c ∈ (completedColumnTree D).cells → c.1 ≤ R.1 + ↑(columnAnchorCutDepth D R)

noncomputable def TrilinearHT.Auto.completedColumnAnchorCuts {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) (R : ℤ × ℤ) (n : ℕ) : Finset (ℤ × ℤ)

Completed anchor partitions on an arbitrary attempt root of the completed column tree. Original masks are refitted on the terminal leaves.

Equations

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

theorem TrilinearHT.Auto.completedColumnAnchorCuts_subset {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (n : ℕ) : completedColumnAnchorCuts D A m g a R n ⊆ (completedColumnTree D).cells

theorem TrilinearHT.Auto.completedColumnAnchorCuts_disjoint {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) (R : ℤ × ℤ) (n : ℕ) : (↑(completedColumnAnchorCuts D A m g a R n)).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell D.grid c.1 c.2

theorem TrilinearHT.Auto.completedColumnAnchorCuts_union {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (n : ℕ) : ⋃ c ∈ completedColumnAnchorCuts D A m g a R n, dyadicGridCell D.grid c.1 c.2 = dyadicGridCell D.grid R.1 R.2

theorem TrilinearHT.Auto.completedColumnAnchorCuts_refines {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) (R : ℤ × ℤ) {n k : ℕ} (hnk : n ≤ k) {c : ℤ × ℤ} (hc : c ∈ completedColumnAnchorCuts D A m g a R k) : ∃ b ∈ completedColumnAnchorCuts D A m g a R n, dyadicGridCell D.grid c.1 c.2 ⊆ dyadicGridCell D.grid b.1 b.2

noncomputable def TrilinearHT.Auto.columnAnchorProjection {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (l n : ℕ) : ↥(ColumnL2 V) →L[ℂ] ↥(ColumnL2 V)

The layer projections on completed anchor partitions, indexed by coefficient transitions rather than physical depth.

Equations

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

theorem TrilinearHT.Auto.columnAnchorProjection_isStarProjection {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (l n : ℕ) : IsStarProjection (columnAnchorProjection D A m g a hR l n)

theorem TrilinearHT.Auto.columnAnchorProjection_nested {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (l : ℕ) {n k : ℕ} (hnk : n ≤ k) : columnAnchorProjection D A m g a hR l n ∘SL columnAnchorProjection D A m g a hR l k = columnAnchorProjection D A m g a hR l n

Blueprint lem:compression, line 569: every completed layer is a nested orthogonal projection family, proved from inherited masks and refinement.

theorem TrilinearHT.Auto.columnAnchorProjection_product_jumps {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (T : ℕ) (z : ↥(ColumnL2 V)) : ∑ n : Fin T, ‖(nestedProjectionProduct (columnAnchorProjection D A m g a hR) (m + 1) (↑n + 1)) z - (nestedProjectionProduct (columnAnchorProjection D A m g a hR) (m + 1) ↑n) z‖ ^ 2 ≤ ↑(m + 1) ^ 2 * projectionPrefixConstant T ^ (2 * m) * ‖z‖ ^ 2

The source jump theorem applies to the constructed anchor projections; no nestedness or Bessel condition is added as a new hypothesis.

theorem TrilinearHT.Auto.cellColumnProjection_input_superset {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) {s : Set ℝ} (hs : MeasurableSet s) (hcs : dyadicGridCell D.grid c.1 c.2 ⊆ s) (g : ↥(ColumnL2 V)) : (cellColumnProjection D A hc) ((columnL2Restriction s hs) g) = (cellColumnProjection D A hc) g

Restricting the input to any measurable superset of a cell leaves its projection unchanged.

theorem TrilinearHT.Auto.cellColumnProduct_input_superset {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) {s : Set ℝ} (hs : MeasurableSet s) (hcs : dyadicGridCell D.grid c.1 c.2 ⊆ s) (k : ℕ) (g : ↥(ColumnL2 V)) : (cellColumnProduct D A hc (k + 1)) ((columnL2Restriction s hs) g) = (cellColumnProduct D A hc (k + 1)) g

theorem TrilinearHT.Auto.columnAnchorProduct_restrict_atom {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (n : ℕ) {c : ℤ × ℤ} (hc : c ∈ completedColumnAnchorCuts D A m g a R n) (k : ℕ) (z : ↥(ColumnL2 V)) : (columnL2Restriction (dyadicGridCell D.grid c.1 c.2) ⋯) ((nestedProjectionProduct (columnAnchorProjection D A m g a hR) (k + 1) n) z) = (cellColumnProduct (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) ⋯ (k + 1)) z

At an anchor atom, a nonempty partition product equals the original cell product after restriction to that atom.

theorem TrilinearHT.Auto.columnAnchorProduct_ae_eq_atom {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (n : ℕ) {c : ℤ × ℤ} (hc : c ∈ completedColumnAnchorCuts D A m g a R n) (k : ℕ) : ∀ᵐ (y : ℝ), y ∈ dyadicGridCell D.grid c.1 c.2 → ↑↑((nestedProjectionProduct (columnAnchorProjection D A m g a hR) (k + 1) n) ((columnL2Restriction (dyadicGridCell D.grid R.1 R.2) ⋯) g)) y = ↑↑((cellColumnProduct (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) ⋯ (k + 1)) g) y

Restricting the input to the attempt root does not change any anchor product on an atom. This is the same-input restart requirement in the source.

theorem TrilinearHT.Auto.completedColumnAnchorCuts_anchor_mem {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (n : ℕ) {K : ℤ × ℤ} (hK : K ∈ columnAnchors (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) m g a R n) : K ∈ completedColumnAnchorCuts D A m g a R n

theorem TrilinearHT.Auto.columnAnchorProduct_jump_lower {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (n : ℕ) {K c : ℤ × ℤ} (hK : K ∈ columnAnchors (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) m g a R n) (hc : c ∈ dyadicNextAnchors D.grid (completedColumnTree D).cells (columnCoefficientField (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) m g) (columnAnchorTolerance D a) K) : ∀ᵐ (y : ℝ), y ∈ dyadicGridCell D.grid c.1 c.2 → D.budget⁻¹ * columnAnchorTolerance D a < ‖↑↑((nestedProjectionProduct (columnAnchorProjection D A m g a hR) (m + 1) (n + 1)) ((columnL2Restriction (dyadicGridCell D.grid R.1 R.2) ⋯) g)) y - ↑↑((nestedProjectionProduct (columnAnchorProjection D A m g a hR) (m + 1) n) ((columnL2Restriction (dyadicGridCell D.grid R.1 R.2) ⋯) g)) y‖

Blueprint lem:compression, line 569: on every next anchor the successive partition-product jump is strictly greater than D⁻¹ τ a almost everywhere. Both products use the same input restricted to the attempt root.

theorem TrilinearHT.Auto.columnAnchorProduct_restart_budget_sharp {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) {a : ℝ} (ha : 0 ≤ a) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (T : ℕ) : ↑T * D.budget⁻¹ ^ 2 * (D.budget⁻¹ ^ 10) ^ 2 * a ^ 2 * ∑ r ∈ columnAnchors (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) m g a R T, dyadicGridLength D.grid r.1 ≤ ↑(m + 1) ^ 2 * projectionPrefixConstant T ^ (2 * m) * ‖(columnL2Restriction (dyadicGridCell D.grid R.1 R.2) ⋯) g‖ ^ 2

Blueprint lem:compression, lines 570–572: all T transitions on each disjoint restart root charge its length to the product-jump energy. The exponent here is the sharper 2(m-1) from the jump theorem, written with m+1 layers; the source's 2m version follows below.

theorem TrilinearHT.Auto.columnAnchorProduct_restart_budget {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) {a : ℝ} (ha : 0 ≤ a) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (T : ℕ) : ↑T * D.budget⁻¹ ^ 2 * (D.budget⁻¹ ^ 10) ^ 2 * a ^ 2 * ∑ r ∈ columnAnchors (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) m g a R T, dyadicGridLength D.grid r.1 ≤ ↑(m + 1) ^ 2 * projectionPrefixConstant T ^ (2 * (m + 1)) * ‖(columnL2Restriction (dyadicGridCell D.grid R.1 R.2) ⋯) g‖ ^ 2

The exact printed restart-length budget, with m+1 denoting the nonempty product length and with no spatial-depth factor.

theorem TrilinearHT.Auto.columnL2Restriction_norm_sq {V : Type u_1} [Fintype V] (s : Set ℝ) (hs : MeasurableSet s) (g : ↥(ColumnL2 V)) : ‖(columnL2Restriction s hs) g‖ ^ 2 = ∫ (y : ℝ) in s, ‖↑↑g y‖ ^ 2

Restriction energy is the integral over the restricting set.

theorem TrilinearHT.Auto.columnL2Restriction_energy_le {V : Type u_1} [Fintype V] (G : RealDyadicGrid) (g : ↥(ColumnL2 V)) (B : ℝ) (hB : 0 ≤ B) (hg : ∀ᵐ (y : ℝ), ‖↑↑g y‖ ≤ B) (c : ℤ × ℤ) : ‖(columnL2Restriction (dyadicGridCell G c.1 c.2) ⋯) g‖ ^ 2 ≤ B ^ 2 * dyadicGridLength G c.1

The global essential bound charges each restricted energy to cell length.

noncomputable def TrilinearHT.Auto.columnRestartFactor {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (m T : ℕ) : ℝ

The common length and energy contraction factor printed in the source.

Equations

• TrilinearHT.Auto.columnRestartFactor D m T = 16 * D.budget ^ 32 * ↑m ^ 2 * TrilinearHT.Auto.projectionPrefixConstant T ^ (2 * m) / ↑T

theorem TrilinearHT.Auto.columnRestartFactor_nonneg {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (m T : ℕ) : 0 ≤ columnRestartFactor D m T

theorem TrilinearHT.Auto.columnRestartFactor_balance {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (m T : ℕ) (hT : 0 < T) (a : ℝ) : ↑T * D.budget⁻¹ ^ 2 * (D.budget⁻¹ ^ 10) ^ 2 * a ^ 2 * columnRestartFactor D m T = ↑m ^ 2 * projectionPrefixConstant T ^ (2 * m) * (4 * D.budget ^ 5 * a) ^ 2

Exact cancellation of the source jump threshold against the bounded representative energy; no size or depth parameter remains in the factor.

theorem TrilinearHT.Auto.columnRestart_length_le_of_pos {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) {a : ℝ} (ha : 0 < a) (hg : ∀ᵐ (y : ℝ), ‖↑↑g y‖ ≤ 4 * D.budget ^ 5 * a) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (T : ℕ) (hT : 0 < T) : ∑ r ∈ columnAnchors (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) m g a R T, dyadicGridLength D.grid r.1 ≤ columnRestartFactor D (m + 1) T * dyadicGridLength D.grid R.1

Blueprint lem:compression, lines 573–578: the restart length contracts by the printed factor whenever the segment average is positive.

theorem TrilinearHT.Auto.columnRestart_energy_le_of_pos {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) {a : ℝ} (ha : 0 < a) (hg : ∀ᵐ (y : ℝ), ‖↑↑g y‖ ≤ 4 * D.budget ^ 5 * a) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (T : ℕ) (hT : 0 < T) : ∑ r ∈ columnAnchors (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) m g a R T, ‖(columnL2Restriction (dyadicGridCell D.grid r.1 r.2) ⋯) g‖ ^ 2 ≤ columnRestartFactor D (m + 1) T * ‖(columnL2Restriction (dyadicGridCell D.grid R.1 R.2) ⋯) g‖ ^ 2

The same factor contracts the energy on restart roots relative to the actual input energy on the attempt root, not merely its uniform majorant.

theorem TrilinearHT.Auto.columnCoefficientField_zero {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) : columnCoefficientField D A m 0 = fun (x : ℤ × ℤ) => 0

Zero input has zero last-layer coefficients for every mask and cell.

theorem TrilinearHT.Auto.columnAnchors_zero {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (R : ℤ × ℤ) (T : ℕ) (hT : 0 < T) : columnAnchors D A m 0 0 R T = ∅

A zero-size, zero-input segment never makes even one coefficient transition.

theorem TrilinearHT.Auto.columnRestart_contraction {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) {a : ℝ} (ha : 0 ≤ a) (hg : ∀ᵐ (y : ℝ), ‖↑↑g y‖ ≤ 4 * D.budget ^ 5 * a) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (T : ℕ) (hT : 0 < T) : ∑ r ∈ columnAnchors (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) m g a R T, dyadicGridLength D.grid r.1 ≤ columnRestartFactor D (m + 1) T * dyadicGridLength D.grid R.1 ∧ ∑ r ∈ columnAnchors (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) m g a R T, ‖(columnL2Restriction (dyadicGridCell D.grid r.1 r.2) ⋯) g‖ ^ 2 ≤ columnRestartFactor D (m + 1) T * ‖(columnL2Restriction (dyadicGridCell D.grid R.1 R.2) ⋯) g‖ ^ 2

Blueprint lem:compression, lines 573–578: both restart length and restart energy contract by exactly the printed factor, including zero-size segments.

theorem TrilinearHT.Auto.columnRestartFactor_lt_half {V : Type u_1} [Fintype V] (D : ColumnTreeData V) {m : ℕ} (hm : 1 ≤ m) : columnRestartFactor D m (columnRestartCount D m) < 1 / 2

The exact transition count in the source makes the column restart factor strictly smaller than one half for every nonempty product.

noncomputable def TrilinearHT.Auto.completedColumnAttempts {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) (R : ℤ × ℤ) (n : ℕ) : Finset (ℤ × ℤ)

Attempt generations in the completed tree, with the original masks extended once and the same moment input and size at every restart.

Equations

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

theorem TrilinearHT.Auto.completedColumnAttempts_zero {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) (R : ℤ × ℤ) : completedColumnAttempts D A m g a R 0 = {R}

theorem TrilinearHT.Auto.completedColumnAttempts_subset {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (n : ℕ) : completedColumnAttempts D A m g a R n ⊆ (completedColumnTree D).cells

theorem TrilinearHT.Auto.completedColumnAttempts_succ {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) (R : ℤ × ℤ) (n : ℕ) : completedColumnAttempts D A m g a R (n + 1) = (completedColumnAttempts D A m g a R n).biUnion fun (K : ℤ × ℤ) => columnAnchors (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) m g a K (columnRestartCount D (m + 1))

theorem TrilinearHT.Auto.completedColumnAttempts_weight_packing {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (w : ℤ × ℤ → ℝ) (hw : ∀ (r : ℤ × ℤ), 0 ≤ w r) (hchild : ∀ K ∈ (completedColumnTree D).cells, ∑ r ∈ columnAnchors (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) m g a K (columnRestartCount D (m + 1)), w r ≤ columnRestartFactor D (m + 1) (columnRestartCount D (m + 1)) * w K) : (Summable fun (n : ℕ) => ∑ r ∈ completedColumnAttempts D A m g a R n, w r) ∧ ∑' (n : ℕ), ∑ r ∈ completedColumnAttempts D A m g a R n, w r ≤ 2 * w R

Any nonnegative root cost obeying the proved restart contraction has total cost at most twice its initial value.

theorem TrilinearHT.Auto.completedColumnAttempts_packing {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) {a : ℝ} (ha : 0 ≤ a) (hg : ∀ᵐ (y : ℝ), ‖↑↑g y‖ ≤ 4 * D.budget ^ 5 * a) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) : have F := completedColumnAttempts D A m g a R; have E := fun (r : ℤ × ℤ) => ‖(columnL2Restriction (dyadicGridCell D.grid r.1 r.2) ⋯) g‖ ^ 2; (Summable fun (n : ℕ) => ∑ r ∈ F n, dyadicGridLength D.grid r.1) ∧ ∑' (n : ℕ), ∑ r ∈ F n, dyadicGridLength D.grid r.1 ≤ 2 * dyadicGridLength D.grid R.1 ∧ (Summable fun (n : ℕ) => ∑ r ∈ F n, E r) ∧ ∑' (n : ℕ), ∑ r ∈ F n, E r ≤ 2 * E R

Blueprint lem:compression, line 579: the sum of all attempt lengths and the sum of all restricted energies are each at most twice their initial value.

theorem TrilinearHT.Auto.columnMomentRepresentative_root_restriction {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) (z : ↥(ColumnL2 V)) {K : ℤ × ℤ} (hK : K ∈ columnSizeRoots D z) : (columnL2Restriction (dyadicGridCell D.grid K.1 K.2) ⋯) (columnMomentRepresentative D A z hK) = columnMomentRepresentative D A z hK

noncomputable def TrilinearHT.Auto.completedColumnAttemptRoots {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) (R : ℤ × ℤ) : Finset (ℤ × ℤ)

The finite set of all attempt roots; generations beyond this horizon are empty by strict descent in the completed finite tree.

Equations

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

theorem TrilinearHT.Auto.completedColumnAttemptRoots_subset {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) : completedColumnAttemptRoots D A m g a R ⊆ (completedColumnTree D).cells

theorem TrilinearHT.Auto.completedColumnAttemptRoots_cost_le {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) (R : ℤ × ℤ) (w : ℤ × ℤ → ℝ) (hw : ∀ (r : ℤ × ℤ), 0 ≤ w r) (hs : Summable fun (n : ℕ) => ∑ r ∈ completedColumnAttempts D A m g a R n, w r) : ∑ r ∈ completedColumnAttemptRoots D A m g a R, w r ≤ ∑' (n : ℕ), ∑ r ∈ completedColumnAttempts D A m g a R n, w r

Passing from generations to their union can only decrease a nonnegative cost, even before uniqueness of the attempt assignment is used.

theorem TrilinearHT.Auto.completedColumnAttemptRoots_mem_of_generation {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) {a : ℝ} (ha : 0 ≤ a) {R r : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) {n : ℕ} (hr : r ∈ completedColumnAttempts D A m g a R n) : r ∈ completedColumnAttemptRoots D A m g a R

theorem TrilinearHT.Auto.completedColumnAttemptRoots_root_mem {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) (R : ℤ × ℤ) : R ∈ completedColumnAttemptRoots D A m g a R

theorem TrilinearHT.Auto.completedColumnAttemptRoots_restart_mem {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) {a : ℝ} (ha : 0 ≤ a) {R K r : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (hK : K ∈ completedColumnAttemptRoots D A m g a R) (hr : r ∈ columnAnchors (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) m g a K (columnRestartCount D (m + 1))) : r ∈ completedColumnAttemptRoots D A m g a R

theorem TrilinearHT.Auto.completedColumnAttemptRoots_retained_assignment {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) {a : ℝ} (ha : 0 ≤ a) {R u : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (huR : dyadicGridCell D.grid u.1 u.2 ⊆ dyadicGridCell D.grid R.1 R.2) : ∃ K ∈ completedColumnAttemptRoots D A m g a R, dyadicGridCell D.grid u.1 u.2 ⊆ dyadicGridCell D.grid K.1 K.2 ∧ ∀ r ∈ columnAnchors (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) m g a K (columnRestartCount D (m + 1)), ¬dyadicGridCell D.grid u.1 u.2 ⊆ dyadicGridCell D.grid r.1 r.2

Every row cell is retained by a deepest attempt root containing it. Strict depth increase at a restart rules out a further containing restart.

theorem TrilinearHT.Auto.completedColumnAttemptRoots_anchor_assignment {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) {a : ℝ} (ha : 0 ≤ a) {R u : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (hu : u ∈ (completedColumnTree D).cells) (huR : dyadicGridCell D.grid u.1 u.2 ⊆ dyadicGridCell D.grid R.1 R.2) : ∃ K ∈ completedColumnAttemptRoots D A m g a R, ∃ j < columnRestartCount D (m + 1), ∃ b ∈ completedColumnAnchorCuts D A m g a K j, dyadicGridCell D.grid u.1 u.2 ⊆ dyadicGridCell D.grid b.1 b.2 ∧ ‖columnCoefficientField (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) m g u - columnCoefficientField (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) m g b‖ ≤ columnAnchorTolerance D a

Blueprint lem:compression, line 581: every decision cell below the initial root is assigned to an attempt and an anchor partition atom at a time strictly below T, with the stated coefficient error.

noncomputable def TrilinearHT.Auto.columnRowFamilyRestrict {V : Type u_1} {ι : Type u_2} {F : Type u_3} [Fintype V] [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (D : ColumnTreeData V) (B : ColumnRowFamily D ι F) (s : Finset ι) : ColumnRowFamily D (↥s) F

Selecting rows preserves the original square-sum bound and exact decision-cell locality, as needed when grouping rows by attempts.

Equations

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

theorem TrilinearHT.Auto.columnRowFamily_congr_on_cell {V : Type u_1} {ι : Type u_2} {F : Type u_3} [Fintype V] [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (D : ColumnTreeData V) (B : ColumnRowFamily D ι F) (i : ι) (z w : ↥(ColumnL2 V)) (h : ∀ᵐ (y : ℝ), y ∈ dyadicGridCell D.grid (B.decision i).1 (B.decision i).2 → ↑↑z y = ↑↑w y) : (B.row i) z = (B.row i) w

A local row only sees the almost-everywhere values on its decision cell.

theorem TrilinearHT.Auto.columnAnchorProduct_row_eq {V : Type u_1} {ι : Type u_2} {F : Type u_3} [Fintype V] [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (B : ColumnRowFamily D ι F) (i : ι) (n : ℕ) {b : ℤ × ℤ} (hb : b ∈ completedColumnAnchorCuts D A m g a R n) (hu : dyadicGridCell D.grid (B.decision i).1 (B.decision i).2 ⊆ dyadicGridCell D.grid b.1 b.2) : (B.row i) ((cellColumnProduct (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) ⋯ (m + 1)) g) = (B.row i) ((nestedProjectionProduct (columnAnchorProjection D A m g a hR) (m + 1) n) ((columnL2Restriction (dyadicGridCell D.grid R.1 R.2) ⋯) g))

Exact equality of an anchor row with its prefix-product row; the decision cell may be arbitrarily far below the anchor atom.

theorem TrilinearHT.Auto.columnAnchorProduct_rows_bound {V : Type u_1} {ι : Type u_2} {F : Type u_3} [Fintype V] [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) (a : ℝ) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (B : ColumnRowFamily D ι F) (hB : B.bound ≤ 1) (n : ι → ℕ) (hn : ∀ (i : ι), n i < columnRestartCount D (m + 1)) (b : ι → ℤ × ℤ) (hb : ∀ (i : ι), b i ∈ completedColumnAnchorCuts D A m g a R (n i)) (hu : ∀ (i : ι), dyadicGridCell D.grid (B.decision i).1 (B.decision i).2 ⊆ dyadicGridCell D.grid (b i).1 (b i).2) : ∑ i : ι, ‖(B.row i) ((cellColumnProduct (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) ⋯ (m + 1)) g)‖ ^ 2 ≤ projectionPrefixConstant (columnRestartCount D (m + 1)) ^ (2 * (m + 1)) * ‖(columnL2Restriction (dyadicGridCell D.grid R.1 R.2) ⋯) g‖ ^ 2

Blueprint lem:compression, line 581: the squared anchor-row sum on an attempt is bounded by L_T^(2m) times its restricted input energy, independently of the spatial depths of the selected row cells.

theorem TrilinearHT.Auto.birthColumn_memLp {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (v : V) : MeasureTheory.MemLp ((dyadicGridCell D.grid (D.birth v).1 (D.birth v).2).indicator (privateColumnValue D.scalar D.privateWeight v)) 2 MeasureTheory.volume

A full column is supported on its birth cell, exactly as in the error term of blueprint lem:compression, line 582.

noncomputable def TrilinearHT.Auto.birthColumnLp {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (v : V) : ↥(ColumnL2 V)

Birth column represented as an element of the column L² space.

Equations

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

theorem TrilinearHT.Auto.birthColumnLp_coeFn {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (v : V) : ↑↑(birthColumnLp D v) =ᵐ[MeasureTheory.volume] (dyadicGridCell D.grid (D.birth v).1 (D.birth v).2).indicator (privateColumnValue D.scalar D.privateWeight v)

theorem TrilinearHT.Auto.birthColumnLp_square_sum_ae {V : Type u_1} [Fintype V] (D : ColumnTreeData V) : ∀ᵐ (y : ℝ), ∑ v : V, ‖↑↑(birthColumnLp D v) y‖ ^ 2 ≤ D.budget ^ 3

The original path budget bounds the squared column mass pointwise, without counting labels born on disjoint branches.

theorem TrilinearHT.Auto.birthColumnLp_restricted_energy {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (R : ℤ × ℤ) : ∑ v : V, ‖(columnL2Restriction (dyadicGridCell D.grid R.1 R.2) ⋯) (birthColumnLp D v)‖ ^ 2 ≤ D.budget ^ 3 * dyadicGridLength D.grid R.1

Blueprint lem:compression, lines 587–589: integrating the actual path budget over an attempt gives the exact D^3 |R| column-energy bound.

theorem TrilinearHT.Auto.cellColumnLp_eq_restrict_birth {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (v : ↥(A.labels c)) : cellColumnLp D A hc v = (columnL2Restriction (dyadicGridCell D.grid c.1 c.2) ⋯) (birthColumnLp D ↑v)

theorem TrilinearHT.Auto.cellColumnSynthesis_birth_columns {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (a : CellCoefficients D A c) : (cellColumnSynthesis D A hc) a = ∑ v : V, (extendCellCoefficients D A c a).ofLp v • (columnL2Restriction (dyadicGridCell D.grid c.1 c.2) ⋯) (birthColumnLp D v)

Synthesis written in the common full label space, with unavailable coefficients extended by zero and the original birth columns unchanged.

theorem TrilinearHT.Auto.columnRowFamily_restriction_eq {V : Type u_1} {ι : Type u_2} {F : Type u_3} [Fintype V] [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (D : ColumnTreeData V) (B : ColumnRowFamily D ι F) (i : ι) {s t : Set ℝ} (hs : MeasurableSet s) (ht : MeasurableSet t) (hus : dyadicGridCell D.grid (B.decision i).1 (B.decision i).2 ⊆ s) (hut : dyadicGridCell D.grid (B.decision i).1 (B.decision i).2 ⊆ t) (z : ↥(ColumnL2 V)) : (B.row i) ((columnL2Restriction s hs) z) = (B.row i) ((columnL2Restriction t ht) z)

For a local row, restrictions to any two supersets of its decision cell are interchangeable.

theorem TrilinearHT.Auto.cellColumnProduct_row_birth_formula {V : Type u_1} {ι : Type u_2} {F : Type u_3} [Fintype V] [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (B : ColumnRowFamily D ι F) (i : ι) {c R : ℤ × ℤ} (hc : c ∈ D.cells) (huc : dyadicGridCell D.grid (B.decision i).1 (B.decision i).2 ⊆ dyadicGridCell D.grid c.1 c.2) (huR : dyadicGridCell D.grid (B.decision i).1 (B.decision i).2 ⊆ dyadicGridCell D.grid R.1 R.2) (m : ℕ) (g : ↥(ColumnL2 V)) : (B.row i) ((cellColumnProduct D A hc (m + 1)) g) = ∑ v : V, (cellProductCoefficients D A hc m g).ofLp v • (B.row i) ((columnL2Restriction (dyadicGridCell D.grid R.1 R.2) ⋯) (birthColumnLp D v))

Exact local expansion of a product row using the birth-supported columns restricted only to the attempt root.

theorem TrilinearHT.Auto.cellColumnProduct_row_error_formula {V : Type u_1} {ι : Type u_2} {F : Type u_3} [Fintype V] [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (B : ColumnRowFamily D ι F) (i : ι) {c b R : ℤ × ℤ} (hc : c ∈ D.cells) (hb : b ∈ D.cells) (huc : dyadicGridCell D.grid (B.decision i).1 (B.decision i).2 ⊆ dyadicGridCell D.grid c.1 c.2) (hub : dyadicGridCell D.grid (B.decision i).1 (B.decision i).2 ⊆ dyadicGridCell D.grid b.1 b.2) (huR : dyadicGridCell D.grid (B.decision i).1 (B.decision i).2 ⊆ dyadicGridCell D.grid R.1 R.2) (m : ℕ) (g : ↥(ColumnL2 V)) : (B.row i) ((cellColumnProduct D A hc (m + 1)) g - (cellColumnProduct D A hb (m + 1)) g) = ∑ v : V, (cellProductCoefficients D A hc m g - cellProductCoefficients D A hb m g).ofLp v • (B.row i) ((columnL2Restriction (dyadicGridCell D.grid R.1 R.2) ⋯) (birthColumnLp D v))

Blueprint lem:compression, lines 581–584: subtracting the anchor product gives exactly the coefficient-error row stated in the source.

theorem TrilinearHT.Auto.columnRowFamily_coefficient_rows_bound {V : Type u_1} {ι : Type u_2} {F : Type u_3} [Fintype V] [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (D : ColumnTreeData V) (B : ColumnRowFamily D ι F) (hB : B.bound ≤ 1) (R : ℤ × ℤ) (e : ι → EuclideanSpace ℂ V) {δ : ℝ} (hδ : 0 ≤ δ) (he : ∀ (i : ι), ‖e i‖ ≤ δ) : ∑ i : ι, ‖∑ v : V, (e i).ofLp v • (B.row i) ((columnL2Restriction (dyadicGridCell D.grid R.1 R.2) ⋯) (birthColumnLp D v))‖ ^ 2 ≤ δ ^ 2 * D.budget ^ 3 * dyadicGridLength D.grid R.1

Blueprint lem:compression, lines 585–589: coefficient errors of Euclidean norm at most δ have squared row sum at most δ² D³ |R|. The estimate uses the original row inequality separately for each column.

theorem TrilinearHT.Auto.columnAnchorProduct_error_rows_bound {V : Type u_1} {ι : Type u_2} {F : Type u_3} [Fintype V] [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) {a : ℝ} (ha : 0 ≤ a) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (B : ColumnRowFamily D ι F) (hB : B.bound ≤ 1) (n : ι → ℕ) (b : ι → ℤ × ℤ) (hb : ∀ (i : ι), b i ∈ completedColumnAnchorCuts D A m g a R (n i)) (hu : ∀ (i : ι), dyadicGridCell D.grid (B.decision i).1 (B.decision i).2 ⊆ dyadicGridCell D.grid (b i).1 (b i).2) (he : ∀ (i : ι), ‖columnCoefficientField (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) m g (B.decision i) - columnCoefficientField (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) m g (b i)‖ ≤ columnAnchorTolerance D a) : ∑ i : ι, ‖(B.row i) ((cellColumnProduct (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) ⋯ (m + 1)) g - (cellColumnProduct (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) ⋯ (m + 1)) g)‖ ^ 2 ≤ columnAnchorTolerance D a ^ 2 * D.budget ^ 3 * dyadicGridLength D.grid R.1

The error estimate applies to the actual difference between each decision-cell product and its assigned anchor product.

theorem TrilinearHT.Auto.columnAttempt_rows_bound {V : Type u_1} {ι : Type u_2} {F : Type u_3} [Fintype V] [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) {a : ℝ} (ha : 0 ≤ a) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (B : ColumnRowFamily D ι F) (hB : B.bound ≤ 1) (n : ι → ℕ) (hn : ∀ (i : ι), n i < columnRestartCount D (m + 1)) (b : ι → ℤ × ℤ) (hb : ∀ (i : ι), b i ∈ completedColumnAnchorCuts D A m g a R (n i)) (hu : ∀ (i : ι), dyadicGridCell D.grid (B.decision i).1 (B.decision i).2 ⊆ dyadicGridCell D.grid (b i).1 (b i).2) (he : ∀ (i : ι), ‖columnCoefficientField (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) m g (B.decision i) - columnCoefficientField (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) m g (b i)‖ ≤ columnAnchorTolerance D a) : ∑ i : ι, ‖(B.row i) ((cellColumnProduct (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) ⋯ (m + 1)) g)‖ ^ 2 ≤ 2 * projectionPrefixConstant (columnRestartCount D (m + 1)) ^ (2 * (m + 1)) * ‖(columnL2Restriction (dyadicGridCell D.grid R.1 R.2) ⋯) g‖ ^ 2 + 2 * columnAnchorTolerance D a ^ 2 * D.budget ^ 3 * dyadicGridLength D.grid R.1

Combining the proved anchor and coefficient-error estimates gives the squared row bound for one attempt (lem:compression, lines 592–595).

theorem TrilinearHT.Auto.columnAttemptFamily_rows_bound {V : Type u_1} {ι : Type u_2} {F : Type u_3} [Fintype V] [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (g : ↥(ColumnL2 V)) {a : ℝ} (ha : 0 ≤ a) (hg : ∀ᵐ (y : ℝ), ‖↑↑g y‖ ≤ 4 * D.budget ^ 5 * a) {R : ℤ × ℤ} (hR : R ∈ (completedColumnTree D).cells) (B : ColumnRowFamily D ι F) (hB : B.bound ≤ 1) (huR : ∀ (i : ι), dyadicGridCell D.grid (B.decision i).1 (B.decision i).2 ⊆ dyadicGridCell D.grid R.1 R.2) : ∑ i : ι, ‖(B.row i) ((cellColumnProduct (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) ⋯ (m + 1)) g)‖ ^ 2 ≤ 4 * projectionPrefixConstant (columnRestartCount D (m + 1)) ^ (2 * (m + 1)) * ‖(columnL2Restriction (dyadicGridCell D.grid R.1 R.2) ⋯) g‖ ^ 2 + 4 * columnAnchorTolerance D a ^ 2 * D.budget ^ 3 * dyadicGridLength D.grid R.1

Summing the constructed attempts gives a depth-independent bound below one initial root, using both length and restricted-energy packing.

theorem TrilinearHT.Auto.columnMoment_segment_rows_bound {V : Type u_1} {ι : Type u_2} {F : Type u_3} [Fintype V] [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (z : ↥(ColumnL2 V)) {K : ℤ × ℤ} (hK : K ∈ columnSizeRoots D z) (B : ColumnRowFamily D ι F) (hB : B.bound ≤ 1) (huK : ∀ (i : ι), dyadicGridCell D.grid (B.decision i).1 (B.decision i).2 ⊆ dyadicGridCell D.grid K.1 K.2) : have g := columnMomentRepresentative D (A 0) z hK; ∑ i : ι, ‖(B.row i) ((cellColumnProduct (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) ⋯ (m + 1)) g)‖ ^ 2 ≤ 4 * projectionPrefixConstant (columnRestartCount D (m + 1)) ^ (2 * (m + 1)) * ‖g‖ ^ 2 + 4 * columnAnchorTolerance D (columnCellAverage D z K) ^ 2 * D.budget ^ 3 * dyadicGridLength D.grid K.1

Blueprint lem:compression, lines 591–595: all attempts of one size segment cost at most four times its moment energy and length budget.

theorem TrilinearHT.Auto.completedColumnMask_product_eq {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) (k : ℕ) : cellColumnProduct (completedColumnTree D) (fun (l : ℕ) => completedColumnMask D (A l)) ⋯ k = cellColumnProduct D A hc k

Completing the finite tree leaves every product at an original cell unchanged.

theorem TrilinearHT.Auto.columnMomentRepresentative_preserves_product {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (z : ↥(ColumnL2 V)) {K u : ℤ × ℤ} (hK : K ∈ columnSizeRoots D z) (hu : u ∈ D.cells) (hsegment : u ∈ columnSizeSegment D z K) (m : ℕ) : (cellColumnProduct D A hu (m + 1)) (columnMomentRepresentative D (A 0) z hK) = (cellColumnProduct D A hu (m + 1)) z

Preservation of the first projection by the moment representative preserves the entire ordered nonempty product on its size segment.

theorem TrilinearHT.Auto.columnCompression_size_sum {V : Type u_1} {ι : Type u_2} {F : Type u_3} [Fintype V] [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (z : ↥(ColumnL2 V)) (B : ColumnRowFamily D ι F) (hB : B.bound ≤ 1) : ∑ i : ι, ‖(B.row i) ((cellColumnProduct D A ⋯ (m + 1)) z)‖ ^ 2 ≤ 4 * projectionPrefixConstant (columnRestartCount D (m + 1)) ^ (2 * (m + 1)) * columnMomentEnergy D (A 0) z + 4 * D.budget⁻¹ ^ 20 * D.budget ^ 3 * ∑ K ∈ columnSizeRoots D z, columnCellAverage D z K ^ 2 * dyadicGridLength D.grid K.1

Blueprint lem:compression, lines 591–595: grouping the original rows by their size segments yields the moment-energy and size-energy sum.

theorem TrilinearHT.Auto.columnCompression_logarithmic_square_bound {V : Type u_1} {ι : Type u_2} {F : Type u_3} [Fintype V] [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (z : ↥(ColumnL2 V)) (B : ColumnRowFamily D ι F) (hB : B.bound ≤ 1) : ∑ i : ι, ‖(B.row i) ((cellColumnProduct D A ⋯ (m + 1)) z)‖ ^ 2 ≤ (4 * projectionPrefixConstant (columnRestartCount D (m + 1)) ^ (2 * (m + 1)) * (7 / Real.log 2 * Real.log (2 * D.budget)) + 64 / 3 * D.budget⁻¹ ^ 20 * D.budget ^ 3) * ‖z‖ ^ 2

The logarithmic moment-energy bound and geometric size-energy bound give the depth-independent squared estimate in lem:compression, line 595.

theorem TrilinearHT.Auto.columnBudget_log_one_le {V : Type u_1} [Fintype V] (D : ColumnTreeData V) : 1 ≤ Real.log (2 * D.budget)

theorem TrilinearHT.Auto.columnCompression_clean_square_bound {V : Type u_1} {ι : Type u_2} {F : Type u_3} [Fintype V] [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (z : ↥(ColumnL2 V)) (B : ColumnRowFamily D ι F) (hB : B.bound ≤ 1) : ∑ i : ι, ‖(B.row i) ((cellColumnProduct D A ⋯ (m + 1)) z)‖ ^ 2 ≤ 128 * projectionPrefixConstant (columnRestartCount D (m + 1)) ^ (2 * (m + 1)) * Real.log (2 * D.budget) * ‖z‖ ^ 2

A uniform numerical form of the global squared compression bound.

theorem TrilinearHT.Auto.columnCompression_nonempty_bound {V : Type u_1} {ι : Type u_2} {F : Type u_3} [Fintype V] [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (z : ↥(ColumnL2 V)) (B : ColumnRowFamily D ι F) (hB : B.bound ≤ 1) : (finiteRowNorm fun (i : ι) => (B.row i) ((cellColumnProduct D A ⋯ (m + 1)) z)) ≤ (512 * (↑m + 2) ^ 3 * Real.log (2 * D.budget)) ^ (m + 2) * ‖z‖

An explicit polynomial-logarithmic bound for nonempty products, stronger than the unspecified universal-constant form in the source.

theorem TrilinearHT.Auto.columnSpatialCompression {V : Type u_1} {ι : Type u_2} {F : Type u_3} [Fintype V] [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (m : ℕ) (z : ↥(ColumnL2 V)) (B : ColumnRowFamily D ι F) (hB : B.bound ≤ 1) : (finiteRowNorm fun (i : ι) => (B.row i) ((cellColumnProduct D A ⋯ m) z)) ≤ (512 * (↑m + 1) ^ 512 * Real.log (2 * D.budget)) ^ (512 * (m + 1)) * ‖z‖

Blueprint eq:compression, lines 545–548 and 597: spatial compression for every number of inherited projection factors, including the empty product. The universal constant can be taken to be 512; the bound is independent of tree depth and the total number of labels.

noncomputable def TrilinearHT.Auto.columnCompressionBase {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (m : ℕ) : ℝ

Base logarithmic budget for compressing moments of order m.

Equations

• TrilinearHT.Auto.columnCompressionBase D m = 512 * (↑m + 1) ^ 512 * Real.log (2 * D.budget)

noncomputable def TrilinearHT.Auto.columnCompressionBound {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (m : ℕ) : ℝ

Moment-compression bound obtained by raising the base budget to its prescribed power.

Equations

• TrilinearHT.Auto.columnCompressionBound D m = TrilinearHT.Auto.columnCompressionBase D m ^ (512 * (m + 1))

theorem TrilinearHT.Auto.columnCompressionBase_one_le {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (m : ℕ) : 1 ≤ columnCompressionBase D m

theorem TrilinearHT.Auto.columnCompressionBound_one_le {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (m : ℕ) : 1 ≤ columnCompressionBound D m

theorem TrilinearHT.Auto.columnCompressionBound_mono {V : Type u_1} [Fintype V] (D : ColumnTreeData V) {m n : ℕ} (hmn : m ≤ n) : columnCompressionBound D m ≤ columnCompressionBound D n

theorem TrilinearHT.Auto.cellColumnProduct_congr {V : Type u_1} [Fintype V] (D : ColumnTreeData V) {A C : ℕ → InheritedColumnMask D} {c : ℤ × ℤ} (hc : c ∈ D.cells) (n : ℕ) (h : ∀ j < n, A j = C j) : cellColumnProduct D A hc n = cellColumnProduct D C hc n

theorem TrilinearHT.Auto.columnSubproduct_eq_shorter_product {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (σ : ℕ → Bool) (m : ℕ) : ∃ k ≤ m, ∃ (C : ℕ → InheritedColumnMask D), ∀ (c : ℤ × ℤ) (hc : c ∈ D.cells), operatorSubproduct (fun (l : ℕ) => cellColumnProjection D (A l) hc) σ m = cellColumnProduct D C hc k

Every ordered selection of column factors is a shorter product of the same inherited masks, uniformly on every original decision cell.

theorem TrilinearHT.Auto.columnSubproduct_rows_bound {V : Type u_1} {ι : Type u_2} {F : Type u_3} [Fintype V] [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (σ : ℕ → Bool) (m : ℕ) (z : ↥(ColumnL2 V)) (B : ColumnRowFamily D ι F) (hB : B.bound ≤ 1) : (finiteRowNorm fun (i : ι) => (B.row i) ((operatorSubproduct (fun (l : ℕ) => cellColumnProjection D (A l) ⋯) σ m) z)) ≤ columnCompressionBound D m * ‖z‖

The spatial-compression constant for length m bounds every ordered subproduct, including the empty selection.

theorem TrilinearHT.Auto.columnComplementProduct_rows_bound {V : Type u_1} {ι : Type u_2} {F : Type u_3} [Fintype V] [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (θ : ℕ → Bool) (m : ℕ) (z : ↥(ColumnL2 V)) (B : ColumnRowFamily D ι F) (hB : B.bound ≤ 1) : (finiteRowNorm fun (i : ι) => (B.row i) ((operatorComplementProduct (fun (l : ℕ) => cellColumnProjection D (A l) ⋯) θ m) z)) ≤ 2 ^ m * (columnCompressionBound D m * ‖z‖)

The explicit factor 2^m in the source's complement expansion, applied to the actual inherited column products.

theorem TrilinearHT.Auto.columnSpatialCompression_complements {V : Type u_1} {ι : Type u_2} {F : Type u_3} [Fintype V] [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (D : ColumnTreeData V) (A : ℕ → InheritedColumnMask D) (θ : ℕ → Bool) (m : ℕ) (z : ↥(ColumnL2 V)) (B : ColumnRowFamily D ι F) (hB : B.bound ≤ 1) : (finiteRowNorm fun (i : ι) => (B.row i) ((operatorComplementProduct (fun (l : ℕ) => cellColumnProjection D (A l) ⋯) θ m) z)) ≤ (1024 * (↑m + 1) ^ 1024 * Real.log (2 * D.budget)) ^ (1024 * (m + 1)) * ‖z‖

Blueprint lem:compression, lines 548–550 and 597: any factors may be replaced by complements, with the same type of depth-independent bound. The universal constant 1024 absorbs the exact binary expansion cost.