Construct the residual calculus data from the classical iterates, their actual AMNR regularity, and the smooth flow.
noncomputable def
AVenhance.Infra.Section5.frozenResidualPointwiseDataOfIterates
{β : ℝ}
(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 → ℝ)
(hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
(T : ℕ → ℝ → Homogenization.Vec 2 → ℝ)
(hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T)
(t : ℝ)
(ht : 0 < t)
(x : Homogenization.Vec 2)
(ρ : ℝ)
(hρ : 0 < ρ)
:
FrozenResidualPointwiseData I hΦ m hm κm κprev θ₀ θprev T hT t ht x ρ hρ
Every component of the source's pointwise residual-calculus record is obtained from the classical iterate and the declared smooth flow.
Equations
- One or more equations did not get rendered due to their size.