Pointwise calculus for the LeftJacobian Piola source

For a constant matrix M, the divergence of the pulled gap flux y ↦ Σ_l ξ̂_l F_lᵀ M F_l ∇T is bounded pointwise by 32 A · hmPiolaQ, where A bounds the entries of M and hmPiolaQ is the Hessian/gradient majorant already used for the averaged pulled gradient. The proof is the plain product rule: the derivative of F_l is expressed through the second flow derivative xFlowHess and the Jacobian of the inverse flow, and all active flow factors are bounded by the stream-function estimates.

noncomputable def AVenhance.Infra.Section5.Contracts.hmPiolaQ (E : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

The pointwise majorant of the entries of ∇G_l, built from ∇T and the two first-order Hessian rows of T.

Equations

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

theorem AVenhance.Infra.Section5.Contracts.hmPiolaQ_nonneg (E : ℝ) (hE : 0 < E) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : 0 ≤ hmPiolaQ E T t x

theorem AVenhance.Infra.Section5.Contracts.hmPiolaQ_ge (E : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : 2 ^ 19 / E * √(Homogenization.vecNormSq (spaceGrad (T t) x)) ≤ hmPiolaQ E T t x

theorem AVenhance.Infra.Section5.Contracts.hmPiola_spaceGrad_G_abs_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (T : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) {E : ℝ} (hE : 0 < E) (l : ℤ) (hFlow : ∀ (x : Homogenization.Vec 2) (i j : Fin 2), |I.flowGrad hΦ m l t x i j| ≤ 2) (hInv : ∀ (x : Homogenization.Vec 2) (i j : Fin 2), |gradMatrix (fun (y : Homogenization.Vec 2) => I.xFlowInv hΦ m l t y) x i j| ≤ 2) (hHess : ∀ (x : Homogenization.Vec 2) (p j q : Fin 2), |RelativeError.xFlowHess I hΦ m l t x p j q| ≤ 2 ^ 16 / E) (x : Homogenization.Vec 2) (i j : Fin 2) : |spaceGrad (fun (y : Homogenization.Vec 2) => G I hΦ m T l t y j) x i| ≤ hmPiolaQ E T t x

Per-l pointwise bound for the entries of ∇G_l (the per-l content of the bound for ∇GDot).

theorem AVenhance.Infra.Section5.Contracts.hmPiola_spaceGrad_flowGrad_entry {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (i p r : Fin 2) : spaceGrad (fun (y : Homogenization.Vec 2) => I.flowGrad hΦ m l t y p r) x i = ∑ q : Fin 2, gradMatrix (fun (z : Homogenization.Vec 2) => I.xFlowInv hΦ m l t z) x i q * RelativeError.xFlowHess I hΦ m l t (I.xFlowInv hΦ m l t x) r p q

The spatial derivative of an entry of F_l = flowGrad: ∂_i (F_l)_{pr} = Σ_q (∇Y_l)_{iq} · ∂_q ∂_p X^r_l(Y_l x).

theorem AVenhance.Infra.Section5.Contracts.hmPiola_vecDiv_sum_smul {S : Finset ℤ} (c : ℤ → ℝ) {V : ℤ → Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} (hV : ∀ l ∈ S, DifferentiableAt ℝ (V l) x) : vecDiv (fun (y : Homogenization.Vec 2) => ∑ l ∈ S, c l • V l y) x = ∑ l ∈ S, c l * vecDiv (V l) x

Finite weighted sums commute with the divergence.

theorem AVenhance.Infra.Section5.Contracts.hmPiola_term_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (M : Matrix (Fin 2) (Fin 2) ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (hT : ContDiff ℝ (↑⊤) (T t)) : ContDiff ℝ ↑⊤ fun (y : Homogenization.Vec 2) => (I.flowGrad hΦ m l t y).transpose.mulVec (M.mulVec ((I.flowGrad hΦ m l t y).mulVec (spaceGrad (T t) y)))

The per-l pulled flux y ↦ F_lᵀ M F_l ∇T is smooth.

theorem AVenhance.Infra.Section5.Contracts.HmPiolaRateCalculus.hmPiola_arith {A Q g E : ℝ} (hA : 0 ≤ A) (hQ : 2 ^ 19 / E * g ≤ Q) : 4 * (4 * A * Q + 2 ^ 21 * A * g / E) ≤ 32 * A * Q

Real arithmetic closing the pointwise Piola bound.

theorem AVenhance.Infra.Section5.Contracts.hmPiola_vecDiv_term_abs_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (T : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) {E : ℝ} (hE : 0 < E) (l : ℤ) (hFlow : ∀ (x : Homogenization.Vec 2) (i j : Fin 2), |I.flowGrad hΦ m l t x i j| ≤ 2) (hInv : ∀ (x : Homogenization.Vec 2) (i j : Fin 2), |gradMatrix (fun (y : Homogenization.Vec 2) => I.xFlowInv hΦ m l t y) x i j| ≤ 2) (hHess : ∀ (x : Homogenization.Vec 2) (p j q : Fin 2), |RelativeError.xFlowHess I hΦ m l t x p j q| ≤ 2 ^ 16 / E) (M : Matrix (Fin 2) (Fin 2) ℝ) {A : ℝ} (hA : ∀ (i j : Fin 2), |M i j| ≤ A) (x : Homogenization.Vec 2) : |vecDiv (fun (y : Homogenization.Vec 2) => (I.flowGrad hΦ m l t y).transpose.mulVec (M.mulVec ((I.flowGrad hΦ m l t y).mulVec (spaceGrad (T t) y)))) x| ≤ 32 * A * hmPiolaQ E T t x

Per-l pointwise bound for the divergence of F_lᵀ M F_l ∇T.

theorem AVenhance.Infra.Section5.Contracts.hmPiola_vecDiv_tsum_abs_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (T : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) {E : ℝ} (hE : 0 < E) (hFlow : ∀ (l : ℤ), I.hatXiML m l t ≠ 0 → ∀ (x : Homogenization.Vec 2) (i j : Fin 2), |I.flowGrad hΦ m l t x i j| ≤ 2) (hInv : ∀ (l : ℤ), I.hatXiML m l t ≠ 0 → ∀ (x : Homogenization.Vec 2) (i j : Fin 2), |gradMatrix (fun (y : Homogenization.Vec 2) => I.xFlowInv hΦ m l t y) x i j| ≤ 2) (hHess : ∀ (l : ℤ), I.hatXiML m l t ≠ 0 → ∀ (x : Homogenization.Vec 2) (p j q : Fin 2), |RelativeError.xFlowHess I hΦ m l t x p j q| ≤ 2 ^ 16 / E) (M : Matrix (Fin 2) (Fin 2) ℝ) {A : ℝ} (hA : ∀ (i j : Fin 2), |M i j| ≤ A) (x : Homogenization.Vec 2) : |vecDiv (fun (y : Homogenization.Vec 2) => ∑' (l : ℤ), I.hatXiML m l t • (I.flowGrad hΦ m l t y).transpose.mulVec (M.mulVec ((I.flowGrad hΦ m l t y).mulVec (spaceGrad (T t) y)))) x| ≤ 32 * A * hmPiolaQ E T t x

Pointwise bound for the divergence of the full ξ̂-weighted pulled gap flux.