mathlib3 documentation

measure_theory.lattice

Typeclasses for measurability of lattice operations #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define classes has_measurable_sup and has_measurable_inf and prove dot-style lemmas (measurable.sup, ae_measurable.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 has_measurable_sup₂ etc require α to have a second countable topology.

For instances relating, e.g., has_continuous_sup to has_measurable_sup see file measure_theory.borel_space.

Tags #

measurable function, lattice operation

@[class]
structure has_measurable_sup (M : Type u_1) [measurable_space M] [has_sup M] :
Prop

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

Instances of this typeclass
@[class]
structure has_measurable_sup₂ (M : Type u_1) [measurable_space M] [has_sup M] :
Prop

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

Instances of this typeclass
@[class]
structure has_measurable_inf (M : Type u_1) [measurable_space M] [has_inf M] :
Prop

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

Instances of this typeclass
@[class]
structure has_measurable_inf₂ (M : Type u_1) [measurable_space M] [has_inf M] :
Prop

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

Instances of this typeclass
@[measurability]
theorem measurable.const_sup {M : Type u_1} [measurable_space M] {α : Type u_2} {m : measurable_space α} {f : α M} [has_sup M] [has_measurable_sup M] (hf : measurable f) (c : M) :
measurable (λ (x : α), c f x)
@[measurability]
theorem ae_measurable.const_sup {M : Type u_1} [measurable_space M] {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α M} [has_sup M] [has_measurable_sup M] (hf : ae_measurable f μ) (c : M) :
ae_measurable (λ (x : α), c f x) μ
@[measurability]
theorem measurable.sup_const {M : Type u_1} [measurable_space M] {α : Type u_2} {m : measurable_space α} {f : α M} [has_sup M] [has_measurable_sup M] (hf : measurable f) (c : M) :
measurable (λ (x : α), f x c)
@[measurability]
theorem ae_measurable.sup_const {M : Type u_1} [measurable_space M] {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α M} [has_sup M] [has_measurable_sup M] (hf : ae_measurable f μ) (c : M) :
ae_measurable (λ (x : α), f x c) μ
@[measurability]
theorem measurable.sup' {M : Type u_1} [measurable_space M] {α : Type u_2} {m : measurable_space α} {f g : α M} [has_sup M] [has_measurable_sup₂ M] (hf : measurable f) (hg : measurable g) :
@[measurability]
theorem measurable.sup {M : Type u_1} [measurable_space M] {α : Type u_2} {m : measurable_space α} {f g : α M} [has_sup M] [has_measurable_sup₂ M] (hf : measurable f) (hg : measurable g) :
measurable (λ (a : α), f a g a)
@[measurability]
theorem ae_measurable.sup' {M : Type u_1} [measurable_space M] {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α M} [has_sup M] [has_measurable_sup₂ M] (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
@[measurability]
theorem ae_measurable.sup {M : Type u_1} [measurable_space M] {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α M} [has_sup M] [has_measurable_sup₂ M] (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (λ (a : α), f a g a) μ
@[measurability]
theorem measurable.const_inf {M : Type u_1} [measurable_space M] {α : Type u_2} {m : measurable_space α} {f : α M} [has_inf M] [has_measurable_inf M] (hf : measurable f) (c : M) :
measurable (λ (x : α), c f x)
@[measurability]
theorem ae_measurable.const_inf {M : Type u_1} [measurable_space M] {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α M} [has_inf M] [has_measurable_inf M] (hf : ae_measurable f μ) (c : M) :
ae_measurable (λ (x : α), c f x) μ
@[measurability]
theorem measurable.inf_const {M : Type u_1} [measurable_space M] {α : Type u_2} {m : measurable_space α} {f : α M} [has_inf M] [has_measurable_inf M] (hf : measurable f) (c : M) :
measurable (λ (x : α), f x c)
@[measurability]
theorem ae_measurable.inf_const {M : Type u_1} [measurable_space M] {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α M} [has_inf M] [has_measurable_inf M] (hf : ae_measurable f μ) (c : M) :
ae_measurable (λ (x : α), f x c) μ
@[measurability]
theorem measurable.inf' {M : Type u_1} [measurable_space M] {α : Type u_2} {m : measurable_space α} {f g : α M} [has_inf M] [has_measurable_inf₂ M] (hf : measurable f) (hg : measurable g) :
@[measurability]
theorem measurable.inf {M : Type u_1} [measurable_space M] {α : Type u_2} {m : measurable_space α} {f g : α M} [has_inf M] [has_measurable_inf₂ M] (hf : measurable f) (hg : measurable g) :
measurable (λ (a : α), f a g a)
@[measurability]
theorem ae_measurable.inf' {M : Type u_1} [measurable_space M] {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α M} [has_inf M] [has_measurable_inf₂ M] (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
@[measurability]
theorem ae_measurable.inf {M : Type u_1} [measurable_space M] {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α M} [has_inf M] [has_measurable_inf₂ M] (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (λ (a : α), f a g a) μ
@[measurability]
theorem finset.measurable_sup' {α : Type u_2} {m : measurable_space α} {δ : Type u_3} [measurable_space δ] [semilattice_sup α] [has_measurable_sup₂ α] {ι : Type u_1} {s : finset ι} (hs : s.nonempty) {f : ι δ α} (hf : (n : ι), n s measurable (f n)) :
measurable (s.sup' hs f)
@[measurability]
theorem finset.measurable_range_sup' {α : Type u_2} {m : measurable_space α} {δ : Type u_3} [measurable_space δ] [semilattice_sup α] [has_measurable_sup₂ α] {f : δ α} {n : } (hf : (k : ), k n measurable (f k)) :
@[measurability]
theorem finset.measurable_range_sup'' {α : Type u_2} {m : measurable_space α} {δ : Type u_3} [measurable_space δ] [semilattice_sup α] [has_measurable_sup₂ α] {f : δ α} {n : } (hf : (k : ), k n measurable (f k)) :
measurable (λ (x : δ), (finset.range (n + 1)).sup' finset.nonempty_range_succ (λ (k : ), f k x))