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

Given two finite families of Borel spaces (i : ι) → X i and (j : κ) → Y j satisfying HasOuterApproxClosed, a finite measure μ over (Π i, X i) × (Π j, Y j) is determined by the values ∫ p, (Π i, f i (p.1 i)) * (Π j, g j (p.2 j)) ∂μ, for f : (i : ι) → X i → ℝ and g : (j : κ) → Y j → ℝ any families of bounded continuous functions.

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

We specialize these results to the cases where one of the families contains only one type.

Main statements

• ext_of_integral_prod_mul_prod_boundedContinuousFunction: A finite measure μ over (Π i, X i) × (Π j, Y j) is determined by the values ∫ p, (Π i, f i (p.1 i)) * (Π j, g j (p.2 j)) ∂μ, for f : (i : ι) → X i → ℝ and g : (j : κ) → Y j → ℝ any families of bounded continuous functions.

  This is stronger than ext_of_integral_mul_boundedContinuousFunction because we do not require Π i, X i and Π j, Y j to be Borel spaces and only consider products of continuous bounded functions rather than general continuous bounded functions (Π i, X i) → ℝ and (Π j, Y j) → ℝ.

• eq_prod_of_integral_prod_mul_prod_boundedContinuousFunction: The product of two finite measures μ and ν is the only finite measure ξ over (Π i, X i) × (Π j, Y j) such that for all families of real bounded continuous functions f and g we have ∫ p, (Π i, f i (p.1 i)) * (Π j, g j (p.2 j)) ∂ξ = (∫ x, Π i, f i (x i) ∂μ) * (∫ y, Π j, g j (y j) ∂ν).

• ext_of_integral_mul_boundedContinuousFunction: A finite measure μ over X × Y is determined by the values ∫ p, f p.1 * g p.2 ∂μ, for f : X → ℝ and g : Y → ℝ any 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_prod_mul_prod_boundedContinuousFunction {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {X : ι → Type u_5} {Y : κ → Type u_6} {mX : (i : ι) → MeasurableSpace (X i)} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), HasOuterApproxClosed (X i)] {mY : (j : κ) → MeasurableSpace (Y j)} [(j : κ) → TopologicalSpace (Y j)] [∀ (j : κ), BorelSpace (Y j)] [∀ (j : κ), HasOuterApproxClosed (Y j)] {μ ν : MeasureTheory.Measure (((i : ι) → X i) × ((j : κ) → Y j))} [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (f : (i : ι) → BoundedContinuousFunction (X i) NNReal) (g : (j : κ) → BoundedContinuousFunction (Y j) NNReal), ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i : ι, (f i) (p.1 i)) * ↑(∏ j : κ, (g j) (p.2 j)) ∂μ = ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i : ι, (f i) (p.1 i)) * ↑(∏ j : κ, (g j) (p.2 j)) ∂ν) : μ = ν

A finite measure μ over (Π i, X i) × (Π j, Y j) is determined by the values ∫⁻ p, (Π i, f i (p.1 i)) * (Π j, g j (p.2 j)) ∂μ, for f : (i : ι) → X i → ℝ≥0 and g : (j : κ) → Y j → ℝ≥0 any families of bounded continuous functions.

theorem Measure.ext_of_integral_prod_mul_prod_boundedContinuousFunction {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {X : ι → Type u_5} {Y : κ → Type u_6} {mX : (i : ι) → MeasurableSpace (X i)} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), HasOuterApproxClosed (X i)] {mY : (j : κ) → MeasurableSpace (Y j)} [(j : κ) → TopologicalSpace (Y j)] [∀ (j : κ), BorelSpace (Y j)] [∀ (j : κ), HasOuterApproxClosed (Y j)] {μ ν : MeasureTheory.Measure (((i : ι) → X i) × ((j : κ) → Y j))} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : ∀ (f : (i : ι) → BoundedContinuousFunction (X i) ℝ) (g : (j : κ) → BoundedContinuousFunction (Y j) ℝ), ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), (∏ i : ι, (f i) (p.1 i)) * ∏ j : κ, (g j) (p.2 j) ∂μ = ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), (∏ i : ι, (f i) (p.1 i)) * ∏ j : κ, (g j) (p.2 j) ∂ν) : μ = ν

A finite measure μ over (Π i, X i) × (Π j, Y j) is determined by the values ∫ p, (Π i, f i (p.1 i)) * (Π j, g j (p.2 j)) ∂μ, for f : (i : ι) → X i → ℝ and g : (j : κ) → Y j → ℝ any families of bounded continuous functions.

