Bounded step-function realizations of finite Gram matrices

Adapted for Lean Pool from the Apache-2.0 upstream formalization, with module-system, Mathlib API, and compilation changes.

theorem OlevskiiGram.stepFunctionRealization {n : Type u_1} {m : ℕ} (p : Fin m → ℝ) (ζ : Fin m → n → ℂ) : (∀ (r : Fin m), 0 ≤ p r) → ∑ r : Fin m, p r = 1 → (∀ (r : Fin m) (j : n), ‖ζ r j‖ ≤ 1) → ∃ (f : n → ℝ → ℂ), (∀ (j : n), LInfNormLe 1 (f j)) ∧ ∀ (j k : n), ∫ (t : ℝ) in Set.Ioo 0 1, f j t * star (f k t) = ∑ r : Fin m, ↑(p r) * ζ r j * star (ζ r k)

Realize a finite weighted complex Gram decomposition by piecewise constant functions on (0,1).

theorem OlevskiiGram.stepFunctionRealizationOnUnitInterval {n : Type u_1} {m : ℕ} (p : Fin m → ℝ) (ζ : Fin m → n → ℂ) : (∀ (r : Fin m), 0 ≤ p r) → ∑ r : Fin m, p r = 1 → (∀ (r : Fin m) (j : n), ‖ζ r j‖ ≤ 1) → ∃ (f : n → ℝ → ℂ), (∀ (j : n), MeasureTheory.AEStronglyMeasurable (f j) (MeasureTheory.volume.restrict (Set.Icc 0 1))) ∧ (∀ (j : n) (t : ℝ), ‖f j t‖ ≤ 1) ∧ ∀ (j k : n), ∫ (t : ℝ) in Set.Icc 0 1, f j t * star (f k t) = ∑ r : Fin m, ↑(p r) * ζ r j * star (ζ r k)

The same finite realization with the concrete measurability and everywhere pointwise bound needed by the countable compactness construction. The moment identity is written on [0,1]; changing the endpoints does not change a Lebesgue integral.