Trilinear Hilbert transform: lowDelayedReplacement #
theorem
TrilinearHT.Auto.lowDelayedReplacement
(κ : LocalKernelClass)
{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 ε : ℝ}
(hDl : 0 ≤ Dl)
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{V : Type}
[Fintype V]
(P : PathColumnSystem G J N V)
{R : ℤ × ℤ}
(hR : R ∈ dyadicFiniteTree G J N)
{c₀ : ℕ}
{H : ℝ}
(Xi Xk : LowList G J N R c₀ H)
(hcov :
∀ (I : ℤ × ℤ) (li : Xi.Λ) (lk : Xk.Λ),
Xi.coef I li ≠ 0 →
Xk.coef I lk ≠ 0 →
PredictorCover κ P a i k b B Dl ε (Xi.chart (Xi.birth I li) li) (Xk.chart (Xk.birth I lk) lk)
(jointBirth Xi Xk I li lk))
(f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume))
(K₀ : ℕ)
(S : Finset (ℤ × ℤ))
(hS : ∀ I ∈ S, I ∈ pathBelow G J N R)
(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)
(hzbJ :
∀ J' ∈ dyadicFiniteTree G J N,
dyadicGridCell G J'.1 J'.2 ⊆ dyadicGridCell G R.1 R.2 →
IsAdmissibleOpponent G J' Fb zb Kb ∧ 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)))
(hFb : MeasureTheory.IntegrableOn (fun (y : ℝ) => ‖Fb y‖ ^ 2) (dyadicGridCell G R.1 R.2) MeasureTheory.volume)
:
∑ I ∈ S,
dyadicGridLength G I.1 * ‖localProgressionForm (dyadicGridLength G I.1) (w I) (slots4 a i k (↑↑f) (Xi.val I) (Xk.val I) (zb I)) - localProgressionForm (dyadicGridLength G I.1) (w I)
(slots4 a i k ((P.family R hR).delayed f K₀ I) (Xi.val I) (Xk.val I) (zb I))‖ ≤ ↑(Fintype.card Xi.Λ) * ↑(Fintype.card Xk.Λ) * (2 * Real.exp (-B) * (2 * (compressionOneConst (P.rooted R) + ↑K₀) + 1) * Kb + Dl ^ 2 * (delayConst κ * (2⁻¹ ^ K₀ + (1 + ↑K₀) * √ε) * (1 + Dl) ^ 4 * Kb)) * √(∫ (y : ℝ) in dyadicGridCell G R.1 R.2, ‖↑↑f y‖ ^ 2) * √(∫ (y : ℝ) in dyadicGridCell G R.1 R.2, ‖Fb y‖ ^ 2)
Blueprint prop:base, proof lines 1626-1632: inserting the conjugate predictors of every
low pair at its joint birth cell, the delayed replacement of the input in slot a (against the
low arguments in slots i, k and an admissible opponent in slot b) has absolute scale-sum
error controlled by the number of low label pairs, the predictor accuracy e^{-B}, and the
delay error 2^{-K₀} + (1 + K₀)√ε.
theorem
TrilinearHT.Auto.LowList.birth_eq_of_le
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ : ℕ}
{H : ℝ}
(X : LowList G J N R c₀ H)
{c d : ℤ × ℤ}
{l : X.Λ}
(hc : X.avail c l)
(hd : X.avail d l)
(hcd : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2)
:
Births of a label available at two nested tree cells agree.
def
TrilinearHT.Auto.PredAvail
(κ : LocalKernelClass)
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ c₁ : ℕ}
{H : ℝ}
(Xi Xk : LowList G J N R c₀ H)
(a i k b : Fin 4)
(B D : ℝ)
(pkg : (K K' : ℤ × ℤ) → (li : Xi.Λ) → (lk : Xk.Λ) → PredictorPackage κ (Xi.chart K li) (Xk.chart K' lk) a i k b B D c₁)
(c : ℤ × ℤ)
(v : Xi.Λ × Xk.Λ × Fin ⌊D⌋₊)
:
Predictor availability: both low labels available and the index within the list.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
TrilinearHT.Auto.predScalarB
(κ : LocalKernelClass)
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ c₁ : ℕ}
{H : ℝ}
(Xi Xk : LowList G J N R c₀ H)
(a i k b : Fin 4)
(B D : ℝ)
(pkg : (K K' : ℤ × ℤ) → (li : Xi.Λ) → (lk : Xk.Λ) → PredictorPackage κ (Xi.chart K li) (Xk.chart K' lk) a i k b B D c₁)
(K K' : ℤ × ℤ)
(v : Xi.Λ × Xk.Λ × Fin ⌊D⌋₊)
(y : ℝ)
:
The conjugate predictor with index v.2.2 of the pair (v.1, v.2.1) born at (K, K').
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
TrilinearHT.Auto.predScalar
(κ : LocalKernelClass)
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ c₁ : ℕ}
{H : ℝ}
(Xi Xk : LowList G J N R c₀ H)
(a i k b : Fin 4)
(B D : ℝ)
(pkg : (K K' : ℤ × ℤ) → (li : Xi.Λ) → (lk : Xk.Λ) → PredictorPackage κ (Xi.chart K li) (Xk.chart K' lk) a i k b B D c₁)
(c : ℤ × ℤ)
(v : Xi.Λ × Xk.Λ × Fin ⌊D⌋₊)
(y : ℝ)
:
The scalar of a predictor label at a cell.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TrilinearHT.Auto.predAvail_mono
(κ : LocalKernelClass)
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ c₁ : ℕ}
{H : ℝ}
(Xi Xk : LowList G J N R c₀ H)
(a i k b : Fin 4)
(B D : ℝ)
(pkg : (K K' : ℤ × ℤ) → (li : Xi.Λ) → (lk : Xk.Λ) → PredictorPackage κ (Xi.chart K li) (Xk.chart K' lk) a i k b B D c₁)
{c d : ℤ × ℤ}
(hc : c ∈ dyadicFiniteTree G J N)
(hcd : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2)
{v : Xi.Λ × Xk.Λ × Fin ⌊D⌋₊}
(h : PredAvail κ Xi Xk a i k b B D pkg d v)
:
PredAvail κ Xi Xk a i k b B D pkg c v
theorem
TrilinearHT.Auto.predScalar_eq
(κ : LocalKernelClass)
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ c₁ : ℕ}
{H : ℝ}
(Xi Xk : LowList G J N R c₀ H)
(a i k b : Fin 4)
(B D : ℝ)
(pkg : (K K' : ℤ × ℤ) → (li : Xi.Λ) → (lk : Xk.Λ) → PredictorPackage κ (Xi.chart K li) (Xk.chart K' lk) a i k b B D c₁)
{c d : ℤ × ℤ}
(hc : c ∈ dyadicFiniteTree G J N)
(hcd : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2)
{v : Xi.Λ × Xk.Λ × Fin ⌊D⌋₊}
(h : PredAvail κ Xi Xk a i k b B D pkg d v)
:
theorem
TrilinearHT.Auto.predScalar_measurable
(κ : LocalKernelClass)
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ c₁ : ℕ}
{H : ℝ}
(Xi Xk : LowList G J N R c₀ H)
(a i k b : Fin 4)
(B D : ℝ)
(pkg : (K K' : ℤ × ℤ) → (li : Xi.Λ) → (lk : Xk.Λ) → PredictorPackage κ (Xi.chart K li) (Xk.chart K' lk) a i k b B D c₁)
(c : ℤ × ℤ)
(v : Xi.Λ × Xk.Λ × Fin ⌊D⌋₊)
:
Measurable (predScalar κ Xi Xk a i k b B D pkg c v)
theorem
TrilinearHT.Auto.predScalar_bound
(κ : LocalKernelClass)
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ c₁ : ℕ}
{H : ℝ}
(Xi Xk : LowList G J N R c₀ H)
(a i k b : Fin 4)
(B D : ℝ)
(pkg : (K K' : ℤ × ℤ) → (li : Xi.Λ) → (lk : Xk.Λ) → PredictorPackage κ (Xi.chart K li) (Xk.chart K' lk) a i k b B D c₁)
(c : ℤ × ℤ)
(v : Xi.Λ × Xk.Λ × Fin ⌊D⌋₊)
(y : ℝ)
:
noncomputable def
TrilinearHT.Auto.predSystem
(κ : LocalKernelClass)
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ c₁ : ℕ}
{H : ℝ}
(Xi Xk : LowList G J N R c₀ H)
(a i k b : Fin 4)
(B D : ℝ)
(pkg : (K K' : ℤ × ℤ) → (li : Xi.Λ) → (lk : Xk.Λ) → PredictorPackage κ (Xi.chart K li) (Xk.chart K' lk) a i k b B D c₁)
{ε : ℝ}
(hε0 : 0 < ε)
(hε1 : ε ≤ 1)
:
The predictor high system of a pair of low lists (blueprint prop:base, line 1626): one
label for each low label pair and predictor index, available below the pair's joint birth, with
scalar the conjugate predictor and private weight ε.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TrilinearHT.Auto.predSystem_cover
(κ : LocalKernelClass)
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ c₁ : ℕ}
{H : ℝ}
(Xi Xk : LowList G J N R c₀ H)
(a i k b : Fin 4)
(B D : ℝ)
(pkg : (K K' : ℤ × ℤ) → (li : Xi.Λ) → (lk : Xk.Λ) → PredictorPackage κ (Xi.chart K li) (Xk.chart K' lk) a i k b B D c₁)
{ε : ℝ}
(hε0 : 0 < ε)
(hε1 : ε ≤ 1)
(hD1 : 1 ≤ D)
{I : ℤ × ℤ}
{li : Xi.Λ}
{lk : Xk.Λ}
(hci : Xi.coef I li ≠ 0)
(hck : Xk.coef I lk ≠ 0)
:
PredictorCover κ (predSystem κ Xi Xk a i k b B D pkg hε0 hε1) a i k b B D ε (Xi.chart (Xi.birth I li) li)
(Xk.chart (Xk.birth I lk) lk) (jointBirth Xi Xk I li lk)
Blueprint prop:base, line 1626: the predictor system covers every low pair at its joint birth cell.
Low lists from the adaptive fits #
The ancestor of I at depth d.
Equations
- TrilinearHT.Auto.ancAt G I d = (d, TrilinearHT.Auto.dyadicIndex G d (TrilinearHT.Auto.dyadicGridLeft G I.1 I.2))
Instances For
theorem
TrilinearHT.Auto.subset_ancAt
(G : RealDyadicGrid)
(I : ℤ × ℤ)
{d : ℤ}
(hd : d ≤ I.1)
:
dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G (ancAt G I d).1 (ancAt G I d).2
theorem
TrilinearHT.Auto.ancAt_subset
{G : RealDyadicGrid}
{I R : ℤ × ℤ}
(hIR : dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R.1 R.2)
{d : ℤ}
(hd : R.1 ≤ d)
:
dyadicGridCell G (ancAt G I d).1 (ancAt G I d).2 ⊆ dyadicGridCell G R.1 R.2
theorem
TrilinearHT.Auto.ancAt_eq_of_subset
{G : RealDyadicGrid}
{I c : ℤ × ℤ}
(h : dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G c.1 c.2)
:
A cell containing I at depth d is the ancestor of I at depth d.
noncomputable def
TrilinearHT.Auto.fitCoef
{c₂ : ℕ}
{B : ℝ}
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{w : ℤ × ℤ → ℝ × ℝ → ℂ}
{j : Fin 4}
{q : ℝ}
{f : ℝ → ℂ}
{k M : ℕ}
{roots : Finset (ℤ × ℤ)}
{seg : ℤ × ℤ → ℤ × ℤ}
{n : ℤ × ℤ → ℕ}
{a : ℤ × ℤ → ℕ → ℝ → ℂ}
{g : ℤ × ℤ → ℝ → ℂ}
(hF : IsAdaptiveFit c₂ B G J N w j q f k M roots seg n a g)
(I : ℤ × ℤ)
:
The coefficients of a fit at a cell.
Equations
- TrilinearHT.Auto.fitCoef hF I = if h : I ∈ TrilinearHT.Auto.dyadicFiniteTree G J N ∧ TrilinearHT.Auto.kernelHull G J N w I then Classical.choose ⋯ else 0
Instances For
theorem
TrilinearHT.Auto.fitCoef_spec
{c₂ : ℕ}
{B : ℝ}
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{w : ℤ × ℤ → ℝ × ℝ → ℂ}
{j : Fin 4}
{q : ℝ}
{f : ℝ → ℂ}
{k M : ℕ}
{roots : Finset (ℤ × ℤ)}
{seg : ℤ × ℤ → ℤ × ℤ}
{n : ℤ × ℤ → ℕ}
{a : ℤ × ℤ → ℕ → ℝ → ℂ}
{g : ℤ × ℤ → ℝ → ℂ}
(hF : IsAdaptiveFit c₂ B G J N w j q f k M roots seg n a g)
{I : ℤ × ℤ}
(hI : I ∈ dyadicFiniteTree G J N)
(hIT : kernelHull G J N w I)
:
theorem
TrilinearHT.Auto.fitCoef_le
{c₂ : ℕ}
{B : ℝ}
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{w : ℤ × ℤ → ℝ × ℝ → ℂ}
{j : Fin 4}
{q : ℝ}
{f : ℝ → ℂ}
{k M : ℕ}
{roots : Finset (ℤ × ℤ)}
{seg : ℤ × ℤ → ℤ × ℤ}
{n : ℤ × ℤ → ℕ}
{a : ℤ × ℤ → ℕ → ℝ → ℂ}
{g : ℤ × ℤ → ℝ → ℂ}
(hF : IsAdaptiveFit c₂ B G J N w j q f k M roots seg n a g)
(I : ℤ × ℤ)
(m : Fin M)
:
theorem
TrilinearHT.Auto.kernelHull_of_fitCoef_ne
{c₂ : ℕ}
{B : ℝ}
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{w : ℤ × ℤ → ℝ × ℝ → ℂ}
{j : Fin 4}
{q : ℝ}
{f : ℝ → ℂ}
{k M : ℕ}
{roots : Finset (ℤ × ℤ)}
{seg : ℤ × ℤ → ℤ × ℤ}
{n : ℤ × ℤ → ℕ}
{a : ℤ × ℤ → ℕ → ℝ → ℂ}
{g : ℤ × ℤ → ℝ → ℂ}
(hF : IsAdaptiveFit c₂ B G J N w j q f k M roots seg n a g)
{I : ℤ × ℤ}
{m : Fin M}
(h : fitCoef hF I m ≠ 0)
:
kernelHull G J N w I
noncomputable def
TrilinearHT.Auto.fitBirth
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N M : ℕ}
{cnt : ℤ × ℤ → ℤ × ℤ → ℕ}
{R K : ℤ × ℤ}
(I : ℤ × ℤ)
(m : Fin M)
:
The birth cell: the shallowest ancestor of I below R where the label is available.
Equations
- TrilinearHT.Auto.fitBirth I m = if h : TrilinearHT.Auto.fitAvail cnt G J N R K I m then TrilinearHT.Auto.ancAt G I (R.1 + ↑(Nat.find ⋯)) else R
Instances For
theorem
TrilinearHT.Auto.fitBirth_spec
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N M : ℕ}
{cnt : ℤ × ℤ → ℤ × ℤ → ℕ}
{R K : ℤ × ℤ}
(hR : R ∈ dyadicFiniteTree G J N)
{I : ℤ × ℤ}
{m : Fin M}
(h : fitAvail cnt G J N R K I m)
:
dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G (fitBirth I m).1 (fitBirth I m).2 ∧ fitAvail cnt G J N R K (fitBirth I m) m
theorem
TrilinearHT.Auto.fitBirth_depth_le
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N M : ℕ}
{cnt : ℤ × ℤ → ℤ × ℤ → ℕ}
{R K I c : ℤ × ℤ}
{m : Fin M}
(h : fitAvail cnt G J N R K I m)
(hIc : dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G c.1 c.2)
(hcR : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G R.1 R.2)
(hmc : ↑m < cnt K c)
:
theorem
TrilinearHT.Auto.fitBirth_canon
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N M : ℕ}
{cnt : ℤ × ℤ → ℤ × ℤ → ℕ}
{R K : ℤ × ℤ}
(hR : R ∈ dyadicFiniteTree G J N)
{I₁ I₂ : ℤ × ℤ}
{m : Fin M}
(h₁ : fitAvail cnt G J N R K I₁ m)
(h₂ : fitAvail cnt G J N R K I₂ m)
(hnd :
¬Disjoint (dyadicGridCell G (fitBirth I₁ m).1 (fitBirth I₁ m).2)
(dyadicGridCell G (fitBirth I₂ m).1 (fitBirth I₂ m).2))
:
noncomputable def
TrilinearHT.Auto.fitChartData
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N M : ℕ}
{cnt : ℤ × ℤ → ℤ × ℤ → ℕ}
{atm : ℤ × ℤ → ℤ × ℤ → ℕ → ℝ → ℂ}
{K : ℤ × ℤ}
{c₀ : ℕ}
{H : ℝ}
(hpad :
∀ (b : ℤ × ℤ) (m : Fin M),
b ∈ dyadicFiniteTree G J N ∧ dyadicGridCell G b.1 b.2 ⊆ dyadicGridCell G K.1 K.2 ∧ ↑m < cnt K b →
∃ (d : ℕ) (Φ : QuadraticChartData d),
1 ≤ d ∧ QuadraticChartComplexity c₀ H Φ ∧ IsBoundedQuadraticChart Φ ∧ ∀ (y : ℝ), quadraticChartAtom Φ y = atm K b (↑m) y)
(hdef : ∃ (d : ℕ) (Φ : QuadraticChartData d), 1 ≤ d ∧ QuadraticChartComplexity c₀ H Φ ∧ IsBoundedQuadraticChart Φ)
(b : ℤ × ℤ)
(m : Fin M)
:
(d : ℕ) × QuadraticChartData d
The chart of label m at the birth cell b (padded to positive dimension).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TrilinearHT.Auto.fitChartData_spec
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N M : ℕ}
{cnt : ℤ × ℤ → ℤ × ℤ → ℕ}
{atm : ℤ × ℤ → ℤ × ℤ → ℕ → ℝ → ℂ}
{K : ℤ × ℤ}
{c₀ : ℕ}
{H : ℝ}
(hpad :
∀ (b : ℤ × ℤ) (m : Fin M),
b ∈ dyadicFiniteTree G J N ∧ dyadicGridCell G b.1 b.2 ⊆ dyadicGridCell G K.1 K.2 ∧ ↑m < cnt K b →
∃ (d : ℕ) (Φ : QuadraticChartData d),
1 ≤ d ∧ QuadraticChartComplexity c₀ H Φ ∧ IsBoundedQuadraticChart Φ ∧ ∀ (y : ℝ), quadraticChartAtom Φ y = atm K b (↑m) y)
(hdef : ∃ (d : ℕ) (Φ : QuadraticChartData d), 1 ≤ d ∧ QuadraticChartComplexity c₀ H Φ ∧ IsBoundedQuadraticChart Φ)
(b : ℤ × ℤ)
(m : Fin M)
:
1 ≤ (fitChartData hpad hdef b m).fst ∧ QuadraticChartComplexity c₀ H (fitChartData hpad hdef b m).snd ∧ IsBoundedQuadraticChart (fitChartData hpad hdef b m).snd
theorem
TrilinearHT.Auto.fitChartData_atom
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N M : ℕ}
{cnt : ℤ × ℤ → ℤ × ℤ → ℕ}
{atm : ℤ × ℤ → ℤ × ℤ → ℕ → ℝ → ℂ}
{K : ℤ × ℤ}
{c₀ : ℕ}
{H : ℝ}
(hpad :
∀ (b : ℤ × ℤ) (m : Fin M),
b ∈ dyadicFiniteTree G J N ∧ dyadicGridCell G b.1 b.2 ⊆ dyadicGridCell G K.1 K.2 ∧ ↑m < cnt K b →
∃ (d : ℕ) (Φ : QuadraticChartData d),
1 ≤ d ∧ QuadraticChartComplexity c₀ H Φ ∧ IsBoundedQuadraticChart Φ ∧ ∀ (y : ℝ), quadraticChartAtom Φ y = atm K b (↑m) y)
(hdef : ∃ (d : ℕ) (Φ : QuadraticChartData d), 1 ≤ d ∧ QuadraticChartComplexity c₀ H Φ ∧ IsBoundedQuadraticChart Φ)
{b : ℤ × ℤ}
{m : Fin M}
(h : b ∈ dyadicFiniteTree G J N ∧ dyadicGridCell G b.1 b.2 ⊆ dyadicGridCell G K.1 K.2 ∧ ↑m < cnt K b)
(y : ℝ)
:
noncomputable def
TrilinearHT.Auto.fitLowList
{c₂ : ℕ}
{B : ℝ}
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{w : ℤ × ℤ → ℝ × ℝ → ℂ}
{j : Fin 4}
{q : ℝ}
{f : ℝ → ℂ}
{k M : ℕ}
{roots : Finset (ℤ × ℤ)}
{seg : ℤ × ℤ → ℤ × ℤ}
{n : ℤ × ℤ → ℕ}
{a : ℤ × ℤ → ℕ → ℝ → ℂ}
{g : ℤ × ℤ → ℝ → ℂ}
{cnt : ℤ × ℤ → ℤ × ℤ → ℕ}
{atm : ℤ × ℤ → ℤ × ℤ → ℕ → ℝ → ℂ}
(hF : IsAdaptiveFit c₂ B G J N w j q f k M roots seg n a g)
(hA : IsAttemptData c₂ B G J N M roots seg n a cnt atm)
{R K : ℤ × ℤ}
(hR : R ∈ dyadicFiniteTree G J N)
(hK : K ∈ roots)
(hRK : dyadicGridCell G R.1 R.2 ⊆ dyadicGridCell G K.1 K.2)
{c₀ : ℕ}
{H : ℝ}
(hpad :
∀ (b : ℤ × ℤ) (m : Fin M),
b ∈ dyadicFiniteTree G J N ∧ dyadicGridCell G b.1 b.2 ⊆ dyadicGridCell G K.1 K.2 ∧ ↑m < cnt K b →
∃ (d : ℕ) (Φ : QuadraticChartData d),
1 ≤ d ∧ QuadraticChartComplexity c₀ H Φ ∧ IsBoundedQuadraticChart Φ ∧ ∀ (y : ℝ), quadraticChartAtom Φ y = atm K b (↑m) y)
(hdef : ∃ (d : ℕ) (Φ : QuadraticChartData d), 1 ≤ d ∧ QuadraticChartComplexity c₀ H Φ ∧ IsBoundedQuadraticChart Φ)
:
LowList G J N R c₀ H
The low list of one adaptive fit on the tree below R, in the attempt rooted at
K ⊇ R (blueprint prop:base, lines 1626-1630).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TrilinearHT.Auto.fitLowList_val
{c₂ : ℕ}
{B : ℝ}
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{w : ℤ × ℤ → ℝ × ℝ → ℂ}
{j : Fin 4}
{q : ℝ}
{f : ℝ → ℂ}
{k M : ℕ}
{roots : Finset (ℤ × ℤ)}
{seg : ℤ × ℤ → ℤ × ℤ}
{n : ℤ × ℤ → ℕ}
{a : ℤ × ℤ → ℕ → ℝ → ℂ}
{g : ℤ × ℤ → ℝ → ℂ}
{cnt : ℤ × ℤ → ℤ × ℤ → ℕ}
{atm : ℤ × ℤ → ℤ × ℤ → ℕ → ℝ → ℂ}
(hF : IsAdaptiveFit c₂ B G J N w j q f k M roots seg n a g)
(hA : IsAttemptData c₂ B G J N M roots seg n a cnt atm)
{R K : ℤ × ℤ}
(hR : R ∈ dyadicFiniteTree G J N)
(hK : K ∈ roots)
(hRK : dyadicGridCell G R.1 R.2 ⊆ dyadicGridCell G K.1 K.2)
{c₀ : ℕ}
{H : ℝ}
(hpad :
∀ (b : ℤ × ℤ) (m : Fin M),
b ∈ dyadicFiniteTree G J N ∧ dyadicGridCell G b.1 b.2 ⊆ dyadicGridCell G K.1 K.2 ∧ ↑m < cnt K b →
∃ (d : ℕ) (Φ : QuadraticChartData d),
1 ≤ d ∧ QuadraticChartComplexity c₀ H Φ ∧ IsBoundedQuadraticChart Φ ∧ ∀ (y : ℝ), quadraticChartAtom Φ y = atm K b (↑m) y)
(hdef : ∃ (d : ℕ) (Φ : QuadraticChartData d), 1 ≤ d ∧ QuadraticChartComplexity c₀ H Φ ∧ IsBoundedQuadraticChart Φ)
{I : ℤ × ℤ}
(hI : I ∈ dyadicFiniteTree G J N)
(hIR : dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R.1 R.2)
(hseg : seg I = K)
(hIT : kernelHull G J N w I)
(y : ℝ)
:
On the cells of the segment of K below R, the low list is the fit.
Column ranges at one cell #
Admissible data for the column of label v on the set s.
Equations
- TrilinearHT.Auto.ColOK s sc wt v = (MeasurableSet s ∧ MeasureTheory.volume s < ⊤ ∧ Measurable (sc v) ∧ (∀ (y : ℝ), ‖sc v y‖ ≤ 1) ∧ 0 ≤ wt v ∧ wt v ≤ 1)
Instances For
theorem
TrilinearHT.Auto.ColOK.memLp
{V : Type}
[Fintype V]
{s : Set ℝ}
{sc : V → ℝ → ℂ}
{wt : V → ℝ}
{v : V}
(h : ColOK s sc wt v)
:
MeasureTheory.MemLp (s.indicator (privateColumnValue sc wt v)) 2 MeasureTheory.volume
noncomputable def
TrilinearHT.Auto.col
{V : Type}
[Fintype V]
(s : Set ℝ)
(sc : V → ℝ → ℂ)
(wt : V → ℝ)
(v : V)
:
↥(ColumnL2 V)
The column 1_s (φ_v, √(w_v) e_v).
Equations
- TrilinearHT.Auto.col s sc wt v = if h : TrilinearHT.Auto.ColOK s sc wt v then MeasureTheory.MemLp.toLp (s.indicator (TrilinearHT.Auto.privateColumnValue sc wt v)) ⋯ else 0
Instances For
theorem
TrilinearHT.Auto.col_coeFn
{V : Type}
[Fintype V]
{s : Set ℝ}
{sc : V → ℝ → ℂ}
{wt : V → ℝ}
{v : V}
(h : ColOK s sc wt v)
:
↑↑(col s sc wt v) =ᵐ[MeasureTheory.volume] s.indicator (privateColumnValue sc wt v)
noncomputable def
TrilinearHT.Auto.colRange
{V : Type}
[Fintype V]
(s : Set ℝ)
(sc : V → ℝ → ℂ)
(wt : V → ℝ)
(A : Finset V)
:
The range of the columns of the labels in A on s.
Equations
- TrilinearHT.Auto.colRange s sc wt A = Submodule.span ℂ (TrilinearHT.Auto.col s sc wt '' ↑A)
Instances For
theorem
TrilinearHT.Auto.colRange_gain
{V : Type}
[Fintype V]
[DecidableEq V]
{s : Set ℝ}
{sc : V → ℝ → ℂ}
{wt : V → ℝ}
{A : Finset V}
{v : V}
(hv : v ∉ A)
(h : ColOK s sc wt v)
(z : ↥(ColumnL2 V))
(hz : ∀ᵐ (y : ℝ), (↑↑z y).ofLp (some v) = 0)
:
Inserting a fresh column gains at least |∫_s conj(φ_v) (z - P z)_phys|² / (4|s|) of
projection energy (blueprint §11.2, line 1577 and prop:base, proof line 1637).
theorem
TrilinearHT.Auto.ColData.ok
{V : Type}
{sc : V → ℝ → ℂ}
{wt : V → ℝ}
(h : ColData sc wt)
{s : Set ℝ}
(hs : MeasurableSet s)
(hsv : MeasureTheory.volume s < ⊤)
(v : V)
:
ColOK s sc wt v
theorem
TrilinearHT.Auto.col_union
{V : Type}
[Fintype V]
{s₁ s₂ : Set ℝ}
(hs₁ : MeasurableSet s₁)
(hs₁v : MeasureTheory.volume s₁ < ⊤)
(hs₂ : MeasurableSet s₂)
(hs₂v : MeasureTheory.volume s₂ < ⊤)
(hd : Disjoint s₁ s₂)
{sc : V → ℝ → ℂ}
{wt : V → ℝ}
(h : ColData sc wt)
(v : V)
:
theorem
TrilinearHT.Auto.colRange_le_sup
{V : Type}
[Fintype V]
{s₁ s₂ : Set ℝ}
(hs₁ : MeasurableSet s₁)
(hs₁v : MeasureTheory.volume s₁ < ⊤)
(hs₂ : MeasurableSet s₂)
(hs₂v : MeasureTheory.volume s₂ < ⊤)
(hd : Disjoint s₁ s₂)
{sc sc₁ sc₂ : V → ℝ → ℂ}
{wt : V → ℝ}
(h : ColData sc wt)
(h₁ : ColData sc₁ wt)
(h₂ : ColData sc₂ wt)
{A A₁ A₂ : Finset V}
(hA₁ : A ⊆ A₁)
(hA₂ : A ⊆ A₂)
(hc₁ : ∀ v ∈ A, ∀ y ∈ s₁, sc v y = sc₁ v y)
(hc₂ : ∀ v ∈ A, ∀ y ∈ s₂, sc v y = sc₂ v y)
:
Refinement: the range on a union of two cells lies in the sum of the ranges on the cells with inherited labels and consistent scalars.
theorem
TrilinearHT.Auto.colRange_energy_split
{V : Type}
[Fintype V]
{s₁ s₂ : Set ℝ}
(hs₁ : MeasurableSet s₁)
(hs₁v : MeasureTheory.volume s₁ < ⊤)
(hs₂ : MeasurableSet s₂)
(hs₂v : MeasureTheory.volume s₂ < ⊤)
(hd : Disjoint s₁ s₂)
{sc sc₁ sc₂ : V → ℝ → ℂ}
{wt : V → ℝ}
(h : ColData sc wt)
(h₁ : ColData sc₁ wt)
(h₂ : ColData sc₂ wt)
{A A₁ A₂ : Finset V}
(hA₁ : A ⊆ A₁)
(hA₂ : A ⊆ A₂)
(hc₁ : ∀ v ∈ A, ∀ y ∈ s₁, sc v y = sc₁ v y)
(hc₂ : ∀ v ∈ A, ∀ y ∈ s₂, sc v y = sc₂ v y)
(z : ↥(ColumnL2 V))
:
theorem
TrilinearHT.Auto.colRange_proj_restrict
{V : Type}
[Fintype V]
{s : Set ℝ}
(hs : MeasurableSet s)
(sc : V → ℝ → ℂ)
(wt : V → ℝ)
(A : Finset V)
(z : ↥(ColumnL2 V))
:
(colRange s sc wt A).starProjection ((columnL2Restriction s hs) z) = (colRange s sc wt A).starProjection z
The projection only sees the input on its cell.
noncomputable def
TrilinearHT.Auto.colCoeff
{V : Type}
[Fintype V]
(s : Set ℝ)
(sc : V → ℝ → ℂ)
(wt : V → ℝ)
(A : Finset V)
(z : ↥(ColumnL2 V))
:
V → ℂ
Coefficients of the projection in the columns.
Equations
- TrilinearHT.Auto.colCoeff s sc wt A z = Classical.choose ⋯
Instances For
noncomputable def
TrilinearHT.Auto.colPhys
{V : Type}
[Fintype V]
(s : Set ℝ)
(sc : V → ℝ → ℂ)
(wt : V → ℝ)
(A : Finset V)
(z : ↥(ColumnL2 V))
(y : ℝ)
:
The pointwise physical part of the projection: ∑ c_v φ_v over admissible labels.
Equations
- TrilinearHT.Auto.colPhys s sc wt A z y = ∑ v ∈ A, if TrilinearHT.Auto.ColOK s sc wt v then TrilinearHT.Auto.colCoeff s sc wt A z v * sc v y else 0
Instances For
The data of the accurate high fits of one input (blueprint prop:base, proof lines
1634-1641): a predictor system, the delay K₀, coarse cells tested at depth +K₀, fit labels
Fin M with private weight one, the input f in slot e at accuracy e^{-k}.
- G : RealDyadicGrid
Dyadic grid used for the accurate high-fit construction.
Root cell for the accurate high-fit construction.
- N : ℕ
Number of fine-grid generations below the root.
- K₀ : ℕ
Delay between coarse fitting cells and their fine descendants.
- V₀ : Type
Finite label type of the predictor column system.
- P₀ : PathColumnSystem self.G self.J self.N self.V₀
Predictor columns available along the dyadic paths.
- M : ℕ
Maximum number of additional fit labels.
Input function fitted in the selected high slot.
Admissible local kernels assigned to the fitting cells.
- e : Fin 4
High slot occupied by the input being fitted.
- q : ℝ
Integrability exponent used in the high-fit residual estimates.
- k : ℕ
Accuracy exponent specifying the high-fit error threshold.
- c₂ : ℕ
Complexity exponent supplied to the high-fit oracle.
- B : ℝ
Complexity budget supplied to the high-fit oracle.
Instances For
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
Instances For
The column input.
Equations
Instances For
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
- detect (I : ℤ × ℤ) (a : ℕ → ℝ → ℂ) (n : ℕ) : I ∈ dyadicFiniteTree S.G S.J S.Nc → Measurable (S.res I a n) → MeasureTheory.eLpNorm (S.res I a n) 2 (normalizedIntervalMeasure (dyadicGridLeft S.G I.1 I.2) (dyadicGridLength S.G I.1)) ≤ ENNReal.ofReal 2 → ¬FormSmall (dyadicGridLeft S.G I.1 I.2) (dyadicGridLength S.G I.1) (S.w I) S.e S.q (S.res I a n) (Real.exp (-↑S.k)) → ∃ (p : (d : ℕ) × QuadraticChartData d), FitChartGood S.c₂ S.B (dyadicGridLeft S.G I.1 I.2) (dyadicGridLength S.G I.1) (S.res I a n) p
Instances For
theorem
TrilinearHT.Auto.setIntegral_cell_eq_sum_generation_complex
(G : RealDyadicGrid)
(I : ℤ × ℤ)
(n : ℕ)
{F : ℝ → ℂ}
(hF : MeasureTheory.IntegrableOn F (dyadicGridCell G I.1 I.2) MeasureTheory.volume)
:
∫ (y : ℝ) in dyadicGridCell G I.1 I.2, F y = ∑ Q ∈ dyadicGeneration G I n, ∫ (y : ℝ) in dyadicGridCell G Q.1 Q.2, F y
theorem
TrilinearHT.Auto.AccSetup.Hyp.memLp
{S : AccSetup}
(h : S.Hyp)
:
MeasureTheory.MemLp ((S.cell S.J).indicator S.f) 2 MeasureTheory.volume
theorem
TrilinearHT.Auto.AccSetup.Hyp.res_eLpNorm_le
{S : AccSetup}
(h : S.Hyp)
{I : ℤ × ℤ}
(hI : I ∈ dyadicFiniteTree S.G S.J S.Nc)
(hT : kernelHull S.G S.J S.N S.w I)
(a : ℕ → ℝ → ℂ)
(n : ℕ)
:
MeasureTheory.eLpNorm (S.res I a n) 2
(normalizedIntervalMeasure (dyadicGridLeft S.G I.1 I.2) (dyadicGridLength S.G I.1)) ≤ ENNReal.ofReal 2
The coarse residual has normalized L² norm at most two.
theorem
TrilinearHT.Auto.AccSetup.Hyp.gain
{S : AccSetup}
(h : S.Hyp)
{I : ℤ × ℤ}
(hI : I ∈ dyadicFiniteTree S.G S.J S.Nc)
{a : ℕ → ℝ → ℂ}
{n : ℕ}
(hn : n < S.M)
(hP : ¬S.P I a n)
:
Blueprint prop:base, proof lines 1634-1637: inserting the detection atom with a fresh label
on all fine subcells of a failing coarse cell increases the fine energy by B⁻²|I|/4.
theorem
TrilinearHT.Auto.dyadicGeneration_succ_eq_biUnion
(G : RealDyadicGrid)
(I : ℤ × ℤ)
(n : ℕ)
:
dyadicGeneration G I (n + 1) = (dyadicChildren G I).biUnion fun (I' : ℤ × ℤ) => dyadicGeneration G I' n
Generations below I regrouped by the children of I.
theorem
TrilinearHT.Auto.dyadicChildren_generation_disjoint
(G : RealDyadicGrid)
(I : ℤ × ℤ)
(n : ℕ)
:
(↑(dyadicChildren G I)).PairwiseDisjoint fun (I' : ℤ × ℤ) => dyadicGeneration G I' n
theorem
TrilinearHT.Auto.AccSetup.Hyp.energy_children
{S : AccSetup}
(h : S.Hyp)
{I : ℤ × ℤ}
(hI : I ∈ dyadicFiniteTree S.G S.J S.Nc)
(hIN : I.1 + 1 ≤ S.J.1 + ↑S.Nc)
{a : ℕ → ℝ → ℂ}
(ha : ∀ (i : ℕ), Measurable (a i) ∧ ∀ (y : ℝ), ‖a i y‖ ≤ 1)
(n : ℕ)
:
Blueprint prop:base, line 1639 (orthogonal energy of the chronological fitting sequence): with the same fit list, the fine energy of a coarse cell is at most the fine energies of its children at the next stage.
theorem
TrilinearHT.Auto.AccSetup.Hyp.system_delayed_ae
{S : AccSetup}
(h : S.Hyp)
{K R I : ℤ × ℤ}
(hR : R ∈ dyadicFiniteTree S.G S.J S.N)
(hIR : I ∈ pathBelow S.G S.J S.N R)
(hIc : I ∈ dyadicFiniteTree S.G S.J S.Nc)
(hIK : S.cell I ⊆ S.cell K)
(hKI : K.1 ≤ I.1)
:
The delayed opponent of the attempt system rooted at a cell R is, on a coarse cell I,
the physical part of its fine projections.
theorem
TrilinearHT.Auto.AccSetup.Hyp.phys_sup
{S : AccSetup}
(h : S.Hyp)
{ε : ℝ}
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(hwε : ∀ (v : S.V₀), ε ≤ S.P₀.weight v)
{I : ℤ × ℤ}
(hIc : I ∈ dyadicFiniteTree S.G S.J S.Nc)
(hIT : kernelHull S.G S.J S.N S.w I)
{a : ℕ → ℝ → ℂ}
(ha : ∀ (i : ℕ), Measurable (a i) ∧ ∀ (y : ℝ), ‖a i y‖ ≤ 1)
(n : ℕ)
(y : ℝ)
:
Private-coordinate recovery bounds the physical part of the fine projections on a coarse cell (blueprint prop:base, line 1641).
Pair control for the replaced tuple #
theorem
TrilinearHT.Auto.FormSmall.apply_pair_Lq
{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)
{C : ℝ}
(hC : 0 < C)
(hVq : MeasureTheory.eLpNorm V (ENNReal.ofReal q) (normalizedIntervalMeasure a₀ r) ≤ ENNReal.ofReal C)
{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)
:
Residual smallness against an L^q input of size at most C.
The data of the replaced tuple at one cell (blueprint prop:base, eq:Y and proof lines
1641-1642): low arguments bounded by S, high arguments X_e = f_e - g_e and their
replacements Y_e = P_e - g_e with d_{e,I}(f_e - P_e) ≤ δ_e.
- a₀ : ℝ
Left endpoint of the cell in the tuple-replacement estimate.
- r : ℝ
Positive length of the cell in the tuple-replacement estimate.
Admissible kernel used by the tuple-replacement local form.
- q : ℝ
Integrability exponent of the normalized original inputs.
- i : Fin 4
First low slot, whose input is uniformly bounded.
- j : Fin 4
Second low slot, distinct from the first low slot.
- a : Fin 4
First high slot, replaced using the approximation
Pa. - b : Fin 4
Second high slot, replaced using the approximation
Pb. Tuple before replacement, with high entries represented as residuals.
Original normalized input functions in the high-slot residuals.
Projected approximations subtracted from the original inputs.
Accurate approximation replacing the first high-slot input.
Accurate approximation replacing the second high-slot input.
- S : ℝ
Uniform norm bound for the low inputs and the subtracted projections.
- Sa : ℝ
Uniform norm bound for the first accurate high-slot approximation.
- Sb : ℝ
Uniform norm bound for the second accurate high-slot approximation.
- η₀ : ℝ
Pair-smallness threshold for distinct entries of the original tuple.
- δa : ℝ
Residual-smallness tolerance for the first high-slot replacement.
- δb : ℝ
Residual-smallness tolerance for the second high-slot replacement.
- adm : IsAdmissibleLocalKernel κ self.a₀ self.r self.w
- X_meas (l : Fin 4) : Measurable (self.X l)
- f_meas (l : Fin 4) : Measurable (self.f l)
- f_norm (l : Fin 4) : MeasureTheory.eLpNorm (self.f l) (ENNReal.ofReal self.q) (normalizedIntervalMeasure self.a₀ self.r) ≤ 1
- g_meas (l : Fin 4) : Measurable (self.g l)
- Pa_meas : Measurable self.Pa
- Pb_meas : Measurable self.Pb
Instances For
@[reducible, inline]
The normalized measure of the cell.
Equations
Instances For
@[reducible, inline]
noncomputable abbrev
TrilinearHT.Auto.YCell.H
{κ : LocalKernelClass}
(C : YCell κ)
(F : Fin 4 → ℝ → ℂ)
:
The local form.
Equations
- C.H F = TrilinearHT.Auto.localProgressionForm C.r C.w F
Instances For
theorem
TrilinearHT.Auto.YCell.high_Lq
{κ : LocalKernelClass}
(C : YCell κ)
{l : Fin 4}
(hl : l = C.a ∨ l = C.b)
:
def
TrilinearHT.Auto.YCell.Spect
{κ : LocalKernelClass}
(C : YCell κ)
(z : Fin 4 → ℝ → ℂ)
(p p' : Fin 4)
:
Normalized spectators for the slots p, p'.
Equations
Instances For
theorem
TrilinearHT.Auto.YCell.Spect.flip
{κ : LocalKernelClass}
{C : YCell κ}
{z : Fin 4 → ℝ → ℂ}
{p p' : Fin 4}
(h : C.Spect z p p')
:
C.Spect z p' p
theorem
TrilinearHT.Auto.YCell.Spect.ok
{κ : LocalKernelClass}
{C : YCell κ}
{z : Fin 4 → ℝ → ℂ}
{p p' : Fin 4}
(h : C.Spect z p p')
:
SpectatorOK C.a₀ C.r z p p'
The pair bound for the replaced tuple: the supremum S_a of the first new catalog only
multiplies the second precision δ_b (blueprint prop:base, line 1640).
Instances For
theorem
TrilinearHT.Auto.YCell.Y_pairSmall
{κ : LocalKernelClass}
(C : YCell κ)
{s s' : Fin 4}
(hss : s ≠ s')
:
Blueprint prop:base, proof lines 1641-1642: every pair of the replaced tuple Y has
bilinear norm at most η₀ + (2 + 2S)(δ_a + δ_b) + (1 + S_a) δ_b.
Local sizes, the basic side and the two-U term #
theorem
TrilinearHT.Auto.PairSmall.le_mul
{a₀ r : ℝ}
{w : ℝ × ℝ → ℂ}
{p p' : Fin 4}
(hpp : p ≠ p')
{X Y : ℝ → ℂ}
{η : ℝ}
(h : PairSmall a₀ r w p p' X Y η)
{F : Fin 4 → ℝ → ℂ}
(hF : ∀ (l : Fin 4), Measurable (F l))
{a b : Fin 4}
(hab : a ≠ b)
(hap : a ≠ p)
(hap' : a ≠ p')
(hbp : b ≠ p)
(hbp' : b ≠ p')
{ca cb : ℝ}
(hca : 0 < ca)
(hcb : 0 < cb)
(hFa : MeasureTheory.eLpNorm (F a) 2 (normalizedIntervalMeasure a₀ r) ≤ ENNReal.ofReal ca)
(hFb : MeasureTheory.eLpNorm (F b) 2 (normalizedIntervalMeasure a₀ r) ≤ ENNReal.ofReal cb)
:
A pair estimate against spectators of arbitrary normalized L² size:
|H(X, Y, z_a, z_b)| ≤ η ‖z_a‖ ‖z_b‖.
theorem
TrilinearHT.Auto.PairSmall.le_norm_mul
{a₀ r : ℝ}
{w : ℝ × ℝ → ℂ}
{p p' : Fin 4}
(hpp : p ≠ p')
{X Y : ℝ → ℂ}
{η : ℝ}
(hη : 0 ≤ η)
(h : PairSmall a₀ r w p p' X Y η)
{F : Fin 4 → ℝ → ℂ}
(hF : ∀ (l : Fin 4), Measurable (F l))
{a b : Fin 4}
(hab : a ≠ b)
(hap : a ≠ p)
(hap' : a ≠ p')
(hbp : b ≠ p)
(hbp' : b ≠ p')
(hfa : MeasureTheory.eLpNorm (F a) 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤)
(hfb : MeasureTheory.eLpNorm (F b) 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤)
:
‖localProgressionForm r w (slotPair F p p' X Y)‖ ≤ (MeasureTheory.eLpNorm (F a) 2 (normalizedIntervalMeasure a₀ r)).toReal * (MeasureTheory.eLpNorm (F b) 2 (normalizedIntervalMeasure a₀ r)).toReal * η
The pair estimate with the spectators' exact normalized sizes.
Several-variable charts from one-variable charts (blueprint lines 642-660) #
The lift of a one-variable chart along a linear functional ℓ on ℝ^k:
z ↦ φ(ℓ · z).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TrilinearHT.Auto.liftChart_alongLine
{d k : ℕ}
(B : QuadraticChartData d)
(ℓ z : Fin k → ℝ)
:
theorem
TrilinearHT.Auto.liftChart_complexity
{d k c₀ : ℕ}
{H : ℝ}
{B : QuadraticChartData d}
(hB : QuadraticChartComplexity c₀ H B)
(ℓ : Fin k → ℝ)
:
MultivariableQuadraticChartComplexity c₀ H (liftChart B ℓ)
noncomputable def
TrilinearHT.Auto.mvProductChart
{k d e : ℕ}
(M : MultivariableQuadraticChartData k d)
(N : MultivariableQuadraticChartData k e)
:
MultivariableQuadraticChartData k (d + e)
The product of two several-variable charts in the same variables.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TrilinearHT.Auto.mvProductChart_alongLine
{k d e : ℕ}
(M : MultivariableQuadraticChartData k d)
(N : MultivariableQuadraticChartData k e)
(v : Fin k → ℝ)
:
theorem
TrilinearHT.Auto.mvProductChart_atom
{k d e : ℕ}
(M : MultivariableQuadraticChartData k d)
(N : MultivariableQuadraticChartData k e)
(z : Fin k → ℝ)
:
theorem
TrilinearHT.Auto.mvProductChart_complexity
{k d e c₀ : ℕ}
{H : ℝ}
{M : MultivariableQuadraticChartData k d}
{N : MultivariableQuadraticChartData k e}
(hM : MultivariableQuadraticChartComplexity c₀ H M)
(hN : MultivariableQuadraticChartComplexity c₀ H N)
(hc : 1 ≤ c₀)
:
MultivariableQuadraticChartComplexity c₀ (H ^ 6) (mvProductChart M N)
noncomputable def
TrilinearHT.Auto.mvDilateChart
{k d : ℕ}
(a : ℝ)
(A : MultivariableQuadraticChartData k d)
:
Dilation of a several-variable chart: z ↦ Q(a z).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TrilinearHT.Auto.mvDilateChart_alongLine
{k d : ℕ}
(a : ℝ)
(A : MultivariableQuadraticChartData k d)
(v : Fin k → ℝ)
:
theorem
TrilinearHT.Auto.mvDilateChart_atom
{k d : ℕ}
(a : ℝ)
(A : MultivariableQuadraticChartData k d)
(z : Fin k → ℝ)
:
theorem
TrilinearHT.Auto.mvDilateChart_complexity
{k d c₀ : ℕ}
{H : ℝ}
{A : MultivariableQuadraticChartData k d}
(hA : MultivariableQuadraticChartComplexity c₀ H A)
(a : ℝ)
:
noncomputable def
TrilinearHT.Auto.mvEffQuad
{k d : ℕ}
(A : MultivariableQuadraticChartData k d)
(M : Matrix (Fin d) (Fin d) ℚ)
:
The effective quadratic form of a several-variable chart for a rational matrix M,
symmetrized: Λ + sym(Vᵀ M V).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TrilinearHT.Auto.effectiveReturnQuadratic_eq_sym
{d k : ℕ}
(C : Matrix (Fin d) (Fin d) ℝ)
(Λ : Matrix (Fin k) (Fin k) ℝ)
(V : Matrix (Fin d) (Fin k) ℝ)
(Qr : Matrix (Fin d) (Fin d) ℝ)
:
effectiveReturnQuadratic C Λ V ((1 - Qr) * V) (Qr * V) = Λ + realSymmetricPart (V.transpose * ((1 / 2) • realSymmetricPart C + (1 - Qr).transpose * realSkewPart C * Qr) * V)
theorem
TrilinearHT.Auto.effectiveReturnQuadratic_eq_mvEffQuad
{k d : ℕ}
(A : MultivariableQuadraticChartData k d)
(Q : Matrix (Fin d) (Fin d) ℚ)
:
effectiveReturnQuadratic (A.matrix.map fun (q : ℚ) => ↑q) A.quadratic A.horizontal
((1 - Q.map fun (q : ℚ) => ↑q) * A.horizontal) ((Q.map fun (q : ℚ) => ↑q) * A.horizontal) = mvEffQuad A (separatedPhaseMatrix A.matrix Q)
theorem
TrilinearHT.Auto.mvSeparatedPhase
(c₀ : ℕ)
(hc : 1 ≤ c₀)
(k : ℕ)
(hk1 : 1 ≤ k)
(hk3 : k ≤ 3)
(R : ℝ)
(hR : 0 ≤ R)
:
∃ (D : ℕ),
1 ≤ D ∧ ∃ (DJ : ℕ → ℕ),
∀ {d : ℕ} (H δ : ℝ) (A : MultivariableQuadraticChartData k d),
MultivariableQuadraticChartComplexity c₀ H A →
∀ (θ : (Fin k → ℝ) → ℂ),
Measurable θ →
(∀ (z : Fin k → ℝ), ‖θ z‖ ≤ H) →
(∀ (x y : Fin k → ℝ), ‖θ y - θ x‖ ≤ H * ‖y - x‖) →
(∀ (z : Fin k → ℝ), θ z ≠ 0 → ∀ (i : Fin k), |z i| ≤ R) →
0 < δ →
(∀ t < δ,
∃ (ξ : EuclideanSpace ℝ (Fin k)),
t < ‖FourierTransform.fourier
(fun (z : EuclideanSpace ℝ (Fin k)) =>
θ z.ofLp * multivariableQuadraticChartAtom A z.ofLp)
ξ‖) →
have X := 1 + Real.log H + Real.log (max 1 δ⁻¹);
∃ (M : Matrix (Fin d) (Fin d) ℚ),
(∀ (i j : Fin d), ↑(rationalHeight (M i j)) ≤ Real.exp (↑D * X ^ D)) ∧ (∀ (i j : Fin k), |mvEffQuad A M i j| ≤ Real.exp (↑D * X ^ D)) ∧ ∃ (ι : Type) (x : Fintype ι) (σ : ι × (Fin (d + d) → ℤ) → Fin d → ℚ),
↑(Fintype.card ι) ≤ Real.exp (↑D * X ^ D) ∧ (∀ (p : ι × (Fin (d + d) → ℤ)) (i : Fin d),
↑(rationalHeight (σ p i)) ≤ Real.exp (↑D * X ^ D) * (1 + frequencyLength p.2)) ∧ ∃ (a : ι × (Fin (d + d) → ℤ) → ℂ),
(∀ (z : Fin k → ℝ),
(∀ (i : Fin k), |z i| ≤ R) →
HasSum
(fun (p : ι × (Fin (d + d) → ℤ)) =>
a p * ↑(Real.fourierChar
((fun (i : Fin d) => ↑(σ p i)) ⬝ᵥ A.horizontal.mulVec z)))
(↑(Real.fourierChar (-(z ⬝ᵥ (mvEffQuad A M).mulVec z + A.linear ⬝ᵥ z))) * multivariableQuadraticChartAtom A z)) ∧ (Summable fun (p : ι × (Fin (d + d) → ℤ)) => ‖a p‖) ∧ ∑' (p : ι × (Fin (d + d) → ℤ)), ‖a p‖ ≤ Real.exp (↑D * X ^ D) ∧ ∀ (J : ℕ),
(∀ (p : ι × (Fin (d + d) → ℤ)),
‖a p‖ * (1 + frequencyLength p.2) ^ (J * (d + 1) ^ 2) ≤ Real.exp (↑(DJ J) * X ^ DJ J)) ∧ ∀ (T : ℝ),
1 ≤ T →
(∑ f : ι, ∑ v ∈ frequencyShell (d + d) T, ‖a (f, v)‖) * T ^ (J * (d + 1) ^ 2) ≤ Real.exp (↑(DJ J) * X ^ DJ J)
Blueprint lem:separation in up to three variables: lemmas lem:weyl and
lem:chartfourier combined. If the Fourier supremum of θ Q is at least δ, then on the box
Q(z) = e(zᵀΛ_* z + b·z) Σ a_ℓ e(σ_ℓ·Vz) exactly and absolutely, with
Λ_* = Λ + sym(Vᵀ M V) for a rational matrix M of bounded height and bounded entries.
One-dimensional Fourier estimates for a kernel slice #
theorem
TrilinearHT.Auto.continuous_fourierChar_mul
(ν : ℝ)
:
Continuous fun (x : ℝ) => ↑(Real.fourierChar (ν * x))
The doubled kernel in three variables #
theorem
TrilinearHT.Auto.sixTheta_fourier_bound
{W : ℝ × ℝ → ℂ}
{K R S : ℝ}
(hR : 0 ≤ R)
(hW : Continuous W)
(hK : ∀ (p : ℝ × ℝ), ‖W p‖ ≤ K)
(hs : ∀ (p : ℝ × ℝ), W p ≠ 0 → |p.1| ≤ R ∧ |p.2| ≤ R)
(ν : Fin 3 → ℝ)
(hS : ∀ (u : ℝ), ‖∫ (τ : ℝ), W (u, τ) * ↑(Real.fourierChar (ν 1 * τ))‖ ≤ S)
:
The τ-integral controls the Fourier coefficients of the doubled kernel.
theorem
TrilinearHT.Auto.fintype_prod_tail
{ι : Type u_1}
[Fintype ι]
{D k : ℕ}
(hD : 1 ≤ D)
(hk : D < k)
(a : ι × (Fin D → ℤ) → ℂ)
{E : ℝ}
(hE : 0 ≤ E)
(ha : ∀ (p : ι × (Fin D → ℤ)), ‖a p‖ * (1 + frequencyLength p.2) ^ k ≤ E)
(K₀ : ℕ)
:
Coefficient mass beyond a frequency truncation, for coefficients indexed by a finite family times a frequency lattice.
The volume of the box [-1,1]³.
theorem
TrilinearHT.Auto.sixTheta_continuous
{W : ℝ × ℝ → ℂ}
(hW : Continuous W)
:
Continuous (sixTheta W)
theorem
TrilinearHT.Auto.sixTheta_mul_norm_le
{W : ℝ × ℝ → ℂ}
{K c : ℝ}
(hK : ∀ (p : ℝ × ℝ), ‖W p‖ ≤ K)
(hs : ∀ (p : ℝ × ℝ), W p ≠ 0 → |p.1| ≤ 1 ∧ |p.2| ≤ 1)
{g : (Fin 3 → ℝ) → ℂ}
(hg : ∀ (z : Fin 3 → ℝ), (∀ (i : Fin 3), |z i| ≤ 1) → ‖g z‖ ≤ c)
(z : Fin 3 → ℝ)
:
Bound by K² times an indicator of the box.
theorem
TrilinearHT.Auto.slice_fourier_le
{W : ℝ × ℝ → ℂ}
{K L : ℝ}
(hW : Continuous W)
(hK : ∀ (p : ℝ × ℝ), ‖W p‖ ≤ K)
(hL : ∀ (p q : ℝ × ℝ), ‖W p - W q‖ ≤ L * ‖p - q‖)
(hs : ∀ (p : ℝ × ℝ), W p ≠ 0 → |p.1| ≤ 1 ∧ |p.2| ≤ 1)
(hm : ∀ (u : ℝ), ∫ (τ : ℝ), W (u, τ) = 0)
(hL0 : 0 ≤ L)
{ν α₁ β₁ : ℝ}
(hα₁ : 0 ≤ α₁)
(hβ₁ : 1 ≤ β₁)
(hν : |ν| ≤ α₁ ∨ β₁ ≤ |ν|)
(u : ℝ)
:
The τ-integral of a kernel slice against a tiny or a large frequency.
theorem
TrilinearHT.Auto.sixTheta_expansion_bound
{W : ℝ × ℝ → ℂ}
{K L : ℝ}
(hW : Continuous W)
(hK : ∀ (p : ℝ × ℝ), ‖W p‖ ≤ K)
(hL : ∀ (p q : ℝ × ℝ), ‖W p - W q‖ ≤ L * ‖p - q‖)
(hs : ∀ (p : ℝ × ℝ), W p ≠ 0 → |p.1| ≤ 1 ∧ |p.2| ≤ 1)
(hm : ∀ (u : ℝ), ∫ (τ : ℝ), W (u, τ) = 0)
(hL0 : 0 ≤ L)
{τt : Type u_1}
(Φ : (Fin 3 → ℝ) → ℂ)
(N : Matrix (Fin 3) (Fin 3) ℝ)
(b : Fin 3 → ℝ)
{d : ℕ}
(V : Matrix (Fin d) (Fin 3) ℝ)
(σ : τt → Fin d → ℝ)
(a : τt → ℂ)
(hsum : Summable fun (p : τt) => ‖a p‖)
(hexp :
∀ (z : Fin 3 → ℝ),
(∀ (i : Fin 3), |z i| ≤ 1) →
HasSum (fun (p : τt) => a p * ↑(Real.fourierChar (σ p ⬝ᵥ V.mulVec z)))
(↑(Real.fourierChar (-(z ⬝ᵥ N.mulVec z + b ⬝ᵥ z))) * Φ z))
{α α₁ β₁ : ℝ}
(hα : ∀ (i j : Fin 3), |N i j| ≤ α)
(hα₁ : 0 ≤ α₁)
(hβ₁ : 1 ≤ β₁)
(F : Finset τt)
(hF : ∀ p ∈ F, |b 1 + ∑ i : Fin d, σ p i * V i 1| ≤ α₁ ∨ β₁ ≤ |b 1 + ∑ i : Fin d, σ p i * V i 1|)
:
Blueprint prop:base, proof line 1651: the doubled-kernel integral of an expanded chart.
At a scale where every effective quadratic entry is tiny and every retained τ-frequency is
tiny or large, the integral is bounded by the tiny/large errors and the truncation tail.
noncomputable def
TrilinearHT.Auto.effQuadVector
{k d : ℕ}
(A : MultivariableQuadraticChartData k d)
(i j : Fin k)
:
The fixed real parameters of an effective quadratic entry.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TrilinearHT.Auto.effQuad_eval
{k d : ℕ}
(A : MultivariableQuadraticChartData k d)
(M : Matrix (Fin d) (Fin d) ℚ)
(i j : Fin k)
:
∑ l : Fin (d * d + 1),
↑(Fin.cons 1 (fun (x : Fin (d * d)) => M (finProdFinEquiv.symm x).1 (finProdFinEquiv.symm x).2) l) * effQuadVector A i j l = mvEffQuad A M i j
noncomputable def
TrilinearHT.Auto.freqVector
{k d : ℕ}
(A : MultivariableQuadraticChartData k d)
(j : Fin k)
:
The fixed real parameters of a τ-frequency.
Equations
- TrilinearHT.Auto.freqVector A j = Fin.cons (A.linear j) fun (i : Fin d) => A.horizontal i j
Instances For
theorem
TrilinearHT.Auto.freq_eval
{k d : ℕ}
(r : ℝ)
(A : MultivariableQuadraticChartData k d)
(j : Fin k)
(σ : Fin d → ℚ)
:
(mvDilateChart r A).linear j + ∑ i : Fin d, ↑(σ i) * (mvDilateChart r A).horizontal i j = r * ∑ l : Fin (d + 1), ↑(Fin.cons 1 σ l) * freqVector A j l
theorem
TrilinearHT.Auto.sixTheta_count_thresholds
(c₀ : ℕ)
(hc : 1 ≤ c₀)
:
∃ (D : ℕ),
1 ≤ D ∧ ∃ (DJ : ℕ → ℕ),
∀ {d : ℕ} (H K ε r₀ : ℝ) (A : MultivariableQuadraticChartData 3 d),
MultivariableQuadraticChartComplexity c₀ H A →
1 ≤ K →
0 < ε →
0 < r₀ →
∀ (T : Finset ℤ) (W : ℤ → ℝ × ℝ → ℂ),
(∀ (n : ℤ), Continuous (W n)) →
(∀ (n : ℤ) (p : ℝ × ℝ), ‖W n p‖ ≤ K) →
(∀ (n : ℤ) (p q : ℝ × ℝ), ‖W n p - W n q‖ ≤ K * ‖p - q‖) →
(∀ (n : ℤ) (p : ℝ × ℝ), W n p ≠ 0 → |p.1| ≤ 1 ∧ |p.2| ≤ 1) →
(∀ (n : ℤ) (u : ℝ), ∫ (τ : ℝ), W n (u, τ) = 0) →
(∀ n ∈ T,
ε < ‖∫ (z : Fin 3 → ℝ), sixTheta (W n) z * multivariableQuadraticChartAtom A ((r₀ * 2 ^ (-n)) • z)‖) →
∀ (α α₁ β₁ : ℝ) (K₀ : ℕ),
have X := 1 + Real.log (2 * H * K ^ 2) + Real.log (max 1 ε⁻¹);
have E := Real.exp (↑D * X ^ D);
have E₁ := Real.exp (↑(DJ 1) * X ^ DJ 1);
0 < α →
α ≤ E →
0 < α₁ →
α₁ ≤ β₁ →
1 ≤ β₁ →
E * (4 * K * (4 * Real.pi * K * α₁ + 2 * K / β₁) + 8 * (K ^ 2 * (2 * Real.pi * (9 * α)))) + 8 * (K ^ 2 * (E * (E₁ * (2 * 7 ^ (d + d) * (2 * Real.pi) ^ (d + 1) ^ 2 / 2 ^ K₀)))) ≤ ε →
↑T.card ≤ 9 * (32 * (↑(d * d + 1) + 1) ^ 4 * (Real.log (2 * E) + Real.log (2 * E / α))) + 32 * (↑(d + 1) + 1) ^ 4 * (Real.log (2 * (E * (1 + 2 ^ K₀))) + Real.log (2 * β₁ / α₁))
Blueprint prop:base, proof lines 1647-1651, with explicit thresholds: the number of
scales at which the doubled-kernel integral of a fixed three-variable chart exceeds ε
is at most the number of intermediate scales of the effective quadratic entries and of the
retained τ-frequencies (lem:height).
theorem
TrilinearHT.Auto.count_threshold_big
{K E E₁ G ε Z a : ℝ}
{m : ℕ}
(hK : 1 ≤ K)
(hE : 1 ≤ E)
(hE₁ : 1 ≤ E₁)
(hG : 1 ≤ G)
(hε : 0 < ε)
(hZ1 : 1 ≤ Z)
(hZm : Z ≤ Z ^ m)
(hZ2m : Z ^ 2 ≤ Z ^ m)
(hlK : Real.log K ≤ Z)
(hlε : Real.log ε⁻¹ ≤ Z)
(hlG : Real.log G ≤ 13 * Z ^ 2)
(hlE : Real.log E ≤ a * Z ^ m)
(hlE₁ : Real.log E₁ ≤ a * Z ^ m)
:
The threshold that dominates all errors of the scale estimate.
theorem
TrilinearHT.Auto.sixTheta_scale_count
(c₀ : ℕ)
(hc : 1 ≤ c₀)
:
∃ (C : ℕ),
1 ≤ C ∧ ∀ {d : ℕ} (H K ε r₀ : ℝ) (A : MultivariableQuadraticChartData 3 d),
MultivariableQuadraticChartComplexity c₀ H A →
1 ≤ K →
0 < ε →
ε ≤ 1 →
0 < r₀ →
∀ (T : Finset ℤ) (W : ℤ → ℝ × ℝ → ℂ),
(∀ (n : ℤ), Continuous (W n)) →
(∀ (n : ℤ) (p : ℝ × ℝ), ‖W n p‖ ≤ K) →
(∀ (n : ℤ) (p q : ℝ × ℝ), ‖W n p - W n q‖ ≤ K * ‖p - q‖) →
(∀ (n : ℤ) (p : ℝ × ℝ), W n p ≠ 0 → |p.1| ≤ 1 ∧ |p.2| ≤ 1) →
(∀ (n : ℤ) (u : ℝ), ∫ (τ : ℝ), W n (u, τ) = 0) →
(∀ n ∈ T,
ε < ‖∫ (z : Fin 3 → ℝ), sixTheta (W n) z * multivariableQuadraticChartAtom A ((r₀ * 2 ^ (-n)) • z)‖) →
↑T.card ≤ ↑C * (Real.log H + Real.log K + Real.log ε⁻¹) ^ C
Blueprint prop:base, proof line 1651: the number of scales at which the doubled-kernel
integral of a fixed three-variable chart exceeds ε is polynomial in
log H + log K + log ε⁻¹.
The rescaled kernel slice at a fixed path point #
The kernel in the rescaled coordinates (U, τ) = ((u - y)/r, t/r) of the transposed form
in slot m: W(U, τ) = w(y + r(U - mτ), rτ) (blueprint prop:base, line 1645).
Instances For
Lipschitz constant of the kernel slices of the class.
Equations
- TrilinearHT.Auto.kernelLipConst κ = 5 * (κ.derivativeConstant * 3) ^ (κ.derivativeConstant * 3)
Instances For
One constant bounding the slices and their Lipschitz constants.
Equations
Instances For
theorem
TrilinearHT.Auto.kernelSlice_continuous
{κ : LocalKernelClass}
{a₀ r : ℝ}
{w : ℝ × ℝ → ℂ}
(hw : IsAdmissibleLocalKernel κ a₀ r w)
(y : ℝ)
(m : Fin 4)
:
Continuous (kernelSlice w y r m)
theorem
TrilinearHT.Auto.kernelSlice_norm_le
{κ : LocalKernelClass}
{a₀ r : ℝ}
{w : ℝ × ℝ → ℂ}
(hw : IsAdmissibleLocalKernel κ a₀ r w)
(y : ℝ)
(m : Fin 4)
(p : ℝ × ℝ)
:
theorem
TrilinearHT.Auto.kernelSlice_marginal
{κ : LocalKernelClass}
{a₀ r : ℝ}
{w : ℝ × ℝ → ℂ}
(hw : IsAdmissibleLocalKernel κ a₀ r w)
(y : ℝ)
(m : Fin 4)
(U : ℝ)
:
theorem
TrilinearHT.Auto.admissibleKernel_lipschitz
{κ : LocalKernelClass}
{a₀ r : ℝ}
{w : ℝ × ℝ → ℂ}
(hw : IsAdmissibleLocalKernel κ a₀ r w)
(x x' t t' : ℝ)
:
Mean value bound for the kernel along coordinate lines.
theorem
TrilinearHT.Auto.kernelSlice_lipschitz
{κ : LocalKernelClass}
{a₀ r : ℝ}
(hr : 0 < r)
{w : ℝ × ℝ → ℂ}
(hw : IsAdmissibleLocalKernel κ a₀ r w)
(y : ℝ)
(m : Fin 4)
(p q : ℝ × ℝ)
:
The transposed form in one slot #
The product of the three fixed slots along the transposed line.
Equations
- TrilinearHT.Auto.transposeProduct φ m u t = ∏ j ∈ Finset.univ.erase m, φ j (u + (↑↑j - ↑↑m) * t)
Instances For
theorem
TrilinearHT.Auto.transposeProduct_measurable
{φ : Fin 4 → ℝ → ℂ}
(hφ : ∀ (j : Fin 4), Measurable (φ j))
(m : Fin 4)
:
theorem
TrilinearHT.Auto.tripleTranspose_measurable
{κ : LocalKernelClass}
{a₀ r : ℝ}
{w : ℝ × ℝ → ℂ}
(hw : IsAdmissibleLocalKernel κ a₀ r w)
(m : Fin 4)
{φ : Fin 4 → ℝ → ℂ}
(hφ : ∀ (j : Fin 4), Measurable (φ j))
:
Measurable (tripleTranspose r w m φ)
theorem
TrilinearHT.Auto.localProgressionForm_transpose
{κ : LocalKernelClass}
{a₀ r : ℝ}
(hr : 0 < r)
{w : ℝ × ℝ → ℂ}
(hw : IsAdmissibleLocalKernel κ a₀ r w)
(m : Fin 4)
{F : Fin 4 → ℝ → ℂ}
(hF : ∀ (j : Fin 4), Measurable (F j))
{B : ℝ}
(hB0 : 0 ≤ B)
(hB : ∀ (j : Fin 4), j ≠ m → ∀ (x : ℝ), ‖F j x‖ ≤ B)
(hFm : MeasureTheory.IntegrableOn (F m) (Set.Icc a₀ (a₀ + r)) MeasureTheory.volume)
:
The local form transposed to slot m: H(F) = r⁻¹ ∫ F_m T.
noncomputable def
TrilinearHT.Auto.sixPsi
(φ : Fin 4 → ℝ → ℂ)
(m : Fin 4)
(y r : ℝ)
(z : Fin 3 → ℝ)
:
The six atoms of the squared transposed form at the path point y (blueprint prop:base,
line 1645): the triple at anchor y + r z₀ with times r z₁ and its conjugate with r z₂.
Equations
- TrilinearHT.Auto.sixPsi φ m y r z = TrilinearHT.Auto.transposeProduct φ m (y + r * z 0) (r * z 1) * (starRingEnd ℂ) (TrilinearHT.Auto.transposeProduct φ m (y + r * z 0) (r * z 2))
Instances For
theorem
TrilinearHT.Auto.integrable_of_bound_of_support
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℂ}
{S : Set X}
(hSμ : μ S ≠ ⊤)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
{M : ℝ}
(hM : ∀ (x : X), ‖f x‖ ≤ M)
(hs : ∀ x ∉ S, f x = 0)
:
A bounded measurable function vanishing outside a set of finite measure is integrable.
theorem
TrilinearHT.Auto.tripleTranspose_sq_eq
{κ : LocalKernelClass}
{a₀ r : ℝ}
(hr : 0 < r)
{w : ℝ × ℝ → ℂ}
(hw : IsAdmissibleLocalKernel κ a₀ r w)
(m : Fin 4)
{φ : Fin 4 → ℝ → ℂ}
(hφ : ∀ (j : Fin 4), Measurable (φ j))
{B : ℝ}
(hB0 : 0 ≤ B)
(hB : ∀ (j : Fin 4), j ≠ m → ∀ (x : ℝ), ‖φ j x‖ ≤ B)
(y : ℝ)
:
Blueprint prop:base, line 1645: the squared normalized L² norm of the transposed function
is the doubled-kernel integral of the six atoms in the rescaled variables.
theorem
TrilinearHT.Auto.localProgressionForm_le_six
{κ : LocalKernelClass}
{a₀ r : ℝ}
(hr : 0 < r)
{w : ℝ × ℝ → ℂ}
(hw : IsAdmissibleLocalKernel κ a₀ r w)
(m : Fin 4)
{F : Fin 4 → ℝ → ℂ}
(hF : ∀ (j : Fin 4), Measurable (F j))
{B : ℝ}
(hB0 : 0 ≤ B)
(hB : ∀ (j : Fin 4), j ≠ m → ∀ (x : ℝ), ‖F j x‖ ≤ B)
(hFm : MeasureTheory.MemLp (F m) 2 (normalizedIntervalMeasure a₀ r))
(y : ℝ)
:
‖localProgressionForm r w F‖ ≤ (MeasureTheory.eLpNorm (F m) 2 (normalizedIntervalMeasure a₀ r)).toReal * √‖∫ (z : Fin 3 → ℝ), sixTheta (kernelSlice w y r m) z * sixPsi F m y r z‖
Blueprint prop:base, line 1645: the transpose norm of three fixed slots against a
normalized L² input in the fourth slot is the square root of the doubled-kernel integral of
the six atoms.
theorem
TrilinearHT.Auto.prod_erase_eq_succAbove
{M : Type u_1}
[CommMonoid M]
(m : Fin 4)
(f : Fin 4 → M)
:
noncomputable def
TrilinearHT.Auto.pairChart
{d : ℕ}
(B : QuadraticChartData d)
(c : ℝ)
:
MultivariableQuadraticChartData 3 (d + d)
The two atoms of one slot: the slot atom along z₀ + c z₁ and its conjugate along
z₀ + c z₂.
Equations
Instances For
theorem
TrilinearHT.Auto.pairChart_atom
{d : ℕ}
(B : QuadraticChartData d)
(c r : ℝ)
(z : Fin 3 → ℝ)
:
multivariableQuadraticChartAtom (pairChart B c) (r • z) = quadraticChartAtom B (r * (z 0 + c * z 1)) * (starRingEnd ℂ) (quadraticChartAtom B (r * (z 0 + c * z 2)))
noncomputable def
TrilinearHT.Auto.sixChart
{d : Fin 3 → ℕ}
(B : (i : Fin 3) → QuadraticChartData (d i))
(c : Fin 3 → ℝ)
:
The six-atom chart in three variables (blueprint prop:base, line 1645).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TrilinearHT.Auto.sixChart_atom
{d : Fin 3 → ℕ}
(B : (i : Fin 3) → QuadraticChartData (d i))
(c : Fin 3 → ℝ)
(r : ℝ)
(z : Fin 3 → ℝ)
:
multivariableQuadraticChartAtom (sixChart B c) (r • z) = ∏ i : Fin 3,
quadraticChartAtom (B i) (r * (z 0 + c i * z 1)) * (starRingEnd ℂ) (quadraticChartAtom (B i) (r * (z 0 + c i * z 2)))
theorem
TrilinearHT.Auto.pairChart_complexity
{d c₀ : ℕ}
{H : ℝ}
{B : QuadraticChartData d}
(hB : QuadraticChartComplexity c₀ H B)
(hc : 1 ≤ c₀)
(c : ℝ)
:
MultivariableQuadraticChartComplexity c₀ (H ^ 6) (pairChart B c)
theorem
TrilinearHT.Auto.mvComplexity_mono
{k d c₀ : ℕ}
{H K : ℝ}
{A : MultivariableQuadraticChartData k d}
(hA : MultivariableQuadraticChartComplexity c₀ H A)
(hHK : H ≤ K)
:
theorem
TrilinearHT.Auto.sixChart_complexity
{d : Fin 3 → ℕ}
{c₀ : ℕ}
{H : ℝ}
{B : (i : Fin 3) → QuadraticChartData (d i)}
(hB : ∀ (i : Fin 3), QuadraticChartComplexity c₀ H (B i))
(hc : 1 ≤ c₀)
(c : Fin 3 → ℝ)
:
MultivariableQuadraticChartComplexity c₀ (H ^ 216) (sixChart B c)
theorem
TrilinearHT.Auto.sixPsi_eq_sixChart
{φ : Fin 4 → ℝ → ℂ}
(m : Fin 4)
(y r : ℝ)
{d : Fin 3 → ℕ}
(B : (i : Fin 3) → QuadraticChartData (d i))
(hB : ∀ (i : Fin 3) (s : ℝ), quadraticChartAtom (B i) s = φ (m.succAbove i) (s + y))
(z : Fin 3 → ℝ)
:
The six atoms as a chart atom: with φ_{m.succAbove i}(y + s) = Bᵢ(s),
Ψ(z) = Q(r z) for the fixed six-atom chart Q.
noncomputable def
TrilinearHT.Auto.tripleNorm
(w : ℝ × ℝ → ℂ)
(φ : Fin 4 → ℝ → ℂ)
(m : Fin 4)
(y r : ℝ)
:
The transpose norm of three fixed slots on a cell of scale r through y
(blueprint prop:base, line 1645): A_I = (∫ θ Ψ)^{1/2}.
Equations
- TrilinearHT.Auto.tripleNorm w φ m y r = √‖∫ (z : Fin 3 → ℝ), TrilinearHT.Auto.sixTheta (TrilinearHT.Auto.kernelSlice w y r m) z * TrilinearHT.Auto.sixPsi φ m y r z‖
Instances For
theorem
TrilinearHT.Auto.tripleNorm_count
(κ : LocalKernelClass)
(c₀ : ℕ)
(hc : 1 ≤ c₀)
:
∃ (C : ℕ),
1 ≤ C ∧ ∀ {d : Fin 3 → ℕ} (H r₀ s y : ℝ) (B : (i : Fin 3) → QuadraticChartData (d i)) (φ : Fin 4 → ℝ → ℂ) (m : Fin 4),
(∀ (i : Fin 3), QuadraticChartComplexity c₀ H (B i)) →
(∀ (i : Fin 3) (u : ℝ), quadraticChartAtom (B i) u = φ (m.succAbove i) (u + y)) →
0 < r₀ →
0 < s →
s ≤ 1 →
∀ (a : ℤ → ℝ) (w : ℤ → ℝ × ℝ → ℂ) (T : Finset ℤ),
(∀ n ∈ T, IsAdmissibleLocalKernel κ (a n) (r₀ * 2 ^ (-n)) (w n)) →
(∀ n ∈ T, y ∈ Set.Icc (a n) (a n + r₀ * 2 ^ (-n))) →
(∀ n ∈ T, s < tripleNorm (w n) φ m y (r₀ * 2 ^ (-n))) →
↑T.card ≤ ↑C * (216 * Real.log H + Real.log (sliceConst κ) + 2 * Real.log s⁻¹) ^ C
Blueprint prop:base, proof line 1651: along a path through y, the scales where three fixed
basic atoms have transpose norm above s are polynomially many in log H + log s⁻¹.
theorem
TrilinearHT.Auto.tripleTail
(κ : LocalKernelClass)
(c₀ : ℕ)
(hc : 1 ≤ c₀)
:
∃ (C : ℕ) (Cr : ℝ),
0 ≤ Cr ∧ ∀ {d : Fin 3 → ℕ} (H r₀ δ y : ℝ) (B : (i : Fin 3) → QuadraticChartData (d i)) (φ : Fin 4 → ℝ → ℂ) (m : Fin 4),
(∀ (i : Fin 3), QuadraticChartComplexity c₀ H (B i)) →
(∀ (i : Fin 3) (u : ℝ), quadraticChartAtom (B i) u = φ (m.succAbove i) (u + y)) →
0 < r₀ →
0 < δ →
δ ≤ 1 →
∀ (a : ℤ → ℝ) (w : ℤ → ℝ × ℝ → ℂ) (T : Finset ℤ),
(∀ n ∈ T, IsAdmissibleLocalKernel κ (a n) (r₀ * 2 ^ (-n)) (w n)) →
(∀ n ∈ T, y ∈ Set.Icc (a n) (a n + r₀ * 2 ^ (-n))) →
∑ n ∈ T with tripleNorm (w n) φ m y (r₀ * 2 ^ (-n)) ≤ δ, tripleNorm (w n) φ m y (r₀ * 2 ^ (-n)) ≤ δ * Cr * (Real.log H + Real.log δ⁻¹ + 1) ^ C
Blueprint prop:base, eq:triple-tail (line 1653): along a path through y, the transpose
norms of three fixed basic atoms that are at most δ sum to at most
δ poly(log H, log δ⁻¹).
Active cells (blueprint prop:base, lines 1655-1660) #
theorem
TrilinearHT.Auto.tripleNorm_eq_transposeNorm
{κ : LocalKernelClass}
{a₀ r : ℝ}
(hr : 0 < r)
{w : ℝ × ℝ → ℂ}
(hw : IsAdmissibleLocalKernel κ a₀ r w)
(m : Fin 4)
{φ : Fin 4 → ℝ → ℂ}
(hφ : ∀ (j : Fin 4), Measurable (φ j))
{B : ℝ}
(hB0 : 0 ≤ B)
(hB : ∀ (j : Fin 4), j ≠ m → ∀ (x : ℝ), ‖φ j x‖ ≤ B)
(y : ℝ)
:
The transpose norm is the doubled-kernel triple norm at every path point.
theorem
TrilinearHT.Auto.localProgressionForm_le_transposeNorm
{κ : LocalKernelClass}
{a₀ r : ℝ}
(hr : 0 < r)
{w : ℝ × ℝ → ℂ}
(hw : IsAdmissibleLocalKernel κ a₀ r w)
(m : Fin 4)
{F : Fin 4 → ℝ → ℂ}
(hF : ∀ (j : Fin 4), Measurable (F j))
{B : ℝ}
(hB0 : 0 ≤ B)
(hB : ∀ (j : Fin 4), j ≠ m → ∀ (x : ℝ), ‖F j x‖ ≤ B)
(hFm : MeasureTheory.MemLp (F m) 2 (normalizedIntervalMeasure a₀ r))
:
‖localProgressionForm r w F‖ ≤ (MeasureTheory.eLpNorm (F m) 2 (normalizedIntervalMeasure a₀ r)).toReal * transposeNorm r w m F
|H_I(F)| ≤ ‖F_m‖_{2,I} A_I for bounded slots other than m.
theorem
TrilinearHT.Auto.tripleTranspose_congr
{κ : LocalKernelClass}
{a₀ r : ℝ}
(hr : 0 < r)
{w : ℝ × ℝ → ℂ}
(hw : IsAdmissibleLocalKernel κ a₀ r w)
(m : Fin 4)
{φ ψ : Fin 4 → ℝ → ℂ}
(h : ∀ (j : Fin 4), j ≠ m → ∀ x ∈ Set.Ico a₀ (a₀ + r), φ j x = ψ j x)
:
The transposed function only sees the slots other than m inside the cell.
theorem
TrilinearHT.Auto.localProgressionForm_slot_sum_le
{κ : LocalKernelClass}
{a₀ r : ℝ}
(hr : 0 < r)
{w : ℝ × ℝ → ℂ}
(hw : IsAdmissibleLocalKernel κ a₀ r w)
{F : Fin 4 → ℝ → ℂ}
(hF : ∀ (j : Fin 4), Measurable (F j))
(hFf : ∀ (j : Fin 4), MeasureTheory.eLpNorm (F j) 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤)
(k : Fin 4)
{L : Type u_1}
[Fintype L]
(c : L → ℂ)
(φ : L → ℝ → ℂ)
(hφ : ∀ (v : L), Measurable (φ v))
(hφf : ∀ (v : L), MeasureTheory.eLpNorm (φ v) 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤)
(hk : F k = fun (x : ℝ) => ∑ v : L, c v * φ v x)
:
‖localProgressionForm r w F‖ ≤ ∑ v : L, ‖c v‖ * ‖localProgressionForm r w (Function.update F k (φ v))‖
Expansion of one slot given as a finite combination.
noncomputable def
TrilinearHT.Auto.tripleSlots
(F : Fin 4 → ℝ → ℂ)
(m : Fin 4)
(f : Fin 3 → ℝ → ℂ)
:
The tuple with the three slots other than m replaced.
Equations
- TrilinearHT.Auto.tripleSlots F m f = Function.update (Function.update (Function.update F (m.succAbove 0) (f 0)) (m.succAbove 1) (f 1)) (m.succAbove 2) (f 2)
Instances For
theorem
TrilinearHT.Auto.localProgressionForm_triple_le
{κ : LocalKernelClass}
{a₀ r : ℝ}
(hr : 0 < r)
{w : ℝ × ℝ → ℂ}
(hw : IsAdmissibleLocalKernel κ a₀ r w)
(m : Fin 4)
{F : Fin 4 → ℝ → ℂ}
(hF : ∀ (j : Fin 4), Measurable (F j))
(hFm : MeasureTheory.MemLp (F m) 2 (normalizedIntervalMeasure a₀ r))
{L : Type u_1}
[Fintype L]
(c : Fin 3 → L → ℂ)
(φ : Fin 3 → L → ℝ → ℂ)
(hφ : ∀ (i : Fin 3) (v : L), Measurable (φ i v))
(hφb : ∀ (i : Fin 3) (v : L) (x : ℝ), ‖φ i v x‖ ≤ 1)
(hFs : ∀ (i : Fin 3), F (m.succAbove i) = fun (x : ℝ) => ∑ v : L, c i v * φ i v x)
:
‖localProgressionForm r w F‖ ≤ ∑ v₀ : L,
∑ v₁ : L,
∑ v₂ : L,
‖c 0 v₀‖ * ‖c 1 v₁‖ * ‖c 2 v₂‖ * ((MeasureTheory.eLpNorm (F m) 2 (normalizedIntervalMeasure a₀ r)).toReal * transposeNorm r w m (tripleSlots F m ![φ 0 v₀, φ 1 v₁, φ 2 v₂]))
Blueprint prop:base, line 1657: expanding the three slots other than m, each a finite
combination of bounded atoms, bounds the form by the coefficient products times the transpose
norms of the atom triples against the fourth slot.
theorem
TrilinearHT.Auto.cells_triple_reindex
(κ : LocalKernelClass)
{d : Fin 3 → ℕ}
(G : RealDyadicGrid)
(cells : Finset (ℤ × ℤ))
(w : ℤ × ℤ → ℝ × ℝ → ℂ)
(hw : ∀ I ∈ cells, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I))
(y : ℝ)
(B : (i : Fin 3) → QuadraticChartData (d i))
(hBb : ∀ (i : Fin 3), IsBoundedQuadraticChart (B i))
(m : Fin 4)
(Φ : ℤ × ℤ → Fin 4 → ℝ → ℂ)
(hΦ :
∀ I ∈ cells,
y ∈ dyadicGridCell G I.1 I.2 →
∀ (i : Fin 3), ∀ x ∈ dyadicGridCell G I.1 I.2, Φ I (m.succAbove i) x = quadraticChartAtom (B i) (x - y))
:
∃ (T : Finset ℤ) (a : ℤ → ℝ) (w' : ℤ → ℝ × ℝ → ℂ) (φ : Fin 4 → ℝ → ℂ),
(∀ (i : Fin 3), φ (m.succAbove i) = fun (x : ℝ) => quadraticChartAtom (B i) (x - y)) ∧ (∀ n ∈ T, IsAdmissibleLocalKernel κ (a n) (G.baseLength * 2 ^ (-n)) (w' n)) ∧ (∀ n ∈ T, y ∈ Set.Icc (a n) (a n + G.baseLength * 2 ^ (-n))) ∧ ∀ (P : ℝ → Prop) (F : ℝ → ℝ),
∑ I ∈ cells with y ∈ dyadicGridCell G I.1 I.2 ∧ P (transposeNorm (dyadicGridLength G I.1) (w I) m (Φ I)),
F (transposeNorm (dyadicGridLength G I.1) (w I) m (Φ I)) = ∑ n ∈ T with P (tripleNorm (w' n) φ m y (G.baseLength * 2 ^ (-n))),
F (tripleNorm (w' n) φ m y (G.baseLength * 2 ^ (-n)))
Reindex the cells through one point by depth and transport their chart triples. The identity applies to every filtered weighted sum, including tails and counts.
theorem
TrilinearHT.Auto.cells_tripleTail
(κ : LocalKernelClass)
(c₀ : ℕ)
(hc : 1 ≤ c₀)
:
∃ (C : ℕ) (Cr : ℝ),
0 ≤ Cr ∧ ∀ {d : Fin 3 → ℕ} (G : RealDyadicGrid) (cells : Finset (ℤ × ℤ)) (w : ℤ × ℤ → ℝ × ℝ → ℂ),
(∀ I ∈ cells, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) →
∀ (H δ y : ℝ) (B : (i : Fin 3) → QuadraticChartData (d i)),
(∀ (i : Fin 3), QuadraticChartComplexity c₀ H (B i)) →
(∀ (i : Fin 3), IsBoundedQuadraticChart (B i)) →
0 < δ →
δ ≤ 1 →
∀ (m : Fin 4) (Φ : ℤ × ℤ → Fin 4 → ℝ → ℂ),
(∀ I ∈ cells,
y ∈ dyadicGridCell G I.1 I.2 →
∀ (i : Fin 3),
∀ x ∈ dyadicGridCell G I.1 I.2, Φ I (m.succAbove i) x = quadraticChartAtom (B i) (x - y)) →
∑ I ∈ cells with
y ∈ dyadicGridCell G I.1 I.2 ∧ transposeNorm (dyadicGridLength G I.1) (w I) m (Φ I) ≤ δ,
transposeNorm (dyadicGridLength G I.1) (w I) m (Φ I) ≤ δ * Cr * (Real.log H + Real.log δ⁻¹ + 1) ^ C
Blueprint eq:triple-tail for a finite collection of dyadic cells: the cells through y
whose triple, a fixed chart triple near the path, has transpose norm at most δ contribute at
most δ poly(log H, log δ⁻¹).
theorem
TrilinearHT.Auto.cells_tripleCount
(κ : LocalKernelClass)
(c₀ : ℕ)
(hc : 1 ≤ c₀)
:
∃ (C : ℕ),
1 ≤ C ∧ ∀ {d : Fin 3 → ℕ} (G : RealDyadicGrid) (cells : Finset (ℤ × ℤ)) (w : ℤ × ℤ → ℝ × ℝ → ℂ),
(∀ I ∈ cells, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) →
∀ (H δ y : ℝ) (B : (i : Fin 3) → QuadraticChartData (d i)),
(∀ (i : Fin 3), QuadraticChartComplexity c₀ H (B i)) →
(∀ (i : Fin 3), IsBoundedQuadraticChart (B i)) →
0 < δ →
δ ≤ 1 →
∀ (m : Fin 4) (Φ : ℤ × ℤ → Fin 4 → ℝ → ℂ),
(∀ I ∈ cells,
y ∈ dyadicGridCell G I.1 I.2 →
∀ (i : Fin 3),
∀ x ∈ dyadicGridCell G I.1 I.2, Φ I (m.succAbove i) x = quadraticChartAtom (B i) (x - y)) →
↑{I ∈ cells |
y ∈ dyadicGridCell G I.1 I.2 ∧ δ < transposeNorm (dyadicGridLength G I.1) (w I) m (Φ I)}.card ≤ ↑C * (216 * Real.log H + Real.log (sliceConst κ) + 2 * Real.log δ⁻¹) ^ C
Blueprint prop:base, line 1655: the cells through y whose triple, a fixed chart triple
near the path, has transpose norm above δ are polynomially many in log H + log δ⁻¹.
theorem
TrilinearHT.Auto.AccSetup.accurateFit
(κ : LocalKernelClass)
:
∃ (c₂ : ℕ) (C : ℕ),
1 ≤ c₂ ∧ 1 ≤ C ∧ ∀ (q : ℝ),
2 < q →
∃ (Cq : ℝ),
0 < Cq ∧ ∀ (S : AccSetup),
S.c₂ = c₂ →
S.q = q →
S.B = fitBudget Cq C S.k →
1 ≤ S.k →
Measurable S.f →
(∀ c ∈ dyadicFiniteTree S.G S.J S.N,
c = S.J ∨ 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) →
S.K₀ ≤ S.N →
(∀ (I : ℤ × ℤ),
IsAdmissibleLocalKernel κ (dyadicGridLeft S.G I.1 I.2) (dyadicGridLength S.G I.1)
(S.w I)) →
16 * S.B ^ 2 < ↑S.M →
S.Hyp ∧ dyadicRootLength S.G S.tree.roots ≤ 4 / 3 * dyadicGridLength S.G S.J.1 ∧ ∀ I ∈ dyadicFiniteTree S.G S.J S.Nc,
S.tree.seg I ∈ S.tree.roots ∧ S.cell I ⊆ S.cell (S.tree.seg I) ∧ FormSmall (dyadicGridLeft S.G I.1 I.2) (dyadicGridLength S.G I.1) (S.w I)
S.e S.q (S.res I (S.tree.st I).1 (S.tree.st I).2) (Real.exp (-↑S.k))
Blueprint prop:base, proof lines 1634-1638: the tuple-specific accurate fits. With the
detection budget of lem:detection at accuracy e^{-k} and a cap M > 16 B², the greedy
attempts satisfy the hypotheses, their restart roots have total length at most 4/3 |J|, and on
every coarse cell the residual of the delayed fine projection is e^{-k}-small.
theorem
TrilinearHT.Auto.AccSetup.predictorCover_system
{κ : LocalKernelClass}
(S : AccSetup)
(K : ℤ × ℤ)
{a i k b : Fin 4}
{B Dl ε : ℝ}
{d e : ℕ}
{A : QuadraticChartData d}
{A' : QuadraticChartData e}
{J' : ℤ × ℤ}
(h : PredictorCover κ S.P₀ a i k b B Dl ε A A' J')
:
PredictorCover κ (S.system K) a i k b B Dl ε A A' J'
A predictor cover persists in the accurate-fit system, whose predictor labels are those of the underlying system.
theorem
TrilinearHT.Auto.dyadicGridCell_nested_of_common
(G : RealDyadicGrid)
{I A B : ℤ × ℤ}
(hA : dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G A.1 A.2)
(hB : dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G B.1 B.2)
:
dyadicGridCell G A.1 A.2 ⊆ dyadicGridCell G B.1 B.2 ∨ dyadicGridCell G B.1 B.2 ⊆ dyadicGridCell G A.1 A.2
Two dyadic cells containing a common cell are nested.
def
TrilinearHT.Auto.LowList.Inh
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ : ℕ}
{H : ℝ}
(X : LowList G J N R c₀ H)
(K : ℤ × ℤ)
(l : X.Λ)
:
A label is inherited by the subroot K when it is available below K but born strictly
above.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
TrilinearHT.Auto.LowList.inhBirth
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ : ℕ}
{H : ℝ}
(X : LowList G J N R c₀ H)
(K : ℤ × ℤ)
(l : X.Λ)
:
The original birth of an inherited label.
Equations
- X.inhBirth K l = if h : X.Inh K l then X.birth (Classical.choose h) l else K
Instances For
noncomputable def
TrilinearHT.Auto.LowList.restrictChart
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ : ℕ}
{H : ℝ}
(X : LowList G J N R c₀ H)
(K c : ℤ × ℤ)
(l : X.Λ)
:
(d : ℕ) × QuadraticChartData d
The chart of the restriction: inherited labels keep the chart of their original birth.
Equations
Instances For
theorem
TrilinearHT.Auto.LowList.restrictChart_good
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ : ℕ}
{H : ℝ}
(X : LowList G J N R c₀ H)
(K c : ℤ × ℤ)
(l : X.Λ)
:
1 ≤ (X.restrictChart K c l).fst ∧ QuadraticChartComplexity c₀ H (X.restrictChart K c l).snd ∧ IsBoundedQuadraticChart (X.restrictChart K c l).snd
theorem
TrilinearHT.Auto.LowList.birth_of_inh
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ : ℕ}
{H : ℝ}
(X : LowList G J N R c₀ H)
{K I : ℤ × ℤ}
{l : X.Λ}
(hav : X.avail I l)
(hIK : dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G K.1 K.2)
(hb : ¬dyadicGridCell G (X.birth I l).1 (X.birth I l).2 ⊆ dyadicGridCell G K.1 K.2)
:
dyadicGridCell G K.1 K.2 ⊆ dyadicGridCell G (X.birth I l).1 (X.birth I l).2
Every available cell lies below the subroot or its birth contains it.
theorem
TrilinearHT.Auto.LowList.inhBirth_eq
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ : ℕ}
{H : ℝ}
(X : LowList G J N R c₀ H)
{K I : ℤ × ℤ}
{l : X.Λ}
(hav : X.avail I l)
(hIK : dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G K.1 K.2)
(hb : ¬dyadicGridCell G (X.birth I l).1 (X.birth I l).2 ⊆ dyadicGridCell G K.1 K.2)
:
noncomputable def
TrilinearHT.Auto.LowList.restrict
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ : ℕ}
{H : ℝ}
(X : LowList G J N R c₀ H)
(K : ℤ × ℤ)
(hK : K ∈ dyadicFiniteTree G J N)
:
LowList G J N K c₀ H
Restriction of a low list to a subroot K: coefficients below K, and labels inherited from
above K are treated as born at K (blueprint prop:base, line 1628).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TrilinearHT.Auto.LowList.restrict_atom
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ : ℕ}
{H : ℝ}
(X : LowList G J N R c₀ H)
(K : ℤ × ℤ)
(hK : K ∈ dyadicFiniteTree G J N)
{I : ℤ × ℤ}
{l : X.Λ}
(hav : X.avail I l)
(hIK : dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G K.1 K.2)
:
theorem
TrilinearHT.Auto.LowList.restrict_val
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ : ℕ}
{H : ℝ}
(X : LowList G J N R c₀ H)
(K : ℤ × ℤ)
(hK : K ∈ dyadicFiniteTree G J N)
{I : ℤ × ℤ}
(hIK : dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G K.1 K.2)
(y : ℝ)
:
theorem
TrilinearHT.Auto.LowList.restrict_birth_sub
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ : ℕ}
{H : ℝ}
(X : LowList G J N R c₀ H)
(K : ℤ × ℤ)
(hK : K ∈ dyadicFiniteTree G J N)
{I : ℤ × ℤ}
{l : X.Λ}
(hav : X.avail I l)
(hIK : dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G K.1 K.2)
:
dyadicGridCell G ((X.restrict K hK).birth I l).1 ((X.restrict K hK).birth I l).2 ⊆
dyadicGridCell G (X.birth I l).1 (X.birth I l).2
theorem
TrilinearHT.Auto.LowList.restrict_chart_sigma
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ : ℕ}
{H : ℝ}
(X : LowList G J N R c₀ H)
(K : ℤ × ℤ)
(hK : K ∈ dyadicFiniteTree G J N)
{I : ℤ × ℤ}
{l : X.Λ}
(hav : X.avail I l)
(hIK : dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G K.1 K.2)
:
theorem
TrilinearHT.Auto.PredictorCover.congr_chart
{κ : LocalKernelClass}
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{V : Type}
[Fintype V]
{P : PathColumnSystem G J N V}
{a i k b : Fin 4}
{B Dl ε : ℝ}
{d d' e e' : ℕ}
{A : QuadraticChartData d}
{A₁ : QuadraticChartData d'}
{A' : QuadraticChartData e}
{A₁' : QuadraticChartData e'}
{J' : ℤ × ℤ}
(h1 : ⟨d, A⟩ = ⟨d', A₁⟩)
(h2 : ⟨e, A'⟩ = ⟨e', A₁'⟩)
(hc : PredictorCover κ P a i k b B Dl ε A A' J')
:
PredictorCover κ P a i k b B Dl ε A₁ A₁' J'
theorem
TrilinearHT.Auto.predSystem_cover_mono
(κ : LocalKernelClass)
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ c₁ : ℕ}
{H : ℝ}
(Xi Xk : LowList G J N R c₀ H)
(a i k b : Fin 4)
(B D : ℝ)
(pkg : (K K' : ℤ × ℤ) → (li : Xi.Λ) → (lk : Xk.Λ) → PredictorPackage κ (Xi.chart K li) (Xk.chart K' lk) a i k b B D c₁)
{ε : ℝ}
(hε0 : 0 < ε)
(hε1 : ε ≤ 1)
{d e : ℕ}
{A : QuadraticChartData d}
{A' : QuadraticChartData e}
{c c' : ℤ × ℤ}
(hc : c ∈ dyadicFiniteTree G J N)
(hcc' : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G c'.1 c'.2)
(h : PredictorCover κ (predSystem κ Xi Xk a i k b B D pkg hε0 hε1) a i k b B D ε A A' c')
:
PredictorCover κ (predSystem κ Xi Xk a i k b B D pkg hε0 hε1) a i k b B D ε A A' c
A predictor cover of the predictor system persists at smaller cells of the tree.
theorem
TrilinearHT.Auto.predSystem_cover_restrict
(κ : LocalKernelClass)
{G : RealDyadicGrid}
{J : ℤ × ℤ}
{N : ℕ}
{R : ℤ × ℤ}
{c₀ c₁ : ℕ}
{H : ℝ}
(Xi Xk : LowList G J N R c₀ H)
(a i k b : Fin 4)
(B D : ℝ)
(pkg : (K K' : ℤ × ℤ) → (li : Xi.Λ) → (lk : Xk.Λ) → PredictorPackage κ (Xi.chart K li) (Xk.chart K' lk) a i k b B D c₁)
{ε : ℝ}
(hε0 : 0 < ε)
(hε1 : ε ≤ 1)
(hD1 : 1 ≤ D)
(K : ℤ × ℤ)
(hK : K ∈ dyadicFiniteTree G J N)
{I : ℤ × ℤ}
{li : Xi.Λ}
{lk : Xk.Λ}
(hci : (Xi.restrict K hK).coef I li ≠ 0)
(hck : (Xk.restrict K hK).coef I lk ≠ 0)
:
PredictorCover κ (predSystem κ Xi Xk a i k b B D pkg hε0 hε1) a i k b B D ε
((Xi.restrict K hK).chart ((Xi.restrict K hK).birth I li) li)
((Xk.restrict K hK).chart ((Xk.restrict K hK).birth I lk) lk)
(jointBirth (Xi.restrict K hK) (Xk.restrict K hK) I li lk)
Blueprint prop:base, line 1628: at a restart root K the restricted low lists (inherited
labels born at K) are covered by the predictor system of the original lists.