pith. machine review for the scientific record. sign in
theorem proved term proof

normalized_vorticity_bounded

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)

 130theorem normalized_vorticity_bounded (M : ℕ → ℝ) (hpos : ∀ n, 0 < M n) (n : ℕ) :
 131    normalized M n ≤ 1 :=

proof body

Term-mode proof.

 132  normalized_le_one M n (hpos n)
 133
 134/-- The running maximum is the correct normalization: after normalizing,
 135    the sequence no longer diverges. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.