velocityGradientMag

formal source

  83/-! ## Velocity Gradient Magnitude -/
  84
  85/-- Maximum absolute forward difference across all component/direction pairs. -/
  86def velocityGradientMag {siteCount : ℕ} (Λ : LatticeTopology siteCount) (h : ℝ)
  87    (u : VectorField siteCount) (x : Fin siteCount) : ℝ :=
  88  Finset.sup' (Finset.univ ×ˢ Finset.univ)
  89    (by exact Finset.Nonempty.product Finset.univ_nonempty Finset.univ_nonempty)
  90    (fun p => |forwardDiff Λ h (fun y => u y p.1) p.2 x|)
  91
  92/-! ## Core NS Operator (physical data only) -/
  93
  94/-- Physical data of a discrete incompressible lattice Navier--Stokes flow.
  95No pair-budget or absorption fields—those are derived below. -/
  96structure CoreNSOperator (siteCount : ℕ) extends EvolutionIdentity siteCount where
  97  topology : LatticeTopology siteCount
  98  h : ℝ
  99  ν : ℝ
 100  h_pos : 0 < h
 101  ν_pos : 0 < ν
 102  state : State siteCount
 103  velocity : VectorField siteCount
 104  divergence_free : ∀ x : Fin siteCount, divergence topology h velocity x = 0
 105  transportFlux : ScalarField siteCount
 106  transportPerm : Equiv.Perm (Fin siteCount)
 107  transport_def :
 108    contributions.transport = conservativeTransportField transportFlux transportPerm
 109  viscous_def :
 110    contributions.viscous = fun x => ν * scalarLaplacian topology h state.omega x
 111  omega_rms : ℝ
 112  omega_rms_pos : 0 < omega_rms
 113  normalized_omega_pos : ∀ i : Fin siteCount, 0 < |state.omega i| / omega_rms
 114  gradientMag_nonneg : ∀ i : Fin siteCount,
 115    0 ≤ velocityGradientMag topology h velocity i
 116  dt : ℝ