Differentiating spatial divergence under the A material recursion.

@[reducible, inline]

abbrev AVenhance.Infra.Section5.ST : Type

Joint time-space domain for the two-dimensional residual calculation.

Equations

• AVenhance.Infra.Section5.ST = (ℝ × Homogenization.Vec 2)

noncomputable def AVenhance.Infra.Section5.stDiv (F : ST → Homogenization.Vec 2) (p : ST) : ℝ

Spatial divergence of a vector field on joint time-space.

Equations

• AVenhance.Infra.Section5.stDiv F p = ∑ i : Fin 2, (fderiv ℝ F p) (0, Homogenization.basisVec i) i

theorem AVenhance.Infra.Section5.stDiv_congr_of_eventuallyEq {F G : ST → Homogenization.Vec 2} {p : ST} (hF : DifferentiableAt ℝ F p) (hEq : F =ᶠ[nhds p] G) : stDiv F p = stDiv G p

Spatial divergence is unchanged when vector fields agree near the space-time point.

noncomputable def AVenhance.Infra.Section5.stMaterial (F b : ST → Homogenization.Vec 2) (p : ST) : Homogenization.Vec 2

Material derivative of a vector field along the prescribed drift.

Equations

• AVenhance.Infra.Section5.stMaterial F b p = (fderiv ℝ F p) (1, b p)

noncomputable def AVenhance.Infra.Section5.stCorrection (F b : ST → Homogenization.Vec 2) (p : ST) : Homogenization.Vec 2

Jacobian of the drift applied to a vector field, the correction in the Lie derivative.

Equations

• AVenhance.Infra.Section5.stCorrection F b p i = ∑ j : Fin 2, (fderiv ℝ b p) (0, Homogenization.basisVec j) i * F p j

noncomputable def AVenhance.Infra.Section5.stLieDerivative (F b : ST → Homogenization.Vec 2) (p : ST) : Homogenization.Vec 2

Lie derivative obtained by subtracting the drift-Jacobian correction from material transport.

Equations

• AVenhance.Infra.Section5.stLieDerivative F b p = AVenhance.Infra.Section5.stMaterial F b p - AVenhance.Infra.Section5.stCorrection F b p

noncomputable def AVenhance.Infra.Section5.AmnrMaterialStep.stDivDerivative (F : ST → Homogenization.Vec 2) (p : ST) : ST →L[ℝ] ℝ

Continuous linear differential of the spatial divergence, expressed using second derivatives.

Equations

• AVenhance.Infra.Section5.AmnrMaterialStep.stDivDerivative F p = ∑ i : Fin 2, ContinuousLinearMap.proj i ∘SL (fderiv ℝ (fderiv ℝ F) p).flip (0, Homogenization.basisVec i)

noncomputable def AVenhance.Infra.Section5.AmnrMaterialStep.stCorrectionDerivative (F b : ST → Homogenization.Vec 2) (p : ST) : ST →L[ℝ] Homogenization.Vec 2

Differential of the drift-Jacobian correction, expressed by the product rule.

Equations

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

theorem AVenhance.Infra.Section5.stDiv_hasFDerivAt {F : ST → Homogenization.Vec 2} {p : ST} (hF : ContDiffAt ℝ 2 F p) : HasFDerivAt (stDiv F) (AmnrMaterialStep.stDivDerivative F p) p

theorem AVenhance.Infra.Section5.AmnrMaterialStep.stMaterial_hasFDerivAt {F b : ST → Homogenization.Vec 2} {p : ST} (hF : ContDiffAt ℝ 2 F p) (hb : ContDiffAt ℝ 2 b p) : HasFDerivAt (fun (q : ST) => stMaterial F b q) (fderiv ℝ F p ∘SL ContinuousLinearMap.prod 0 (fderiv ℝ b p) + (fderiv ℝ (fderiv ℝ F) p).flip (1, b p)) p

theorem AVenhance.Infra.Section5.AmnrMaterialStep.stCorrection_hasFDerivAt {F b : ST → Homogenization.Vec 2} {p : ST} (hF : ContDiffAt ℝ 2 F p) (hb : ContDiffAt ℝ 2 b p) : HasFDerivAt (fun (q : ST) => stCorrection F b q) (stCorrectionDerivative F b p) p

