module module

`IndisputableMonolith.NavierStokes.RunningMaxNormalization`

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

declarations in this module (20)

def runningMax L33
theorem runningMax_ge L38
theorem runningMax_mono L45
theorem runningMax_tendsto_atTop L53
theorem runningMax_pos L62
def normalized L70
theorem normalized_le_one L74
theorem normalized_eq_one_at_max L80
def rescaleLength L91
theorem rescaleLength_pos L95
theorem rescaleLength_tendsto_zero L102
theorem normalized_vorticity_bounded L130
theorem normalized_bounded L136
theorem tf_pinch_at_zero_node L152
theorem constant_vorticity_implies_rigid_rotation L169
def rigid_rotation_infinite_energy L186
theorem rigid_rotation_energy_lower_bound L190
theorem rigid_rotation_infinite_energy_proved L287
structure RunningMaxCert L335
theorem runningMaxCert L353