trivialModel

proof body

Definition body.

  31  C := {
  32    Knet := 1,
  33    Cproj := 1,
  34    Ceng := 1,
  35    Cdisp := 1,
  36    Knet_nonneg := by norm_num,
  37    Cproj_nonneg := by norm_num,
  38    Ceng_nonneg := by norm_num,
  39    Cdisp_nonneg := by norm_num
  40  },
  41  defectMass := fun _ => 0,
  42  orthoMass := fun _ => 0,
  43  energyGap := fun _ => 0,
  44  tests := fun _ => 0,
  45  projection_defect := by intro _; norm_num,
  46  energy_control := by intro _; norm_num,
  47  dispersion := by intro _; norm_num
  48}
  49
  50/-- Verify coercivity theorem applies to trivial model. -/
  51example : trivialModel.defectMass () ≤
  52    (trivialModel.C.Knet * trivialModel.C.Cproj * trivialModel.C.Ceng) *
  53    trivialModel.energyGap () :=
  54  trivialModel.defect_le_constants_mul_energyGap ()
  55
  56/-- Verify aggregation theorem applies to trivial model. -/
  57example : trivialModel.defectMass () ≤
  58    (trivialModel.C.Knet * trivialModel.C.Cproj * trivialModel.C.Cdisp) *
  59    trivialModel.tests () :=
  60  trivialModel.defect_le_constants_mul_tests ()
  61
  62/-! ## Example 2: Subspace Model -/
  63
  64/-- Subspace model: K_net = C_proj = 1, functionals satisfy equality.
  65This tests the subspace shortcut lemmas. -/