functionalsNormSq

formal source

  86    Cdisp_nonneg := by norm_num }
  87
  88/-- Concrete functionals: everything is measured by `‖u‖^2` (a nonnegative scalar). -/
  89noncomputable def functionalsNormSq (N : ℕ) : Functionals N :=
  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`. -/
  96noncomputable def hypothesisNormSq (N : ℕ) : Hypothesis N :=
  97  { C := constantsOne
  98    F := functionalsNormSq N
  99    projection_defect := by
 100      intro a
 101      simp [constantsOne, functionalsNormSq]
 102    energy_control := by
 103      intro a
 104      simp [constantsOne, functionalsNormSq]
 105    dispersion := by
 106      intro a
 107      simp [constantsOne, functionalsNormSq] }
 108
 109/-- The corresponding concrete CPM bridge instance (still minimal/placeholder). -/
 110noncomputable def bridgeNormSq (N : ℕ) : ClassicalBridge.Fluids.CPMBridge (State N) :=
 111  bridge (hypothesisNormSq N)
 112
 113end CPM2D
 114
 115end IndisputableMonolith.ClassicalBridge.Fluids