Section 11.2, part 2a: adaptive fits and staggered increments

This file was automatically generated by Claude.

Formalization of blueprint Section 11, "The base reduction" (sec:base), subsection 2, "Adaptive fits and the two earliest increments", part 2a: adaptive fits and staggered increments (lines 1569-1597) of blueprint/formalization_blueprint.tex.

Energy gain of one fresh column

theorem TrilinearHT.Auto.starProjection_sup_span_gain {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (U : Submodule ℂ E) [FiniteDimensional ℂ ↥U] (u z : E) : ‖(U ⊔ ℂ ∙ u).starProjection z‖ ^ 2 ≥ ‖U.starProjection z‖ ^ 2 + ‖inner ℂ u (z - U.starProjection z)‖ ^ 2 / ‖u‖ ^ 2

Adding a vector u to a closed range U increases the projection energy of z by at least |⟨u, z - P_U z⟩|² / ‖u‖² (blueprint §11.2, line 1577: "squared energy gain").

Fit columns with private weight one

noncomputable def TrilinearHT.Auto.fitColumnValue {V : Type u_1} [DecidableEq V] (φ : ℝ → ℂ) (v : V) (y : ℝ) : ColumnHilbert V

The value (φ(y), e_v) of a fit column.

Equations

• TrilinearHT.Auto.fitColumnValue φ v y = φ y • EuclideanSpace.single none 1 + EuclideanSpace.single (some v) 1

theorem TrilinearHT.Auto.fitColumnValue_none {V : Type u_1} [DecidableEq V] (φ : ℝ → ℂ) (v : V) (y : ℝ) : (fitColumnValue φ v y).ofLp none = φ y

theorem TrilinearHT.Auto.fitColumnValue_some {V : Type u_1} [DecidableEq V] (φ : ℝ → ℂ) (v w : V) (y : ℝ) : (fitColumnValue φ v y).ofLp (some w) = if w = v then 1 else 0

theorem TrilinearHT.Auto.norm_fitColumnValue_le {V : Type u_1} [Fintype V] [DecidableEq V] {φ : ℝ → ℂ} (hφ : ∀ (y : ℝ), ‖φ y‖ ≤ 1) (v : V) (y : ℝ) : ‖fitColumnValue φ v y‖ ≤ 2

theorem TrilinearHT.Auto.measurable_fitColumnValue {V : Type u_1} [Finite V] [DecidableEq V] {φ : ℝ → ℂ} (hφ : Measurable φ) (v : V) : Measurable (fitColumnValue φ v)

def TrilinearHT.Auto.FitAdmissible (s : Set ℝ) (φ : ℝ → ℂ) : Prop

The predicate on fit data: a measurable set of finite measure and a bounded measurable atom.

Equations

• TrilinearHT.Auto.FitAdmissible s φ = (MeasurableSet s ∧ MeasureTheory.volume s < ⊤ ∧ Measurable φ ∧ ∀ (y : ℝ), ‖φ y‖ ≤ 1)

theorem TrilinearHT.Auto.fitColumn_memLp {V : Type u_1} [Fintype V] [DecidableEq V] {s : Set ℝ} {φ : ℝ → ℂ} (h : FitAdmissible s φ) (v : V) : MeasureTheory.MemLp (s.indicator (fitColumnValue φ v)) 2 MeasureTheory.volume

noncomputable def TrilinearHT.Auto.fitColumn {V : Type u_1} [Fintype V] [DecidableEq V] (s : Set ℝ) (φ : ℝ → ℂ) (v : V) : ↥(ColumnL2 V)

The fit column 1_s (φ, e_v) in L²(ℝ; ℂ ⊕ ℓ²(V)).

Equations

• TrilinearHT.Auto.fitColumn s φ v = if h : TrilinearHT.Auto.FitAdmissible s φ then MeasureTheory.MemLp.toLp (s.indicator (TrilinearHT.Auto.fitColumnValue φ v)) ⋯ else 0

theorem TrilinearHT.Auto.fitColumn_coeFn {V : Type u_1} [Fintype V] [DecidableEq V] {s : Set ℝ} {φ : ℝ → ℂ} (h : FitAdmissible s φ) (v : V) : ↑↑(fitColumn s φ v) =ᵐ[MeasureTheory.volume] s.indicator (fitColumnValue φ v)

noncomputable def TrilinearHT.Auto.fitRange {M : ℕ} (s : Set ℝ) (a : ℕ → ℝ → ℂ) (n : ℕ) : Submodule ℂ ↥(ColumnL2 (Fin M))

The range of the first n fit columns 1_s (a_i, e_i), i < n, over labels Fin M.

Equations

• TrilinearHT.Auto.fitRange s a n = Submodule.span ℂ {x : ↥(TrilinearHT.Auto.ColumnL2 (Fin M)) | ∃ (i : Fin M), ↑i < n ∧ TrilinearHT.Auto.fitColumn s (a ↑i) i = x}

instance TrilinearHT.Auto.fitRange_finiteDimensional {M : ℕ} (s : Set ℝ) (a : ℕ → ℝ → ℂ) (n : ℕ) : FiniteDimensional ℂ ↥(fitRange s a n)

theorem TrilinearHT.Auto.fitRange_succ {M : ℕ} (s : Set ℝ) (a : ℕ → ℝ → ℂ) {n : ℕ} (hn : n < M) : fitRange s a (n + 1) = fitRange s a n ⊔ ℂ ∙ fitColumn s (a n) ⟨n, hn⟩

theorem TrilinearHT.Auto.fitRange_fresh_zero {M : ℕ} {s : Set ℝ} {a : ℕ → ℝ → ℂ} {n : ℕ} {m : Fin M} (hm : n ≤ ↑m) {x : ↥(ColumnL2 (Fin M))} (hx : x ∈ fitRange s a n) : ∀ᵐ (y : ℝ), (↑↑x y).ofLp (some m) = 0

Fresh coordinates vanish on the range of the earlier columns.

theorem TrilinearHT.Auto.inner_fitColumn {M : ℕ} {s : Set ℝ} {φ : ℝ → ℂ} (h : FitAdmissible s φ) (m : Fin M) (r : ↥(ColumnL2 (Fin M))) (hr : ∀ᵐ (y : ℝ), (↑↑r y).ofLp (some m) = 0) : inner ℂ (fitColumn s φ m) r = ∫ (y : ℝ) in s, (starRingEnd ℂ) (φ y) * (↑↑r y).ofLp none

The inner product of a fit column with a residual whose fresh coordinate vanishes.

theorem TrilinearHT.Auto.norm_fitColumn_sq_le {M : ℕ} {s : Set ℝ} {φ : ℝ → ℂ} (h : FitAdmissible s φ) (m : Fin M) : ‖fitColumn s φ m‖ ^ 2 ≤ 4 * MeasureTheory.volume.real s

Residual smallness and detection

def TrilinearHT.Auto.FormSmall (a₀ r : ℝ) (w : ℝ × ℝ → ℂ) (j : Fin 4) (q : ℝ) (R : ℝ → ℂ) (η : ℝ) : Prop

d_{j,I}(R) ≤ η (blueprint §11.2, line 1568): every local form at the cell [a₀, a₀ + r) with R in slot j, one normalized L^q input and two normalized L² inputs in the other slots (any choice of the L^q position) is at most η.

Equations

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

noncomputable def TrilinearHT.Auto.fitBudget (Cq : ℝ) (C k : ℕ) : ℝ

The detection budget at accuracy e^{-k} for residuals of normalized size at most two.

Equations

• TrilinearHT.Auto.fitBudget Cq C k = Real.exp (Cq * (1 + Real.log 2 + ↑k) ^ C)

theorem TrilinearHT.Auto.one_le_fitBudget {Cq : ℝ} (hCq : 0 < Cq) (C k : ℕ) : 1 ≤ fitBudget Cq C k

theorem TrilinearHT.Auto.fit_detect (κ : LocalKernelClass) : ∃ (c₂ : ℕ) (C : ℕ), 1 ≤ c₂ ∧ 1 ≤ C ∧ ∀ (q : ℝ), 2 < q → ∃ (Cq : ℝ), 0 < Cq ∧ ∀ {a₀ r : ℝ}, 0 < r → ∀ {w : ℝ × ℝ → ℂ}, IsAdmissibleLocalKernel κ a₀ r w → ∀ {j : Fin 4} {R : ℝ → ℂ}, Measurable R → MeasureTheory.eLpNorm R 2 (normalizedIntervalMeasure a₀ r) ≤ ENNReal.ofReal 2 → ∀ {k : ℕ}, 1 ≤ k → ¬FormSmall a₀ r w j q R (Real.exp (-↑k)) → ∃ (d : ℕ) (Φ : QuadraticChartData d), QuadraticChartComplexity c₂ (fitBudget Cq C k) Φ ∧ IsBoundedQuadraticChart Φ ∧ (fitBudget Cq C k)⁻¹ ≤ r⁻¹ * ‖∫ (x : ℝ) in a₀..a₀ + r, R x * (starRingEnd ℂ) (quadraticChartAtom Φ x)‖

Blueprint §11.2, line 1577 (detection step of the adaptive fit): a residual failing d_{j,I} ≤ e^{-k} correlates with a bounded atom of complexity at most fitBudget by at least fitBudget⁻¹ (Lemma lem:detection with C₁ = 2, δ = e^{-k}).

The greedy insertion at one cell

noncomputable def TrilinearHT.Auto.fitStep (M : ℕ) (P : (ℕ → ℝ → ℂ) → ℕ → Prop) (O : (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ) (st : (ℕ → ℝ → ℂ) × ℕ) : (ℕ → ℝ → ℂ) × ℕ

One insertion step: while the residual is not small and the cap M is not reached, insert the oracle's atom as the next label (blueprint §11.2, line 1577).

Equations

• TrilinearHT.Auto.fitStep M P O st = if st.2 < M ∧ ¬P st.1 st.2 then (Function.update st.1 st.2 (O st.1 st.2), st.2 + 1) else st

noncomputable def TrilinearHT.Auto.fitGreedy (M : ℕ) (P : (ℕ → ℝ → ℂ) → ℕ → Prop) (O : (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ) (st : (ℕ → ℝ → ℂ) × ℕ) : (ℕ → ℝ → ℂ) × ℕ

The greedy fit at one cell: M insertion steps.

Equations

• TrilinearHT.Auto.fitGreedy M P O st = (TrilinearHT.Auto.fitStep M P O)^[M] st

theorem TrilinearHT.Auto.fitStep_count {M : ℕ} {P : (ℕ → ℝ → ℂ) → ℕ → Prop} {O : (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ} (st : (ℕ → ℝ → ℂ) × ℕ) : fitStep M P O st = st ∨ st.2 < M ∧ ¬P st.1 st.2 ∧ fitStep M P O st = (Function.update st.1 st.2 (O st.1 st.2), st.2 + 1)

theorem TrilinearHT.Auto.fitStep_iterate_dichotomy {M : ℕ} {P : (ℕ → ℝ → ℂ) → ℕ → Prop} {O : (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ} (st : (ℕ → ℝ → ℂ) × ℕ) (t : ℕ) : fitStep M P O ((fitStep M P O)^[t] st) = (fitStep M P O)^[t] st ∨ ((fitStep M P O)^[t] st).2 = st.2 + t

Either the iterate is a fixed point or every step inserted.

theorem TrilinearHT.Auto.fitStep_count_le {M : ℕ} {P : (ℕ → ℝ → ℂ) → ℕ → Prop} {O : (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ} (st : (ℕ → ℝ → ℂ) × ℕ) (hst : st.2 ≤ M) (t : ℕ) : st.2 ≤ ((fitStep M P O)^[t] st).2 ∧ ((fitStep M P O)^[t] st).2 ≤ M

theorem TrilinearHT.Auto.fitGreedy_final {M : ℕ} {P : (ℕ → ℝ → ℂ) → ℕ → Prop} {O : (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ} (st : (ℕ → ℝ → ℂ) × ℕ) (hst : st.2 ≤ M) : P (fitGreedy M P O st).1 (fitGreedy M P O st).2 ∨ (fitGreedy M P O st).2 = M

The greedy fit ends with a small residual or at the cap.

theorem TrilinearHT.Auto.fitGreedy_prefix {M : ℕ} {P : (ℕ → ℝ → ℂ) → ℕ → Prop} {O : (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ} (st : (ℕ → ℝ → ℂ) × ℕ) (hst : st.2 ≤ M) {i : ℕ} (hi : i < st.2) : (fitGreedy M P O st).1 i = st.1 i

The greedy fit only appends: earlier atoms are unchanged.

theorem TrilinearHT.Auto.fitGreedy_count {M : ℕ} {P : (ℕ → ℝ → ℂ) → ℕ → Prop} {O : (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ} (st : (ℕ → ℝ → ℂ) × ℕ) (hst : st.2 ≤ M) : st.2 ≤ (fitGreedy M P O st).2 ∧ (fitGreedy M P O st).2 ≤ M

theorem TrilinearHT.Auto.fitGreedy_energy {M : ℕ} {P : (ℕ → ℝ → ℂ) → ℕ → Prop} {O : (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ} (E : (ℕ → ℝ → ℂ) → ℕ → ℝ) {g : ℝ} (hE : ∀ (a : ℕ → ℝ → ℂ), ∀ n < M, ¬P a n → E a n + g ≤ E (Function.update a n (O a n)) (n + 1)) (st : (ℕ → ℝ → ℂ) × ℕ) : E st.1 st.2 + g * (↑(fitGreedy M P O st).2 - ↑st.2) ≤ E (fitGreedy M P O st).1 (fitGreedy M P O st).2

Energy accumulates at least g per insertion along the greedy fit.

noncomputable def TrilinearHT.Auto.fitProj (M : ℕ) (s : Set ℝ) (a : ℕ → ℝ → ℂ) (n : ℕ) : ↥(ColumnL2 (Fin M)) →L[ℂ] ↥(ColumnL2 (Fin M))

The fit projection at a cell with the first n atoms.

Equations

• TrilinearHT.Auto.fitProj M s a n = (TrilinearHT.Auto.fitRange s a n).starProjection

noncomputable def TrilinearHT.Auto.fitResid (M : ℕ) (s : Set ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (a : ℕ → ℝ → ℂ) (n : ℕ) (y : ℝ) : ℂ

The fit residual f - (P F)_phys.

Equations

• TrilinearHT.Auto.fitResid M s f a n y = ↑↑f y - (↑↑((TrilinearHT.Auto.fitProj M s a n) (TrilinearHT.Auto.physicalColumnInput f)) y).ofLp none

theorem TrilinearHT.Auto.fitRange_update {M : ℕ} (s : Set ℝ) (a : ℕ → ℝ → ℂ) (n : ℕ) (φ : ℝ → ℂ) {n' : ℕ} (hn' : n' ≤ n) : fitRange s (Function.update a n φ) n' = fitRange s a n'

theorem TrilinearHT.Auto.starProjection_congr {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {K L : Submodule ℂ E} [K.HasOrthogonalProjection] [L.HasOrthogonalProjection] (h : K = L) (z : E) : K.starProjection z = L.starProjection z

theorem TrilinearHT.Auto.fitEnergy_gain {M : ℕ} {s : Set ℝ} (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (a : ℕ → ℝ → ℂ) {n : ℕ} (hn : n < M) {φ : ℝ → ℂ} (hφ : FitAdmissible s φ) {ρ : ℝ} (hρ : 0 ≤ ρ) (hcorr : ρ * MeasureTheory.volume.real s ≤ ‖∫ (y : ℝ) in s, (starRingEnd ℂ) (φ y) * fitResid M s f a n y‖) : ‖(fitProj M s a n) (physicalColumnInput f)‖ ^ 2 + ρ ^ 2 * MeasureTheory.volume.real s / 4 ≤ ‖(fitProj M s (Function.update a n φ) (n + 1)) (physicalColumnInput f)‖ ^ 2

Blueprint §11.2, line 1577: inserting an atom whose correlation with the residual is at least ρ |I| increases the fit energy by at least ρ² |I| / 4.

theorem TrilinearHT.Auto.starProjection_energy_le_of_le_sup {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {K U₁ U₂ : Submodule ℂ E} [FiniteDimensional ℂ ↥K] [FiniteDimensional ℂ ↥U₁] [FiniteDimensional ℂ ↥U₂] (hK : K ≤ U₁ ⊔ U₂) (h12 : U₁ ⟂ U₂) (z : E) : ‖K.starProjection z‖ ^ 2 ≤ ‖U₁.starProjection z‖ ^ 2 + ‖U₂.starProjection z‖ ^ 2

A range inside the orthogonal sum of two ranges has at most their total projection energy.

theorem TrilinearHT.Auto.fitColumn_union {M : ℕ} {s₁ s₂ : Set ℝ} (hs₁ : MeasurableSet s₁) (hs₁v : MeasureTheory.volume s₁ < ⊤) (hs₂ : MeasurableSet s₂) (hs₂v : MeasureTheory.volume s₂ < ⊤) (hd : Disjoint s₁ s₂) (φ : ℝ → ℂ) (m : Fin M) : fitColumn (s₁ ∪ s₂) φ m = fitColumn s₁ φ m + fitColumn s₂ φ m

The fit column on a disjoint union is the sum of the fit columns on the parts.

theorem TrilinearHT.Auto.fitRange_le_sup_union {M : ℕ} {s₁ s₂ : Set ℝ} (hs₁ : MeasurableSet s₁) (hs₁v : MeasureTheory.volume s₁ < ⊤) (hs₂ : MeasurableSet s₂) (hs₂v : MeasureTheory.volume s₂ < ⊤) (hd : Disjoint s₁ s₂) (a : ℕ → ℝ → ℂ) (n : ℕ) : fitRange (s₁ ∪ s₂) a n ≤ fitRange s₁ a n ⊔ fitRange s₂ a n

theorem TrilinearHT.Auto.fitRange_isOrtho {M : ℕ} {s₁ s₂ : Set ℝ} (hd : Disjoint s₁ s₂) (a b : ℕ → ℝ → ℂ) (n n' : ℕ) : fitRange s₁ a n ⟂ fitRange s₂ b n'

Fit ranges on disjoint sets are orthogonal.

theorem TrilinearHT.Auto.fitEnergy_split {M : ℕ} {s₁ s₂ : Set ℝ} (hs₁ : MeasurableSet s₁) (hs₁v : MeasureTheory.volume s₁ < ⊤) (hs₂ : MeasurableSet s₂) (hs₂v : MeasureTheory.volume s₂ < ⊤) (hd : Disjoint s₁ s₂) (a : ℕ → ℝ → ℂ) (n : ℕ) (z : ↥(ColumnL2 (Fin M))) : ‖(fitProj M (s₁ ∪ s₂) a n) z‖ ^ 2 ≤ ‖(fitProj M s₁ a n) z‖ ^ 2 + ‖(fitProj M s₂ a n) z‖ ^ 2

The fit energy on a cell is at most the sum of the fit energies on its two halves with the same atoms (refinement of the partition; nested subspaces).

theorem TrilinearHT.Auto.fitRange_ae_zero_off {M : ℕ} {s : Set ℝ} {a : ℕ → ℝ → ℂ} {n : ℕ} {x : ↥(ColumnL2 (Fin M))} (hx : x ∈ fitRange s a n) : ∀ᵐ (y : ℝ), y ∉ s → ↑↑x y = 0

theorem TrilinearHT.Auto.fitProj_restrict {M : ℕ} {s : Set ℝ} (hs : MeasurableSet s) (a : ℕ → ℝ → ℂ) (n : ℕ) (z : ↥(ColumnL2 (Fin M))) : (fitProj M s a n) ((columnL2Restriction s hs) z) = (fitProj M s a n) z

The fit projection only sees the input on its cell.

theorem TrilinearHT.Auto.fitEnergy_le {M : ℕ} {s : Set ℝ} (hs : MeasurableSet s) (a : ℕ → ℝ → ℂ) (n : ℕ) (z : ↥(ColumnL2 (Fin M))) : ‖(fitProj M s a n) z‖ ^ 2 ≤ ∫ (y : ℝ) in s, ‖↑↑z y‖ ^ 2

Contraction of the fit projection on its cell: ‖P z‖² ≤ ∫_s ‖z‖².

One attempt of the adaptive fit on a dyadic tree

noncomputable def TrilinearHT.Auto.dyadicParent (G : RealDyadicGrid) (c : ℤ × ℤ) : ℤ × ℤ

The parent cell.

Equations

• TrilinearHT.Auto.dyadicParent G c = (c.1 - 1, TrilinearHT.Auto.dyadicIndex G (c.1 - 1) (TrilinearHT.Auto.dyadicGridLeft G c.1 c.2))

theorem TrilinearHT.Auto.dyadicParent_of_mem_children (G : RealDyadicGrid) {p c : ℤ × ℤ} (hc : c ∈ dyadicChildren G p) : dyadicParent G c = p

noncomputable def TrilinearHT.Auto.fitState (G : RealDyadicGrid) (M : ℕ) (P : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → Prop) (O : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ) : ℕ → ℤ × ℤ → (ℕ → ℝ → ℂ) × ℕ

The states of one attempt: atoms and count at each cell of depth root + d.

Equations

• TrilinearHT.Auto.fitState G M P O 0 x✝ = TrilinearHT.Auto.fitGreedy M (P x✝) (O x✝) (fun (x : ℕ) => 0, 0)
• TrilinearHT.Auto.fitState G M P O d.succ x✝ = TrilinearHT.Auto.fitGreedy M (P x✝) (O x✝) (TrilinearHT.Auto.fitState G M P O d (TrilinearHT.Auto.dyadicParent G x✝))

theorem TrilinearHT.Auto.fitState_count_le (G : RealDyadicGrid) (M : ℕ) (P : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → Prop) (O : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ) (d : ℕ) (c : ℤ × ℤ) : (fitState G M P O d c).2 ≤ M

noncomputable def TrilinearHT.Auto.fitInherited (G : RealDyadicGrid) (M : ℕ) (P : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → Prop) (O : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ) : ℕ → ℤ × ℤ → (ℕ → ℝ → ℂ) × ℕ

The inherited count of a cell: the parent's final count (zero at the root).

Equations

• TrilinearHT.Auto.fitInherited G M P O 0 x✝ = (fun (x : ℕ) => 0, 0)
• TrilinearHT.Auto.fitInherited G M P O d.succ x✝ = TrilinearHT.Auto.fitState G M P O d (TrilinearHT.Auto.dyadicParent G x✝)

theorem TrilinearHT.Auto.fitState_eq_greedy (G : RealDyadicGrid) (M : ℕ) (P : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → Prop) (O : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ) (d : ℕ) (c : ℤ × ℤ) : fitState G M P O d c = fitGreedy M (P c) (O c) (fitInherited G M P O d c)

theorem TrilinearHT.Auto.fitInherited_count_le (G : RealDyadicGrid) (M : ℕ) (P : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → Prop) (O : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ) (d : ℕ) (c : ℤ × ℤ) : (fitInherited G M P O d c).2 ≤ M

noncomputable def TrilinearHT.Auto.fitNew (G : RealDyadicGrid) (M : ℕ) (P : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → Prop) (O : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ) (d : ℕ) (c : ℤ × ℤ) : ℕ

The number of atoms inserted at a cell.

Equations

• TrilinearHT.Auto.fitNew G M P O d c = (TrilinearHT.Auto.fitState G M P O d c).2 - (TrilinearHT.Auto.fitInherited G M P O d c).2

theorem TrilinearHT.Auto.fitNew_add (G : RealDyadicGrid) (M : ℕ) (P : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → Prop) (O : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ) (d : ℕ) (c : ℤ × ℤ) : (fitState G M P O d c).2 = (fitInherited G M P O d c).2 + fitNew G M P O d c

theorem TrilinearHT.Auto.fitNew_eq_zero_of_P (G : RealDyadicGrid) (M : ℕ) (P : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → Prop) (O : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ) (d : ℕ) (c : ℤ × ℤ) (hP : ∀ (a : ℕ → ℝ → ℂ) (n : ℕ), P c a n) : fitNew G M P O d c = 0

A cell whose stopping predicate holds for every state inserts nothing.

def TrilinearHT.Auto.FitOracle (G : RealDyadicGrid) (M : ℕ) (P : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → Prop) (O : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (ρ : ℝ) : Prop

The oracle hypothesis: whenever the residual at a cell is not small and the cap is not reached, the oracle's atom is admissible and correlates with the residual by ρ |I|.

Equations

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

noncomputable def TrilinearHT.Auto.fitCellEnergy (G : RealDyadicGrid) (M : ℕ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (c : ℤ × ℤ) (st : (ℕ → ℝ → ℂ) × ℕ) : ℝ

The fit energy at a cell for a state.

Equations

• TrilinearHT.Auto.fitCellEnergy G M f c st = ‖(TrilinearHT.Auto.fitProj M (TrilinearHT.Auto.dyadicGridCell G c.1 c.2) st.1 st.2) (TrilinearHT.Auto.physicalColumnInput f)‖ ^ 2

theorem TrilinearHT.Auto.fitCellEnergy_gain (G : RealDyadicGrid) (M : ℕ) (P : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → Prop) (O : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) {ρ : ℝ} (hρ : 0 ≤ ρ) (horacle : FitOracle G M P O f ρ) (d : ℕ) (c : ℤ × ℤ) : fitCellEnergy G M f c (fitInherited G M P O d c) + ρ ^ 2 * dyadicGridLength G c.1 / 4 * ↑(fitNew G M P O d c) ≤ fitCellEnergy G M f c (fitState G M P O d c)

theorem TrilinearHT.Auto.fitCellEnergy_children (G : RealDyadicGrid) (M : ℕ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (p : ℤ × ℤ) (st : (ℕ → ℝ → ℂ) × ℕ) : fitCellEnergy G M f p st ≤ ∑ c ∈ dyadicChildren G p, fitCellEnergy G M f c st

The two children of a cell carry at least the parent's fit energy with the same atoms.

theorem TrilinearHT.Auto.dyadicGeneration_children_disjoint (G : RealDyadicGrid) (R : ℤ × ℤ) (k : ℕ) : (↑(dyadicGeneration G R k)).PairwiseDisjoint (dyadicChildren G)

theorem TrilinearHT.Auto.fitEnergy_telescope (G : RealDyadicGrid) (M : ℕ) (P : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → Prop) (O : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) {ρ : ℝ} (hρ : 0 ≤ ρ) (horacle : FitOracle G M P O f ρ) (R : ℤ × ℤ) (d : ℕ) : ∑ k ∈ Finset.range (d + 1), ∑ c ∈ dyadicGeneration G R k, ρ ^ 2 * dyadicGridLength G c.1 / 4 * ↑(fitNew G M P O k c) ≤ ∑ c ∈ dyadicGeneration G R d, fitCellEnergy G M f c (fitState G M P O d c)

Blueprint §11.2, line 1577 ("fits and refinements form nested subspaces"): the energy gains of all insertions down to generation d are at most the fit energy of that generation.

theorem TrilinearHT.Auto.fitEnergy_generation_le (G : RealDyadicGrid) (M : ℕ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (R : ℤ × ℤ) (d : ℕ) (st : ℤ × ℤ → (ℕ → ℝ → ℂ) × ℕ) : ∑ c ∈ dyadicGeneration G R d, fitCellEnergy G M f c (st c) ≤ ∫ (y : ℝ) in dyadicGridCell G R.1 R.2, ‖↑↑f y‖ ^ 2

The fit energy of a generation is at most the input energy on the root.

Coefficients of the fit projection

theorem TrilinearHT.Auto.columnHilbert_sum_apply {V : Type u_1} {ι : Type u_2} (s : Finset ι) (x : ι → ColumnHilbert V) (o : Option V) : (∑ i ∈ s, x i).ofLp o = ∑ i ∈ s, (x i).ofLp o

def TrilinearHT.Auto.fitLabels (M n : ℕ) : Finset (Fin M)

The labels of the first n fit columns.

Equations

• TrilinearHT.Auto.fitLabels M n = {i : Fin M | ↑i < n}

theorem TrilinearHT.Auto.fitRange_exists_coeff {M : ℕ} {s : Set ℝ} {a : ℕ → ℝ → ℂ} {n : ℕ} {x : ↥(ColumnL2 (Fin M))} (hx : x ∈ fitRange s a n) : ∃ (c : Fin M → ℂ), x = ∑ i ∈ fitLabels M n, c i • fitColumn s (a ↑i) i

noncomputable def TrilinearHT.Auto.fitCoeff (M : ℕ) (s : Set ℝ) (a : ℕ → ℝ → ℂ) (n : ℕ) (z : ↥(ColumnL2 (Fin M))) : Fin M → ℂ

Coefficients of the fit projection in the fit columns.

Equations

• TrilinearHT.Auto.fitCoeff M s a n z = Classical.choose ⋯

theorem TrilinearHT.Auto.fitCoeff_spec (M : ℕ) (s : Set ℝ) (a : ℕ → ℝ → ℂ) (n : ℕ) (z : ↥(ColumnL2 (Fin M))) : (fitProj M s a n) z = ∑ i ∈ fitLabels M n, fitCoeff M s a n z i • fitColumn s (a ↑i) i

noncomputable def TrilinearHT.Auto.fitPhys (M : ℕ) (s : Set ℝ) (a : ℕ → ℝ → ℂ) (n : ℕ) (z : ↥(ColumnL2 (Fin M))) (y : ℝ) : ℂ

The pointwise physical part of the fit projection: ∑ c_i a_i over admissible atoms.

Equations

• TrilinearHT.Auto.fitPhys M s a n z y = ∑ i ∈ TrilinearHT.Auto.fitLabels M n, if TrilinearHT.Auto.FitAdmissible s (a ↑i) then TrilinearHT.Auto.fitCoeff M s a n z i * a (↑i) y else 0

theorem TrilinearHT.Auto.fitProj_coeFn (M : ℕ) {s : Set ℝ} (a : ℕ → ℝ → ℂ) (n : ℕ) (z : ↥(ColumnL2 (Fin M))) : ∀ᵐ (y : ℝ), y ∈ s → ↑↑((fitProj M s a n) z) y = ∑ i ∈ fitLabels M n, if FitAdmissible s (a ↑i) then fitCoeff M s a n z i • fitColumnValue (a ↑i) i y else 0

theorem TrilinearHT.Auto.fitProj_none (M : ℕ) {s : Set ℝ} (a : ℕ → ℝ → ℂ) (n : ℕ) (z : ↥(ColumnL2 (Fin M))) : ∀ᵐ (y : ℝ), y ∈ s → (↑↑((fitProj M s a n) z) y).ofLp none = fitPhys M s a n z y

The physical coordinate of the fit projection is fitPhys almost everywhere on the cell.

theorem TrilinearHT.Auto.fitProj_some (M : ℕ) {s : Set ℝ} (a : ℕ → ℝ → ℂ) (n : ℕ) (z : ↥(ColumnL2 (Fin M))) (m : Fin M) : ∀ᵐ (y : ℝ), y ∈ s → (↑↑((fitProj M s a n) z) y).ofLp (some m) = if m ∈ fitLabels M n ∧ FitAdmissible s (a ↑m) then fitCoeff M s a n z m else 0

The private coordinates of the fit projection are the coefficients.

noncomputable def TrilinearHT.Auto.fitCoeffSq (M : ℕ) (s : Set ℝ) (a : ℕ → ℝ → ℂ) (n : ℕ) (z : ↥(ColumnL2 (Fin M))) : ℝ

The squared coefficient norm over admissible atoms.

Equations

• TrilinearHT.Auto.fitCoeffSq M s a n z = ∑ i ∈ TrilinearHT.Auto.fitLabels M n, if TrilinearHT.Auto.FitAdmissible s (a ↑i) then ‖TrilinearHT.Auto.fitCoeff M s a n z i‖ ^ 2 else 0

theorem TrilinearHT.Auto.fitCoeffSq_nonneg (M : ℕ) (s : Set ℝ) (a : ℕ → ℝ → ℂ) (n : ℕ) (z : ↥(ColumnL2 (Fin M))) : 0 ≤ fitCoeffSq M s a n z

theorem TrilinearHT.Auto.fitCoeffSq_le (M : ℕ) {s : Set ℝ} (hs : MeasurableSet s) (hsv : MeasureTheory.volume s < ⊤) (a : ℕ → ℝ → ℂ) (n : ℕ) (z : ↥(ColumnL2 (Fin M))) : MeasureTheory.volume.real s * fitCoeffSq M s a n z ≤ ∫ (y : ℝ) in s, ‖↑↑((fitProj M s a n) z) y‖ ^ 2

Private weights one bound the coefficient ℓ² norm: |s| ∑ |c_i|² ≤ ∫_s ‖P z‖².

theorem TrilinearHT.Auto.norm_fitPhys_sq_le (M : ℕ) (s : Set ℝ) (a : ℕ → ℝ → ℂ) (n : ℕ) (z : ↥(ColumnL2 (Fin M))) (y : ℝ) : ‖fitPhys M s a n z y‖ ^ 2 ≤ ↑M * fitCoeffSq M s a n z

The pointwise bound |∑ c_i a_i|² ≤ M ∑ |c_i|² for atoms bounded by one.

theorem TrilinearHT.Auto.fitPhys_measurable (M : ℕ) (s : Set ℝ) (a : ℕ → ℝ → ℂ) (n : ℕ) (z : ↥(ColumnL2 (Fin M))) : Measurable (fitPhys M s a n z)

theorem TrilinearHT.Auto.setIntegral_fitPhys_sq_le (M : ℕ) {s : Set ℝ} (hs : MeasurableSet s) (hsv : MeasureTheory.volume s < ⊤) (a : ℕ → ℝ → ℂ) (n : ℕ) (z : ↥(ColumnL2 (Fin M))) : ∫ (y : ℝ) in s, ‖fitPhys M s a n z y‖ ^ 2 ≤ ∫ (y : ℝ) in s, ‖↑↑((fitProj M s a n) z) y‖ ^ 2

The physical fit is bounded in L²(s) by the fit energy.

The adaptive-fit oracle

theorem TrilinearHT.Auto.eLpNorm_normalized_le_of_integral {a r : ℝ} (hr : 0 < r) {g : ℝ → ℂ} (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (Set.Ico a (a + r)))) {C : ℝ} (hC : 0 ≤ C) (h : ∫ (y : ℝ) in Set.Ico a (a + r), ‖g y‖ ^ 2 ≤ C ^ 2 * r) : MeasureTheory.eLpNorm g 2 (normalizedIntervalMeasure a r) ≤ ENNReal.ofReal C

theorem TrilinearHT.Auto.intervalIntegral_eq_cell {a r : ℝ} (hr : 0 ≤ r) (h : ℝ → ℂ) : ∫ (x : ℝ) in a..a + r, h x = ∫ (x : ℝ) in Set.Ico a (a + r), h x

def TrilinearHT.Auto.FitChartGood (c₂ : ℕ) (B a₀ r : ℝ) (R : ℝ → ℂ) (p : (d : ℕ) × QuadraticChartData d) : Prop

A detection chart: complexity and boundedness at budget B, and correlation B⁻¹.

Equations

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

noncomputable def TrilinearHT.Auto.fitOracleAtom (c₂ : ℕ) (B a₀ r : ℝ) (R : ℝ → ℂ) : ℝ → ℂ

The oracle atom: a chosen detection chart, when one exists.

Equations

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

theorem TrilinearHT.Auto.fitOracleAtom_good {c₂ : ℕ} {B a₀ r : ℝ} {R : ℝ → ℂ} (h : ∃ (p : (d : ℕ) × QuadraticChartData d), FitChartGood c₂ B a₀ r R p) : ∃ (p : (d : ℕ) × QuadraticChartData d), FitChartGood c₂ B a₀ r R p ∧ fitOracleAtom c₂ B a₀ r R = quadraticChartAtom p.snd

def TrilinearHT.Auto.kernelHull (G : RealDyadicGrid) (J : ℤ × ℤ) (N : ℕ) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (c : ℤ × ℤ) : Prop

The kernel hull of a finite tree: cells containing a tree cell with a nonzero kernel (blueprint prop:normalized, line 2832: the normalization is only assumed on the rooted subtree of the used cells; the other cells carry the zero kernel).

Equations

• TrilinearHT.Auto.kernelHull G J N w c = ∃ c' ∈ TrilinearHT.Auto.dyadicFiniteTree G J N, TrilinearHT.Auto.dyadicGridCell G c'.1 c'.2 ⊆ TrilinearHT.Auto.dyadicGridCell G c.1 c.2 ∧ w c' ≠ 0

theorem TrilinearHT.Auto.kernelHull_of_ne {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {w : ℤ × ℤ → ℝ × ℝ → ℂ} {c : ℤ × ℤ} (hc : c ∈ dyadicFiniteTree G J N) (hw : w c ≠ 0) : kernelHull G J N w c

theorem TrilinearHT.Auto.kernelHull.mono {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {w : ℤ × ℤ → ℝ × ℝ → ℂ} {c d : ℤ × ℤ} (h : kernelHull G J N w c) (hcd : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2) : kernelHull G J N w d

theorem TrilinearHT.Auto.eq_zero_of_not_kernelHull {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {w : ℤ × ℤ → ℝ × ℝ → ℂ} {c : ℤ × ℤ} (hc : c ∈ dyadicFiniteTree G J N) (h : ¬kernelHull G J N w c) : w c = 0

theorem TrilinearHT.Auto.localProgressionForm_zero_kernel (r : ℝ) (F : Fin 4 → ℝ → ℂ) : localProgressionForm r 0 F = 0

theorem TrilinearHT.Auto.formSmall_zero_kernel {a₀ r : ℝ} {j : Fin 4} {q : ℝ} {R : ℝ → ℂ} {η : ℝ} (hη : 0 ≤ η) : FormSmall a₀ r 0 j q R η

Every residual is small for the zero kernel.

theorem TrilinearHT.Auto.kernelHull_of_not_formSmall {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {w : ℤ × ℤ → ℝ × ℝ → ℂ} {c : ℤ × ℤ} (hc : c ∈ dyadicFiniteTree G J N) {a₀ r : ℝ} {j : Fin 4} {q : ℝ} {R : ℝ → ℂ} {k : ℝ} (hns : ¬FormSmall a₀ r (w c) j q R (Real.exp (-k))) : kernelHull G J N w c

A failing residual test happens only at a cell of the kernel hull.

structure TrilinearHT.Auto.FitSetup : Type

The data of one adaptive-fit construction.

• G : RealDyadicGrid

  Dyadic grid used for the adaptive-fit construction.

• J : ℤ × ℤ

  Root cell on which the adaptive-fit input is normalized.

• N : ℕ

  Number of dyadic generations available below the root.

• M : ℕ

  Maximum number of fit columns available to an attempt.

• f : ℝ → ℂ

  Scalar input to be approximated by the adaptive fit.

• w : ℤ × ℤ → ℝ × ℝ → ℂ

  Local kernels assigned to the dyadic cells.

• j : Fin 4

  Position of the input in the four-linear local form.

• q : ℝ

  Integrability exponent used in the residual-smallness test.

• k : ℕ

  Accuracy parameter giving the residual threshold exp (-k).

• c₂ : ℕ

  Complexity exponent supplied to the fit oracle.

• B : ℝ

  Complexity budget supplied to the fit oracle.

@[reducible, inline]

noncomputable abbrev TrilinearHT.Auto.FitSetup.cell (S : FitSetup) (c : ℤ × ℤ) : Set ℝ

The cell of an index.

Equations

• S.cell c = TrilinearHT.Auto.dyadicGridCell S.G c.1 c.2

noncomputable def TrilinearHT.Auto.FitSetup.input (S : FitSetup) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

The input 1_J f as an L² class.

Equations

• S.input = if h : MeasureTheory.MemLp ((S.cell S.J).indicator S.f) 2 MeasureTheory.volume then MeasureTheory.MemLp.toLp ((S.cell S.J).indicator S.f) h else 0

noncomputable def TrilinearHT.Auto.FitSetup.Z (S : FitSetup) : ↥(ColumnL2 (Fin S.M))

The column input.

Equations

• S.Z = TrilinearHT.Auto.physicalColumnInput S.input

noncomputable def TrilinearHT.Auto.FitSetup.phys (S : FitSetup) (c : ℤ × ℤ) (a : ℕ → ℝ → ℂ) (n : ℕ) (y : ℝ) : ℂ

The pointwise physical fit at a cell.

Equations

• S.phys c a n y = TrilinearHT.Auto.fitPhys S.M (S.cell c) a n S.Z y

noncomputable def TrilinearHT.Auto.FitSetup.res (S : FitSetup) (c : ℤ × ℤ) (a : ℕ → ℝ → ℂ) (n : ℕ) (y : ℝ) : ℂ

The pointwise residual f - g_I.

Equations

• S.res c a n y = S.f y - S.phys c a n y

def TrilinearHT.Auto.FitSetup.P (S : FitSetup) (c : ℤ × ℤ) (a : ℕ → ℝ → ℂ) (n : ℕ) : Prop

The stopping predicate: the cell leaves the tree or the residual is small.

Equations

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

noncomputable def TrilinearHT.Auto.FitSetup.O (S : FitSetup) (c : ℤ × ℤ) (a : ℕ → ℝ → ℂ) (n : ℕ) : ℝ → ℂ

The oracle.

Equations

• S.O c a n = TrilinearHT.Auto.fitOracleAtom S.c₂ S.B (TrilinearHT.Auto.dyadicGridLeft S.G c.1 c.2) (TrilinearHT.Auto.dyadicGridLength S.G c.1) (S.res c a n)

structure TrilinearHT.Auto.FitSetup.Hyp (S : FitSetup) : Prop

Hypotheses on the data.

• f_meas : Measurable S.f
• f_norm_root : MeasureTheory.eLpNorm S.f 2 (normalizedIntervalMeasure (dyadicGridLeft S.G S.J.1 S.J.2) (dyadicGridLength S.G S.J.1)) ≤ 1
• f_norm (c : ℤ × ℤ) : c ∈ dyadicFiniteTree S.G S.J S.N → kernelHull S.G S.J S.N S.w c → MeasureTheory.eLpNorm S.f 2 (normalizedIntervalMeasure (dyadicGridLeft S.G c.1 c.2) (dyadicGridLength S.G c.1)) ≤ 1
• B_pos : 0 < S.B
• detect (c : ℤ × ℤ) (a : ℕ → ℝ → ℂ) (n : ℕ) : c ∈ dyadicFiniteTree S.G S.J S.N → Measurable (S.res c a n) → MeasureTheory.eLpNorm (S.res c a n) 2 (normalizedIntervalMeasure (dyadicGridLeft S.G c.1 c.2) (dyadicGridLength S.G c.1)) ≤ ENNReal.ofReal 2 → ¬FormSmall (dyadicGridLeft S.G c.1 c.2) (dyadicGridLength S.G c.1) (S.w c) S.j S.q (S.res c a n) (Real.exp (-↑S.k)) → ∃ (p : (d : ℕ) × QuadraticChartData d), FitChartGood S.c₂ S.B (dyadicGridLeft S.G c.1 c.2) (dyadicGridLength S.G c.1) (S.res c a n) p

theorem TrilinearHT.Auto.FitSetup.tree_cell_subset {S : FitSetup} {c : ℤ × ℤ} (hc : c ∈ dyadicFiniteTree S.G S.J S.N) : S.cell c ⊆ S.cell S.J

theorem TrilinearHT.Auto.FitSetup.Hyp.memLp {S : FitSetup} (h : S.Hyp) : MeasureTheory.MemLp ((S.cell S.J).indicator S.f) 2 MeasureTheory.volume

theorem TrilinearHT.Auto.FitSetup.Hyp.input_ae {S : FitSetup} (h : S.Hyp) : ↑↑S.input =ᵐ[MeasureTheory.volume] (S.cell S.J).indicator S.f

theorem TrilinearHT.Auto.FitSetup.Hyp.input_energy_le {S : FitSetup} (h : S.Hyp) {c : ℤ × ℤ} (hc : c ∈ dyadicFiniteTree S.G S.J S.N) (hT : kernelHull S.G S.J S.N S.w c) : ∫ (y : ℝ) in S.cell c, ‖↑↑S.input y‖ ^ 2 ≤ dyadicGridLength S.G c.1

The input energy on a cell inside the root is at most its length.

theorem TrilinearHT.Auto.FitSetup.phys_measurable {S : FitSetup} (c : ℤ × ℤ) (a : ℕ → ℝ → ℂ) (n : ℕ) : Measurable (S.phys c a n)

theorem TrilinearHT.Auto.FitSetup.Hyp.res_measurable {S : FitSetup} (h : S.Hyp) (c : ℤ × ℤ) (a : ℕ → ℝ → ℂ) (n : ℕ) : Measurable (S.res c a n)

theorem TrilinearHT.Auto.FitSetup.Hyp.fitProj_sq_le {S : FitSetup} (h : S.Hyp) {c : ℤ × ℤ} (hc : c ∈ dyadicFiniteTree S.G S.J S.N) (hT : kernelHull S.G S.J S.N S.w c) (a : ℕ → ℝ → ℂ) (n : ℕ) : ∫ (y : ℝ) in S.cell c, ‖↑↑((fitProj S.M (S.cell c) a n) S.Z) y‖ ^ 2 ≤ dyadicGridLength S.G c.1

The fit energy at a cell inside the root is at most its length.

theorem TrilinearHT.Auto.FitSetup.Hyp.phys_sq_le {S : FitSetup} (h : S.Hyp) {c : ℤ × ℤ} (hc : c ∈ dyadicFiniteTree S.G S.J S.N) (hT : kernelHull S.G S.J S.N S.w c) (a : ℕ → ℝ → ℂ) (n : ℕ) : ∫ (y : ℝ) in S.cell c, ‖S.phys c a n y‖ ^ 2 ≤ dyadicGridLength S.G c.1

theorem TrilinearHT.Auto.FitSetup.Hyp.coeffSq_le {S : FitSetup} (h : S.Hyp) {c : ℤ × ℤ} (hc : c ∈ dyadicFiniteTree S.G S.J S.N) (hT : kernelHull S.G S.J S.N S.w c) (a : ℕ → ℝ → ℂ) (n : ℕ) : fitCoeffSq S.M (S.cell c) a n S.Z ≤ 1

The coefficient ℓ² norm is at most one.

theorem TrilinearHT.Auto.FitSetup.Hyp.res_eLpNorm_le {S : FitSetup} (h : S.Hyp) {c : ℤ × ℤ} (hc : c ∈ dyadicFiniteTree S.G S.J S.N) (hT : kernelHull S.G S.J S.N S.w c) (a : ℕ → ℝ → ℂ) (n : ℕ) : MeasureTheory.eLpNorm (S.res c a n) 2 (normalizedIntervalMeasure (dyadicGridLeft S.G c.1 c.2) (dyadicGridLength S.G c.1)) ≤ ENNReal.ofReal 2

The residual has normalized L² norm at most two.

theorem TrilinearHT.Auto.FitSetup.Hyp.res_ae {S : FitSetup} (h : S.Hyp) {c : ℤ × ℤ} (hc : c ∈ dyadicFiniteTree S.G S.J S.N) (a : ℕ → ℝ → ℂ) (n : ℕ) : ∀ᵐ (y : ℝ), y ∈ S.cell c → S.res c a n y = fitResid S.M (S.cell c) S.input a n y

The residual equals the fit residual almost everywhere on a cell inside the root.

theorem TrilinearHT.Auto.FitSetup.Hyp.oracle {S : FitSetup} (h : S.Hyp) : FitOracle S.G S.M S.P S.O S.input S.B⁻¹

Blueprint §11.2, line 1577: the oracle inserts a bounded atom of residual correlation B⁻¹ on every failing cell.

Ancestor chains, inherited lists and counts

theorem TrilinearHT.Auto.dyadicGridCell_subset_of_common_point (G : RealDyadicGrid) {c d : ℤ × ℤ} {x : ℝ} (hxc : x ∈ dyadicGridCell G c.1 c.2) (hxd : x ∈ dyadicGridCell G d.1 d.2) (hdc : d.1 ≤ c.1) : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2

theorem TrilinearHT.Auto.dyadicGridCell_eq_of_common_point (G : RealDyadicGrid) {c d : ℤ × ℤ} {x : ℝ} (hxc : x ∈ dyadicGridCell G c.1 c.2) (hxd : x ∈ dyadicGridCell G d.1 d.2) (hdc : d.1 = c.1) : c = d

theorem TrilinearHT.Auto.dyadicParent_subset (G : RealDyadicGrid) (c : ℤ × ℤ) : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G (dyadicParent G c).1 (dyadicParent G c).2

theorem TrilinearHT.Auto.dyadicParent_subset_of_subset (G : RealDyadicGrid) {c d : ℤ × ℤ} (h : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2) (hne : c ≠ d) : dyadicGridCell G (dyadicParent G c).1 (dyadicParent G c).2 ⊆ dyadicGridCell G d.1 d.2

A strict ancestor contains the parent.

def TrilinearHT.Auto.FitPrefix (st st' : (ℕ → ℝ → ℂ) × ℕ) : Prop

st extends the list st'.

Equations

• TrilinearHT.Auto.FitPrefix st st' = (st'.2 ≤ st.2 ∧ ∀ i < st'.2, st.1 i = st'.1 i)

theorem TrilinearHT.Auto.FitPrefix.refl (st : (ℕ → ℝ → ℂ) × ℕ) : FitPrefix st st

theorem TrilinearHT.Auto.FitPrefix.trans {st st' st'' : (ℕ → ℝ → ℂ) × ℕ} (h : FitPrefix st st') (h' : FitPrefix st' st'') : FitPrefix st st''

theorem TrilinearHT.Auto.fitGreedy_fitPrefix {M : ℕ} {P : (ℕ → ℝ → ℂ) → ℕ → Prop} {O : (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ} (st : (ℕ → ℝ → ℂ) × ℕ) (hst : st.2 ≤ M) : FitPrefix (fitGreedy M P O st) st

theorem TrilinearHT.Auto.fitGreedy_inv {M : ℕ} {P : (ℕ → ℝ → ℂ) → ℕ → Prop} {O : (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ} (Good : (ℝ → ℂ) → Prop) (hO : ∀ (a : ℕ → ℝ → ℂ), ∀ n < M, ¬P a n → Good (O a n)) (st : (ℕ → ℝ → ℂ) × ℕ) (h : ∀ i < st.2, Good (st.1 i)) (i : ℕ) : i < (fitGreedy M P O st).2 → Good ((fitGreedy M P O st).1 i)

Every atom of the greedy fit satisfies a property preserved by the oracle.

theorem TrilinearHT.Auto.fitState_inv (G : RealDyadicGrid) (M : ℕ) (P : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → Prop) (O : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ) (Good : (ℝ → ℂ) → Prop) (hO : ∀ (c : ℤ × ℤ) (a : ℕ → ℝ → ℂ), ∀ n < M, ¬P c a n → Good (O c a n)) (d : ℕ) (c : ℤ × ℤ) (i : ℕ) : i < (fitState G M P O d c).2 → Good ((fitState G M P O d c).1 i)

theorem TrilinearHT.Auto.fitState_fitPrefix (G : RealDyadicGrid) (M : ℕ) (P : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → Prop) (O : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ) (d : ℕ) (c' : ℤ × ℤ) (e : ℕ) (c : ℤ × ℤ) : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G c'.1 c'.2 → c.1 = c'.1 + ↑e → FitPrefix (fitState G M P O (d + e) c) (fitState G M P O d c')

Along an ancestor chain, the deeper state extends the shallower one.

theorem TrilinearHT.Auto.fitState_count_eq_ancestorSum (G : RealDyadicGrid) (M : ℕ) (P : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → Prop) (O : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ) (K : ℤ × ℤ) (L d : ℕ) (c : ℤ × ℤ) : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G K.1 K.2 → c.1 = K.1 + ↑d → d ≤ L → ↑(fitState G M P O d c).2 = dyadicAncestorSum G (dyadicFiniteTree G K L) (fun (c' : ℤ × ℤ) => ↑(fitNew G M P O (c'.1 - K.1).toNat c')) c

The count at a cell is the ancestor sum of the insertion counts within its attempt.

theorem TrilinearHT.Auto.fitWeightedMass_le (G : RealDyadicGrid) (M : ℕ) (P : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → Prop) (O : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) {ρ : ℝ} (hρ : 0 ≤ ρ) (horacle : FitOracle G M P O f ρ) (K : ℤ × ℤ) (L : ℕ) : (ρ ^ 2 / 4 * dyadicWeightedMass G (dyadicFiniteTree G K L) fun (c' : ℤ × ℤ) => ↑(fitNew G M P O (c'.1 - K.1).toNat c')) ≤ ∫ (y : ℝ) in dyadicGridCell G K.1 K.2, ‖↑↑f y‖ ^ 2

The weighted insertion mass of an attempt is at most 4/ρ² times the input energy.

Greedy attempts with restarts on a finite tree

structure TrilinearHT.Auto.GreedyTree : Type

A greedy attempt structure: per-cell greedy insertion with predicate P and oracle O, inherited along each attempt (fitState), with integrated insertion mass at most A |K| on every attempt root K (blueprint sec:reduction, lines 429-451; §11.2, line 1577).

• G : RealDyadicGrid

  Dyadic grid supporting the greedy attempts and restarts.

• J : ℤ × ℤ

  Initial root cell for the greedy construction.

• N : ℕ

  Number of dyadic generations below the initial root.

• M : ℕ

  Maximum number of insertions available in one greedy state.

• P : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → Prop

  Predicate deciding when an insertion attempt stops.

• O : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ

  Oracle producing a new atom when the stopping predicate fails.

• A : ℝ

  Integrated insertion-mass bound per unit length of an attempt root.

@[reducible, inline]

noncomputable abbrev TrilinearHT.Auto.GreedyTree.cell (S : GreedyTree) (c : ℤ × ℤ) : Set ℝ

The cell of an index.

Equations

• S.cell c = TrilinearHT.Auto.dyadicGridCell S.G c.1 c.2

noncomputable def TrilinearHT.Auto.GreedyTree.state (S : GreedyTree) (d : ℕ) (c : ℤ × ℤ) : (ℕ → ℝ → ℂ) × ℕ

The state of the attempt d generations below its root.

Equations

• S.state d c = TrilinearHT.Auto.fitState S.G S.M S.P S.O d c

noncomputable def TrilinearHT.Auto.GreedyTree.newAt (S : GreedyTree) (K c : ℤ × ℤ) : ℝ

Insertion counts of the attempt rooted at K.

Equations

• S.newAt K c = ↑(TrilinearHT.Auto.fitNew S.G S.M S.P S.O (c.1 - K.1).toNat c)

noncomputable def TrilinearHT.Auto.GreedyTree.T (S : GreedyTree) : ℝ

The first-crossing threshold A / (1/4).

Equations

• S.T = S.A / (1 / 4)

noncomputable def TrilinearHT.Auto.GreedyTree.sub (S : GreedyTree) (K : ℤ × ℤ) : Finset (ℤ × ℤ)

The finite tree below K.

Equations

• S.sub K = TrilinearHT.Auto.dyadicFiniteTree S.G K (TrilinearHT.Auto.dyadicRemainingDepth S.J S.N K)

noncomputable def TrilinearHT.Auto.GreedyTree.next (S : GreedyTree) (K : ℤ × ℤ) : Finset (ℤ × ℤ)

The roots of the next attempts below K: the first crossings of the path count.

Equations

• S.next K = TrilinearHT.Auto.dyadicFirstCrossings S.G (S.sub K) (S.newAt K) S.T

noncomputable def TrilinearHT.Auto.GreedyTree.gen (S : GreedyTree) : ℕ → Finset (ℤ × ℤ)

Restart generations.

Equations

• S.gen 0 = {S.J}
• S.gen n.succ = (S.gen n).biUnion S.next

noncomputable def TrilinearHT.Auto.GreedyTree.roots (S : GreedyTree) : Finset (ℤ × ℤ)

All attempt roots.

Equations

• S.roots = (Finset.range (S.N + 1)).biUnion S.gen

structure TrilinearHT.Auto.GreedyTree.Hyp (S : GreedyTree) : Prop

Hypotheses: nonnegative mass constant, the mass bound, and trivial stopping off the tree.

• A_nonneg : 0 ≤ S.A
• mass (K : ℤ × ℤ) : K ∈ dyadicFiniteTree S.G S.J S.N → dyadicWeightedMass S.G (S.sub K) (S.newAt K) ≤ S.A * dyadicGridLength S.G K.1
• escape (c : ℤ × ℤ) (a : ℕ → ℝ → ℂ) (n : ℕ) : c ∉ dyadicFiniteTree S.G S.J S.N → S.P c a n

theorem TrilinearHT.Auto.GreedyTree.newAt_nonneg {S : GreedyTree} (K c : ℤ × ℤ) : 0 ≤ S.newAt K c

theorem TrilinearHT.Auto.GreedyTree.sub_mem_iff {S : GreedyTree} {K : ℤ × ℤ} (hK : K ∈ dyadicFiniteTree S.G S.J S.N) (c : ℤ × ℤ) : c ∈ S.sub K ↔ c ∈ dyadicFiniteTree S.G S.J S.N ∧ S.cell c ⊆ S.cell K

theorem TrilinearHT.Auto.GreedyTree.cell_subset_of_tree {S : GreedyTree} {c : ℤ × ℤ} (hc : c ∈ dyadicFiniteTree S.G S.J S.N) : S.cell c ⊆ S.cell S.J

theorem TrilinearHT.Auto.GreedyTree.Hyp.next_length_le {S : GreedyTree} (h : S.Hyp) {K : ℤ × ℤ} (hK : K ∈ dyadicFiniteTree S.G S.J S.N) : dyadicRootLength S.G (S.next K) ≤ 1 / 4 * dyadicGridLength S.G K.1

theorem TrilinearHT.Auto.GreedyTree.count_eq_ancestorSum {S : GreedyTree} {K c : ℤ × ℤ} (hc : c ∈ S.sub K) : ↑(S.state (c.1 - K.1).toNat c).2 = dyadicAncestorSum S.G (S.sub K) (S.newAt K) c

theorem TrilinearHT.Auto.GreedyTree.Hyp.next_depth {S : GreedyTree} (h : S.Hyp) {K b : ℤ × ℤ} (hK : K ∈ dyadicFiniteTree S.G S.J S.N) (hb : b ∈ S.next K) : K.1 < b.1 ∧ S.cell b ⊆ S.cell K

theorem TrilinearHT.Auto.GreedyTree.Hyp.gen_mem {S : GreedyTree} (h : S.Hyp) (n : ℕ) {c : ℤ × ℤ} (hc : c ∈ S.gen n) : c ∈ dyadicFiniteTree S.G S.J S.N ∧ S.J.1 + ↑n ≤ c.1

theorem TrilinearHT.Auto.GreedyTree.Hyp.gen_length_le {S : GreedyTree} (h : S.Hyp) (n : ℕ) : dyadicRootLength S.G (S.gen n) ≤ (1 / 4) ^ n * dyadicGridLength S.G S.J.1

theorem TrilinearHT.Auto.GreedyTree.Hyp.roots_length_le {S : GreedyTree} (h : S.Hyp) : dyadicRootLength S.G S.roots ≤ 4 / 3 * dyadicGridLength S.G S.J.1

The restarted segments have total root length at most 4/3 |J|.

theorem TrilinearHT.Auto.GreedyTree.J_mem_roots {S : GreedyTree} : S.J ∈ S.roots

theorem TrilinearHT.Auto.GreedyTree.Hyp.roots_mem {S : GreedyTree} (h : S.Hyp) {K : ℤ × ℤ} (hK : K ∈ S.roots) : K ∈ dyadicFiniteTree S.G S.J S.N

theorem TrilinearHT.Auto.GreedyTree.Hyp.roots_closed {S : GreedyTree} (h : S.Hyp) {K b : ℤ × ℤ} (hK : K ∈ S.roots) (hb : b ∈ S.next K) : b ∈ S.roots

theorem TrilinearHT.Auto.GreedyTree.Hyp.segment_exists {S : GreedyTree} (h : S.Hyp) {u : ℤ × ℤ} (hu : u ∈ dyadicFiniteTree S.G S.J S.N) : ∃ K ∈ S.roots, S.cell u ⊆ S.cell K ∧ (∀ b ∈ S.next K, ¬S.cell u ⊆ S.cell b) ∧ ∀ L ∈ S.roots, S.cell u ⊆ S.cell L → L.1 ≤ K.1

noncomputable def TrilinearHT.Auto.GreedyTree.seg (S : GreedyTree) (u : ℤ × ℤ) : ℤ × ℤ

The root of the segment containing a tree cell: its deepest attempt root.

Equations

• S.seg u = if h : u ∈ TrilinearHT.Auto.dyadicFiniteTree S.G S.J S.N ∧ S.Hyp then Classical.choose ⋯ else u

noncomputable def TrilinearHT.Auto.GreedyTree.depthIn (S : GreedyTree) (u : ℤ × ℤ) : ℕ

The depth of a cell below its segment root.

Equations

• S.depthIn u = (u.1 - (S.seg u).1).toNat

noncomputable def TrilinearHT.Auto.GreedyTree.st (S : GreedyTree) (u : ℤ × ℤ) : (ℕ → ℝ → ℂ) × ℕ

The final state at a cell.

Equations

• S.st u = S.state (S.depthIn u) u

theorem TrilinearHT.Auto.GreedyTree.Hyp.seg_spec {S : GreedyTree} (h : S.Hyp) {u : ℤ × ℤ} (hu : u ∈ dyadicFiniteTree S.G S.J S.N) : S.seg u ∈ S.roots ∧ S.cell u ⊆ S.cell (S.seg u) ∧ (∀ b ∈ S.next (S.seg u), ¬S.cell u ⊆ S.cell b) ∧ ∀ L ∈ S.roots, S.cell u ⊆ S.cell L → L.1 ≤ (S.seg u).1

theorem TrilinearHT.Auto.GreedyTree.Hyp.retained {S : GreedyTree} (h : S.Hyp) (hM : S.T < ↑S.M) {u : ℤ × ℤ} (hu : u ∈ dyadicFiniteTree S.G S.J S.N) : (S.st u).2 < S.M ∧ S.P u (S.st u).1 (S.st u).2

On every tree cell the greedy stopped below the cap, so the predicate holds.

Tuple-specific accurate high fits

theorem TrilinearHT.Auto.GreedyTree.Hyp.seg_between {S : GreedyTree} (h : S.Hyp) {u v : ℤ × ℤ} (hu : u ∈ dyadicFiniteTree S.G S.J S.N) (hv : v ∈ dyadicFiniteTree S.G S.J S.N) (huv : S.cell u ⊆ S.cell v) (hvs : S.cell v ⊆ S.cell (S.seg u)) : S.seg v = S.seg u

A cell between a tree cell and its segment root has the same segment root.

Restarts and segments of the adaptive fit

noncomputable def TrilinearHT.Auto.FitSetup.toGreedyTree (S : FitSetup) : GreedyTree

The adaptive fit is the general restart construction with insertion mass 4 B².

Equations

• S.toGreedyTree = { G := S.G, J := S.J, N := S.N, M := S.M, P := S.P, O := S.O, A := 4 * S.B ^ 2 }

noncomputable def TrilinearHT.Auto.FitSetup.state (S : FitSetup) (d : ℕ) (c : ℤ × ℤ) : (ℕ → ℝ → ℂ) × ℕ

The state of the attempt d generations below its root.

Equations

• S.state d c = TrilinearHT.Auto.fitState S.G S.M S.P S.O d c

noncomputable def TrilinearHT.Auto.FitSetup.newAt (S : FitSetup) (K c : ℤ × ℤ) : ℝ

Insertion counts of the attempt rooted at K.

Equations

• S.newAt K c = ↑(TrilinearHT.Auto.fitNew S.G S.M S.P S.O (c.1 - K.1).toNat c)

noncomputable def TrilinearHT.Auto.FitSetup.T (S : FitSetup) : ℝ

The first-crossing threshold (4 B²)/(1/4).

Equations

• S.T = 4 * S.B ^ 2 / (1 / 4)

noncomputable def TrilinearHT.Auto.FitSetup.sub (S : FitSetup) (K : ℤ × ℤ) : Finset (ℤ × ℤ)

The finite tree below K.

Equations

• S.sub K = TrilinearHT.Auto.dyadicFiniteTree S.G K (TrilinearHT.Auto.dyadicRemainingDepth S.J S.N K)

noncomputable def TrilinearHT.Auto.FitSetup.next (S : FitSetup) (K : ℤ × ℤ) : Finset (ℤ × ℤ)

The roots of the next attempts below K: the first crossings of the path count.

Equations

• S.next K = TrilinearHT.Auto.dyadicFirstCrossings S.G (S.sub K) (S.newAt K) S.T

noncomputable def TrilinearHT.Auto.FitSetup.gen (S : FitSetup) : ℕ → Finset (ℤ × ℤ)

Restart generations.

Equations

• S.gen = S.toGreedyTree.gen

noncomputable def TrilinearHT.Auto.FitSetup.roots (S : FitSetup) : Finset (ℤ × ℤ)

All attempt roots.

Equations

• S.roots = S.toGreedyTree.roots

theorem TrilinearHT.Auto.FitSetup.newAt_nonneg {S : FitSetup} (K c : ℤ × ℤ) : 0 ≤ S.newAt K c

theorem TrilinearHT.Auto.FitSetup.sub_mem_iff {S : FitSetup} {K : ℤ × ℤ} (hK : K ∈ dyadicFiniteTree S.G S.J S.N) (c : ℤ × ℤ) : c ∈ S.sub K ↔ c ∈ dyadicFiniteTree S.G S.J S.N ∧ S.cell c ⊆ S.cell K

theorem TrilinearHT.Auto.FitSetup.cell_subset_of_tree {S : FitSetup} {c : ℤ × ℤ} (hc : c ∈ dyadicFiniteTree S.G S.J S.N) : S.cell c ⊆ S.cell S.J

theorem TrilinearHT.Auto.FitSetup.T_eq {S : FitSetup} : S.T = 16 * S.B ^ 2

theorem TrilinearHT.Auto.FitSetup.Hyp.mass_le {S : FitSetup} (h : S.Hyp) {K : ℤ × ℤ} (hK : K ∈ dyadicFiniteTree S.G S.J S.N) : dyadicWeightedMass S.G (S.sub K) (S.newAt K) ≤ 4 * S.B ^ 2 * dyadicGridLength S.G K.1

The weighted insertion mass of the attempt at K is at most 4 B² |K|.

theorem TrilinearHT.Auto.FitSetup.Hyp.toGreedyTree {S : FitSetup} (h : S.Hyp) : S.toGreedyTree.Hyp

Analytic fit hypotheses supply the three hypotheses of the general restart theorem.

theorem TrilinearHT.Auto.FitSetup.Hyp.next_length_le {S : FitSetup} (h : S.Hyp) {K : ℤ × ℤ} (hK : K ∈ dyadicFiniteTree S.G S.J S.N) : dyadicRootLength S.G (S.next K) ≤ 1 / 4 * dyadicGridLength S.G K.1

Blueprint §11.2, line 1577: the first stopped roots cost at most a quarter of the root.

theorem TrilinearHT.Auto.FitSetup.count_eq_ancestorSum {S : FitSetup} {K c : ℤ × ℤ} (hc : c ∈ S.sub K) : ↑(S.state (c.1 - K.1).toNat c).2 = dyadicAncestorSum S.G (S.sub K) (S.newAt K) c

The count at a cell of the attempt at K equals its ancestor sum.

theorem TrilinearHT.Auto.FitSetup.Hyp.next_depth {S : FitSetup} (h : S.Hyp) {K b : ℤ × ℤ} (hK : K ∈ dyadicFiniteTree S.G S.J S.N) (hb : b ∈ S.next K) : K.1 < b.1 ∧ S.cell b ⊆ S.cell K

Next roots are strictly below their attempt root.

theorem TrilinearHT.Auto.FitSetup.Hyp.gen_mem {S : FitSetup} (h : S.Hyp) (n : ℕ) {c : ℤ × ℤ} (hc : c ∈ S.gen n) : c ∈ dyadicFiniteTree S.G S.J S.N ∧ S.J.1 + ↑n ≤ c.1

theorem TrilinearHT.Auto.FitSetup.Hyp.gen_length_le {S : FitSetup} (h : S.Hyp) (n : ℕ) : dyadicRootLength S.G (S.gen n) ≤ (1 / 4) ^ n * dyadicGridLength S.G S.J.1

theorem TrilinearHT.Auto.FitSetup.Hyp.roots_length_le {S : FitSetup} (h : S.Hyp) : dyadicRootLength S.G S.roots ≤ 4 / 3 * dyadicGridLength S.G S.J.1

Blueprint §11.2, line 1577: the restarted segments have total root length at most 4/3 |J|.

theorem TrilinearHT.Auto.FitSetup.J_mem_roots {S : FitSetup} : S.J ∈ S.roots

theorem TrilinearHT.Auto.FitSetup.Hyp.roots_mem {S : FitSetup} (h : S.Hyp) {K : ℤ × ℤ} (hK : K ∈ S.roots) : K ∈ dyadicFiniteTree S.G S.J S.N

theorem TrilinearHT.Auto.FitSetup.Hyp.roots_closed {S : FitSetup} (h : S.Hyp) {K b : ℤ × ℤ} (hK : K ∈ S.roots) (hb : b ∈ S.next K) : b ∈ S.roots

theorem TrilinearHT.Auto.FitSetup.Hyp.segment_exists {S : FitSetup} (h : S.Hyp) {u : ℤ × ℤ} (hu : u ∈ dyadicFiniteTree S.G S.J S.N) : ∃ K ∈ S.roots, S.cell u ⊆ S.cell K ∧ (∀ b ∈ S.next K, ¬S.cell u ⊆ S.cell b) ∧ ∀ L ∈ S.roots, S.cell u ⊆ S.cell L → L.1 ≤ K.1

Every tree cell lies in the segment of its deepest root.

The inherited adaptive fit

noncomputable def TrilinearHT.Auto.FitSetup.seg (S : FitSetup) (u : ℤ × ℤ) : ℤ × ℤ

The root of the segment containing a tree cell: its deepest attempt root.

Equations

• S.seg u = if h : u ∈ TrilinearHT.Auto.dyadicFiniteTree S.G S.J S.N ∧ S.Hyp then Classical.choose ⋯ else u

noncomputable def TrilinearHT.Auto.FitSetup.depthIn (S : FitSetup) (u : ℤ × ℤ) : ℕ

The depth of a cell below its segment root.

Equations

• S.depthIn u = (u.1 - (S.seg u).1).toNat

noncomputable def TrilinearHT.Auto.FitSetup.st (S : FitSetup) (u : ℤ × ℤ) : (ℕ → ℝ → ℂ) × ℕ

The final state at a cell.

Equations

• S.st u = S.state (S.depthIn u) u

noncomputable def TrilinearHT.Auto.FitSetup.g (S : FitSetup) (u : ℤ × ℤ) : ℝ → ℂ

The fitted physical function g_I at a cell.

Equations

• S.g u = S.phys u (S.st u).1 (S.st u).2

theorem TrilinearHT.Auto.FitSetup.Hyp.seg_spec {S : FitSetup} (h : S.Hyp) {u : ℤ × ℤ} (hu : u ∈ dyadicFiniteTree S.G S.J S.N) : S.seg u ∈ S.roots ∧ S.cell u ⊆ S.cell (S.seg u) ∧ (∀ b ∈ S.next (S.seg u), ¬S.cell u ⊆ S.cell b) ∧ ∀ L ∈ S.roots, S.cell u ⊆ S.cell L → L.1 ≤ (S.seg u).1

theorem TrilinearHT.Auto.FitSetup.Hyp.retained {S : FitSetup} (h : S.Hyp) (hM : S.T < ↑S.M) {u : ℤ × ℤ} (hu : u ∈ dyadicFiniteTree S.G S.J S.N) : (S.st u).2 < S.M ∧ FormSmall (dyadicGridLeft S.G u.1 u.2) (dyadicGridLength S.G u.1) (S.w u) S.j S.q (S.res u (S.st u).1 (S.st u).2) (Real.exp (-↑S.k))

On every tree cell the greedy fit stopped below the cap, so the residual is small.

theorem TrilinearHT.Auto.FitSetup.Hyp.inherited {S : FitSetup} (h : S.Hyp) {u u' : ℤ × ℤ} (hu : u ∈ dyadicFiniteTree S.G S.J S.N) (hu' : u' ∈ dyadicFiniteTree S.G S.J S.N) (huu' : S.cell u ⊆ S.cell u') (hu'K : S.cell u' ⊆ S.cell (S.seg u)) : S.seg u' = S.seg u ∧ FitPrefix (S.st u) (S.st u')

Within a segment, deeper cells inherit the list of their ancestors.

theorem TrilinearHT.Auto.FitSetup.Hyp.atoms_good {S : FitSetup} (h : S.Hyp) (d : ℕ) (c : ℤ × ℤ) (i : ℕ) : i < (S.state d c).2 → ∃ (p : (d : ℕ) × QuadraticChartData d), QuadraticChartComplexity S.c₂ S.B p.snd ∧ IsBoundedQuadraticChart p.snd ∧ (S.state d c).1 i = quadraticChartAtom p.snd

Every atom of every list is a bounded detection chart.

theorem TrilinearHT.Auto.FitSetup.Hyp.g_coeff {S : FitSetup} (h : S.Hyp) {u : ℤ × ℤ} (hu : u ∈ dyadicFiniteTree S.G S.J S.N) (hT : kernelHull S.G S.J S.N S.w u) : ∃ (coef : Fin S.M → ℂ), ∑ i : Fin S.M, ‖coef i‖ ^ 2 ≤ 1 ∧ (∀ (i : Fin S.M), (S.st u).2 ≤ ↑i → coef i = 0) ∧ ∀ (y : ℝ), S.g u y = ∑ i : Fin S.M, coef i * (S.st u).1 (↑i) y

The fitted function is a combination of the atoms with coefficient ℓ² norm at most one.

theorem TrilinearHT.Auto.FitSetup.Hyp.g_norm_le {S : FitSetup} (h : S.Hyp) {u : ℤ × ℤ} (hu : u ∈ dyadicFiniteTree S.G S.J S.N) (hT : kernelHull S.G S.J S.N S.w u) (y : ℝ) : ‖S.g u y‖ ≤ √↑S.M

Packaging the adaptive fit as column tree data

theorem TrilinearHT.Auto.fitGreedy_inv_all {M : ℕ} {P : (ℕ → ℝ → ℂ) → ℕ → Prop} {O : (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ} (Good : (ℝ → ℂ) → Prop) (hO : ∀ (a : ℕ → ℝ → ℂ) (n : ℕ), Good (O a n)) (st : (ℕ → ℝ → ℂ) × ℕ) (h : ∀ (i : ℕ), Good (st.1 i)) (i : ℕ) : Good ((fitGreedy M P O st).1 i)

theorem TrilinearHT.Auto.fitState_inv_all (G : RealDyadicGrid) (M : ℕ) (P : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → Prop) (O : ℤ × ℤ → (ℕ → ℝ → ℂ) → ℕ → ℝ → ℂ) (Good : (ℝ → ℂ) → Prop) (h0 : Good 0) (hO : ∀ (c : ℤ × ℤ) (a : ℕ → ℝ → ℂ) (n : ℕ), Good (O c a n)) (d : ℕ) (c : ℤ × ℤ) (i : ℕ) : Good ((fitState G M P O d c).1 i)

theorem TrilinearHT.Auto.fitOracleAtom_measurable (c₂ : ℕ) (B a₀ r : ℝ) (R : ℝ → ℂ) : Measurable (fitOracleAtom c₂ B a₀ r R)

theorem TrilinearHT.Auto.fitOracleAtom_bound (c₂ : ℕ) (B a₀ r : ℝ) (R : ℝ → ℂ) (y : ℝ) : ‖fitOracleAtom c₂ B a₀ r R y‖ ≤ 1

theorem TrilinearHT.Auto.norm_privateColumnValue_sq {V : Type u_1} [Fintype V] (φ : V → ℝ → ℂ) (ε : V → ℝ) (v : V) (y : ℝ) (hε : 0 ≤ ε v) : ‖privateColumnValue φ ε v y‖ ^ 2 = ‖φ v y‖ ^ 2 + ε v

theorem TrilinearHT.Auto.dyadicIndex_measurable (G : RealDyadicGrid) (h : ℤ) : Measurable (dyadicIndex G h)

theorem TrilinearHT.Auto.FitSetup.state_measurable {S : FitSetup} (d : ℕ) (c : ℤ × ℤ) (i : ℕ) : Measurable ((S.state d c).1 i)

theorem TrilinearHT.Auto.FitSetup.state_bound {S : FitSetup} (d : ℕ) (c : ℤ × ℤ) (i : ℕ) (y : ℝ) : ‖(S.state d c).1 i y‖ ≤ 1

def TrilinearHT.Auto.FitSetup.leafDepth (S : FitSetup) : ℤ

The depth of the leaves of the tree.

Equations

• S.leafDepth = S.J.1 + ↑S.N

noncomputable def TrilinearHT.Auto.FitSetup.leaf (S : FitSetup) (y : ℝ) : ℤ × ℤ

The leaf containing y.

Equations

• S.leaf y = (S.leafDepth, TrilinearHT.Auto.dyadicIndex S.G S.leafDepth y)

noncomputable def TrilinearHT.Auto.FitSetup.count (S : FitSetup) (K c : ℤ × ℤ) : ℕ

The count of the attempt rooted at K at the cell c.

Equations

• S.count K c = (S.state (c.1 - K.1).toNat c).2

noncomputable def TrilinearHT.Auto.FitSetup.atoms (S : FitSetup) (K c : ℤ × ℤ) : ℕ → ℝ → ℂ

The atoms of the attempt rooted at K at the cell c.

Equations

• S.atoms K c = (S.state (c.1 - K.1).toNat c).1

noncomputable def TrilinearHT.Auto.FitSetup.scalar (S : FitSetup) (K : ℤ × ℤ) (v : Fin S.M) (y : ℝ) : ℂ

The scalar of label v for the attempt rooted at K: the atom of the leaf below y.

Equations

• S.scalar K v y = if y ∈ S.cell K then S.atoms K (S.leaf y) (↑v) y else 0

theorem TrilinearHT.Auto.FitSetup.leaf_mem {S : FitSetup} (y : ℝ) : y ∈ S.cell (S.leaf y)

theorem TrilinearHT.Auto.FitSetup.scalar_measurable {S : FitSetup} (K : ℤ × ℤ) (v : Fin S.M) : Measurable (S.scalar K v)

theorem TrilinearHT.Auto.FitSetup.scalar_bound {S : FitSetup} (K : ℤ × ℤ) (v : Fin S.M) (y : ℝ) : ‖S.scalar K v y‖ ≤ 1

theorem TrilinearHT.Auto.FitSetup.atoms_leaf {S : FitSetup} {K c : ℤ × ℤ} (hK : K ∈ dyadicFiniteTree S.G S.J S.N) (hc : c ∈ S.sub K) {y : ℝ} (hy : y ∈ S.cell c) {v : ℕ} (hv : v < S.count K c) : S.atoms K (S.leaf y) v = S.atoms K c v

Below the attempt root, the leaf list extends the list of every cell containing y.

theorem TrilinearHT.Auto.FitSetup.scalar_eq {S : FitSetup} {K c : ℤ × ℤ} (hK : K ∈ dyadicFiniteTree S.G S.J S.N) (hc : c ∈ S.sub K) {y : ℝ} (hy : y ∈ S.cell c) {v : Fin S.M} (hv : ↑v < S.count K c) : S.scalar K v y = S.atoms K c (↑v) y

theorem TrilinearHT.Auto.FitSetup.count_mono {S : FitSetup} {K c d : ℤ × ℤ} (h2 : K.1 ≤ d.1) (hcd : S.cell c ⊆ S.cell d) : S.count K d ≤ S.count K c

noncomputable def TrilinearHT.Auto.FitSetup.treeData (S : FitSetup) (K R : ℤ × ℤ) : ColumnTreeData (Fin S.M)

The column tree data of the attempt rooted at K, on the tree below a cell R of it (blueprint §11.2, line 1574; renormalized at R as in sec:reduction, line 429): labels Fin M, all born at R, private weight one, leaf-piecewise scalars.

Equations

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

noncomputable def TrilinearHT.Auto.FitSetup.treeMask (S : FitSetup) (K R : ℤ × ℤ) (hKR : K.1 ≤ R.1) : InheritedColumnMask (S.treeData K R)

The inherited mask {m < count} of the attempt rooted at K.

Equations

• S.treeMask K R hKR = { labels := fun (c : ℤ × ℤ) => {v : Fin S.M | ↑v < S.count K c}, available := ⋯, inherited := ⋯ }

noncomputable def TrilinearHT.Auto.FitSetup.depthFamily (S : FitSetup) (K R : ℤ × ℤ) (hR : R ∈ dyadicFiniteTree S.G S.J S.N) (hKR : K.1 ≤ R.1) : ColumnDepthFamily (Fin S.M)

The attempt rooted at K as a column depth family on the tree below R.

Equations

• S.depthFamily K R hR hKR = { D := S.treeData K R, A := S.treeMask K R hKR, N := S.leafDepth, root_le := ⋯, complete := ⋯ }

theorem TrilinearHT.Auto.FitSetup.treeProjection_eq {S : FitSetup} {K R c : ℤ × ℤ} (hK : K ∈ dyadicFiniteTree S.G S.J S.N) (hR : R ∈ dyadicFiniteTree S.G S.J S.N) (hRK : S.cell R ⊆ S.cell K) (hKR : K.1 ≤ R.1) (hc : c ∈ (S.treeData K R).cells) (z : ↥(ColumnL2 (Fin S.M))) : (cellColumnProjection (S.treeData K R) (S.treeMask K R hKR) hc) z = (fitProj S.M (S.cell c) (S.atoms K c) (S.count K c)) z

The projection of the packaged data is the fit projection.

Current projections: cellwise identification and depth energy

theorem TrilinearHT.Auto.ColumnDepthFamily.anc_self {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) {I : ℤ × ℤ} (hI : I.1 ≤ Ψ.N) : Ψ.anc I = I

theorem TrilinearHT.Auto.ColumnDepthFamily.current_of_mem {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) {I : ℤ × ℤ} (hI : Ψ.anc I ∈ Ψ.D.cells) : Ψ.current f I = fun (y : ℝ) => (↑↑((cellColumnProjection Ψ.D Ψ.A hI) (physicalColumnInput f)) y).ofLp none

theorem TrilinearHT.Auto.ColumnDepthFamily.current_ae_proj {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) {I : ℤ × ℤ} (hI : dyadicGridCell Ψ.D.grid I.1 I.2 ⊆ dyadicGridCell Ψ.D.grid Ψ.D.root.1 Ψ.D.root.2) : ∀ᵐ (y : ℝ) ∂MeasureTheory.volume.restrict (dyadicGridCell Ψ.D.grid I.1 I.2), Ψ.current f I y = (↑↑((Ψ.proj I.1) (physicalColumnInput f)) y).ofLp none

On a row cell below the root, the current projection is a.e. the depth projection.

theorem TrilinearHT.Auto.ColumnDepthFamily.current_depthEnergy {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : HasDepthEnergy Ψ.D.grid Ψ.D.root (↑↑f) (Ψ.current f) 1

Current projection opponents have depth energy with constant one.

theorem TrilinearHT.Auto.FitSetup.current_ae_fit {S : FitSetup} {K R I : ℤ × ℤ} (hK : K ∈ dyadicFiniteTree S.G S.J S.N) (hR : R ∈ dyadicFiniteTree S.G S.J S.N) (hRK : S.cell R ⊆ S.cell K) (hKR : K.1 ≤ R.1) (hI : I ∈ S.sub R) : ∀ᵐ (y : ℝ), y ∈ S.cell I → (S.depthFamily K R hR hKR).current S.input I y = S.phys I (S.atoms K I) (S.count K I) y

On tree cells below R, the current projection of the packaged attempt is the fit (a.e. on the cell).

The fits as admissible opponents

theorem TrilinearHT.Auto.isAdmissibleOpponent_congr {G : RealDyadicGrid} {J : ℤ × ℤ} {F F' : ℝ → ℂ} {z z' : ℤ × ℤ → ℝ → ℂ} {K : ℝ} (h : IsAdmissibleOpponent G J F z K) (hz : ∀ (I : ℤ × ℤ), dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G J.1 J.2 → z' I = z I) (hF : ∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖F y‖ ^ 2 = ∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖F' y‖ ^ 2) : IsAdmissibleOpponent G J F' z' K

Admissibility is invariant under changes of the opponent on the cells below the root and of the input with the same energy on the root.

theorem TrilinearHT.Auto.hasDepthEnergy_congr {G : RealDyadicGrid} {J : ℤ × ℤ} {F F' : ℝ → ℂ} {z z' : ℤ × ℤ → ℝ → ℂ} {K : ℝ} (h : HasDepthEnergy G J F z K) (hz : ∀ (I : ℤ × ℤ), dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G J.1 J.2 → z' I = z I) (hF : ∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖F y‖ ^ 2 = ∫ (y : ℝ) in dyadicGridCell G J.1 J.2, ‖F' y‖ ^ 2) : HasDepthEnergy G J F' z' K

noncomputable def TrilinearHT.Auto.fitOpponentConst (M : ℕ) : ℝ

The compression constant of the fit families (lem:compression with m = 1 and budget max 2 M).

Equations

• TrilinearHT.Auto.fitOpponentConst M = (512 * (↑1 + 1) ^ 512 * Real.log (2 * max 2 ↑M)) ^ (512 * (1 + 1))

theorem TrilinearHT.Auto.fitOpponentConst_nonneg (M : ℕ) : 0 ≤ fitOpponentConst M

def TrilinearHT.Auto.IsAdaptiveFit (c₂ : ℕ) (B : ℝ) (G : RealDyadicGrid) (J : ℤ × ℤ) (N : ℕ) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (j : Fin 4) (q : ℝ) (f : ℝ → ℂ) (k M : ℕ) (roots : Finset (ℤ × ℤ)) (seg : ℤ × ℤ → ℤ × ℤ) (n : ℤ × ℤ → ℕ) (a : ℤ × ℤ → ℕ → ℝ → ℂ) (g : ℤ × ℤ → ℝ → ℂ) : Prop

The conclusion of the adaptive fit (blueprint §11.2, lines 1567-1579) for an input f in slot j at accuracy e^{-k} with chart budget B, on the complete finite tree of depth N below J: restarted segments with total root length at most 4/3 |J|, inherited lists of at most M ≤ 17 B² bounded chart atoms extending along each segment, and fitted combinations g_I (coefficient ℓ² norm at most one, |g_I| ≤ √M, ‖g_I‖_{2,I} ≤ 1) with small residual d_{j,I}(f - g_I) ≤ e^{-k} on every tree cell.

Equations

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

def TrilinearHT.Auto.PairSmall (a₀ r : ℝ) (w : ℝ × ℝ → ℂ) (p p' : Fin 4) (X Y : ℝ → ℂ) (η : ℝ) : Prop

The bilinear norm of the pair (X, Y) in slots p ≠ p' against normalized L² spectators is at most η (blueprint §11.2, lines 1589-1596).

Equations

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

theorem TrilinearHT.Auto.fin4_other_two (p p' : Fin 4) : p ≠ p' → ∃ (a : Fin 4) (b : Fin 4), a ≠ b ∧ a ≠ p ∧ a ≠ p' ∧ b ≠ p ∧ b ≠ p' ∧ ∀ (l : Fin 4), l = p ∨ l = p' ∨ l = a ∨ l = b

theorem TrilinearHT.Auto.localProgressionForm_update_sub {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {f : Fin 4 → ℝ → ℂ} (hf : ∀ (j : Fin 4), Measurable (f j)) (hfin : ∀ (j : Fin 4), MeasureTheory.eLpNorm (f j) 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (k : Fin 4) {g₁ g₂ : ℝ → ℂ} (hg₁ : Measurable g₁) (hg₂ : Measurable g₂) (hg₁f : MeasureTheory.eLpNorm g₁ 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hg₂f : MeasureTheory.eLpNorm g₂ 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) : localProgressionForm r w (Function.update f k (g₁ - g₂)) = localProgressionForm r w (Function.update f k g₁) - localProgressionForm r w (Function.update f k g₂)

Subtraction in one slot of the local form, for finite normalized L² inputs.

def TrilinearHT.Auto.SpectatorOK (a₀ r : ℝ) (z : Fin 4 → ℝ → ℂ) (p p' : Fin 4) : Prop

Hypotheses for pair computations: measurable spectators of finite normalized L² norm.

Equations

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

def TrilinearHT.Auto.FinL2 (a₀ r : ℝ) (X : ℝ → ℂ) : Prop

A function with finite normalized L² norm.

Equations

• TrilinearHT.Auto.FinL2 a₀ r X = (Measurable X ∧ MeasureTheory.eLpNorm X 2 (TrilinearHT.Auto.normalizedIntervalMeasure a₀ r) ≠ ⊤)

theorem TrilinearHT.Auto.FinL2.sub {a₀ r : ℝ} {X Y : ℝ → ℂ} (hX : FinL2 a₀ r X) (hY : FinL2 a₀ r Y) : FinL2 a₀ r (X - Y)

theorem TrilinearHT.Auto.FinL2.zero {a₀ r : ℝ} : FinL2 a₀ r 0

theorem TrilinearHT.Auto.FinL2.of_bound {a₀ r : ℝ} (hr : 0 < r) {X : ℝ → ℂ} (hX : Measurable X) {S : ℝ} (hS : ∀ (y : ℝ), ‖X y‖ ≤ S) : FinL2 a₀ r X

theorem TrilinearHT.Auto.slotPair_meas {z : Fin 4 → ℝ → ℂ} {p p' : Fin 4} (hz : ∀ (l : Fin 4), Measurable (z l)) {X Y : ℝ → ℂ} (hX : Measurable X) (hY : Measurable Y) (l : Fin 4) : Measurable (slotPair z p p' X Y l)

theorem TrilinearHT.Auto.slotPair_fin {a₀ r : ℝ} {z : Fin 4 → ℝ → ℂ} {p p' : Fin 4} (hz : SpectatorOK a₀ r z p p') {X Y : ℝ → ℂ} (hX : FinL2 a₀ r X) (hY : FinL2 a₀ r Y) (l : Fin 4) : MeasureTheory.eLpNorm (slotPair z p p' X Y l) 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤

theorem TrilinearHT.Auto.slotPair_sub_right {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {z : Fin 4 → ℝ → ℂ} {p p' : Fin 4} (hz : SpectatorOK a₀ r z p p') {X Y Y' : ℝ → ℂ} (hX : FinL2 a₀ r X) (hY : FinL2 a₀ r Y) (hY' : FinL2 a₀ r Y') : localProgressionForm r w (slotPair z p p' X (Y - Y')) = localProgressionForm r w (slotPair z p p' X Y) - localProgressionForm r w (slotPair z p p' X Y')

theorem TrilinearHT.Auto.slotPair_sub_left {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {z : Fin 4 → ℝ → ℂ} {p p' : Fin 4} (hpp : p ≠ p') (hz : SpectatorOK a₀ r z p p') {X X' Y : ℝ → ℂ} (hX : FinL2 a₀ r X) (hX' : FinL2 a₀ r X') (hY : FinL2 a₀ r Y) : localProgressionForm r w (slotPair z p p' (X - X') Y) = localProgressionForm r w (slotPair z p p' X Y) - localProgressionForm r w (slotPair z p p' X' Y)

theorem TrilinearHT.Auto.slotPair_const_smul_right {r : ℝ} {w : ℝ × ℝ → ℂ} (z : Fin 4 → ℝ → ℂ) (p p' : Fin 4) (X Y : ℝ → ℂ) (c : ℂ) : localProgressionForm r w (slotPair z p p' X (c • Y)) = c * localProgressionForm r w (slotPair z p p' X Y)

theorem TrilinearHT.Auto.FormSmall.apply_pair {a₀ r : ℝ} {w : ℝ × ℝ → ℂ} {p p' : Fin 4} (hpp : p ≠ p') {q : ℝ} {R : ℝ → ℂ} {η : ℝ} (h : FormSmall a₀ r w p q R η) (hR : Measurable R) {V : ℝ → ℂ} (hV : Measurable V) (hVq : MeasureTheory.eLpNorm V (ENNReal.ofReal q) (normalizedIntervalMeasure a₀ r) ≤ 1) {z : Fin 4 → ℝ → ℂ} (hz : ∀ (l : Fin 4), Measurable (z l)) (hz2 : ∀ (l : Fin 4), l ≠ p → l ≠ p' → MeasureTheory.eLpNorm (z l) 2 (normalizedIntervalMeasure a₀ r) ≤ 1) : ‖localProgressionForm r w (slotPair z p p' R V)‖ ≤ η

Apply residual smallness with the residual in slot p and an L^q input in slot p'.

theorem TrilinearHT.Auto.FormSmall.apply_pair_bounded {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} {p p' : Fin 4} (hpp : p ≠ p') {q : ℝ} {R : ℝ → ℂ} {η : ℝ} (h : FormSmall a₀ r w p q R η) (hR : Measurable R) {V : ℝ → ℂ} (hV : Measurable V) {S : ℝ} (hS : 0 < S) (hVS : ∀ (y : ℝ), ‖V y‖ ≤ S) {z : Fin 4 → ℝ → ℂ} (hz : ∀ (l : Fin 4), Measurable (z l)) (hz2 : ∀ (l : Fin 4), l ≠ p → l ≠ p' → MeasureTheory.eLpNorm (z l) 2 (normalizedIntervalMeasure a₀ r) ≤ 1) : ‖localProgressionForm r w (slotPair z p p' R V)‖ ≤ S * η

The L^q slot may carry a function bounded by S, at the cost of the factor S.

Cyclic updates at one cell

def TrilinearHT.Auto.stagPos (t : ℕ) : Fin 4

The position updated at level t (cyclic order).

Equations

• TrilinearHT.Auto.stagPos t = ⟨t % 4, ⋯⟩

structure TrilinearHT.Auto.StaggerCell (κ : LocalKernelClass) : Type

The data of the cyclic updates at one cell: inputs normalized in L^q, and at each level t ≥ 1 a bounded projection of the input in position t mod 4 with residual smallness e^{-k_t}; the accuracies grow fast enough to dominate the supremum bounds.

• a₀ : ℝ

  Left endpoint of the cell undergoing staggered updates.

• r : ℝ

  Positive length of the cell undergoing staggered updates.

• w : ℝ × ℝ → ℂ

  Admissible local kernel on the update cell.

• q : ℝ

  Integrability exponent for the normalized input functions.

• f : Fin 4 → ℝ → ℂ

  The four input functions before staggered projection updates.

• g : ℕ → ℝ → ℂ

  Projected approximation selected at each update level.

• k : ℕ → ℝ

  Accuracy exponent controlling the residual at each update level.

• S : ℕ → ℝ

  Pointwise norm bound for each projected approximation.

• r_pos : 0 < self.r
• adm : IsAdmissibleLocalKernel κ self.a₀ self.r self.w
• two_le_q : 2 ≤ self.q
• f_meas (p : Fin 4) : Measurable (self.f p)
• f_norm (p : Fin 4) : MeasureTheory.eLpNorm (self.f p) (ENNReal.ofReal self.q) (normalizedIntervalMeasure self.a₀ self.r) ≤ 1
• g_meas (t : ℕ) : Measurable (self.g t)
• S_pos (t : ℕ) : 0 < self.S t
• g_bound (t : ℕ) (y : ℝ) : ‖self.g t y‖ ≤ self.S t
• g_L2 (t : ℕ) : MeasureTheory.eLpNorm (self.g t) 2 (normalizedIntervalMeasure self.a₀ self.r) ≤ 1
• g_small (t : ℕ) : 1 ≤ t → FormSmall self.a₀ self.r self.w (stagPos t) self.q (self.f (stagPos t) - self.g t) (Real.exp (-self.k t))
• k_nonneg (t : ℕ) : 0 ≤ self.k t
• k_grow (v h : ℕ) : 1 ≤ v → v < h → 2 * self.k v ≤ self.k h
• S_le (v h : ℕ) : 1 ≤ v → v < h → self.S v ≤ Real.exp (self.k h / 2)

@[reducible, inline]

noncomputable abbrev TrilinearHT.Auto.StaggerCell.μ {κ : LocalKernelClass} (C : StaggerCell κ) : MeasureTheory.Measure ℝ

The normalized measure of the cell.

Equations

• C.μ = TrilinearHT.Auto.normalizedIntervalMeasure C.a₀ C.r

@[reducible, inline]

noncomputable abbrev TrilinearHT.Auto.StaggerCell.H {κ : LocalKernelClass} (C : StaggerCell κ) (F : Fin 4 → ℝ → ℂ) : ℂ

The local form.

Equations

• C.H F = TrilinearHT.Auto.localProgressionForm C.r C.w F

theorem TrilinearHT.Auto.StaggerCell.k_mono {κ : LocalKernelClass} (C : StaggerCell κ) {v h : ℕ} (hv : 1 ≤ v) (hvh : v ≤ h) : C.k v ≤ C.k h

theorem TrilinearHT.Auto.StaggerCell.finL2_f {κ : LocalKernelClass} (C : StaggerCell κ) (p : Fin 4) : FinL2 C.a₀ C.r (C.f p)

theorem TrilinearHT.Auto.StaggerCell.finL2_g {κ : LocalKernelClass} (C : StaggerCell κ) (t : ℕ) : FinL2 C.a₀ C.r (C.g t)

def TrilinearHT.Auto.StaggerCell.tv {κ : LocalKernelClass} (C : StaggerCell κ) (s : Fin 4) : Option ℕ → ℝ → ℂ

Values of terms: none is the actual input, some ℓ the projection of level ℓ.

Equations

• C.tv s none = C.f s
• C.tv s (some ℓ) = C.g ℓ

theorem TrilinearHT.Auto.StaggerCell.finL2_tv {κ : LocalKernelClass} (C : StaggerCell κ) (s : Fin 4) (A : Option ℕ) : FinL2 C.a₀ C.r (C.tv s A)

def TrilinearHT.Auto.StaggerCell.Valid (s : Fin 4) (m : ℕ) (A : Option ℕ) : Prop

A term at slot s with projection levels at least m.

Equations

• TrilinearHT.Auto.StaggerCell.Valid s m A = ∀ (ℓ : ℕ), A = some ℓ → 1 ≤ ℓ ∧ TrilinearHT.Auto.stagPos ℓ = s ∧ m ≤ ℓ

def TrilinearHT.Auto.StaggerCell.Spect {κ : LocalKernelClass} (C : StaggerCell κ) (z : Fin 4 → ℝ → ℂ) (p p' : Fin 4) : Prop

Normalized spectators for the slots p, p'.

Equations

• C.Spect z p p' = ((∀ (l : Fin 4), Measurable (z l)) ∧ ∀ (l : Fin 4), l ≠ p → l ≠ p' → MeasureTheory.eLpNorm (z l) 2 C.μ ≤ 1)

theorem TrilinearHT.Auto.StaggerCell.Spect.flip {κ : LocalKernelClass} {C : StaggerCell κ} {z : Fin 4 → ℝ → ℂ} {p p' : Fin 4} (h : C.Spect z p p') : C.Spect z p' p

theorem TrilinearHT.Auto.StaggerCell.Spect.ok {κ : LocalKernelClass} {C : StaggerCell κ} {z : Fin 4 → ℝ → ℂ} {p p' : Fin 4} (h : C.Spect z p p') : SpectatorOK C.a₀ C.r z p p'

theorem TrilinearHT.Auto.StaggerCell.H_comm {κ : LocalKernelClass} (C : StaggerCell κ) (z : Fin 4 → ℝ → ℂ) {p p' : Fin 4} (h : p ≠ p') (X Y : ℝ → ℂ) : C.H (slotPair z p p' X Y) = C.H (slotPair z p' p Y X)

theorem TrilinearHT.Auto.StaggerCell.repl_input {κ : LocalKernelClass} (C : StaggerCell κ) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) {s' : Fin 4} (hs : stagPos ℓ ≠ s') {z : Fin 4 → ℝ → ℂ} (hz : C.Spect z (stagPos ℓ) s') : ‖C.H (slotPair z (stagPos ℓ) s' (C.g ℓ) (C.f s')) - C.H (slotPair z (stagPos ℓ) s' (C.f (stagPos ℓ)) (C.f s'))‖ ≤ Real.exp (-C.k ℓ)

Replacing a projection by its input against an actual input: error e^{-k_ℓ}.

theorem TrilinearHT.Auto.StaggerCell.repl_bounded {κ : LocalKernelClass} (C : StaggerCell κ) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) {s' : Fin 4} (hs : stagPos ℓ ≠ s') {z : Fin 4 → ℝ → ℂ} (hz : C.Spect z (stagPos ℓ) s') (v : ℕ) : ‖C.H (slotPair z (stagPos ℓ) s' (C.g ℓ) (C.g v)) - C.H (slotPair z (stagPos ℓ) s' (C.f (stagPos ℓ)) (C.g v))‖ ≤ C.S v * Real.exp (-C.k ℓ)

Replacing a projection by its input against a bounded function: error S e^{-k_ℓ}.

theorem TrilinearHT.Auto.StaggerCell.exp_half_le {κ : LocalKernelClass} (C : StaggerCell κ) {m h : ℕ} (hm : 1 ≤ m) (hmh : m ≤ h) : Real.exp (-C.k h) ≤ Real.exp (-C.k m)

theorem TrilinearHT.Auto.StaggerCell.S_exp_le {κ : LocalKernelClass} (C : StaggerCell κ) {v h : ℕ} (hv : 1 ≤ v) (hvh : v < h) : C.S v * Real.exp (-C.k h) ≤ Real.exp (-C.k h / 2)

S_v e^{-k_h} ≤ e^{-k_h/2} for v < h.

theorem TrilinearHT.Auto.StaggerCell.term_bound {κ : LocalKernelClass} (C : StaggerCell κ) {s s' : Fin 4} (hss : s ≠ s') {m : ℕ} (hm : 1 ≤ m) {A B : Option ℕ} (hA : Valid s m A) (hB : Valid s' m B) {z : Fin 4 → ℝ → ℂ} (hz : C.Spect z s s') : ‖C.H (slotPair z s s' (C.tv s A) (C.tv s' B)) - C.H (slotPair z s s' (C.f s) (C.f s'))‖ ≤ 2 * Real.exp (-C.k m)

Blueprint eq:stagger (line 1589): replacing any two valid terms in distinct slots by the actual inputs costs at most 2 e^{-k_m}.

theorem TrilinearHT.Auto.StaggerCell.diff4_bound {κ : LocalKernelClass} (C : StaggerCell κ) {s s' : Fin 4} (hss : s ≠ s') {z : Fin 4 → ℝ → ℂ} (hz : C.Spect z s s') {A₁ A₂ B₁ B₂ : ℝ → ℂ} (hA₁ : FinL2 C.a₀ C.r A₁) (hA₂ : FinL2 C.a₀ C.r A₂) (hB₁ : FinL2 C.a₀ C.r B₁) (hB₂ : FinL2 C.a₀ C.r B₂) (c : ℂ) {ε : ℝ} (h11 : ‖C.H (slotPair z s s' A₁ B₁) - c‖ ≤ ε) (h12 : ‖C.H (slotPair z s s' A₁ B₂) - c‖ ≤ ε) (h21 : ‖C.H (slotPair z s s' A₂ B₁) - c‖ ≤ ε) (h22 : ‖C.H (slotPair z s s' A₂ B₂) - c‖ ≤ ε) : ‖C.H (slotPair z s s' (A₁ - A₂) (B₁ - B₂))‖ ≤ 4 * ε

Expansion of a pair of differences around a common reference value.

theorem TrilinearHT.Auto.StaggerCell.diff2_bound {κ : LocalKernelClass} (C : StaggerCell κ) {s s' : Fin 4} {z : Fin 4 → ℝ → ℂ} (hz : C.Spect z s s') {V B₁ B₂ : ℝ → ℂ} (hV : FinL2 C.a₀ C.r V) (hB₁ : FinL2 C.a₀ C.r B₁) (hB₂ : FinL2 C.a₀ C.r B₂) (c : ℂ) {ε : ℝ} (h1 : ‖C.H (slotPair z s s' V B₁) - c‖ ≤ ε) (h2 : ‖C.H (slotPair z s s' V B₂) - c‖ ≤ ε) : ‖C.H (slotPair z s s' V (B₁ - B₂))‖ ≤ 2 * ε

def TrilinearHT.Auto.StaggerCell.LateRep {κ : LocalKernelClass} (C : StaggerCell κ) (l : Fin 4) (m : ℕ) (X : ℝ → ℂ) : Prop

A difference of two valid terms.

Equations

• C.LateRep l m X = ∃ (A₁ : Option ℕ) (A₂ : Option ℕ), TrilinearHT.Auto.StaggerCell.Valid l m A₁ ∧ TrilinearHT.Auto.StaggerCell.Valid l m A₂ ∧ X = C.tv l A₁ - C.tv l A₂

theorem TrilinearHT.Auto.StaggerCell.LateRep.mono {κ : LocalKernelClass} {C : StaggerCell κ} {l : Fin 4} {m m' : ℕ} (hm : m' ≤ m) {X : ℝ → ℂ} (h : C.LateRep l m X) : C.LateRep l m' X

theorem TrilinearHT.Auto.StaggerCell.late_pair {κ : LocalKernelClass} (C : StaggerCell κ) {s s' : Fin 4} (hss : s ≠ s') {m : ℕ} (hm : 1 ≤ m) {X Y : ℝ → ℂ} (hX : C.LateRep s m X) (hY : C.LateRep s' m Y) {z : Fin 4 → ℝ → ℂ} (hz : C.Spect z s s') : ‖C.H (slotPair z s s' X Y)‖ ≤ 8 * Real.exp (-C.k m)

Two late differences in distinct slots have pair norm at most 8 e^{-k_m}.

theorem TrilinearHT.Auto.StaggerCell.old_term_bound {κ : LocalKernelClass} (C : StaggerCell κ) {s s' : Fin 4} (hss : s ≠ s') {v m : ℕ} (hv : 1 ≤ v) (hvm : v < m) {B : Option ℕ} (hB : Valid s' m B) {z : Fin 4 → ℝ → ℂ} (hz : C.Spect z s s') : ‖C.H (slotPair z s s' (C.g v) (C.tv s' B)) - C.H (slotPair z s s' (C.g v) (C.f s'))‖ ≤ Real.exp (-C.k m / 2)

A bounded old projection against a late term: replacing the late term costs e^{-k_m/2}.

theorem TrilinearHT.Auto.StaggerCell.H_zero_left {κ : LocalKernelClass} (C : StaggerCell κ) {s s' : Fin 4} (hss : s ≠ s') (z : Fin 4 → ℝ → ℂ) (Y : ℝ → ℂ) : C.H (slotPair z s s' 0 Y) = 0

The tuple of the two earliest increments

noncomputable def TrilinearHT.Auto.StaggerCell.prevProj {κ : LocalKernelClass} (C : StaggerCell κ) (t : ℕ) : ℝ → ℂ

The previous value of the position updated at level t (zero before its first update).

Equations

• C.prevProj t = if t ≤ 4 then 0 else C.g (t - 4)

noncomputable def TrilinearHT.Auto.StaggerCell.incr {κ : LocalKernelClass} (C : StaggerCell κ) (t : ℕ) : ℝ → ℂ

The increment at level t.

Equations

• C.incr t = C.g t - C.prevProj t

def TrilinearHT.Auto.StaggerCell.lastLevel (l : Fin 4) (t : ℕ) : ℕ

The last update level of position l before level t.

Equations

• TrilinearHT.Auto.StaggerCell.lastLevel l t = t - (t + 4 - ↑l) % 4

theorem TrilinearHT.Auto.StaggerCell.stagPos_eq_iff (t : ℕ) (l : Fin 4) : stagPos t = l ↔ t % 4 = ↑l

theorem TrilinearHT.Auto.StaggerCell.lastLevel_spec {l : Fin 4} {t : ℕ} (hl : l ≠ stagPos t) (ht : 4 ≤ t) : stagPos (lastLevel l t) = l ∧ t - 3 ≤ lastLevel l t ∧ lastLevel l t < t

noncomputable def TrilinearHT.Auto.StaggerCell.lastProj {κ : LocalKernelClass} (C : StaggerCell κ) (l : Fin 4) (t : ℕ) : ℝ → ℂ

The current projection of position l after the updates of levels ≤ t (zero before its first update).

Equations

• C.lastProj l t = if 1 ≤ TrilinearHT.Auto.StaggerCell.lastLevel l t then C.g (TrilinearHT.Auto.StaggerCell.lastLevel l t) else 0

noncomputable def TrilinearHT.Auto.StaggerCell.tuple {κ : LocalKernelClass} (C : StaggerCell κ) (u t : ℕ) (l : Fin 4) : ℝ → ℂ

Blueprint eq:base-tuple (line 1583): X_i = g_u - g_{u-4}, X_j = g_t - g_{t-4} and X_e = F_e - g_{e,prev} in the remaining slots.

Equations

• C.tuple u t l = if l = TrilinearHT.Auto.stagPos u then C.incr u else if l = TrilinearHT.Auto.stagPos t then C.incr t else C.f l - C.lastProj l t

theorem TrilinearHT.Auto.StaggerCell.tuple_late_j {κ : LocalKernelClass} (C : StaggerCell κ) {u t : ℕ} (hut : stagPos u ≠ stagPos t) (ht : 5 ≤ t) : C.LateRep (stagPos t) (t - 4) (C.tuple u t (stagPos t))

theorem TrilinearHT.Auto.StaggerCell.tuple_late_other {κ : LocalKernelClass} (C : StaggerCell κ) {u t : ℕ} {l : Fin 4} (hlu : l ≠ stagPos u) (hlt : l ≠ stagPos t) (ht : 4 ≤ t) : C.LateRep l (t - 3) (C.tuple u t l)

theorem TrilinearHT.Auto.StaggerCell.tuple_late_i {κ : LocalKernelClass} (C : StaggerCell κ) {u t : ℕ} (hu : 5 ≤ u) : C.LateRep (stagPos u) (u - 4) (C.tuple u t (stagPos u))

theorem TrilinearHT.Auto.StaggerCell.tuple_i {κ : LocalKernelClass} (C : StaggerCell κ) (u t : ℕ) : C.tuple u t (stagPos u) = C.g u - C.prevProj u

theorem TrilinearHT.Auto.StaggerCell.early_pair {κ : LocalKernelClass} (C : StaggerCell κ) {s' : Fin 4} {u m : ℕ} (hu : 1 ≤ u) (hum : u < m) (hss : stagPos u ≠ s') {Y : ℝ → ℂ} (hY : C.LateRep s' m Y) {z : Fin 4 → ℝ → ℂ} (hz : C.Spect z (stagPos u) s') : ‖C.H (slotPair z (stagPos u) s' (C.g u - C.prevProj u) Y)‖ ≤ 4 * Real.exp (-C.k m / 2)

The early slot against a late difference (blueprint line 1596, case u < t - 4): each of its two old projections is tested directly.

theorem TrilinearHT.Auto.StaggerCell.tuple_pairSmall {κ : LocalKernelClass} (C : StaggerCell κ) {u t : ℕ} (ht : 12 ≤ t) (hu : 1 ≤ u) (hut : u < t) (hpos : stagPos u ≠ stagPos t) {s s' : Fin 4} (hss : s ≠ s') : PairSmall C.a₀ C.r C.w s s' (C.tuple u t s) (C.tuple u t s') (8 * Real.exp (-C.k (t - 7)))

Blueprint §11.2, line 1596: for t ≥ 12 and the two earliest increment levels u < t in distinct positions, every pair of full tuple arguments has bilinear norm at most 8 e^{-k_{t-7}}.

The expansion at a finite cutoff

noncomputable def TrilinearHT.Auto.StaggerCell.tail {κ : LocalKernelClass} (C : StaggerCell κ) (τ : ℕ) : Fin 4 → ℝ → ℂ

The terminal residuals F_p - (current projection) after the updates of levels ≤ τ.

Equations

• C.tail τ p = C.f p - C.lastProj p τ

theorem TrilinearHT.Auto.StaggerCell.lastLevel_self {τ : ℕ} {p : Fin 4} (h : stagPos τ = p) : lastLevel p τ = τ

theorem TrilinearHT.Auto.StaggerCell.lastLevel_pred_self {τ : ℕ} {p : Fin 4} (h : stagPos τ = p) : lastLevel p (τ - 1) = τ - 4

theorem TrilinearHT.Auto.StaggerCell.lastLevel_pred_other {τ : ℕ} (hτ : 1 ≤ τ) {p : Fin 4} (h : stagPos τ ≠ p) : lastLevel p (τ - 1) = lastLevel p τ

theorem TrilinearHT.Auto.StaggerCell.lastProj_zero {κ : LocalKernelClass} (C : StaggerCell κ) (p : Fin 4) : C.lastProj p 0 = 0

theorem TrilinearHT.Auto.StaggerCell.lastProj_self {κ : LocalKernelClass} (C : StaggerCell κ) {τ : ℕ} (hτ : 1 ≤ τ) : C.lastProj (stagPos τ) τ = C.g τ

theorem TrilinearHT.Auto.StaggerCell.lastProj_pred_self {κ : LocalKernelClass} (C : StaggerCell κ) (τ : ℕ) : C.lastProj (stagPos τ) (τ - 1) = C.prevProj τ

theorem TrilinearHT.Auto.StaggerCell.lastProj_pred_other {κ : LocalKernelClass} (C : StaggerCell κ) {τ : ℕ} (hτ : 1 ≤ τ) {p : Fin 4} (h : stagPos τ ≠ p) : C.lastProj p (τ - 1) = C.lastProj p τ

theorem TrilinearHT.Auto.StaggerCell.finL2_lastProj {κ : LocalKernelClass} (C : StaggerCell κ) (p : Fin 4) (τ : ℕ) : FinL2 C.a₀ C.r (C.lastProj p τ)

theorem TrilinearHT.Auto.StaggerCell.finL2_prevProj {κ : LocalKernelClass} (C : StaggerCell κ) (τ : ℕ) : FinL2 C.a₀ C.r (C.prevProj τ)

theorem TrilinearHT.Auto.StaggerCell.finL2_incr {κ : LocalKernelClass} (C : StaggerCell κ) (τ : ℕ) : FinL2 C.a₀ C.r (C.incr τ)

theorem TrilinearHT.Auto.StaggerCell.finL2_tail {κ : LocalKernelClass} (C : StaggerCell κ) (τ : ℕ) (p : Fin 4) : FinL2 C.a₀ C.r (C.tail τ p)

theorem TrilinearHT.Auto.StaggerCell.tail_zero {κ : LocalKernelClass} (C : StaggerCell κ) : C.tail 0 = C.f

theorem TrilinearHT.Auto.StaggerCell.tail_pred {κ : LocalKernelClass} (C : StaggerCell κ) {τ : ℕ} (hτ : 1 ≤ τ) : C.tail (τ - 1) = Function.update (C.tail τ) (stagPos τ) (C.incr τ + C.tail τ (stagPos τ))

theorem TrilinearHT.Auto.StaggerCell.H_update_add {κ : LocalKernelClass} (C : StaggerCell κ) {W : Fin 4 → ℝ → ℂ} (hW : ∀ (l : Fin 4), FinL2 C.a₀ C.r (W l)) (p : Fin 4) {A B : ℝ → ℂ} (hA : FinL2 C.a₀ C.r A) (hB : FinL2 C.a₀ C.r B) : C.H (Function.update W p (A + B)) = C.H (Function.update W p A) + C.H (Function.update W p B)

theorem TrilinearHT.Auto.StaggerCell.expansion_first {κ : LocalKernelClass} (C : StaggerCell κ) (T : ℕ) : C.H C.f = C.H (C.tail T) + ∑ τ ∈ Finset.Icc 1 T, C.H (Function.update (C.tail τ) (stagPos τ) (C.incr τ))

First increment decomposition: telescoping over the levels in time order.

noncomputable def TrilinearHT.Auto.StaggerCell.W {κ : LocalKernelClass} (C : StaggerCell κ) (u τ : ℕ) : Fin 4 → ℝ → ℂ

The inputs after the first increment u has been fixed in its slot.

Equations

• C.W u τ = Function.update (C.tail τ) (TrilinearHT.Auto.stagPos u) (C.incr u)

theorem TrilinearHT.Auto.StaggerCell.finL2_W {κ : LocalKernelClass} (C : StaggerCell κ) (u τ : ℕ) (l : Fin 4) : FinL2 C.a₀ C.r (C.W u τ l)

theorem TrilinearHT.Auto.StaggerCell.W_update_eq_tuple {κ : LocalKernelClass} (C : StaggerCell κ) {u τ : ℕ} (h : stagPos τ ≠ stagPos u) : Function.update (C.W u τ) (stagPos τ) (C.incr τ) = C.tuple u τ

theorem TrilinearHT.Auto.StaggerCell.W_step {κ : LocalKernelClass} (C : StaggerCell κ) {u τ : ℕ} (hτ : 1 ≤ τ) : C.H (C.W u (τ - 1)) = C.H (C.W u τ) + if stagPos τ ≠ stagPos u then C.H (C.tuple u τ) else 0

theorem TrilinearHT.Auto.StaggerCell.expansion_second {κ : LocalKernelClass} (C : StaggerCell κ) (u T : ℕ) : u ≤ T → C.H (C.W u u) = C.H (C.W u T) + ∑ t ∈ Finset.Ioc u T, if stagPos t ≠ stagPos u then C.H (C.tuple u t) else 0

Second increment decomposition with the first increment fixed.

theorem TrilinearHT.Auto.StaggerCell.expansion {κ : LocalKernelClass} (C : StaggerCell κ) (T : ℕ) : C.H C.f = C.H (C.tail T) + ∑ u ∈ Finset.Icc 1 T, (C.H (Function.update (C.tail T) (stagPos u) (C.incr u)) + ∑ t ∈ Finset.Ioc u T, if stagPos t ≠ stagPos u then C.H (C.tuple u t) else 0)

Blueprint §11.2, line 1587: at a finite cutoff T the expansion of every input into its increments and terminal residual groups exactly into the tuples eq:base-tuple of the two earliest increments u < t (distinct positions), the terms with a single increment, and the term with four terminal residuals.

Sizes and remainders

theorem TrilinearHT.Auto.StaggerCell.f_L2 {κ : LocalKernelClass} (C : StaggerCell κ) (p : Fin 4) : MeasureTheory.eLpNorm (C.f p) 2 C.μ ≤ 1

theorem TrilinearHT.Auto.StaggerCell.lastProj_L2 {κ : LocalKernelClass} (C : StaggerCell κ) (p : Fin 4) (τ : ℕ) : MeasureTheory.eLpNorm (C.lastProj p τ) 2 C.μ ≤ 1

theorem TrilinearHT.Auto.StaggerCell.prevProj_L2 {κ : LocalKernelClass} (C : StaggerCell κ) (τ : ℕ) : MeasureTheory.eLpNorm (C.prevProj τ) 2 C.μ ≤ 1

theorem TrilinearHT.Auto.StaggerCell.sub_L2_le {κ : LocalKernelClass} (C : StaggerCell κ) {X Y : ℝ → ℂ} (hX : MeasureTheory.eLpNorm X 2 C.μ ≤ 1) (hY : MeasureTheory.eLpNorm Y 2 C.μ ≤ 1) : MeasureTheory.eLpNorm (X - Y) 2 C.μ ≤ 2

theorem TrilinearHT.Auto.StaggerCell.incr_L2 {κ : LocalKernelClass} (C : StaggerCell κ) (τ : ℕ) : MeasureTheory.eLpNorm (C.incr τ) 2 C.μ ≤ 2

theorem TrilinearHT.Auto.StaggerCell.tail_L2 {κ : LocalKernelClass} (C : StaggerCell κ) (τ : ℕ) (p : Fin 4) : MeasureTheory.eLpNorm (C.tail τ p) 2 C.μ ≤ 2

theorem TrilinearHT.Auto.StaggerCell.tuple_L2 {κ : LocalKernelClass} (C : StaggerCell κ) (u t : ℕ) (l : Fin 4) : MeasureTheory.eLpNorm (C.tuple u t l) 2 C.μ ≤ 2

Blueprint line 1596: all tuple factors have bounded normalized L² norm.

theorem TrilinearHT.Auto.StaggerCell.H_update_smul_self {κ : LocalKernelClass} (C : StaggerCell κ) (F : Fin 4 → ℝ → ℂ) (l : Fin 4) (c : ℂ) : C.H (Function.update F l (c • F l)) = c * C.H F

theorem TrilinearHT.Auto.StaggerCell.pairSmall_scaled {κ : LocalKernelClass} (C : StaggerCell κ) {p p' : Fin 4} (hpp : p ≠ p') {X Y : ℝ → ℂ} {η : ℝ} (h : PairSmall C.a₀ C.r C.w p p' X Y η) {F : Fin 4 → ℝ → ℂ} (hF : ∀ (l : Fin 4), Measurable (F l)) {c : ℝ} (hc : 0 < c) (hFc : ∀ (l : Fin 4), l ≠ p → l ≠ p' → MeasureTheory.eLpNorm (F l) 2 C.μ ≤ ENNReal.ofReal c) : ‖C.H (slotPair F p p' X Y)‖ ≤ c ^ 2 * η

A pair estimate against spectators of normalized size at most c.

theorem TrilinearHT.Auto.StaggerCell.tail_late {κ : LocalKernelClass} (C : StaggerCell κ) {T : ℕ} (hT : 4 ≤ T) (p : Fin 4) : C.LateRep p (T - 3) (C.tail T p)

theorem TrilinearHT.Auto.StaggerCell.slotPair_self (F : Fin 4 → ℝ → ℂ) (p p' : Fin 4) : slotPair F p p' (F p) (F p') = F

theorem TrilinearHT.Auto.StaggerCell.exists_two_ne (p : Fin 4) : ∃ (a : Fin 4) (b : Fin 4), a ≠ b ∧ a ≠ p ∧ b ≠ p

theorem TrilinearHT.Auto.StaggerCell.remainder_four {κ : LocalKernelClass} (C : StaggerCell κ) {T : ℕ} (hT : 4 ≤ T) : ‖C.H (C.tail T)‖ ≤ 4 * (8 * Real.exp (-C.k (T - 3)))

Blueprint line 1594: the term with four terminal residuals tends to zero.

theorem TrilinearHT.Auto.StaggerCell.remainder_one {κ : LocalKernelClass} (C : StaggerCell κ) {T : ℕ} (hT : 4 ≤ T) (u : ℕ) : ‖C.H (Function.update (C.tail T) (stagPos u) (C.incr u))‖ ≤ 4 * (8 * Real.exp (-C.k (T - 3)))

Blueprint line 1587: each term with a single increment and three terminal residuals tends to zero.

The accuracy schedule and the declaration stagger

def TrilinearHT.Auto.stagAcc (k₁ A t : ℕ) : ℕ

The accuracies k_t = k_1^{A^{t-1}}, so that k_{t+1} = k_t^A.

Equations

• TrilinearHT.Auto.stagAcc k₁ A t = k₁ ^ A ^ (t - 1)

theorem TrilinearHT.Auto.stagAcc_pow {k₁ A v h : ℕ} (hv : 1 ≤ v) (hvh : v ≤ h) : stagAcc k₁ A h = stagAcc k₁ A v ^ A ^ (h - v)

theorem TrilinearHT.Auto.le_stagAcc {k₁ A : ℕ} (hk : 1 ≤ k₁) (hA : 1 ≤ A) (t : ℕ) : k₁ ≤ stagAcc k₁ A t

theorem TrilinearHT.Auto.stagAcc_grow {k₁ A v h : ℕ} (hk : 1 ≤ k₁) (hA : 1 ≤ A) (hv : 1 ≤ v) (hvh : v < h) : stagAcc k₁ A v ^ A ≤ stagAcc k₁ A h

theorem TrilinearHT.Auto.sqrt_seventeen_le_exp_two : √17 ≤ Real.exp 2

theorem TrilinearHT.Auto.budget_le_exp {Cq : ℝ} (hCq : 0 < Cq) {C x : ℕ} (hx : 16 ≤ x) (hxC : 4 * Cq * 2 ^ C ≤ ↑x) : √17 * fitBudget Cq C x ≤ Real.exp (↑x ^ (C + 1) / 2)

The supremum bound √17 · B_k is at most exp(k^{C+1}/2) for large k.

theorem TrilinearHT.Auto.eight_exp_le {y : ℝ} (hy : 16 ≤ y) : 8 * Real.exp (-y) ≤ Real.exp (-2 * √y)

8 e^{-y} ≤ e^{-2 √y} for y ≥ 16.

theorem TrilinearHT.Auto.PairSmall.mono {a₀ r : ℝ} {w : ℝ × ℝ → ℂ} {p p' : Fin 4} {X Y : ℝ → ℂ} {η η' : ℝ} (h : PairSmall a₀ r w p p' X Y η) (hη : η ≤ η') : PairSmall a₀ r w p p' X Y η'

theorem TrilinearHT.Auto.eLpNorm_fit_le {G : RealDyadicGrid} {I : ℤ × ℤ} {g : ℝ → ℂ} (hg : Measurable g) {S : ℝ} (hS : ∀ (y : ℝ), ‖g y‖ ≤ S) (h : ∫ (y : ℝ) in dyadicGridCell G I.1 I.2, ‖g y‖ ^ 2 ≤ dyadicGridLength G I.1) : MeasureTheory.eLpNorm g 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≤ 1

The normalized L² norm of a fit is at most one.

theorem TrilinearHT.Auto.PathColumnSystem.scalar_measurable {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) (R : ℤ × ℤ) (v : V) : Measurable (P.scalar R v)

theorem TrilinearHT.Auto.PathColumnSystem.leaf_tree {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {y : ℝ} (hy : y ∈ dyadicGridCell G J.1 J.2) : pathLeaf G J N y ∈ dyadicFiniteTree G J N

theorem TrilinearHT.Auto.PathColumnSystem.scalar_eq {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) {R c : ℤ × ℤ} (hc : c ∈ dyadicFiniteTree G J N) (hcR : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G R.1 R.2) {v : V} (hv : v ∈ P.avail c) {y : ℝ} (hy : y ∈ dyadicGridCell G c.1 c.2) : P.scalar R v y = P.scalarAt c v y

On a tree cell, the leaf-read scalar is the cellwise scalar of an available label.

noncomputable def TrilinearHT.Auto.PathColumnSystem.rooted {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) (R : ℤ × ℤ) : ColumnTreeData V

The column tree data rooted at a tree cell R, all labels born at R.

Equations

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

noncomputable def TrilinearHT.Auto.PathColumnSystem.mask {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) (R : ℤ × ℤ) (hR : R ∈ dyadicFiniteTree G J N) : InheritedColumnMask (P.rooted R)

The inherited mask of a rooted system.

Equations

• P.mask R hR = { labels := P.avail, available := ⋯, inherited := ⋯ }

noncomputable def TrilinearHT.Auto.PathColumnSystem.family {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) (R : ℤ × ℤ) (hR : R ∈ dyadicFiniteTree G J N) : ColumnDepthFamily V

The system rooted at R as a column depth family down to the leaves.

Equations

• P.family R hR = { D := P.rooted R, A := P.mask R hR, N := J.1 + ↑N, root_le := ⋯, complete := ⋯ }

theorem TrilinearHT.Auto.PathColumnSystem.column_memLp {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) (c : ℤ × ℤ) (v : V) : MeasureTheory.MemLp ((dyadicGridCell G c.1 c.2).indicator (privateColumnValue (P.scalarAt c) P.weight v)) 2 MeasureTheory.volume

noncomputable def TrilinearHT.Auto.PathColumnSystem.column {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) (c : ℤ × ℤ) (v : V) : ↥(ColumnL2 V)

The column 1_c (φ_v, √ε_v e_v) of the system at the cell c.

Equations

• P.column c v = MeasureTheory.MemLp.toLp ((TrilinearHT.Auto.dyadicGridCell G c.1 c.2).indicator (TrilinearHT.Auto.privateColumnValue (P.scalarAt c) P.weight v)) ⋯

noncomputable def TrilinearHT.Auto.PathColumnSystem.range {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) (c : ℤ × ℤ) : Submodule ℂ ↥(ColumnL2 V)

The range of the available columns at c.

Equations

• P.range c = Submodule.span ℂ (P.column c '' ↑(P.avail c))

instance TrilinearHT.Auto.PathColumnSystem.instFiniteDimensionalComplexSubtypeAEEqFunRealColumnHilbertVolumeMemAddSubgroupColumnL2SubmoduleRange {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) (c : ℤ × ℤ) : FiniteDimensional ℂ ↥(P.range c)

noncomputable def TrilinearHT.Auto.PathColumnSystem.proj {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) (c : ℤ × ℤ) : ↥(ColumnL2 V) →L[ℂ] ↥(ColumnL2 V)

The cell projection of the system.

Equations

• P.proj c = (P.range c).starProjection

theorem TrilinearHT.Auto.PathColumnSystem.rooted_proj {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) {R c : ℤ × ℤ} (hR : R ∈ dyadicFiniteTree G J N) (hc : c ∈ (P.rooted R).cells) : cellColumnProjection (P.rooted R) (P.mask R hR) hc = P.proj c

The rooted cell projections are the root-independent system projections.

theorem TrilinearHT.Auto.ColumnDepthFamily.delayed_admissible {V : Type u_1} [Fintype V] (Ψ : ColumnDepthFamily V) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (K₀ : ℕ) : IsAdmissibleOpponent Ψ.D.grid Ψ.D.root (↑↑f) (Ψ.delayed f K₀) (2 * (compressionOneConst Ψ.D + ↑K₀))

The delayed opponent is the current projection plus a rolling square-energy sequence, hence admissible (blueprint lem:delay, line 1565; prop:base, line 1632).

theorem TrilinearHT.Auto.PathColumnSystem.scalar_root {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) {R : ℤ × ℤ} (hR : R ∈ dyadicFiniteTree G J N) {v : V} (hv : v ∈ P.avail R) (y : ℝ) : P.scalar R v y = P.scalarAt R v y

An available label's rooted scalar is the cellwise scalar at the root, everywhere.

def TrilinearHT.Auto.ColData {V : Type} (sc : V → ℝ → ℂ) (wt : V → ℝ) : Prop

Scalars bounded by one and weights in [0, 1] for all labels.

Equations

• TrilinearHT.Auto.ColData sc wt = ∀ (v : V), Measurable (sc v) ∧ (∀ (y : ℝ), ‖sc v y‖ ≤ 1) ∧ 0 ≤ wt v ∧ wt v ≤ 1

noncomputable def TrilinearHT.Auto.stagTuple (f : Fin 4 → ℝ → ℂ) (g : ℕ → ℤ × ℤ → ℝ → ℂ) (u t : ℕ) (I : ℤ × ℤ) (l : Fin 4) : ℝ → ℂ

The tuple eq:base-tuple of the two earliest increments at a cell, from the stagger fits.

Equations

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

theorem TrilinearHT.Auto.StaggerCell.tuple_eq_stagTuple {κ : LocalKernelClass} (D : StaggerCell κ) {f : Fin 4 → ℝ → ℂ} {g : ℕ → ℤ × ℤ → ℝ → ℂ} {I : ℤ × ℤ} (hf : D.f = f) (hg : ∀ (t : ℕ), D.g t = g t I) (u t : ℕ) : D.tuple u t = stagTuple f g u t I

theorem TrilinearHT.Auto.fitOpponentConst_mono {M M' : ℕ} (h : M ≤ M') : fitOpponentConst M ≤ fitOpponentConst M'

theorem TrilinearHT.Auto.err_mono_real {c c' e T K xa xa' xb xb' Cga Cga' Cgb Cgb' : ℝ} (hc : 0 ≤ c) (hcc : c ≤ c') (he : 0 ≤ e) (hT : 0 ≤ T) (hK : 0 ≤ K) (hxa : 0 ≤ xa) (hxb : 0 ≤ xb) (ha : xa ≤ xa') (hb : xb ≤ xb') (hCga : 0 ≤ Cga) (hCgb : 0 ≤ Cgb) (hCa : Cga ≤ Cga') (hCb : Cgb ≤ Cgb') : c * ((2 * e * (2 * (xa + K) + 1) + T) * (2 * (1 + Cgb) + 4) + (2 * e * (2 * (xb + K) + 1) + T) * (2 * (2 * (xa + K) + Cga) + 4)) ≤ c' * ((2 * e * (2 * (xa' + K) + 1) + T) * (2 * (1 + Cgb') + 4) + (2 * e * (2 * (xb' + K) + 1) + T) * (2 * (2 * (xa' + K) + Cga') + 4))

theorem TrilinearHT.Auto.StaggerCell.lastLevel_spec' {l : Fin 4} {t : ℕ} (hl : l ≠ stagPos t) (ht : 1 ≤ t) : lastLevel l t < t ∧ (1 ≤ lastLevel l t → stagPos (lastLevel l t) = l)

The last update level of a slot other than the current one, for every t ≥ 1: it is below t, and when it is positive it is a level of that slot.

theorem TrilinearHT.Auto.isAdmissibleOpponent_of_ae_zero {G : RealDyadicGrid} {J : ℤ × ℤ} {F : ℝ → ℂ} {z : ℤ × ℤ → ℝ → ℂ} (hz : ∀ (I : ℤ × ℤ), ∀ᵐ (y : ℝ), z I y = 0) (K : ℝ) : IsAdmissibleOpponent G J F z K

An a.e. zero opponent is admissible with any nonnegative constant.

theorem TrilinearHT.Auto.hasDepthEnergy_of_ae_zero {G : RealDyadicGrid} {J : ℤ × ℤ} {F : ℝ → ℂ} {z : ℤ × ℤ → ℝ → ℂ} (hz : ∀ (I : ℤ × ℤ), ∀ᵐ (y : ℝ), z I y = 0) : HasDepthEnergy G J F z 1

An a.e. zero opponent has depth energy with constant one.