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:
MeasurableSupsays that both left and right sup are measurable;MeasurableSup₂says thatfun 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 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
- measurable_const_sup : ∀ (c : M), Measurable fun x => c ⊔ x
- measurable_sup_const : ∀ (c : M), Measurable fun x => x ⊔ c
We say that a type has MeasurableSup if (c ⊔ ·) and (· ⊔ c) are measurable functions.
For a typeclass assuming measurability of uncurry (· ⊔ ·) see MeasurableSup₂.
Instances
- measurable_sup : Measurable fun p => p.fst ⊔ p.snd
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
- measurable_const_inf : ∀ (c : M), Measurable fun x => c ⊓ x
- measurable_inf_const : ∀ (c : M), Measurable fun x => x ⊓ c
We say that a type has MeasurableInf if (c ⊓ ·) and (· ⊓ c) are measurable functions.
For a typeclass assuming measurability of uncurry (· ⊓ ·) see MeasurableInf₂.
Instances
- measurable_inf : Measurable fun p => p.fst ⊓ p.snd
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
instance
OrderDual.instMeasurableSup₂
{M : Type u_1}
[MeasurableSpace M]
[Inf M]
[MeasurableInf₂ M]
:
instance
OrderDual.instMeasurableInf₂
{M : Type u_1}
[MeasurableSpace M]
[Sup M]
[MeasurableSup₂ M]
:
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)
:
Measurable (f ⊔ 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
MeasurableSup₂.toMeasurableSup
{M : Type u_1}
[MeasurableSpace M]
[Sup M]
[MeasurableSup₂ M]
:
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)
:
Measurable (f ⊓ 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
MeasurableInf₂.to_hasMeasurableInf
{M : Type u_1}
[MeasurableSpace M]
[Inf M]
[MeasurableInf₂ M]
:
theorem
Finset.measurable_sup'
{α : Type u_2}
{m : MeasurableSpace α}
{δ : Type u_3}
[MeasurableSpace δ]
[SemilatticeSup α]
[MeasurableSup₂ α]
{ι : Type u_4}
{s : Finset ι}
(hs : Finset.Nonempty s)
{f : ι → δ → α}
(hf : ∀ (n : ι), n ∈ s → Measurable (f n))
:
Measurable (Finset.sup' s hs f)
theorem
Finset.measurable_range_sup'
{α : Type u_2}
{m : MeasurableSpace α}
{δ : Type u_3}
[MeasurableSpace δ]
[SemilatticeSup α]
[MeasurableSup₂ α]
{f : ℕ → δ → α}
{n : ℕ}
(hf : ∀ (k : ℕ), k ≤ n → Measurable (f k))
:
Measurable (Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) f)
theorem
Finset.measurable_range_sup''
{α : Type u_2}
{m : MeasurableSpace α}
{δ : Type u_3}
[MeasurableSpace δ]
[SemilatticeSup α]
[MeasurableSup₂ α]
{f : ℕ → δ → α}
{n : ℕ}
(hf : ∀ (k : ℕ), k ≤ n → Measurable (f k))
:
Measurable fun x => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) fun k => f k x