Source bounds for the second spatial derivative of the actual velocity.

theorem AVenhance.Infra.Section4.amnr_clm_norm_le_two_basis_general {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Homogenization.Vec 2 →L[ℝ] E} {B : ℝ} (hB : 0 ≤ B) (h : ∀ (i : Fin 2), ‖L (Homogenization.basisVec i)‖ ≤ B) : ‖L‖ ≤ 2 * B

Two coordinate directions control an operator into any normed real space.

theorem AVenhance.Infra.Section4.amnr_previous_velocityJacobian_norm_le_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) (x : Homogenization.Vec 2) : ‖Flow.jointSpatialFDeriv (streamVel (Φ (m - 1))) t x‖ ≤ 2 ^ 20 * a β I.Λ (m - 1)

The source velocity Lipschitz rate bounds the actual spatial derivative operator, uniformly at the preceding scale.