Theorems · Theorem · measure theory

Measure.eq_prod_of_integral_prod_mul_prod_boundedContinuousFunction

∀ {ι : Type u_1} {κ : Type u_2} {X : ι → Type u_5} {Y : κ → Type u_6} {mX : (i : ι) → MeasurableSpace (X i)}
  [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), HasOuterApproxClosed (X i)]
  {mY : (j : κ) → MeasurableSpace (Y j)} [inst_3 : (j : κ) → TopologicalSpace (Y j)] [∀ (j : κ), BorelSpace (Y j)]
  [∀ (j : κ), HasOuterApproxClosed (Y j)] [inst_6 : Fintype ι] [inst_7 : Fintype κ]
  {μ : MeasureTheory.Measure ((i : ι) → X i)} {ν : MeasureTheory.Measure ((j : κ) → Y j)}
  {ξ : MeasureTheory.Measure (((i : ι) → X i) × ((j : κ) → Y j))} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ξ],
  (∀ (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) ∂ν).

Defined in

Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd

Cited by

1 results in Mathlib

Foundations

Depth 267 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceBorelSpaceHasOuterApproxClosedTopologicalSpaceBorelSpaceHasOuterApproxClosedFintypeFintypeMeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure