Documentation

Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Borel (measurable) spaces ℝ, ℝ≥0, ℝ≥0∞ #

Main statements #

theorem Real.borel_eq_generateFrom_Ioo_rat :
borel = MeasurableSpace.generateFrom (⋃ (a : ), ⋃ (b : ), ⋃ (_ : a < b), {Set.Ioo a b})
theorem Real.isPiSystem_Ioo_rat :
IsPiSystem (⋃ (a : ), ⋃ (b : ), ⋃ (_ : a < b), {Set.Ioo a b})
def Real.finiteSpanningSetsInIooRat (μ : MeasureTheory.Measure ) [MeasureTheory.IsLocallyFiniteMeasure μ] :
μ.FiniteSpanningSetsIn (⋃ (a : ), ⋃ (b : ), ⋃ (_ : a < b), {Set.Ioo a b})

The intervals (-(n + 1), (n + 1)) form a finite spanning sets in the set of open intervals with rational endpoints for a locally finite measure μ on .

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem Real.measure_ext_Ioo_rat {μ : MeasureTheory.Measure } {ν : MeasureTheory.Measure } [MeasureTheory.IsLocallyFiniteMeasure μ] (h : ∀ (a b : ), μ (Set.Ioo a b) = ν (Set.Ioo a b)) :
    μ = ν
    theorem Measurable.real_toNNReal {α : Type u_1} [MeasurableSpace α] {f : α} (hf : Measurable f) :
    Measurable fun (x : α) => (f x).toNNReal
    theorem AEMeasurable.real_toNNReal {α : Type u_1} [MeasurableSpace α] {f : α} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) :
    AEMeasurable (fun (x : α) => (f x).toNNReal) μ
    theorem Measurable.coe_nnreal_real {α : Type u_1} [MeasurableSpace α] {f : αNNReal} (hf : Measurable f) :
    Measurable fun (x : α) => (f x)
    theorem AEMeasurable.coe_nnreal_real {α : Type u_1} [MeasurableSpace α] {f : αNNReal} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) :
    AEMeasurable (fun (x : α) => (f x)) μ
    theorem Measurable.coe_nnreal_ennreal {α : Type u_1} [MeasurableSpace α] {f : αNNReal} (hf : Measurable f) :
    Measurable fun (x : α) => (f x)
    theorem AEMeasurable.coe_nnreal_ennreal {α : Type u_1} [MeasurableSpace α] {f : αNNReal} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) :
    AEMeasurable (fun (x : α) => (f x)) μ
    theorem Measurable.ennreal_ofReal {α : Type u_1} [MeasurableSpace α] {f : α} (hf : Measurable f) :
    Measurable fun (x : α) => ENNReal.ofReal (f x)
    theorem AEMeasurable.ennreal_ofReal {α : Type u_1} [MeasurableSpace α] {f : α} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) :
    AEMeasurable (fun (x : α) => ENNReal.ofReal (f x)) μ
    @[simp]
    theorem measurable_coe_nnreal_real_iff {α : Type u_1} [MeasurableSpace α] {f : αNNReal} :
    (Measurable fun (x : α) => (f x)) Measurable f
    @[simp]
    theorem aemeasurable_coe_nnreal_real_iff {α : Type u_1} [MeasurableSpace α] {f : αNNReal} {μ : MeasureTheory.Measure α} :
    AEMeasurable (fun (x : α) => (f x)) μ AEMeasurable f μ
    @[deprecated aemeasurable_coe_nnreal_real_iff]
    theorem aEMeasurable_coe_nnreal_real_iff {α : Type u_1} [MeasurableSpace α] {f : αNNReal} {μ : MeasureTheory.Measure α} :
    AEMeasurable (fun (x : α) => (f x)) μ AEMeasurable f μ

    Alias of aemeasurable_coe_nnreal_real_iff.

    The set of finite ℝ≥0∞ numbers is MeasurableEquiv to ℝ≥0.

    Equations
    Instances For
      theorem ENNReal.measurable_of_measurable_nnreal {α : Type u_1} [MeasurableSpace α] {f : ENNRealα} (h : Measurable fun (p : NNReal) => f p) :
      theorem ENNReal.measurable_of_measurable_nnreal_prod {β : Type u_2} {γ : Type u_3} [MeasurableSpace β] [MeasurableSpace γ] {f : ENNReal × βγ} (H₁ : Measurable fun (p : NNReal × β) => f (p.1, p.2)) (H₂ : Measurable fun (x : β) => f (, x)) :
      theorem ENNReal.measurable_of_measurable_nnreal_nnreal {β : Type u_2} [MeasurableSpace β] {f : ENNReal × ENNRealβ} (h₁ : Measurable fun (p : NNReal × NNReal) => f (p.1, p.2)) (h₂ : Measurable fun (r : NNReal) => f (, r)) (h₃ : Measurable fun (r : NNReal) => f (r, )) :
      theorem ENNReal.measurable_of_tendsto' {α : Type u_1} [MeasurableSpace α] {ι : Type u_5} {f : ιαENNReal} {g : αENNReal} (u : Filter ι) [u.NeBot] [u.IsCountablyGenerated] (hf : ∀ (i : ι), Measurable (f i)) (lim : Filter.Tendsto f u (nhds g)) :

      A limit (over a general filter) of measurable ℝ≥0∞ valued functions is measurable.

      @[deprecated ENNReal.measurable_of_tendsto']
      theorem measurable_of_tendsto_ennreal' {α : Type u_1} [MeasurableSpace α] {ι : Type u_5} {f : ιαENNReal} {g : αENNReal} (u : Filter ι) [u.NeBot] [u.IsCountablyGenerated] (hf : ∀ (i : ι), Measurable (f i)) (lim : Filter.Tendsto f u (nhds g)) :

      Alias of ENNReal.measurable_of_tendsto'.


      A limit (over a general filter) of measurable ℝ≥0∞ valued functions is measurable.

      theorem ENNReal.measurable_of_tendsto {α : Type u_1} [MeasurableSpace α] {f : αENNReal} {g : αENNReal} (hf : ∀ (i : ), Measurable (f i)) (lim : Filter.Tendsto f Filter.atTop (nhds g)) :

      A sequential limit of measurable ℝ≥0∞ valued functions is measurable.

      @[deprecated ENNReal.measurable_of_tendsto]
      theorem measurable_of_tendsto_ennreal {α : Type u_1} [MeasurableSpace α] {f : αENNReal} {g : αENNReal} (hf : ∀ (i : ), Measurable (f i)) (lim : Filter.Tendsto f Filter.atTop (nhds g)) :

      Alias of ENNReal.measurable_of_tendsto.


      A sequential limit of measurable ℝ≥0∞ valued functions is measurable.

      theorem ENNReal.aemeasurable_of_tendsto' {α : Type u_1} [MeasurableSpace α] {ι : Type u_5} {f : ιαENNReal} {g : αENNReal} {μ : MeasureTheory.Measure α} (u : Filter ι) [u.NeBot] [u.IsCountablyGenerated] (hf : ∀ (i : ι), AEMeasurable (f i) μ) (hlim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (i : ι) => f i a) u (nhds (g a))) :

      A limit (over a general filter) of a.e.-measurable ℝ≥0∞ valued functions is a.e.-measurable.

      theorem ENNReal.aemeasurable_of_tendsto {α : Type u_1} [MeasurableSpace α] {f : αENNReal} {g : αENNReal} {μ : MeasureTheory.Measure α} (hf : ∀ (i : ), AEMeasurable (f i) μ) (hlim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (i : ) => f i a) Filter.atTop (nhds (g a))) :

      A limit of a.e.-measurable ℝ≥0∞ valued functions is a.e.-measurable.

      theorem Measurable.ennreal_toNNReal {α : Type u_1} [MeasurableSpace α] {f : αENNReal} (hf : Measurable f) :
      Measurable fun (x : α) => (f x).toNNReal
      theorem AEMeasurable.ennreal_toNNReal {α : Type u_1} [MeasurableSpace α] {f : αENNReal} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) :
      AEMeasurable (fun (x : α) => (f x).toNNReal) μ
      @[simp]
      theorem measurable_coe_nnreal_ennreal_iff {α : Type u_1} [MeasurableSpace α] {f : αNNReal} :
      (Measurable fun (x : α) => (f x)) Measurable f
      @[simp]
      theorem aemeasurable_coe_nnreal_ennreal_iff {α : Type u_1} [MeasurableSpace α] {f : αNNReal} {μ : MeasureTheory.Measure α} :
      AEMeasurable (fun (x : α) => (f x)) μ AEMeasurable f μ
      theorem Measurable.ennreal_toReal {α : Type u_1} [MeasurableSpace α] {f : αENNReal} (hf : Measurable f) :
      Measurable fun (x : α) => (f x).toReal
      theorem AEMeasurable.ennreal_toReal {α : Type u_1} [MeasurableSpace α] {f : αENNReal} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) :
      AEMeasurable (fun (x : α) => (f x).toReal) μ
      theorem Measurable.ennreal_tsum {α : Type u_1} [MeasurableSpace α] {ι : Type u_5} [Countable ι] {f : ιαENNReal} (h : ∀ (i : ι), Measurable (f i)) :
      Measurable fun (x : α) => ∑' (i : ι), f i x

      note: ℝ≥0∞ can probably be generalized in a future version of this lemma.

      theorem Measurable.ennreal_tsum' {α : Type u_1} [MeasurableSpace α] {ι : Type u_5} [Countable ι] {f : ιαENNReal} (h : ∀ (i : ι), Measurable (f i)) :
      Measurable (∑' (i : ι), f i)
      theorem Measurable.nnreal_tsum {α : Type u_1} [MeasurableSpace α] {ι : Type u_5} [Countable ι] {f : ιαNNReal} (h : ∀ (i : ι), Measurable (f i)) :
      Measurable fun (x : α) => ∑' (i : ι), f i x
      theorem AEMeasurable.ennreal_tsum {α : Type u_1} [MeasurableSpace α] {ι : Type u_5} [Countable ι] {f : ιαENNReal} {μ : MeasureTheory.Measure α} (h : ∀ (i : ι), AEMeasurable (f i) μ) :
      AEMeasurable (fun (x : α) => ∑' (i : ι), f i x) μ
      theorem AEMeasurable.nnreal_tsum {α : Type u_5} [MeasurableSpace α] {ι : Type u_6} [Countable ι] {f : ιαNNReal} {μ : MeasureTheory.Measure α} (h : ∀ (i : ι), AEMeasurable (f i) μ) :
      AEMeasurable (fun (x : α) => ∑' (i : ι), f i x) μ
      theorem Measurable.coe_real_ereal {α : Type u_1} [MeasurableSpace α] {f : α} (hf : Measurable f) :
      Measurable fun (x : α) => (f x)
      theorem AEMeasurable.coe_real_ereal {α : Type u_1} [MeasurableSpace α] {f : α} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) :
      AEMeasurable (fun (x : α) => (f x)) μ

      The set of finite EReal numbers is MeasurableEquiv to .

      Equations
      Instances For
        theorem EReal.measurable_of_measurable_real {α : Type u_1} [MeasurableSpace α] {f : ERealα} (h : Measurable fun (p : ) => f p) :
        theorem Measurable.ereal_toReal {α : Type u_1} [MeasurableSpace α] {f : αEReal} (hf : Measurable f) :
        Measurable fun (x : α) => (f x).toReal
        theorem AEMeasurable.ereal_toReal {α : Type u_1} [MeasurableSpace α] {f : αEReal} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) :
        AEMeasurable (fun (x : α) => (f x).toReal) μ
        theorem Measurable.coe_ereal_ennreal {α : Type u_1} [MeasurableSpace α] {f : αENNReal} (hf : Measurable f) :
        Measurable fun (x : α) => (f x)
        theorem AEMeasurable.coe_ereal_ennreal {α : Type u_1} [MeasurableSpace α] {f : αENNReal} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) :
        AEMeasurable (fun (x : α) => (f x)) μ
        theorem NNReal.measurable_of_tendsto' {α : Type u_1} [MeasurableSpace α] {ι : Type u_5} {f : ιαNNReal} {g : αNNReal} (u : Filter ι) [u.NeBot] [u.IsCountablyGenerated] (hf : ∀ (i : ι), Measurable (f i)) (lim : Filter.Tendsto f u (nhds g)) :

        A limit (over a general filter) of measurable ℝ≥0 valued functions is measurable.

        @[deprecated NNReal.measurable_of_tendsto']
        theorem measurable_of_tendsto_nnreal' {α : Type u_1} [MeasurableSpace α] {ι : Type u_5} {f : ιαNNReal} {g : αNNReal} (u : Filter ι) [u.NeBot] [u.IsCountablyGenerated] (hf : ∀ (i : ι), Measurable (f i)) (lim : Filter.Tendsto f u (nhds g)) :

        Alias of NNReal.measurable_of_tendsto'.


        A limit (over a general filter) of measurable ℝ≥0 valued functions is measurable.

        theorem NNReal.measurable_of_tendsto {α : Type u_1} [MeasurableSpace α] {f : αNNReal} {g : αNNReal} (hf : ∀ (i : ), Measurable (f i)) (lim : Filter.Tendsto f Filter.atTop (nhds g)) :

        A sequential limit of measurable ℝ≥0 valued functions is measurable.

        @[deprecated NNReal.measurable_of_tendsto]
        theorem measurable_of_tendsto_nnreal {α : Type u_1} [MeasurableSpace α] {f : αNNReal} {g : αNNReal} (hf : ∀ (i : ), Measurable (f i)) (lim : Filter.Tendsto f Filter.atTop (nhds g)) :

        Alias of NNReal.measurable_of_tendsto.


        A sequential limit of measurable ℝ≥0 valued functions is measurable.

        theorem exists_spanning_measurableSet_le {α : Type u_5} {m : MeasurableSpace α} {f : αNNReal} (hf : Measurable f) (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] :
        ∃ (s : Set α), (∀ (n : ), MeasurableSet (s n) μ (s n) < xs n, f x n) ⋃ (i : ), s i = Set.univ

        If a function f : α → ℝ≥0 is measurable and the measure is σ-finite, then there exists spanning measurable sets with finite measure on which f is bounded. See also StronglyMeasurable.exists_spanning_measurableSet_norm_le for functions into normed groups.