The actual pulled flow Jacobian has every source spatial derivative rate.

noncomputable def AVenhance.Infra.Section4.amnrJacobianEntryProjection (i j : Fin 2) : (Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) →L[ℝ] ℝ

Evaluate one actual matrix entry with unit norm cost.

Equations

• AVenhance.Infra.Section4.amnrJacobianEntryProjection i j = ContinuousLinearMap.proj j ∘SL (ContinuousLinearMap.apply ℝ (Homogenization.Vec 2)) (Homogenization.basisVec i)

theorem AVenhance.Infra.Section4.amnrJacobianEntryProjection_norm_le (i j : Fin 2) : ‖amnrJacobianEntryProjection i j‖ ≤ 1

theorem AVenhance.Infra.Section4.amnr_flowGrad_iteratedFDeriv_norm_le_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) (t : ℝ) (ht : |t - ↑l * tauPP β I.Λ m| ≤ tauPP β I.Λ m / 2 + tauP β I.Λ m) (n : ℕ) (hbudget : n ≤ Nstar β) (i j : Fin 2) (x : Homogenization.Vec 2) : ‖iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => I.flowGrad hΦ m l t y i j) x‖ ≤ ↑n.factorial * amnrFlowSpatialSourceConstant (Nstar β) ^ (n + 1) * (epsilon β I.Λ (m - 1))⁻¹ ^ n

The entire finite spatial budget of the actual pulled Jacobian is controlled uniformly in scale, cutoff index, target time and position.