John's ellipsoid with a free center in Lean: first-moment estimate and separation in (E →L E) × E

Converse ('if') half: if c + A(B) ⊆ K and u is a contact point, then ⟪u,c⟫ + ‖A* u‖ ≤ 1. Weighting by cᵢ and using ∑cᵢuᵢ = 0 gives only ∑ cᵢ‖A* uᵢ‖ ≤ d, a first moment. The squared estimate ∑cᵢ‖A*uᵢ‖² ≤ d that suffices for centered ellipsoids now fails (you get d + ‖c‖²). Fix: let αⱼ = √μⱼ, where μⱼ are the eigenvalues of AA* (from IsSymmetric.eigenvectorBasis). For unit u the weights pⱼ = ⟪vⱼ,u⟫² sum to 1, and the variance identity ∑pⱼ(αⱼ - m)² = ‖A*u‖² - m², with m = ∑αⱼpⱼ, gives m ≤ ‖A*u‖ without Jensen or sqrt lemmas (by_contra + nlinarith). Then ∑αⱼ ≤ d and ∏αⱼ = |det A|, via sq_eq_sq₀ and Finset.prod_pow, so AM–GM finishes. The 'only if' half reuses the centered perturbation proof with geometric_hahn_banach_closed_point in the product space (E →L[ℝ] E) × E. Split φ into φ.comp (ContinuousLinearMap.inl ..) and the Riesz vector of φ.comp (inr ..), via InnerProductSpace.toDual.symm. Perturb the center by (1+cδ)δ•a as well as the shape. The new arithmetic is X ≤ 1 - δt - δη/4 from X² ≤ (that)², which needs one extra smallness condition δ(‖a‖+η) ≤ 1. Gotcha: with open Finset, sum_apply is ambiguous, so write _root_.sum_apply. ContinuousLinearMap.sum_apply/smul_apply/add_apply are deprecated in favour of the root names.