Section 11.2, part 2b: prop:base, low pairs and accurate high fits

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 2b: prop:base, low pairs and accurate high fits (proof lines 1626-1641) (lines 1598-1666) of blueprint/formalization_blueprint.tex.

def TrilinearHT.Auto.IsFitOpponent (G : RealDyadicGrid) (J : ℤ × ℤ) (N : ℕ) (f : ℝ → ℂ) (roots : Finset (ℤ × ℤ)) (seg : ℤ × ℤ → ℤ × ℤ) (g : ℤ × ℤ → ℝ → ℂ) (C Bd : ℝ) (c : ℕ) (Hc : ℝ) : Prop

The adaptive fits as opponents (blueprint prop:base, line 1630, and lem:compression): for each attempt root K there is one opponent, equal to the fit on the cells of the segment of K, which is admissible with depth energy one on every tree cell below K; it is the physical part of the current projections g_I = P_I F of a column depth family rooted at K applied to the input F = 1_J f (blueprint line 1570), whose column budget (eq:columnbudget: inverse square-root private weights, path counts and column bounds) is at most Bd and whose columns available on a tree cell below K are bounded quadratic chart atoms of order c and complexity at most Hc on that cell (the fit atoms, line 1575).

Equations

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

theorem TrilinearHT.Auto.FitSetup.compressionOneConst_treeData {S : FitSetup} (K R : ℤ × ℤ) : compressionOneConst (S.treeData K R) = fitOpponentConst S.M

theorem TrilinearHT.Auto.FitSetup.Hyp.isFitOpponent {S : FitSetup} (h : S.Hyp) : IsFitOpponent S.G S.J S.N S.f S.roots S.seg S.g (fitOpponentConst S.M) (max 2 ↑S.M) S.c₂ S.B

