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

coeffBound

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)

1400def coeffBound {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) :
1401    IdentificationHypothesis HC :=

proof body

Definition body.

1402  { IsSolution := fun u => ∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B
1403    isSolution := by
1404      intro t ht k
1405      simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := HC) t ht k) }
1406
1407/-- Identification constructor: coefficient bound + divergence-free (Fourier-side).
1408
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-/

depends on (16)

Lean names referenced from this declaration's body.