Induction infrastructure for the AMNR tensors.

theorem AVenhance.Infra.Section4.amnrRec_contDiffOn {U : Set AmnrSpace} (hU : IsOpen U) {N : ℕ} {b : AmnrSpace → Homogenization.Vec 2} (hb : ContDiffOn ℝ (↑N) b U) {B f : Fin 2 → Fin 2 → AmnrSpace → ℝ} {g : Fin 2 → AmnrSpace → ℝ} (hB : ∀ (i p : Fin 2), ContDiffOn ℝ (↑N) (B i p) U) (hf : ∀ (i p : Fin 2), ContDiffOn ℝ (↑N) (f i p) U) (hg : ∀ (p : Fin 2), ContDiffOn ℝ (↑N) (g p) U) {A : ℕ → Fin 2 → AmnrSpace → ℝ} (hzero : ∀ (i : Fin 2), Set.EqOn (A 0 i) (fun (z : AmnrSpace) => ∑ p : Fin 2, f i p z * g p z) U) (hrec : ∀ r < N, ∀ (i : Fin 2), Set.EqOn (A (r + 1) i) (fun (z : AmnrSpace) => amnrOp b none (A r i) z - ∑ p : Fin 2, B i p z * A r p z) U) {r n : ℕ} (hr : n + r ≤ N) (i : Fin 2) : ContDiffOn ℝ (↑n) (A r i) U

Finite-order regularity propagated by the contraction recurrence. The premises describe its primitive factors and defining identities, not A bounds.

theorem AVenhance.Infra.Section4.amnrRec_word_succ {U : Set AmnrSpace} (hU : IsOpen U) {N : ℕ} {b : AmnrSpace → Homogenization.Vec 2} (hb : ContDiffOn ℝ (↑N) b U) {B f : Fin 2 → Fin 2 → AmnrSpace → ℝ} {g : Fin 2 → AmnrSpace → ℝ} (hB : ∀ (i p : Fin 2), ContDiffOn ℝ (↑N) (B i p) U) (hf : ∀ (i p : Fin 2), ContDiffOn ℝ (↑N) (f i p) U) (hg : ∀ (p : Fin 2), ContDiffOn ℝ (↑N) (g p) U) {A : ℕ → Fin 2 → AmnrSpace → ℝ} (hzero : ∀ (i : Fin 2), Set.EqOn (A 0 i) (fun (z : AmnrSpace) => ∑ p : Fin 2, f i p z * g p z) U) (hrec : ∀ r < N, ∀ (i : Fin 2), Set.EqOn (A (r + 1) i) (fun (z : AmnrSpace) => amnrOp b none (A r i) z - ∑ p : Fin 2, B i p z * A r p z) U) (r : ℕ) (w : List (Option (Fin 2))) (hw : w.length + (r + 1) ≤ N) (i : Fin 2) : Set.EqOn (amnrWord b w (A (r + 1) i)) (fun (z : AmnrSpace) => amnrWord b (w ++ [none]) (A r i) z - ∑ p : Fin 2, amnrWord b w (B i p * A r p) z) U

Differentiated recurrence for ordered words, with finite-order regularity proved from the primitive seed.

theorem AVenhance.Infra.Section4.amnrWord_sum_mul_L2_le {U : Set AmnrSpace} (hU : IsOpen U) {μ : MeasureTheory.Measure AmnrSpace} (hμ : μ.AbsolutelyContinuous (MeasureTheory.volume.restrict U)) {b : AmnrSpace → Homogenization.Vec 2} {M N : ℕ} (hMN : M ≤ N) (hb : ContDiffOn ℝ (↑M) b U) {f g : Fin 2 → AmnrSpace → ℝ} (hf : ∀ (p : Fin 2), ContDiffOn ℝ (↑M) (f p) U) (hg : ∀ (p : Fin 2), ContDiffOn ℝ (↑M) (g p) U) {S H F G : ℝ} (hS : 0 ≤ S) (hH : 0 ≤ H) (hF : 0 ≤ F) (hG : 0 ≤ G) (w : List (Option (Fin 2))) (hw : amnrBudget w ≤ M) (hfb : ∀ (p : Fin 2) (v : List (Option (Fin 2))), v.Sublist w → ∀ z ∈ U, |amnrWord b v (f p) z| ≤ F * amnrWeight S H v) (hgb : ∀ (p : Fin 2) (v : List (Option (Fin 2))), v.Sublist w → MeasureTheory.eLpNorm (amnrWord b v (g p)) 2 μ ≤ ENNReal.ofReal (G * amnrWeight S H v)) : MeasureTheory.eLpNorm (amnrWord b w fun (z : AmnrSpace) => ∑ p : Fin 2, f p z * g p z) 2 μ ≤ ENNReal.ofReal (2 ^ (N + 1) * F * G * amnrWeight S H w)

