subspaceModel

formal source

  63
  64/-- Subspace model: K_net = C_proj = 1, functionals satisfy equality.
  65This tests the subspace shortcut lemmas. -/
  66def subspaceModel : Model Unit := {
  67  C := {
  68    Knet := 1,
  69    Cproj := 1,
  70    Ceng := 2,
  71    Cdisp := 1,
  72    Knet_nonneg := by norm_num,
  73    Cproj_nonneg := by norm_num,
  74    Ceng_nonneg := by norm_num,
  75    Cdisp_nonneg := by norm_num
  76  },
  77  defectMass := fun _ => 1,
  78  orthoMass := fun _ => 1,
  79  energyGap := fun _ => 1,
  80  tests := fun _ => 2,
  81  projection_defect := by intro _; norm_num,
  82  energy_control := by intro _; norm_num,
  83  dispersion := by intro _; norm_num
  84}
  85
  86/-- Verify subspace shortcut: D ≤ orthoMass when K_net = C_proj = 1. -/
  87example : subspaceModel.defectMass () ≤ subspaceModel.orthoMass () :=
  88  Model.defect_le_ortho_of_Knet_one_Cproj_one subspaceModel rfl rfl ()
  89
  90/-- Verify subspace equality when orthoMass = defectMass. -/
  91example : subspaceModel.defectMass () = subspaceModel.orthoMass () :=
  92  Model.defect_eq_ortho_of_subspace_case subspaceModel rfl rfl (fun _ => rfl) ()
  93
  94/-! ## Example 3: RS Cone Constants Model -/
  95
  96/-- Model using the canonical RS cone constants. -/