No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
86def velocityGradientMag {siteCount : ℕ} (Λ : LatticeTopology siteCount) (h : ℝ)
87 (u : VectorField siteCount) (x : Fin siteCount) : ℝ :=
proof body
Definition body.
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. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (11)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
Physical
in IndisputableMonolith.Bridge.DataCore
decl_use
-
or
in IndisputableMonolith.Constants.EulerMascheroni
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
forwardDiff
in IndisputableMonolith.NavierStokes.DiscreteNSOperator
decl_use
-
LatticeTopology
in IndisputableMonolith.NavierStokes.DiscreteNSOperator
decl_use
-
VectorField
in IndisputableMonolith.NavierStokes.DiscreteNSOperator
decl_use
-
VectorField
in IndisputableMonolith.Relativity.Geometry.Tensor
decl_use