theorem TrilinearHT.Auto.inheritedAdaptiveFit (κ : LocalKernelClass) : ∃ (c₂ : ℕ) (C : ℕ), 1 ≤ c₂ ∧ 1 ≤ C ∧ ∀ (q : ℝ), 2 < q → ∃ (Cq : ℝ), 0 < Cq ∧ ∀ (G : RealDyadicGrid) (J : ℤ × ℤ) (N : ℕ) (w : ℤ × ℤ → ℝ × ℝ → ℂ), (∀ (I : ℤ × ℤ), IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) → ∀ (j : Fin 4) {f : ℝ → ℂ}, Measurable f → (∀ I ∈ dyadicFiniteTree G J N, I = J ∨ kernelHull G J N w I → MeasureTheory.eLpNorm f (ENNReal.ofReal q) (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≤ 1) → ∀ {k : ℕ}, 1 ≤ k → ∃ (M : ℕ) (roots : Finset (ℤ × ℤ)) (seg : ℤ × ℤ → ℤ × ℤ) (n : ℤ × ℤ → ℕ) (a : ℤ × ℤ → ℕ → ℝ → ℂ) (g : ℤ × ℤ → ℝ → ℂ) (cnt : ℤ × ℤ → ℤ × ℤ → ℕ) (atm : ℤ × ℤ → ℤ × ℤ → ℕ → ℝ → ℂ), IsAdaptiveFit c₂ (fitBudget Cq C k) G J N w j q f k M roots seg n a g ∧ IsAttemptData c₂ (fitBudget Cq C k) G J N M roots seg n a cnt atm ∧ IsFitOpponent G J N f roots seg g (fitOpponentConst M) (max 2 ↑M) c₂ (fitBudget Cq C k)

Blueprint §11.2, Declaration adaptive-fit (THT.Base.inheritedAdaptiveFit, lines 1567-1579). For accuracy e^{-k} and an input normalized by ‖f‖_{q,I} ≤ 1 on every cell I of the complete finite tree of depth N below the root J (the normalization of sec:reduction, line 418), there are restarted segments (roots with total length at most 4/3 |J|) and inherited lists of at most M ≤ 17 B² bounded chart atoms of complexity budget B = exp(C_q (1 + log 2 + k)^C), extending along each segment, whose fitted combinations g_I (coefficient ℓ² norm at most one, hence |g_I| ≤ √M and ‖g_I‖_{2,I} ≤ 1) leave a small residual: d_{j,I}(f - g_I) ≤ e^{-k} on every cell.

theorem TrilinearHT.Auto.twoEarliestIncrements (κ : LocalKernelClass) : ∃ (c₂ : ℕ) (C : ℕ) (A : ℕ) (θ₀ : ℝ), 1 ≤ c₂ ∧ 1 ≤ C ∧ 2 ≤ A ∧ 0 < θ₀ ∧ θ₀ ≤ 1 ∧ ∀ (q : ℝ), 2 < q → ∃ (Cq : ℝ) (K₁ : ℕ), 0 < Cq ∧ ∀ (k₁ : ℕ), K₁ ≤ k₁ → ∀ (G : RealDyadicGrid) (J : ℤ × ℤ) (N : ℕ) (w : ℤ × ℤ → ℝ × ℝ → ℂ), (∀ (I : ℤ × ℤ), IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) → ∀ (f : Fin 4 → ℝ → ℂ), (∀ (p : Fin 4), Measurable (f p)) → (∀ (p : Fin 4), ∀ I ∈ dyadicFiniteTree G J N, I = J ∨ kernelHull G J N w I → MeasureTheory.eLpNorm (f p) (ENNReal.ofReal q) (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≤ 1) → ∃ (M : ℕ → ℕ) (roots : ℕ → Finset (ℤ × ℤ)) (seg : ℕ → ℤ × ℤ → ℤ × ℤ) (n : ℕ → ℤ × ℤ → ℕ) (a : ℕ → ℤ × ℤ → ℕ → ℝ → ℂ) (g : ℕ → ℤ × ℤ → ℝ → ℂ) (cnt : ℕ → ℤ × ℤ → ℤ × ℤ → ℕ) (atm : ℕ → ℤ × ℤ → ℤ × ℤ → ℕ → ℝ → ℂ), (∀ (t : ℕ), IsAdaptiveFit c₂ (fitBudget Cq C (stagAcc k₁ A t)) G J N w (stagPos t) q (f (stagPos t)) (stagAcc k₁ A t) (M t) (roots t) (seg t) (n t) (a t) (g t) ∧ IsAttemptData c₂ (fitBudget Cq C (stagAcc k₁ A t)) G J N (M t) (roots t) (seg t) (n t) (a t) (cnt t) (atm t) ∧ IsFitOpponent G J N (f (stagPos t)) (roots t) (seg t) (g t) (fitOpponentConst (M t)) (max 2 ↑(M t)) c₂ (fitBudget Cq C (stagAcc k₁ A t))) ∧ (∀ (L : Finset ℕ), dyadicRootLength G (L.biUnion roots) ≤ ↑L.card * (4 / 3 * dyadicGridLength G J.1)) ∧ ∀ I ∈ dyadicFiniteTree G J N, kernelHull G J N w I → ∃ (D : StaggerCell κ), D.a₀ = dyadicGridLeft G I.1 I.2 ∧ D.r = dyadicGridLength G I.1 ∧ D.w = w I ∧ D.q = q ∧ D.f = f ∧ (∀ (t : ℕ), D.g t = g t I) ∧ (∀ (t : ℕ), D.k t = ↑(stagAcc k₁ A t)) ∧ (∀ (u t : ℕ), 12 ≤ t → 1 ≤ u → u < t → stagPos u ≠ stagPos t → ⋯) ∧ (∀ (T : ℕ), D.H D.f = D.H (D.tail T) + ∑ u ∈ Finset.Icc 1 T, ⋯) ∧ (∀ (T : ℕ), 4 ≤ T → ⋯ ∧ ⋯) ∧ ∀ (u t : ℕ) (l : Fin 4), ⋯ ≤ 2

Blueprint §11.2, Declaration stagger (THT.Base.twoEarliestIncrements, lines 1581-1598). Update the four positions cyclically by the adaptive fits at accuracies k_t = k_1^{A^{t-1}}. On every tree cell the update data form a StaggerCell, so eq:stagger holds (StaggerCell.term_bound), the expansion at every finite cutoff groups exactly into the tuples eq:base-tuple of the two earliest increments (StaggerCell.expansion) with remainders tending to zero (StaggerCell.remainder_four, StaggerCell.remainder_one), all tuple factors have normalized L² norm at most 2, and for t ≥ 12 every pair of full tuple arguments has bilinear norm at most e^{-2 k_t^{θ₀}}. Unions of finitely many level segment families have total root length at most their number times 4/3 |J|.

theorem TrilinearHT.Auto.predictorDelay_group (κ : LocalKernelClass) {d e : ℕ} {A : QuadraticChartData d} {A' : QuadraticChartData e} {a i k b : Fin 4} (hai : a ≠ i) (hak : a ≠ k) (hab : a ≠ b) (hik : i ≠ k) (hib : i ≠ b) (hkb : k ≠ b) {B Dl ε : ℝ} {ι : Type} {L : Finset ι} {ψa ψb : ι → QuadraticChartData (d + e)} {lam : ι → ℝ} {coef : ι → ℝ → ℂ} (hP : PredictorApprox κ A A' a i k b B L ψa ψb lam coef) (hDl : 0 ≤ Dl) (hcard : ↑L.card ≤ Dl) (hcoef : ∀ (r : ℝ), ∑ ℓ ∈ L, ‖coef ℓ r‖ ≤ Dl) (hlam : ∀ (ℓ : ι) (r : ℝ), coef ℓ r ≠ 0 → |lam ℓ| * r ^ 2 ≤ Dl) (hbdd : ∀ ℓ ∈ L, IsBoundedQuadraticChart (ψa ℓ) ∧ IsBoundedQuadraticChart (ψb ℓ)) {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) {J' : ℤ × ℤ} (hJ' : J' ∈ dyadicFiniteTree G J N) (p : ι → V) (hp : ∀ ℓ ∈ L, p ℓ ∈ P.avail J') (hscal : ∀ ℓ ∈ L, ∀ (y : ℝ), P.scalarAt J' (p ℓ) y = (starRingEnd ℂ) (quadraticChartAtom (ψa ℓ) y)) (hε : ∀ ℓ ∈ L, P.weight (p ℓ) ≤ ε) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (K₀ : ℕ) (S' : Finset (ℤ × ℤ)) (hS' : ∀ I ∈ S', I ∈ pathBelow G J N J') (hK₀ : ∀ I ∈ S', I.1 + ↑K₀ ≤ J.1 + ↑N) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (hw : ∀ I ∈ S', IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) {Fb : ℝ → ℂ} {zb : ℤ × ℤ → ℝ → ℂ} {Kb : ℝ} (hKb : 0 ≤ Kb) (hzb : IsAdmissibleOpponent G J' Fb zb Kb) (hzbd : HasDepthEnergy G J' Fb zb Kb) (hzbm : ∀ (I : ℤ × ℤ), Measurable (zb I)) (hzb2 : ∀ (I : ℤ × ℤ), MeasureTheory.MemLp (zb I) 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) (c : ℤ × ℤ → ℂ) (hc : ∀ (I : ℤ × ℤ), ‖c I‖ ≤ 1) : ∑ I ∈ S', dyadicGridLength G I.1 * (‖c I‖ * ‖localProgressionForm (dyadicGridLength G I.1) (w I) (slots4 a i k (↑↑f) (quadraticChartAtom A) (quadraticChartAtom A') (zb I)) - localProgressionForm (dyadicGridLength G I.1) (w I) (slots4 a i k ((P.family J' hJ').delayed f K₀ I) (quadraticChartAtom A) (quadraticChartAtom A') (zb I))‖) ≤ (2 * Real.exp (-B) * (2 * (compressionOneConst (P.rooted J') + ↑K₀) + 1) * Kb + Dl ^ 2 * (delayConst κ * (2⁻¹ ^ K₀ + (1 + ↑K₀) * √ε) * (1 + Dl) ^ 4 * Kb)) * √(∫ (y : ℝ) in dyadicGridCell G J'.1 J'.2, ‖↑↑f y‖ ^ 2) * √(∫ (y : ℝ) in dyadicGridCell G J'.1 J'.2, ‖Fb y‖ ^ 2)

Blueprint prop:base, proof lines 1626-1632, for one low pair: apply the predictor approximation on both sides of the delayed replacement of the input in slot a (with the high system rooted at the pair's joint birth cell J'), and lem:delay to each predictor. The absolute scale sum of the replacement error, with cell coefficients of modulus at most one, is controlled by the energies on J'.

theorem TrilinearHT.Auto.PathColumnSystem.family_proj_ae {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) {R Q : ℤ × ℤ} (hR : R ∈ dyadicFiniteTree G J N) (h : ℤ) (hQ : Q ∈ ((P.family R hR).partition h).cells) (z : ↥(ColumnL2 V)) : ↑↑(((P.family R hR).proj h) z) =ᵐ[MeasureTheory.volume.restrict (dyadicGridCell G Q.1 Q.2)] ↑↑((P.proj Q) z)

On a partition cell, the depth projection of any rooted family is the system projection.

theorem TrilinearHT.Auto.PathColumnSystem.delayed_ae {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) {R R' I : ℤ × ℤ} (hR : R ∈ dyadicFiniteTree G J N) (hR' : R' ∈ dyadicFiniteTree G J N) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (K₀ : ℕ) (hIR : I ∈ pathBelow G J N R) (hIR' : I ∈ pathBelow G J N R') (hK₀ : I.1 + ↑K₀ ≤ J.1 + ↑N) : ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → (P.family R hR).delayed f K₀ I y = (P.family R' hR').delayed f K₀ I y

Delayed opponents of two rooted families agree a.e. on common cells.

structure TrilinearHT.Auto.LowList (G : RealDyadicGrid) (J : ℤ × ℤ) (N : ℕ) (R : ℤ × ℤ) (c₀ : ℕ) (H : ℝ) : Type 1

A low list on the tree below R (blueprint prop:base, lines 1626-1630): cellwise coefficients of modulus at most one on labels available at the cell, availability inherited along paths, and atoms given by bounded charts fixed below canonical birth cells (each label's birth cells along different paths are equal or disjoint).

• Λ : Type

  Finite label type for the low-argument catalog.

• fin : Fintype self.Λ
• coef : ℤ × ℤ → self.Λ → ℂ

  Cell-dependent coefficient of each low catalog atom.

• coef_le (I : ℤ × ℤ) (l : self.Λ) : ‖self.coef I l‖ ≤ 1
• avail : ℤ × ℤ → self.Λ → Prop

  Predicate recording which low catalog labels are available at a cell.

• coef_avail (I : ℤ × ℤ) (l : self.Λ) : self.coef I l ≠ 0 → self.avail I l
• avail_mono (c d : ℤ × ℤ) (l : self.Λ) : c ∈ dyadicFiniteTree G J N → d ∈ dyadicFiniteTree G J N → dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2 → self.avail d l → self.avail c l
• birth : ℤ × ℤ → self.Λ → ℤ × ℤ

  Birth cell of a catalog label as viewed from the current cell.

• dim : ℤ × ℤ → self.Λ → ℕ

  Dimension of the quadratic chart assigned at a birth cell.

• chart (K : ℤ × ℤ) (l : self.Λ) : QuadraticChartData (self.dim K l)

  Quadratic chart realizing the catalog atom at its birth cell.

• birth_spec (I : ℤ × ℤ) (l : self.Λ) : self.avail I l → dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G (self.birth I l).1 (self.birth I l).2 ∧ self.birth I l ∈ dyadicFiniteTree G J N ∧ dyadicGridCell G (self.birth I l).1 (self.birth I l).2 ⊆ dyadicGridCell G R.1 R.2
• avail_birth (I : ℤ × ℤ) (l : self.Λ) : self.avail I l → self.avail (self.birth I l) l
• birth_canon' (I₁ I₂ : ℤ × ℤ) (l : self.Λ) : self.avail I₁ l → self.avail I₂ l → ¬Disjoint (dyadicGridCell G (self.birth I₁ l).1 (self.birth I₁ l).2) (dyadicGridCell G (self.birth I₂ l).1 (self.birth I₂ l).2) → self.birth I₁ l = self.birth I₂ l
• one_le_dim (K : ℤ × ℤ) (l : self.Λ) : 1 ≤ self.dim K l
• complexity (K : ℤ × ℤ) (l : self.Λ) : QuadraticChartComplexity c₀ H (self.chart K l)
• bounded (K : ℤ × ℤ) (l : self.Λ) : IsBoundedQuadraticChart (self.chart K l)

theorem TrilinearHT.Auto.LowList.birth_sub {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {R : ℤ × ℤ} {c₀ : ℕ} {H : ℝ} (X : LowList G J N R c₀ H) (I : ℤ × ℤ) (l : X.Λ) (h : X.coef I l ≠ 0) : dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G (X.birth I l).1 (X.birth I l).2 ∧ X.birth I l ∈ dyadicFiniteTree G J N ∧ dyadicGridCell G (X.birth I l).1 (X.birth I l).2 ⊆ dyadicGridCell G R.1 R.2

theorem TrilinearHT.Auto.LowList.birth_canon {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {R : ℤ × ℤ} {c₀ : ℕ} {H : ℝ} (X : LowList G J N R c₀ H) (I₁ I₂ : ℤ × ℤ) (l : X.Λ) (h₁ : X.coef I₁ l ≠ 0) (h₂ : X.coef I₂ l ≠ 0) (hnd : ¬Disjoint (dyadicGridCell G (X.birth I₁ l).1 (X.birth I₁ l).2) (dyadicGridCell G (X.birth I₂ l).1 (X.birth I₂ l).2)) : X.birth I₁ l = X.birth I₂ l

noncomputable def TrilinearHT.Auto.LowList.atom {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {R : ℤ × ℤ} {c₀ : ℕ} {H : ℝ} (X : LowList G J N R c₀ H) (I : ℤ × ℤ) (l : X.Λ) : ℝ → ℂ

The atom of label l at the cell I.

Equations

• X.atom I l = TrilinearHT.Auto.quadraticChartAtom (X.chart (X.birth I l) l)

noncomputable def TrilinearHT.Auto.LowList.val {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {R : ℤ × ℤ} {c₀ : ℕ} {H : ℝ} (X : LowList G J N R c₀ H) (I : ℤ × ℤ) (y : ℝ) : ℂ

The low argument X(I) = Σ_l c_{I,l} φ_{I,l}.

Equations

• X.val I y = ∑ l : X.Λ, X.coef I l * X.atom I l y

theorem TrilinearHT.Auto.LowList.atom_measurable {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {R : ℤ × ℤ} {c₀ : ℕ} {H : ℝ} (X : LowList G J N R c₀ H) (I : ℤ × ℤ) (l : X.Λ) : Measurable (X.atom I l)

theorem TrilinearHT.Auto.LowList.atom_bound {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {R : ℤ × ℤ} {c₀ : ℕ} {H : ℝ} (X : LowList G J N R c₀ H) (I : ℤ × ℤ) (l : X.Λ) (y : ℝ) : ‖X.atom I l y‖ ≤ 1

theorem TrilinearHT.Auto.LowList.val_measurable {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {R : ℤ × ℤ} {c₀ : ℕ} {H : ℝ} (X : LowList G J N R c₀ H) (I : ℤ × ℤ) : Measurable (X.val I)

theorem TrilinearHT.Auto.slots4_update_i {a i k : Fin 4} (hai : a ≠ i) (hik : i ≠ k) (za φ φ' zb : ℝ → ℂ) : slots4 a i k za φ φ' zb = Function.update (slots4 a i k za 0 φ' zb) i φ

theorem TrilinearHT.Auto.slots4_update_k {a i k : Fin 4} (hak : a ≠ k) (hik : i ≠ k) (za φ φ' zb : ℝ → ℂ) : slots4 a i k za φ φ' zb = Function.update (slots4 a i k za φ 0 zb) k φ'

theorem TrilinearHT.Auto.localProgressionForm_slots4_expand {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {a i k : Fin 4} (hai : a ≠ i) (hak : a ≠ k) (hik : i ≠ k) {za zb : ℝ → ℂ} (hza : FinL2 a₀ r za) (hzb : FinL2 a₀ r zb) {Λ Λ' : Type} [Fintype Λ] [Fintype Λ'] (c : Λ → ℂ) (c' : Λ' → ℂ) (φ : Λ → ℝ → ℂ) (φ' : Λ' → ℝ → ℂ) (hφ : ∀ (l : Λ), FinL2 a₀ r (φ l)) (hφ' : ∀ (l : Λ'), FinL2 a₀ r (φ' l)) : localProgressionForm r w (slots4 a i k za (fun (y : ℝ) => ∑ l : Λ, c l * φ l y) (fun (y : ℝ) => ∑ l : Λ', c' l * φ' l y) zb) = ∑ l : Λ, ∑ l' : Λ', c l * c' l' * localProgressionForm r w (slots4 a i k za (φ l) (φ' l') zb)

Bilinear expansion of a local form over finite combinations in two slots.

Assembly of the delayed replacement over all low pairs

theorem TrilinearHT.Auto.sum_sqrt_energy_le {G : RealDyadicGrid} {R : ℤ × ℤ} (T : Finset (ℤ × ℤ)) (hT : (↑T).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2) (hTR : ∀ c ∈ T, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G R.1 R.2) {F₁ F₂ : ℝ → ℂ} (h₁ : MeasureTheory.IntegrableOn (fun (y : ℝ) => ‖F₁ y‖ ^ 2) (dyadicGridCell G R.1 R.2) MeasureTheory.volume) (h₂ : MeasureTheory.IntegrableOn (fun (y : ℝ) => ‖F₂ y‖ ^ 2) (dyadicGridCell G R.1 R.2) MeasureTheory.volume) : ∑ c ∈ T, √(∫ (y : ℝ) in dyadicGridCell G c.1 c.2, ‖F₁ y‖ ^ 2) * √(∫ (y : ℝ) in dyadicGridCell G c.1 c.2, ‖F₂ y‖ ^ 2) ≤ √(∫ (y : ℝ) in dyadicGridCell G R.1 R.2, ‖F₁ y‖ ^ 2) * √(∫ (y : ℝ) in dyadicGridCell G R.1 R.2, ‖F₂ y‖ ^ 2)

theorem TrilinearHT.Auto.finL2_of_memLp_cell {G : RealDyadicGrid} {I : ℤ × ℤ} {g : ℝ → ℂ} (hg : Measurable g) (h : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) : FinL2 (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) g

noncomputable def TrilinearHT.Auto.jointBirth {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {R : ℤ × ℤ} {c₀ : ℕ} {H : ℝ} (Xi Xk : LowList G J N R c₀ H) (I : ℤ × ℤ) (li : Xi.Λ) (lk : Xk.Λ) : ℤ × ℤ

The joint birth cell of a low pair at I: the deeper of the two birth cells.

Equations

• TrilinearHT.Auto.jointBirth Xi Xk I li lk = if (Xi.birth I li).1 ≤ (Xk.birth I lk).1 then Xk.birth I lk else Xi.birth I li

theorem TrilinearHT.Auto.jointBirth_spec {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {R : ℤ × ℤ} {c₀ : ℕ} {H : ℝ} (Xi Xk : LowList G J N R c₀ H) {I : ℤ × ℤ} {li : Xi.Λ} {lk : Xk.Λ} (hi : Xi.coef I li ≠ 0) (hk : Xk.coef I lk ≠ 0) : dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G (jointBirth Xi Xk I li lk).1 (jointBirth Xi Xk I li lk).2 ∧ jointBirth Xi Xk I li lk ∈ dyadicFiniteTree G J N ∧ dyadicGridCell G (jointBirth Xi Xk I li lk).1 (jointBirth Xi Xk I li lk).2 ⊆ dyadicGridCell G (Xi.birth I li).1 (Xi.birth I li).2 ∧ dyadicGridCell G (jointBirth Xi Xk I li lk).1 (jointBirth Xi Xk I li lk).2 ⊆ dyadicGridCell G (Xk.birth I lk).1 (Xk.birth I lk).2

theorem TrilinearHT.Auto.jointBirth_canon {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {R : ℤ × ℤ} {c₀ : ℕ} {H : ℝ} (Xi Xk : LowList G J N R c₀ H) {I₁ I₂ : ℤ × ℤ} {li : Xi.Λ} {lk : Xk.Λ} (hi₁ : Xi.coef I₁ li ≠ 0) (hk₁ : Xk.coef I₁ lk ≠ 0) (hi₂ : Xi.coef I₂ li ≠ 0) (hk₂ : Xk.coef I₂ lk ≠ 0) (hnd : ¬Disjoint (dyadicGridCell G (jointBirth Xi Xk I₁ li lk).1 (jointBirth Xi Xk I₁ li lk).2) (dyadicGridCell G (jointBirth Xi Xk I₂ li lk).1 (jointBirth Xi Xk I₂ li lk).2)) : Xi.birth I₁ li = Xi.birth I₂ li ∧ Xk.birth I₁ lk = Xk.birth I₂ lk

theorem TrilinearHT.Auto.jointBirth_eq_of {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {R : ℤ × ℤ} {c₀ : ℕ} {H : ℝ} (Xi Xk : LowList G J N R c₀ H) {I₁ I₂ : ℤ × ℤ} {li : Xi.Λ} {lk : Xk.Λ} (h : Xi.birth I₁ li = Xi.birth I₂ li ∧ Xk.birth I₁ lk = Xk.birth I₂ lk) : jointBirth Xi Xk I₁ li lk = jointBirth Xi Xk I₂ li lk

def TrilinearHT.Auto.PredictorCover (κ : LocalKernelClass) {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) (a i k b : Fin 4) (B Dl ε : ℝ) {d e : ℕ} (A : QuadraticChartData d) (A' : QuadraticChartData e) (J' : ℤ × ℤ) : Prop

Predictor cover of a low pair: a predictor list for its two charts whose conjugate predictors are available labels of the high system at the joint birth cell.

Equations

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

theorem TrilinearHT.Auto.slots4_update_a {a i k : Fin 4} (za φ φ' zb : ℝ → ℂ) : slots4 a i k za φ φ' zb = Function.update (slots4 a i k 0 φ φ' zb) a za

theorem TrilinearHT.Auto.ae_normalized_of_cell {a r : ℝ} {p : ℝ → Prop} (h : ∀ᵐ (y : ℝ), y ∈ Set.Ico a (a + r) → p y) : ∀ᵐ (y : ℝ) ∂normalizedIntervalMeasure a r, p y