Documentation

PFR.ForMathlib.FiniteMeasureProd

Products of finite measures and probability measures #

source
noncomputable def MeasureTheory.FiniteMeasure.prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) :
MeasureTheory.FiniteMeasure (α × β)

The binary product of finite measures.

Equations
  • μ.prod ν = ⟨(↑μ).prod ↑ν, ⋯⟩
Instances For
    source
    @[simp]
    theorem MeasureTheory.FiniteMeasure.toMeasure_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) :
    ↑(μ.prod ν) = (↑μ).prod ↑ν
    source
    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
    source
    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
    source
    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
    source
    theorem MeasureTheory.FiniteMeasure.mass_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) :
    (μ.prod ν).mass = μ.mass * ν.mass
    source
    theorem MeasureTheory.FiniteMeasure.zero_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (ν : MeasureTheory.FiniteMeasure β) :
    MeasureTheory.FiniteMeasure.prod 0 ν = 0
    source
    theorem MeasureTheory.FiniteMeasure.prod_zero {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) :
    μ.prod 0 = 0
    source
    @[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 • μ
    source
    @[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 • ν
    source
    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)
    source
    theorem MeasureTheory.FiniteMeasure.prod_apply_null {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) {s : Set (α × β)} (hs : MeasurableSet s) :
    (μ.prod ν) s = 0 ↔ (fun (x : α) => ν (Prod.mk x ⁻¹' s)) =ᵐ[↑μ] 0
    source
    theorem MeasureTheory.FiniteMeasure.measure_ae_null_of_prod_null {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) {s : Set (α × β)} (h : (μ.prod ν) s = 0) :
    (fun (x : α) => ν (Prod.mk x ⁻¹' s)) =ᵐ[↑μ] 0
    source
    theorem MeasureTheory.FiniteMeasure.prod_swap {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) :
    (μ.prod ν).map Prod.swap = ν.prod μ
    source
    noncomputable def MeasureTheory.ProbabilityMeasure.prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) :
    MeasureTheory.ProbabilityMeasure (α × β)

    The binary product of probability measures.

    Equations
    • μ.prod ν = ⟨(↑μ).prod ↑ν, ⋯⟩
    Instances For
      source
      @[simp]
      theorem MeasureTheory.ProbabilityMeasure.toMeasure_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) :
      ↑(μ.prod ν) = (↑μ).prod ↑ν
      source
      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
      source
      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
      source
      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
      source
      @[simp]
      theorem MeasureTheory.ProbabilityMeasure.map_fst_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) :
      (μ.prod ν).map ⋯ = μ
      source
      @[simp]
      theorem MeasureTheory.ProbabilityMeasure.map_snd_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) :
      (μ.prod ν).map ⋯ = ν
      source
      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 ⋯
      source
      theorem MeasureTheory.ProbabilityMeasure.prod_apply_null {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) {s : Set (α × β)} (hs : MeasurableSet s) :
      (μ.prod ν) s = 0 ↔ (fun (x : α) => ν (Prod.mk x ⁻¹' s)) =ᵐ[↑μ] 0
      source
      theorem MeasureTheory.ProbabilityMeasure.measure_ae_null_of_prod_null {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) {s : Set (α × β)} (h : (μ.prod ν) s = 0) :
      (fun (x : α) => ν (Prod.mk x ⁻¹' s)) =ᵐ[↑μ] 0
      source
      theorem MeasureTheory.ProbabilityMeasure.prod_swap {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) :
      (μ.prod ν).map ⋯ = ν.prod μ