diff --git a/CvxLean/Command/Solve/Float/Coeffs.lean b/CvxLean/Command/Solve/Float/Coeffs.lean
index c8ba9f35..a7f26e2d 100644
--- a/CvxLean/Command/Solve/Float/Coeffs.lean
+++ b/CvxLean/Command/Solve/Float/Coeffs.lean
@@ -3,6 +3,19 @@ import CvxLean.Lib.Cones.All
 import CvxLean.Command.Solve.Float.ProblemData
 import CvxLean.Command.Solve.Float.RealToFloat
 
+
+/-!
+# Extract coefficients from problem to generate problem data
+
+TODO
+
+## TODO
+
+* This is probably a big source of inefficency for the `solve` command. We should come up with
+  a better way to extract the numerical values from the Lean expressions.
+* A first step is to not `unrollVectors` and turn thos expressions into floats directly.
+-/
+
 namespace CvxLean
 
 open Lean Meta Elab Tactic
@@ -173,13 +186,24 @@ unsafe def unrollVectors (constraints : Expr) : MetaM (Array Expr) := do
           res := res.push (← mkAppM ``Real.expCone #[ai, bi, ci])
     -- Vector second-order cone.
     | .app (.app (.app (.app (.app (.const ``Real.Vec.soCone _)
-        exprN@(.app (.const ``Fin _) n)) (.app (.const ``Fin _) m)) finTypeN) t) X =>
+        exprN@(.app (.const ``Fin _) _n)) (.app (.const ``Fin _) m)) finTypeN) t) X =>
         let m : Nat ← evalExpr Nat (mkConst ``Nat) m
         for i in [:m] do
           let idxExpr ← mkFinIdxExpr i m
           let ti := mkApp t idxExpr
           let Xi := mkApp X idxExpr
           res := res.push (mkAppN (mkConst ``Real.soCone) #[exprN, finTypeN, ti, Xi])
+    -- Vector rotated second-order cone.
+    -- Vector second-order cone.
+    | .app (.app (.app (.app (.app (.app (.const ``Real.Vec.rotatedSoCone _)
+        exprN@(.app (.const ``Fin _) _n)) (.app (.const ``Fin _) m)) finTypeN) v) w) X =>
+        let m : Nat ← evalExpr Nat (mkConst ``Nat) m
+        for i in [:m] do
+          let idxExpr ← mkFinIdxExpr i m
+          let vi := mkApp v idxExpr
+          let wi := mkApp w idxExpr
+          let Xi := mkApp X idxExpr
+          res := res.push (mkAppN (mkConst ``Real.rotatedSoCone) #[exprN, finTypeN, vi, wi, Xi])
     | _ =>
         res := res.push c
 
@@ -254,7 +278,10 @@ unsafe def determineCoeffsFromExpr (minExpr : Meta.MinimizationExpr) :
     let mut idx := 0
     for c in cs do
       trace[Meta.debug] "Coeffs going through constraint {c}."
+      let mut isTrivial := false
       match Expr.consumeMData c with
+      | .const ``True _ => do
+          isTrivial := true
       | .app (.const ``Real.zeroCone _) e => do
           let e ← realToFloat e
           let res ← determineScalarCoeffsAux e p floatDomain
@@ -331,7 +358,8 @@ unsafe def determineCoeffsFromExpr (minExpr : Meta.MinimizationExpr) :
               idx := idx + 1
       | _ => throwError "No match: {c}."
       -- New group, add idx.
-      sections := sections.push idx
+      if !isTrivial then
+        sections := sections.push idx
     return (data, sections)
 
   let (objectiveDataA, objectiveDataB) := objectiveData
diff --git a/CvxLean/Command/Solve/Float/RealToFloat.lean b/CvxLean/Command/Solve/Float/RealToFloat.lean
index 2ccfe240..c8981bdd 100644
--- a/CvxLean/Command/Solve/Float/RealToFloat.lean
+++ b/CvxLean/Command/Solve/Float/RealToFloat.lean
@@ -24,15 +24,25 @@ partial def realToFloat (e : Expr) : MetaM Expr := do
   for translation in translations do
     let (mvars, _, pattern) ← lambdaMetaTelescope translation.real
     if ← isDefEq pattern e then
-    -- TODO: Search for conditions.
+      -- TODO: Search for conditions.
       let args ← mvars.mapM instantiateMVars
       return mkAppNBeta translation.float args
     else
       trace[Meta.debug] "`real-to-float` error: no match for \n{pattern} \n{e}"
   match e with
   | Expr.app a b => return mkApp (← realToFloat a) (← realToFloat b)
-  | Expr.lam n ty b d => return mkLambda n d (← realToFloat ty) (← realToFloat b)
-  | Expr.forallE n ty b d => return mkForall n d (← realToFloat ty) (← realToFloat b)
+  | Expr.lam n ty b d => do
+      withLocalDecl n d (← realToFloat ty) fun fvar => do
+        let b := b.instantiate1 fvar
+        let bF ← realToFloat b
+        mkLambdaFVars #[fvar] bF
+      -- return mkLambda n d (← realToFloat ty) (← realToFloat b)
+  | Expr.forallE n ty b d => do
+      withLocalDecl n d (← realToFloat ty) fun fvar => do
+        let b := b.instantiate1 fvar
+        let bF ← realToFloat b
+        mkForallFVars #[fvar] bF
+      -- return mkForall n d (← realToFloat ty) (← realToFloat b)
   | Expr.mdata m e => return mkMData m (← realToFloat e)
   | Expr.letE n ty t b _ => return mkLet n (← realToFloat ty) (← realToFloat t) (← realToFloat b)
   | Expr.proj typeName idx struct => return mkProj typeName idx (← realToFloat struct)
@@ -183,12 +193,18 @@ addRealToFloat (i) : @instHDiv Real i :=
 addRealToFloat (i) : @HPow.hPow Real Nat Real i :=
   fun f n => Float.pow f (Float.ofNat n)
 
-addRealToFloat (i) : @HPow.hPow Real Real Real i :=
+addRealToFloat (i) : @HPow.hPow.{0, 0, 0} Real Real Real i :=
   fun f n => Float.pow f n
 
-addRealToFloat (i) : @instHPow Real i :=
+addRealToFloat (β) (i) : @instHPow Real β i :=
   @HPow.mk Float Float Float Float.pow
 
+addRealToFloat (n) (i) : @HPow.hPow (Fin n → Real) Real (Fin n → Real) i :=
+  fun (x : Fin n → Float) (p : Float) (i : Fin n) => Float.pow (x i) p
+
+addRealToFloat (n) (β) (i) : @instHPow (Fin n → Real) β i :=
+  @HPow.mk (Fin n → Float) Float (Fin n → Float) (fun x p i => Float.pow (x i) p)
+
 addRealToFloat (i) : @LE.le Real i :=
   Float.le
 
@@ -210,6 +226,12 @@ addRealToFloat : @Real.sqrt :=
 addRealToFloat : @Real.log :=
   Float.log
 
+def Float.norm {n : ℕ} (x : Fin n → Float) : Float :=
+  Float.sqrt (Vec.Computable.sum (fun i => (Float.pow (x i) 2)))
+
+addRealToFloat (n) (i) : @Norm.norm.{0} (Fin n → ℝ) i :=
+  @Float.norm n
+
 addRealToFloat (i) : @OfScientific.ofScientific Real i :=
   Float.ofScientific
 
@@ -260,9 +282,12 @@ addRealToFloat (n) (i) (hn) : @Vec.sum.{0} ℝ i (Fin n) hn :=
 addRealToFloat (n) (i) (hn) : @Matrix.sum (Fin n) Real hn i :=
   @Matrix.Computable.sum n
 
-addRealToFloat (n) : @Vec.cumsum n :=
+addRealToFloat (n) (i) : @Vec.cumsum.{0} ℝ i n :=
   @Vec.Computable.cumsum n
 
+addRealToFloat : @Vec.norm :=
+  @Vec.Computable.norm
+
 addRealToFloat (n) (i1) (i2) (i3) : @Matrix.dotProduct (Fin n) ℝ i1 i2 i3 :=
   @Matrix.Computable.dotProduct n
 
diff --git a/CvxLean/Examples/All.lean b/CvxLean/Examples/All.lean
index ea00d3ce..eed9a70d 100644
--- a/CvxLean/Examples/All.lean
+++ b/CvxLean/Examples/All.lean
@@ -1,5 +1,5 @@
 import CvxLean.Examples.CovarianceEstimation
 import CvxLean.Examples.FittingSphere
 import CvxLean.Examples.HypersonicShapeDesign
-import CvxLean.Examples.OptimalVehicleSpeed
 import CvxLean.Examples.TrussDesign
+import CvxLean.Examples.VehicleSpeedScheduling
diff --git a/CvxLean/Examples/FittingSphere.lean b/CvxLean/Examples/FittingSphere.lean
index a4e2b8ea..9f750a8e 100644
--- a/CvxLean/Examples/FittingSphere.lean
+++ b/CvxLean/Examples/FittingSphere.lean
@@ -2,9 +2,68 @@ import CvxLean
 
 noncomputable section
 
-namespace FittingSphere
+open CvxLean Minimization Real BigOperators Matrix Finset
+
+section LeastSquares
+
+def leastSquares {n : ℕ} (a : Fin n → ℝ) :=
+  optimization (x : ℝ)
+    minimize (∑ i, ((a i - x) ^ 2) : ℝ)
+
+@[reducible]
+def mean {n : ℕ} (a : Fin n → ℝ) : ℝ := (1 / n) * ∑ i, (a i)
+
+/-- It is useful to rewrite the sum of squares in the following way to prove
+`leastSquares_optimal_eq_mean`, following Marty Cohen's answer in
+https://math.stackexchange.com/questions/2554243. -/
+lemma leastSquares_alt_objFun {n : ℕ} (hn : 0 < n) (a : Fin n → ℝ) (x : ℝ) :
+  (∑ i, ((a i - x) ^ 2)) = n * ((x - mean a) ^ 2 + (mean (a ^ 2) - (mean a) ^ 2)) := by
+  calc
+  -- 1) Σ (aᵢ - x)² = Σ (aᵢ² - 2aᵢx + x²)
+  _ = ∑ i, ((a i) ^ 2 - 2 * (a i) * x + (x ^ 2)) := by
+    congr; funext i; simp; ring
+  -- 2) ... = Σ aᵢ² - 2xΣ aᵢ + nx²
+  _ = ∑ i, ((a i) ^ 2) - 2 * x * ∑ i, (a i) + n * (x ^ 2) := by
+    rw [sum_add_distrib, sum_sub_distrib, ← sum_mul, ← mul_sum]; simp [sum_const]; ring
+  -- 3) ... = n{a²} - 2xn{a} + nx²
+  _ = n * mean (a ^ 2) - 2 * x * n * mean a + n * (x ^ 2) := by
+    simp [mean]; field_simp; ring
+  -- 4) ... = n((x - {a})² + ({a²} - {a}²))
+  _ = n * ((x - mean a) ^ 2 + (mean (a ^ 2) - (mean a) ^ 2)) := by
+    simp [mean]; field_simp; ring
+
+/-- Key result about least squares: `x* = mean a`. -/
+lemma leastSquares_optimal_eq_mean {n : ℕ} (hn : 0 < n) (a : Fin n → ℝ) (x : ℝ)
+  (h : (leastSquares a).optimal x) : x = mean a := by
+  simp [optimal, feasible, leastSquares] at h
+  replace h : ∀ y, (x - mean a) ^ 2 ≤ (y - mean a) ^ 2  := by
+    intros y
+    have hy := h y
+    have h_rw_x := leastSquares_alt_objFun hn a x
+    have h_rw_y := leastSquares_alt_objFun hn a y
+    simp only [rpow_two] at h_rw_x h_rw_y ⊢
+    rwa [h_rw_x, h_rw_y, mul_le_mul_left (by positivity), add_le_add_iff_right] at hy
+  have hmean := h (mean a)
+  simp at hmean
+  have hz := le_antisymm hmean (sq_nonneg _)
+  rwa [sq_eq_zero_iff, sub_eq_zero] at hz
+
+def Vec.leastSquares {n : ℕ} (a : Fin n → ℝ) :=
+  optimization (x : ℝ)
+    minimize (Vec.sum ((a - Vec.const n x) ^ 2) : ℝ)
+
+/-- Same as `leastSquares_optimal_eq_mean` in vector notation. -/
+lemma vec_leastSquares_optimal_eq_mean {n : ℕ} (hn : 0 < n) (a : Fin n → ℝ) (x : ℝ)
+  (h : (Vec.leastSquares a).optimal x) : x = mean a := by
+  apply leastSquares_optimal_eq_mean hn a
+  simp [Vec.leastSquares, leastSquares, optimal, feasible] at h ⊢
+  intros y
+  simp only [Vec.sum, Pi.pow_apply, Pi.sub_apply, Vec.const, rpow_two] at h
+  exact h y
 
