Characterization of a finite measure by the integrals of products of bounded functions

Given two Borel spaces X and Y satisfying HasOuterApproxClosed, a finite measure μ over X × Y is determined by the values ∫ z, f z.1 * g z.2 ∂μ, for f : X → ℝ and g : Y → ℝ any bounded continuous functions.

In particular, If μ and ν and two finite measures over X and Y respectively, then their product is the only finite measure ξ over X × Y such that for any two bounded continuous functions f : X → ℝ and g : Y → ℝ we have ∫ z, f z.1 * g z.2 ∂ξ = (∫ x, f x ∂μ) * (∫ y, g y ∂ν).

Main statements

• ext_of_integral_mul_boundedContinuousFunction: A finite measure on a product space is characterized by the integrals of products of real bounded continuous functions.
• eq_prod_of_integral_mul_boundedContinuousFunction: The product of two finite measures μ and ν is the only finite measure ξ such that for all real bounded continuous functions f and g we have ∫ z, f z.1 * g z.2 ∂ξ = ∫ x, f x ∂μ * ∫ y, g y ∂ν.

Tags

bounded continuous function, product measure

theorem Measure.ext_of_lintegral_mul_boundedContinuousFunction {X : Type u_1} {Y : Type u_2} {mX : MeasurableSpace X} [TopologicalSpace X] [BorelSpace X] [HasOuterApproxClosed X] {mY : MeasurableSpace Y} [TopologicalSpace Y] [BorelSpace Y] [HasOuterApproxClosed Y] {μ ν : MeasureTheory.Measure (X × Y)} [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (f : BoundedContinuousFunction X NNReal) (g : BoundedContinuousFunction Y NNReal), ∫⁻ (z : X × Y), ↑(f z.1) * ↑(g z.2) ∂μ = ∫⁻ (z : X × Y), ↑(f z.1) * ↑(g z.2) ∂ν) : μ = ν

A finite measure on a product space is characterized by the integrals of products of bounded nonnegative continuous functions.

theorem Measure.ext_of_integral_mul_boundedContinuousFunction {X : Type u_1} {Y : Type u_2} {mX : MeasurableSpace X} [TopologicalSpace X] [BorelSpace X] [HasOuterApproxClosed X] {mY : MeasurableSpace Y} [TopologicalSpace Y] [BorelSpace Y] [HasOuterApproxClosed Y] {μ ν : MeasureTheory.Measure (X × Y)} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : ∀ (f : BoundedContinuousFunction X ℝ) (g : BoundedContinuousFunction Y ℝ), ∫ (z : X × Y), f z.1 * g z.2 ∂μ = ∫ (z : X × Y), f z.1 * g z.2 ∂ν) : μ = ν

A finite measure on a product space is characterized by the integrals of products of real and bounded continuous functions.

theorem Measure.eq_prod_of_integral_mul_boundedContinuousFunction {X : Type u_1} {Y : Type u_2} {mX : MeasurableSpace X} [TopologicalSpace X] [BorelSpace X] [HasOuterApproxClosed X] {mY : MeasurableSpace Y} [TopologicalSpace Y] [BorelSpace Y] [HasOuterApproxClosed Y] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] {ν : MeasureTheory.Measure Y} [MeasureTheory.IsFiniteMeasure ν] {ξ : MeasureTheory.Measure (X × Y)} [MeasureTheory.IsFiniteMeasure ξ] (h : ∀ (f : BoundedContinuousFunction X ℝ) (g : BoundedContinuousFunction Y ℝ), ∫ (z : X × Y), f z.1 * g z.2 ∂ξ = (∫ (x : X), f x ∂μ) * ∫ (y : Y), g y ∂ν) : ξ = μ.prod ν

The product of two finite measures μ and ν is the only finite measure ξ such that for all real bounded continuous functions f and g we have ∫ z, f z.1 * g z.2 ∂ξ = ∫ x, f x ∂μ * ∫ y, g y ∂ν.