Countable moment measures

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

@[reducible, inline]

abbrev GrothendieckBessel.ClosedComplexUnitDisk : Type

The closed unit disk in ℂ, as a compact measurable subtype.

Equations

• GrothendieckBessel.ClosedComplexUnitDisk = ↑(Metric.closedBall 0 1)

@[reducible, inline]

abbrev GrothendieckBessel.ClosedComplexUnitDiskProduct (J : Type u_1) : Type u_1

Countable products of the closed complex unit disk.

Equations

• GrothendieckBessel.ClosedComplexUnitDiskProduct J = (J → GrothendieckBessel.ClosedComplexUnitDisk)

instance GrothendieckBessel.closedComplexUnitDisk_compactSpace : CompactSpace ClosedComplexUnitDisk

instance GrothendieckBessel.closedComplexUnitDisk_standardBorelSpace : StandardBorelSpace ClosedComplexUnitDisk

instance GrothendieckBessel.closedComplexUnitDisk_nonempty : Nonempty ClosedComplexUnitDisk

theorem GrothendieckBessel.ClosedComplexUnitDisk.norm_coe_le_one (z : ClosedComplexUnitDisk) : ‖↑z‖ ≤ 1

Coercions from the closed unit disk have norm at most one.

def GrothendieckBessel.Complex.toClosedUnitDisk (z : ℂ) (hz : ‖z‖ ≤ 1) : ClosedComplexUnitDisk

Package a complex number whose norm is at most one as a point of the closed unit disk.

Equations

• GrothendieckBessel.Complex.toClosedUnitDisk z hz = ⟨z, ⋯⟩

def GrothendieckBessel.zeroClosedComplexUnitDisk : ClosedComplexUnitDisk

The zero point of the closed complex unit disk.

Equations

• GrothendieckBessel.zeroClosedComplexUnitDisk = GrothendieckBessel.Complex.toClosedUnitDisk 0 GrothendieckBessel.zeroClosedComplexUnitDisk._proof_1

theorem GrothendieckBessel.compact_standard_borel_product (J : Type u_1) [Countable J] : CompactSpace (ClosedComplexUnitDiskProduct J) ∧ StandardBorelSpace (ClosedComplexUnitDiskProduct J)

Compact standard Borel structure for the product closedDisk^J.

theorem GrothendieckBessel.probability_measures_compact (X : Type u_1) [TopologicalSpace X] [CompactSpace X] [MeasurableSpace X] [T2Space X] [BorelSpace X] : CompactSpace (MeasureTheory.ProbabilityMeasure X)

Compactness of probability measures on a compact metrizable space.

noncomputable def GrothendieckBessel.diskMomentBCF {J : Type u_1} (j k : J) : BoundedContinuousFunction (ClosedComplexUnitDiskProduct J) ℂ

The bounded continuous test function for the (j,k) moment.

Equations

• One or more equations did not get rendered due to their size.

theorem GrothendieckBessel.continuous_probability_integral_complex {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] (f : BoundedContinuousFunction X ℂ) : Continuous fun (μ : MeasureTheory.ProbabilityMeasure X) => ∫ (x : X), f x ∂↑μ

Complex-valued weak-continuity of integration of a bounded continuous test function.

theorem GrothendieckBessel.momentIntegral_continuous {J : Type u_1} [Countable J] (j k : J) : Continuous fun (μ : MeasureTheory.ProbabilityMeasure (ClosedComplexUnitDiskProduct J)) => ∫ (x : ClosedComplexUnitDiskProduct J), (diskMomentBCF j k) x ∂↑μ

The map sending a probability measure to its (j,k) moment is continuous.

def GrothendieckBessel.momentConstraint {J : Type u_1} (h : J → J → ℂ) (j k : J) : Set (MeasureTheory.ProbabilityMeasure (ClosedComplexUnitDiskProduct J))

The closed set of probability measures satisfying one prescribed moment.

Equations

• One or more equations did not get rendered due to their size.

theorem GrothendieckBessel.closed_moment_constraints {J : Type u_1} [Countable J] (h : J → J → ℂ) (j k : J) : IsClosed (momentConstraint h j k)

Closedness of one moment constraint.

theorem GrothendieckBessel.FiniteHermitianPositiveContraction.restrictSubtype {J : Type u_1} {h : J → J → ℂ} (hh : FiniteHermitianPositiveContraction h) (S : Finset J) : FiniteHermitianPositiveContraction fun (a b : ↥S) => h ↑a ↑b

Restriction of a positive-contraction kernel to a finite subtype. This is the adapter needed before applying the finite Olevskii realization to finitely many coordinates of a countable kernel.

def GrothendieckBessel.pairCoordinateFinset {J : Type u_1} [DecidableEq J] (S : Finset (J × J)) : Finset J

Coordinates appearing in a finite set of requested moment pairs.

Equations

• GrothendieckBessel.pairCoordinateFinset S = Finset.image Prod.fst S ∪ Finset.image Prod.snd S

theorem GrothendieckBessel.pairCoordinateFinset_fst_mem {J : Type u_1} [DecidableEq J] {S : Finset (J × J)} {p : J × J} (hp : p ∈ S) : p.1 ∈ pairCoordinateFinset S

theorem GrothendieckBessel.pairCoordinateFinset_snd_mem {J : Type u_1} [DecidableEq J] {S : Finset (J × J)} {p : J × J} (hp : p ∈ S) : p.2 ∈ pairCoordinateFinset S

theorem GrothendieckBessel.pairCoordinateFinset_nonempty_of_nonempty {J : Type u_1} [DecidableEq J] {S : Finset (J × J)} (hS : S.Nonempty) : (pairCoordinateFinset S).Nonempty

