mathlib documentation

measure_theory.lattice

Typeclasses for measurability of lattice operations #

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
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)
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) μ
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)
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) μ
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) :
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)
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 μ) :
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) μ
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)
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) μ
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)
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) μ
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) :
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)
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 μ) :
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) μ