89noncomputable def functionalsNormSq (N : ℕ) : Functionals N :=
proof body
Definition body.
90 { defectMass := fun u => ‖u‖ ^ 2 91 orthoMass := fun u => ‖u‖ ^ 2 92 energyGap := fun u => ‖u‖ ^ 2 93 tests := fun u => ‖u‖ ^ 2 } 94 95/-- A no-assumption CPM hypothesis instance using `constantsOne` and `functionalsNormSq`. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.