All-order divergence-form forcing with exact coefficient-gradient products.

theorem AVenhance.Infra.Section4.iterateSpatialWord_gradient {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (w : List (Fin 2)) (j : Fin 2) : (iterateSpatialWord w fun (x : Homogenization.Vec 2) => spaceGrad f x j) = fun (x : Homogenization.Vec 2) => spaceGrad (iterateSpatialWord w f) x j

Ordered spatial derivatives commute with each coordinate gradient.

theorem AVenhance.Infra.Section4.iterateSpatialWord_sum {ι : Type u_1} (s : Finset ι) (f : ι → Homogenization.Vec 2 → ℝ) (hf : ∀ i ∈ s, ContDiff ℝ (↑⊤) (f i)) (w : List (Fin 2)) : (iterateSpatialWord w fun (x : Homogenization.Vec 2) => ∑ i ∈ s, f i x) = fun (x : Homogenization.Vec 2) => ∑ i ∈ s, iterateSpatialWord w (f i) x

Ordered spatial differentiation commutes with every finite smooth sum.

noncomputable def AVenhance.Infra.Section4.iterateWordFlux (A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (v : Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) (x : Homogenization.Vec 2) : Homogenization.Vec 2

The differentiated vector flux keeps every coefficient-gradient Leibniz term, including the principal term with no derivative on the coefficient.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section4.iterateSpatialWord_matrix_flux {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : Homogenization.Vec 2 → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hv : ContDiff ℝ (↑⊤) v) (w : List (Fin 2)) (i : Fin 2) : (iterateSpatialWord w fun (x : Homogenization.Vec 2) => (A x).mulVec (spaceGrad v x) i) = fun (x : Homogenization.Vec 2) => iterateWordFlux A v w x i

Each component of the differentiated actual flux is exactly the expanded flux, with multiplicities supplied by the ordered splits.

theorem AVenhance.Infra.Section4.iterateSpatialWord_divergence {H : Homogenization.Vec 2 → Homogenization.Vec 2} (hH : ContDiff ℝ (↑⊤) H) (w : List (Fin 2)) : iterateSpatialWord w (vecDiv H) = vecDiv fun (x : Homogenization.Vec 2) (i : Fin 2) => iterateSpatialWord w (fun (y : Homogenization.Vec 2) => H y i) x

Spatial words commute with divergence of the actual smooth vector flux.

theorem AVenhance.Infra.Section4.iterateSpatialWord_matrix_forcing_divergence {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : Homogenization.Vec 2 → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hv : ContDiff ℝ (↑⊤) v) (w : List (Fin 2)) : iterateSpatialWord w (vecDiv fun (x : Homogenization.Vec 2) => (A x).mulVec (spaceGrad v x)) = vecDiv (iterateWordFlux A v w)

Exact all-order forcing in divergence form. No differentiated forcing formula is supplied as a hypothesis.