Section 11.2, part 2c: prop:base, statement and assembly

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 2c: prop:base, statement and assembly: sizes, triple tail, active cells (lines 1600-1623, 1643-1660) (lines 1598-1666) of blueprint/formalization_blueprint.tex.

theorem TrilinearHT.Auto.PairSmall.slots4_le_norm_mul {a₀ r : ℝ} {w : ℝ × ℝ → ℂ} {a i k b : Fin 4} (hai : a ≠ i) (hak : a ≠ k) (hab : a ≠ b) (hik : i ≠ k) (hib : i ≠ b) (hkb : k ≠ b) {η : ℝ} (hη : 0 ≤ η) {Fi Fk : ℝ → ℂ} (hp : PairSmall a₀ r w i k Fi Fk η) (hFi : Measurable Fi) (hFk : Measurable Fk) (Fa Fb : ℝ → ℂ) (hFa : Measurable Fa) (hFb : Measurable Fb) (hfa : MeasureTheory.eLpNorm Fa 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hfb : MeasureTheory.eLpNorm Fb 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) : ‖localProgressionForm r w (slots4 a i k Fa Fi Fk Fb)‖ ≤ (MeasureTheory.eLpNorm Fa 2 (normalizedIntervalMeasure a₀ r)).toReal * (MeasureTheory.eLpNorm Fb 2 (normalizedIntervalMeasure a₀ r)).toReal * η

Pair smallness bounds a four-slot form by the exact sizes of its two spectators.

theorem TrilinearHT.Auto.AccSetup.Hyp.f_fin {S : AccSetup} (h : S.Hyp) {c : ℤ × ℤ} (hc : c ∈ dyadicFiniteTree S.G S.J S.N) : MeasureTheory.eLpNorm S.f 2 (normalizedIntervalMeasure (dyadicGridLeft S.G c.1 c.2) (dyadicGridLength S.G c.1)) ≠ ⊤

The input has finite normalized L² norm on every tree cell (only the root normalization is used).

theorem TrilinearHT.Auto.AccSetup.phys_fin (S : AccSetup) (I : ℤ × ℤ) (a : ℕ → ℝ → ℂ) (n : ℕ) : MeasureTheory.eLpNorm (S.phys I a n) 2 (normalizedIntervalMeasure (dyadicGridLeft S.G I.1 I.2) (dyadicGridLength S.G I.1)) ≠ ⊤

The physical fine projections have finite normalized L² norm on every cell.

