Shared tensor-independent spatial/material directional calculus.

The mixed calculus below keeps spatial and material operations ordered.

noncomputable def AVenhance.Infra.Section4.amnrMaterial (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (f : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

Scalar material operator. This calculus does not depend on a corrector tensor.

Equations

• AVenhance.Infra.Section4.amnrMaterial b f t x = deriv (fun (s : ℝ) => f s x) t + Homogenization.vecDot (b t x) (AVenhance.spaceGrad (f t) x)

@[reducible, inline]

abbrev AVenhance.Infra.Section4.AmnrSpace : Type

Space-time coordinate carrier used only to express the differential operators.

Equations

• AVenhance.Infra.Section4.AmnrSpace = (ℝ × Homogenization.Vec 2)

def AVenhance.Infra.Section4.amnrDirection (b : AmnrSpace → Homogenization.Vec 2) (d : Option (Fin 2)) (z : AmnrSpace) : AmnrSpace

none is the material direction; some i is the i-th spatial direction.

Equations

• AVenhance.Infra.Section4.amnrDirection b none z = (1, b z)
• AVenhance.Infra.Section4.amnrDirection b (some i) z = (0, Homogenization.basisVec i)

noncomputable def AVenhance.Infra.Section4.amnrOp (b : AmnrSpace → Homogenization.Vec 2) (d : Option (Fin 2)) (f : AmnrSpace → ℝ) (z : AmnrSpace) : ℝ

A directional differential operator on the actual space-time function.

Equations

• AVenhance.Infra.Section4.amnrOp b d f z = (fderiv ℝ f z) (AVenhance.Infra.Section4.amnrDirection b d z)

def AVenhance.Infra.Section4.amnrWord (b : AmnrSpace → Homogenization.Vec 2) : List (Option (Fin 2)) → (AmnrSpace → ℝ) → AmnrSpace → ℝ

Ordered differential words, with the outermost operator at the head.

Equations

• AVenhance.Infra.Section4.amnrWord b [] x✝ = x✝
• AVenhance.Infra.Section4.amnrWord b (d :: w) x✝ = AVenhance.Infra.Section4.amnrOp b d (AVenhance.Infra.Section4.amnrWord b w x✝)

theorem AVenhance.Infra.Section4.Calculus.amnrDirection_contDiffOn {b : AmnrSpace → Homogenization.Vec 2} {U : Set AmnrSpace} {n : ℕ} (hb : ContDiffOn ℝ (↑n) b U) (d : Option (Fin 2)) : ContDiffOn ℝ (↑n) (amnrDirection b d) U

Smoothness of each spatial or material direction.

theorem AVenhance.Infra.Section4.amnrWord_contDiffOn {b : AmnrSpace → Homogenization.Vec 2} {U : Set AmnrSpace} (hU : IsOpen U) {N : ℕ} (hb : ContDiffOn ℝ (↑N) b U) {f : AmnrSpace → ℝ} (hf : ContDiffOn ℝ (↑N) f U) (w : List (Option (Fin 2))) {n : ℕ} (hn : n + w.length ≤ N) : ContDiffOn ℝ (↑n) (amnrWord b w f) U

Every word consumes exactly one ordinary derivative per letter.

theorem AVenhance.Infra.Section4.amnrOp_mul {b : AmnrSpace → Homogenization.Vec 2} (d : Option (Fin 2)) {f g : AmnrSpace → ℝ} {z : AmnrSpace} (hf : DifferentiableAt ℝ f z) (hg : DifferentiableAt ℝ g z) : amnrOp b d (f * g) z = amnrOp b d f z * g z + f z * amnrOp b d g z

Directional Leibniz rule, with no quantitative hypothesis.

theorem AVenhance.Infra.Section4.amnrOp_sum {ι : Type u_1} (S : Finset ι) {b : AmnrSpace → Homogenization.Vec 2} (d : Option (Fin 2)) (f : ι → AmnrSpace → ℝ) (z : AmnrSpace) (hf : ∀ i ∈ S, DifferentiableAt ℝ (f i) z) : amnrOp b d (∑ i ∈ S, f i) z = ∑ i ∈ S, amnrOp b d (f i) z

Directional differentiation commutes with finite sums of differentiable functions.

theorem AVenhance.Infra.Section4.amnrOp_material {b : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} {z : AmnrSpace} (hf : DifferentiableAt ℝ f z) : amnrOp b none f z = amnrMaterial (fun (t : ℝ) (x : Homogenization.Vec 2) => b (t, x)) (fun (t : ℝ) (x : Homogenization.Vec 2) => f (t, x)) z.1 z.2

The joint directional operator is precisely the material operator.