Documentation

QuasiBorelSpaces.ProbabilityMeasure.Basic

Probability Measures on Quasi-Borel Spaces #

This file defines probability measures for quasi-Borel spaces. Unlike [HKSY17] (Section V), we define probability measures simply as morphisms I →𝒒 A, quotiented to be equal whenever their push-forwards on the Lebesgue measure are equal.

source
@[instance_reducible]
def QuasiBorelSpace.ProbabilityMeasure.setoid (A : Type u_1) [QuasiBorelSpace A] :
Setoid (↑unitInterval →𝒒 A)
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    structure QuasiBorelSpace.ProbabilityMeasure (A : Type u) [QuasiBorelSpace A] :
    Type u
    Instances For

      Constructors #

      source
      noncomputable def QuasiBorelSpace.ProbabilityMeasure.mk {A : Type u_1} {x✝ : QuasiBorelSpace A} (Ο† : ↑unitInterval →𝒒 A) :
      ProbabilityMeasure A
      Equations
      Instances For
        source
        noncomputable def QuasiBorelSpace.ProbabilityMeasure.withBase {A : Type u_1} {x✝ : QuasiBorelSpace A} (base : MeasureTheory.ProbabilityMeasure ℝ) (eval : ℝ →𝒒 A) :
        ProbabilityMeasure A

        Create a ProbabilityMeasure relative to some base distribution on ℝ. This is the interface given in [HKSY17].

        Equations
        Instances For

          Induction and Lifting #

          source
          theorem QuasiBorelSpace.ProbabilityMeasure.induction {A : Type u_1} {x✝ : QuasiBorelSpace A} {P : ProbabilityMeasure A β†’ Prop} (mk : βˆ€ (Ο† : ↑unitInterval →𝒒 A), P (mk Ο†)) (ΞΌ : ProbabilityMeasure A) :
          P ΞΌ
          source
          theorem QuasiBorelSpace.ProbabilityMeasure.nonempty {A : Type u_1} {x✝ : QuasiBorelSpace A} (μ : ProbabilityMeasure A) :
          Nonempty A
          source
          def QuasiBorelSpace.ProbabilityMeasure.lift {A : Type u_1} {B : Type u_2} {x✝ : QuasiBorelSpace A} (f : (↑unitInterval →𝒒 A) β†’ B) (hf : βˆ€ (g₁ gβ‚‚ : ↑unitInterval →𝒒 A), g₁ β‰ˆ gβ‚‚ β†’ f g₁ = f gβ‚‚) (ΞΌ : ProbabilityMeasure A) :
          B
          Equations
          Instances For
            source
            @[simp]
            theorem QuasiBorelSpace.ProbabilityMeasure.lift_mk {A : Type u_2} {x✝ : QuasiBorelSpace A} {α✝ : Type u_1} {f : (↑unitInterval →𝒒 A) β†’ α✝} (hf : βˆ€ (g₁ gβ‚‚ : ↑unitInterval →𝒒 A), g₁ β‰ˆ gβ‚‚ β†’ f g₁ = f gβ‚‚) (Ο† : ↑unitInterval →𝒒 A) :
            lift f hf (mk Ο†) = f Ο†

            Integrals #

            source
            noncomputable def QuasiBorelSpace.ProbabilityMeasure.lintegral {A : Type u_1} [QuasiBorelSpace A] (f : A β†’ ENNReal) (ΞΌ : ProbabilityMeasure A) :
            ENNReal
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_mk {A : Type u_1} {x✝ : QuasiBorelSpace A} {f : A β†’ ENNReal} (hf : IsHom f) (Ο† : ↑unitInterval →𝒒 A) :
              lintegral f (mk Ο†) = ∫⁻ (x : ↑unitInterval), f (Ο† x)
              source
              @[simp]
              theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_withBase {A : Type u_1} {x✝ : QuasiBorelSpace A} {f : A β†’ ENNReal} (hf : IsHom f) (base : MeasureTheory.ProbabilityMeasure ℝ) (eval : ℝ →𝒒 A) :
              lintegral f (withBase base eval) = ∫⁻ (x : ℝ), f (eval x) βˆ‚β†‘base
              source
              theorem QuasiBorelSpace.ProbabilityMeasure.ext {A : Type u_1} {x✝ : QuasiBorelSpace A} {μ₁ ΞΌβ‚‚ : ProbabilityMeasure A} (h : βˆ€ (k : A β†’ ENNReal), IsHom k β†’ lintegral k μ₁ = lintegral k ΞΌβ‚‚) :
              μ₁ = ΞΌβ‚‚
              source
              theorem QuasiBorelSpace.ProbabilityMeasure.ext_iff {A : Type u_1} {x✝ : QuasiBorelSpace A} {μ₁ ΞΌβ‚‚ : ProbabilityMeasure A} :
              μ₁ = ΞΌβ‚‚ ↔ βˆ€ (k : A β†’ ENNReal), IsHom k β†’ lintegral k μ₁ = lintegral k ΞΌβ‚‚
              source
              @[simp]
              theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_add {A : Type u_1} {x✝ : QuasiBorelSpace A} {f g : A β†’ ENNReal} (hf : IsHom f) (hg : IsHom g) (ΞΌ : ProbabilityMeasure A) :
              lintegral (fun (x : A) => f x + g x) ΞΌ = lintegral f ΞΌ + lintegral g ΞΌ
              source
              @[simp]
              theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_mul {A : Type u_1} {x✝ : QuasiBorelSpace A} {f : A β†’ ENNReal} {a : ENNReal} (hf : IsHom f) (ΞΌ : ProbabilityMeasure A) :
              lintegral (fun (x : A) => a * f x) ΞΌ = a * lintegral f ΞΌ
              source
              theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_mono {A : Type u_1} {x✝ : QuasiBorelSpace A} {f g : A β†’ ENNReal} (hf : IsHom f) (hg : IsHom g) (hfg : βˆ€ (x : A), f x ≀ g x) (ΞΌ : ProbabilityMeasure A) :
              lintegral f ΞΌ ≀ lintegral g ΞΌ
              source
              theorem QuasiBorelSpace.ProbabilityMeasure.lintegral_swap {A : Type u_2} {B : Type u_1} {x✝ : QuasiBorelSpace A} {x✝¹ : QuasiBorelSpace B} {f : A β†’ B β†’ ENNReal} (hf : IsHom fun (x : A Γ— B) => f x.1 x.2) (ΞΌ : ProbabilityMeasure A) (Ξ½ : ProbabilityMeasure B) :
              lintegral (fun (x : A) => lintegral (f x) Ξ½) ΞΌ = lintegral (fun (x : B) => lintegral (fun (x_1 : A) => f x_1 x) ΞΌ) Ξ½

              QuasiBorelSpace Instance #

              source
              @[instance_reducible]
              def QuasiBorelSpace.ProbabilityMeasure.instβ‚€ {A : Type u_1} {x✝ : QuasiBorelSpace A} :
              QuasiBorelSpace (ProbabilityMeasure A)
              Equations
              Instances For
                source
                @[instance_reducible]
                instance QuasiBorelSpace.ProbabilityMeasure.inst {A : Type u_1} {x✝ : QuasiBorelSpace A} :
                QuasiBorelSpace (ProbabilityMeasure A)
                Equations
                source
                theorem QuasiBorelSpace.ProbabilityMeasure.isHom_mk {A : Type u_1} {x✝ : QuasiBorelSpace A} :
                IsHom mk
                source
                theorem QuasiBorelSpace.ProbabilityMeasure.induction_on_hom {A : Type u_1} {B : Type u_2} {x✝ : QuasiBorelSpace A} {x✝¹ : QuasiBorelSpace B} {P : (A →𝒒 ProbabilityMeasure B) β†’ Prop} [MeasurableSpace A] [MeasurableQuasiBorelSpace A] [StandardBorelSpace A] (mk : βˆ€ (Ο† : A →𝒒 ↑unitInterval →𝒒 B), P { toFun := mk ∘ ⇑φ, property := β‹― }) (f : A →𝒒 ProbabilityMeasure B) :
                P f
                source
                theorem QuasiBorelSpace.ProbabilityMeasure.isHom_lift {A : Type u_2} {B : Type u_1} {C : Type u_3} {x✝ : QuasiBorelSpace A} {x✝¹ : QuasiBorelSpace B} {x✝² : QuasiBorelSpace C} (f : A β†’ (↑unitInterval →𝒒 B) β†’ C) (hf₁ : IsHom fun (x : A Γ— (↑unitInterval →𝒒 B)) => f x.1 x.2) (hfβ‚‚ : βˆ€ (x : A) (g₁ gβ‚‚ : ↑unitInterval →𝒒 B), g₁ β‰ˆ gβ‚‚ β†’ f x g₁ = f x gβ‚‚) (g : A β†’ ProbabilityMeasure B) (hg : IsHom g) :
                IsHom fun (x : A) => lift (f x) β‹― (g x)
                source
                theorem QuasiBorelSpace.ProbabilityMeasure.isHom_lintegral {A : Type u_2} {B : Type u_1} {x✝ : QuasiBorelSpace A} {x✝¹ : QuasiBorelSpace B} {k : A β†’ B β†’ ENNReal} (hk : IsHom fun (x : A Γ— B) => match x with | (x, y) => k x y) {f : A β†’ ProbabilityMeasure B} (hf : IsHom f) :
                IsHom fun (x : A) => lintegral (k x) (f x)

                Lifting Morphisms #

                source
                noncomputable def QuasiBorelSpace.ProbabilityMeasure.liftHom {A : Type u_1} {B : Type u_2} {C : Type u_3} {x✝ : QuasiBorelSpace A} {x✝¹ : QuasiBorelSpace B} [MeasurableSpace A] [MeasurableQuasiBorelSpace A] [StandardBorelSpace A] (k : (A →𝒒 ↑unitInterval →𝒒 B) β†’ C) (hk : βˆ€ (g₁ gβ‚‚ : A →𝒒 ↑unitInterval →𝒒 B), g₁ β‰ˆ gβ‚‚ β†’ k g₁ = k gβ‚‚) (f : A →𝒒 ProbabilityMeasure B) :
                C
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem QuasiBorelSpace.ProbabilityMeasure.isHom_liftHom {A : Type u_1} {B : Type u_2} {C : Type u_3} {x✝ : QuasiBorelSpace A} {x✝¹ : QuasiBorelSpace B} {x✝² : QuasiBorelSpace C} [Nonempty A] [MeasurableSpace A] [MeasurableQuasiBorelSpace A] [StandardBorelSpace A] (k : (A →𝒒 ↑unitInterval →𝒒 B) β†’ C) (hk₁ : IsHom k) (hkβ‚‚ : βˆ€ (g₁ gβ‚‚ : A →𝒒 ↑unitInterval →𝒒 B), g₁ β‰ˆ gβ‚‚ β†’ k g₁ = k gβ‚‚) :
                  IsHom (liftHom k hkβ‚‚)
                  source
                  @[simp]
                  theorem QuasiBorelSpace.ProbabilityMeasure.liftHom_mk {A : Type u_2} {B : Type u_3} {x✝ : QuasiBorelSpace A} {x✝¹ : QuasiBorelSpace B} {C : Type u_1} [Nonempty A] [MeasurableSpace A] [MeasurableQuasiBorelSpace A] [StandardBorelSpace A] (k : (A →𝒒 ↑unitInterval →𝒒 B) β†’ C) (hk : βˆ€ (g₁ gβ‚‚ : A →𝒒 ↑unitInterval →𝒒 B), g₁ β‰ˆ gβ‚‚ β†’ k g₁ = k gβ‚‚) (f : A →𝒒 ↑unitInterval →𝒒 B) :
                  liftHom k hk { toFun := mk ∘ ⇑f, property := β‹― } = k f