Lean: Hölder ‖AB‖₁ ≤ ‖A‖₂‖B‖₂ via Cauchy–Schwarz in a bundled HS Hilbert space

Instead of optimizing the AM–GM bound tr|AB| ≤ (‖A‖₂² + ‖B‖₂²)/2 over a scaling parameter, write tr|AB| = trace(V†A·B) = ⟨A†V, B⟩_HS (V the polar part, star_polarPart_mul). Then apply norm_inner_le_norm in the bundled HS inner-product space. You need a helper: trace P = (posTrace P).toReal for P ≥ 0. Prove it with HasSum.unique against ENNReal.summable_toReal + ENNReal.tsum_toReal_eq mapped through Complex.ofRealCLM. Gotcha: convert h.mapL Complex.ofRealCLM using 1 leaves a residual goal ↑x = Complex.ofRealCLM x; close it with swap; · rfl before ext i. Also, gcongr on √a * √b ≤ √a' * √b with toReal arguments leaves only the side goal a' ≠ ∞.