theorem Measure.ext_of_integral_prod_mul_prod_boundedContinuousFunction' {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {X : ι → Type u_5} {Y : κ → Type u_6} {mX : (i : ι) → MeasurableSpace (X i)} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), HasOuterApproxClosed (X i)] {mY : (j : κ) → MeasurableSpace (Y j)} [(j : κ) → TopologicalSpace (Y j)] [∀ (j : κ), BorelSpace (Y j)] [∀ (j : κ), HasOuterApproxClosed (Y j)] {μ ν : MeasureTheory.Measure (((i : ι) → X i) × ((j : κ) → Y j))} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : ∀ (f : BoundedContinuousFunction ((i : ι) → X i) ℝ) (g : BoundedContinuousFunction ((j : κ) → Y j) ℝ), ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), f p.1 * g p.2 ∂μ = ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), f p.1 * g p.2 ∂ν) : μ = ν

theorem Measure.eq_prod_of_integral_prod_mul_prod_boundedContinuousFunction {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {X : ι → Type u_5} {Y : κ → Type u_6} {mX : (i : ι) → MeasurableSpace (X i)} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), HasOuterApproxClosed (X i)] {mY : (j : κ) → MeasurableSpace (Y j)} [(j : κ) → TopologicalSpace (Y j)] [∀ (j : κ), BorelSpace (Y j)] [∀ (j : κ), HasOuterApproxClosed (Y j)] {μ : MeasureTheory.Measure ((i : ι) → X i)} {ν : MeasureTheory.Measure ((j : κ) → Y j)} {ξ : MeasureTheory.Measure (((i : ι) → X i) × ((j : κ) → Y j))} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ξ] (h : ∀ (f : (i : ι) → BoundedContinuousFunction (X i) ℝ) (g : (j : κ) → BoundedContinuousFunction (Y j) ℝ), ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), (∏ i : ι, (f i) (p.1 i)) * ∏ j : κ, (g j) (p.2 j) ∂ξ = (∫ (x : (i : ι) → X i), ∏ i : ι, (f i) (x i) ∂μ) * ∫ (y : (j : κ) → Y j), ∏ j : κ, (g j) (y j) ∂ν) : ξ = μ.prod ν

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

theorem Measure.eq_prod_of_integral_prod_mul_prod_boundedContinuousFunction' {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {X : ι → Type u_5} {Y : κ → Type u_6} {mX : (i : ι) → MeasurableSpace (X i)} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), HasOuterApproxClosed (X i)] {mY : (j : κ) → MeasurableSpace (Y j)} [(j : κ) → TopologicalSpace (Y j)] [∀ (j : κ), BorelSpace (Y j)] [∀ (j : κ), HasOuterApproxClosed (Y j)] {μ : MeasureTheory.Measure ((i : ι) → X i)} {ν : MeasureTheory.Measure ((j : κ) → Y j)} {ξ : MeasureTheory.Measure (((i : ι) → X i) × ((j : κ) → Y j))} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ξ] (h : ∀ (f : BoundedContinuousFunction ((i : ι) → X i) ℝ) (g : BoundedContinuousFunction ((j : κ) → Y j) ℝ), ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), f p.1 * g p.2 ∂ξ = (∫ (x : (i : ι) → X i), f x ∂μ) * ∫ (y : (j : κ) → Y j), g y ∂ν) : ξ = μ.prod ν

theorem Measure.ext_of_integral_prod_mul_boundedContinuousFunction {ι : Type u_1} {T : Type u_4} [Fintype ι] {X : ι → Type u_5} {mX : (i : ι) → MeasurableSpace (X i)} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), HasOuterApproxClosed (X i)] {mT : MeasurableSpace T} [TopologicalSpace T] [BorelSpace T] [HasOuterApproxClosed T] {μ ν : MeasureTheory.Measure (((i : ι) → X i) × T)} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : ∀ (f : (i : ι) → BoundedContinuousFunction (X i) ℝ) (g : BoundedContinuousFunction T ℝ), ∫ (p : ((i : ι) → X i) × T), (∏ i : ι, (f i) (p.1 i)) * g p.2 ∂μ = ∫ (p : ((i : ι) → X i) × T), (∏ i : ι, (f i) (p.1 i)) * g p.2 ∂ν) : μ = ν

