Basic.lean

/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Yury Kudryashov
-/
import Mathlib.Analysis.Normed.Group.Basic
import Mathlib.MeasureTheory.Function.AEMeasurableSequence
import Mathlib.MeasureTheory.Group.Arithmetic
import Mathlib.MeasureTheory.Order.Lattice
import Mathlib.Topology.Instances.EReal
import Mathlib.Topology.MetricSpace.Thickening
import Mathlib.Topology.GDelta
import Mathlib.Topology.Order.Lattice
import Mathlib.Topology.Semicontinuous

#align_import measure_theory.constructions.borel_space.basic from "leanprover-community/mathlib"@"9f55d0d4363ae59948c33864cbc52e0b12e0e8ce"

/-!
# Borel (measurable) space

## Main definitions

* `borel α` : the least `σ`-algebra that contains all open sets;
* `class BorelSpace` : a space with `TopologicalSpace` and `MeasurableSpace` structures
  such that `‹MeasurableSpace α› = borel α`;
* `class OpensMeasurableSpace` : a space with `TopologicalSpace` and `MeasurableSpace`
  structures such that all open sets are measurable; equivalently, `borel α ≤ ‹MeasurableSpace α›`.
* `BorelSpace` instances on `Empty`, `Unit`, `Bool`, `Nat`, `Int`, `Rat`;
* `MeasurableSpace` and `BorelSpace` instances on `ℝ`, `ℝ≥0`, `ℝ≥0∞`.

## Main statements

* `IsOpen.measurableSet`, `IsClosed.measurableSet`: open and closed sets are measurable;
* `Continuous.measurable` : a continuous function is measurable;
* `Continuous.measurable2` : if `f : α → β` and `g : α → γ` are measurable and `op : β × γ → δ`
  is continuous, then `fun x => op (f x, g y)` is measurable;
* `Measurable.add` etc : dot notation for arithmetic operations on `Measurable` predicates,
  and similarly for `dist` and `edist`;
* `AEMeasurable.add` : similar dot notation for almost everywhere measurable functions;
* `Measurable.ennreal*` : special cases for arithmetic operations on `ℝ≥0∞`.
-/


noncomputable section

open Set Filter MeasureTheory

open scoped Classical BigOperators Topology NNReal ENNReal MeasureTheory

universe u v w x y

variable {α β γ γ₂ δ : Type*} {ι : Sort y} {s t u : Set α}

open MeasurableSpace TopologicalSpace

/-- `MeasurableSpace` structure generated by `TopologicalSpace`. -/
def borel (α : Type u) [TopologicalSpace α] : MeasurableSpace α :=
  generateFrom { s : Set α | IsOpen s }
#align borel borel

theorem borel_anti : Antitone (@borel α) := fun _ _ h =>
  MeasurableSpace.generateFrom_le fun _ hs => .basic _ (h _ hs)
#align borel_anti borel_anti

theorem borel_eq_top_of_discrete [TopologicalSpace α] [DiscreteTopology α] : borel α = ⊤ :=
  top_le_iff.1 fun s _ => GenerateMeasurable.basic s (isOpen_discrete s)
#align borel_eq_top_of_discrete borel_eq_top_of_discrete

theorem borel_eq_top_of_countable [TopologicalSpace α] [T1Space α] [Countable α] : borel α = ⊤ := by
  refine' top_le_iff.1 fun s _ => biUnion_of_singleton s ▸ _
  apply MeasurableSet.biUnion s.to_countable
  intro x _
  apply MeasurableSet.of_compl
  apply GenerateMeasurable.basic
  exact isClosed_singleton.isOpen_compl
#align borel_eq_top_of_countable borel_eq_top_of_countable

theorem borel_eq_generateFrom_of_subbasis {s : Set (Set α)} [t : TopologicalSpace α]
    [SecondCountableTopology α] (hs : t = .generateFrom s) : borel α = .generateFrom s :=
  le_antisymm
    (generateFrom_le fun u (hu : t.IsOpen u) => by
      rw [hs] at hu
      induction hu with
      | basic u hu => exact GenerateMeasurable.basic u hu
      | univ => exact @MeasurableSet.univ α (generateFrom s)
      | inter s₁ s₂ _ _ hs₁ hs₂ => exact @MeasurableSet.inter α (generateFrom s) _ _ hs₁ hs₂
      | sUnion f hf ih =>
        rcases isOpen_sUnion_countable f (by rwa [hs]) with ⟨v, hv, vf, vu⟩
        rw [← vu]
        exact @MeasurableSet.sUnion α (generateFrom s) _ hv fun x xv => ih _ (vf xv))
    (generateFrom_le fun u hu =>
      GenerateMeasurable.basic _ <| show t.IsOpen u by rw [hs]; exact GenerateOpen.basic _ hu)
#align borel_eq_generate_from_of_subbasis borel_eq_generateFrom_of_subbasis

theorem TopologicalSpace.IsTopologicalBasis.borel_eq_generateFrom [TopologicalSpace α]
    [SecondCountableTopology α] {s : Set (Set α)} (hs : IsTopologicalBasis s) :
    borel α = .generateFrom s :=
  borel_eq_generateFrom_of_subbasis hs.eq_generateFrom
#align topological_space.is_topological_basis.borel_eq_generate_from TopologicalSpace.IsTopologicalBasis.borel_eq_generateFrom

theorem isPiSystem_isOpen [TopologicalSpace α] : IsPiSystem ({s : Set α | IsOpen s}) :=
  fun _s hs _t ht _ => IsOpen.inter hs ht
#align is_pi_system_is_open isPiSystem_isOpen

lemma isPiSystem_isClosed [TopologicalSpace α] : IsPiSystem ({s : Set α | IsClosed s}) :=
  fun _s hs _t ht _ ↦ IsClosed.inter hs ht

theorem borel_eq_generateFrom_isClosed [TopologicalSpace α] :
    borel α = .generateFrom { s | IsClosed s } :=
  le_antisymm
    (generateFrom_le fun _t ht =>
      @MeasurableSet.of_compl α _ (generateFrom { s | IsClosed s })
        (GenerateMeasurable.basic _ <| isClosed_compl_iff.2 ht))
    (generateFrom_le fun _t ht =>
      @MeasurableSet.of_compl α _ (borel α) (GenerateMeasurable.basic _ <| isOpen_compl_iff.2 ht))
#align borel_eq_generate_from_is_closed borel_eq_generateFrom_isClosed

section OrderTopology

