Ordered spatial derivatives and the actual source seminorm.

def AVenhance.Infra.Section4.amnrSpaceWord : List (Fin 2) → (Homogenization.Vec 2 → ℝ) → Homogenization.Vec 2 → ℝ

Ordered spatial differentiation of a scalar on the actual Vec carrier.

Equations

• AVenhance.Infra.Section4.amnrSpaceWord [] x✝ = x✝
• AVenhance.Infra.Section4.amnrSpaceWord (i :: α) x✝ = fun (x : Homogenization.Vec 2) => (fderiv ℝ (AVenhance.Infra.Section4.amnrSpaceWord α x✝) x) (Homogenization.basisVec i)

def AVenhance.Infra.Section4.amnrSpatialIndices (α : List (Fin 2)) : Fin α.length → Fin 2

Coordinate tuple corresponding to the ordered spatial word.

Equations

• AVenhance.Infra.Section4.amnrSpatialIndices [] j = j.elim0
• AVenhance.Infra.Section4.amnrSpatialIndices (i :: α) j = Fin.cons i (AVenhance.Infra.Section4.amnrSpatialIndices α) j

def AVenhance.Infra.Section4.amnrSpatialDirections (α : List (Fin 2)) : Fin α.length → Homogenization.Vec 2

The exact tuple of spatial directions, retaining the word order.

Equations

• AVenhance.Infra.Section4.amnrSpatialDirections [] j = j.elim0
• AVenhance.Infra.Section4.amnrSpatialDirections (i :: α) j = Fin.cons (Homogenization.basisVec i) (AVenhance.Infra.Section4.amnrSpatialDirections α) j

theorem AVenhance.Infra.Section4.amnrSpatialDirections_eq (α : List (Fin 2)) : amnrSpatialDirections α = fun (j : Fin α.length) => Homogenization.basisVec (amnrSpatialIndices α j)

theorem AVenhance.Infra.Section4.amnrSpaceWord_eq_iteratedFDeriv {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (α : List (Fin 2)) : amnrSpaceWord α f = fun (x : Homogenization.Vec 2) => (iteratedFDeriv ℝ α.length f x) (amnrSpatialDirections α)

The ordered spatial derivatives are the actual iterated Frechet derivative on the coordinate tuple, rather than a separate derivative carrier.

theorem AVenhance.Infra.Section4.amnrSpaceWord_norm_le_of_barNorm {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (α : List (Fin 2)) {R B : ℝ} (hR : 0 < R) (hB : 0 ≤ B) (hb : barNorm α.length R f ≤ ENNReal.ofReal B) (x : Homogenization.Vec 2) : ‖amnrSpaceWord α f x‖ ≤ B * ↑α.length.factorial * R ^ α.length / (↑α.length + 1) ^ 2

Source seminorm control applies to every ordered spatial derivative with its exact factorial factor.

theorem AVenhance.Infra.Section4.amnrWord_spatial_slice {f : AmnrSpace → ℝ} (hf : ContDiff ℝ (↑⊤) f) (b : AmnrSpace → Homogenization.Vec 2) (α : List (Fin 2)) : amnrWord b (List.map some α) f = fun (z : AmnrSpace) => amnrSpaceWord α (fun (y : Homogenization.Vec 2) => f (z.1, y)) z.2

The spatial part of the mixed calculus is exactly the ordered derivative of the time slice. No quantitative assumption enters this bridge.

theorem AVenhance.Infra.Section4.amnrSpaceWord_append (α η : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) : amnrSpaceWord (α ++ η) f = amnrSpaceWord α (amnrSpaceWord η f)

Concatenating spatial words composes the actual derivative operators.

theorem AVenhance.Infra.Section4.amnrSpaceWord_const_smul (c : ℝ) (α : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) : amnrSpaceWord α (c • f) = c • amnrSpaceWord α f

Scalar multiplication commutes with all spatial derivatives, including at points where the total Frechet derivative uses its default value.

theorem AVenhance.Infra.Section4.amnrVelocityGradient_stream_zero (φ : ℝ → Homogenization.Vec 2 → ℝ) (p : Fin 2) (t : ℝ) : (fun (x : Homogenization.Vec 2) => amnrVelocityGradient (fun (z : AmnrSpace) => streamVel φ z.1 z.2) 0 p (t, x)) = -1 • amnrSpaceWord [p, 1] (φ t)

The source velocity-gradient slice has precisely the two spatial stream derivatives and the rotation sign encoded by sigmaMat.

theorem AVenhance.Infra.Section4.amnrVelocityGradient_stream_one (φ : ℝ → Homogenization.Vec 2 → ℝ) (p : Fin 2) (t : ℝ) : (fun (x : Homogenization.Vec 2) => amnrVelocityGradient (fun (z : AmnrSpace) => streamVel φ z.1 z.2) 1 p (t, x)) = amnrSpaceWord [p, 0] (φ t)