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)
44def normalizedAmplitude {siteCount : ℕ} (f : Fin siteCount → ℝ) (i : Fin siteCount) : ℝ :=
proof body
Definition body.
45 |f i| / rms f
46
47/-- The total J-cost of a discrete vorticity field relative to its RMS scale. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
totalJcost
in IndisputableMonolith.NavierStokes.DiscreteVorticity
decl_use
depends on (11)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
scale
in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
rms
in IndisputableMonolith.NavierStokes.DiscreteVorticity
decl_use
-
total
in IndisputableMonolith.NavierStokes.DiscreteVorticity
decl_use
-
total
in IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget
decl_use