feat: full solution to fitting sphere to data

Author: ramonfmir

CvxLean/Command/Solve/Float/RealToFloat.lean

@@ -23,12 +23,9 @@ partial def realToFloat (e : Expr) : MetaM Expr := do
   let translations ← discrTree.getMatch e
   for translation in translations do
     let (mvars, _, pattern) ← lambdaMetaTelescope translation.real
-    trace[Meta.debug] (s!"`real-to-float` trying:\n{pattern}\n{e}")
-    trace[Meta.debug] (s!"`real-to-float` mvars:\n{mvars}")
     if ← isDefEq pattern e then
       -- TODO: Search for conditions.
       let args ← mvars.mapM instantiateMVars
-      trace[Meta.debug] (s!"`real-to-float` matched:\n{pattern}\n{e}")
       return mkAppNBeta translation.float args
     else
       trace[Meta.debug] "`real-to-float` error: no match for \n{pattern} \n{e}"

CvxLean/Examples/FittingSphere.lean

@@ -211,9 +211,11 @@ solve fittingSphereConvex nₚ mₚ xₚ
 
 -- Finally, we recover the solution to the original problem.
 
-#eval fittingSphereConvex.solution
+def sol := eqv.backward_map nₚ mₚ xₚ.float fittingSphereConvex.solution
 
-def sol := eqv.backward_map
+#print eqv.backward_map
+
+#eval sol -- (![1.664863, 0.031932], 1.159033)
 
 end FittingSphere
 

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)