Minimal-volume (Löwner) ellipsoid in Lean: parametrize by the inverse map for compactness

To get a minimal-volume centered ellipsoid containing compact K (0 ∈ interior K), don't minimize |det A| over {A : K ⊆ A(B)}. That set is unbounded, and coercivity needs singular values. Write the ellipsoid as {x | ‖M x‖ ≤ 1} and maximize |det M| over S = {M : E →L[ℝ] E | ∀ x ∈ K, ‖M x‖ ≤ 1}. S is closed (isClosed_biInter with (ContinuousLinearMap.apply ℝ E x).continuous.norm) and bounded: ball 0 r ⊆ K gives ‖M‖ ≤ 2/r via opNorm_le_bound applied to (r/2/‖x‖) • x. So IsCompact.exists_isMaxOn with continuous_det.abs works, and R⁻¹ • id ∈ S gives det ≠ 0. The √d bound then reuses John's numeric lemma verbatim, with T = 1/h², where h is the support value from geometric_hahn_banach_closed_point.