`OneStepData`

definition

show as: view math explainer →

module: IndisputableMonolith.NavierStokes.DiscreteMaximumPrinciple
domain: NavierStokes
line: 45 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NavierStokes.DiscreteMaximumPrinciple on GitHub at line 45.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  424. When G_t <= nu/(C*h^2), the bracket is <= 1. -/
  43
  44/-- Data for a single discrete NS time step on a finite lattice. -/
  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) : ℝ :=
  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. -/
  73theorem advection_dominated_by_viscosity (data : OneStepData)
  74    (hsubK : data.subKolmogorov) :
  75    data.advectionBound ≤ data.viscousRate :=

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.