Pointwise calculus for the spacetime gradient of the averaged pulled temperature gradient.

theorem AVenhance.Infra.Section4.gradMatrix_Gbar_entry_abs_le_of_active_flow_bounds {β : ℝ} (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), |Section5.RelativeError.xFlowHess I hΦ m l t x p j q| ≤ 2 ^ 16 / E) (x : Homogenization.Vec 2) (i j : Fin 2) : |gradMatrix (Section5.Gbar I hΦ m T t) x i j| ≤ 4 * (√(Homogenization.vecNormSq (spaceGrad (iterateSpatialWord [0] (T t)) x)) + √(Homogenization.vecNormSq (spaceGrad (iterateSpatialWord [1] (T t)) x))) + 2 ^ 19 / E * √(Homogenization.vecNormSq (spaceGrad (T t) x))

A convex average of the differentiated pulled gradients is controlled by the Hessian and gradient of the temperature, provided the active flow Jacobians and their first spatial derivatives have the indicated bounds.

theorem AVenhance.Infra.Section4.HmSourceRatesGradientCore.iteratedFDeriv_component {f : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : Homogenization.Vec 2) (J : Fin n → Fin 2) (i : Fin 2) : ((iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => f y i) x) fun (k : Fin n) => Homogenization.basisVec (J k)) = (iteratedFDeriv ℝ n f x) (fun (k : Fin n) => Homogenization.basisVec (J k)) i

The quantitative limit-field regularity package controls every flow factor on the support of the large cutoff used in Gbar.

theorem AVenhance.Infra.Section4.hm_Gbar_active_flow_bounds {β Cmat Creg : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hflow : FlowBoundsData I Φ hΦ Cmat) (hreg : StreamRegularityBounds Creg I Φ) {m : ℕ} (hm : 2 ≤ m) {t : ℝ} (l : ℤ) (hactive : I.hatXiML m l t ≠ 0) : (∀ (x : Homogenization.Vec 2) (i j : Fin 2), |I.flowGrad hΦ m l t x i j| ≤ 2) ∧ (∀ (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) ∧ ∀ (x : Homogenization.Vec 2) (p j q : Fin 2), |Section5.RelativeError.xFlowHess I hΦ m l t x p j q| ≤ 2 ^ 16 * (epsilon β I.Λ (m - 1))⁻¹