theorem Measure.ext_of_integral_prod_mul_boundedContinuousFunction' {ι : Type u_1} {T : Type u_4} [Fintype ι] {X : ι → Type u_5} {mX : (i : ι) → MeasurableSpace (X i)} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), HasOuterApproxClosed (X i)] {mT : MeasurableSpace T} [TopologicalSpace T] [BorelSpace T] [HasOuterApproxClosed T] {μ ν : MeasureTheory.Measure (((i : ι) → X i) × T)} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : ∀ (f : BoundedContinuousFunction ((i : ι) → X i) ℝ) (g : BoundedContinuousFunction T ℝ), ∫ (p : ((i : ι) → X i) × T), f p.1 * g p.2 ∂μ = ∫ (p : ((i : ι) → X i) × T), f p.1 * g p.2 ∂ν) : μ = ν

theorem Measure.eq_prod_of_integral_prod_mul_boundedContinuousFunction {ι : Type u_1} {T : Type u_4} [Fintype ι] {X : ι → Type u_5} {mX : (i : ι) → MeasurableSpace (X i)} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), HasOuterApproxClosed (X i)] {mT : MeasurableSpace T} [TopologicalSpace T] [BorelSpace T] [HasOuterApproxClosed T] {μ : MeasureTheory.Measure ((i : ι) → X i)} {ν : MeasureTheory.Measure T} {ξ : MeasureTheory.Measure (((i : ι) → X i) × T)} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ξ] (h : ∀ (f : (i : ι) → BoundedContinuousFunction (X i) ℝ) (g : BoundedContinuousFunction T ℝ), ∫ (p : ((i : ι) → X i) × T), (∏ i : ι, (f i) (p.1 i)) * g p.2 ∂ξ = (∫ (x : (i : ι) → X i), ∏ i : ι, (f i) (x i) ∂μ) * ∫ (t : T), g t ∂ν) : ξ = μ.prod ν

theorem Measure.eq_prod_of_integral_prod_mul_boundedContinuousFunction' {ι : Type u_1} {T : Type u_4} [Fintype ι] {X : ι → Type u_5} {mX : (i : ι) → MeasurableSpace (X i)} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), HasOuterApproxClosed (X i)] {mT : MeasurableSpace T} [TopologicalSpace T] [BorelSpace T] [HasOuterApproxClosed T] {μ : MeasureTheory.Measure ((i : ι) → X i)} {ν : MeasureTheory.Measure T} {ξ : MeasureTheory.Measure (((i : ι) → X i) × T)} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ξ] (h : ∀ (f : BoundedContinuousFunction ((i : ι) → X i) ℝ) (g : BoundedContinuousFunction T ℝ), ∫ (p : ((i : ι) → X i) × T), f p.1 * g p.2 ∂ξ = (∫ (x : (i : ι) → X i), f x ∂μ) * ∫ (t : T), g t ∂ν) : ξ = μ.prod ν

theorem Measure.ext_of_integral_mul_prod_boundedContinuousFunction {κ : Type u_2} {Z : Type u_3} [Fintype κ] {Y : κ → Type u_6} {mY : (j : κ) → MeasurableSpace (Y j)} [(j : κ) → TopologicalSpace (Y j)] [∀ (j : κ), BorelSpace (Y j)] [∀ (j : κ), HasOuterApproxClosed (Y j)] {mZ : MeasurableSpace Z} [TopologicalSpace Z] [BorelSpace Z] [HasOuterApproxClosed Z] {μ ν : MeasureTheory.Measure (Z × ((j : κ) → Y j))} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : ∀ (f : BoundedContinuousFunction Z ℝ) (g : (j : κ) → BoundedContinuousFunction (Y j) ℝ), ∫ (p : Z × ((j : κ) → Y j)), f p.1 * ∏ j : κ, (g j) (p.2 j) ∂μ = ∫ (p : Z × ((j : κ) → Y j)), f p.1 * ∏ j : κ, (g j) (p.2 j) ∂ν) : μ = ν

theorem Measure.ext_of_integral_mul_prod_boundedContinuousFunction' {κ : Type u_2} {Z : Type u_3} [Fintype κ] {Y : κ → Type u_6} {mY : (j : κ) → MeasurableSpace (Y j)} [(j : κ) → TopologicalSpace (Y j)] [∀ (j : κ), BorelSpace (Y j)] [∀ (j : κ), HasOuterApproxClosed (Y j)] {mZ : MeasurableSpace Z} [TopologicalSpace Z] [BorelSpace Z] [HasOuterApproxClosed Z] {μ ν : MeasureTheory.Measure (Z × ((i : κ) → Y i))} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : ∀ (f : BoundedContinuousFunction Z ℝ) (g : BoundedContinuousFunction ((j : κ) → Y j) ℝ), ∫ (p : Z × ((i : κ) → Y i)), f p.1 * g p.2 ∂μ = ∫ (p : Z × ((i : κ) → Y i)), f p.1 * g p.2 ∂ν) : μ = ν

