Calculus infrastructure for the AMNR tensors.

The mixed calculus below keeps spatial and material operations ordered.

def AVenhance.Infra.Section4.amnrSplits : List (Option (Fin 2)) → List (List (Option (Fin 2)) × List (Option (Fin 2)))

Ordered Leibniz splittings; each letter goes to exactly one factor.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Section4.amnrSplits [] = [([], [])]

theorem AVenhance.Infra.Section4.amnrSplits_length (w : List (Option (Fin 2))) : (amnrSplits w).length = 2 ^ w.length

theorem AVenhance.Infra.Section4.amnrSplits_sublist (w : List (Option (Fin 2))) (q : List (Option (Fin 2)) × List (Option (Fin 2))) (hq : q ∈ amnrSplits w) : q.1.Sublist w ∧ q.2.Sublist w ∧ q.1.length + q.2.length = w.length

theorem AVenhance.Infra.Section4.Calculus.amnrList_differentiable (L : List (AmnrSpace → ℝ)) (z : AmnrSpace) (h : ∀ f ∈ L, DifferentiableAt ℝ f z) : DifferentiableAt ℝ L.sum z

theorem AVenhance.Infra.Section4.Calculus.amnrOp_listSum {b : AmnrSpace → Homogenization.Vec 2} (d : Option (Fin 2)) (L : List (AmnrSpace → ℝ)) (z : AmnrSpace) (hL : ∀ f ∈ L, DifferentiableAt ℝ f z) : amnrOp b d L.sum z = (List.map (fun (f : AmnrSpace → ℝ) => amnrOp b d f z) L).sum

theorem AVenhance.Infra.Section4.amnrWord_mul {U : Set AmnrSpace} (hU : IsOpen U) {N : ℕ} {b : AmnrSpace → Homogenization.Vec 2} (hb : ContDiffOn ℝ (↑N) b U) {f g : AmnrSpace → ℝ} (hf : ContDiffOn ℝ (↑N) f U) (hg : ContDiffOn ℝ (↑N) g U) (w : List (Option (Fin 2))) (hw : w.length ≤ N) : Set.EqOn (amnrWord b w (f * g)) (fun (z : AmnrSpace) => (List.map (fun (q : List (Option (Fin 2)) × List (Option (Fin 2))) => amnrWord b q.1 f z * amnrWord b q.2 g z) (amnrSplits w)).sum) U

The exact mixed Leibniz expansion, derived from directional calculus.

def AVenhance.Infra.Section4.amnrWeight (S H : ℝ) (w : List (Option (Fin 2))) : ℝ

Radius weights associated with an ordered mixed derivative.

Equations

• AVenhance.Infra.Section4.amnrWeight S H w = (List.map (fun (d : Option (Fin 2)) => match d with | none => H | some val => S) w).prod

theorem AVenhance.Infra.Section4.amnrWeight_nonneg {S H : ℝ} (hS : 0 ≤ S) (hH : 0 ≤ H) (w : List (Option (Fin 2))) : 0 ≤ amnrWeight S H w

theorem AVenhance.Infra.Section4.amnrWeight_split (S H : ℝ) (w : List (Option (Fin 2))) (q : List (Option (Fin 2)) × List (Option (Fin 2))) (hq : q ∈ amnrSplits w) : amnrWeight S H q.1 * amnrWeight S H q.2 = amnrWeight S H w

def AVenhance.Infra.Section4.IsAmnrMixedWord (w : List (Option (Fin 2))) : Prop

Spatial derivatives outside, material derivatives inside, as in the source.

Equations

• AVenhance.Infra.Section4.IsAmnrMixedWord w = List.Pairwise (fun (a b : Option (Fin 2)) => a = none → b = none) w

theorem AVenhance.Infra.Section4.IsAmnrMixedWord.split {w : List (Option (Fin 2))} (hw : IsAmnrMixedWord w) {q : List (Option (Fin 2)) × List (Option (Fin 2))} (hq : q ∈ amnrSplits w) : IsAmnrMixedWord q.1 ∧ IsAmnrMixedWord q.2

A splitting never changes the order of differentiation on either factor.

def AVenhance.Infra.Section4.amnrBudget (w : List (Option (Fin 2))) : ℕ

Material derivatives cost two units in the approved finite-order budget.

Equations

• AVenhance.Infra.Section4.amnrBudget w = (List.map (fun (d : Option (Fin 2)) => match d with | none => 2 | some val => 1) w).sum

theorem AVenhance.Infra.Section4.amnrBudget_length_le (w : List (Option (Fin 2))) : w.length ≤ amnrBudget w

theorem AVenhance.Infra.Section4.amnrBudget_split (w : List (Option (Fin 2))) (q : List (Option (Fin 2)) × List (Option (Fin 2))) (hq : q ∈ amnrSplits w) : amnrBudget q.1 + amnrBudget q.2 = amnrBudget w

theorem AVenhance.Infra.Section4.amnrL2_listSum_le (L : List (AmnrSpace → ℝ)) (μ : MeasureTheory.Measure AmnrSpace) : MeasureTheory.eLpNorm L.sum 2 μ ≤ (List.map (fun (f : AmnrSpace → ℝ) => MeasureTheory.eLpNorm f 2 μ) L).sum

The L2 triangle inequality for a list, retaining duplicate Leibniz terms.

