Actual all-order joint source regularity on an open cutoff neighborhood.

theorem AVenhance.Infra.Section4.amnr_short_source_jacobian_product {A d : ℝ} (hA : 0 < A) (hd : |d| ≤ 2 ^ (-24) * A⁻¹) : |d| * (2 ^ 20 * A) ≤ 1 / 16

Abstract short-interval arithmetic, separated from flow differentiation.

def AVenhance.Infra.Section4.amnrSourceFlowDomain {β : ℝ} (I : Ingredients β) (m : ℕ) (l : ℤ) : Set AmnrSpace

An open time neighborhood strictly containing every actual source cutoff support, including its endpoints.

Equations

• AVenhance.Infra.Section4.amnrSourceFlowDomain I m l = {z : AVenhance.Infra.Section4.AmnrSpace | |z.1 - ↑l * AVenhance.tauPP β I.Λ m| < 2 ^ (-24) * (AVenhance.a β I.Λ (m - 1))⁻¹}

theorem AVenhance.Infra.Section4.amnrSourceFlowDomain_isOpen {β : ℝ} (I : Ingredients β) (m : ℕ) (l : ℤ) : IsOpen (amnrSourceFlowDomain I m l)

theorem AVenhance.Infra.Section4.amnr_cutoff_window_mem_sourceFlowDomain {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) (z : AmnrSpace) (ht : |z.1 - ↑l * tauPP β I.Λ m| ≤ tauPP β I.Λ m / 2 + tauP β I.Λ m) : z ∈ amnrSourceFlowDomain I m l

Each actual cutoff window lies inside the open smoothness domain.

theorem AVenhance.Infra.Section4.amnr_flowGrad_contDiffOn_infty_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) (i j : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2 i j) (amnrSourceFlowDomain I m l)

The actual pulled source Jacobian has every mixed derivative on the open cutoff neighborhood. Its quantitative bounds remain separate.