pith. machine review for the scientific record. sign in
structure definition def or abbrev

OneStepData

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)

  45structure OneStepData where
  46  nu : ℝ
  47  h : ℝ
  48  dt : ℝ
  49  gradMax : ℝ
  50  nu_pos : 0 < nu
  51  h_pos : 0 < h
  52  dt_pos : 0 < dt
  53  gradMax_nonneg : 0 ≤ gradMax
  54  advectionBound : ℝ
  55  advectionBound_nonneg : 0 ≤ advectionBound
  56  advectionBound_le_gradMax : advectionBound ≤ gradMax
  57
  58/-- The viscous contraction rate on the lattice: nu / h^2. -/
  59def OneStepData.viscousRate (data : OneStepData) : ℝ :=

proof body

Definition body.

  60  data.nu / data.h ^ 2
  61
  62theorem OneStepData.viscousRate_pos (data : OneStepData) :
  63    0 < data.viscousRate := by
  64  unfold viscousRate
  65  exact div_pos data.nu_pos (pow_pos data.h_pos 2)
  66
  67/-- The sub-Kolmogorov condition: gradMax <= nu/h^2. -/
  68def OneStepData.subKolmogorov (data : OneStepData) : Prop :=
  69  data.gradMax ≤ data.viscousRate
  70
  71/-- When the sub-Kolmogorov condition holds, the advection rate is
  72dominated by the viscous contraction rate. -/

used by (4)

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

depends on (12)

Lean names referenced from this declaration's body.