theorem AVenhance.Infra.Section4.amnrL2_mul_le {U : Set AmnrSpace} (hU : IsOpen U) {μ : MeasureTheory.Measure AmnrSpace} (hμ : μ.AbsolutelyContinuous (MeasureTheory.volume.restrict U)) {f g : AmnrSpace → ℝ} (hf : ContinuousOn f U) (hg : ContinuousOn g U) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ z ∈ U, |f z| ≤ C) : MeasureTheory.eLpNorm (f * g) 2 μ ≤ ENNReal.ofReal C * MeasureTheory.eLpNorm g 2 μ

A bounded smooth multiplier acts on the L2 norm, with an explicit constant.

theorem AVenhance.Infra.Section4.amnrWord_mul_L2_le {U : Set AmnrSpace} (hU : IsOpen U) {μ : MeasureTheory.Measure AmnrSpace} (hμ : μ.AbsolutelyContinuous (MeasureTheory.volume.restrict U)) {b : AmnrSpace → Homogenization.Vec 2} {f g : AmnrSpace → ℝ} {N : ℕ} (hb : ContDiffOn ℝ (↑N) b U) (hf : ContDiffOn ℝ (↑N) f U) (hg : ContDiffOn ℝ (↑N) g 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 ≤ N) (hfb : ∀ (v : List (Option (Fin 2))), v.Sublist w → ∀ z ∈ U, |amnrWord b v f z| ≤ F * amnrWeight S H v) (hgb : ∀ (v : List (Option (Fin 2))), v.Sublist w → MeasureTheory.eLpNorm (amnrWord b v g) 2 μ ≤ ENNReal.ofReal (G * amnrWeight S H v)) : MeasureTheory.eLpNorm (amnrWord b w (f * g)) 2 μ ≤ ENNReal.ofReal (2 ^ w.length * F * G * amnrWeight S H w)

Quantitative mixed Leibniz rule. The two factors consume complementary budgets, including the two-unit cost of each material derivative.

theorem AVenhance.Infra.Section4.amnrWord_congr {U : Set AmnrSpace} (hU : IsOpen U) {b : AmnrSpace → Homogenization.Vec 2} {f g : AmnrSpace → ℝ} (hfg : Set.EqOn f g U) (w : List (Option (Fin 2))) : Set.EqOn (amnrWord b w f) (amnrWord b w g) U

A word depends only on the germ of the differentiated function.

theorem AVenhance.Infra.Section4.amnrWord_append {b : AmnrSpace → Homogenization.Vec 2} (w v : List (Option (Fin 2))) (f : AmnrSpace → ℝ) : amnrWord b (w ++ v) f = amnrWord b w (amnrWord b v f)

Appending an inner material derivative is exactly the term used by the recursion.

theorem AVenhance.Infra.Section4.amnrWeight_append (S H : ℝ) (w v : List (Option (Fin 2))) : amnrWeight S H (w ++ v) = amnrWeight S H w * amnrWeight S H v

theorem AVenhance.Infra.Section4.amnrBudget_append (w v : List (Option (Fin 2))) : amnrBudget (w ++ v) = amnrBudget w + amnrBudget v

theorem AVenhance.Infra.Section4.IsAmnrMixedWord.material {w : List (Option (Fin 2))} (hw : IsAmnrMixedWord w) : IsAmnrMixedWord (w ++ [none])

Mixed words remain mixed when an inner material derivative is appended.

theorem AVenhance.Infra.Section4.amnrLevelBudget {N r : ℕ} {w : List (Option (Fin 2))} (hw : amnrBudget w + 2 * (r + 1) ≤ N) : amnrBudget (w ++ [none]) + 2 * r ≤ N ∧ ∀ q ∈ amnrSplits w, amnrBudget q.1 + 2 * r ≤ N ∧ amnrBudget q.2 + 2 * r ≤ N

The Jcut step consumes two units, and every Leibniz factor stays in the previous level's budget. This check is used at each induction step.

theorem AVenhance.Infra.Section4.amnrWord_sub {U : Set AmnrSpace} (hU : IsOpen U) {b : AmnrSpace → Homogenization.Vec 2} {f g : AmnrSpace → ℝ} {N : ℕ} (hb : ContDiffOn ℝ (↑N) b U) (hf : ContDiffOn ℝ (↑N) f U) (hg : ContDiffOn ℝ (↑N) g U) (w : List (Option (Fin 2))) (hw : w.length ≤ N) : Set.EqOn (amnrWord b w (f - g)) (amnrWord b w f - amnrWord b w g) U

Differentiating a difference, retaining the actual minus sign.

theorem AVenhance.Infra.Section4.amnrWord_sum {U : Set AmnrSpace} (hU : IsOpen U) {b : AmnrSpace → Homogenization.Vec 2} {N : ℕ} (hb : ContDiffOn ℝ (↑N) b U) {ι : Type u_1} (s : Finset ι) (f : ι → AmnrSpace → ℝ) (hf : ∀ i ∈ s, ContDiffOn ℝ (↑N) (f i) U) (w : List (Option (Fin 2))) (hw : w.length ≤ N) : Set.EqOn (amnrWord b w (∑ i ∈ s, f i)) (∑ i ∈ s, amnrWord b w (f i)) U

Finite tensor contractions commute with every admissible differential word.