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:
has_measurable_supsays that both left and right sup are measurable;has_measurable_sup₂says thatλ p : α × α, p.1 ⊔ p.2is measurable,
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]
- measurable_const_sup : ∀ (c : M), measurable (has_sup.sup c)
- measurable_sup_const : ∀ (c : M), measurable (λ (_x : M), _x ⊔ c)
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]
- measurable_sup : measurable (λ (p : M × M), p.fst ⊔ p.snd)
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]
- measurable_const_inf : ∀ (c : M), measurable (has_inf.inf c)
- measurable_inf_const : ∀ (c : M), measurable (λ (_x : M), _x ⊓ c)
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]
- measurable_inf : measurable (λ (p : M × M), p.fst ⊓ p.snd)
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
@[protected, instance]
def
order_dual.has_measurable_sup
{M : Type u_1}
[measurable_space M]
[has_inf M]
[has_measurable_inf M] :
@[protected, instance]
def
order_dual.has_measurable_inf
{M : Type u_1}
[measurable_space M]
[has_sup M]
[has_measurable_sup M] :
@[protected, instance]
def
order_dual.has_measurable_sup₂
{M : Type u_1}
[measurable_space M]
[has_inf M]
[has_measurable_inf₂ M] :
@[protected, instance]
def
order_dual.has_measurable_inf₂
{M : Type u_1}
[measurable_space M]
[has_sup M]
[has_measurable_sup₂ M] :
@[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) :
measurable (f ⊔ 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 μ) :
ae_measurable (f ⊔ 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) μ
@[protected, instance]
def
has_measurable_sup₂.to_has_measurable_sup
{M : Type u_1}
[measurable_space M]
[has_sup M]
[has_measurable_sup₂ M] :
@[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) :
measurable (f ⊓ 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 μ) :
ae_measurable (f ⊓ 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) μ
@[protected, instance]
def
has_measurable_inf₂.to_has_measurable_inf
{M : Type u_1}
[measurable_space M]
[has_inf M]
[has_measurable_inf₂ M] :
@[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)) :
measurable ((finset.range (n + 1)).sup' finset.nonempty_range_succ 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)) :
measurable (λ (x : δ), (finset.range (n + 1)).sup' finset.nonempty_range_succ (λ (k : ℕ), f k x))