theorem TrilinearHT.Auto.LowList.val_bound {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {R : ℤ × ℤ} {c₀ : ℕ} {H : ℝ} (X : LowList G J N R c₀ H) (I : ℤ × ℤ) (y : ℝ) : ‖X.val I y‖ ≤ ↑(Fintype.card X.Λ)

theorem TrilinearHT.Auto.localProgressionForm_slots4_congr_a {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {a i k b : Fin 4} (hai : a ≠ i) (hak : a ≠ k) (hab : a ≠ b) (hik : i ≠ k) (hib : i ≠ b) (hkb : k ≠ b) {z₁ z₂ φ φ' zb : ℝ → ℂ} (hz₁ : Measurable z₁) (hz₂ : Measurable z₂) (hφ : Measurable φ) (hφ' : Measurable φ') (hzb : Measurable zb) (hz₁f : MeasureTheory.eLpNorm z₁ 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hz₂f : MeasureTheory.eLpNorm z₂ 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hφf : MeasureTheory.eLpNorm φ 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hφ'f : MeasureTheory.eLpNorm φ' 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hzbf : MeasureTheory.eLpNorm zb 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hae : z₁ =ᵐ[normalizedIntervalMeasure a₀ r] z₂) : localProgressionForm r w (slots4 a i k z₁ φ φ' zb) = localProgressionForm r w (slots4 a i k z₂ φ φ' zb)

Changing the slot-a input of slots4 almost everywhere on the cell does not change the form.

The delayed replacement of one high input on an accurate-fit root

noncomputable def TrilinearHT.Auto.predAccSetup (κ : LocalKernelClass) {G : RealDyadicGrid} {J : ℤ × ℤ} {N c₀ c₁ : ℕ} {H : ℝ} (Xi Xk : LowList G J N J c₀ H) (a i k b : Fin 4) (Bp D : ℝ) (pkg : (K K' : ℤ × ℤ) → (li : Xi.Λ) → (lk : Xk.Λ) → PredictorPackage κ (Xi.chart K li) (Xk.chart K' lk) a i k b Bp D c₁) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε ≤ 1) (K₀ M : ℕ) (f : ℝ → ℂ) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (q : ℝ) (kk c₂ : ℕ) (Bf : ℝ) : AccSetup

The accurate-fit setup of the high slot a over the predictor system of the low lists (blueprint prop:base, lines 1626 and 1634).

Equations

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

theorem TrilinearHT.Auto.replaceSlot (κ : LocalKernelClass) {G : RealDyadicGrid} {J : ℤ × ℤ} {N c₀ c₁ : ℕ} {H : ℝ} (Xi Xk : LowList G J N J c₀ H) (a i k b : Fin 4) (Bp D : ℝ) (pkg : (K K' : ℤ × ℤ) → (li : Xi.Λ) → (lk : Xk.Λ) → PredictorPackage κ (Xi.chart K li) (Xk.chart K' lk) a i k b Bp D c₁) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε ≤ 1) (hai : a ≠ i) (hak : a ≠ k) (hab : a ≠ b) (hik : i ≠ k) (hib : i ≠ b) (hkb : k ≠ b) (hD1 : 1 ≤ D) (K₀ M : ℕ) (f : ℝ → ℂ) (w : ℤ × ℤ → ℝ × ℝ → ℂ) (q : ℝ) (k' c₂ : ℕ) (Bf : ℝ) (h : (predAccSetup κ Xi Xk a i k b Bp D pkg hε0 hε1 K₀ M f w q k' c₂ Bf).Hyp) (hw : ∀ (I : ℤ × ℤ), IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (w I)) {K : ℤ × ℤ} (hKr : K ∈ (predAccSetup κ Xi Xk a i k b Bp D pkg hε0 hε1 K₀ M f w q k' c₂ Bf).tree.roots) {R : ℤ × ℤ} (hR : R ∈ dyadicFiniteTree G J N) (T : Finset (ℤ × ℤ)) (hT : ∀ I ∈ T, I ∈ dyadicFiniteTree G J (predAccSetup κ Xi Xk a i k b Bp D pkg hε0 hε1 K₀ M f w q k' c₂ Bf).Nc ∧ (predAccSetup κ Xi Xk a i k b Bp D pkg hε0 hε1 K₀ M f w q k' c₂ Bf).tree.seg I = K ∧ dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G R.1 R.2) {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) : have S := predAccSetup κ Xi Xk a i k b Bp D pkg hε0 hε1 K₀ M f w q k' c₂ Bf; ∑ I ∈ T, 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 (S.phys I (S.tree.st I).1 (S.tree.st I).2) (Xi.val I) (Xk.val I) (zb I))‖ ≤ ↑(Fintype.card Xi.Λ) * ↑(Fintype.card Xk.Λ) * (2 * Real.exp (-Bp) * (2 * (compressionOneConst ((S.system K).rooted R) + ↑K₀) + 1) * Kb + D ^ 2 * (delayConst κ * (2⁻¹ ^ K₀ + (1 + ↑K₀) * √ε) * (1 + D) ^ 4 * Kb)) * √(∫ (y : ℝ) in dyadicGridCell G R.1 R.2, ‖↑↑S.input y‖ ^ 2) * √(∫ (y : ℝ) in dyadicGridCell G R.1 R.2, ‖Fb y‖ ^ 2)

Blueprint prop:base, proof lines 1626-1641: on the segment of an accurate-fit root K, the input in slot a is replaced by the delayed physical projection of the accurate-fit system, with the absolute scale-sum error of lem:predictors and lem:delay.

Opponent algebra for the replaced tuple

theorem TrilinearHT.Auto.IsAdmissibleOpponent.neg {G : RealDyadicGrid} {J : ℤ × ℤ} {F : ℝ → ℂ} {z : ℤ × ℤ → ℝ → ℂ} {K : ℝ} (h : IsAdmissibleOpponent G J F z K) : IsAdmissibleOpponent G J F (fun (I : ℤ × ℤ) (y : ℝ) => -z I y) K

theorem TrilinearHT.Auto.HasDepthEnergy.neg {G : RealDyadicGrid} {J : ℤ × ℤ} {F : ℝ → ℂ} {z : ℤ × ℤ → ℝ → ℂ} {K : ℝ} (h : HasDepthEnergy G J F z K) : HasDepthEnergy G J F (fun (I : ℤ × ℤ) (y : ℝ) => -z I y) K

theorem TrilinearHT.Auto.IsAdmissibleOpponent.of_zero_or {G : RealDyadicGrid} {J : ℤ × ℤ} {F : ℝ → ℂ} {z z' : ℤ × ℤ → ℝ → ℂ} {K : ℝ} (h : IsAdmissibleOpponent G J F z K) (hz : ∀ (I : ℤ × ℤ), z' I = z I ∨ z' I = 0) : IsAdmissibleOpponent G J F z' K

Discarding the opponent on some cells keeps it admissible.

theorem TrilinearHT.Auto.HasDepthEnergy.of_zero_or {G : RealDyadicGrid} {J : ℤ × ℤ} {F : ℝ → ℂ} {z z' : ℤ × ℤ → ℝ → ℂ} {K : ℝ} (h : HasDepthEnergy G J F z K) (hz : ∀ (I : ℤ × ℤ), z' I = z I ∨ z' I = 0) : HasDepthEnergy G J F z' K

theorem TrilinearHT.Auto.localProgressionForm_slots4_congr_b {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {a i k b : Fin 4} (hai : a ≠ i) (hak : a ≠ k) (hab : a ≠ b) (hik : i ≠ k) (hib : i ≠ b) (hkb : k ≠ b) {za φ φ' z₁ z₂ : ℝ → ℂ} (hza : Measurable za) (hφ : Measurable φ) (hφ' : Measurable φ') (hz₁ : Measurable z₁) (hz₂ : Measurable z₂) (hzaf : MeasureTheory.eLpNorm za 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hφf : MeasureTheory.eLpNorm φ 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hφ'f : MeasureTheory.eLpNorm φ' 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hz₁f : MeasureTheory.eLpNorm z₁ 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hz₂f : MeasureTheory.eLpNorm z₂ 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hae : z₁ =ᵐ[normalizedIntervalMeasure a₀ r] z₂) : localProgressionForm r w (slots4 a i k za φ φ' z₁) = localProgressionForm r w (slots4 a i k za φ φ' z₂)

Changing the opponent slot of slots4 almost everywhere on the cell does not change the form.

theorem TrilinearHT.Auto.localProgressionForm_slots4_sub_common {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {a i k b : Fin 4} (hai : a ≠ i) (hak : a ≠ k) (hab : a ≠ b) (hik : i ≠ k) (hib : i ≠ b) (hkb : k ≠ b) {u v c φ φ' zb : ℝ → ℂ} (hu : Measurable u) (hv : Measurable v) (hc : Measurable c) (hφ : Measurable φ) (hφ' : Measurable φ') (hzb : Measurable zb) (huf : MeasureTheory.eLpNorm u 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hvf : MeasureTheory.eLpNorm v 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hcf : MeasureTheory.eLpNorm c 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hφf : MeasureTheory.eLpNorm φ 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hφ'f : MeasureTheory.eLpNorm φ' 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hzbf : MeasureTheory.eLpNorm zb 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) : localProgressionForm r w (slots4 a i k (u - c) φ φ' zb) - localProgressionForm r w (slots4 a i k (v - c) φ φ' zb) = localProgressionForm r w (slots4 a i k u φ φ' zb) - localProgressionForm r w (slots4 a i k v φ φ' zb)

Linearity in slot a: subtracting a common term.

theorem TrilinearHT.Auto.compressionOneConst_rooted {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) (R R' : ℤ × ℤ) : compressionOneConst (P.rooted R) = compressionOneConst (P.rooted R')

theorem TrilinearHT.Auto.HasDepthEnergy.congr_cell {G : RealDyadicGrid} {J : ℤ × ℤ} {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 → ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → z' I y = z I y) : HasDepthEnergy G J F z' K

theorem TrilinearHT.Auto.PathColumnSystem.delayed_opponent {G : RealDyadicGrid} {J : ℤ × ℤ} {N : ℕ} {V : Type} [Fintype V] (P : PathColumnSystem G J N V) {R : ℤ × ℤ} (hR : R ∈ dyadicFiniteTree G J N) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (K₀ : ℕ) : have z := fun (I : ℤ × ℤ) => if I.1 + ↑K₀ ≤ J.1 + ↑N then (P.family R hR).delayed f K₀ I else 0; (∀ (I : ℤ × ℤ), Measurable (z I) ∧ MeasureTheory.MemLp (z I) 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) ∧ ∀ J' ∈ dyadicFiniteTree G J N, dyadicGridCell G J'.1 J'.2 ⊆ dyadicGridCell G R.1 R.2 → IsAdmissibleOpponent G J' (↑↑f) z (2 * (compressionOneConst (P.rooted R) + ↑K₀)) ∧ HasDepthEnergy G J' (↑↑f) z 1

The delayed projection of a path-uniform column system, discarded on cells too deep for the delay, is an admissible opponent with depth energy one on every tree cell below the root of its family (blueprint lem:delay, sequential replacement).