A finite, exhaustive index set for the bounded canonical jet budget.

def AVenhance.Infra.Section4.amnrSpatialWords : ℕ → Finset (List (Fin 2))

All ordered two-dimensional spatial words of an exact length.

Equations

• AVenhance.Infra.Section4.amnrSpatialWords 0 = {[]}
• AVenhance.Infra.Section4.amnrSpatialWords n.succ = Finset.univ.biUnion fun (i : Fin 2) => Finset.image (List.cons i) (AVenhance.Infra.Section4.amnrSpatialWords n)

@[simp]

theorem AVenhance.Infra.Section4.amnrSpatialWords_mem (α : List (Fin 2)) (n : ℕ) : α ∈ amnrSpatialWords n ↔ α.length = n

def AVenhance.Infra.Section4.amnrCanonicalSamples (N cut : ℕ) : Finset (List (Fin 2) × ℕ)

The finite sample contains precisely the admissible canonical jets.

Equations

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

@[simp]

theorem AVenhance.Infra.Section4.amnrCanonicalSamples_mem (α : List (Fin 2)) (r N cut : ℕ) : (α, r) ∈ amnrCanonicalSamples N cut ↔ α.length + 2 * r ≤ N ∧ r ≤ cut

noncomputable def AVenhance.Infra.Section4.amnrCanonicalEnvelope (N cut : ℕ) (S H : ℝ) (b : AmnrSpace → Homogenization.Vec 2) (f : AmnrSpace → ℝ) (z : AmnrSpace) : ℝ

Normalizing and summing the finite canonical jet family gives a pointwise majorant without replacing an L2 estimate by a pointwise assumption.

Equations

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

theorem AVenhance.Infra.Section4.amnrCanonicalEnvelope_nonneg {S H : ℝ} (hS : 0 ≤ S) (hH : 0 ≤ H) (N cut : ℕ) (b : AmnrSpace → Homogenization.Vec 2) (f : AmnrSpace → ℝ) (z : AmnrSpace) : 0 ≤ amnrCanonicalEnvelope N cut S H b f z

theorem AVenhance.Infra.Section4.amnrCanonicalEnvelope_dominates {S H : ℝ} (hS : 0 < S) (hH : 0 < H) (N cut : ℕ) (b : AmnrSpace → Homogenization.Vec 2) (f : AmnrSpace → ℝ) (z : AmnrSpace) (α : List (Fin 2)) (r : ℕ) (hbudget : α.length + 2 * r ≤ N) (hcut : r ≤ cut) : |amnrWord b (amnrMixedWord α r) f z| ≤ amnrCanonicalEnvelope N cut S H b f z * amnrWeight S H (amnrMixedWord α r)