theorem GrothendieckBessel.μOn_unitInterval_isProbabilityMeasure : MeasureTheory.IsProbabilityMeasure (μOn unitInterval)

The restricted Lebesgue measure on the ambient [0,1] is a probability measure.

noncomputable def GrothendieckBessel.diskProductSample {J : Type u_1} [DecidableEq J] (T : Finset J) (a : ↥T → ℝ → ℂ) (ha_bound : ∀ (j : ↥T), ∀ t ∈ unitInterval, ‖a j t‖ ≤ 1) : ℝ → ClosedComplexUnitDiskProduct J

Build a disk-product sample from finitely many bounded coordinate functions.

Equations

• One or more equations did not get rendered due to their size.

theorem GrothendieckBessel.diskProductSample_of_mem {J : Type u_1} [DecidableEq J] {T : Finset J} {a : ↥T → ℝ → ℂ} {ha_bound : ∀ (j : ↥T), ∀ t ∈ unitInterval, ‖a j t‖ ≤ 1} {j : J} (hj : j ∈ T) {t : ℝ} (ht : t ∈ unitInterval) : ↑(diskProductSample T a ha_bound t j) = a ⟨j, hj⟩ t

theorem GrothendieckBessel.diskProductSample_aemeasurable {J : Type u_1} [Countable J] [DecidableEq J] {T : Finset J} {a : ↥T → ℝ → ℂ} {ha_bound : ∀ (j : ↥T), ∀ t ∈ unitInterval, ‖a j t‖ ≤ 1} (ha_meas : ∀ (j : ↥T), MeasureTheory.AEStronglyMeasurable (a j) (μOn unitInterval)) : AEMeasurable (diskProductSample T a ha_bound) (μOn unitInterval)

The finite disk-product sample map is measurable for the restricted unit-interval measure.

noncomputable def GrothendieckBessel.diskProductSampleMeasure {J : Type u_1} [Countable J] [DecidableEq J] (T : Finset J) (a : ↥T → ℝ → ℂ) (ha_bound : ∀ (j : ↥T), ∀ t ∈ unitInterval, ‖a j t‖ ≤ 1) (ha_meas : ∀ (j : ↥T), MeasureTheory.AEStronglyMeasurable (a j) (μOn unitInterval)) : MeasureTheory.ProbabilityMeasure (ClosedComplexUnitDiskProduct J)

Push the restricted unit-interval measure forward through a finite disk-product sample.

Equations

• One or more equations did not get rendered due to their size.

theorem GrothendieckBessel.diskProductSampleMeasure_moment_of_mem {J : Type u_1} [Countable J] [DecidableEq J] {T : Finset J} {a : ↥T → ℝ → ℂ} {ha_bound : ∀ (j : ↥T), ∀ t ∈ unitInterval, ‖a j t‖ ≤ 1} {ha_meas : ∀ (j : ↥T), MeasureTheory.AEStronglyMeasurable (a j) (μOn unitInterval)} {j k : J} (hj : j ∈ T) (hk : k ∈ T) : ∫ (x : ClosedComplexUnitDiskProduct J), (diskMomentBCF j k) x ∂↑(diskProductSampleMeasure T a ha_bound ha_meas) = l2InnerOn unitInterval (a ⟨j, hj⟩) (a ⟨k, hk⟩)

Moments of the finite disk-product sample agree with the original finite coordinate functions for coordinates in the finite coordinate set.

theorem GrothendieckBessel.finite_moment_constraints_nonempty {J : Type u_1} [Countable J] (h : J → J → ℂ) (hh : FiniteHermitianPositiveContraction h) (S : Finset (J × J)) : (⋂ p ∈ S, momentConstraint h p.1 p.2).Nonempty

Finite satisfiability of moment constraints, obtained by applying the finite Olevskii realization theorem to the coordinates appearing in the finite set of pairs and pushing the restricted unit-interval measure forward to the full disk product.

theorem GrothendieckBessel.moment_constraints_all_nonempty_of_finite {J : Type u_1} [Countable J] (h : J → J → ℂ) (hfinite : ∀ (S : Finset (J × J)), (⋂ p ∈ S, momentConstraint h p.1 p.2).Nonempty) : (⋂ (p : J × J), momentConstraint h p.1 p.2).Nonempty

Finite intersection property in the compact space of disk-product probability measures.

theorem GrothendieckBessel.countable_moment_measure_of_finite_satisfiable {J : Type u_1} [Countable J] (h : J → J → ℂ) (hfinite : ∀ (S : Finset (J × J)), (⋂ p ∈ S, momentConstraint h p.1 p.2).Nonempty) : ∃ (μ : MeasureTheory.ProbabilityMeasure (ClosedComplexUnitDiskProduct J)), ∀ (j k : J), ∫ (x : ClosedComplexUnitDiskProduct J), (diskMomentBCF j k) x ∂↑μ = h j k

If every finite family of moment constraints is satisfiable, then there is one probability measure satisfying all countably many constraints.

theorem GrothendieckBessel.finite_intersection_step {J : Type u_1} [Countable J] (h : J → J → ℂ) (hh : FiniteHermitianPositiveContraction h) (S : Finset (J × J)) : (⋂ p ∈ S, momentConstraint h p.1 p.2).Nonempty

Finite-intersection step for finitely many moment constraints.

theorem GrothendieckBessel.countable_moment_measure {J : Type u_1} [Countable J] (h : J → J → ℂ) (hh : FiniteHermitianPositiveContraction h) : ∃ (μ : MeasureTheory.ProbabilityMeasure (ClosedComplexUnitDiskProduct J)), ∀ (j k : J), ∫ (x : ClosedComplexUnitDiskProduct J), (diskMomentBCF j k) x ∂↑μ = h j k

Countable moment measure obtained from finite satisfiability and compactness.