Löwner ellipsoid contact-point theorem in Lean: check containment pointwise, no inner separation

For the outer (Löwner) characterization (K ⊆ B minimal ⇒ (I/d, 0) ∈ conv{(u⊗u, u) : u ∈ K ∩ sphere}), first separate with geometric_hahn_banach_closed_point. The hull is closed because isCompact_convexHull of the compact image of K ∩ sphere (hK.inter_right isClosed_sphere) is closed. This yields a trace-free G and a vector a with q(x) = ⟪Gx,x⟫ + ⟪a,x⟫ ≤ -η on K ∩ sphere. Then show directly that x ↦ (1+cδ)(x + δ(Gx + a)) maps K into the unit ball. Split on q x ≤ -η/2 and expand ‖x + δ(Gx+a)‖² = ‖x‖² + 2δ q(x) + δ²‖Gx+a‖². Otherwise, {x ∈ K | q x ≥ -η/2} is compact and misses the sphere, so IsCompact.exists_isMaxOn on ‖·‖ gives radius 1-γ. Unlike the inner (John) case, you never need a second Hahn–Banach for containment. The converse is easy with squares: ∑cᵢ‖Nuᵢ - b‖² ≤ d expands to tr(N*N) + d‖b‖² ≤ d once ∑cᵢuᵢ = 0. To get N itself (not just N*) isometric in the equality case, pass to the first moment, via 2∑cᵢtᵢ ≤ ∑cᵢtᵢ² + ∑cᵢ. Gotcha: Set.Finite.isCompact_convexHull needs (𝕜 := ℝ) explicitly or it fails with 'Field 𝕜'.