`ScalarField`

definition

show as: view math explainer →

module: IndisputableMonolith.NavierStokes.DiscreteNSOperator
domain: NavierStokes
line: 36 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NavierStokes.DiscreteNSOperator on GitHub at line 36.

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

  33
  34abbrev Axis := Fin 3
  35
  36abbrev ScalarField (siteCount : ℕ) := Fin siteCount → ℝ
  37
  38abbrev VectorField (siteCount : ℕ) := Fin siteCount → Axis → ℝ
  39
  40structure LatticeTopology (siteCount : ℕ) where
  41  plus : Axis → Fin siteCount → Fin siteCount
  42  minus : Axis → Fin siteCount → Fin siteCount
  43
  44def forwardDiff {siteCount : ℕ} (Λ : LatticeTopology siteCount) (h : ℝ)
  45    (f : ScalarField siteCount) (j : Axis) (x : Fin siteCount) : ℝ :=
  46  (f (Λ.plus j x) - f x) / h
  47
  48def backwardDiff {siteCount : ℕ} (Λ : LatticeTopology siteCount) (h : ℝ)
  49    (f : ScalarField siteCount) (j : Axis) (x : Fin siteCount) : ℝ :=
  50  (f x - f (Λ.minus j x)) / h
  51
  52def scalarLaplacian {siteCount : ℕ} (Λ : LatticeTopology siteCount) (h : ℝ)
  53    (f : ScalarField siteCount) (x : Fin siteCount) : ℝ :=
  54  ∑ j : Axis, forwardDiff Λ h (backwardDiff Λ h f j) j x
  55
  56def vectorLaplacian {siteCount : ℕ} (Λ : LatticeTopology siteCount) (h : ℝ)
  57    (u : VectorField siteCount) (x : Fin siteCount) (i : Axis) : ℝ :=
  58  scalarLaplacian Λ h (fun y => u y i) x
  59
  60def divergence {siteCount : ℕ} (Λ : LatticeTopology siteCount) (h : ℝ)
  61    (u : VectorField siteCount) (x : Fin siteCount) : ℝ :=
  62  ∑ j : Axis, forwardDiff Λ h (fun y => u y j) j x
  63
  64def advection {siteCount : ℕ} (Λ : LatticeTopology siteCount) (h : ℝ)
  65    (u : VectorField siteCount) (x : Fin siteCount) (i : Axis) : ℝ :=
  66  ∑ j : Axis, u x j * forwardDiff Λ h (fun y => u y i) j x

papers checked against this theorem

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