-open CvxLean Minimization Real BigOperators Matrix
+end LeastSquares
+
+namespace FittingSphere
 
 -- Dimension.
 variable (n : ℕ)
@@ -19,7 +78,144 @@ def fittingSphere :=
   optimization (c : Fin n → ℝ) (r : ℝ)
     minimize (∑ i, (‖(x i) - c‖ ^ 2 - r ^ 2) ^ 2 : ℝ)
     subject to
-      _ : True
+      h₁ : 0 < r
+
+instance : ChangeOfVariables fun (ct : (Fin n → ℝ) × ℝ) => (ct.1, sqrt (ct.2 + ‖ct.1‖ ^ 2)) :=
+  { inv := fun (c, r) => (c, r ^ 2 - ‖c‖ ^ 2),
+    condition := fun (_, t) => 0 ≤ t,
+    property := fun ⟨c, t⟩ h => by simp [sqrt_sq h] }
+
+set_option trace.Meta.debug true
+
+equivalence' eqv/fittingSphereT (n m : ℕ) (x : Fin m → Fin n → ℝ) : fittingSphere n m x := by
+  -- Change of variables.
+  equivalence_step =>
+    apply ChangeOfVariables.toEquivalence
+      (fun (ct : (Fin n → ℝ) × ℝ) => (ct.1, sqrt (ct.2 + ‖ct.1‖ ^ 2)))
+    . rintro _ h; exact le_of_lt h
+  rename_vars [c, t]
+  -- Clean up.
+  conv_constr h₁ => dsimp
+  conv_obj => dsimp
+  -- Rewrite objective.
+  equivalence_step =>
+    apply Equivalence.rewrite_objFun
+      (g := fun (ct : (Fin n → ℝ) × ℝ) =>
+        Vec.sum (((Vec.norm x) ^ 2 - 2 * (Matrix.mulVec x ct.1) - Vec.const m ct.2) ^ 2))
+    . rintro ⟨c, t⟩ h
+      dsimp at h ⊢; simp [Vec.sum, Vec.norm, Vec.const]
+      congr; funext i; congr 1;
+      rw [@norm_sub_sq ℝ (Fin n → ℝ) _ (PiLp.normedAddCommGroup _ _) (PiLp.innerProductSpace _)]
+      rw [sq_sqrt (rpow_two _ ▸ le_of_lt (sqrt_pos.mp <| h))]
+      simp [mulVec, inner, dotProduct]
+  rename_vars [c, t]
+
+#print fittingSphereT
+
+relaxation rel/fittingSphereConvex (n m : ℕ) (x : Fin m → Fin n → ℝ) : fittingSphereT n m x := by
+  relaxation_step =>
+    apply Relaxation.weaken_constraint (cs' := fun _ => True)
+    . rintro ⟨c, t⟩ _; trivial
+
+/-- If the squared error is zero, then `aᵢ = x`. -/
+lemma vec_squared_norm_error_eq_zero_iff {n m : ℕ} (a : Fin m → Fin n → ℝ) (x : Fin n → ℝ) :
+    ∑ i, ‖a i - x‖ ^ 2 = 0 ↔ ∀ i, a i = x := by
+  simp [rpow_two]
+  rw [sum_eq_zero_iff_of_nonneg (fun _ _ => sq_nonneg _)]
+  constructor
+  . intros h i
+    have hi := h i (by simp)
+    rw [sq_eq_zero_iff, @norm_eq_zero _ (PiLp.normedAddCommGroup _ _).toNormedAddGroup] at hi
+    rwa [sub_eq_zero] at hi
+  . intros h i _
+    rw [sq_eq_zero_iff, @norm_eq_zero _ (PiLp.normedAddCommGroup _ _).toNormedAddGroup, sub_eq_zero]
+    exact h i
+
+/-- This tells us that solving the relaxed problem is sufficient for optimal points if the solution
+is non-trivial. -/
+lemma optimal_relaxed_implies_optimal (hm : 0 < m) (c : Fin n → ℝ) (t : ℝ)
+  (h_nontrivial : x ≠ Vec.const m c)
+  (h_opt : (fittingSphereConvex n m x).optimal (c, t)) : (fittingSphereT n m x).optimal (c, t) := by
+  simp [fittingSphereT, fittingSphereConvex, optimal, feasible] at h_opt ⊢
+  constructor
+  . let a := Vec.norm x ^ 2 - 2 * mulVec x c
+    have h_ls : optimal (Vec.leastSquares a) t := by
+      refine ⟨trivial, ?_⟩
+      intros y _
+      simp [objFun, Vec.leastSquares]
+      exact h_opt c y
+    -- Apply key result about least squares to `a` and `t`.
+    have ht_eq := vec_leastSquares_optimal_eq_mean hm a t h_ls
+    have hc2_eq : ‖c‖ ^ 2 = (1 / m) * ∑ i : Fin m, ‖c‖ ^ 2 := by
+      simp [sum_const]
+      field_simp; ring
+    have ht : t + ‖c‖ ^ 2 = (1 / m) * ∑ i, ‖(x i) - c‖ ^ 2 := by
+      rw [ht_eq]; dsimp [mean]
+      rw [hc2_eq, mul_sum, mul_sum, mul_sum, ← sum_add_distrib]
+      congr; funext i; rw [← mul_add]
+      congr; simp [Vec.norm]
+      rw [@norm_sub_sq ℝ (Fin n → ℝ) _ (PiLp.normedAddCommGroup _ _) (PiLp.innerProductSpace _)]
+      congr
+    -- We use the result to establish that `t + ‖c‖ ^ 2` is non-negative.
+    have h_tc2_nonneg : 0 ≤ t + ‖c‖ ^ 2 := by
+      rw [ht]
+      apply mul_nonneg (by norm_num)
+      apply sum_nonneg
+      intros i _
+      rw [rpow_two]
+      exact sq_nonneg _
+    cases (lt_or_eq_of_le h_tc2_nonneg) with
+    | inl h_tc2_lt_zero =>
+        -- If it is positive, we are done.
+        convert h_tc2_lt_zero; simp
+    | inr h_tc2_eq_zero =>
+        -- Otherwise, it contradicts the non-triviality assumption.
+        exfalso
+        rw [ht, zero_eq_mul] at h_tc2_eq_zero
+        rcases h_tc2_eq_zero with (hc | h_sum_eq_zero)
+        . simp at hc; linarith
+        rw [vec_squared_norm_error_eq_zero_iff] at h_sum_eq_zero
+        apply h_nontrivial
+        funext i
+        exact h_sum_eq_zero i
+  . intros c' x' _
+    exact h_opt c' x'
+
+#print fittingSphereConvex
+
+-- We proceed to solve the problem on a concrete example.
+-- https://github.com/cvxgrp/cvxbook_additional_exercises/blob/main/python/sphere_fit_data.py
+
+@[optimization_param]
+def nₚ := 2
+
+@[optimization_param]
+def mₚ := 10
+
+@[optimization_param]
+def xₚ : Fin mₚ → Fin nₚ → ℝ := Matrix.transpose <| ![
+  ![1.824183228637652032e+00, 1.349093690455489103e+00, 6.966316403935147727e-01,
+    7.599387854623529392e-01, 2.388321695850912363e+00, 8.651370608981923116e-01,
+    1.863922545015865406e+00, 7.099743941474848663e-01, 6.005484882320809570e-01,
+    4.561429569892232472e-01],
+  ![-9.644136284187876385e-01, 1.069547315003422927e+00, 6.733229334437943470e-01,
+    7.788072961810316164e-01, -9.467465278344706636e-01, -8.591303443863639311e-01,
+    1.279527420871080956e+00, 5.314829019311283487e-01, 6.975676079749143499e-02,
+    -4.641873429414754559e-01]]
+
+-- We use the `solve` command on the data above.
+
+set_option maxHeartbeats 1000000
+
+solve fittingSphereConvex nₚ mₚ xₚ
+
+-- Finally, we recover the solution to the original problem.
+
+def sol := eqv.backward_map nₚ mₚ xₚ.float fittingSphereConvex.solution
+
+#print eqv.backward_map
+
+#eval sol -- (![1.664863, 0.031932], 1.159033)
 
 end FittingSphere
 
diff --git a/CvxLean/Examples/OptimalVehicleSpeed.lean b/CvxLean/Examples/VehicleSpeedScheduling.lean
similarity index 92%
rename from CvxLean/Examples/OptimalVehicleSpeed.lean
rename to CvxLean/Examples/VehicleSpeedScheduling.lean
index 9063f8a7..f842721d 100644
--- a/CvxLean/Examples/OptimalVehicleSpeed.lean
+++ b/CvxLean/Examples/VehicleSpeedScheduling.lean
@@ -2,7 +2,7 @@ import CvxLean
 
 noncomputable section
 
-namespace OptimalVehicleSpeed
+namespace VehicleSpeedSched
 
 open CvxLean Minimization Real BigOperators Matrix
 
@@ -23,7 +23,7 @@ variable (F : ℝ → ℝ)
 
 open FinsetInterval
 
-def optimalVehicleSpeed [Fact (0 < n)] :=
+def vehSpeedSched [Fact (0 < n)] :=
   optimization (s : Fin n → ℝ)
     minimize ∑ i, (d i / s i) * F (s i)
     subject to
@@ -46,9 +46,9 @@ private lemma fold_partial_sum [hn : Fact (0 < n)] (t : Fin n → ℝ) (i : Fin
   . rfl
   . linarith [hn.out]
 
-equivalence' eqv₁/optimalVehicleSpeedConvex (n : ℕ) (d : Fin n → ℝ)
+equivalence' eqv₁/vehSpeedSchedConvex (n : ℕ) (d : Fin n → ℝ)
     (τmin τmax smin smax : Fin n → ℝ) (F : ℝ → ℝ) (h_n_pos : 0 < n) (h_d_pos : StrongLT 0 d)
-    (h_smin_pos : StrongLT 0 smin) : @optimalVehicleSpeed n d τmin τmax smin smax F ⟨h_n_pos⟩ := by
+    (h_smin_pos : StrongLT 0 smin) : @vehSpeedSched n d τmin τmax smin smax F ⟨h_n_pos⟩ := by
   replace h_d_pos : ∀ i, 0 < d i := fun i => h_d_pos i
   replace h_smin_pos : ∀ i, 0 < smin i := fun i => h_smin_pos i
   haveI : Fact (0 < n) := ⟨h_n_pos⟩
@@ -81,7 +81,7 @@ equivalence' eqv₁/optimalVehicleSpeedConvex (n : ℕ) (d : Fin n → ℝ)
   rename_vars [t]
   rename_constrs [c_smin, c_smax, c_τmin, c_τmax]
 
-#print optimalVehicleSpeedConvex
+#print vehSpeedSchedConvex
 
 #check eqv₁.backward_map
 
@@ -92,10 +92,10 @@ equivalence' eqv₁/optimalVehicleSpeedConvex (n : ℕ) (d : Fin n → ℝ)
 -- We fix `F` and declare an atom for this particular application of the perspective function.
 -- Let `F(s) = a * s^2 + b * s + c` with `0 ≤ a`.
 
-equivalence' eqv₂/optimalVehicleSpeedQuadratic (n : ℕ) (d : Fin n → ℝ)
+equivalence' eqv₂/vehSpeedSchedQuadratic (n : ℕ) (d : Fin n → ℝ)
     (τmin τmax smin smax : Fin n → ℝ) (a b c : ℝ) (h_n_pos : 0 < n) (h_d_pos : StrongLT 0 d)
     (h_smin_pos : StrongLT 0 smin) :
-    optimalVehicleSpeedConvex n d τmin τmax smin smax (fun s => a • s ^ (2 : ℝ) + b • s + c)
+    vehSpeedSchedConvex n d τmin τmax smin smax (fun s => a • s ^ (2 : ℝ) + b • s + c)
       h_n_pos h_d_pos h_smin_pos := by
   have t_pos_of_c_smin : ∀ t, smin ≤ d / t → StrongLT 0 t := fun t h i => by
     have h_di_div_ti_pos := lt_of_lt_of_le (h_smin_pos i) (h i)
@@ -129,7 +129,7 @@ equivalence' eqv₂/optimalVehicleSpeedQuadratic (n : ℕ) (d : Fin n → ℝ)
   rename_constrs [c_t, c_smin, c_smax, c_τmin, c_τmax]
   -- Finally, we can apply `dcp`! (or we can call `solve`, as we do below).
 
-#print optimalVehicleSpeedQuadratic
+#print vehSpeedSchedQuadratic
 
 #check eqv₂.backward_map
 
@@ -195,7 +195,7 @@ def bₚ : ℝ := 6
 @[optimization_param]
 def cₚ : ℝ := 10
 
-def p := optimalVehicleSpeedQuadratic nₚ dₚ τminₚ τmaxₚ sminₚ smaxₚ aₚ bₚ cₚ nₚ_pos dₚ_pos sminₚ_pos
+def p := vehSpeedSchedQuadratic nₚ dₚ τminₚ τmaxₚ sminₚ smaxₚ aₚ bₚ cₚ nₚ_pos dₚ_pos sminₚ_pos
 
 set_option trace.Meta.debug true
 
@@ -221,6 +221,6 @@ def sol := eqv₁.backward_mapₚ (eqv₂.backward_mapₚ p.solution)
 -- ![0.955578, 0.955548, 0.955565, 0.955532, 0.955564, 0.955560, 0.912362, 0.960401, 0.912365,
 --   0.912375]
 
-end OptimalVehicleSpeed
+end VehicleSpeedSched
 
 end
diff --git a/CvxLean/Examples/covariance_estimation.py b/CvxLean/Examples/covariance_estimation.py
new file mode 100644
index 00000000..7d2be7b6
--- /dev/null
+++ b/CvxLean/Examples/covariance_estimation.py
@@ -0,0 +1,32 @@
+import numpy as np
+import cvxpy as cp
+
+n = 2
+
+N = 4
+
+alpha = 1
+
+Y = np.array([[0, 2], [2, 0], [-2, 0], [0, -2]])
+
+R = cp.Variable(shape=(n, n), PSD=True)
+
+def covMat(X):
+    # TODO: Different from np.cov(X, rowvar=False) ?
+    (N, n) = X.shape
+    res = np.zeros((n, n))
+    for i in range(n):
+        for j in range(n):
+            res[i, j] = np.sum([X[k, i] * X[k, j] for k in range(N)]) / N
+    return res
+
+p = cp.Problem(
+    cp.Minimize(
+            -(-(N * np.log(np.sqrt((2 * np.pi) ** n)) + (N * (-cp.log_det(R) / 2))) +
+            -(N * cp.trace(covMat(Y) * cp.transpose(R)) / 2))
+        ), [
+        cp.sum(cp.abs(R)) <= alpha
+    ])
+p.solve(solver=cp.MOSEK, verbose=True)
+
+print("R* = ", R.value)
diff --git a/CvxLean/Examples/fitting_sphere.py b/CvxLean/Examples/fitting_sphere.py
new file mode 100644
index 00000000..025fb7fc
--- /dev/null
+++ b/CvxLean/Examples/fitting_sphere.py
@@ -0,0 +1,32 @@
+import numpy as np
+import cvxpy as cp
+
+n = 2
+
+m = 10
+
+x = np.array([[
+    1.824183228637652032e+00, 1.349093690455489103e+00, 6.966316403935147727e-01,
+    7.599387854623529392e-01, 2.388321695850912363e+00, 8.651370608981923116e-01,
+    1.863922545015865406e+00, 7.099743941474848663e-01, 6.005484882320809570e-01,
+    4.561429569892232472e-01], [
+    -9.644136284187876385e-01, 1.069547315003422927e+00, 6.733229334437943470e-01,
+    7.788072961810316164e-01, -9.467465278344706636e-01, -8.591303443863639311e-01,
+    1.279527420871080956e+00, 5.314829019311283487e-01, 6.975676079749143499e-02,
+    -4.641873429414754559e-01]]).T
+
+c = cp.Variable((n))
+t = cp.Variable(1)
+
+p = cp.Problem(
+    cp.Minimize(
+            cp.sum([((cp.norm(x[i]) ** 2) - 2 * (x[i] @ c) - t) ** 2 for i in range(m)])
+        ), [])
+p.solve(solver=cp.MOSEK, verbose=True)
+
+# Backward map from change of variables.
+r = np.sqrt(t.value + (np.linalg.norm(c.value) ** 2))
+
+print("t* = ", t.value)
+print("c* = ", c.value)
+print("r* = ", r)
diff --git a/CvxLean/Examples/optimal_vehicle_speed.py b/CvxLean/Examples/vehicle_speed_scheduling.py
similarity index 96%
rename from CvxLean/Examples/optimal_vehicle_speed.py
rename to CvxLean/Examples/vehicle_speed_scheduling.py
index d126fb5a..77ae6212 100644
--- a/CvxLean/Examples/optimal_vehicle_speed.py
+++ b/CvxLean/Examples/vehicle_speed_scheduling.py
@@ -1,6 +1,5 @@
 import numpy as np
 import cvxpy as cp
-import matplotlib.pyplot as plt 
 
 n = 10
 
diff --git a/CvxLean/Lib/Math/Data/Real.lean b/CvxLean/Lib/Math/Data/Real.lean
index ea0dd3f7..a333d225 100644
--- a/CvxLean/Lib/Math/Data/Real.lean
+++ b/CvxLean/Lib/Math/Data/Real.lean
@@ -11,6 +11,9 @@ some components of our automated procedures such as pattern-matching in `dcp` or
 @[default_instance]
 noncomputable instance (priority := high) : HPow ℝ ℝ ℝ := by infer_instance
 
+@[default_instance]
+noncomputable instance (priority := high) : HPow (Fin n → ℝ) ℝ (Fin n → ℝ) := by infer_instance
+
 section Functions
 
 /-!
diff --git a/CvxLean/Lib/Math/Data/Vec.lean b/CvxLean/Lib/Math/Data/Vec.lean
index a7e39c5a..aff173f4 100644
--- a/CvxLean/Lib/Math/Data/Vec.lean
+++ b/CvxLean/Lib/Math/Data/Vec.lean
@@ -1,3 +1,4 @@
+import Mathlib.Analysis.NormedSpace.PiLp
 import CvxLean.Lib.Math.Data.Real
 import CvxLean.Lib.Math.Data.Fin
 
@@ -39,7 +40,7 @@ def sum {m : Type} [Fintype m] (x : m → α) : α :=
 open FinsetInterval
 
 /-- See `CvxLean.Tactic.DCP.AtomLibrary.Fns.CumSum`. -/
-def cumsum (t : Fin n → ℝ) : Fin n → ℝ :=
+def cumsum (t : Fin n → α) : Fin n → α :=
   fun i => if h : 0 < n then ∑ j in [[⟨0, h⟩, i]], t j else 0
 
 end AddCommMonoid
@@ -55,8 +56,7 @@ Named functions on real vectors, including those defined in
 open Real BigOperators
 
 /-- See `CvxLean.Tactic.DCP.AtomLibrary.Fns.Norm2`. -/
-instance : Norm (m → ℝ) where
-  norm x := sqrt (∑ i, (x i) ^ 2)
+instance : Norm (m → ℝ) := PiLp.hasNorm 2 _
 
 variable (x y : m → ℝ)
 
@@ -75,6 +75,10 @@ def huber : m → ℝ := fun i => Real.huber (x i)
 /-- See `CvxLean.Tactic.DCP.AtomLibrary.Fns.KLDiv`. -/
 def klDiv : m → ℝ := fun i => Real.klDiv (x i) (y i)
 
+/-- See `CvxLean.Tactic.DCP.AtomLibrary.Fns.Norm2`. -/
+def norm {n m : ℕ} (x : Fin n → Fin m → ℝ) : Fin n → ℝ :=
+  fun i => ‖x i‖
+
 end Real
 
 
@@ -116,6 +120,9 @@ def sum (x : Fin n → Float) : Float :=
 def cumsum (x : Fin n → Float) : Fin n → Float :=
   fun i => (((toArray x).toList.take (i.val + 1)).foldl Float.add 0)
 
+def norm {n m : ℕ} (x : Fin n → Fin m → Float) : Fin n → Float :=
+  fun i => Float.sqrt (sum (Vec.map (Float.pow · 2) (x i)))
+
 end Computable
 
 end Vec
diff --git a/CvxLean/Lib/Relaxation.lean b/CvxLean/Lib/Relaxation.lean
index ab3ec4ea..a43d3988 100644
--- a/CvxLean/Lib/Relaxation.lean
+++ b/CvxLean/Lib/Relaxation.lean
@@ -106,6 +106,11 @@ def remove_constraint {c cs' : D → Prop} (hcs : ∀ x, cs x ↔ c x ∧ cs' x)
     phi_feasibility := fun x h_feas_x => ((hcs x).mp h_feas_x).2,
     phi_optimality := fun _ _ => le_refl _ }
 
+def weaken_constraint (cs' : D → Prop) (hcs : ∀ x, cs x → cs' x) : ⟨f, cs⟩ ≽' ⟨f, cs'⟩ :=
+  { phi := id,
+    phi_feasibility := fun x h_feas_x => hcs x h_feas_x,
+    phi_optimality := fun _ _ => le_refl _ }
+
 end Relaxation
 
 end Minimization
diff --git a/CvxLean/Syntax/Minimization.lean b/CvxLean/Syntax/Minimization.lean
index e4bee31e..b2c89616 100644
--- a/CvxLean/Syntax/Minimization.lean
+++ b/CvxLean/Syntax/Minimization.lean
@@ -30,12 +30,16 @@ partial def elabVars (idents : Array Syntax) : TermElabM (Array (Lean.Name × Ex
       | _ => throwError "Expected identifier: {id}"
   return idents
 
+macro_rules
+| `(optimization $idents* $minOrMax:minOrMax $obj) =>
+    `(optimization $idents* $minOrMax:minOrMax $obj subject to _ : True)
+
 -- TODO: allow dependently typed variables?
 
 /-- Elaborate "optimization" problem syntax. -/
 @[term_elab «optimization»] def elabOptmiziation : Term.TermElab := fun stx expectedType? => do
   match stx with
-  | `(optimization $idents* $minOrMax:minOrMax $obj subject to $constraints ) =>
+  | `(optimization $idents* $minOrMax:minOrMax $obj subject to $constraints) =>
     -- Determine names and types of the variables.
     let vars ← elabVars <| idents.map (·.raw)
     -- Construct domain type.
@@ -125,32 +129,33 @@ def withDomainBinding [Inhabited α] (domain : Expr) (x : DelabM α) : DelabM α
 partial def delabMinimization : Delab := do
   if not (pp.optMinimization.get (← getOptions)) then Alternative.failure
   match ← getExpr with
-  | Expr.app
-      (Expr.app
-        (Expr.app
-          (Expr.app (Expr.const `Minimization.mk _) domain)
-          codomain)
-        objFun) constraints  =>
-    let constraints : Array Syntax := #[]
-    let idents ← withType $ withNaryArg 0 do
+  | .app (.app (.app (.app (.const `Minimization.mk _) domain) codomain) objFun) constraints =>
+    let idents ← withType <| withNaryArg 0 do
       let tys ← delabDomain
-      let tys ← tys.mapM fun (name, stx) => do
-        `(Parser.minimizationVar|($(mkIdent name) : $stx))
+      let tys ← tys.mapM fun (name, stx) => do `(Parser.minimizationVar| ($(mkIdent name) : $stx))
       return tys.toArray
     let (objFun, isMax) ← withNaryArg 2 do withDomainBinding domain do
       match ← getExpr with
-      | Expr.app (Expr.app (Expr.app (Expr.const ``maximizeNeg _) _) _) e =>
-        withExpr e do
-          return (← delab, true)
+      | .app (.app (.app (.const ``maximizeNeg _) _) _) e =>
+          withExpr e do
+            return (← delab, true)
       | _ =>
-        return (← delab, false)
+          return (← delab, false)
+    let noConstrs ← withLambdaBody constraints fun _ constrsBody => do
+      isDefEq constrsBody (mkConst ``True)
     let constraints := ← withNaryArg 3 do
       let cs ← withDomainBinding domain delabConstraints
       return mkNode ``Parser.constraints #[mkNullNode <| cs.toArray.map (·.raw)]
-    if isMax then
-      `(optimization $idents* maximize $objFun subject to $constraints)
+    if noConstrs then
+      if isMax then
+        `(optimization $idents* maximize $objFun)
+      else
+        `(optimization $idents*  minimize $objFun)
     else
-      `(optimization $idents* minimize $objFun subject to $constraints)
+      if isMax then
+        `(optimization $idents* maximize $objFun subject to $constraints)
+      else
+        `(optimization $idents* minimize $objFun subject to $constraints)
   | _ => Alternative.failure
 
 end Delab
diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Norm.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Norm.lean
index 94ee4cb3..18c06dce 100644
--- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Norm.lean
+++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Norm.lean
@@ -7,6 +7,8 @@ namespace CvxLean
 
 open Real
 
+#check sqrt_eq_rpow
+
 declare_atom norm2 [convex] (n : Nat)& (x : Fin n → ℝ)? : ‖x‖ :=
 vconditions
 implementationVars (t : ℝ)
@@ -18,10 +20,10 @@ solutionEqualsAtom by rfl
 feasibility
   (c : by
     unfold soCone
-    simp [Norm.norm])
+    simp [Norm.norm, sqrt_eq_rpow])
 optimality by
   unfold soCone at c
-  simp [Norm.norm] at c ⊢
+  simp [Norm.norm, sqrt_eq_rpow] at c ⊢
   exact c
 vconditionElimination
 
@@ -41,6 +43,24 @@ optimality by
 vconditionElimination
 
 lemma norm2₂_eq_norm2 {x y : ℝ} : ‖![x, y]‖ = sqrt (x ^ 2 + y ^ 2) :=
-  by simp [Norm.norm]
+  by simp [Norm.norm, sqrt_eq_rpow]
+
+declare_atom Vec.norm [convex] (n : Nat)& (m : Nat)&  (x : Fin n → Fin m → ℝ)? : Vec.norm x :=
+vconditions
+implementationVars (t : Fin n → ℝ)
+implementationObjective (t)
+implementationConstraints
+  (c : Vec.soCone t x)
+solution (t := Vec.norm x)
+solutionEqualsAtom by rfl
+feasibility
+  (c : by
+    unfold Vec.soCone soCone; dsimp;
+    intros i; simp [Vec.norm, Norm.norm, sqrt_eq_rpow])
+optimality by
+  unfold Vec.soCone soCone at c
+  intros i; simp [Vec.norm, Norm.norm, sqrt_eq_rpow] at c ⊢
+  exact c i
+vconditionElimination
 
 end CvxLean
diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Sets/Cones.lean b/CvxLean/Tactic/DCP/AtomLibrary/Sets/Cones.lean
index 9441c646..a7e7d569 100644
--- a/CvxLean/Tactic/DCP/AtomLibrary/Sets/Cones.lean
+++ b/CvxLean/Tactic/DCP/AtomLibrary/Sets/Cones.lean
@@ -77,4 +77,12 @@ optimality le_refl _
 
 end PSDCone
 
+/- Trivial cone. -/
+section Trivial
+
+declare_atom trivial [cone] : True :=
+optimality le_refl _
+
+end Trivial
+
 end CvxLean