`ContributionFields`

definition

show as: view math explainer →

module: IndisputableMonolith.NavierStokes.DiscreteVorticity
domain: NavierStokes
line: 52 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NavierStokes.DiscreteVorticity on GitHub at line 52.

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

  49  total (fun i => Jcost (normalizedAmplitude f i))
  50
  51/-- Contribution fields appearing in the J-cost derivative identity. -/
  52structure ContributionFields (siteCount : ℕ) where
  53  transport : Fin siteCount → ℝ
  54  viscous : Fin siteCount → ℝ
  55  stretching : Fin siteCount → ℝ
  56
  57/-- Total contributions of the three pieces. -/
  58def totalTransport {siteCount : ℕ} (c : ContributionFields siteCount) : ℝ :=
  59  total c.transport
  60
  61def totalViscous {siteCount : ℕ} (c : ContributionFields siteCount) : ℝ :=
  62  total c.viscous
  63
  64def totalStretching {siteCount : ℕ} (c : ContributionFields siteCount) : ℝ :=
  65  total c.stretching
  66
  67/-- Data recording an exact J-cost derivative split. -/
  68structure EvolutionIdentity (siteCount : ℕ) where
  69  contributions : ContributionFields siteCount
  70  dJdt : ℝ
  71  split :
  72    dJdt = totalTransport contributions
  73      + totalViscous contributions
  74      + totalStretching contributions
  75
  76/-- If the transport contribution has zero total, it cancels exactly. -/
  77theorem transport_term_cancels {siteCount : ℕ} (c : ContributionFields siteCount)
  78    (htransport : totalTransport c = 0) :
  79    totalTransport c = 0 := htransport
  80
  81/-- If every viscous contribution is nonpositive, then the total viscous term is
  82nonpositive. -/

papers checked against this theorem

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