A two-coordinate contraction costs at most 2^(N+1) Leibniz terms. The smoothness order M can decrease along the recursion while N stays fixed.

theorem AVenhance.Infra.Section4.amnrBudget_sublist {v w : List (Option (Fin 2))} (h : v.Sublist w) : amnrBudget v ≤ amnrBudget w

Taking a subword cannot increase its weighted regularity budget.

theorem AVenhance.Infra.Section4.amnrRec_mixed_L2_le {U : Set AmnrSpace} (hU : IsOpen U) {μ : MeasureTheory.Measure AmnrSpace} (hμ : μ.AbsolutelyContinuous (MeasureTheory.volume.restrict U)) {N : ℕ} {b : AmnrSpace → Homogenization.Vec 2} (hb : ContDiffOn ℝ (↑N) b U) {B f : Fin 2 → Fin 2 → AmnrSpace → ℝ} {g : Fin 2 → AmnrSpace → ℝ} (hB : ∀ (i p : Fin 2), ContDiffOn ℝ (↑N) (B i p) U) (hf : ∀ (i p : Fin 2), ContDiffOn ℝ (↑N) (f i p) U) (hg : ∀ (p : Fin 2), ContDiffOn ℝ (↑N) (g p) U) {A : ℕ → Fin 2 → AmnrSpace → ℝ} (hzero : ∀ (i : Fin 2), Set.EqOn (A 0 i) (fun (z : AmnrSpace) => ∑ p : Fin 2, f i p z * g p z) U) (hrec : ∀ r < N, ∀ (i : Fin 2), Set.EqOn (A (r + 1) i) (fun (z : AmnrSpace) => amnrOp b none (A r i) z - ∑ p : Fin 2, B i p z * A r p z) U) {S H F G Cb : ℝ} (hS : 0 ≤ S) (hH : 0 ≤ H) (hF : 0 ≤ F) (hG : 0 ≤ G) (hCb : 0 ≤ Cb) (hfb : ∀ (i p : Fin 2) (w : List (Option (Fin 2))), IsAmnrMixedWord w → amnrBudget w ≤ N → ∀ z ∈ U, |amnrWord b w (f i p) z| ≤ F * amnrWeight S H w) (hgb : ∀ (p : Fin 2) (w : List (Option (Fin 2))), IsAmnrMixedWord w → amnrBudget w ≤ N → MeasureTheory.eLpNorm (amnrWord b w (g p)) 2 μ ≤ ENNReal.ofReal (G * amnrWeight S H w)) (hBb : ∀ (i p : Fin 2) (w : List (Option (Fin 2))), IsAmnrMixedWord w → amnrBudget w + 2 ≤ N → ∀ z ∈ U, |amnrWord b w (B i p) z| ≤ Cb * H * amnrWeight S H w) (r : ℕ) (w : List (Option (Fin 2))) (hw : IsAmnrMixedWord w) (hbudget : amnrBudget w + 2 * r ≤ N) (i : Fin 2) : MeasureTheory.eLpNorm (amnrWord b w (A r i)) 2 μ ≤ ENNReal.ofReal (2 ^ (N + 1) * F * G * (1 + 2 ^ (N + 1) * Cb) ^ r * H ^ r * amnrWeight S H w)

The complete higher mixed-derivative contraction induction. The seed is estimated from its primitive coefficient and gradient factors; no A bound is a premise. The order budget is checked in the base, the material shift, and every Leibniz factor at every level.

def AVenhance.Infra.Section4.amnrMixedWord (α : List (Fin 2)) (ℓ : ℕ) : List (Option (Fin 2))

Coordinate version of ∇^k D^ℓ: all k spatial letters are outside the ℓ material letters. No commutation of these operators is asserted.

Equations

• AVenhance.Infra.Section4.amnrMixedWord α ℓ = List.map some α ++ List.replicate ℓ none

theorem AVenhance.Infra.Section4.amnrMixedWord_mixed (α : List (Fin 2)) (ℓ : ℕ) : IsAmnrMixedWord (amnrMixedWord α ℓ)

theorem AVenhance.Infra.Section4.amnrMixedWord_budget (α : List (Fin 2)) (ℓ : ℕ) : amnrBudget (amnrMixedWord α ℓ) = α.length + 2 * ℓ

theorem AVenhance.Infra.Section4.amnrMixedWord_weight (S H : ℝ) (α : List (Fin 2)) (ℓ : ℕ) : amnrWeight S H (amnrMixedWord α ℓ) = S ^ α.length * H ^ ℓ