divFreeCoeffBound

formal source

1409The coefficient bound part is proved from `UniformBoundsHypothesis` + convergence.
1410The divergence-free part is proved from the extra assumption that *each approximant* is divergence-free.
1411-/
1412def divFreeCoeffBound {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H)
1413    (hDF : ∀ N : ℕ, ∀ t : ℝ, ∀ k : Mode2, divConstraint k ((extendByZero (H.uN N t)) k) = 0) :
1414    IdentificationHypothesis HC :=
1415  { IsSolution := fun u =>
1416      (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B) ∧ IsDivergenceFreeTraj u
1417    isSolution := by
1418      refine ⟨?_, ?_⟩
1419      · intro t ht k
1420        simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := HC) t ht k)
1421      · intro t k
1422        exact ConvergenceHypothesis.divConstraint_eq_zero_of_forall (HC := HC) (t := t) (k := k)
1423          (hDF := fun N => hDF N t k) }
1424
1425/-- Identification constructor: coefficient bound + (linear) Stokes/heat mild identity.
1426
1427The bound part is proved from `UniformBoundsHypothesis` + convergence.
1428The mild Stokes identity is proved from the extra assumption that it holds for every approximant. -/
1429def stokesMildCoeffBound {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) (ν : ℝ)
1430    (hMild :
1431      ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
1432        (extendByZero (H.uN N t) k) = (heatFactor ν t k) • (extendByZero (H.uN N 0) k)) :
1433    IdentificationHypothesis HC :=
1434  { IsSolution := fun u =>
1435      (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B) ∧ IsStokesMildTraj ν u
1436    isSolution := by
1437      refine ⟨?_, ?_⟩
1438      · intro t ht k
1439        simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := HC) t ht k)
1440      · exact ConvergenceHypothesis.stokesMild_of_forall (HC := HC) (ν := ν) hMild }
1441
1442/-- Identification constructor: coefficient bound + a first nonlinear (Duhamel-style) remainder identity.