Source increment bounds with independent spatial and material cutoffs.
The spatial stream-regularity and inverse-flow bounds hold at every order; only cutoff-time
orders use the literal Nstar.
theorem
AVenhance.Infra.Construction.MaterialAuxiliaryWords.material_aux_amnrSpaceWord_abs_le_iteratedFDeriv
{f : Homogenization.Vec 2 → ℝ}
(hf : ContDiff ℝ (↑⊤) f)
(α : List (Fin 2))
(x : Homogenization.Vec 2)
:
theorem
AVenhance.Infra.Construction.material_aux_nextStreamTerm_mixed_abs_le_of_A3
{β C : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(hreg : StreamRegularityBounds C I Φ)
{m : ℕ}
(hm : 1 ≤ m)
(k : ℤ)
(α : List (Fin 2))
(ell : ℕ)
{Nspace : ℕ}
(hα : α.length ≤ Nspace)
(hell : ell ≤ Nstar β)
(z : Section4.AmnrSpace)
:
|Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2)
(List.map some α ++ List.replicate ell none)
(fun (y : Section4.AmnrSpace) => I.nextStreamTerm m (Φ (m - 1)) ⋯ y.1 y.2 k) z| ≤ 2 ^ ell * I.Chat * I.Czeta * (Section4.amnrTransportSpatialConstant Nspace * a β I.Λ m * epsilon β I.Λ m ^ 2 * (epsilon β I.Λ m)⁻¹ ^ α.length) * (tau β I.Λ m)⁻¹ ^ ell
A transported recursion summand has arbitrary auxiliary spatial order,
while its time-cutoff derivative stays within Nstar.
theorem
AVenhance.Infra.Construction.material_aux_streamIncrement_mixed_abs_le_of_A3
{β C : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(hreg : StreamRegularityBounds C I Φ)
{m : ℕ}
(hm : 1 ≤ m)
(α : List (Fin 2))
(ell : ℕ)
{Nspace : ℕ}
(hα : α.length ≤ Nspace)
(hell : ell ≤ Nstar β)
(z : Section4.AmnrSpace)
:
|Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2)
(List.map some α ++ List.replicate ell none) (fun (y : Section4.AmnrSpace) => Φ m y.1 y.2 - Φ (m - 1) y.1 y.2)
z| ≤ 3 * (2 ^ ell * I.Chat * I.Czeta * (Section4.amnrTransportSpatialConstant Nspace * a β I.Λ m * epsilon β I.Λ m ^ 2 * (epsilon β I.Λ m)⁻¹ ^ α.length) * (tau β I.Λ m)⁻¹ ^ ell)
The three locally active recursion summands give the mixed stream increment bound at independent spatial and material orders.
noncomputable def
AVenhance.Infra.Construction.materialAuxStreamMixedCurrentConstant
{β : ℝ}
(I : Ingredients β)
(Nspace : ℕ)
:
The mixed stream increment has its current material amplitude, with an auxiliary spatial order and literal cutoff-time order.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AVenhance.Infra.Construction.materialAuxStreamMixedCurrentConstant_nonneg
{β : ℝ}
(I : Ingredients β)
(Nspace : ℕ)
:
theorem
AVenhance.Infra.Construction.material_aux_streamIncrement_mixed_current_abs_le_of_A3
{β C : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(hreg : StreamRegularityBounds C I Φ)
{m : ℕ}
(hm : 1 ≤ m)
(α : List (Fin 2))
(ell : ℕ)
{Nspace : ℕ}
(hα : α.length ≤ Nspace)
(hell : ell ≤ Nstar β)
(z : Section4.AmnrSpace)
:
|Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (Section4.amnrMixedWord α ell)
(fun (y : Section4.AmnrSpace) => Φ m y.1 y.2 - Φ (m - 1) y.1 y.2) z| ≤ materialAuxStreamMixedCurrentConstant I Nspace * a β I.Λ m * epsilon β I.Λ m ^ 2 * (epsilon β I.Λ m)⁻¹ ^ α.length * a β I.Λ m ^ ell