Documentation

Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Borel (measurable) space #

Main definitions #

Main statements #

MeasurableSpace structure generated by TopologicalSpace.

Equations
Instances For
    theorem borel_anti {α : Type u_1} :
    theorem isPiSystem_isOpen {α : Type u_1} [TopologicalSpace α] :
    IsPiSystem {s : Set α | IsOpen s}
    theorem borel_comap {α : Type u_1} {β : Type u_2} {f : αβ} {t : TopologicalSpace β} :
    theorem Continuous.borel_measurable {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (hf : Continuous f) :

    A space with MeasurableSpace and TopologicalSpace structures such that all open sets are measurable.

    • borel_le : borel α h

      Borel-measurable sets are measurable.

    Instances

      A space with MeasurableSpace and TopologicalSpace structures such that the σ-algebra of measurable sets is exactly the σ-algebra generated by open sets.

      • measurable_eq : inst✝ = borel α

        The measurable sets are exactly the Borel-measurable sets.

      Instances

        The behaviour of borelize α depends on the existing assumptions on α.

        Finally, borelize α β γ runs borelize α; borelize β; borelize γ.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Add instances borel e : MeasurableSpace e and ⟨rfl⟩ : BorelSpace e.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Given a type e, an assumption i : MeasurableSpace e, and an instance [BorelSpace e], replace i with borel e.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Given a type $t, if there is an assumption [i : MeasurableSpace $t], then try to prove [BorelSpace $t] and replace i with borel $t. Otherwise, add instances borel $t : MeasurableSpace $t and ⟨rfl⟩ : BorelSpace $t.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • =

                In a BorelSpace all open sets are measurable.

                Equations
                • =
                instance Subtype.borelSpace {α : Type u_6} [TopologicalSpace α] [MeasurableSpace α] [hα : BorelSpace α] (s : Set α) :
                Equations
                • =
                Equations
                • =
                theorem MeasurableSet.induction_on_open {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] {C : Set αProp} (h_open : ∀ (U : Set α), IsOpen UC U) (h_compl : ∀ (t : Set α), MeasurableSet tC tC t) (h_union : ∀ (f : Set α), Pairwise (Disjoint on f)(∀ (i : ), MeasurableSet (f i))(∀ (i : ), C (f i))C (⋃ (i : ), f i)) ⦃t : Set α :
                MeasurableSet tC t
                theorem measurableSet_of_continuousAt {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {β : Type u_6} [EMetricSpace β] (f : αβ) :
                theorem Inseparable.mem_measurableSet_iff {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] {x : γ} {y : γ} (h : Inseparable x y) {s : Set γ} (hs : MeasurableSet s) :
                x s y s

                If two points are topologically inseparable, then they can't be separated by a Borel measurable set.

                theorem IsCompact.closure_subset_measurableSet {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [R1Space γ] {K : Set γ} {s : Set γ} (hK : IsCompact K) (hs : MeasurableSet s) (hKs : K s) :

                If K is a compact set in an R₁ space and s ⊇ K is a Borel measurable superset, then s includes the closure of K as well.

                theorem IsCompact.measure_closure {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [R1Space γ] {K : Set γ} (hK : IsCompact K) (μ : MeasureTheory.Measure γ) :
                μ (closure K) = μ K

                In an R₁ topological space with Borel measure μ, the measure of the closure of a compact set K is equal to the measure of K.

                See also MeasureTheory.Measure.OuterRegular.measure_closure_eq_of_isCompact for a version that assumes μ to be outer regular but does not assume the σ-algebra to be Borel.

                theorem measurable_of_isOpen {γ : Type u_3} {δ : Type u_5} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [MeasurableSpace δ] {f : δγ} (hf : ∀ (s : Set γ), IsOpen sMeasurableSet (f ⁻¹' s)) :
                theorem measurable_of_isClosed {γ : Type u_3} {δ : Type u_5} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [MeasurableSpace δ] {f : δγ} (hf : ∀ (s : Set γ), IsClosed sMeasurableSet (f ⁻¹' s)) :
                theorem measurable_of_isClosed' {γ : Type u_3} {δ : Type u_5} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [MeasurableSpace δ] {f : δγ} (hf : ∀ (s : Set γ), IsClosed sSet.Nonempty ss Set.univMeasurableSet (f ⁻¹' s)) :

                If s is a measurable set, then 𝓝[s] a is a measurably generated filter for each a. This cannot be an instance because it depends on a non-instance hs : MeasurableSet s.

                instance Pi.opensMeasurableSpace {ι : Type u_6} {π : ιType u_7} [Countable ι] [t' : (i : ι) → TopologicalSpace (π i)] [(i : ι) → MeasurableSpace (π i)] [∀ (i : ι), SecondCountableTopology (π i)] [∀ (i : ι), OpensMeasurableSpace (π i)] :
                OpensMeasurableSpace ((i : ι) → π i)
                Equations
                • =

                The typeclass SecondCountableTopologyEither α β registers the fact that at least one of the two spaces has second countable topology. This is the right assumption to ensure that continuous maps from α to β are strongly measurable.

                Instances

                  If either α or β has second-countable topology, then the open sets in α × β belong to the product sigma-algebra.

                  Equations
                  • =
                  theorem measure_interior_of_null_frontier {α' : Type u_6} [TopologicalSpace α'] [MeasurableSpace α'] {μ : MeasureTheory.Measure α'} {s : Set α'} (h : μ (frontier s) = 0) :
                  μ (interior s) = μ s
                  theorem measure_closure_of_null_frontier {α' : Type u_6} [TopologicalSpace α'] [MeasurableSpace α'] {μ : MeasureTheory.Measure α'} {s : Set α'} (h : μ (frontier s) = 0) :
                  μ (closure s) = μ s
                  @[simp]
                  theorem measurableSet_le {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [PartialOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f : δα} {g : δα} (hf : Measurable f) (hg : Measurable g) :
                  MeasurableSet {a : δ | f a g a}
                  theorem measurableSet_lt {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f : δα} {g : δα} (hf : Measurable f) (hg : Measurable g) :
                  MeasurableSet {a : δ | f a < g a}
                  theorem nullMeasurableSet_lt {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {μ : MeasureTheory.Measure δ} {f : δα} {g : δα} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
                  MeasureTheory.NullMeasurableSet {a : δ | f a < g a} μ
                  theorem nullMeasurableSet_le {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {μ : MeasureTheory.Measure δ} {f : δα} {g : δα} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
                  MeasureTheory.NullMeasurableSet {a : δ | f a g a} μ
                  theorem generateFrom_Ico_mem_le_borel {α : Type u_7} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] (s : Set α) (t : Set α) :
                  MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l < u Set.Ico l u = S} borel α
                  theorem Dense.borel_eq_generateFrom_Ico_mem_aux {α : Type u_7} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {s : Set α} (hd : Dense s) (hbot : ∀ (x : α), IsBot xx s) (hIoo : ∀ (x y : α), x < ySet.Ioo x y = y s) :
                  borel α = MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u Set.Ico l u = S}
                  theorem Dense.borel_eq_generateFrom_Ico_mem {α : Type u_7} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [DenselyOrdered α] [NoMinOrder α] {s : Set α} (hd : Dense s) :
                  borel α = MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u Set.Ico l u = S}
                  theorem borel_eq_generateFrom_Ico (α : Type u_7) [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] :
                  borel α = MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l < u Set.Ico l u = S}
                  theorem Dense.borel_eq_generateFrom_Ioc_mem_aux {α : Type u_7} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {s : Set α} (hd : Dense s) (hbot : ∀ (x : α), IsTop xx s) (hIoo : ∀ (x y : α), x < ySet.Ioo x y = x s) :
                  borel α = MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u Set.Ioc l u = S}
                  theorem Dense.borel_eq_generateFrom_Ioc_mem {α : Type u_7} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [DenselyOrdered α] [NoMaxOrder α] {s : Set α} (hd : Dense s) :
                  borel α = MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u Set.Ioc l u = S}
                  theorem borel_eq_generateFrom_Ioc (α : Type u_7) [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] :
                  borel α = MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l < u Set.Ioc l u = S}
                  theorem MeasureTheory.Measure.ext_of_Ico_finite {α : Type u_7} [TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (hμν : μ Set.univ = ν Set.univ) (h : ∀ ⦃a b : α⦄, a < bμ (Set.Ico a b) = ν (Set.Ico a b)) :
                  μ = ν

                  Two finite measures on a Borel space are equal if they agree on all closed-open intervals. If α is a conditionally complete linear order with no top element, MeasureTheory.Measure.ext_of_Ico is an extensionality lemma with weaker assumptions on μ and ν.

                  theorem MeasureTheory.Measure.ext_of_Ioc_finite {α : Type u_7} [TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (hμν : μ Set.univ = ν Set.univ) (h : ∀ ⦃a b : α⦄, a < bμ (Set.Ioc a b) = ν (Set.Ioc a b)) :
                  μ = ν

                  Two finite measures on a Borel space are equal if they agree on all open-closed intervals. If α is a conditionally complete linear order with no top element, MeasureTheory.Measure.ext_of_Ioc is an extensionality lemma with weaker assumptions on μ and ν.

                  theorem MeasureTheory.Measure.ext_of_Ico' {α : Type u_7} [TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] [NoMaxOrder α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) (hμ : ∀ ⦃a b : α⦄, a < bμ (Set.Ico a b) ) (h : ∀ ⦃a b : α⦄, a < bμ (Set.Ico a b) = ν (Set.Ico a b)) :
                  μ = ν

                  Two measures which are finite on closed-open intervals are equal if they agree on all closed-open intervals.

                  theorem MeasureTheory.Measure.ext_of_Ioc' {α : Type u_7} [TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] [NoMinOrder α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) (hμ : ∀ ⦃a b : α⦄, a < bμ (Set.Ioc a b) ) (h : ∀ ⦃a b : α⦄, a < bμ (Set.Ioc a b) = ν (Set.Ioc a b)) :
                  μ = ν

                  Two measures which are finite on closed-open intervals are equal if they agree on all open-closed intervals.

                  theorem MeasureTheory.Measure.ext_of_Ico {α : Type u_7} [TopologicalSpace α] {_m : MeasurableSpace α} [SecondCountableTopology α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [BorelSpace α] [NoMaxOrder α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] (h : ∀ ⦃a b : α⦄, a < bμ (Set.Ico a b) = ν (Set.Ico a b)) :
                  μ = ν

                  Two measures which are finite on closed-open intervals are equal if they agree on all closed-open intervals.

                  theorem MeasureTheory.Measure.ext_of_Ioc {α : Type u_7} [TopologicalSpace α] {_m : MeasurableSpace α} [SecondCountableTopology α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [BorelSpace α] [NoMinOrder α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] (h : ∀ ⦃a b : α⦄, a < bμ (Set.Ioc a b) = ν (Set.Ioc a b)) :
                  μ = ν

                  Two measures which are finite on closed-open intervals are equal if they agree on all open-closed intervals.

                  theorem MeasureTheory.Measure.ext_of_Iic {α : Type u_7} [TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (a : α), μ (Set.Iic a) = ν (Set.Iic a)) :
                  μ = ν

                  Two finite measures on a Borel space are equal if they agree on all left-infinite right-closed intervals.

                  theorem MeasureTheory.Measure.ext_of_Ici {α : Type u_7} [TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (a : α), μ (Set.Ici a) = ν (Set.Ici a)) :
                  μ = ν

                  Two finite measures on a Borel space are equal if they agree on all left-closed right-infinite intervals.

                  theorem Measurable.max {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f : δα} {g : δα} (hf : Measurable f) (hg : Measurable g) :
                  Measurable fun (a : δ) => max (f a) (g a)
                  theorem AEMeasurable.max {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f : δα} {g : δα} {μ : MeasureTheory.Measure δ} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
                  AEMeasurable (fun (a : δ) => max (f a) (g a)) μ
                  theorem Measurable.min {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f : δα} {g : δα} (hf : Measurable f) (hg : Measurable g) :
                  Measurable fun (a : δ) => min (f a) (g a)
                  theorem AEMeasurable.min {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f : δα} {g : δα} {μ : MeasureTheory.Measure δ} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
                  AEMeasurable (fun (a : δ) => min (f a) (g a)) μ
                  theorem Continuous.measurable {α : Type u_1} {γ : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] {f : αγ} (hf : Continuous f) :

                  A continuous function from an OpensMeasurableSpace to a BorelSpace is measurable.

                  theorem Continuous.aemeasurable {α : Type u_1} {γ : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] {f : αγ} (h : Continuous f) {μ : MeasureTheory.Measure α} :

                  A continuous function from an OpensMeasurableSpace to a BorelSpace is ae-measurable.

                  theorem ContinuousOn.measurable_piecewise {α : Type u_1} {γ : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] {f : αγ} {g : αγ} {s : Set α} [(j : α) → Decidable (j s)] (hf : ContinuousOn f s) (hg : ContinuousOn g s) (hs : MeasurableSet s) :

                  If a function is defined piecewise in terms of functions which are continuous on their respective pieces, then it is measurable.

                  Equations
                  • =
                  Equations
                  • =
                  Equations
                  • =
                  Equations
                  • =
                  Equations
                  • =
                  def Homeomorph.toMeasurableEquiv {γ : Type u_3} {γ₂ : Type u_4} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [TopologicalSpace γ₂] [MeasurableSpace γ₂] [BorelSpace γ₂] (h : γ ≃ₜ γ₂) :
                  γ ≃ᵐ γ₂

                  A homeomorphism between two Borel spaces is a measurable equivalence.

                  Equations
                  Instances For
                    theorem Homeomorph.measurableEmbedding {γ : Type u_3} {γ₂ : Type u_4} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [TopologicalSpace γ₂] [MeasurableSpace γ₂] [BorelSpace γ₂] (h : γ ≃ₜ γ₂) :
                    @[simp]
                    theorem Homeomorph.toMeasurableEquiv_coe {γ : Type u_3} {γ₂ : Type u_4} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [TopologicalSpace γ₂] [MeasurableSpace γ₂] [BorelSpace γ₂] (h : γ ≃ₜ γ₂) :
                    @[simp]
                    theorem Homeomorph.toMeasurableEquiv_symm_coe {γ : Type u_3} {γ₂ : Type u_4} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [TopologicalSpace γ₂] [MeasurableSpace γ₂] [BorelSpace γ₂] (h : γ ≃ₜ γ₂) :
                    theorem Continuous.measurable2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace β] [MeasurableSpace β] [OpensMeasurableSpace β] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [MeasurableSpace δ] [SecondCountableTopologyEither α β] {f : δα} {g : δβ} {c : αβγ} (h : Continuous fun (p : α × β) => c p.1 p.2) (hf : Measurable f) (hg : Measurable g) :
                    Measurable fun (a : δ) => c (f a) (g a)
                    theorem Continuous.aemeasurable2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace β] [MeasurableSpace β] [OpensMeasurableSpace β] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [MeasurableSpace δ] [SecondCountableTopologyEither α β] {f : δα} {g : δβ} {c : αβγ} {μ : MeasureTheory.Measure δ} (h : Continuous fun (p : α × β) => c p.1 p.2) (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
                    AEMeasurable (fun (a : δ) => c (f a) (g a)) μ
                    theorem pi_le_borel_pi {ι : Type u_6} {π : ιType u_7} [(i : ι) → TopologicalSpace (π i)] [(i : ι) → MeasurableSpace (π i)] [∀ (i : ι), BorelSpace (π i)] :
                    MeasurableSpace.pi borel ((i : ι) → π i)
                    theorem prod_le_borel_prod {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] :
                    Prod.instMeasurableSpace borel (α × β)
                    instance Pi.borelSpace {ι : Type u_6} {π : ιType u_7} [Countable ι] [(i : ι) → TopologicalSpace (π i)] [(i : ι) → MeasurableSpace (π i)] [∀ (i : ι), SecondCountableTopology (π i)] [∀ (i : ι), BorelSpace (π i)] :
                    BorelSpace ((i : ι) → π i)
                    Equations
                    • =
                    Equations
                    • =
                    theorem MeasurableEmbedding.borelSpace {α : Type u_6} {β : Type u_7} [MeasurableSpace α] [TopologicalSpace α] [MeasurableSpace β] [TopologicalSpace β] [hβ : BorelSpace β] {e : αβ} (h'e : MeasurableEmbedding e) (h''e : Inducing e) :

                    Given a measurable embedding to a Borel space which is also a topological embedding, then the source space is also a Borel space.

                    theorem measurable_of_Iio {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δα} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' Set.Iio x)) :
                    theorem measurable_of_Ioi {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δα} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' Set.Ioi x)) :
                    theorem measurable_of_Iic {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δα} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' Set.Iic x)) :
                    theorem measurable_of_Ici {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δα} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' Set.Ici x)) :
                    theorem Measurable.isLUB {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} [Countable ι] {f : ιδα} {g : δα} (hf : ∀ (i : ι), Measurable (f i)) (hg : ∀ (b : δ), IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)) :

                    If a function is the least upper bound of countably many measurable functions, then it is measurable.

                    theorem Measurable.isLUB_of_mem {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} [Countable ι] {f : ιδα} {g : δα} {g' : δα} (hf : ∀ (i : ι), Measurable (f i)) {s : Set δ} (hs : MeasurableSet s) (hg : bs, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)) (hg' : Set.EqOn g g' s) (g'_meas : Measurable g') :

                    If a function is the least upper bound of countably many measurable functions on a measurable set s, and coincides with a measurable function outside of s, then it is measurable.

                    theorem AEMeasurable.isLUB {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} {μ : MeasureTheory.Measure δ} [Countable ι] {f : ιδα} {g : δα} (hf : ∀ (i : ι), AEMeasurable (f i) μ) (hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)) :
                    theorem Measurable.isGLB {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} [Countable ι] {f : ιδα} {g : δα} (hf : ∀ (i : ι), Measurable (f i)) (hg : ∀ (b : δ), IsGLB {a : α | ∃ (i : ι), f i b = a} (g b)) :

                    If a function is the greatest lower bound of countably many measurable functions, then it is measurable.

                    theorem Measurable.isGLB_of_mem {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} [Countable ι] {f : ιδα} {g : δα} {g' : δα} (hf : ∀ (i : ι), Measurable (f i)) {s : Set δ} (hs : MeasurableSet s) (hg : bs, IsGLB {a : α | ∃ (i : ι), f i b = a} (g b)) (hg' : Set.EqOn g g' s) (g'_meas : Measurable g') :

                    If a function is the greatest lower bound of countably many measurable functions on a measurable set s, and coincides with a measurable function outside of s, then it is measurable.

                    theorem AEMeasurable.isGLB {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} {μ : MeasureTheory.Measure δ} [Countable ι] {f : ιδα} {g : δα} (hf : ∀ (i : ι), AEMeasurable (f i) μ) (hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a : α | ∃ (i : ι), f i b = a} (g b)) :
                    theorem measurableSet_of_mem_nhdsWithin_Ioi_aux {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {s : Set α} (h : xs, s nhdsWithin x (Set.Ioi x)) (h' : xs, ∃ (y : α), x < y) :

                    If a set is a right-neighborhood of all of its points, then it is measurable.

                    theorem measurableSet_bddAbove_range {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} [Countable ι] {f : ιδα} (hf : ∀ (i : ι), Measurable (f i)) :
                    MeasurableSet {b : δ | BddAbove (Set.range fun (i : ι) => f i b)}
                    theorem measurableSet_bddBelow_range {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} [Countable ι] {f : ιδα} (hf : ∀ (i : ι), Measurable (f i)) :
                    MeasurableSet {b : δ | BddBelow (Set.range fun (i : ι) => f i b)}
                    theorem Measurable.iSup_Prop {δ : Type u_5} [MeasurableSpace δ] {α : Type u_6} [MeasurableSpace α] [ConditionallyCompleteLattice α] (p : Prop) {f : δα} (hf : Measurable f) :
                    Measurable fun (b : δ) => ⨆ (_ : p), f b
                    theorem Measurable.iInf_Prop {δ : Type u_5} [MeasurableSpace δ] {α : Type u_6} [MeasurableSpace α] [ConditionallyCompleteLattice α] (p : Prop) {f : δα} (hf : Measurable f) :
                    Measurable fun (b : δ) => ⨅ (_ : p), f b
                    theorem measurable_iSup {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} [Countable ι] {f : ιδα} (hf : ∀ (i : ι), Measurable (f i)) :
                    Measurable fun (b : δ) => ⨆ (i : ι), f i b
                    theorem aemeasurable_iSup {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} {μ : MeasureTheory.Measure δ} [Countable ι] {f : ιδα} (hf : ∀ (i : ι), AEMeasurable (f i) μ) :
                    AEMeasurable (fun (b : δ) => ⨆ (i : ι), f i b) μ
                    theorem measurable_iInf {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} [Countable ι] {f : ιδα} (hf : ∀ (i : ι), Measurable (f i)) :
                    Measurable fun (b : δ) => ⨅ (i : ι), f i b
                    theorem aemeasurable_iInf {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} {μ : MeasureTheory.Measure δ} [Countable ι] {f : ιδα} (hf : ∀ (i : ι), AEMeasurable (f i) μ) :
                    AEMeasurable (fun (b : δ) => ⨅ (i : ι), f i b) μ
                    theorem measurable_sSup {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_6} {f : ιδα} {s : Set ι} (hs : Set.Countable s) (hf : is, Measurable (f i)) :
                    Measurable fun (x : δ) => sSup ((fun (i : ι) => f i x) '' s)
                    theorem measurable_sInf {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_6} {f : ιδα} {s : Set ι} (hs : Set.Countable s) (hf : is, Measurable (f i)) :
                    Measurable fun (x : δ) => sInf ((fun (i : ι) => f i x) '' s)
                    theorem measurable_biSup {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_6} (s : Set ι) {f : ιδα} (hs : Set.Countable s) (hf : is, Measurable (f i)) :
                    Measurable fun (b : δ) => ⨆ i ∈ s, f i b
                    theorem aemeasurable_biSup {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_6} {μ : MeasureTheory.Measure δ} (s : Set ι) {f : ιδα} (hs : Set.Countable s) (hf : is, AEMeasurable (f i) μ) :
                    AEMeasurable (fun (b : δ) => ⨆ i ∈ s, f i b) μ
                    theorem measurable_biInf {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_6} (s : Set ι) {f : ιδα} (hs : Set.Countable s) (hf : is, Measurable (f i)) :
                    Measurable fun (b : δ) => ⨅ i ∈ s, f i b
                    theorem aemeasurable_biInf {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_6} {μ : MeasureTheory.Measure δ} (s : Set ι) {f : ιδα} (hs : Set.Countable s) (hf : is, AEMeasurable (f i) μ) :
                    AEMeasurable (fun (b : δ) => ⨅ i ∈ s, f i b) μ
                    theorem measurable_liminf' {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_6} {ι' : Type u_7} {f : ιδα} {v : Filter ι} (hf : ∀ (i : ι), Measurable (f i)) {p : ι'Prop} {s : ι'Set ι} (hv : Filter.HasCountableBasis v p s) (hs : ∀ (j : ι'), Set.Countable (s j)) :
                    Measurable fun (x : δ) => Filter.liminf (fun (x_1 : ι) => f x_1 x) v

                    liminf over a general filter is measurable. See measurable_liminf for the version over .

                    theorem measurable_limsup' {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_6} {ι' : Type u_7} {f : ιδα} {u : Filter ι} (hf : ∀ (i : ι), Measurable (f i)) {p : ι'Prop} {s : ι'Set ι} (hu : Filter.HasCountableBasis u p s) (hs : ∀ (i : ι'), Set.Countable (s i)) :
                    Measurable fun (x : δ) => Filter.limsup (fun (i : ι) => f i x) u

                    limsup over a general filter is measurable. See measurable_limsup for the version over .

                    theorem measurable_liminf {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δα} (hf : ∀ (i : ), Measurable (f i)) :
                    Measurable fun (x : δ) => Filter.liminf (fun (i : ) => f i x) Filter.atTop

                    liminf over is measurable. See measurable_liminf' for a version with a general filter.

                    theorem measurable_limsup {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δα} (hf : ∀ (i : ), Measurable (f i)) :
                    Measurable fun (x : δ) => Filter.limsup (fun (i : ) => f i x) Filter.atTop

                    limsup over is measurable. See measurable_limsup' for a version with a general filter.

                    Convert a Homeomorph to a MeasurableEquiv.

                    Equations
                    Instances For
                      Equations
                      theorem measure_eq_measure_preimage_add_measure_tsum_Ico_zpow {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : αENNReal} (hf : Measurable f) {s : Set α} (hs : MeasurableSet s) {t : NNReal} (ht : 1 < t) :
                      μ s = μ (s f ⁻¹' {0}) + μ (s f ⁻¹' {}) + ∑' (n : ), μ (s f ⁻¹' Set.Ico (t ^ n) (t ^ (n + 1)))

                      One can cut out ℝ≥0∞ into the sets {0}, Ico (t^n) (t^(n+1)) for n : ℤ and {∞}. This gives a way to compute the measure of a set in terms of sets on which a given function f does not fluctuate by more than t.

                      theorem Measurable.infDist {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : βα} (hf : Measurable f) {s : Set α} :
                      Measurable fun (x : β) => Metric.infDist (f x) s
                      theorem Measurable.infNndist {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : βα} (hf : Measurable f) {s : Set α} :
                      Measurable fun (x : β) => Metric.infNndist (f x) s
                      theorem Measurable.dist {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] [SecondCountableTopology α] {f : βα} {g : βα} (hf : Measurable f) (hg : Measurable g) :
                      Measurable fun (b : β) => dist (f b) (g b)
                      theorem Measurable.nndist {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] [SecondCountableTopology α] {f : βα} {g : βα} (hf : Measurable f) (hg : Measurable g) :
                      Measurable fun (b : β) => nndist (f b) (g b)
                      theorem measurable_edist_left {α : Type u_1} [PseudoEMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {x : α} :
                      Measurable fun (y : α) => edist y x
                      theorem Measurable.infEdist {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : βα} (hf : Measurable f) {s : Set α} :
                      Measurable fun (x : β) => EMetric.infEdist (f x) s
                      theorem tendsto_measure_cthickening {α : Type u_1} [PseudoEMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : ∃ R > 0, μ (Metric.cthickening R s) ) :
                      Filter.Tendsto (fun (r : ) => μ (Metric.cthickening r s)) (nhds 0) (nhds (μ (closure s)))

                      If a set has a closed thickening with finite measure, then the measure of its r-closed thickenings converges to the measure of its closure as r tends to 0.

                      theorem tendsto_measure_cthickening_of_isClosed {α : Type u_1} [PseudoEMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : ∃ R > 0, μ (Metric.cthickening R s) ) (h's : IsClosed s) :
                      Filter.Tendsto (fun (r : ) => μ (Metric.cthickening r s)) (nhds 0) (nhds (μ s))

                      If a closed set has a closed thickening with finite measure, then the measure of its closed r-thickenings converge to its measure as r tends to 0.

                      theorem tendsto_measure_thickening {α : Type u_1} [PseudoEMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : ∃ R > 0, μ (Metric.thickening R s) ) :
                      Filter.Tendsto (fun (r : ) => μ (Metric.thickening r s)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (μ (closure s)))

                      If a set has a thickening with finite measure, then the measures of its r-thickenings converge to the measure of its closure as r > 0 tends to 0.

                      theorem tendsto_measure_thickening_of_isClosed {α : Type u_1} [PseudoEMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : ∃ R > 0, μ (Metric.thickening R s) ) (h's : IsClosed s) :
                      Filter.Tendsto (fun (r : ) => μ (Metric.thickening r s)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (μ s))

                      If a closed set has a thickening with finite measure, then the measure of its r-thickenings converge to its measure as r > 0 tends to 0.

                      theorem Measurable.edist {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] [SecondCountableTopology α] {f : βα} {g : βα} (hf : Measurable f) (hg : Measurable g) :
                      Measurable fun (b : β) => edist (f b) (g b)
                      theorem AEMeasurable.edist {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] [SecondCountableTopology α] {f : βα} {g : βα} {μ : MeasureTheory.Measure β} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
                      AEMeasurable (fun (a : β) => edist (f a) (g a)) μ

                      Given a compact set in a proper space, the measure of its r-closed thickenings converges to its measure as r tends to 0.

                      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})

                      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 : α) => Real.toNNReal (f x)
                        theorem AEMeasurable.real_toNNReal {α : Type u_1} [MeasurableSpace α] {f : α} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) :
                        AEMeasurable (fun (x : α) => Real.toNNReal (f x)) μ
                        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.

                        theorem ENNReal.measurable_of_measurable_nnreal {α : Type u_1} [MeasurableSpace α] {f : ENNRealα} (h : Measurable fun (p : NNReal) => f p) :

                        ℝ≥0∞ is MeasurableEquiv to ℝ≥0 ⊕ Unit.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          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_6} {f : ιαENNReal} {g : αENNReal} (u : Filter ι) [Filter.NeBot u] [Filter.IsCountablyGenerated u] (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_6} {f : ιαENNReal} {g : αENNReal} (u : Filter ι) [Filter.NeBot u] [Filter.IsCountablyGenerated u] (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_6} {f : ιαENNReal} {g : αENNReal} {μ : MeasureTheory.Measure α} (u : Filter ι) [Filter.NeBot u] [Filter.IsCountablyGenerated u] (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_6} [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_6} [Countable ι] {f : ιαENNReal} (h : ∀ (i : ι), Measurable (f i)) :
                          Measurable (∑' (i : ι), f i)
                          theorem Measurable.nnreal_tsum {α : Type u_1} [MeasurableSpace α] {ι : Type u_6} [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_6} [Countable ι] {f : ιαENNReal} {μ : MeasureTheory.Measure α} (h : ∀ (i : ι), AEMeasurable (f i) μ) :
                          AEMeasurable (fun (x : α) => ∑' (i : ι), f i x) μ
                          theorem AEMeasurable.nnreal_tsum {α : Type u_6} [MeasurableSpace α] {ι : Type u_7} [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)) μ
                          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 : α) => EReal.toReal (f x)
                          theorem AEMeasurable.ereal_toReal {α : Type u_1} [MeasurableSpace α] {f : αEReal} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) :
                          AEMeasurable (fun (x : α) => EReal.toReal (f x)) μ
                          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_6} {f : ιαNNReal} {g : αNNReal} (u : Filter ι) [Filter.NeBot u] [Filter.IsCountablyGenerated u] (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_6} {f : ιαNNReal} {g : αNNReal} (u : Filter ι) [Filter.NeBot u] [Filter.IsCountablyGenerated u] (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_1} {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.

                          theorem Measurable.norm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [NormedAddCommGroup α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : βα} (hf : Measurable f) :
                          Measurable fun (a : β) => f a
                          theorem AEMeasurable.norm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [NormedAddCommGroup α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : βα} {μ : MeasureTheory.Measure β} (hf : AEMeasurable f μ) :
                          AEMeasurable (fun (a : β) => f a) μ
                          theorem Measurable.nnnorm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [NormedAddCommGroup α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : βα} (hf : Measurable f) :
                          Measurable fun (a : β) => f a‖₊
                          theorem AEMeasurable.nnnorm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [NormedAddCommGroup α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : βα} {μ : MeasureTheory.Measure β} (hf : AEMeasurable f μ) :
                          AEMeasurable (fun (a : β) => f a‖₊) μ
                          theorem Measurable.ennnorm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [NormedAddCommGroup α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : βα} (hf : Measurable f) :
                          Measurable fun (a : β) => f a‖₊
                          theorem AEMeasurable.ennnorm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [NormedAddCommGroup α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : βα} {μ : MeasureTheory.Measure β} (hf : AEMeasurable f μ) :
                          AEMeasurable (fun (a : β) => f a‖₊) μ