theorem proved term proof

`gradient_nonincreasing`

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

formal statement (Lean)

  88theorem gradient_nonincreasing (data : OneStepData)
  89    (hsubK : data.subKolmogorov)
  90    (newGradMax : ℝ)
  91    (h_update : newGradMax ≤
  92      data.gradMax * (1 + data.dt * (data.advectionBound - data.viscousRate))) :
  93    newGradMax ≤ data.gradMax := by

proof body

Term-mode proof.

  94  have hfactor := one_step_factor_le_one data hsubK
  95  exact le_trans h_update (mul_le_of_le_one_right data.gradMax_nonneg hfactor)
  96
  97/-- The sub-Kolmogorov condition is preserved by one step. -/

used by (1)

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

subK_preserved in IndisputableMonolith.NavierStokes.DiscreteMaximumPrinciple decl_use

depends on (15)

Lean names referenced from this declaration's body.

step in IndisputableMonolith.Complexity.CellularAutomata decl_use
le_trans in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
one in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
one in IndisputableMonolith.Foundation.RationalsFromLogic 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
OneStepData in IndisputableMonolith.NavierStokes.DiscreteMaximumPrinciple decl_use
one_step_factor_le_one in IndisputableMonolith.NavierStokes.DiscreteMaximumPrinciple decl_use
viscousRate in IndisputableMonolith.NavierStokes.VortexStretching decl_use
sub in IndisputableMonolith.Numerics.Interval.Basic decl_use
one in IndisputableMonolith.QFT.SpinStatistics decl_use
one in IndisputableMonolith.RecogSpec.Core decl_use
sub in IndisputableMonolith.RecogSpec.Core decl_use