`runningMaxCert`

proved

show as: view math explainer →

module: IndisputableMonolith.NavierStokes.RunningMaxNormalization
domain: NavierStokes
line: 353 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NavierStokes.RunningMaxNormalization on GitHub at line 353.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.