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

RunningMaxCert

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)

 335structure RunningMaxCert where
 336  /-- Running max is monotone. -/
 337  monotone : ∀ a : ℕ → ℝ, Monotone (runningMax a)
 338  /-- Normalization by the running max bounds the rescaled sequence by 1. -/
 339  bounded : ∀ M : ℕ → ℝ, (∀ n, 0 < M n) → ∀ n, normalized M n ≤ 1
 340  /-- A zero of the positive-definite J-cost in `(0,∞)` must occur at `1`. -/
 341  tf_pinch :
 342    ∀ (J : ℝ → ℝ), ConvexOn ℝ (Set.Ioi 0) J → J 1 = 0 →
 343      (∀ x, x ∈ Set.Ioi 0 → x ≠ 1 → J x > 0) →
 344      ∀ x, x ∈ Set.Ioi 0 → J x = 0 → x = 1
 345  /-- Constant vorticity profiles are rigid rotations. -/
 346  rigid_rotation :
 347    ∀ ω₀ : ℝ, ∃ (u : ℝ × ℝ → ℝ × ℝ), ∀ (x : ℝ × ℝ),
 348      u x = (ω₀ / 2 * (-x.2), ω₀ / 2 * x.1)
 349  /-- Nonzero rigid rotations force quartically divergent ball energy. -/
 350  rigid_rotation_energy_diverges :
 351    ∀ (ω₀ : ℝ) (hω₀ : ω₀ ≠ 0), rigid_rotation_infinite_energy ω₀ hω₀
 352

used by (1)

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

depends on (20)

Lean names referenced from this declaration's body.