Documentation

Mathlib.MeasureTheory.Order.Lattice

Typeclasses for measurability of lattice operations #

In this file we define classes MeasurableSup and MeasurableInf and prove dot-style lemmas (Measurable.sup, AEMeasurable.sup etc). For binary operations we define two typeclasses:

and similarly for other binary operations. The reason for introducing these classes is that in case of topological space α equipped with the Borel σ-algebra, instances for MeasurableSup₂ etc require α to have a second countable topology.

For instances relating, e.g., ContinuousSup to MeasurableSup see file MeasureTheory.BorelSpace.

Tags #

measurable function, lattice operation

class MeasurableSup (M : Type u_1) [MeasurableSpace M] [Sup M] :

We say that a type has MeasurableSup if (c ⊔ ·) and (· ⊔ c) are measurable functions. For a typeclass assuming measurability of uncurry (· ⊔ ·) see MeasurableSup₂.

  • measurable_const_sup : ∀ (c : M), Measurable fun (x : M) => c x
  • measurable_sup_const : ∀ (c : M), Measurable fun (x : M) => x c
Instances
    theorem MeasurableSup.measurable_const_sup {M : Type u_1} :
    ∀ {inst : MeasurableSpace M} {inst_1 : Sup M} [self : MeasurableSup M] (c : M), Measurable fun (x : M) => c x
    theorem MeasurableSup.measurable_sup_const {M : Type u_1} :
    ∀ {inst : MeasurableSpace M} {inst_1 : Sup M} [self : MeasurableSup M] (c : M), Measurable fun (x : M) => x c
    class MeasurableSup₂ (M : Type u_1) [MeasurableSpace M] [Sup M] :

    We say that a type has MeasurableSup₂ if uncurry (· ⊔ ·) is a measurable functions. For a typeclass assuming measurability of (c ⊔ ·) and (· ⊔ c) see MeasurableSup.

    Instances
      theorem MeasurableSup₂.measurable_sup {M : Type u_1} :
      ∀ {inst : MeasurableSpace M} {inst_1 : Sup M} [self : MeasurableSup₂ M], Measurable fun (p : M × M) => p.1 p.2
      class MeasurableInf (M : Type u_1) [MeasurableSpace M] [Inf M] :

      We say that a type has MeasurableInf if (c ⊓ ·) and (· ⊓ c) are measurable functions. For a typeclass assuming measurability of uncurry (· ⊓ ·) see MeasurableInf₂.

      • measurable_const_inf : ∀ (c : M), Measurable fun (x : M) => c x
      • measurable_inf_const : ∀ (c : M), Measurable fun (x : M) => x c
      Instances
        theorem MeasurableInf.measurable_const_inf {M : Type u_1} :
        ∀ {inst : MeasurableSpace M} {inst_1 : Inf M} [self : MeasurableInf M] (c : M), Measurable fun (x : M) => c x
        theorem MeasurableInf.measurable_inf_const {M : Type u_1} :
        ∀ {inst : MeasurableSpace M} {inst_1 : Inf M} [self : MeasurableInf M] (c : M), Measurable fun (x : M) => x c
        class MeasurableInf₂ (M : Type u_1) [MeasurableSpace M] [Inf M] :

        We say that a type has MeasurableInf₂ if uncurry (· ⊓ ·) is a measurable functions. For a typeclass assuming measurability of (c ⊓ ·) and (· ⊓ c) see MeasurableInf.

        Instances
          theorem MeasurableInf₂.measurable_inf {M : Type u_1} :
          ∀ {inst : MeasurableSpace M} {inst_1 : Inf M} [self : MeasurableInf₂ M], Measurable fun (p : M × M) => p.1 p.2
          @[instance 100]
          Equations
          • =
          @[instance 100]
          Equations
          • =
          @[instance 100]
          Equations
          • =
          @[instance 100]
          Equations
          • =
          theorem Measurable.const_sup {M : Type u_1} [MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {f : αM} [Sup M] [MeasurableSup M] (hf : Measurable f) (c : M) :
          Measurable fun (x : α) => c f x
          theorem AEMeasurable.const_sup {M : Type u_1} [MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αM} [Sup M] [MeasurableSup M] (hf : AEMeasurable f μ) (c : M) :
          AEMeasurable (fun (x : α) => c f x) μ
          theorem Measurable.sup_const {M : Type u_1} [MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {f : αM} [Sup M] [MeasurableSup M] (hf : Measurable f) (c : M) :
          Measurable fun (x : α) => f x c
          theorem AEMeasurable.sup_const {M : Type u_1} [MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αM} [Sup M] [MeasurableSup M] (hf : AEMeasurable f μ) (c : M) :
          AEMeasurable (fun (x : α) => f x c) μ
          theorem Measurable.sup' {M : Type u_1} [MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {f : αM} {g : αM} [Sup M] [MeasurableSup₂ M] (hf : Measurable f) (hg : Measurable g) :
          theorem Measurable.sup {M : Type u_1} [MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {f : αM} {g : αM} [Sup M] [MeasurableSup₂ M] (hf : Measurable f) (hg : Measurable g) :
          Measurable fun (a : α) => f a g a
          theorem AEMeasurable.sup' {M : Type u_1} [MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αM} {g : αM} [Sup M] [MeasurableSup₂ M] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
          AEMeasurable (f g) μ
          theorem AEMeasurable.sup {M : Type u_1} [MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αM} {g : αM} [Sup M] [MeasurableSup₂ M] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
          AEMeasurable (fun (a : α) => f a g a) μ
          @[instance 100]
          Equations
          • =
          theorem Measurable.const_inf {M : Type u_1} [MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {f : αM} [Inf M] [MeasurableInf M] (hf : Measurable f) (c : M) :
          Measurable fun (x : α) => c f x
          theorem AEMeasurable.const_inf {M : Type u_1} [MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αM} [Inf M] [MeasurableInf M] (hf : AEMeasurable f μ) (c : M) :
          AEMeasurable (fun (x : α) => c f x) μ
          theorem Measurable.inf_const {M : Type u_1} [MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {f : αM} [Inf M] [MeasurableInf M] (hf : Measurable f) (c : M) :
          Measurable fun (x : α) => f x c
          theorem AEMeasurable.inf_const {M : Type u_1} [MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αM} [Inf M] [MeasurableInf M] (hf : AEMeasurable f μ) (c : M) :
          AEMeasurable (fun (x : α) => f x c) μ
          theorem Measurable.inf' {M : Type u_1} [MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {f : αM} {g : αM} [Inf M] [MeasurableInf₂ M] (hf : Measurable f) (hg : Measurable g) :
          theorem Measurable.inf {M : Type u_1} [MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {f : αM} {g : αM} [Inf M] [MeasurableInf₂ M] (hf : Measurable f) (hg : Measurable g) :
          Measurable fun (a : α) => f a g a
          theorem AEMeasurable.inf' {M : Type u_1} [MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αM} {g : αM} [Inf M] [MeasurableInf₂ M] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
          AEMeasurable (f g) μ
          theorem AEMeasurable.inf {M : Type u_1} [MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αM} {g : αM} [Inf M] [MeasurableInf₂ M] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
          AEMeasurable (fun (a : α) => f a g a) μ
          @[instance 100]
          Equations
          • =
          theorem Finset.measurable_sup' {α : Type u_2} {m : MeasurableSpace α} {δ : Type u_3} [MeasurableSpace δ] [SemilatticeSup α] [MeasurableSup₂ α] {ι : Type u_4} {s : Finset ι} (hs : s.Nonempty) {f : ιδα} (hf : ns, Measurable (f n)) :
          Measurable (s.sup' hs f)
          theorem Finset.measurable_range_sup' {α : Type u_2} {m : MeasurableSpace α} {δ : Type u_3} [MeasurableSpace δ] [SemilatticeSup α] [MeasurableSup₂ α] {f : δα} {n : } (hf : kn, Measurable (f k)) :
          Measurable ((Finset.range (n + 1)).sup' f)
          theorem Finset.measurable_range_sup'' {α : Type u_2} {m : MeasurableSpace α} {δ : Type u_3} [MeasurableSpace δ] [SemilatticeSup α] [MeasurableSup₂ α] {f : δα} {n : } (hf : kn, Measurable (f k)) :
          Measurable fun (x : δ) => (Finset.range (n + 1)).sup' fun (k : ) => f k x