The coarse-coefficient interface for the shared directional calculus.

The mixed calculus below keeps spatial and material operations ordered.

noncomputable def AVenhance.Infra.Section4.IterateCalculus.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.IterateCalculus.amnrMaterial b f t x = AVenhance.Infra.Section4.amnrMaterial b f t x

@[reducible, inline]

abbrev AVenhance.Infra.Section4.IterateCalculus.AmnrSpace : Type

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

Equations

• AVenhance.Infra.Section4.IterateCalculus.AmnrSpace = AVenhance.Infra.Section4.AmnrSpace

def AVenhance.Infra.Section4.IterateCalculus.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.IterateCalculus.amnrDirection b d z = AVenhance.Infra.Section4.amnrDirection b d z

noncomputable def AVenhance.Infra.Section4.IterateCalculus.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.IterateCalculus.amnrOp b d f z = AVenhance.Infra.Section4.amnrOp b d f z

noncomputable def AVenhance.Infra.Section4.IterateCalculus.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.IterateCalculus.amnrWord b = AVenhance.Infra.Section4.amnrWord b

theorem AVenhance.Infra.Section4.IterateCalculus.DirectionalCalculus.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

theorem AVenhance.Infra.Section4.IterateCalculus.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.IterateCalculus.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.IterateCalculus.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.IterateCalculus.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