Documentation

Mathlib.MeasureTheory.Measure.FiniteMeasureProd

Products of finite measures and probability measures #

This file introduces binary 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 #

TODO #

The binary product of finite measures.

Equations
  • μ.prod ν = (↑μ).prod ν,
Instances For
    @[simp]
    theorem MeasureTheory.FiniteMeasure.toMeasure_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) :
    (μ.prod ν) = (↑μ).prod ν
    theorem MeasureTheory.FiniteMeasure.prod_apply {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) (s : Set (α × β)) (s_mble : MeasurableSet s) :
    (μ.prod ν) s = (∫⁻ (x : α), ν (Prod.mk x ⁻¹' s)μ).toNNReal
    theorem MeasureTheory.FiniteMeasure.prod_apply_symm {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) (s : Set (α × β)) (s_mble : MeasurableSet s) :
    (μ.prod ν) s = (∫⁻ (y : β), μ ((fun (x : α) => (x, y)) ⁻¹' s)ν).toNNReal
    theorem MeasureTheory.FiniteMeasure.prod_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) (s : Set α) (t : Set β) :
    (μ.prod ν) (s ×ˢ t) = μ s * ν t
    @[simp]
    theorem MeasureTheory.FiniteMeasure.mass_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) :
    (μ.prod ν).mass = μ.mass * ν.mass
    @[simp]
    theorem MeasureTheory.FiniteMeasure.prod_zero {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) :
    μ.prod 0 = 0
    @[simp]
    theorem MeasureTheory.FiniteMeasure.map_fst_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) :
    (μ.prod ν).map Prod.fst = ν Set.univ μ
    @[simp]
    theorem MeasureTheory.FiniteMeasure.map_snd_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) :
    (μ.prod ν).map Prod.snd = μ Set.univ ν
    theorem MeasureTheory.FiniteMeasure.map_prod_map {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) {α' : Type u_3} [MeasurableSpace α'] {β' : Type u_4} [MeasurableSpace β'] {f : αα'} {g : ββ'} (f_mble : Measurable f) (g_mble : Measurable g) :
    (μ.map f).prod (ν.map g) = (μ.prod ν).map (Prod.map f g)
    theorem MeasureTheory.FiniteMeasure.prod_swap {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) :
    (μ.prod ν).map Prod.swap = ν.prod μ

    The binary product of probability measures.

    Equations
    • μ.prod ν = (↑μ).prod ν,
    Instances For
      @[simp]
      theorem MeasureTheory.ProbabilityMeasure.toMeasure_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) :
      (μ.prod ν) = (↑μ).prod ν
      theorem MeasureTheory.ProbabilityMeasure.prod_apply {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) (s : Set (α × β)) (s_mble : MeasurableSet s) :
      (μ.prod ν) s = (∫⁻ (x : α), ν (Prod.mk x ⁻¹' s)μ).toNNReal
      theorem MeasureTheory.ProbabilityMeasure.prod_apply_symm {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) (s : Set (α × β)) (s_mble : MeasurableSet s) :
      (μ.prod ν) s = (∫⁻ (y : β), μ ((fun (x : α) => (x, y)) ⁻¹' s)ν).toNNReal
      theorem MeasureTheory.ProbabilityMeasure.prod_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) (s : Set α) (t : Set β) :
      (μ.prod ν) (s ×ˢ t) = μ s * ν t
      @[simp]

      The first marginal of a product probability measure is the first probability measure.

      @[simp]

      The second marginal of a product probability measure is the second probability measure.

      theorem MeasureTheory.ProbabilityMeasure.map_prod_map {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) {α' : Type u_3} [MeasurableSpace α'] {β' : Type u_4} [MeasurableSpace β'] {f : αα'} {g : ββ'} (f_mble : Measurable f) (g_mble : Measurable g) :
      (μ.map ).prod (ν.map ) = (μ.prod ν).map