constantsOne

formal source

  75-/
  76
  77/-- A convenient all-ones constant bundle. -/
  78noncomputable def constantsOne : Constants :=
  79  { Knet := 1
  80    Cproj := 1
  81    Ceng := 1
  82    Cdisp := 1
  83    Knet_nonneg := by norm_num
  84    Cproj_nonneg := by norm_num
  85    Ceng_nonneg := by norm_num
  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