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
      theorem OpensMeasurableSpace.borel_le {α : Type u_6} :
      ∀ {inst : TopologicalSpace α} {h : MeasurableSpace α} [self : OpensMeasurableSpace α], borel α h

      Borel-measurable sets are measurable.

      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
        theorem BorelSpace.measurable_eq {α : Type u_6} :
        ∀ {inst : TopologicalSpace α} {inst_1 : MeasurableSpace α} [self : BorelSpace α], inst_1 = borel α

        The measurable sets are exactly the Borel-measurable sets.

        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
                @[instance 100]
                Equations
                • =
                @[instance 100]
                Equations
                • =
                @[instance 100]

                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 ss.Nonemptys Set.univMeasurableSet (f ⁻¹' s)) :
                instance nhds_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] (a : α) :
                (nhds a).IsMeasurablyGenerated
                Equations
                • =
                theorem MeasurableSet.nhdsWithin_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α} (hs : MeasurableSet s) (a : α) :
                (nhdsWithin a s).IsMeasurablyGenerated

                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
                  @[instance 100]
                  Equations
                  • =
                  @[instance 100]
                  Equations
                  • =

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

                  Equations
                  • =
                  theorem interior_ae_eq_of_null_frontier {α' : Type u_6} [TopologicalSpace α'] [MeasurableSpace α'] {μ : MeasureTheory.Measure α'} {s : Set α'} (h : μ (frontier s) = 0) :
                  theorem measure_interior_of_null_frontier {α' : Type u_6} [TopologicalSpace α'] [MeasurableSpace α'] {μ : MeasureTheory.Measure α'} {s : Set α'} (h : μ (frontier s) = 0) :
                  μ (interior s) = μ s
                  theorem closure_ae_eq_of_null_frontier {α' : Type u_6} [TopologicalSpace α'] [MeasurableSpace α'] {μ : MeasureTheory.Measure α'} {s : Set α'} (h : μ (frontier s) = 0) :
                  theorem measure_closure_of_null_frontier {α' : Type u_6} [TopologicalSpace α'] [MeasurableSpace α'] {μ : MeasureTheory.Measure α'} {s : Set α'} (h : μ (frontier s) = 0) :
                  μ (closure s) = μ s
                  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) :
                  Measurable (s.piecewise f g)

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

                  @[instance 100]
                  Equations
                  • =
                  @[instance 100]
                  Equations
                  • =
                  @[instance 100]
                  Equations
                  • =
                  @[instance 100]
                  Equations
                  • =
                  @[instance 100]
                  Equations
                  • =
                  @[instance 100]
                  Equations
                  • =
                  @[instance 100]
                  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
                  • h.toMeasurableEquiv = { toEquiv := h.toEquiv, measurable_toFun := , measurable_invFun := }
                  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 : γ ≃ₜ γ₂) :
                    h.toMeasurableEquiv = h
                    @[simp]
                    theorem Homeomorph.toMeasurableEquiv_symm_coe {γ : Type u_3} {γ₂ : Type u_4} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [TopologicalSpace γ₂] [MeasurableSpace γ₂] [BorelSpace γ₂] (h : γ ≃ₜ γ₂) :
                    h.toMeasurableEquiv.symm = h.symm
                    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)) μ
                    @[instance 100]
                    Equations
                    • =
                    @[instance 100]
                    Equations
                    • =
                    @[instance 100]
                    Equations
                    • =
                    @[instance 100]
                    Equations
                    • =
                    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.

                    Equations