theorem proved term proof

`runningMax_mono`

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

formal statement (Lean)

  45theorem runningMax_mono (a : ℕ → ℝ) : Monotone (runningMax a) := by

proof body

Term-mode proof.

  46  intro m n hmn
  47  unfold runningMax
  48  apply Finset.sup'_le
  49  intro k hk
  50  exact Finset.le_sup' a (Finset.range_mono (by omega) hk)
  51
  52/-- The running maximum of a divergent sequence is divergent. -/

used by (2)

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

runningMaxCert in IndisputableMonolith.NavierStokes.RunningMaxNormalization decl_use
runningMax_tendsto_atTop in IndisputableMonolith.NavierStokes.RunningMaxNormalization decl_use

depends on (10)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
runningMax in IndisputableMonolith.NavierStokes.RunningMaxNormalization decl_use