Finite complex Olevskii realization

This connects the finite quadratic-form condition to the real and complex convex decompositions and their bounded measurable step-function realization. Adapted for Lean Pool from the Apache-2.0 upstream formalization, with module-system, Mathlib API, and compilation changes.

theorem GrothendieckBessel.FiniteHermitianPositiveContraction.toComplexLoewner {F : Type u_1} [Fintype F] [DecidableEq F] {h : Matrix F F ℂ} (hh : FiniteHermitianPositiveContraction h) : OlevskiiGram.ComplexLoewnerBetweenZeroAndOne h

The finite-sum positive-contraction condition implies matrix Loewner bounds.

theorem GrothendieckBessel.finite_complex_olevskii_gram_realization {F : Type u_1} [Finite F] (h : Matrix F F ℂ) (hh : FiniteHermitianPositiveContraction h) : ∃ (a : F → ℝ → ℂ), (∀ (j : F), MeasureTheory.AEStronglyMeasurable (a j) (μOn unitInterval)) ∧ (∀ (j : F), ∀ t ∈ unitInterval, ‖a j t‖ ≤ 1) ∧ ∀ (j k : F), l2InnerOn unitInterval (a j) (a k) = h j k

Finite complex Olevskii Gram realization on [0,1], proved from the finite convex-decomposition development rather than assumed as an axiom.