RunningMaxCert

formal source

 332
 333/-! ## Summary Certificate -/
 334
 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
 353theorem runningMaxCert : RunningMaxCert where
 354  monotone := runningMax_mono
 355  bounded := normalized_bounded
 356  tf_pinch := tf_pinch_at_zero_node
 357  rigid_rotation := constant_vorticity_implies_rigid_rotation
 358  rigid_rotation_energy_diverges := rigid_rotation_infinite_energy_proved
 359
 360end RunningMaxNormalization
 361end NavierStokes
 362end IndisputableMonolith