Documentation

Mathlib.MeasureTheory.Measure.FiniteMeasurePi

Products of finite measures and probability measures #

This file introduces finite products of finite measures and probability measures. The constructions are obtained from special cases of products of general measures. Taking products nevertheless has specific properties in the cases of finite measures and probability measures, notably the fact that the product measures depend continuously on their factors in the topology of weak convergence when the underlying space is metrizable and separable.

Main definitions #

Main results #

MeasureTheory.ProbabilityMeasure.continuous_pi: the product probability measure depends continuously on the factors.

source
noncomputable def MeasureTheory.FiniteMeasure.pi {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → FiniteMeasure (α i)) :
FiniteMeasure ((i : ι) → α i)

The product of finitely many finite measures.

Equations
Instances For
    source
    @[simp]
    theorem MeasureTheory.FiniteMeasure.toMeasure_pi {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → FiniteMeasure (α i)) :
    ↑(pi μ) = Measure.pi fun (i : ι) => ↑(μ i)
    source
    @[simp]
    theorem MeasureTheory.FiniteMeasure.pi_pi {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → FiniteMeasure (α i)) (s : (i : ι) → Set (α i)) :
    (pi μ) (Set.univ.pi s) = ∏ i : ι, (μ i) (s i)
    source
    @[simp]
    theorem MeasureTheory.FiniteMeasure.mass_pi {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → FiniteMeasure (α i)) :
    (pi μ).mass = ∏ i : ι, (μ i).mass
    source
    theorem MeasureTheory.FiniteMeasure.pi_map_pi {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → FiniteMeasure (α i)) {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] {f : (i : ι) → α i → β i} (f_mble : ∀ (i : ι), AEMeasurable (f i) ↑(μ i)) :
    ((pi μ).map fun (x : (i : ι) → α i) (i : ι) => f i (x i)) = pi fun (i : ι) => (μ i).map (f i)
    source
    noncomputable def MeasureTheory.ProbabilityMeasure.pi {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → ProbabilityMeasure (α i)) :
    ProbabilityMeasure ((i : ι) → α i)

    The product of finitely many probability measures.

    Equations
    Instances For
      source
      @[simp]
      theorem MeasureTheory.ProbabilityMeasure.toMeasure_pi {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → ProbabilityMeasure (α i)) :
      ↑(pi μ) = Measure.pi fun (i : ι) => ↑(μ i)
      source
      @[simp]
      theorem MeasureTheory.ProbabilityMeasure.pi_pi {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → ProbabilityMeasure (α i)) (s : (i : ι) → Set (α i)) :
      (pi μ) (Set.univ.pi s) = ∏ i : ι, (μ i) (s i)
      source
      theorem MeasureTheory.ProbabilityMeasure.continuous_pi {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), SecondCountableTopology (α i)] [∀ (i : ι), TopologicalSpace.PseudoMetrizableSpace (α i)] [∀ (i : ι), OpensMeasurableSpace (α i)] :
      Continuous fun (μ : (i : ι) → ProbabilityMeasure (α i)) => pi μ

      The map associating to finitely many probability measures their product is a continuous map.