pith. machine review for the scientific record. sign in
def definition def or abbrev

stokesMildCoeffBound

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

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 :=

proof body

Definition body.

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.
1443
1444The coefficient bound part is proved from `UniformBoundsHypothesis` + convergence.
1445The Duhamel-remainder identity is proved from the extra assumptions:
1446
1447- each approximant satisfies `extendByZero uN(t,k) = heatFactor • extendByZero uN(0,k) + D_N(t,k)`, and
1448- `D_N(t,k) → D(t,k)` modewise.
1449
1450In later milestones, `D_N` will be instantiated as an actual time-integrated nonlinear forcing term. -/

depends on (22)

Lean names referenced from this declaration's body.