Actual preceding Hessian contraction for the transferred drift error.

theorem AVenhance.Infra.Section4.IteratesHessianFactor.four_square_le (a b c d : ℝ) : (a + b + c + d) ^ 2 ≤ 4 * (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2)

theorem AVenhance.Infra.Section4.iterate_hessian_contraction_sq_bound (Q H : Matrix (Fin 2) (Fin 2) ℝ) {D : ℝ} (hD : 0 ≤ D) (hQ : ∀ (j k : Fin 2), |Q j k| ≤ D) : (∑ j : Fin 2, ∑ k : Fin 2, Q j k * H j k) ^ 2 ≤ 4 * D ^ 2 * ∑ j : Fin 2, ∑ k : Fin 2, H j k ^ 2

Four actual Hessian components control the scalar matrix contraction.

theorem AVenhance.Infra.Section4.iterate_hessian_factor_continuousOn {v : ℝ → Homogenization.Vec 2 → ℝ} {Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ} (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hQc : ContinuousOn Q (Set.Ici 0)) (w : List (Fin 2)) : ContinuousOn (fun (z : AmnrSpace) => ∑ j : Fin 2, ∑ k : Fin 2, Q z.1 j k * spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad (iterateSpatialWord w (v z.1)) y k) z.2 j) (Set.Ici 0 ×ˢ Set.univ)

The actual preceding Hessian factor is continuous up to initial time.

theorem AVenhance.Infra.Section4.iterate_hessian_factor_energy_bound {v : ℝ → Homogenization.Vec 2 → ℝ} {Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ} (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hQc : ContinuousOn Q (Set.Ici 0)) (w : List (Fin 2)) {D G : ℝ} (hD : 0 ≤ D) (hQ : ∀ (t : ℝ) (j k : Fin 2), |Q t j k| ≤ D) (hE : ∀ (k : Fin 2), (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord (k :: w) (v t))) ≤ G ^ 2) : ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, (∑ j : Fin 2, ∑ k : Fin 2, Q z.1 j k * spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad (iterateSpatialWord w (v z.1)) y k) z.2 j) ^ 2 ≤ (4 * D * G) ^ 2

Continuity and the L2 estimate of the actual preceding Hessian factor. The only quantitative scalar premises are preceding gradient energies.