theorem Measure.eq_prod_of_integral_mul_prod_boundedContinuousFunction {κ : Type u_2} {Z : Type u_3} [Fintype κ] {Y : κ → Type u_6} {mY : (j : κ) → MeasurableSpace (Y j)} [(j : κ) → TopologicalSpace (Y j)] [∀ (j : κ), BorelSpace (Y j)] [∀ (j : κ), HasOuterApproxClosed (Y j)] {mZ : MeasurableSpace Z} [TopologicalSpace Z] [BorelSpace Z] [HasOuterApproxClosed Z] {μ : MeasureTheory.Measure Z} {ν : MeasureTheory.Measure ((j : κ) → Y j)} {ξ : MeasureTheory.Measure (Z × ((j : κ) → Y j))} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ξ] (h : ∀ (f : BoundedContinuousFunction Z ℝ) (g : (j : κ) → BoundedContinuousFunction (Y j) ℝ), ∫ (p : Z × ((j : κ) → Y j)), f p.1 * ∏ j : κ, (g j) (p.2 j) ∂ξ = (∫ (z : Z), f z ∂μ) * ∫ (y : (j : κ) → Y j), ∏ j : κ, (g j) (y j) ∂ν) : ξ = μ.prod ν

theorem Measure.eq_prod_of_integral_mul_prod_boundedContinuousFunction' {κ : Type u_2} {Z : Type u_3} [Fintype κ] {Y : κ → Type u_6} {mY : (j : κ) → MeasurableSpace (Y j)} [(j : κ) → TopologicalSpace (Y j)] [∀ (j : κ), BorelSpace (Y j)] [∀ (j : κ), HasOuterApproxClosed (Y j)] {mZ : MeasurableSpace Z} [TopologicalSpace Z] [BorelSpace Z] [HasOuterApproxClosed Z] {μ : MeasureTheory.Measure Z} {ν : MeasureTheory.Measure ((j : κ) → Y j)} {ξ : MeasureTheory.Measure (Z × ((j : κ) → Y j))} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ξ] (h : ∀ (f : BoundedContinuousFunction Z ℝ) (g : BoundedContinuousFunction ((j : κ) → Y j) ℝ), ∫ (p : Z × ((j : κ) → Y j)), f p.1 * g p.2 ∂ξ = (∫ (z : Z), f z ∂μ) * ∫ (y : (j : κ) → Y j), g y ∂ν) : ξ = μ.prod ν

theorem Measure.ext_of_integral_mul_boundedContinuousFunction {Z : Type u_3} {T : Type u_4} {mZ : MeasurableSpace Z} [TopologicalSpace Z] [BorelSpace Z] [HasOuterApproxClosed Z] {mT : MeasurableSpace T} [TopologicalSpace T] [BorelSpace T] [HasOuterApproxClosed T] {μ ν : MeasureTheory.Measure (Z × T)} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : ∀ (f : BoundedContinuousFunction Z ℝ) (g : BoundedContinuousFunction T ℝ), ∫ (p : Z × T), f p.1 * g p.2 ∂μ = ∫ (p : Z × T), f p.1 * g p.2 ∂ν) : μ = ν

A finite measure μ over X × Y is determined by the values ∫ p, f p.1 * g p.2 ∂μ, for f : X → ℝ and g : Y → ℝ any bounded continuous functions.

theorem Measure.eq_prod_of_integral_mul_boundedContinuousFunction {Z : Type u_3} {T : Type u_4} {mZ : MeasurableSpace Z} [TopologicalSpace Z] [BorelSpace Z] [HasOuterApproxClosed Z] {mT : MeasurableSpace T} [TopologicalSpace T] [BorelSpace T] [HasOuterApproxClosed T] {μ : MeasureTheory.Measure Z} {ν : MeasureTheory.Measure T} {ξ : MeasureTheory.Measure (Z × T)} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ξ] (h : ∀ (f : BoundedContinuousFunction Z ℝ) (g : BoundedContinuousFunction T ℝ), ∫ (p : Z × T), f p.1 * g p.2 ∂ξ = (∫ (z : Z), f z ∂μ) * ∫ (t : T), g t ∂ν) : ξ = μ.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 ∂ν.