def definition def or abbrev

`runningMax`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  33noncomputable def runningMax (a : ℕ → ℝ) : ℕ → ℝ :=

proof body

Definition body.

  34  fun n => Finset.sup' (Finset.range (n + 1))
  35    (Finset.nonempty_range_add_one) a
  36
  37/-- The running maximum is always ≥ the current value. -/

used by (9)

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

normalized in IndisputableMonolith.NavierStokes.RunningMaxNormalization decl_use
normalized_eq_one_at_max in IndisputableMonolith.NavierStokes.RunningMaxNormalization decl_use
rescaleLength in IndisputableMonolith.NavierStokes.RunningMaxNormalization decl_use
rescaleLength_tendsto_zero in IndisputableMonolith.NavierStokes.RunningMaxNormalization decl_use
RunningMaxCert in IndisputableMonolith.NavierStokes.RunningMaxNormalization decl_use
runningMax_ge in IndisputableMonolith.NavierStokes.RunningMaxNormalization decl_use
runningMax_mono in IndisputableMonolith.NavierStokes.RunningMaxNormalization decl_use
runningMax_pos in IndisputableMonolith.NavierStokes.RunningMaxNormalization decl_use
runningMax_tendsto_atTop in IndisputableMonolith.NavierStokes.RunningMaxNormalization decl_use

depends on (5)

Lean names referenced from this declaration's body.

is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use