pith. machine review for the scientific record. sign in
theorem proved term proof

one_step_factor_le_one

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

formal statement (Lean)

  79theorem one_step_factor_le_one (data : OneStepData)
  80    (hsubK : data.subKolmogorov) :
  81    1 + data.dt * (data.advectionBound - data.viscousRate) ≤ 1 := by

proof body

Term-mode proof.

  82  have h1 : data.advectionBound - data.viscousRate ≤ 0 :=
  83    sub_nonpos.mpr (advection_dominated_by_viscosity data hsubK)
  84  linarith [mul_nonpos_of_nonneg_of_nonpos data.dt_pos.le h1]
  85
  86/-- The gradient maximum is non-increasing under one NS time step when
  87the sub-Kolmogorov condition holds. -/

used by (1)

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

depends on (16)

Lean names referenced from this declaration's body.