Theorems · Theorem · measure theory

Measure.eq_prod_of_integral_mul_boundedContinuousFunction

∀ {Z : Type u_3} {T : Type u_4} {mZ : MeasurableSpace Z} [inst : TopologicalSpace Z] [BorelSpace Z]
  [HasOuterApproxClosed Z] {mT : MeasurableSpace T} [inst_3 : TopologicalSpace T] [BorelSpace T]
  [HasOuterApproxClosed T] {μ : MeasureTheory.Measure Z} {ν : MeasureTheory.Measure T}
  {ξ : MeasureTheory.Measure (Z × T)} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν]
  [MeasureTheory.IsFiniteMeasure ξ],
  (∀ (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 ∂ν.

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

TopologicalSpaceBorelSpaceHasOuterApproxClosedTopologicalSpaceBorelSpaceHasOuterApproxClosedMeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure