Auxiliary lemmas for John's ellipsoid theorem

General-purpose results needed by the proof of the John decomposition of identity (BasicResults/John.lean), none of which are specific to convex bodies. Each is a candidate for upstreaming to Mathlib:

• Real.exp_sub_two_mul_sq_le and one_sub_two_mul_sum_sq_le_prod_one_add — a quantitative Weierstrass-type product bound: if ∑ aᵢ = 0 and |aᵢ| ≤ 1/2, then ∏ (1 + aᵢ) ≥ 1 - 2 ∑ aᵢ². This is why a trace-zero perturbation 1 + tH of the identity loses determinant only to second order in t.
• IsCompact.convexHull — in a finite-dimensional real normed space, the convex hull of a compact set is compact. Mathlib's TotallyBounded.convexHull yields total boundedness of the hull, hence compactness only of its closure; the work here is that in finite dimension the hull is already closed.
• Seminorm.exists_inner_le_of_apply — the supporting-vector form of Hahn–Banach dominated by a seminorm on an inner product space over RCLike 𝕜: every point admits a supporting functional x ↦ re ⟪x, v⟫ of the seminorm attaining its value at the point. The extension itself is Mathlib's Module.Dual.exists_extension_of_le_seminorm; what is added is the representing vector v.
• ContinuousLinearMap.exists_trace_repr — trace duality: every linear functional on the endomorphisms of a finite-dimensional inner product space is A ↦ tr (A ∘ G) for some endomorphism G.

A quantitative Weierstrass product inequality

theorem Real.exp_sub_two_mul_sq_le {a : ℝ} (ha : -(1 / 2) ≤ a) : exp (a - 2 * a ^ 2) ≤ 1 + a

Pointwise exponential bound: exp (a - 2a²) ≤ 1 + a for a ≥ -1/2.

This is the elementary inequality behind the second-order determinant bound: it follows from 1 + x ≤ exp x applied to x = 2a² - a, since (1 + 2a² - a) * (1 + a) = 1 + a² (1 + 2a) ≥ 1 when 1 + 2a ≥ 0.

theorem one_sub_two_mul_sum_sq_le_prod_one_add {ι : Type u_1} (s : Finset ι) (a : ι → ℝ) (ha : ∀ i ∈ s, |a i| ≤ 1 / 2) (hsum : ∑ i ∈ s, a i = 0) : 1 - 2 * ∑ i ∈ s, a i ^ 2 ≤ ∏ i ∈ s, (1 + a i)

Weierstrass-type product lower bound. If ∑ aᵢ = 0 and every |aᵢ| ≤ 1/2, then ∏ (1 + aᵢ) ≥ 1 - 2 ∑ aᵢ².

Mathematically: a multiplicative perturbation with vanishing first-order term loses volume only to second order. Proof: ∏ (1 + aᵢ) ≥ ∏ exp (aᵢ - 2aᵢ²) = exp (∑ aᵢ - 2 ∑ aᵢ²) = exp (-2 ∑ aᵢ²) ≥ 1 - 2 ∑ aᵢ², using Real.exp_sub_two_mul_sq_le and Real.add_one_le_exp.

The convex hull of a compact set is compact (finite dimensions)

theorem IsCompact.convexHull {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} (hs : IsCompact s) : IsCompact ((_root_.convexHull ℝ) s)

The convex hull of a compact set is compact, in a finite-dimensional real normed space. Mathlib has the finite-set case (Set.Finite.isCompact_convexHull) and TotallyBounded.convexHull, which gives total boundedness of the hull and so compactness only of its closure; the point here is that in finite dimension the hull is already closed.

By Carathéodory's theorem every point of the hull is a convex combination of at most finrank ℝ E + 1 affinely independent points of s, so the hull is the image of the compact set stdSimplex × s^(finrank+1) under the continuous map (w, z) ↦ ∑ᵢ wᵢ • zᵢ.

Hahn–Banach dominated by a seminorm, inner-product form

theorem Seminorm.exists_inner_le_of_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (q : Seminorm 𝕜 E) (u : E) : ∃ (v : E), (∀ (x : E), RCLike.re (inner 𝕜 x v) ≤ q x) ∧ RCLike.re (inner 𝕜 u v) = q u

Hahn–Banach dominated by a seminorm, inner-product form. For every continuous seminorm q on a finite-dimensional inner product space over RCLike 𝕜 and every point u, there is a vector v whose associated real functional x ↦ re ⟪x, v⟫ is dominated by q everywhere and attains the value q u at u.

Mathematically: the convex body {q ≤ 1} has a supporting hyperplane at each boundary point. On the 𝕜-span of u the functional c • u ↦ c · q u satisfies ‖f z‖ = q z outright, so Mathlib's seminorm Hahn–Banach (Module.Dual.exists_extension_of_le_seminorm) extends it to all of E keeping that bound; the Riesz isomorphism (InnerProductSpace.toDual) then represents the extension by a vector.

Trace duality for endomorphisms of a finite-dimensional inner product space

theorem ContinuousLinearMap.trace_adjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [CompleteSpace E] (G : E →L[𝕜] E) : (LinearMap.trace 𝕜 E) ↑(adjoint G) = (starRingEnd 𝕜) ((LinearMap.trace 𝕜 E) ↑G)

The trace of the adjoint is the conjugate of the trace: tr G* = conj (tr G). (Compute both traces in an orthonormal basis.)

theorem ContinuousLinearMap.exists_trace_repr {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [CompleteSpace E] (f : (E →L[𝕜] E) →ₗ[𝕜] 𝕜) : ∃ (G : E →L[𝕜] E), ∀ (A : E →L[𝕜] E), f A = (LinearMap.trace 𝕜 E) (↑A ∘ₗ ↑G)

Trace duality. Every 𝕜-linear functional f on the continuous endomorphisms of a finite-dimensional inner product space is of the form A ↦ tr (A ∘ G) for some endomorphism G.

The pairing (G, A) ↦ tr (A ∘ G) is nondegenerate — testing against A = G* gives tr (G* ∘ G) = ∑ᵢ ‖G eᵢ‖² — so G ↦ tr (· ∘ G) is an injective linear map into the dual, hence surjective by equality of dimensions.