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)
488structure SphericalProjection (P : RM2URadialProfile) where
489 total_energy : ℝ
490 hE_pos : 0 < total_energy
491 projection_bound :
492 IntegrableOn (fun r : ℝ => (P.A r) ^ 2 * r ^ 2) (Set.Ioi (1 : ℝ)) volume
493
494/-- A `SphericalProjection` immediately gives `WeightedL2Moment`. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (6)
Lean names referenced from this declaration's body.
-
A
in IndisputableMonolith.Foundation.IntegrationGap
decl_use
-
A
in IndisputableMonolith.Masses.Anchor
decl_use
-
A
in IndisputableMonolith.Modal.Actualization
decl_use
-
RM2URadialProfile
in IndisputableMonolith.NavierStokes.RM2U.Core
decl_use
-
WeightedL2Moment
in IndisputableMonolith.NavierStokes.RM2U.TailFluxInstantiation
decl_use
-
volume
in IndisputableMonolith.Papers.GCIC.BrainHolography
decl_use