EvolutionIdentity

formal source

  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. -/
  83theorem viscous_term_dissipative {siteCount : ℕ} (c : ContributionFields siteCount)
  84    (hvisc : ∀ i : Fin siteCount, c.viscous i ≤ 0) :
  85    totalViscous c ≤ 0 := by
  86  unfold totalViscous total
  87  exact Finset.sum_nonpos (fun i _ => hvisc i)
  88
  89/-- If every stretching contribution is nonnegative, then the total stretching
  90term is nonnegative. -/
  91theorem stretching_term_nonneg {siteCount : ℕ} (c : ContributionFields siteCount)
  92    (hstretch : ∀ i : Fin siteCount, 0 ≤ c.stretching i) :
  93    0 ≤ totalStretching c := by
  94  unfold totalStretching total
  95  exact Finset.sum_nonneg (fun i _ => hstretch i)
  96
  97/-- A pointwise transport field with zero entries has zero total. -/
  98theorem zero_transport_cancels {siteCount : ℕ} (c : ContributionFields siteCount)