Finite regularity of the spacetime fluxes used by the residual data.

@[reducible, inline]

abbrev AVenhance.Infra.Section5.ResidualFluxRegularity.residualPositiveDomain : Set (ℝ × Homogenization.Vec 2)

Joint time-space domain with strictly positive time.

Equations

• AVenhance.Infra.Section5.ResidualFluxRegularity.residualPositiveDomain = Set.Ioi 0 ×ˢ Set.univ

theorem AVenhance.Infra.Section5.ResidualFluxRegularity.residual_qMNR_entry_joint {β : ℝ} (I : Ingredients β) (κ : ℝ) (m n r : ℕ) (j k : Fin 2) : ContDiff ℝ ↑⊤ fun (z : ℝ × Homogenization.Vec 2) => I.qMNR κ m n r z.1 j k

theorem AVenhance.Infra.Section5.residual_pairFluxSum_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (N r p : ℕ) (hbudget : ∀ n ∈ Finset.range N, p + r ≤ Nstar β) : ContDiffOn ℝ (↑p) (amnrPairFluxSum I hΦ m N κm (T (Nstar β)) r) ResidualFluxRegularity.residualPositiveDomain

The finite A q flux inherits any regularity order allowed by the AMNR budget.

theorem AVenhance.Infra.Section5.residual_pairEndpointFluxSum_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (N r p : ℕ) (hbudget : ∀ n ∈ Finset.range N, p + r ≤ Nstar β) : ContDiffOn ℝ (↑p) (amnrPairEndpointFluxSum I hΦ m N κm (T (Nstar β)) r) ResidualFluxRegularity.residualPositiveDomain

The endpoint A q_r flux has the same finite regularity budget.

theorem AVenhance.Infra.Section5.ResidualFluxRegularity.residual_stDiv_contDiffOn {p : ℕ} {F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2} (hF : ContDiffOn ℝ (↑p + 1) F residualPositiveDomain) : ContDiffOn ℝ (↑p) (stDiv F) residualPositiveDomain

theorem AVenhance.Infra.Section5.residual_Hmr_contDiffOn_two {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (r : ℕ) (hr : r ∈ Finset.range (Jcut β)) : ContDiffOn ℝ 2 (fun (z : ST) => I.Hmr hΦ m κm (T (Nstar β)) r z.1 z.2) ResidualFluxRegularity.residualPositiveDomain

H_{m,r} has the two derivatives required by the residual calculus.

theorem AVenhance.Infra.Section5.residual_Hm_contDiffOn_two {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) : ContDiffOn ℝ 2 (fun (z : ST) => I.Hm hΦ m κm (T (Nstar β)) z.1 z.2) ResidualFluxRegularity.residualPositiveDomain

The finite H_m sum has two joint derivatives on positive time.