Construct the residual calculus data from the classical iterates, their actual AMNR regularity, and the smooth flow.

@[reducible, inline]

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

Joint time-space domain with strictly positive time.

Equations

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

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_Gslice_smooth {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (hT : ContDiffOn ℝ (↑⊤) (Function.uncurry T) (Set.Ici 0 ×ˢ Set.univ)) {t : ℝ} (ht : 0 ≤ t) (l : ℤ) : ContDiff ℝ (↑⊤) (G I hΦ m T l t)

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_Gbar_slice_smooth {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (T : ℝ → Homogenization.Vec 2 → ℝ) (hT : ContDiffOn ℝ (↑⊤) (Function.uncurry T) (Set.Ici 0 ×ˢ Set.univ)) {t : ℝ} (ht : 0 ≤ t) : ContDiff ℝ (↑⊤) (Gbar I hΦ m T t)

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_Gbar_eq_source_flowAverage {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) (hT : ContDiff ℝ 1 (T t)) : Gbar I hΦ m T t x = ∑' (l : ℤ), I.hatXiML m l t • (I.flowGrad hΦ m l t x).mulVec (spaceGrad (T t) x)

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_time_hasDerivAt {F : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} {x : Homogenization.Vec 2} (hF : ContDiffOn ℝ 1 (Function.uncurry F) residualPositiveDomain) (ht : 0 < t) : HasDerivAt (fun (s : ℝ) => F s x) ((fderiv ℝ (Function.uncurry F) (t, x)) (1, 0)) t

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_slice_hasFDerivAt {F : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} {x : Homogenization.Vec 2} {L : Homogenization.Vec 2 →L[ℝ] ℝ} (hF : ContDiffAt ℝ 1 (Function.uncurry F) (t, x)) (hL : L = fderiv ℝ (Function.uncurry F) (t, x) ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Homogenization.Vec 2))) : HasFDerivAt (F t) L x

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_slice_hasFDerivAt_canonical {F : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} {x : Homogenization.Vec 2} (hF : ContDiffAt ℝ 1 (Function.uncurry F) (t, x)) : HasFDerivAt (F t) (fderiv ℝ (F t) x) x

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_matrixMulVec_contDiff {n : ℕ} {M : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : Homogenization.Vec 2 → Homogenization.Vec 2} (hM : ContDiff ℝ (↑n) M) (hv : ContDiff ℝ (↑n) v) : ContDiff ℝ ↑n fun (x : Homogenization.Vec 2) => (M x).mulVec (v x)

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_vecDiv_contDiff {n : ℕ} {V : Homogenization.Vec 2 → Homogenization.Vec 2} (hV : ContDiff ℝ (↑n + 1) V) : ContDiff ℝ ↑n fun (x : Homogenization.Vec 2) => vecDiv V x

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_Gspatial_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (hT : ContDiffOn ℝ (↑⊤) (Function.uncurry T) (Set.Ici 0 ×ˢ Set.univ)) {t : ℝ} (ht : 0 ≤ t) (l : ℤ) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => G I hΦ m T l t x

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_gradMatrix_contDiff {n : ℕ} {F : Homogenization.Vec 2 → Homogenization.Vec 2} (hF : ContDiff ℝ (↑n + 1) F) : ContDiff ℝ ↑n fun (x : Homogenization.Vec 2) => gradMatrix F x

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_contDiffOn_slice {n : ℕ} {F : ℝ × Homogenization.Vec 2 → ℝ} (hF : ContDiffOn ℝ (↑n) F residualPositiveDomain) {t : ℝ} (ht : 0 < t) : ContDiff ℝ ↑n fun (x : Homogenization.Vec 2) => F (t, x)

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_hmEndpoint_budget {β : ℝ} {r : ℕ} (hr : r ∈ Finset.range (Jcut β)) : 1 + (r + 1) ≤ Nstar β

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_hmFlux_budget {β : ℝ} {r : ℕ} (hr : r ∈ Finset.range (Jcut β)) : 3 + r ≤ Nstar β

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_amnrBudget_one {β : ℝ} {r : ℕ} (hr : r ∈ Finset.range (Jcut β)) : 1 + r ≤ Nstar β

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_terminalBudget_one {β : ℝ} (hN : 1 ≤ Nstar β) : 1 + Jcut β ≤ Nstar β

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_spaceGrad_contDiff_order {n : ℕ} {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑n + 1) f) : ContDiff ℝ (↑n) (spaceGrad f)

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_iterateError_spatial_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm κprev t : ℝ) (_ht : 0 ≤ t) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hprev : ContDiff ℝ 3 (T (Nstar β - 1) t)) (hlast : ContDiff ℝ 3 (T (Nstar β) t)) : ContDiff ℝ 2 fun (y : Homogenization.Vec 2) => iterateError I hΦ m κm κprev T t y

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_sourceTail_spatial_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm κprev : ℝ) (hκm : 0 < κm) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → 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) {t : ℝ} (ht : 0 < t) : ContDiff ℝ 1 fun (y : Homogenization.Vec 2) (i : Fin 2) => ∑ n ∈ Finset.range (Nstar β), ∑ j : Fin 2, ∑ k : Fin 2, I.Amnr hΦ m κm n (T (Nstar β)) (Jcut β) t y i j k * I.qMNR κm m n (Jcut β) t j k

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_chiSlice_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) : ContDiff ℝ 2 (I.chiTilde hΦ m κ k t)

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_Gjoint_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (hT : ContDiffOn ℝ (↑⊤) (Function.uncurry T) (Set.Ici 0 ×ˢ Set.univ)) (l : ℤ) : ContDiffOn ℝ (↑⊤) (fun (z : ℝ × Homogenization.Vec 2) => G I hΦ m T l z.1 z.2) residualPositiveDomain

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_matrixMul_contDiff {n : ℕ} {A B : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} (hA : ContDiff ℝ (↑n) A) (hB : ContDiff ℝ (↑n) B) : ContDiff ℝ ↑n fun (y : Homogenization.Vec 2) => A y * B y

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_psi_contDiff_two {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) : ContDiff ℝ 2 (psi β I.Λ m k)

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_psiTilde_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (_hm : 1 ≤ m) (t : ℝ) : ContDiff ℝ 1 (psiTilde I hΦ m t)

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_diffusionMatrix_contDiff_one {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κ t : ℝ) : ContDiff ℝ 1 fun (y : Homogenization.Vec 2) => diffusionMatrix I hΦ m κ t y

theorem AVenhance.Infra.Section5.ResidualPointwiseConstructor.residual_chiGradG_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) (t : ℝ) (hT : ContDiffOn ℝ (↑⊤) (Function.uncurry T) (Set.Ici 0 ×ˢ Set.univ)) (ht : 0 ≤ t) : ContDiff ℝ 1 (chiGradG I hΦ m κ T k t)