Realization on the unit interval

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

theorem GrothendieckBessel.realization_on_unit_interval (X : Type u_1) [MeasurableSpace X] [StandardBorelSpace X] (_nonemptyX : Nonempty X) (μ : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] : ∃ (f : ↑_root_.unitInterval → X), Measurable f ∧ MeasureTheory.Measure.map f MeasureTheory.volume = μ

Standard Borel realization of a probability measure by a map from Mathlib's canonical measured unit interval.

noncomputable def GrothendieckBessel.unitIntervalRealizedCoordinate {J : Type u_1} (g : ↑_root_.unitInterval → ClosedComplexUnitDiskProduct J) (j : J) : ℝ → ℂ

Extend one coordinate of a disk-product random variable on Mathlib's canonical unit interval to an ambient representative on ℝ.

Equations

• GrothendieckBessel.unitIntervalRealizedCoordinate g j = Function.extend Subtype.val (fun (x : ↑unitInterval) => ↑(g x j)) fun (x : ℝ) => 0

theorem GrothendieckBessel.unitIntervalRealizedCoordinate_apply {J : Type u_1} (g : ↑_root_.unitInterval → ClosedComplexUnitDiskProduct J) (j : J) (x : ↑_root_.unitInterval) : unitIntervalRealizedCoordinate g j ↑x = ↑(g x j)

theorem GrothendieckBessel.unitIntervalRealizedCoordinate_aestronglyMeasurable {J : Type u_1} {g : ↑_root_.unitInterval → ClosedComplexUnitDiskProduct J} (hg_meas : Measurable g) (j : J) : MeasureTheory.AEStronglyMeasurable (unitIntervalRealizedCoordinate g j) (μOn unitInterval)

theorem GrothendieckBessel.unitIntervalRealizedCoordinate_bound {J : Type u_1} (g : ↑_root_.unitInterval → ClosedComplexUnitDiskProduct J) (j : J) {t : ℝ} (ht : t ∈ unitInterval) : ‖unitIntervalRealizedCoordinate g j t‖ ≤ 1

theorem GrothendieckBessel.unitIntervalRealizedCoordinate_moment {J : Type u_1} [Countable J] {ν : MeasureTheory.ProbabilityMeasure (ClosedComplexUnitDiskProduct J)} {g : ↑_root_.unitInterval → ClosedComplexUnitDiskProduct J} (hg_meas : Measurable g) (hg_map : MeasureTheory.Measure.map g MeasureTheory.volume = ↑ν) (j k : J) : l2InnerOn unitInterval (unitIntervalRealizedCoordinate g j) (unitIntervalRealizedCoordinate g k) = ∫ (x : ClosedComplexUnitDiskProduct J), (diskMomentBCF j k) x ∂↑ν

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

Countable bounded realization of a positive-contraction moment family on the unit interval.