variable (α)
variable [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [OrderTopology α]

theorem borel_eq_generateFrom_Iio : borel α = .generateFrom (range Iio) := by
  refine' le_antisymm _ (generateFrom_le _)
  · rw [borel_eq_generateFrom_of_subbasis (@OrderTopology.topology_eq_generate_intervals α _ _ _)]
    letI : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
    have H : ∀ a : α, MeasurableSet (Iio a) := fun a => GenerateMeasurable.basic _ ⟨_, rfl⟩
    refine' generateFrom_le _
    rintro _ ⟨a, rfl | rfl⟩
    · rcases em (∃ b, a ⋖ b) with ⟨b, hb⟩ | hcovBy
      · rw [hb.Ioi_eq, ← compl_Iio]
        exact (H _).compl
      · rcases isOpen_biUnion_countable (Ioi a) Ioi fun _ _ ↦ isOpen_Ioi with ⟨t, hat, htc, htU⟩
        have : Ioi a = ⋃ b ∈ t, Ici b := by
          refine Subset.antisymm ?_ <| iUnion₂_subset fun b hb ↦ Ici_subset_Ioi.2 (hat hb)
          refine Subset.trans ?_ <| iUnion₂_mono fun _ _ ↦ Ioi_subset_Ici_self
          simpa [CovBy, htU, subset_def] using hcovBy
        simp only [this, ← compl_Iio]
        exact .biUnion htc <| fun _ _ ↦ (H _).compl
    · apply H
  · rw [forall_mem_range]
    intro a
    exact GenerateMeasurable.basic _ isOpen_Iio
#align borel_eq_generate_from_Iio borel_eq_generateFrom_Iio

theorem borel_eq_generateFrom_Ioi : borel α = .generateFrom (range Ioi) :=
  @borel_eq_generateFrom_Iio αᵒᵈ _ (by infer_instance : SecondCountableTopology α) _ _
#align borel_eq_generate_from_Ioi borel_eq_generateFrom_Ioi

theorem borel_eq_generateFrom_Iic :
    borel α = MeasurableSpace.generateFrom (range Iic) := by
  rw [borel_eq_generateFrom_Ioi]
  refine' le_antisymm _ _
  · refine' MeasurableSpace.generateFrom_le fun t ht => _
    obtain ⟨u, rfl⟩ := ht
    rw [← compl_Iic]
    exact (MeasurableSpace.measurableSet_generateFrom (mem_range.mpr ⟨u, rfl⟩)).compl
  · refine' MeasurableSpace.generateFrom_le fun t ht => _
    obtain ⟨u, rfl⟩ := ht
    rw [← compl_Ioi]
    exact (MeasurableSpace.measurableSet_generateFrom (mem_range.mpr ⟨u, rfl⟩)).compl
#align borel_eq_generate_from_Iic borel_eq_generateFrom_Iic

theorem borel_eq_generateFrom_Ici : borel α = MeasurableSpace.generateFrom (range Ici) :=
  @borel_eq_generateFrom_Iic αᵒᵈ _ _ _ _
#align borel_eq_generate_from_Ici borel_eq_generateFrom_Ici

end OrderTopology

theorem borel_comap {f : α → β} {t : TopologicalSpace β} :
    @borel α (t.induced f) = (@borel β t).comap f :=
  comap_generateFrom.symm
#align borel_comap borel_comap

theorem Continuous.borel_measurable [TopologicalSpace α] [TopologicalSpace β] {f : α → β}
    (hf : Continuous f) : @Measurable α β (borel α) (borel β) f :=
  Measurable.of_le_map <|
    generateFrom_le fun s hs => GenerateMeasurable.basic (f ⁻¹' s) (hs.preimage hf)
#align continuous.borel_measurable Continuous.borel_measurable

/-- A space with `MeasurableSpace` and `TopologicalSpace` structures such that
all open sets are measurable. -/
class OpensMeasurableSpace (α : Type*) [TopologicalSpace α] [h : MeasurableSpace α] : Prop where
  /-- Borel-measurable sets are measurable. -/
  borel_le : borel α ≤ h
#align opens_measurable_space OpensMeasurableSpace
#align opens_measurable_space.borel_le OpensMeasurableSpace.borel_le

/-- A space with `MeasurableSpace` and `TopologicalSpace` structures such that
the `σ`-algebra of measurable sets is exactly the `σ`-algebra generated by open sets. -/
class BorelSpace (α : Type*) [TopologicalSpace α] [MeasurableSpace α] : Prop where
  /-- The measurable sets are exactly the Borel-measurable sets. -/
  measurable_eq : ‹MeasurableSpace α› = borel α
#align borel_space BorelSpace
#align borel_space.measurable_eq BorelSpace.measurable_eq

namespace Mathlib.Tactic.Borelize

open Lean Elab Term Tactic Meta

/-- The behaviour of `borelize α` depends on the existing assumptions on `α`.

- if `α` is a topological space with instances `[MeasurableSpace α] [BorelSpace α]`, then
  `borelize α` replaces the former instance by `borel α`;
- otherwise, `borelize α` adds instances `borel α : MeasurableSpace α` and `⟨rfl⟩ : BorelSpace α`.

Finally, `borelize α β γ` runs `borelize α; borelize β; borelize γ`.
-/
syntax "borelize" (ppSpace colGt term:max)* : tactic

/-- Add instances `borel e : MeasurableSpace e` and `⟨rfl⟩ : BorelSpace e`. -/
def addBorelInstance (e : Expr) : TacticM Unit := do
  let t ← Lean.Elab.Term.exprToSyntax e
  evalTactic <| ← `(tactic|
    refine_lift
      letI : MeasurableSpace $t := borel $t
      haveI : BorelSpace $t := ⟨rfl⟩
      ?_)

/-- Given a type `e`, an assumption `i : MeasurableSpace e`, and an instance `[BorelSpace e]`,
replace `i` with `borel e`. -/
def borelToRefl (e : Expr) (i : FVarId) : TacticM Unit := do
  let te ← Lean.Elab.Term.exprToSyntax e
  evalTactic <| ← `(tactic|
    have := @BorelSpace.measurable_eq $te _ _ _)
  try
    liftMetaTactic fun m => return [← subst m i]
  catch _ =>
    let et ← synthInstance (← mkAppOptM ``TopologicalSpace #[e])
    throwError m!"\
      `‹TopologicalSpace {e}› := {et}\n\
      depends on\n\
      {Expr.fvar i} : MeasurableSpace {e}`\n\
      so `borelize` isn't avaliable"
  evalTactic <| ← `(tactic|
    refine_lift
      letI : MeasurableSpace $te := borel $te
      ?_)

/-- 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`. -/
def borelize (t : Term) : TacticM Unit := withMainContext <| do
  let u ← mkFreshLevelMVar
  let e ← withoutRecover <| Tactic.elabTermEnsuringType t (mkSort (mkLevelSucc u))
  let i? ← findLocalDeclWithType? (← mkAppOptM ``MeasurableSpace #[e])
  i?.elim (addBorelInstance e) (borelToRefl e)

elab_rules : tactic
  | `(tactic| borelize $[$t:term]*) => t.forM borelize

end Mathlib.Tactic.Borelize

instance (priority := 100) OrderDual.opensMeasurableSpace {α : Type*} [TopologicalSpace α]
    [MeasurableSpace α] [h : OpensMeasurableSpace α] : OpensMeasurableSpace αᵒᵈ where
  borel_le := h.borel_le
#align order_dual.opens_measurable_space OrderDual.opensMeasurableSpace

instance (priority := 100) OrderDual.borelSpace {α : Type*} [TopologicalSpace α]
    [MeasurableSpace α] [h : BorelSpace α] : BorelSpace αᵒᵈ where
  measurable_eq := h.measurable_eq
#align order_dual.borel_space OrderDual.borelSpace

/-- In a `BorelSpace` all open sets are measurable. -/
instance (priority := 100) BorelSpace.opensMeasurable {α : Type*} [TopologicalSpace α]
    [MeasurableSpace α] [BorelSpace α] : OpensMeasurableSpace α :=
  ⟨ge_of_eq <| BorelSpace.measurable_eq⟩
#align borel_space.opens_measurable BorelSpace.opensMeasurable

instance Subtype.borelSpace {α : Type*} [TopologicalSpace α] [MeasurableSpace α]
    [hα : BorelSpace α] (s : Set α) : BorelSpace s :=
  ⟨by borelize α; symm; apply borel_comap⟩
#align subtype.borel_space Subtype.borelSpace

instance Countable.instBorelSpace [Countable α] [MeasurableSpace α] [MeasurableSingletonClass α]
    [TopologicalSpace α] [DiscreteTopology α] : BorelSpace α := by
  have : ∀ s, @MeasurableSet α inferInstance s := fun s ↦ s.to_countable.measurableSet
  have : ∀ s, @MeasurableSet α (borel α) s := fun s ↦ measurableSet_generateFrom (isOpen_discrete s)
  exact ⟨by aesop⟩

instance Subtype.opensMeasurableSpace {α : Type*} [TopologicalSpace α] [MeasurableSpace α]
    [h : OpensMeasurableSpace α] (s : Set α) : OpensMeasurableSpace s :=
  ⟨by
    rw [borel_comap]
    exact comap_mono h.1⟩
#align subtype.opens_measurable_space Subtype.opensMeasurableSpace

lemma opensMeasurableSpace_iff_forall_measurableSet
    [TopologicalSpace α] [MeasurableSpace α] :
    OpensMeasurableSpace α ↔  (∀ (s : Set α), IsOpen s → MeasurableSet s) := by
  refine ⟨fun h s hs ↦ ?_, fun h ↦ ⟨generateFrom_le h⟩⟩
  exact OpensMeasurableSpace.borel_le _ <| GenerateMeasurable.basic _ hs

instance (priority := 100) BorelSpace.countablyGenerated {α : Type*} [TopologicalSpace α]
    [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] : CountablyGenerated α := by
  obtain ⟨b, bct, -, hb⟩ := exists_countable_basis α
  refine' ⟨⟨b, bct, _⟩⟩
  borelize α
  exact hb.borel_eq_generateFrom
#align borel_space.countably_generated BorelSpace.countablyGenerated

theorem MeasurableSet.induction_on_open [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α]
    {C : Set α → Prop} (h_open : ∀ U, IsOpen U → C U)
    (h_compl : ∀ t, MeasurableSet t → C t → C tᶜ)
    (h_union :
      ∀ f : ℕ → Set α,
        Pairwise (Disjoint on f) → (∀ i, MeasurableSet (f i)) → (∀ i, C (f i)) → C (⋃ i, f i)) :
    ∀ ⦃t⦄, MeasurableSet t → C t :=
  MeasurableSpace.induction_on_inter BorelSpace.measurable_eq isPiSystem_isOpen
    (h_open _ isOpen_empty) h_open h_compl h_union
#align measurable_set.induction_on_open MeasurableSet.induction_on_open

section

variable [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace β]
  [MeasurableSpace β] [OpensMeasurableSpace β] [TopologicalSpace γ] [MeasurableSpace γ]
  [BorelSpace γ] [TopologicalSpace γ₂] [MeasurableSpace γ₂] [BorelSpace γ₂] [MeasurableSpace δ]

theorem IsOpen.measurableSet (h : IsOpen s) : MeasurableSet s :=
  OpensMeasurableSpace.borel_le _ <| GenerateMeasurable.basic _ h
#align is_open.measurable_set IsOpen.measurableSet

instance (priority := 500) {s : Set α} [HasCountableSeparatingOn α IsOpen s] :
    HasCountableSeparatingOn α MeasurableSet s :=
  .mono (fun _ ↦ IsOpen.measurableSet) Subset.rfl

@[measurability]
theorem measurableSet_interior : MeasurableSet (interior s) :=
  isOpen_interior.measurableSet
#align measurable_set_interior measurableSet_interior

theorem IsGδ.measurableSet (h : IsGδ s) : MeasurableSet s := by
  rcases h with ⟨S, hSo, hSc, rfl⟩
  exact MeasurableSet.sInter hSc fun t ht => (hSo t ht).measurableSet
set_option linter.uppercaseLean3 false in
#align is_Gδ.measurable_set IsGδ.measurableSet

theorem measurableSet_of_continuousAt {β} [EMetricSpace β] (f : α → β) :
    MeasurableSet { x | ContinuousAt f x } :=
  (IsGδ.setOf_continuousAt f).measurableSet
#align measurable_set_of_continuous_at measurableSet_of_continuousAt

theorem IsClosed.measurableSet (h : IsClosed s) : MeasurableSet s :=
  h.isOpen_compl.measurableSet.of_compl
#align is_closed.measurable_set IsClosed.measurableSet

theorem IsCompact.measurableSet [T2Space α] (h : IsCompact s) : MeasurableSet s :=
  h.isClosed.measurableSet
#align is_compact.measurable_set IsCompact.measurableSet

/-- If two points are topologically inseparable,
then they can't be separated by a Borel measurable set. -/
theorem Inseparable.mem_measurableSet_iff {x y : γ} (h : Inseparable x y) {s : Set γ}
    (hs : MeasurableSet s) : x ∈ s ↔ y ∈ s :=
  hs.induction_on_open (C := fun s ↦ (x ∈ s ↔ y ∈ s)) (fun _ ↦ h.mem_open_iff) (fun s _ hs ↦ hs.not)
    fun _ _ _ h ↦ by simp [h]

/-- 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.closure_subset_measurableSet [R1Space γ] {K s : Set γ} (hK : IsCompact K)
    (hs : MeasurableSet s) (hKs : K ⊆ s) : closure K ⊆ s := by
  rw [hK.closure_eq_biUnion_inseparable, iUnion₂_subset_iff]
  exact fun x hx y hy ↦ (hy.mem_measurableSet_iff hs).1 (hKs hx)

/-- 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 IsCompact.measure_closure [R1Space γ] {K : Set γ} (hK : IsCompact K) (μ : Measure γ) :
    μ (closure K) = μ K := by
  refine le_antisymm ?_ (measure_mono subset_closure)
  calc
    μ (closure K) ≤ μ (toMeasurable μ K) := measure_mono <|
      hK.closure_subset_measurableSet (measurableSet_toMeasurable ..) (subset_toMeasurable ..)
    _ = μ K := measure_toMeasurable ..

@[measurability]
theorem measurableSet_closure : MeasurableSet (closure s) :=
  isClosed_closure.measurableSet
#align measurable_set_closure measurableSet_closure

theorem measurable_of_isOpen {f : δ → γ} (hf : ∀ s, IsOpen s → MeasurableSet (f ⁻¹' s)) :
    Measurable f := by
  rw [‹BorelSpace γ›.measurable_eq]
  exact measurable_generateFrom hf
#align measurable_of_is_open measurable_of_isOpen

theorem measurable_of_isClosed {f : δ → γ} (hf : ∀ s, IsClosed s → MeasurableSet (f ⁻¹' s)) :
    Measurable f := by
  apply measurable_of_isOpen; intro s hs
  rw [← MeasurableSet.compl_iff, ← preimage_compl]; apply hf; rw [isClosed_compl_iff]; exact hs
#align measurable_of_is_closed measurable_of_isClosed

theorem measurable_of_isClosed' {f : δ → γ}
    (hf : ∀ s, IsClosed s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)) : Measurable f := by
  apply measurable_of_isClosed; intro s hs
  rcases eq_empty_or_nonempty s with h1 | h1
  · simp [h1]
  by_cases h2 : s = univ
  · simp [h2]
  exact hf s hs h1 h2
#align measurable_of_is_closed' measurable_of_isClosed'

instance nhds_isMeasurablyGenerated (a : α) : (𝓝 a).IsMeasurablyGenerated := by
  rw [nhds, iInf_subtype']
  refine' @Filter.iInf_isMeasurablyGenerated α _ _ _ fun i => _
  exact i.2.2.measurableSet.principal_isMeasurablyGenerated
#align nhds_is_measurably_generated nhds_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`.
-/
theorem MeasurableSet.nhdsWithin_isMeasurablyGenerated {s : Set α} (hs : MeasurableSet s) (a : α) :
    (𝓝[s] a).IsMeasurablyGenerated :=
  haveI := hs.principal_isMeasurablyGenerated
  Filter.inf_isMeasurablyGenerated _ _
#align measurable_set.nhds_within_is_measurably_generated MeasurableSet.nhdsWithin_isMeasurablyGenerated

-- see Note [lower instance priority]
instance (priority := 100) OpensMeasurableSpace.toMeasurableSingletonClass [T1Space α] :
    MeasurableSingletonClass α :=
  ⟨fun _ => isClosed_singleton.measurableSet⟩
#align opens_measurable_space.to_measurable_singleton_class OpensMeasurableSpace.toMeasurableSingletonClass

instance Pi.opensMeasurableSpace {ι : Type*} {π : ι → Type*} [Countable ι]
    [t' : ∀ i, TopologicalSpace (π i)] [∀ i, MeasurableSpace (π i)]
    [∀ i, SecondCountableTopology (π i)] [∀ i, OpensMeasurableSpace (π i)] :
    OpensMeasurableSpace (∀ i, π i) := by
  constructor
  have : Pi.topologicalSpace = .generateFrom { t | ∃ (s : ∀ a, Set (π a)) (i : Finset ι),
      (∀ a ∈ i, s a ∈ countableBasis (π a)) ∧ t = pi (↑i) s } := by
    rw [funext fun a => @eq_generateFrom_countableBasis (π a) _ _, pi_generateFrom_eq]
  rw [borel_eq_generateFrom_of_subbasis this]
  apply generateFrom_le
  rintro _ ⟨s, i, hi, rfl⟩
  refine' MeasurableSet.pi i.countable_toSet fun a ha => IsOpen.measurableSet _
  rw [eq_generateFrom_countableBasis (π a)]
  exact .basic _ (hi a ha)
#align pi.opens_measurable_space Pi.opensMeasurableSpace

/-- 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. -/
class SecondCountableTopologyEither (α β : Type*) [TopologicalSpace α] [TopologicalSpace β] :
  Prop where
  /-- The projection out of `SecondCountableTopologyEither` -/
  out : SecondCountableTopology α ∨ SecondCountableTopology β
#align second_countable_topology_either SecondCountableTopologyEither

instance (priority := 100) secondCountableTopologyEither_of_left (α β : Type*) [TopologicalSpace α]
    [TopologicalSpace β] [SecondCountableTopology α] : SecondCountableTopologyEither α β where
  out := Or.inl (by infer_instance)
#align second_countable_topology_either_of_left secondCountableTopologyEither_of_left

instance (priority := 100) secondCountableTopologyEither_of_right (α β : Type*)
    [TopologicalSpace α] [TopologicalSpace β] [SecondCountableTopology β] :
    SecondCountableTopologyEither α β where
  out := Or.inr (by infer_instance)
#align second_countable_topology_either_of_right secondCountableTopologyEither_of_right

/-- If either `α` or `β` has second-countable topology, then the open sets in `α × β` belong to the
product sigma-algebra. -/
instance Prod.opensMeasurableSpace [h : SecondCountableTopologyEither α β] :
    OpensMeasurableSpace (α × β) := by
  apply opensMeasurableSpace_iff_forall_measurableSet.2 (fun s hs ↦ ?_)
  rcases h.out with hα|hβ
  · let F : Set α → Set β := fun a ↦ {y | ∃ b, IsOpen b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
    have A : ∀ a, IsOpen (F a) := by
      intro a
      apply isOpen_iff_forall_mem_open.2
      rintro y ⟨b, b_open, yb, hb⟩
      exact ⟨b, fun z zb ↦ ⟨b, b_open, zb, hb⟩, b_open, yb⟩
    have : s = ⋃ a ∈ countableBasis α, a ×ˢ F a := by
      apply Subset.antisymm
      · rintro ⟨y1, y2⟩ hy
        rcases isOpen_prod_iff.1 hs y1 y2 hy with ⟨u, v, u_open, v_open, yu, yv, huv⟩
        obtain ⟨a, ha, ya, au⟩ : ∃ a ∈ countableBasis α, y1 ∈ a ∧ a ⊆ u :=
          IsTopologicalBasis.exists_subset_of_mem_open (isBasis_countableBasis α) yu u_open
        simp only [mem_iUnion, mem_prod, mem_setOf_eq, exists_and_left, exists_prop]
        exact ⟨a, ya, ha, v, v_open, yv, (Set.prod_mono_left au).trans huv⟩
      · rintro ⟨y1, y2⟩ hy
        simp only [mem_iUnion, mem_prod, mem_setOf_eq, exists_and_left, exists_prop] at hy
        rcases hy with ⟨a, ya, -, b, -, yb, hb⟩
        exact hb (mem_prod.2 ⟨ya, yb⟩)
    rw [this]
    apply MeasurableSet.biUnion (countable_countableBasis α) (fun a ha ↦ ?_)
    exact (isOpen_of_mem_countableBasis ha).measurableSet.prod (A a).measurableSet
  · let F : Set β → Set α := fun a ↦ {y | ∃ b, IsOpen b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
    have A : ∀ a, IsOpen (F a) := by
      intro a
      apply isOpen_iff_forall_mem_open.2
      rintro y ⟨b, b_open, yb, hb⟩
      exact ⟨b, fun z zb ↦ ⟨b, b_open, zb, hb⟩, b_open, yb⟩
    have : s = ⋃ a ∈ countableBasis β, F a ×ˢ a := by
      apply Subset.antisymm
      · rintro ⟨y1, y2⟩ hy
        rcases isOpen_prod_iff.1 hs y1 y2 hy with ⟨u, v, u_open, v_open, yu, yv, huv⟩
        obtain ⟨a, ha, ya, au⟩ : ∃ a ∈ countableBasis β, y2 ∈ a ∧ a ⊆ v :=
          IsTopologicalBasis.exists_subset_of_mem_open (isBasis_countableBasis β) yv v_open
        simp only [mem_iUnion, mem_prod, mem_setOf_eq, exists_and_left, exists_prop]
        exact ⟨a, ⟨u, u_open, yu, (Set.prod_mono_right au).trans huv⟩, ha, ya⟩
      · rintro ⟨y1, y2⟩ hy
        simp only [mem_iUnion, mem_prod, mem_setOf_eq, exists_and_left, exists_prop] at hy
        rcases hy with ⟨a, ⟨b, -, yb, hb⟩, -, ya⟩
        exact hb (mem_prod.2 ⟨yb, ya⟩)
    rw [this]
    apply MeasurableSet.biUnion (countable_countableBasis β) (fun a ha ↦ ?_)
    exact (A a).measurableSet.prod (isOpen_of_mem_countableBasis ha).measurableSet

variable {α' : Type*} [TopologicalSpace α'] [MeasurableSpace α']

theorem interior_ae_eq_of_null_frontier {μ : Measure α'} {s : Set α'} (h : μ (frontier s) = 0) :
    interior s =ᵐ[μ] s :=
  interior_subset.eventuallyLE.antisymm <| subset_closure.eventuallyLE.trans (ae_le_set.2 h)
#align interior_ae_eq_of_null_frontier interior_ae_eq_of_null_frontier

theorem measure_interior_of_null_frontier {μ : Measure α'} {s : Set α'} (h : μ (frontier s) = 0) :
    μ (interior s) = μ s :=
  measure_congr (interior_ae_eq_of_null_frontier h)
#align measure_interior_of_null_frontier measure_interior_of_null_frontier

theorem nullMeasurableSet_of_null_frontier {s : Set α} {μ : Measure α} (h : μ (frontier s) = 0) :
    NullMeasurableSet s μ :=
  ⟨interior s, isOpen_interior.measurableSet, (interior_ae_eq_of_null_frontier h).symm⟩
#align null_measurable_set_of_null_frontier nullMeasurableSet_of_null_frontier

theorem closure_ae_eq_of_null_frontier {μ : Measure α'} {s : Set α'} (h : μ (frontier s) = 0) :
    closure s =ᵐ[μ] s :=
  ((ae_le_set.2 h).trans interior_subset.eventuallyLE).antisymm <| subset_closure.eventuallyLE
#align closure_ae_eq_of_null_frontier closure_ae_eq_of_null_frontier

theorem measure_closure_of_null_frontier {μ : Measure α'} {s : Set α'} (h : μ (frontier s) = 0) :
    μ (closure s) = μ s :=
  measure_congr (closure_ae_eq_of_null_frontier h)
#align measure_closure_of_null_frontier measure_closure_of_null_frontier

section Preorder

variable [Preorder α] [OrderClosedTopology α] {a b x : α}

@[simp, measurability]
theorem measurableSet_Ici : MeasurableSet (Ici a) :=
  isClosed_Ici.measurableSet
#align measurable_set_Ici measurableSet_Ici

@[simp, measurability]
theorem measurableSet_Iic : MeasurableSet (Iic a) :=
  isClosed_Iic.measurableSet
#align measurable_set_Iic measurableSet_Iic

@[simp, measurability]
theorem measurableSet_Icc : MeasurableSet (Icc a b) :=
  isClosed_Icc.measurableSet
#align measurable_set_Icc measurableSet_Icc

instance nhdsWithin_Ici_isMeasurablyGenerated : (𝓝[Ici b] a).IsMeasurablyGenerated :=
  measurableSet_Ici.nhdsWithin_isMeasurablyGenerated _
#align nhds_within_Ici_is_measurably_generated nhdsWithin_Ici_isMeasurablyGenerated

instance nhdsWithin_Iic_isMeasurablyGenerated : (𝓝[Iic b] a).IsMeasurablyGenerated :=
  measurableSet_Iic.nhdsWithin_isMeasurablyGenerated _
#align nhds_within_Iic_is_measurably_generated nhdsWithin_Iic_isMeasurablyGenerated

instance nhdsWithin_Icc_isMeasurablyGenerated : IsMeasurablyGenerated (𝓝[Icc a b] x) := by
  rw [← Ici_inter_Iic, nhdsWithin_inter]
  infer_instance
#align nhds_within_Icc_is_measurably_generated nhdsWithin_Icc_isMeasurablyGenerated

instance atTop_isMeasurablyGenerated : (Filter.atTop : Filter α).IsMeasurablyGenerated :=
  @Filter.iInf_isMeasurablyGenerated _ _ _ _ fun a =>
    (measurableSet_Ici : MeasurableSet (Ici a)).principal_isMeasurablyGenerated
#align at_top_is_measurably_generated atTop_isMeasurablyGenerated

instance atBot_isMeasurablyGenerated : (Filter.atBot : Filter α).IsMeasurablyGenerated :=
  @Filter.iInf_isMeasurablyGenerated _ _ _ _ fun a =>
    (measurableSet_Iic : MeasurableSet (Iic a)).principal_isMeasurablyGenerated
#align at_bot_is_measurably_generated atBot_isMeasurablyGenerated

instance [R1Space α] : IsMeasurablyGenerated (cocompact α) where
  exists_measurable_subset := by
    intro _ hs
    obtain ⟨t, ht, hts⟩ := mem_cocompact.mp hs
    exact ⟨(closure t)ᶜ, ht.closure.compl_mem_cocompact, isClosed_closure.measurableSet.compl,
      (compl_subset_compl.2 subset_closure).trans hts⟩

end Preorder

section PartialOrder

variable [PartialOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {a b : α}

@[measurability]
theorem measurableSet_le' : MeasurableSet { p : α × α | p.1 ≤ p.2 } :=
  OrderClosedTopology.isClosed_le'.measurableSet
#align measurable_set_le' measurableSet_le'

@[measurability]
theorem measurableSet_le {f g : δ → α} (hf : Measurable f) (hg : Measurable g) :
    MeasurableSet { a | f a ≤ g a } :=
  hf.prod_mk hg measurableSet_le'
#align measurable_set_le measurableSet_le

end PartialOrder

section LinearOrder

variable [LinearOrder α] [OrderClosedTopology α] {a b x : α}

-- we open this locale only here to avoid issues with list being treated as intervals above
open Interval

@[simp, measurability]
theorem measurableSet_Iio : MeasurableSet (Iio a) :=
  isOpen_Iio.measurableSet
#align measurable_set_Iio measurableSet_Iio

@[simp, measurability]
theorem measurableSet_Ioi : MeasurableSet (Ioi a) :=
  isOpen_Ioi.measurableSet
#align measurable_set_Ioi measurableSet_Ioi

@[simp, measurability]
theorem measurableSet_Ioo : MeasurableSet (Ioo a b) :=
  isOpen_Ioo.measurableSet
#align measurable_set_Ioo measurableSet_Ioo

@[simp, measurability]
theorem measurableSet_Ioc : MeasurableSet (Ioc a b) :=
  measurableSet_Ioi.inter measurableSet_Iic
#align measurable_set_Ioc measurableSet_Ioc

@[simp, measurability]
theorem measurableSet_Ico : MeasurableSet (Ico a b) :=
  measurableSet_Ici.inter measurableSet_Iio
#align measurable_set_Ico measurableSet_Ico

instance nhdsWithin_Ioi_isMeasurablyGenerated : (𝓝[Ioi b] a).IsMeasurablyGenerated :=
  measurableSet_Ioi.nhdsWithin_isMeasurablyGenerated _
#align nhds_within_Ioi_is_measurably_generated nhdsWithin_Ioi_isMeasurablyGenerated

instance nhdsWithin_Iio_isMeasurablyGenerated : (𝓝[Iio b] a).IsMeasurablyGenerated :=
  measurableSet_Iio.nhdsWithin_isMeasurablyGenerated _
#align nhds_within_Iio_is_measurably_generated nhdsWithin_Iio_isMeasurablyGenerated

instance nhdsWithin_uIcc_isMeasurablyGenerated : IsMeasurablyGenerated (𝓝[[[a, b]]] x) :=
  nhdsWithin_Icc_isMeasurablyGenerated
#align nhds_within_uIcc_is_measurably_generated nhdsWithin_uIcc_isMeasurablyGenerated

@[measurability]
theorem measurableSet_lt' [SecondCountableTopology α] : MeasurableSet { p : α × α | p.1 < p.2 } :=
  (isOpen_lt continuous_fst continuous_snd).measurableSet
#align measurable_set_lt' measurableSet_lt'

@[measurability]
theorem measurableSet_lt [SecondCountableTopology α] {f g : δ → α} (hf : Measurable f)
    (hg : Measurable g) : MeasurableSet { a | f a < g a } :=
  hf.prod_mk hg measurableSet_lt'
#align measurable_set_lt measurableSet_lt

theorem nullMeasurableSet_lt [SecondCountableTopology α] {μ : Measure δ} {f g : δ → α}
    (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : NullMeasurableSet { a | f a < g a } μ :=
  (hf.prod_mk hg).nullMeasurable measurableSet_lt'
#align null_measurable_set_lt nullMeasurableSet_lt

theorem nullMeasurableSet_lt' [SecondCountableTopology α] {μ : Measure (α × α)} :
    NullMeasurableSet { p : α × α | p.1 < p.2 } μ :=
  measurableSet_lt'.nullMeasurableSet

theorem nullMeasurableSet_le [SecondCountableTopology α] {μ : Measure δ}
    {f g : δ → α} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    NullMeasurableSet { a | f a ≤ g a } μ :=
  (hf.prod_mk hg).nullMeasurable measurableSet_le'

theorem Set.OrdConnected.measurableSet (h : OrdConnected s) : MeasurableSet s := by
  let u := ⋃ (x ∈ s) (y ∈ s), Ioo x y
  have huopen : IsOpen u := isOpen_biUnion fun _ _ => isOpen_biUnion fun _ _ => isOpen_Ioo
  have humeas : MeasurableSet u := huopen.measurableSet
  have hfinite : (s \ u).Finite := s.finite_diff_iUnion_Ioo
  have : u ⊆ s := iUnion₂_subset fun x hx => iUnion₂_subset fun y hy =>
    Ioo_subset_Icc_self.trans (h.out hx hy)
  rw [← union_diff_cancel this]
  exact humeas.union hfinite.measurableSet
#align set.ord_connected.measurable_set Set.OrdConnected.measurableSet

theorem IsPreconnected.measurableSet (h : IsPreconnected s) : MeasurableSet s :=
  h.ordConnected.measurableSet
#align is_preconnected.measurable_set IsPreconnected.measurableSet

theorem generateFrom_Ico_mem_le_borel {α : Type*} [TopologicalSpace α] [LinearOrder α]
    [OrderClosedTopology α] (s t : Set α) :
    MeasurableSpace.generateFrom { S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ico l u = S }
      ≤ borel α := by
  apply generateFrom_le
  borelize α
  rintro _ ⟨a, -, b, -, -, rfl⟩
  exact measurableSet_Ico
#align generate_from_Ico_mem_le_borel generateFrom_Ico_mem_le_borel

theorem Dense.borel_eq_generateFrom_Ico_mem_aux {α : Type*} [TopologicalSpace α] [LinearOrder α]
    [OrderTopology α] [SecondCountableTopology α] {s : Set α} (hd : Dense s)
    (hbot : ∀ x, IsBot x → x ∈ s) (hIoo : ∀ x y : α, x < y → Ioo x y = ∅ → y ∈ s) :
    borel α = .generateFrom { S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S } := by
  set S : Set (Set α) := { S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S }
  refine' le_antisymm _ (generateFrom_Ico_mem_le_borel _ _)
  letI : MeasurableSpace α := generateFrom S
  rw [borel_eq_generateFrom_Iio]
  refine' generateFrom_le (forall_mem_range.2 fun a => _)
  rcases hd.exists_countable_dense_subset_bot_top with ⟨t, hts, hc, htd, htb, -⟩
  by_cases ha : ∀ b < a, (Ioo b a).Nonempty
  · convert_to MeasurableSet (⋃ (l ∈ t) (u ∈ t) (_ : l < u) (_ : u ≤ a), Ico l u)
    · ext y
      simp only [mem_iUnion, mem_Iio, mem_Ico]
      constructor
      · intro hy
        rcases htd.exists_le' (fun b hb => htb _ hb (hbot b hb)) y with ⟨l, hlt, hly⟩
        rcases htd.exists_mem_open isOpen_Ioo (ha y hy) with ⟨u, hut, hyu, hua⟩
        exact ⟨l, hlt, u, hut, hly.trans_lt hyu, hua.le, hly, hyu⟩
      · rintro ⟨l, -, u, -, -, hua, -, hyu⟩
        exact hyu.trans_le hua
    · refine' MeasurableSet.biUnion hc fun a ha => MeasurableSet.biUnion hc fun b hb => _
      refine' MeasurableSet.iUnion fun hab => MeasurableSet.iUnion fun _ => _
      exact .basic _ ⟨a, hts ha, b, hts hb, hab, mem_singleton _⟩
  · simp only [not_forall, not_nonempty_iff_eq_empty] at ha
    replace ha : a ∈ s := hIoo ha.choose a ha.choose_spec.fst ha.choose_spec.snd
    convert_to MeasurableSet (⋃ (l ∈ t) (_ : l < a), Ico l a)
    · symm
      simp only [← Ici_inter_Iio, ← iUnion_inter, inter_eq_right, subset_def, mem_iUnion,
        mem_Ici, mem_Iio]
      intro x hx
      rcases htd.exists_le' (fun b hb => htb _ hb (hbot b hb)) x with ⟨z, hzt, hzx⟩
      exact ⟨z, hzt, hzx.trans_lt hx, hzx⟩
    · refine' .biUnion hc fun x hx => MeasurableSet.iUnion fun hlt => _
      exact .basic _ ⟨x, hts hx, a, ha, hlt, mem_singleton _⟩
#align dense.borel_eq_generate_from_Ico_mem_aux Dense.borel_eq_generateFrom_Ico_mem_aux

theorem Dense.borel_eq_generateFrom_Ico_mem {α : Type*} [TopologicalSpace α] [LinearOrder α]
    [OrderTopology α] [SecondCountableTopology α] [DenselyOrdered α] [NoMinOrder α] {s : Set α}
    (hd : Dense s) :
    borel α = .generateFrom { S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S } :=
  hd.borel_eq_generateFrom_Ico_mem_aux (by simp) fun x y hxy H =>
    ((nonempty_Ioo.2 hxy).ne_empty H).elim
#align dense.borel_eq_generate_from_Ico_mem Dense.borel_eq_generateFrom_Ico_mem

theorem borel_eq_generateFrom_Ico (α : Type*) [TopologicalSpace α] [SecondCountableTopology α]
    [LinearOrder α] [OrderTopology α] :
    borel α = .generateFrom { S : Set α | ∃ (l u : α), l < u ∧ Ico l u = S } := by
  simpa only [exists_prop, mem_univ, true_and_iff] using
    (@dense_univ α _).borel_eq_generateFrom_Ico_mem_aux (fun _ _ => mem_univ _) fun _ _ _ _ =>
      mem_univ _
#align borel_eq_generate_from_Ico borel_eq_generateFrom_Ico

theorem Dense.borel_eq_generateFrom_Ioc_mem_aux {α : Type*} [TopologicalSpace α] [LinearOrder α]
    [OrderTopology α] [SecondCountableTopology α] {s : Set α} (hd : Dense s)
    (hbot : ∀ x, IsTop x → x ∈ s) (hIoo : ∀ x y : α, x < y → Ioo x y = ∅ → x ∈ s) :
    borel α = .generateFrom { S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S } := by
  convert hd.orderDual.borel_eq_generateFrom_Ico_mem_aux hbot fun x y hlt he => hIoo y x hlt _
    using 2
  · ext s
    constructor <;> rintro ⟨l, hl, u, hu, hlt, rfl⟩
    exacts [⟨u, hu, l, hl, hlt, dual_Ico⟩, ⟨u, hu, l, hl, hlt, dual_Ioc⟩]
  · erw [dual_Ioo]
    exact he
#align dense.borel_eq_generate_from_Ioc_mem_aux Dense.borel_eq_generateFrom_Ioc_mem_aux

theorem Dense.borel_eq_generateFrom_Ioc_mem {α : Type*} [TopologicalSpace α] [LinearOrder α]
    [OrderTopology α] [SecondCountableTopology α] [DenselyOrdered α] [NoMaxOrder α] {s : Set α}
    (hd : Dense s) :
    borel α = .generateFrom { S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S } :=
  hd.borel_eq_generateFrom_Ioc_mem_aux (by simp) fun x y hxy H =>
    ((nonempty_Ioo.2 hxy).ne_empty H).elim
#align dense.borel_eq_generate_from_Ioc_mem Dense.borel_eq_generateFrom_Ioc_mem

theorem borel_eq_generateFrom_Ioc (α : Type*) [TopologicalSpace α] [SecondCountableTopology α]
    [LinearOrder α] [OrderTopology α] :
    borel α = .generateFrom { S : Set α | ∃ l u, l < u ∧ Ioc l u = S } := by
  simpa only [exists_prop, mem_univ, true_and_iff] using
    (@dense_univ α _).borel_eq_generateFrom_Ioc_mem_aux (fun _ _ => mem_univ _) fun _ _ _ _ =>
      mem_univ _
#align borel_eq_generate_from_Ioc borel_eq_generateFrom_Ioc

namespace MeasureTheory.Measure

/-- 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 ext_of_Ico_finite {α : Type*} [TopologicalSpace α] {m : MeasurableSpace α}
    [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] (μ ν : Measure α)
    [IsFiniteMeasure μ] (hμν : μ univ = ν univ) (h : ∀ ⦃a b⦄, a < b → μ (Ico a b) = ν (Ico a b)) :
    μ = ν := by
  refine'
    ext_of_generate_finite _ (BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Ico α))
      (isPiSystem_Ico (id : α → α) id) _ hμν
  · rintro - ⟨a, b, hlt, rfl⟩
    exact h hlt
#align measure_theory.measure.ext_of_Ico_finite MeasureTheory.Measure.ext_of_Ico_finite

/-- 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 ext_of_Ioc_finite {α : Type*} [TopologicalSpace α] {m : MeasurableSpace α}
    [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] (μ ν : Measure α)
    [IsFiniteMeasure μ] (hμν : μ univ = ν univ) (h : ∀ ⦃a b⦄, a < b → μ (Ioc a b) = ν (Ioc a b)) :
    μ = ν := by
  refine' @ext_of_Ico_finite αᵒᵈ _ _ _ _ _ ‹_› μ ν _ hμν fun a b hab => _
  erw [dual_Ico (α := α)]
  exact h hab
#align measure_theory.measure.ext_of_Ioc_finite MeasureTheory.Measure.ext_of_Ioc_finite

/-- Two measures which are finite on closed-open intervals are equal if they agree on all
closed-open intervals. -/
theorem ext_of_Ico' {α : Type*} [TopologicalSpace α] {m : MeasurableSpace α}
    [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] [NoMaxOrder α]
    (μ ν : Measure α) (hμ : ∀ ⦃a b⦄, a < b → μ (Ico a b) ≠ ∞)
    (h : ∀ ⦃a b⦄, a < b → μ (Ico a b) = ν (Ico a b)) : μ = ν := by
  rcases exists_countable_dense_bot_top α with ⟨s, hsc, hsd, hsb, _⟩
  have : (⋃ (l ∈ s) (u ∈ s) (_ : l < u), {Ico l u} : Set (Set α)).Countable :=
    hsc.biUnion fun l _ => hsc.biUnion fun u _ => countable_iUnion fun _ => countable_singleton _
  simp only [← setOf_eq_eq_singleton, ← setOf_exists] at this
  refine'
    Measure.ext_of_generateFrom_of_cover_subset
      (BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Ico α)) (isPiSystem_Ico id id) _ this
      _ _ _
  · rintro _ ⟨l, -, u, -, h, rfl⟩
    exact ⟨l, u, h, rfl⟩
  · refine' sUnion_eq_univ_iff.2 fun x => _
    rcases hsd.exists_le' hsb x with ⟨l, hls, hlx⟩
    rcases hsd.exists_gt x with ⟨u, hus, hxu⟩
    exact ⟨_, ⟨l, hls, u, hus, hlx.trans_lt hxu, rfl⟩, hlx, hxu⟩
  · rintro _ ⟨l, -, u, -, hlt, rfl⟩
    exact hμ hlt
  · rintro _ ⟨l, u, hlt, rfl⟩
    exact h hlt
#align measure_theory.measure.ext_of_Ico' MeasureTheory.Measure.ext_of_Ico'

/-- Two measures which are finite on closed-open intervals are equal if they agree on all
open-closed intervals. -/
theorem ext_of_Ioc' {α : Type*} [TopologicalSpace α] {m : MeasurableSpace α}
    [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] [NoMinOrder α]
    (μ ν : Measure α) (hμ : ∀ ⦃a b⦄, a < b → μ (Ioc a b) ≠ ∞)
    (h : ∀ ⦃a b⦄, a < b → μ (Ioc a b) = ν (Ioc a b)) : μ = ν := by
  refine' @ext_of_Ico' αᵒᵈ _ _ _ _ _ ‹_› _ μ ν _ _ <;> intro a b hab <;> erw [dual_Ico (α := α)]
  exacts [hμ hab, h hab]
#align measure_theory.measure.ext_of_Ioc' MeasureTheory.Measure.ext_of_Ioc'

/-- Two measures which are finite on closed-open intervals are equal if they agree on all
closed-open intervals. -/
theorem ext_of_Ico {α : Type*} [TopologicalSpace α] {_m : MeasurableSpace α}
    [SecondCountableTopology α] [ConditionallyCompleteLinearOrder α] [OrderTopology α]
    [BorelSpace α] [NoMaxOrder α] (μ ν : Measure α) [IsLocallyFiniteMeasure μ]
    (h : ∀ ⦃a b⦄, a < b → μ (Ico a b) = ν (Ico a b)) : μ = ν :=
  μ.ext_of_Ico' ν (fun _ _ _ => measure_Ico_lt_top.ne) h
#align measure_theory.measure.ext_of_Ico MeasureTheory.Measure.ext_of_Ico

/-- Two measures which are finite on closed-open intervals are equal if they agree on all
open-closed intervals. -/
theorem ext_of_Ioc {α : Type*} [TopologicalSpace α] {_m : MeasurableSpace α}
    [SecondCountableTopology α] [ConditionallyCompleteLinearOrder α] [OrderTopology α]
    [BorelSpace α] [NoMinOrder α] (μ ν : Measure α) [IsLocallyFiniteMeasure μ]
    (h : ∀ ⦃a b⦄, a < b → μ (Ioc a b) = ν (Ioc a b)) : μ = ν :=
  μ.ext_of_Ioc' ν (fun _ _ _ => measure_Ioc_lt_top.ne) h
#align measure_theory.measure.ext_of_Ioc MeasureTheory.Measure.ext_of_Ioc

/-- Two finite measures on a Borel space are equal if they agree on all left-infinite right-closed
intervals. -/
theorem ext_of_Iic {α : Type*} [TopologicalSpace α] {m : MeasurableSpace α}
    [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] (μ ν : Measure α)
    [IsFiniteMeasure μ] (h : ∀ a, μ (Iic a) = ν (Iic a)) : μ = ν := by
  refine' ext_of_Ioc_finite μ ν _ fun a b hlt => _
  · rcases exists_countable_dense_bot_top α with ⟨s, hsc, hsd, -, hst⟩
    have : DirectedOn (· ≤ ·) s := directedOn_iff_directed.2 (Subtype.mono_coe _).directed_le
    simp only [← biSup_measure_Iic hsc (hsd.exists_ge' hst) this, h]
  rw [← Iic_diff_Iic, measure_diff (Iic_subset_Iic.2 hlt.le) measurableSet_Iic,
    measure_diff (Iic_subset_Iic.2 hlt.le) measurableSet_Iic, h a, h b]
  · rw [← h a]
    exact (measure_lt_top μ _).ne
  · exact (measure_lt_top μ _).ne
#align measure_theory.measure.ext_of_Iic MeasureTheory.Measure.ext_of_Iic

/-- Two finite measures on a Borel space are equal if they agree on all left-closed right-infinite
intervals. -/
theorem ext_of_Ici {α : Type*} [TopologicalSpace α] {m : MeasurableSpace α}
    [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] (μ ν : Measure α)
    [IsFiniteMeasure μ] (h : ∀ a, μ (Ici a) = ν (Ici a)) : μ = ν :=
  @ext_of_Iic αᵒᵈ _ _ _ _ _ ‹_› _ _ _ h
#align measure_theory.measure.ext_of_Ici MeasureTheory.Measure.ext_of_Ici

end MeasureTheory.Measure

end LinearOrder

section LinearOrder

variable [LinearOrder α] [OrderClosedTopology α] {a b : α}

@[measurability]
theorem measurableSet_uIcc : MeasurableSet (uIcc a b) :=
  measurableSet_Icc
#align measurable_set_uIcc measurableSet_uIcc

@[measurability]
theorem measurableSet_uIoc : MeasurableSet (uIoc a b) :=
  measurableSet_Ioc
#align measurable_set_uIoc measurableSet_uIoc

variable [SecondCountableTopology α]

@[measurability]
theorem Measurable.max {f g : δ → α} (hf : Measurable f) (hg : Measurable g) :
    Measurable fun a => max (f a) (g a) := by
  simpa only [max_def'] using hf.piecewise (measurableSet_le hg hf) hg
#align measurable.max Measurable.max

@[measurability]
nonrec theorem AEMeasurable.max {f g : δ → α} {μ : Measure δ} (hf : AEMeasurable f μ)
    (hg : AEMeasurable g μ) : AEMeasurable (fun a => max (f a) (g a)) μ :=
  ⟨fun a => max (hf.mk f a) (hg.mk g a), hf.measurable_mk.max hg.measurable_mk,
    EventuallyEq.comp₂ hf.ae_eq_mk _ hg.ae_eq_mk⟩
#align ae_measurable.max AEMeasurable.max

@[measurability]
theorem Measurable.min {f g : δ → α} (hf : Measurable f) (hg : Measurable g) :
    Measurable fun a => min (f a) (g a) := by
  simpa only [min_def] using hf.piecewise (measurableSet_le hf hg) hg
#align measurable.min Measurable.min

@[measurability]
nonrec theorem AEMeasurable.min {f g : δ → α} {μ : Measure δ} (hf : AEMeasurable f μ)
    (hg : AEMeasurable g μ) : AEMeasurable (fun a => min (f a) (g a)) μ :=
  ⟨fun a => min (hf.mk f a) (hg.mk g a), hf.measurable_mk.min hg.measurable_mk,
    EventuallyEq.comp₂ hf.ae_eq_mk _ hg.ae_eq_mk⟩
#align ae_measurable.min AEMeasurable.min

end LinearOrder

/-- A continuous function from an `OpensMeasurableSpace` to a `BorelSpace`
is measurable. -/
theorem Continuous.measurable {f : α → γ} (hf : Continuous f) : Measurable f :=
  hf.borel_measurable.mono OpensMeasurableSpace.borel_le (le_of_eq <| BorelSpace.measurable_eq)
#align continuous.measurable Continuous.measurable

/-- A continuous function from an `OpensMeasurableSpace` to a `BorelSpace`
is ae-measurable. -/
theorem Continuous.aemeasurable {f : α → γ} (h : Continuous f) {μ : Measure α} : AEMeasurable f μ :=
  h.measurable.aemeasurable
#align continuous.ae_measurable Continuous.aemeasurable

theorem ClosedEmbedding.measurable {f : α → γ} (hf : ClosedEmbedding f) : Measurable f :=
  hf.continuous.measurable
#align closed_embedding.measurable ClosedEmbedding.measurable

/-- If a function is defined piecewise in terms of functions which are continuous on their
respective pieces, then it is measurable. -/
theorem ContinuousOn.measurable_piecewise {f g : α → γ} {s : Set α} [∀ j : α, Decidable (j ∈ s)]
    (hf : ContinuousOn f s) (hg : ContinuousOn g sᶜ) (hs : MeasurableSet s) :
    Measurable (s.piecewise f g) := by
  refine' measurable_of_isOpen fun t ht => _
  rw [piecewise_preimage, Set.ite]
  apply MeasurableSet.union
  · rcases _root_.continuousOn_iff'.1 hf t ht with ⟨u, u_open, hu⟩
    rw [hu]
    exact u_open.measurableSet.inter hs
  · rcases _root_.continuousOn_iff'.1 hg t ht with ⟨u, u_open, hu⟩
    rw [diff_eq_compl_inter, inter_comm, hu]
    exact u_open.measurableSet.inter hs.compl
#align continuous_on.measurable_piecewise ContinuousOn.measurable_piecewise

@[to_additive]
instance (priority := 100) ContinuousMul.measurableMul [Mul γ] [ContinuousMul γ] :
    MeasurableMul γ where
  measurable_const_mul _ := (continuous_const.mul continuous_id).measurable
  measurable_mul_const _ := (continuous_id.mul continuous_const).measurable
#align has_continuous_mul.has_measurable_mul ContinuousMul.measurableMul
#align has_continuous_add.has_measurable_add ContinuousAdd.measurableAdd

instance (priority := 100) ContinuousSub.measurableSub [Sub γ] [ContinuousSub γ] :
    MeasurableSub γ where
  measurable_const_sub _ := (continuous_const.sub continuous_id).measurable
  measurable_sub_const _ := (continuous_id.sub continuous_const).measurable
#align has_continuous_sub.has_measurable_sub ContinuousSub.measurableSub

@[to_additive]
instance (priority := 100) TopologicalGroup.measurableInv [Group γ] [TopologicalGroup γ] :
    MeasurableInv γ :=
  ⟨continuous_inv.measurable⟩
#align topological_group.has_measurable_inv TopologicalGroup.measurableInv
#align topological_add_group.has_measurable_neg TopologicalAddGroup.measurableNeg

instance (priority := 100) ContinuousSMul.measurableSMul {M α} [TopologicalSpace M]
    [TopologicalSpace α] [MeasurableSpace M] [MeasurableSpace α] [OpensMeasurableSpace M]
    [BorelSpace α] [SMul M α] [ContinuousSMul M α] : MeasurableSMul M α :=
  ⟨fun _ => (continuous_const_smul _).measurable, fun _ =>
    (continuous_id.smul continuous_const).measurable⟩
#align has_continuous_smul.has_measurable_smul ContinuousSMul.measurableSMul

section Lattice

instance (priority := 100) ContinuousSup.measurableSup [Sup γ] [ContinuousSup γ] :
    MeasurableSup γ where
  measurable_const_sup _ := (continuous_const.sup continuous_id).measurable
  measurable_sup_const _ := (continuous_id.sup continuous_const).measurable
#align has_continuous_sup.has_measurable_sup ContinuousSup.measurableSup

instance (priority := 100) ContinuousSup.measurableSup₂ [SecondCountableTopology γ] [Sup γ]
    [ContinuousSup γ] : MeasurableSup₂ γ :=
  ⟨continuous_sup.measurable⟩
#align has_continuous_sup.has_measurable_sup₂ ContinuousSup.measurableSup₂

instance (priority := 100) ContinuousInf.measurableInf [Inf γ] [ContinuousInf γ] :
    MeasurableInf γ where
  measurable_const_inf _ := (continuous_const.inf continuous_id).measurable
  measurable_inf_const _ := (continuous_id.inf continuous_const).measurable
#align has_continuous_inf.has_measurable_inf ContinuousInf.measurableInf

instance (priority := 100) ContinuousInf.measurableInf₂ [SecondCountableTopology γ] [Inf γ]
    [ContinuousInf γ] : MeasurableInf₂ γ :=
  ⟨continuous_inf.measurable⟩
#align has_continuous_inf.has_measurable_inf₂ ContinuousInf.measurableInf₂

end Lattice

section Homeomorph

@[measurability]
protected theorem Homeomorph.measurable (h : α ≃ₜ γ) : Measurable h :=
  h.continuous.measurable
#align homeomorph.measurable Homeomorph.measurable

/-- A homeomorphism between two Borel spaces is a measurable equivalence.-/
def Homeomorph.toMeasurableEquiv (h : γ ≃ₜ γ₂) : γ ≃ᵐ γ₂ where
  measurable_toFun := h.measurable
  measurable_invFun := h.symm.measurable
  toEquiv := h.toEquiv
#align homeomorph.to_measurable_equiv Homeomorph.toMeasurableEquiv

lemma Homeomorph.measurableEmbedding (h : γ ≃ₜ γ₂) : MeasurableEmbedding h :=
  h.toMeasurableEquiv.measurableEmbedding

@[simp]
theorem Homeomorph.toMeasurableEquiv_coe (h : γ ≃ₜ γ₂) : (h.toMeasurableEquiv : γ → γ₂) = h :=
  rfl
#align homeomorph.to_measurable_equiv_coe Homeomorph.toMeasurableEquiv_coe

@[simp]
theorem Homeomorph.toMeasurableEquiv_symm_coe (h : γ ≃ₜ γ₂) :
    (h.toMeasurableEquiv.symm : γ₂ → γ) = h.symm :=
  rfl
#align homeomorph.to_measurable_equiv_symm_coe Homeomorph.toMeasurableEquiv_symm_coe

end Homeomorph

@[measurability]
theorem ContinuousMap.measurable (f : C(α, γ)) : Measurable f :=
  f.continuous.measurable
#align continuous_map.measurable ContinuousMap.measurable

theorem measurable_of_continuousOn_compl_singleton [T1Space α] {f : α → γ} (a : α)
    (hf : ContinuousOn f {a}ᶜ) : Measurable f :=
  measurable_of_measurable_on_compl_singleton a
    (continuousOn_iff_continuous_restrict.1 hf).measurable
#align measurable_of_continuous_on_compl_singleton measurable_of_continuousOn_compl_singleton

theorem Continuous.measurable2 [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) :=
  h.measurable.comp (hf.prod_mk hg)
#align continuous.measurable2 Continuous.measurable2

theorem Continuous.aemeasurable2 [SecondCountableTopologyEither α β]
    {f : δ → α} {g : δ → β} {c : α → β → γ} {μ : Measure δ}
    (h : Continuous fun p : α × β => c p.1 p.2) (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    AEMeasurable (fun a => c (f a) (g a)) μ :=
  h.measurable.comp_aemeasurable (hf.prod_mk hg)
#align continuous.ae_measurable2 Continuous.aemeasurable2

instance (priority := 100) HasContinuousInv₀.measurableInv [GroupWithZero γ] [T1Space γ]
    [HasContinuousInv₀ γ] : MeasurableInv γ :=
  ⟨measurable_of_continuousOn_compl_singleton 0 continuousOn_inv₀⟩
#align has_continuous_inv₀.has_measurable_inv HasContinuousInv₀.measurableInv

@[to_additive]
instance (priority := 100) ContinuousMul.measurableMul₂ [SecondCountableTopology γ] [Mul γ]
    [ContinuousMul γ] : MeasurableMul₂ γ :=
  ⟨continuous_mul.measurable⟩
#align has_continuous_mul.has_measurable_mul₂ ContinuousMul.measurableMul₂
#align has_continuous_add.has_measurable_mul₂ ContinuousAdd.measurableMul₂

instance (priority := 100) ContinuousSub.measurableSub₂ [SecondCountableTopology γ] [Sub γ]
    [ContinuousSub γ] : MeasurableSub₂ γ :=
  ⟨continuous_sub.measurable⟩
#align has_continuous_sub.has_measurable_sub₂ ContinuousSub.measurableSub₂

instance (priority := 100) ContinuousSMul.measurableSMul₂ {M α} [TopologicalSpace M]
    [MeasurableSpace M] [OpensMeasurableSpace M] [TopologicalSpace α]
    [SecondCountableTopologyEither M α] [MeasurableSpace α] [BorelSpace α] [SMul M α]
    [ContinuousSMul M α] : MeasurableSMul₂ M α :=
  ⟨continuous_smul.measurable⟩
#align has_continuous_smul.has_measurable_smul₂ ContinuousSMul.measurableSMul₂

end

section BorelSpace

variable [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [TopologicalSpace β]
  [MeasurableSpace β] [BorelSpace β] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ]
  [MeasurableSpace δ]

theorem pi_le_borel_pi {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)]
    [∀ i, MeasurableSpace (π i)] [∀ i, BorelSpace (π i)] :
      MeasurableSpace.pi ≤ borel (∀ i, π i) := by
  have : ‹∀ i, MeasurableSpace (π i)› = fun i => borel (π i) :=
    funext fun i => BorelSpace.measurable_eq
  rw [this]
  exact iSup_le fun i => comap_le_iff_le_map.2 <| (continuous_apply i).borel_measurable
#align pi_le_borel_pi pi_le_borel_pi

theorem prod_le_borel_prod : Prod.instMeasurableSpace ≤ borel (α × β) := by
  rw [‹BorelSpace α›.measurable_eq, ‹BorelSpace β›.measurable_eq]
  refine' sup_le _ _
  · exact comap_le_iff_le_map.mpr continuous_fst.borel_measurable
  · exact comap_le_iff_le_map.mpr continuous_snd.borel_measurable
#align prod_le_borel_prod prod_le_borel_prod

instance Pi.borelSpace {ι : Type*} {π : ι → Type*} [Countable ι] [∀ i, TopologicalSpace (π i)]
    [∀ i, MeasurableSpace (π i)] [∀ i, SecondCountableTopology (π i)] [∀ i, BorelSpace (π i)] :
    BorelSpace (∀ i, π i) :=
  ⟨le_antisymm pi_le_borel_pi OpensMeasurableSpace.borel_le⟩
#align pi.borel_space Pi.borelSpace

instance Prod.borelSpace [SecondCountableTopologyEither α β] :
    BorelSpace (α × β) :=
  ⟨le_antisymm prod_le_borel_prod OpensMeasurableSpace.borel_le⟩
#align prod.borel_space Prod.borelSpace

/-- Given a measurable embedding to a Borel space which is also a topological embedding, then the
source space is also a Borel space. -/
lemma MeasurableEmbedding.borelSpace {α β : Type*} [MeasurableSpace α] [TopologicalSpace α]
    [MeasurableSpace β] [TopologicalSpace β] [hβ : BorelSpace β] {e : α → β}
    (h'e : MeasurableEmbedding e) (h''e : Inducing e) :
    BorelSpace α := by
  constructor
  have : MeasurableSpace.comap e (borel β) = ‹_› := by simpa [hβ.measurable_eq] using h'e.comap_eq
  rw [← this, ← borel_comap, h''e.induced]

instance _root_.ULift.instBorelSpace : BorelSpace (ULift α) :=
  MeasurableEquiv.ulift.measurableEmbedding.borelSpace Homeomorph.ulift.inducing

instance DiscreteMeasurableSpace.toBorelSpace {α : Type*} [TopologicalSpace α] [DiscreteTopology α]
    [MeasurableSpace α] [DiscreteMeasurableSpace α] : BorelSpace α := by
  constructor; ext; simp [MeasurableSpace.measurableSet_generateFrom, measurableSet_discrete]

protected theorem Embedding.measurableEmbedding {f : α → β} (h₁ : Embedding f)
    (h₂ : MeasurableSet (range f)) : MeasurableEmbedding f :=
  show MeasurableEmbedding
      (((↑) : range f → β) ∘ (Homeomorph.ofEmbedding f h₁).toMeasurableEquiv) from
    (MeasurableEmbedding.subtype_coe h₂).comp (MeasurableEquiv.measurableEmbedding _)
#align embedding.measurable_embedding Embedding.measurableEmbedding

protected theorem ClosedEmbedding.measurableEmbedding {f : α → β} (h : ClosedEmbedding f) :
    MeasurableEmbedding f :=
  h.toEmbedding.measurableEmbedding h.isClosed_range.measurableSet
#align closed_embedding.measurable_embedding ClosedEmbedding.measurableEmbedding

protected theorem OpenEmbedding.measurableEmbedding {f : α → β} (h : OpenEmbedding f) :
    MeasurableEmbedding f :=
  h.toEmbedding.measurableEmbedding h.isOpen_range.measurableSet
#align open_embedding.measurable_embedding OpenEmbedding.measurableEmbedding

section LinearOrder

variable [LinearOrder α] [OrderTopology α] [SecondCountableTopology α]

theorem measurable_of_Iio {f : δ → α} (hf : ∀ x, MeasurableSet (f ⁻¹' Iio x)) : Measurable f := by
  convert measurable_generateFrom (α := δ) _
  · exact BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Iio _)
  · rintro _ ⟨x, rfl⟩; exact hf x
#align measurable_of_Iio measurable_of_Iio

theorem UpperSemicontinuous.measurable [TopologicalSpace δ] [OpensMeasurableSpace δ] {f : δ → α}
    (hf : UpperSemicontinuous f) : Measurable f :=
  measurable_of_Iio fun y => (hf.isOpen_preimage y).measurableSet
#align upper_semicontinuous.measurable UpperSemicontinuous.measurable

theorem measurable_of_Ioi {f : δ → α} (hf : ∀ x, MeasurableSet (f ⁻¹' Ioi x)) : Measurable f := by
  convert measurable_generateFrom (α := δ) _
  · exact BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Ioi _)
  · rintro _ ⟨x, rfl⟩; exact hf x
#align measurable_of_Ioi measurable_of_Ioi

theorem LowerSemicontinuous.measurable [TopologicalSpace δ] [OpensMeasurableSpace δ] {f : δ → α}
    (hf : LowerSemicontinuous f) : Measurable f :=
  measurable_of_Ioi fun y => (hf.isOpen_preimage y).measurableSet
#align lower_semicontinuous.measurable LowerSemicontinuous.measurable

theorem measurable_of_Iic {f : δ → α} (hf : ∀ x, MeasurableSet (f ⁻¹' Iic x)) : Measurable f := by
  apply measurable_of_Ioi
  simp_rw [← compl_Iic, preimage_compl, MeasurableSet.compl_iff]
  assumption
#align measurable_of_Iic measurable_of_Iic

theorem measurable_of_Ici {f : δ → α} (hf : ∀ x, MeasurableSet (f ⁻¹' Ici x)) : Measurable f := by
  apply measurable_of_Iio
  simp_rw [← compl_Ici, preimage_compl, MeasurableSet.compl_iff]
  assumption
#align measurable_of_Ici measurable_of_Ici

/-- If a function is the least upper bound of countably many measurable functions,
then it is measurable. -/
theorem Measurable.isLUB {ι} [Countable ι] {f : ι → δ → α} {g : δ → α} (hf : ∀ i, Measurable (f i))
    (hg : ∀ b, IsLUB { a | ∃ i, f i b = a } (g b)) : Measurable g := by
  change ∀ b, IsLUB (range fun i => f i b) (g b) at hg
  rw [‹BorelSpace α›.measurable_eq, borel_eq_generateFrom_Ioi α]
  apply measurable_generateFrom
  rintro _ ⟨a, rfl⟩
  simp_rw [Set.preimage, mem_Ioi, lt_isLUB_iff (hg _), exists_range_iff, setOf_exists]
  exact MeasurableSet.iUnion fun i => hf i (isOpen_lt' _).measurableSet
#align measurable.is_lub Measurable.isLUB

/-- 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 Measurable.isLUB_of_mem {ι} [Countable ι] {f : ι → δ → α} {g g' : δ → α}
    (hf : ∀ i, Measurable (f i))
    {s : Set δ} (hs : MeasurableSet s) (hg : ∀ b ∈ s, IsLUB { a | ∃ i, f i b = a } (g b))
    (hg' : EqOn g g' sᶜ) (g'_meas : Measurable g') : Measurable g := by
  rcases isEmpty_or_nonempty ι with hι|⟨⟨i⟩⟩
  · rcases eq_empty_or_nonempty s with rfl|⟨x, hx⟩
    · convert g'_meas
      rwa [compl_empty, eqOn_univ] at hg'
    · have A : ∀ b ∈ s, IsBot (g b) := by simpa using hg
      have B : ∀ b ∈ s, g b = g x := by
        intro b hb
        apply le_antisymm (A b hb (g x)) (A x hx (g b))
      have : g = s.piecewise (fun _y ↦ g x) g' := by
        ext b
        by_cases hb : b ∈ s
        · simp [hb, B]
        · simp [hb, hg' hb]
      rw [this]
      exact Measurable.piecewise hs measurable_const g'_meas
  · let f' : ι → δ → α := fun i ↦ s.piecewise (f i) g'
    suffices ∀ b, IsLUB { a | ∃ i, f' i b = a } (g b) from
      Measurable.isLUB (fun i ↦ Measurable.piecewise hs (hf i) g'_meas) this
    intro b
    by_cases hb : b ∈ s
    · have A : ∀ i, f' i b = f i b := fun i ↦ by simp [f', hb]
      simpa [A] using hg b hb
    · have A : ∀ i, f' i b = g' b := fun i ↦ by simp [f', hb]
      have : {a | ∃ (_i : ι), g' b = a} = {g' b} := by
        apply Subset.antisymm
        · rintro - ⟨_j, rfl⟩
          simp only [mem_singleton_iff]
        · rintro - rfl
          exact ⟨i, rfl⟩
      simp [A, this, hg' hb, isLUB_singleton]

theorem AEMeasurable.isLUB {ι} {μ : Measure δ} [Countable ι] {f : ι → δ → α} {g : δ → α}
    (hf : ∀ i, AEMeasurable (f i) μ) (hg : ∀ᵐ b ∂μ, IsLUB { a | ∃ i, f i b = a } (g b)) :
    AEMeasurable g μ := by
  nontriviality α
  haveI hα : Nonempty α := inferInstance
  cases' isEmpty_or_nonempty ι with hι hι
  · simp only [IsEmpty.exists_iff, setOf_false, isLUB_empty_iff] at hg
    exact aemeasurable_const' (hg.mono fun a ha => hg.mono fun b hb => (ha _).antisymm (hb _))
  let p : δ → (ι → α) → Prop := fun x f' => IsLUB { a | ∃ i, f' i = a } (g x)
  let g_seq := (aeSeqSet hf p).piecewise g fun _ => hα.some
  have hg_seq : ∀ b, IsLUB { a | ∃ i, aeSeq hf p i b = a } (g_seq b) := by
    intro b
    simp only [g_seq, aeSeq, Set.piecewise]
    split_ifs with h
    · have h_set_eq : { a : α | ∃ i : ι, (hf i).mk (f i) b = a } =
        { a : α | ∃ i : ι, f i b = a } := by
        ext x
        simp_rw [Set.mem_setOf_eq, aeSeq.mk_eq_fun_of_mem_aeSeqSet hf h]
      rw [h_set_eq]
      exact aeSeq.fun_prop_of_mem_aeSeqSet hf h
    · exact IsGreatest.isLUB ⟨(@exists_const (hα.some = hα.some) ι _).2 rfl, fun x ⟨i, hi⟩ => hi.ge⟩
  refine' ⟨g_seq, Measurable.isLUB (aeSeq.measurable hf p) hg_seq, _⟩
  exact
    (ite_ae_eq_of_measure_compl_zero g (fun _ => hα.some) (aeSeqSet hf p)
        (aeSeq.measure_compl_aeSeqSet_eq_zero hf hg)).symm
#align ae_measurable.is_lub AEMeasurable.isLUB

/-- If a function is the greatest lower bound of countably many measurable functions,
then it is measurable. -/
theorem Measurable.isGLB {ι} [Countable ι] {f : ι → δ → α} {g : δ → α} (hf : ∀ i, Measurable (f i))
    (hg : ∀ b, IsGLB { a | ∃ i, f i b = a } (g b)) : Measurable g :=
  Measurable.isLUB (α := αᵒᵈ) hf hg
#align measurable.is_glb Measurable.isGLB

/-- 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 Measurable.isGLB_of_mem {ι} [Countable ι] {f : ι → δ → α} {g g' : δ → α}
    (hf : ∀ i, Measurable (f i))
    {s : Set δ} (hs : MeasurableSet s) (hg : ∀ b ∈ s, IsGLB { a | ∃ i, f i b = a } (g b))
    (hg' : EqOn g g' sᶜ) (g'_meas : Measurable g') : Measurable g :=
  Measurable.isLUB_of_mem (α := αᵒᵈ) hf hs hg hg'  g'_meas

theorem AEMeasurable.isGLB {ι} {μ : Measure δ} [Countable ι] {f : ι → δ → α} {g : δ → α}
    (hf : ∀ i, AEMeasurable (f i) μ) (hg : ∀ᵐ b ∂μ, IsGLB { a | ∃ i, f i b = a } (g b)) :
    AEMeasurable g μ :=
  AEMeasurable.isLUB (α := αᵒᵈ) hf hg
#align ae_measurable.is_glb AEMeasurable.isGLB

protected theorem Monotone.measurable [LinearOrder β] [OrderClosedTopology β] {f : β → α}
    (hf : Monotone f) : Measurable f :=
  suffices h : ∀ x, OrdConnected (f ⁻¹' Ioi x) from measurable_of_Ioi fun x => (h x).measurableSet
  fun _ => ordConnected_def.mpr fun _a ha _ _ _c hc => lt_of_lt_of_le ha (hf hc.1)
#align monotone.measurable Monotone.measurable

theorem aemeasurable_restrict_of_monotoneOn [LinearOrder β] [OrderClosedTopology β] {μ : Measure β}
    {s : Set β} (hs : MeasurableSet s) {f : β → α} (hf : MonotoneOn f s) :
    AEMeasurable f (μ.restrict s) :=
  have : Monotone (f ∘ (↑) : s → α) := fun ⟨x, hx⟩ ⟨y, hy⟩ => fun (hxy : x ≤ y) => hf hx hy hxy
  aemeasurable_restrict_of_measurable_subtype hs this.measurable
#align ae_measurable_restrict_of_monotone_on aemeasurable_restrict_of_monotoneOn

protected theorem Antitone.measurable [LinearOrder β] [OrderClosedTopology β] {f : β → α}
    (hf : Antitone f) : Measurable f :=
  @Monotone.measurable αᵒᵈ β _ _ ‹_› _ _ _ _ _ ‹_› _ _ _ hf
#align antitone.measurable Antitone.measurable

theorem aemeasurable_restrict_of_antitoneOn [LinearOrder β] [OrderClosedTopology β] {μ : Measure β}
    {s : Set β} (hs : MeasurableSet s) {f : β → α} (hf : AntitoneOn f s) :
    AEMeasurable f (μ.restrict s) :=
  @aemeasurable_restrict_of_monotoneOn αᵒᵈ β _ _ ‹_› _ _ _ _ _ ‹_› _ _ _ _ hs _ hf
#align ae_measurable_restrict_of_antitone_on aemeasurable_restrict_of_antitoneOn

theorem measurableSet_of_mem_nhdsWithin_Ioi_aux {s : Set α} (h : ∀ x ∈ s, s ∈ 𝓝[>] x)
    (h' : ∀ x ∈ s, ∃ y, x < y) : MeasurableSet s := by
  choose! M hM using h'
  suffices H : (s \ interior s).Countable by
    have : s = interior s ∪ s \ interior s := by rw [union_diff_cancel interior_subset]
    rw [this]
    exact isOpen_interior.measurableSet.union H.measurableSet
  have A : ∀ x ∈ s, ∃ y ∈ Ioi x, Ioo x y ⊆ s := fun x hx =>
    (mem_nhdsWithin_Ioi_iff_exists_Ioo_subset' (hM x hx)).1 (h x hx)
  choose! y hy h'y using A
  have B : Set.PairwiseDisjoint (s \ interior s) fun x => Ioo x (y x) := by
    intro x hx x' hx' hxx'
    rcases lt_or_gt_of_ne hxx' with (h' | h')
    · refine disjoint_left.2 fun z hz h'z => ?_
      have : x' ∈ interior s :=
        mem_interior.2 ⟨Ioo x (y x), h'y _ hx.1, isOpen_Ioo, ⟨h', h'z.1.trans hz.2⟩⟩
      exact False.elim (hx'.2 this)
    · refine disjoint_left.2 fun z hz h'z => ?_
      have : x ∈ interior s :=
        mem_interior.2 ⟨Ioo x' (y x'), h'y _ hx'.1, isOpen_Ioo, ⟨h', hz.1.trans h'z.2⟩⟩
      exact False.elim (hx.2 this)
  exact B.countable_of_Ioo fun x hx => hy x hx.1
#align measurable_set_of_mem_nhds_within_Ioi_aux measurableSet_of_mem_nhdsWithin_Ioi_aux

/-- If a set is a right-neighborhood of all of its points, then it is measurable. -/
theorem measurableSet_of_mem_nhdsWithin_Ioi {s : Set α} (h : ∀ x ∈ s, s ∈ 𝓝[>] x) :
    MeasurableSet s := by
  by_cases H : ∃ x ∈ s, IsTop x
  · rcases H with ⟨x₀, x₀s, h₀⟩
    have : s = {x₀} ∪ s \ {x₀} := by rw [union_diff_cancel (singleton_subset_iff.2 x₀s)]
    rw [this]
    refine' (measurableSet_singleton _).union _
    have A : ∀ x ∈ s \ {x₀}, x < x₀ := fun x hx => lt_of_le_of_ne (h₀ _) (by simpa using hx.2)
    refine' measurableSet_of_mem_nhdsWithin_Ioi_aux (fun x hx => _) fun x hx => ⟨x₀, A x hx⟩
    obtain ⟨u, hu, us⟩ : ∃ (u : α), u ∈ Ioi x ∧ Ioo x u ⊆ s :=
      (mem_nhdsWithin_Ioi_iff_exists_Ioo_subset' (A x hx)).1 (h x hx.1)
    refine' (mem_nhdsWithin_Ioi_iff_exists_Ioo_subset' (A x hx)).2 ⟨u, hu, fun y hy => ⟨us hy, _⟩⟩
    exact ne_of_lt (hy.2.trans_le (h₀ _))
  · apply measurableSet_of_mem_nhdsWithin_Ioi_aux h
    simp only [IsTop] at H
    push_neg at H
    exact H
#align measurable_set_of_mem_nhds_within_Ioi measurableSet_of_mem_nhdsWithin_Ioi

lemma measurableSet_bddAbove_range {ι} [Countable ι] {f : ι → δ → α} (hf : ∀ i, Measurable (f i)) :
    MeasurableSet {b | BddAbove (range (fun i ↦ f i b))} := by
  rcases isEmpty_or_nonempty α with hα|hα
  · have : ∀ b, range (fun i ↦ f i b) = ∅ := fun b ↦ eq_empty_of_isEmpty _
    simp [this]
  have A : ∀ (i : ι) (c : α), MeasurableSet {x | f i x ≤ c} := by
    intro i c
    exact measurableSet_le (hf i) measurable_const
  have B : ∀ (c : α), MeasurableSet {x | ∀ i, f i x ≤ c} := by
    intro c
    rw [setOf_forall]
    exact MeasurableSet.iInter (fun i ↦ A i c)
  obtain ⟨u, hu⟩ : ∃ (u : ℕ → α), Tendsto u atTop atTop := exists_seq_tendsto (atTop : Filter α)
  have : {b | BddAbove (range (fun i ↦ f i b))} = {x | ∃ n, ∀ i, f i x ≤ u n} := by
    apply Subset.antisymm
    · rintro x ⟨c, hc⟩
      obtain ⟨n, hn⟩ : ∃ n, c ≤ u n := (tendsto_atTop.1 hu c).exists
      exact ⟨n, fun i ↦ (hc ((mem_range_self i))).trans hn⟩
    · rintro x ⟨n, hn⟩
      refine ⟨u n, ?_⟩
      rintro - ⟨i, rfl⟩
      exact hn i
  rw [this, setOf_exists]
  exact MeasurableSet.iUnion (fun n ↦ B (u n))

lemma measurableSet_bddBelow_range {ι} [Countable ι] {f : ι → δ → α} (hf : ∀ i, Measurable (f i)) :
    MeasurableSet {b | BddBelow (range (fun i ↦ f i b))} :=
  measurableSet_bddAbove_range (α := αᵒᵈ) hf

end LinearOrder

@[measurability]
theorem Measurable.iSup_Prop {α} [MeasurableSpace α] [ConditionallyCompleteLattice α]
    (p : Prop) {f : δ → α} (hf : Measurable f) : Measurable fun b => ⨆ _ : p, f b := by
  simp_rw [ciSup_eq_ite]
  split_ifs with h
  · exact hf
  · exact measurable_const
#align measurable.supr_Prop Measurable.iSup_Prop

@[measurability]
theorem Measurable.iInf_Prop {α} [MeasurableSpace α] [ConditionallyCompleteLattice α]
    (p : Prop) {f : δ → α} (hf : Measurable f) : Measurable fun b => ⨅ _ : p, f b := by
  simp_rw [ciInf_eq_ite]
  split_ifs with h
  · exact hf
  · exact measurable_const
#align measurable.infi_Prop Measurable.iInf_Prop

section ConditionallyCompleteLinearOrder

variable [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α]

@[measurability]
theorem measurable_iSup {ι} [Countable ι] {f : ι → δ → α} (hf : ∀ i, Measurable (f i)) :
    Measurable (fun b ↦ ⨆ i, f i b) := by
  rcases isEmpty_or_nonempty ι with hι|hι
  · simp [iSup_of_empty']
  have A : MeasurableSet {b | BddAbove (range (fun i ↦ f i b))} :=
    measurableSet_bddAbove_range hf
  have : Measurable (fun (_b : δ) ↦ sSup (∅ : Set α)) := measurable_const
  apply Measurable.isLUB_of_mem hf A _ _ this
  · rintro b ⟨c, hc⟩
    apply isLUB_ciSup
    refine ⟨c, ?_⟩
    rintro d ⟨i, rfl⟩
    exact hc (mem_range_self i)
  · intro b hb
    apply csSup_of_not_bddAbove
    exact hb

@[measurability]
theorem aemeasurable_iSup {ι} {μ : Measure δ} [Countable ι] {f : ι → δ → α}
    (hf : ∀ i, AEMeasurable (f i) μ) : AEMeasurable (fun b => ⨆ i, f i b) μ := by
  refine ⟨fun b ↦ ⨆ i, (hf i).mk (f i) b, measurable_iSup (fun i ↦ (hf i).measurable_mk), ?_⟩
  filter_upwards [ae_all_iff.2 (fun i ↦ (hf i).ae_eq_mk)] with b hb using by simp [hb]
#align ae_measurable_supr aemeasurable_iSup

@[measurability]
theorem measurable_iInf {ι} [Countable ι] {f : ι → δ → α} (hf : ∀ i, Measurable (f i)) :
    Measurable fun b => ⨅ i, f i b :=
  measurable_iSup (α := αᵒᵈ) hf
#align measurable_infi measurable_iInf

@[measurability]
theorem aemeasurable_iInf {ι} {μ : Measure δ} [Countable ι] {f : ι → δ → α}
    (hf : ∀ i, AEMeasurable (f i) μ) : AEMeasurable (fun b => ⨅ i, f i b) μ :=
  aemeasurable_iSup (α := αᵒᵈ) hf
#align ae_measurable_infi aemeasurable_iInf

theorem measurable_sSup {ι} {f : ι → δ → α} {s : Set ι} (hs : s.Countable)
    (hf : ∀ i ∈ s, Measurable (f i)) :
    Measurable fun x => sSup ((fun i => f i x) '' s) := by
  have : Countable ↑s := countable_coe_iff.2 hs
  convert measurable_iSup (f := (fun (i : s) ↦ f i)) (fun i ↦ hf i i.2) using 1
  ext b
  congr
  exact image_eq_range (fun i ↦ f i b) s
#align measurable_cSup measurable_sSup

theorem measurable_sInf {ι} {f : ι → δ → α} {s : Set ι} (hs : s.Countable)
    (hf : ∀ i ∈ s, Measurable (f i)) :
    Measurable fun x => sInf ((fun i => f i x) '' s) :=
  measurable_sSup (α := αᵒᵈ) hs hf
#align measurable_cInf measurable_sInf

theorem measurable_biSup {ι} (s : Set ι) {f : ι → δ → α} (hs : s.Countable)
    (hf : ∀ i ∈ s, Measurable (f i)) : Measurable fun b => ⨆ i ∈ s, f i b := by
  haveI : Encodable s := hs.toEncodable
  by_cases H : ∀ i, i ∈ s
  · have : ∀ b, ⨆ i ∈ s, f i b = ⨆ (i : s), f i b :=
      fun b ↦ cbiSup_eq_of_forall (f := fun i ↦ f i b) H
    simp only [this]
    exact measurable_iSup (fun (i : s) ↦ hf i i.2)
  · have : ∀ b, ⨆ i ∈ s, f i b = (⨆ (i : s), f i b) ⊔ sSup ∅ :=
      fun b ↦ cbiSup_eq_of_not_forall (f := fun i ↦ f i b) H
    simp only [this]
    apply Measurable.sup _ measurable_const
    exact measurable_iSup (fun (i : s) ↦ hf i i.2)
#align measurable_bsupr measurable_biSup

theorem aemeasurable_biSup {ι} {μ : Measure δ} (s : Set ι) {f : ι → δ → α} (hs : s.Countable)
    (hf : ∀ i ∈ s, AEMeasurable (f i) μ) : AEMeasurable (fun b => ⨆ i ∈ s, f i b) μ := by
  let g : ι → δ → α := fun i ↦ if hi : i ∈ s then (hf i hi).mk (f i) else fun _b ↦ sSup ∅
  have : ∀ i ∈ s, Measurable (g i) := by
    intro i hi
    simpa [g, hi] using (hf i hi).measurable_mk
  refine ⟨fun b ↦ ⨆ (i) (_ : i ∈ s), g i b, measurable_biSup s hs this, ?_⟩
  have : ∀ i ∈ s, ∀ᵐ b ∂μ, f i b = g i b :=
    fun i hi ↦ by simpa [g, hi] using (hf i hi).ae_eq_mk
  filter_upwards [(ae_ball_iff hs).2 this] with b hb
  exact iSup_congr fun i => iSup_congr (hb i)
#align ae_measurable_bsupr aemeasurable_biSup

theorem measurable_biInf {ι} (s : Set ι) {f : ι → δ → α} (hs : s.Countable)
    (hf : ∀ i ∈ s, Measurable (f i)) : Measurable fun b => ⨅ i ∈ s, f i b :=
  measurable_biSup (α := αᵒᵈ) s hs hf
#align measurable_binfi measurable_biInf

theorem aemeasurable_biInf {ι} {μ : Measure δ} (s : Set ι) {f : ι → δ → α} (hs : s.Countable)
    (hf : ∀ i ∈ s, AEMeasurable (f i) μ) : AEMeasurable (fun b => ⨅ i ∈ s, f i b) μ :=
  aemeasurable_biSup (α := αᵒᵈ) s hs hf
#align ae_measurable_binfi aemeasurable_biInf

/-- `liminf` over a general filter is measurable. See `measurable_liminf` for the version over `ℕ`.
-/
theorem measurable_liminf' {ι ι'} {f : ι → δ → α} {v : Filter ι} (hf : ∀ i, Measurable (f i))
    {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasCountableBasis p s) (hs : ∀ j, (s j).Countable) :
    Measurable fun x => liminf (f · x) v := by
  /- We would like to write the liminf as `⨆ (j : Subtype p), ⨅ (i : s j), f i x`, as the
  measurability would follow from the measurability of infs and sups. Unfortunately, this is not
  true in general conditionally complete linear orders because of issues with empty sets or sets
  which are not bounded above or below. A slightly more complicated expression for the liminf,
  valid in general, is given in `Filter.HasBasis.liminf_eq_ite`. This expression, built from
  `if ... then ... else` and infs and sups, can be readily checked to be measurable. -/
  have : Countable (Subtype p) := hv.countable
  rcases isEmpty_or_nonempty (Subtype p) with hp|hp
  · simp [hv.liminf_eq_sSup_iUnion_iInter]
  by_cases H : ∃ (j : Subtype p), s j = ∅
  · simp_rw [hv.liminf_eq_ite, if_pos H, measurable_const]
  simp_rw [hv.liminf_eq_ite, if_neg H]
  have : ∀ i, Countable (s i) := fun i ↦ countable_coe_iff.2 (hs i)
  let m : Subtype p → Set δ := fun j ↦ {x | BddBelow (range (fun (i : s j) ↦ f i x))}
  have m_meas : ∀ j, MeasurableSet (m j) :=
    fun j ↦ measurableSet_bddBelow_range (fun (i : s j) ↦ hf i)
  have mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j} := by
    rw [setOf_forall]
    exact MeasurableSet.iInter (fun j ↦ (m_meas j).compl)
  apply Measurable.piecewise mc_meas measurable_const
  apply measurable_iSup (fun j ↦ ?_)
  let reparam : δ → Subtype p → Subtype p := fun x ↦ liminf_reparam (fun i ↦ f i x) s p
  let F0 : Subtype p → δ → α := fun j x ↦ ⨅ (i : s j), f i x
  have F0_meas : ∀ j, Measurable (F0 j) := fun j ↦ measurable_iInf (fun (i : s j) ↦ hf i)
  set F1 : δ → α := fun x ↦ F0 (reparam x j) x with hF1
  change Measurable F1
  let g : ℕ → Subtype p := Classical.choose (exists_surjective_nat (Subtype p))
  have Z : ∀ x, ∃ n, x ∈ m (g n) ∨ ∀ k, x ∉ m k := by
    intro x
    by_cases H : ∃ k, x ∈ m k
    · rcases H with ⟨k, hk⟩
      rcases Classical.choose_spec (exists_surjective_nat (Subtype p)) k with ⟨n, rfl⟩
      exact ⟨n, Or.inl hk⟩
    · push_neg at H
      exact ⟨0, Or.inr H⟩
  have : F1 = fun x ↦ if x ∈ m j then F0 j x else F0 (g (Nat.find (Z x))) x := by
    ext x
    have A : reparam x j = if x ∈ m j then j else g (Nat.find (Z x)) := rfl
    split_ifs with hjx
    · have : reparam x j = j := by rw [A, if_pos hjx]
      simp only [hF1, this]
    · have : reparam x j = g (Nat.find (Z x)) := by rw [A, if_neg hjx]
      simp only [hF1, this]
  rw [this]
  apply Measurable.piecewise (m_meas j) (F0_meas j)
  apply Measurable.find (fun n ↦ F0_meas (g n)) (fun n ↦ ?_)
  exact (m_meas (g n)).union mc_meas
#align measurable_liminf' measurable_liminf'

/-- `limsup` over a general filter is measurable. See `measurable_limsup` for the version over `ℕ`.
-/
theorem measurable_limsup' {ι ι'} {f : ι → δ → α} {u : Filter ι} (hf : ∀ i, Measurable (f i))
    {p : ι' → Prop} {s : ι' → Set ι} (hu : u.HasCountableBasis p s) (hs : ∀ i, (s i).Countable) :
    Measurable fun x => limsup (fun i => f i x) u :=
  measurable_liminf' (α := αᵒᵈ) hf hu hs
#align measurable_limsup' measurable_limsup'

/-- `liminf` over `ℕ` is measurable. See `measurable_liminf'` for a version with a general filter.
-/
@[measurability]
theorem measurable_liminf {f : ℕ → δ → α} (hf : ∀ i, Measurable (f i)) :
    Measurable fun x => liminf (fun i => f i x) atTop :=
  measurable_liminf' hf atTop_countable_basis fun _ => to_countable _
#align measurable_liminf measurable_liminf

/-- `limsup` over `ℕ` is measurable. See `measurable_limsup'` for a version with a general filter.
-/
@[measurability]
theorem measurable_limsup {f : ℕ → δ → α} (hf : ∀ i, Measurable (f i)) :
    Measurable fun x => limsup (fun i => f i x) atTop :=
  measurable_limsup' hf atTop_countable_basis fun _ => to_countable _
#align measurable_limsup measurable_limsup

end ConditionallyCompleteLinearOrder

/-- Convert a `Homeomorph` to a `MeasurableEquiv`. -/
def Homemorph.toMeasurableEquiv (h : α ≃ₜ β) : α ≃ᵐ β where
  toEquiv := h.toEquiv
  measurable_toFun := h.continuous_toFun.measurable
  measurable_invFun := h.continuous_invFun.measurable
#align homemorph.to_measurable_equiv Homemorph.toMeasurableEquiv

protected theorem IsFiniteMeasureOnCompacts.map (μ : Measure α) [IsFiniteMeasureOnCompacts μ]
    (f : α ≃ₜ β) : IsFiniteMeasureOnCompacts (Measure.map f μ) := by
  refine ⟨fun K hK ↦ ?_⟩
  rw [← Homeomorph.toMeasurableEquiv_coe, MeasurableEquiv.map_apply]
  exact IsCompact.measure_lt_top (f.isCompact_preimage.2 hK)
#align is_finite_measure_on_compacts.map IsFiniteMeasureOnCompacts.map

end BorelSpace

instance Empty.borelSpace : BorelSpace Empty :=
  ⟨borel_eq_top_of_discrete.symm⟩
#align empty.borel_space Empty.borelSpace

instance Unit.borelSpace : BorelSpace Unit :=
  ⟨borel_eq_top_of_discrete.symm⟩
#align unit.borel_space Unit.borelSpace

instance Bool.borelSpace : BorelSpace Bool :=
  ⟨borel_eq_top_of_discrete.symm⟩
#align bool.borel_space Bool.borelSpace

instance Nat.borelSpace : BorelSpace ℕ :=
  ⟨borel_eq_top_of_discrete.symm⟩
#align nat.borel_space Nat.borelSpace

instance Int.borelSpace : BorelSpace ℤ :=
  ⟨borel_eq_top_of_discrete.symm⟩
#align int.borel_space Int.borelSpace

instance Rat.borelSpace : BorelSpace ℚ :=
  ⟨borel_eq_top_of_countable.symm⟩
#align rat.borel_space Rat.borelSpace

/- Instances on `Real` and `Complex` are special cases of `RCLike` but without these instances,
Lean fails to prove `BorelSpace (ι → ℝ)`, so we leave them here. -/
instance Real.measurableSpace : MeasurableSpace ℝ :=
  borel ℝ
#align real.measurable_space Real.measurableSpace

instance Real.borelSpace : BorelSpace ℝ :=
  ⟨rfl⟩
#align real.borel_space Real.borelSpace

instance NNReal.measurableSpace : MeasurableSpace ℝ≥0 :=
  Subtype.instMeasurableSpace
#align nnreal.measurable_space NNReal.measurableSpace

instance NNReal.borelSpace : BorelSpace ℝ≥0 :=
  Subtype.borelSpace _
#align nnreal.borel_space NNReal.borelSpace

instance ENNReal.measurableSpace : MeasurableSpace ℝ≥0∞ :=
  borel ℝ≥0∞
#align ennreal.measurable_space ENNReal.measurableSpace

instance ENNReal.borelSpace : BorelSpace ℝ≥0∞ :=
  ⟨rfl⟩
#align ennreal.borel_space ENNReal.borelSpace

instance EReal.measurableSpace : MeasurableSpace EReal :=
  borel EReal
#align ereal.measurable_space EReal.measurableSpace

instance EReal.borelSpace : BorelSpace EReal :=
  ⟨rfl⟩
#align ereal.borel_space EReal.borelSpace

/-- 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 measure_eq_measure_preimage_add_measure_tsum_Ico_zpow [MeasurableSpace α] (μ : Measure α)
    {f : α → ℝ≥0∞} (hf : Measurable f) {s : Set α} (hs : MeasurableSet s) {t : ℝ≥0} (ht : 1 < t) :
    μ s =
      μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' {∞}) +
      ∑' n : ℤ, μ (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) := by
  have A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0) := by
    rw [← measure_union]
    · rw [← inter_union_distrib_left, ← preimage_union, singleton_union, Ioi_insert,
        ← _root_.bot_eq_zero, Ici_bot, preimage_univ, inter_univ]
    · exact disjoint_singleton_left.mpr not_mem_Ioi_self
        |>.preimage f |>.inter_right' s |>.inter_left' s
    · exact hs.inter (hf measurableSet_Ioi)
  have B : μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {∞}) + μ (s ∩ f ⁻¹' Ioo 0 ∞) := by
    rw [← measure_union]
    · rw [← inter_union_distrib_left]
      congr
      ext x
      simp only [mem_singleton_iff, mem_union, mem_Ioo, mem_Ioi, mem_preimage]
      obtain (H | H) : f x = ∞ ∨ f x < ∞ := eq_or_lt_of_le le_top
      · simp only [H, eq_self_iff_true, or_false_iff, ENNReal.zero_lt_top, not_top_lt, and_false]
      · simp only [H, H.ne, and_true_iff, false_or_iff]
    · refine disjoint_left.2 fun x hx h'x => ?_
      have : f x < ∞ := h'x.2.2
      exact lt_irrefl _ (this.trans_le (le_of_eq hx.2.symm))
    · exact hs.inter (hf measurableSet_Ioo)
  have C : μ (s ∩ f ⁻¹' Ioo 0 ∞) =
      ∑' n : ℤ, μ (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) := by
    rw [← measure_iUnion,
      ENNReal.Ioo_zero_top_eq_iUnion_Ico_zpow (ENNReal.one_lt_coe_iff.2 ht) ENNReal.coe_ne_top,
      preimage_iUnion, inter_iUnion]
    · intro i j hij
      wlog h : i < j generalizing i j
      · exact (this hij.symm (hij.lt_or_lt.resolve_left h)).symm
      refine disjoint_left.2 fun x hx h'x => lt_irrefl (f x) ?_
      calc
        f x < (t : ℝ≥0∞) ^ (i + 1) := hx.2.2
        _ ≤ (t : ℝ≥0∞) ^ j := (ENNReal.zpow_le_of_le (ENNReal.one_le_coe_iff.2 ht.le) h)
        _ ≤ f x := h'x.2.1
    · intro n
      exact hs.inter (hf measurableSet_Ico)
  rw [A, B, C, add_assoc]
#align measure_eq_measure_preimage_add_measure_tsum_Ico_zpow measure_eq_measure_preimage_add_measure_tsum_Ico_zpow

section PseudoMetricSpace

variable [PseudoMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α]
variable [MeasurableSpace β] {x : α} {ε : ℝ}

open Metric

@[measurability]
theorem measurableSet_ball : MeasurableSet (Metric.ball x ε) :=
  Metric.isOpen_ball.measurableSet
#align measurable_set_ball measurableSet_ball

@[measurability]
theorem measurableSet_closedBall : MeasurableSet (Metric.closedBall x ε) :=
  Metric.isClosed_ball.measurableSet
#align measurable_set_closed_ball measurableSet_closedBall

@[measurability]
theorem measurable_infDist {s : Set α} : Measurable fun x => infDist x s :=
  (continuous_infDist_pt s).measurable
#align measurable_inf_dist measurable_infDist

@[measurability]
theorem Measurable.infDist {f : β → α} (hf : Measurable f) {s : Set α} :
    Measurable fun x => infDist (f x) s :=
  measurable_infDist.comp hf
#align measurable.inf_dist Measurable.infDist

@[measurability]
theorem measurable_infNndist {s : Set α} : Measurable fun x => infNndist x s :=
  (continuous_infNndist_pt s).measurable
#align measurable_inf_nndist measurable_infNndist

@[measurability]
theorem Measurable.infNndist {f : β → α} (hf : Measurable f) {s : Set α} :
    Measurable fun x => infNndist (f x) s :=
  measurable_infNndist.comp hf
#align measurable.inf_nndist Measurable.infNndist

section

variable [SecondCountableTopology α]

@[measurability]
theorem measurable_dist : Measurable fun p : α × α => dist p.1 p.2 :=
  continuous_dist.measurable
#align measurable_dist measurable_dist

@[measurability]
theorem Measurable.dist {f g : β → α} (hf : Measurable f) (hg : Measurable g) :
    Measurable fun b => dist (f b) (g b) :=
  (@continuous_dist α _).measurable2 hf hg
#align measurable.dist Measurable.dist

@[measurability]
theorem measurable_nndist : Measurable fun p : α × α => nndist p.1 p.2 :=
  continuous_nndist.measurable
#align measurable_nndist measurable_nndist

@[measurability]
theorem Measurable.nndist {f g : β → α} (hf : Measurable f) (hg : Measurable g) :
    Measurable fun b => nndist (f b) (g b) :=
  (@continuous_nndist α _).measurable2 hf hg
#align measurable.nndist Measurable.nndist

end

end PseudoMetricSpace

section PseudoEMetricSpace

variable [PseudoEMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α]
variable [MeasurableSpace β] {x : α} {ε : ℝ≥0∞}

open EMetric

@[measurability]
theorem measurableSet_eball : MeasurableSet (EMetric.ball x ε) :=
  EMetric.isOpen_ball.measurableSet
#align measurable_set_eball measurableSet_eball

@[measurability]
theorem measurable_edist_right : Measurable (edist x) :=
  (continuous_const.edist continuous_id).measurable
#align measurable_edist_right measurable_edist_right

@[measurability]
theorem measurable_edist_left : Measurable fun y => edist y x :=
  (continuous_id.edist continuous_const).measurable
#align measurable_edist_left measurable_edist_left

@[measurability]
theorem measurable_infEdist {s : Set α} : Measurable fun x => infEdist x s :=
  continuous_infEdist.measurable
#align measurable_inf_edist measurable_infEdist

@[measurability]
theorem Measurable.infEdist {f : β → α} (hf : Measurable f) {s : Set α} :
    Measurable fun x => infEdist (f x) s :=
  measurable_infEdist.comp hf
#align measurable.inf_edist Measurable.infEdist

open Metric EMetric

/-- 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 {μ : Measure α} {s : Set α}
    (hs : ∃ R > 0, μ (cthickening R s) ≠ ∞) :
    Tendsto (fun r => μ (cthickening r s)) (𝓝 0) (𝓝 (μ (closure s))) := by
  have A : Tendsto (fun r => μ (cthickening r s)) (𝓝[Ioi 0] 0) (𝓝 (μ (closure s))) := by
    rw [closure_eq_iInter_cthickening]
    exact
      tendsto_measure_biInter_gt (fun r _ => isClosed_cthickening.measurableSet)
        (fun i j _ ij => cthickening_mono ij _) hs
  have B : Tendsto (fun r => μ (cthickening r s)) (𝓝[Iic 0] 0) (𝓝 (μ (closure s))) := by
    apply Tendsto.congr' _ tendsto_const_nhds
    filter_upwards [self_mem_nhdsWithin (α := ℝ)] with _ hr
    rw [cthickening_of_nonpos hr]
  convert B.sup A
  exact (nhds_left_sup_nhds_right' 0).symm
#align tendsto_measure_cthickening tendsto_measure_cthickening

/-- 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_cthickening_of_isClosed {μ : Measure α} {s : Set α}
    (hs : ∃ R > 0, μ (cthickening R s) ≠ ∞) (h's : IsClosed s) :
    Tendsto (fun r => μ (cthickening r s)) (𝓝 0) (𝓝 (μ s)) := by
  convert tendsto_measure_cthickening hs
  exact h's.closure_eq.symm
#align tendsto_measure_cthickening_of_is_closed tendsto_measure_cthickening_of_isClosed

/-- 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 {μ : Measure α} {s : Set α}
    (hs : ∃ R > 0, μ (thickening R s) ≠ ∞) :
    Tendsto (fun r => μ (thickening r s)) (𝓝[>] 0) (𝓝 (μ (closure s))) := by
  rw [closure_eq_iInter_thickening]
  exact tendsto_measure_biInter_gt (fun r _ => isOpen_thickening.measurableSet)
      (fun i j _ ij => thickening_mono ij _) hs

/-- 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 tendsto_measure_thickening_of_isClosed {μ : Measure α} {s : Set α}
    (hs : ∃ R > 0, μ (thickening R s) ≠ ∞) (h's : IsClosed s) :
    Tendsto (fun r => μ (thickening r s)) (𝓝[>] 0) (𝓝 (μ s)) := by
  convert tendsto_measure_thickening hs
  exact h's.closure_eq.symm

variable [SecondCountableTopology α]

@[measurability]
theorem measurable_edist : Measurable fun p : α × α => edist p.1 p.2 :=
  continuous_edist.measurable
#align measurable_edist measurable_edist

@[measurability]
theorem Measurable.edist {f g : β → α} (hf : Measurable f) (hg : Measurable g) :
    Measurable fun b => edist (f b) (g b) :=
  (@continuous_edist α _).measurable2 hf hg
#align measurable.edist Measurable.edist

@[measurability]
theorem AEMeasurable.edist {f g : β → α} {μ : Measure β} (hf : AEMeasurable f μ)
    (hg : AEMeasurable g μ) : AEMeasurable (fun a => edist (f a) (g a)) μ :=
  (@continuous_edist α _).aemeasurable2 hf hg
#align ae_measurable.edist AEMeasurable.edist

end PseudoEMetricSpace

/-- 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 tendsto_measure_cthickening_of_isCompact [MetricSpace α] [MeasurableSpace α]
    [OpensMeasurableSpace α] [ProperSpace α] {μ : Measure α} [IsFiniteMeasureOnCompacts μ]
    {s : Set α} (hs : IsCompact s) :
    Tendsto (fun r => μ (Metric.cthickening r s)) (𝓝 0) (𝓝 (μ s)) :=
  tendsto_measure_cthickening_of_isClosed
    ⟨1, zero_lt_one, hs.isBounded.cthickening.measure_lt_top.ne⟩ hs.isClosed
#align tendsto_measure_cthickening_of_is_compact tendsto_measure_cthickening_of_isCompact

namespace Real

open MeasurableSpace MeasureTheory

theorem borel_eq_generateFrom_Ioo_rat :
    borel ℝ = .generateFrom (⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo (a : ℝ) (b : ℝ)}) :=
  isTopologicalBasis_Ioo_rat.borel_eq_generateFrom
#align real.borel_eq_generate_from_Ioo_rat Real.borel_eq_generateFrom_Ioo_rat

theorem borel_eq_generateFrom_Iio_rat : borel ℝ = .generateFrom (⋃ a : ℚ, {Iio (a : ℝ)}) := by
  rw [borel_eq_generateFrom_Iio]
  refine le_antisymm
    (generateFrom_le ?_)
    (generateFrom_mono <| iUnion_subset fun q ↦ singleton_subset_iff.mpr <| mem_range_self _)
  rintro _ ⟨a, rfl⟩
  have : IsLUB (range ((↑) : ℚ → ℝ) ∩ Iio a) a := by
    simp [isLUB_iff_le_iff, mem_upperBounds, ← le_iff_forall_rat_lt_imp_le]
  rw [← this.biUnion_Iio_eq, ← image_univ, ← image_inter_preimage, univ_inter, biUnion_image]
  exact MeasurableSet.biUnion (to_countable _)
    fun b _ => GenerateMeasurable.basic (Iio (b : ℝ)) (by simp)

theorem borel_eq_generateFrom_Ioi_rat : borel ℝ = .generateFrom (⋃ a : ℚ, {Ioi (a : ℝ)}) := by
  rw [borel_eq_generateFrom_Ioi]
  refine le_antisymm
    (generateFrom_le ?_)
    (generateFrom_mono <| iUnion_subset fun q ↦ singleton_subset_iff.mpr <| mem_range_self _)
  rintro _ ⟨a, rfl⟩
  have : IsGLB (range ((↑) : ℚ → ℝ) ∩ Ioi a) a := by
    simp [isGLB_iff_le_iff, mem_lowerBounds, ← le_iff_forall_lt_rat_imp_le]
  rw [← this.biUnion_Ioi_eq, ← image_univ, ← image_inter_preimage, univ_inter, biUnion_image]
  exact MeasurableSet.biUnion (to_countable _)
    fun b _ => GenerateMeasurable.basic (Ioi (b : ℝ)) (by simp)

theorem borel_eq_generateFrom_Iic_rat : borel ℝ = .generateFrom (⋃ a : ℚ, {Iic (a : ℝ)}) := by
  rw [borel_eq_generateFrom_Ioi_rat, iUnion_singleton_eq_range, iUnion_singleton_eq_range]
  refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_) <;>
  rintro _ ⟨q, rfl⟩ <;>
  dsimp only <;>
  [rw [← compl_Iic]; rw [← compl_Ioi]] <;>
  exact MeasurableSet.compl (GenerateMeasurable.basic _ (mem_range_self q))

theorem borel_eq_generateFrom_Ici_rat : borel ℝ = .generateFrom (⋃ a : ℚ, {Ici (a : ℝ)}) := by
  rw [borel_eq_generateFrom_Iio_rat, iUnion_singleton_eq_range, iUnion_singleton_eq_range]
  refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_) <;>
  rintro _ ⟨q, rfl⟩ <;>
  dsimp only <;>
  [rw [← compl_Ici]; rw [← compl_Iio]] <;>
  exact MeasurableSet.compl (GenerateMeasurable.basic _ (mem_range_self q))

theorem isPiSystem_Ioo_rat :
    IsPiSystem (⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo (a : ℝ) (b : ℝ)}) := by
  convert isPiSystem_Ioo ((↑) : ℚ → ℝ) ((↑) : ℚ → ℝ)
  ext x
  simp [eq_comm]
#align real.is_pi_system_Ioo_rat Real.isPiSystem_Ioo_rat

theorem isPiSystem_Iio_rat : IsPiSystem (⋃ a : ℚ, {Iio (a : ℝ)}) := by
  convert isPiSystem_image_Iio (((↑) : ℚ → ℝ) '' univ)
  ext x
  simp only [iUnion_singleton_eq_range, mem_range, image_univ, mem_image, exists_exists_eq_and]

theorem isPiSystem_Ioi_rat : IsPiSystem (⋃ a : ℚ, {Ioi (a : ℝ)}) := by
  convert isPiSystem_image_Ioi (((↑) : ℚ → ℝ) '' univ)
  ext x
  simp only [iUnion_singleton_eq_range, mem_range, image_univ, mem_image, exists_exists_eq_and]

theorem isPiSystem_Iic_rat : IsPiSystem (⋃ a : ℚ, {Iic (a : ℝ)}) := by
  convert isPiSystem_image_Iic (((↑) : ℚ → ℝ) '' univ)
  ext x
  simp only [iUnion_singleton_eq_range, mem_range, image_univ, mem_image, exists_exists_eq_and]

theorem isPiSystem_Ici_rat : IsPiSystem (⋃ a : ℚ, {Ici (a : ℝ)}) := by
  convert isPiSystem_image_Ici (((↑) : ℚ → ℝ) '' univ)
  ext x
  simp only [iUnion_singleton_eq_range, mem_range, image_univ, mem_image, exists_exists_eq_and]

/-- 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 `ℝ`. -/
def finiteSpanningSetsInIooRat (μ : Measure ℝ) [IsLocallyFiniteMeasure μ] :
    μ.FiniteSpanningSetsIn (⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo (a : ℝ) (b : ℝ)}) where
  set n := Ioo (-(n + 1)) (n + 1)
  set_mem n := by
    simp only [mem_iUnion, mem_singleton_iff]
    refine' ⟨-(n + 1 : ℕ), n + 1, _, by simp⟩
    -- TODO: norm_cast fails here?
    push_cast
    exact neg_lt_self n.cast_add_one_pos
  finite n := measure_Ioo_lt_top
  spanning :=
    iUnion_eq_univ_iff.2 fun x =>
      ⟨⌊|x|⌋₊, neg_lt.1 ((neg_le_abs x).trans_lt (Nat.lt_floor_add_one _)),
        (le_abs_self x).trans_lt (Nat.lt_floor_add_one _)⟩
#align real.finite_spanning_sets_in_Ioo_rat Real.finiteSpanningSetsInIooRat

theorem measure_ext_Ioo_rat {μ ν : Measure ℝ} [IsLocallyFiniteMeasure μ]
    (h : ∀ a b : ℚ, μ (Ioo a b) = ν (Ioo a b)) : μ = ν :=
  (finiteSpanningSetsInIooRat μ).ext borel_eq_generateFrom_Ioo_rat isPiSystem_Ioo_rat <| by
    simp only [mem_iUnion, mem_singleton_iff]
    rintro _ ⟨a, b, -, rfl⟩
    apply h
#align real.measure_ext_Ioo_rat Real.measure_ext_Ioo_rat

end Real

variable [MeasurableSpace α]

@[measurability]
theorem measurable_real_toNNReal : Measurable Real.toNNReal :=
  continuous_real_toNNReal.measurable
#align measurable_real_to_nnreal measurable_real_toNNReal

@[measurability]
theorem Measurable.real_toNNReal {f : α → ℝ} (hf : Measurable f) :
    Measurable fun x => Real.toNNReal (f x) :=
  measurable_real_toNNReal.comp hf
#align measurable.real_to_nnreal Measurable.real_toNNReal

@[measurability]
theorem AEMeasurable.real_toNNReal {f : α → ℝ} {μ : Measure α} (hf : AEMeasurable f μ) :
    AEMeasurable (fun x => Real.toNNReal (f x)) μ :=
  measurable_real_toNNReal.comp_aemeasurable hf
#align ae_measurable.real_to_nnreal AEMeasurable.real_toNNReal

@[measurability]
theorem measurable_coe_nnreal_real : Measurable ((↑) : ℝ≥0 → ℝ) :=
  NNReal.continuous_coe.measurable
#align measurable_coe_nnreal_real measurable_coe_nnreal_real

@[measurability]
theorem Measurable.coe_nnreal_real {f : α → ℝ≥0} (hf : Measurable f) :
    Measurable fun x => (f x : ℝ) :=
  measurable_coe_nnreal_real.comp hf
#align measurable.coe_nnreal_real Measurable.coe_nnreal_real

@[measurability]
theorem AEMeasurable.coe_nnreal_real {f : α → ℝ≥0} {μ : Measure α} (hf : AEMeasurable f μ) :
    AEMeasurable (fun x => (f x : ℝ)) μ :=
  measurable_coe_nnreal_real.comp_aemeasurable hf
#align ae_measurable.coe_nnreal_real AEMeasurable.coe_nnreal_real

@[measurability]
theorem measurable_coe_nnreal_ennreal : Measurable ((↑) : ℝ≥0 → ℝ≥0∞) :=
  ENNReal.continuous_coe.measurable
#align measurable_coe_nnreal_ennreal measurable_coe_nnreal_ennreal

@[measurability]
theorem Measurable.coe_nnreal_ennreal {f : α → ℝ≥0} (hf : Measurable f) :
    Measurable fun x => (f x : ℝ≥0∞) :=
  ENNReal.continuous_coe.measurable.comp hf
#align measurable.coe_nnreal_ennreal Measurable.coe_nnreal_ennreal

@[measurability]
theorem AEMeasurable.coe_nnreal_ennreal {f : α → ℝ≥0} {μ : Measure α} (hf : AEMeasurable f μ) :
    AEMeasurable (fun x => (f x : ℝ≥0∞)) μ :=
  ENNReal.continuous_coe.measurable.comp_aemeasurable hf
#align ae_measurable.coe_nnreal_ennreal AEMeasurable.coe_nnreal_ennreal

@[measurability]
theorem Measurable.ennreal_ofReal {f : α → ℝ} (hf : Measurable f) :
    Measurable fun x => ENNReal.ofReal (f x) :=
  ENNReal.continuous_ofReal.measurable.comp hf
#align measurable.ennreal_of_real Measurable.ennreal_ofReal

@[measurability]
lemma AEMeasurable.ennreal_ofReal {f : α → ℝ} {μ : Measure α} (hf : AEMeasurable f μ) :
    AEMeasurable (fun x ↦ ENNReal.ofReal (f x)) μ :=
  ENNReal.continuous_ofReal.measurable.comp_aemeasurable hf

@[simp, norm_cast]
theorem measurable_coe_nnreal_real_iff {f : α → ℝ≥0} :
    Measurable (fun x => f x : α → ℝ) ↔ Measurable f :=
  ⟨fun h => by simpa only [Real.toNNReal_coe] using h.real_toNNReal, Measurable.coe_nnreal_real⟩
#align measurable_coe_nnreal_real_iff measurable_coe_nnreal_real_iff

@[simp, norm_cast]
theorem aemeasurable_coe_nnreal_real_iff {f : α → ℝ≥0} {μ : Measure α} :
    AEMeasurable (fun x => f x : α → ℝ) μ ↔ AEMeasurable f μ :=
  ⟨fun h => by simpa only [Real.toNNReal_coe] using h.real_toNNReal, AEMeasurable.coe_nnreal_real⟩
#align ae_measurable_coe_nnreal_real_iff aemeasurable_coe_nnreal_real_iff

@[deprecated] -- 2024-03-02
alias aEMeasurable_coe_nnreal_real_iff := aemeasurable_coe_nnreal_real_iff

/-- The set of finite `ℝ≥0∞` numbers is `MeasurableEquiv` to `ℝ≥0`. -/
def MeasurableEquiv.ennrealEquivNNReal : { r : ℝ≥0∞ | r ≠ ∞ } ≃ᵐ ℝ≥0 :=
  ENNReal.neTopHomeomorphNNReal.toMeasurableEquiv
#align measurable_equiv.ennreal_equiv_nnreal MeasurableEquiv.ennrealEquivNNReal

namespace ENNReal

theorem measurable_of_measurable_nnreal {f : ℝ≥0∞ → α} (h : Measurable fun p : ℝ≥0 => f p) :
    Measurable f :=
  measurable_of_measurable_on_compl_singleton ∞
    (MeasurableEquiv.ennrealEquivNNReal.symm.measurable_comp_iff.1 h)
#align ennreal.measurable_of_measurable_nnreal ENNReal.measurable_of_measurable_nnreal

/-- `ℝ≥0∞` is `MeasurableEquiv` to `ℝ≥0 ⊕ Unit`. -/
def ennrealEquivSum : ℝ≥0∞ ≃ᵐ Sum ℝ≥0 Unit :=
  { Equiv.optionEquivSumPUnit ℝ≥0 with
    measurable_toFun := measurable_of_measurable_nnreal measurable_inl
    measurable_invFun :=
      measurable_sum measurable_coe_nnreal_ennreal (@measurable_const ℝ≥0∞ Unit _ _ ∞) }
#align ennreal.ennreal_equiv_sum ENNReal.ennrealEquivSum

open Function (uncurry)

theorem measurable_of_measurable_nnreal_prod [MeasurableSpace β] [MeasurableSpace γ]
    {f : ℝ≥0∞ × β → γ} (H₁ : Measurable fun p : ℝ≥0 × β => f (p.1, p.2))
    (H₂ : Measurable fun x => f (∞, x)) : Measurable f :=
  let e : ℝ≥0∞ × β ≃ᵐ Sum (ℝ≥0 × β) (Unit × β) :=
    (ennrealEquivSum.prodCongr (MeasurableEquiv.refl β)).trans
      (MeasurableEquiv.sumProdDistrib _ _ _)
  e.symm.measurable_comp_iff.1 <| measurable_sum H₁ (H₂.comp measurable_id.snd)
#align ennreal.measurable_of_measurable_nnreal_prod ENNReal.measurable_of_measurable_nnreal_prod

theorem measurable_of_measurable_nnreal_nnreal [MeasurableSpace β] {f : ℝ≥0∞ × ℝ≥0∞ → β}
    (h₁ : Measurable fun p : ℝ≥0 × ℝ≥0 => f (p.1, p.2)) (h₂ : Measurable fun r : ℝ≥0 => f (∞, r))
    (h₃ : Measurable fun r : ℝ≥0 => f (r, ∞)) : Measurable f :=
  measurable_of_measurable_nnreal_prod
    (measurable_swap_iff.1 <| measurable_of_measurable_nnreal_prod (h₁.comp measurable_swap) h₃)
    (measurable_of_measurable_nnreal h₂)
#align ennreal.measurable_of_measurable_nnreal_nnreal ENNReal.measurable_of_measurable_nnreal_nnreal

@[measurability]
theorem measurable_ofReal : Measurable ENNReal.ofReal :=
  ENNReal.continuous_ofReal.measurable
#align ennreal.measurable_of_real ENNReal.measurable_ofReal

@[measurability]
theorem measurable_toReal : Measurable ENNReal.toReal :=
  ENNReal.measurable_of_measurable_nnreal measurable_coe_nnreal_real
#align ennreal.measurable_to_real ENNReal.measurable_toReal

@[measurability]
theorem measurable_toNNReal : Measurable ENNReal.toNNReal :=
  ENNReal.measurable_of_measurable_nnreal measurable_id
#align ennreal.measurable_to_nnreal ENNReal.measurable_toNNReal

instance instMeasurableMul₂ : MeasurableMul₂ ℝ≥0∞ := by
  refine' ⟨measurable_of_measurable_nnreal_nnreal _ _ _⟩
  · simp only [← ENNReal.coe_mul, measurable_mul.coe_nnreal_ennreal]
  · simp only [ENNReal.top_mul', ENNReal.coe_eq_zero]
    exact measurable_const.piecewise (measurableSet_singleton _) measurable_const
  · simp only [ENNReal.mul_top', ENNReal.coe_eq_zero]
    exact measurable_const.piecewise (measurableSet_singleton _) measurable_const
#align ennreal.has_measurable_mul₂ ENNReal.instMeasurableMul₂

instance instMeasurableSub₂ : MeasurableSub₂ ℝ≥0∞ :=
  ⟨by
    apply measurable_of_measurable_nnreal_nnreal <;>
      simp [← WithTop.coe_sub]; exact continuous_sub.measurable.coe_nnreal_ennreal⟩
#align ennreal.has_measurable_sub₂ ENNReal.instMeasurableSub₂

instance instMeasurableInv : MeasurableInv ℝ≥0∞ :=
  ⟨continuous_inv.measurable⟩
#align ennreal.has_measurable_inv ENNReal.instMeasurableInv

instance : MeasurableSMul ℝ≥0 ℝ≥0∞ where
  measurable_const_smul := by
    simp_rw [ENNReal.smul_def]
    exact fun _ ↦ MeasurableSMul.measurable_const_smul _
  measurable_smul_const := fun x ↦ by
    simp_rw [ENNReal.smul_def]
    exact measurable_coe_nnreal_ennreal.mul_const _

/-- A limit (over a general filter) of measurable `ℝ≥0∞` valued functions is measurable. -/
theorem measurable_of_tendsto' {ι : Type*} {f : ι → α → ℝ≥0∞} {g : α → ℝ≥0∞} (u : Filter ι)
    [NeBot u] [IsCountablyGenerated u] (hf : ∀ i, Measurable (f i)) (lim : Tendsto f u (𝓝 g)) :
    Measurable g := by
  rcases u.exists_seq_tendsto with ⟨x, hx⟩
  rw [tendsto_pi_nhds] at lim
  have : (fun y => liminf (fun n => (f (x n) y : ℝ≥0∞)) atTop) = g := by
    ext1 y
    exact ((lim y).comp hx).liminf_eq
  rw [← this]
  show Measurable fun y => liminf (fun n => (f (x n) y : ℝ≥0∞)) atTop
  exact measurable_liminf fun n => hf (x n)
#align measurable_of_tendsto_ennreal' ENNReal.measurable_of_tendsto'

-- 2024-03-09
@[deprecated] alias _root_.measurable_of_tendsto_ennreal' := ENNReal.measurable_of_tendsto'

/-- A sequential limit of measurable `ℝ≥0∞` valued functions is measurable. -/
theorem measurable_of_tendsto {f : ℕ → α → ℝ≥0∞} {g : α → ℝ≥0∞} (hf : ∀ i, Measurable (f i))
    (lim : Tendsto f atTop (𝓝 g)) : Measurable g :=
  measurable_of_tendsto' atTop hf lim
#align measurable_of_tendsto_ennreal ENNReal.measurable_of_tendsto

-- 2024-03-09
@[deprecated] alias _root_.measurable_of_tendsto_ennreal := ENNReal.measurable_of_tendsto

/-- A limit (over a general filter) of a.e.-measurable `ℝ≥0∞` valued functions is
a.e.-measurable. -/
lemma aemeasurable_of_tendsto' {ι : Type*} {f : ι → α → ℝ≥0∞} {g : α → ℝ≥0∞}
    {μ : Measure α} (u : Filter ι) [NeBot u] [IsCountablyGenerated u]
    (hf : ∀ i, AEMeasurable (f i) μ) (hlim : ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) u (𝓝 (g a))) :
    AEMeasurable g μ := by
  rcases u.exists_seq_tendsto with ⟨v, hv⟩
  have h'f : ∀ n, AEMeasurable (f (v n)) μ := fun n ↦ hf (v n)
  set p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Tendsto f' atTop (𝓝 (g x))
  have hp : ∀ᵐ x ∂μ, p x fun n ↦ f (v n) x := by
    filter_upwards [hlim] with x hx using hx.comp hv
  set aeSeqLim := fun x ↦ ite (x ∈ aeSeqSet h'f p) (g x) (⟨f (v 0) x⟩ : Nonempty ℝ≥0∞).some
  refine ⟨aeSeqLim, measurable_of_tendsto' atTop (aeSeq.measurable h'f p)
    (tendsto_pi_nhds.mpr fun x ↦ ?_), ?_⟩
  · unfold_let aeSeqLim
    simp_rw [aeSeq]
    split_ifs with hx
    · simp_rw [aeSeq.mk_eq_fun_of_mem_aeSeqSet h'f hx]
      exact aeSeq.fun_prop_of_mem_aeSeqSet h'f hx
    · exact tendsto_const_nhds
  · exact (ite_ae_eq_of_measure_compl_zero g (fun x ↦ (⟨f (v 0) x⟩ : Nonempty ℝ≥0∞).some)
      (aeSeqSet h'f p) (aeSeq.measure_compl_aeSeqSet_eq_zero h'f hp)).symm

/-- A limit of a.e.-measurable `ℝ≥0∞` valued functions is a.e.-measurable. -/
lemma aemeasurable_of_tendsto {f : ℕ → α → ℝ≥0∞} {g : α → ℝ≥0∞} {μ : Measure α}
    (hf : ∀ i, AEMeasurable (f i) μ) (hlim : ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (g a))) :
    AEMeasurable g μ :=
  aemeasurable_of_tendsto' atTop hf hlim

end ENNReal

@[measurability]
theorem Measurable.ennreal_toNNReal {f : α → ℝ≥0∞} (hf : Measurable f) :
    Measurable fun x => (f x).toNNReal :=
  ENNReal.measurable_toNNReal.comp hf
#align measurable.ennreal_to_nnreal Measurable.ennreal_toNNReal

@[measurability]
theorem AEMeasurable.ennreal_toNNReal {f : α → ℝ≥0∞} {μ : Measure α} (hf : AEMeasurable f μ) :
    AEMeasurable (fun x => (f x).toNNReal) μ :=
  ENNReal.measurable_toNNReal.comp_aemeasurable hf
#align ae_measurable.ennreal_to_nnreal AEMeasurable.ennreal_toNNReal

@[simp, norm_cast]
theorem measurable_coe_nnreal_ennreal_iff {f : α → ℝ≥0} :
    (Measurable fun x => (f x : ℝ≥0∞)) ↔ Measurable f :=
  ⟨fun h => h.ennreal_toNNReal, fun h => h.coe_nnreal_ennreal⟩
#align measurable_coe_nnreal_ennreal_iff measurable_coe_nnreal_ennreal_iff

@[simp, norm_cast]
theorem aemeasurable_coe_nnreal_ennreal_iff {f : α → ℝ≥0} {μ : Measure α} :
    AEMeasurable (fun x => (f x : ℝ≥0∞)) μ ↔ AEMeasurable f μ :=
  ⟨fun h => h.ennreal_toNNReal, fun h => h.coe_nnreal_ennreal⟩
#align ae_measurable_coe_nnreal_ennreal_iff aemeasurable_coe_nnreal_ennreal_iff

@[measurability]
theorem Measurable.ennreal_toReal {f : α → ℝ≥0∞} (hf : Measurable f) :
    Measurable fun x => ENNReal.toReal (f x) :=
  ENNReal.measurable_toReal.comp hf
#align measurable.ennreal_to_real Measurable.ennreal_toReal

@[measurability]
theorem AEMeasurable.ennreal_toReal {f : α → ℝ≥0∞} {μ : Measure α} (hf : AEMeasurable f μ) :
    AEMeasurable (fun x => ENNReal.toReal (f x)) μ :=
  ENNReal.measurable_toReal.comp_aemeasurable hf
#align ae_measurable.ennreal_to_real AEMeasurable.ennreal_toReal

/-- note: `ℝ≥0∞` can probably be generalized in a future version of this lemma. -/
@[measurability]
theorem Measurable.ennreal_tsum {ι} [Countable ι] {f : ι → α → ℝ≥0∞} (h : ∀ i, Measurable (f i)) :
    Measurable fun x => ∑' i, f i x := by
  simp_rw [ENNReal.tsum_eq_iSup_sum]
  apply measurable_iSup
  exact fun s => s.measurable_sum fun i _ => h i
#align measurable.ennreal_tsum Measurable.ennreal_tsum

@[measurability]
theorem Measurable.ennreal_tsum' {ι} [Countable ι] {f : ι → α → ℝ≥0∞} (h : ∀ i, Measurable (f i)) :
    Measurable (∑' i, f i) := by
  convert Measurable.ennreal_tsum h with x
  exact tsum_apply (Pi.summable.2 fun _ => ENNReal.summable)
#align measurable.ennreal_tsum' Measurable.ennreal_tsum'

@[measurability]
theorem Measurable.nnreal_tsum {ι} [Countable ι] {f : ι → α → ℝ≥0} (h : ∀ i, Measurable (f i)) :
    Measurable fun x => ∑' i, f i x := by
  simp_rw [NNReal.tsum_eq_toNNReal_tsum]
  exact (Measurable.ennreal_tsum fun i => (h i).coe_nnreal_ennreal).ennreal_toNNReal
#align measurable.nnreal_tsum Measurable.nnreal_tsum

@[measurability]
theorem AEMeasurable.ennreal_tsum {ι} [Countable ι] {f : ι → α → ℝ≥0∞} {μ : Measure α}
    (h : ∀ i, AEMeasurable (f i) μ) : AEMeasurable (fun x => ∑' i, f i x) μ := by
  simp_rw [ENNReal.tsum_eq_iSup_sum]
  apply aemeasurable_iSup
  exact fun s => Finset.aemeasurable_sum s fun i _ => h i
#align ae_measurable.ennreal_tsum AEMeasurable.ennreal_tsum

@[measurability]
theorem AEMeasurable.nnreal_tsum {α : Type*} [MeasurableSpace α] {ι : Type*} [Countable ι]
    {f : ι → α → NNReal} {μ : MeasureTheory.Measure α} (h : ∀ i : ι, AEMeasurable (f i) μ) :
    AEMeasurable (fun x : α => ∑' i : ι, f i x) μ := by
  simp_rw [NNReal.tsum_eq_toNNReal_tsum]
  exact (AEMeasurable.ennreal_tsum fun i => (h i).coe_nnreal_ennreal).ennreal_toNNReal
#align ae_measurable.nnreal_tsum AEMeasurable.nnreal_tsum

@[measurability]
theorem measurable_coe_real_ereal : Measurable ((↑) : ℝ → EReal) :=
  continuous_coe_real_ereal.measurable
#align measurable_coe_real_ereal measurable_coe_real_ereal

@[measurability]
theorem Measurable.coe_real_ereal {f : α → ℝ} (hf : Measurable f) :
    Measurable fun x => (f x : EReal) :=
  measurable_coe_real_ereal.comp hf
#align measurable.coe_real_ereal Measurable.coe_real_ereal

@[measurability]
theorem AEMeasurable.coe_real_ereal {f : α → ℝ} {μ : Measure α} (hf : AEMeasurable f μ) :
    AEMeasurable (fun x => (f x : EReal)) μ :=
  measurable_coe_real_ereal.comp_aemeasurable hf
#align ae_measurable.coe_real_ereal AEMeasurable.coe_real_ereal

/-- The set of finite `EReal` numbers is `MeasurableEquiv` to `ℝ`. -/
def MeasurableEquiv.erealEquivReal : ({⊥, ⊤}ᶜ : Set EReal) ≃ᵐ ℝ :=
  EReal.neBotTopHomeomorphReal.toMeasurableEquiv
#align measurable_equiv.ereal_equiv_real MeasurableEquiv.erealEquivReal

theorem EReal.measurable_of_measurable_real {f : EReal → α} (h : Measurable fun p : ℝ => f p) :
    Measurable f :=
  measurable_of_measurable_on_compl_finite {⊥, ⊤} (by simp)
    (MeasurableEquiv.erealEquivReal.symm.measurable_comp_iff.1 h)
#align ereal.measurable_of_measurable_real EReal.measurable_of_measurable_real

@[measurability]
theorem measurable_ereal_toReal : Measurable EReal.toReal :=
  EReal.measurable_of_measurable_real (by simpa using measurable_id)
#align measurable_ereal_to_real measurable_ereal_toReal

@[measurability]
theorem Measurable.ereal_toReal {f : α → EReal} (hf : Measurable f) :
    Measurable fun x => (f x).toReal :=
  measurable_ereal_toReal.comp hf
#align measurable.ereal_to_real Measurable.ereal_toReal

@[measurability]
theorem AEMeasurable.ereal_toReal {f : α → EReal} {μ : Measure α} (hf : AEMeasurable f μ) :
    AEMeasurable (fun x => (f x).toReal) μ :=
  measurable_ereal_toReal.comp_aemeasurable hf
#align ae_measurable.ereal_to_real AEMeasurable.ereal_toReal

@[measurability]
theorem measurable_coe_ennreal_ereal : Measurable ((↑) : ℝ≥0∞ → EReal) :=
  continuous_coe_ennreal_ereal.measurable
#align measurable_coe_ennreal_ereal measurable_coe_ennreal_ereal

@[measurability]
theorem Measurable.coe_ereal_ennreal {f : α → ℝ≥0∞} (hf : Measurable f) :
    Measurable fun x => (f x : EReal) :=
  measurable_coe_ennreal_ereal.comp hf
#align measurable.coe_ereal_ennreal Measurable.coe_ereal_ennreal

@[measurability]
theorem AEMeasurable.coe_ereal_ennreal {f : α → ℝ≥0∞} {μ : Measure α} (hf : AEMeasurable f μ) :
    AEMeasurable (fun x => (f x : EReal)) μ :=
  measurable_coe_ennreal_ereal.comp_aemeasurable hf
#align ae_measurable.coe_ereal_ennreal AEMeasurable.coe_ereal_ennreal

namespace NNReal

/-- A limit (over a general filter) of measurable `ℝ≥0` valued functions is measurable. -/
theorem measurable_of_tendsto' {ι} {f : ι → α → ℝ≥0} {g : α → ℝ≥0} (u : Filter ι) [NeBot u]
    [IsCountablyGenerated u] (hf : ∀ i, Measurable (f i)) (lim : Tendsto f u (𝓝 g)) :
    Measurable g := by
  simp_rw [← measurable_coe_nnreal_ennreal_iff] at hf ⊢
  refine' ENNReal.measurable_of_tendsto' u hf _
  rw [tendsto_pi_nhds] at lim ⊢
  exact fun x => (ENNReal.continuous_coe.tendsto (g x)).comp (lim x)
#align measurable_of_tendsto_nnreal' NNReal.measurable_of_tendsto'

-- 2024-03-09
@[deprecated] alias _root_.measurable_of_tendsto_nnreal' := NNReal.measurable_of_tendsto'

/-- A sequential limit of measurable `ℝ≥0` valued functions is measurable. -/
theorem measurable_of_tendsto {f : ℕ → α → ℝ≥0} {g : α → ℝ≥0} (hf : ∀ i, Measurable (f i))
    (lim : Tendsto f atTop (𝓝 g)) : Measurable g :=
  measurable_of_tendsto' atTop hf lim
#align measurable_of_tendsto_nnreal NNReal.measurable_of_tendsto

-- 2024-03-09
@[deprecated] alias _root_.measurable_of_tendsto_nnreal := NNReal.measurable_of_tendsto

end NNReal

/-- 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 exists_spanning_measurableSet_le {m : MeasurableSpace α} {f : α → ℝ≥0}
    (hf : Measurable f) (μ : Measure α) [SigmaFinite μ] :
    ∃ s : ℕ → Set α,
      (∀ n, MeasurableSet (s n) ∧ μ (s n) < ∞ ∧ ∀ x ∈ s n, f x ≤ n) ∧
      ⋃ i, s i = Set.univ := by
  let sigma_finite_sets := spanningSets μ
  let norm_sets := fun n : ℕ => { x | f x ≤ n }
  have norm_sets_spanning : ⋃ n, norm_sets n = Set.univ := by
    ext1 x
    simp only [Set.mem_iUnion, Set.mem_setOf_eq, Set.mem_univ, iff_true_iff]
    exact exists_nat_ge (f x)
  let sets n := sigma_finite_sets n ∩ norm_sets n
  have h_meas : ∀ n, MeasurableSet (sets n) := by
    refine' fun n => MeasurableSet.inter _ _
    · exact measurable_spanningSets μ n
    · exact hf measurableSet_Iic
  have h_finite : ∀ n, μ (sets n) < ∞ := by
    refine' fun n => (measure_mono (Set.inter_subset_left _ _)).trans_lt _
    exact measure_spanningSets_lt_top μ n
  refine' ⟨sets, fun n => ⟨h_meas n, h_finite n, _⟩, _⟩
  · exact fun x hx => hx.2
  · have :
      ⋃ i, sigma_finite_sets i ∩ norm_sets i = (⋃ i, sigma_finite_sets i) ∩ ⋃ i, norm_sets i := by
      refine' Set.iUnion_inter_of_monotone (monotone_spanningSets μ) fun i j hij x => _
      simp only [norm_sets, Set.mem_setOf_eq]
      refine' fun hif => hif.trans _
      exact mod_cast hij
    rw [this, norm_sets_spanning, iUnion_spanningSets μ, Set.inter_univ]

section NormedAddCommGroup

variable [NormedAddCommGroup α] [OpensMeasurableSpace α] [MeasurableSpace β]

@[measurability]
theorem measurable_norm : Measurable (norm : α → ℝ) :=
  continuous_norm.measurable
#align measurable_norm measurable_norm

@[measurability]
theorem Measurable.norm {f : β → α} (hf : Measurable f) : Measurable fun a => norm (f a) :=
  measurable_norm.comp hf
#align measurable.norm Measurable.norm

@[measurability]
theorem AEMeasurable.norm {f : β → α} {μ : Measure β} (hf : AEMeasurable f μ) :
    AEMeasurable (fun a => norm (f a)) μ :=
  measurable_norm.comp_aemeasurable hf
#align ae_measurable.norm AEMeasurable.norm

@[measurability]
theorem measurable_nnnorm : Measurable (nnnorm : α → ℝ≥0) :=
  continuous_nnnorm.measurable
#align measurable_nnnorm measurable_nnnorm

@[measurability]
theorem Measurable.nnnorm {f : β → α} (hf : Measurable f) : Measurable fun a => ‖f a‖₊ :=
  measurable_nnnorm.comp hf
#align measurable.nnnorm Measurable.nnnorm

@[measurability]
theorem AEMeasurable.nnnorm {f : β → α} {μ : Measure β} (hf : AEMeasurable f μ) :
    AEMeasurable (fun a => ‖f a‖₊) μ :=
  measurable_nnnorm.comp_aemeasurable hf
#align ae_measurable.nnnorm AEMeasurable.nnnorm

@[measurability]
theorem measurable_ennnorm : Measurable fun x : α => (‖x‖₊ : ℝ≥0∞) :=
  measurable_nnnorm.coe_nnreal_ennreal
#align measurable_ennnorm measurable_ennnorm

@[measurability]
theorem Measurable.ennnorm {f : β → α} (hf : Measurable f) : Measurable fun a => (‖f a‖₊ : ℝ≥0∞) :=
  hf.nnnorm.coe_nnreal_ennreal
#align measurable.ennnorm Measurable.ennnorm

@[measurability]
theorem AEMeasurable.ennnorm {f : β → α} {μ : Measure β} (hf : AEMeasurable f μ) :
    AEMeasurable (fun a => (‖f a‖₊ : ℝ≥0∞)) μ :=
  measurable_ennnorm.comp_aemeasurable hf
#align ae_measurable.ennnorm AEMeasurable.ennnorm

end NormedAddCommGroup