theorem AVenhance.Infra.Section5.AmnrMaterialStep.stLieDerivative_hasFDerivAt {F b : ST → Homogenization.Vec 2} {p : ST} (hF : ContDiffAt ℝ 2 F p) (hb : ContDiffAt ℝ 2 b p) : HasFDerivAt (fun (q : ST) => stLieDerivative F b q) (fderiv ℝ F p ∘SL ContinuousLinearMap.prod 0 (fderiv ℝ b p) + (fderiv ℝ (fderiv ℝ F) p).flip (1, b p) - stCorrectionDerivative F b p) p

theorem AVenhance.Infra.Section5.stLieDerivative_differentiableAt {F b : ST → Homogenization.Vec 2} {p : ST} (hF : ContDiffAt ℝ 2 F p) (hb : ContDiffAt ℝ 2 b p) : DifferentiableAt ℝ (stLieDerivative F b) p

The row-corrected material derivative is differentiable whenever the flux and velocity have two derivatives at the point.

def AVenhance.Infra.Section5.AmnrMaterialStep.tensorPairFlux (A : ST → Fin 2 → Fin 2 → Fin 2 → ℝ) (q : ℝ → Fin 2 → Fin 2 → ℝ) (j k : Fin 2) : ST → Homogenization.Vec 2

Vector flux formed by fixing two tensor indices and multiplying by the time coefficient.

Equations

• AVenhance.Infra.Section5.AmnrMaterialStep.tensorPairFlux A q j k z i = A z i j k * q z.1 j k

theorem AVenhance.Infra.Section5.tensorPair_correctedMaterial {A Aplus : ST → Fin 2 → Fin 2 → Fin 2 → ℝ} {q qplus : ℝ → Fin 2 → Fin 2 → ℝ} {b : ST → Homogenization.Vec 2} {p : ST} {LA : Fin 2 → Fin 2 → Fin 2 → ST →L[ℝ] ℝ} (j k : Fin 2) (hA : ∀ (i : Fin 2), HasFDerivAt (fun (z : ST) => A z i j k) (LA i j k) p) (hq : HasDerivAt (fun (s : ℝ) => qplus s j k) (-q p.1 j k) p.1) (hrec : ∀ (i : Fin 2), Aplus p i j k = (LA i j k) (1, b p) - ∑ ℓ : Fin 2, (fderiv ℝ b p) (0, Homogenization.basisVec ℓ) i * A p ℓ j k) : stLieDerivative (AmnrMaterialStep.tensorPairFlux A qplus j k) b p = fun (i : Fin 2) => Aplus p i j k * qplus p.1 j k - A p i j k * q p.1 j k

For one pair of tensor indices, the row-corrected material derivative of A^{·jk} q⁺^{jk} is A⁺^{·jk} q⁺^{jk} - A^{·jk} q^{jk}. The recurrence hypothesis is the coefficient form of the source's recursion; the proof is just the product rule and the time primitive derivative.

theorem AVenhance.Infra.Section5.frozen_amnrPair_correctedMaterial {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (n r : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) (j k : Fin 2) (hA : ∀ (i : Fin 2), DifferentiableAt ℝ (Function.uncurry fun (s : ℝ) (y : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r s y i j k) (t, x)) (hb : DifferentiableAt ℝ (Function.uncurry fun (s : ℝ) (y : Homogenization.Vec 2) => streamVel (Φ (m - 1)) s y) (t, x)) : stLieDerivative (AmnrMaterialStep.tensorPairFlux (fun (z : ST) (i j k : Fin 2) => I.Amnr hΦ m κ n T r z.1 z.2 i j k) (fun (s : ℝ) (j k : Fin 2) => I.qMNR κ m n (r + 1) s j k) j k) (fun (z : ST) => streamVel (Φ (m - 1)) z.1 z.2) (t, x) = fun (i : Fin 2) => I.Amnr hΦ m κ n T (r + 1) t x i j k * I.qMNR κ m n (r + 1) t j k - I.Amnr hΦ m κ n T r t x i j k * I.qMNR κ m n r t j k

The AMNR recursion and the primitive recursion for q give the corrected material derivative of each Amnr row and each fixed (j,k) pair. The only regularity inputs are differentiability of that A_r coefficient and of the previous stream velocity at the spacetime point.

theorem AVenhance.Infra.Section5.stDiv_material_eq_stDiv_lieDerivative {F b : ST → Homogenization.Vec 2} {p : ST} (hF : ContDiffAt ℝ 2 F p) (hb : ContDiffAt ℝ 2 b p) (hdiv : ∀ (q : ST), stDiv b q = 0) : (fderiv ℝ (stDiv F) p) (1, b p) = stDiv (stLieDerivative F b) p

The row-corrected material derivative commutes with divergence when the velocity is divergence-free. This is the differential identity encoded by the recursion.