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
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}
[MeasurableSpace M]
[Sup M]
[self : MeasurableSup M]
(c : M)
:
Measurable fun (x : M) => c ⊔ x
theorem
MeasurableSup.measurable_sup_const
{M : Type u_1}
[MeasurableSpace M]
[Sup M]
[self : MeasurableSup M]
(c : M)
:
Measurable fun (x : M) => x ⊔ c
We say that a type has MeasurableSup₂ if uncurry (· ⊔ ·) is a measurable functions.
For a typeclass assuming measurability of (c ⊔ ·) and (· ⊔ c) see MeasurableSup.
- measurable_sup : Measurable fun (p : M × M) => p.1 ⊔ p.2
Instances
theorem
MeasurableSup₂.measurable_sup
{M : Type u_1}
[MeasurableSpace M]
[Sup M]
[self : MeasurableSup₂ M]
:
Measurable fun (p : M × M) => p.1 ⊔ p.2
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}
[MeasurableSpace M]
[Inf M]
[self : MeasurableInf M]
(c : M)
:
Measurable fun (x : M) => c ⊓ x
theorem
MeasurableInf.measurable_inf_const
{M : Type u_1}
[MeasurableSpace M]
[Inf M]
[self : MeasurableInf M]
(c : M)
:
Measurable fun (x : M) => x ⊓ c
We say that a type has MeasurableInf₂ if uncurry (· ⊓ ·) is a measurable functions.
For a typeclass assuming measurability of (c ⊓ ·) and (· ⊓ c) see MeasurableInf.
- measurable_inf : Measurable fun (p : M × M) => p.1 ⊓ p.2
Instances
theorem
MeasurableInf₂.measurable_inf
{M : Type u_1}
[MeasurableSpace M]
[Inf M]
[self : MeasurableInf₂ M]
:
Measurable fun (p : M × M) => p.1 ⊓ p.2
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
instance
OrderDual.instMeasurableSup₂
{M : Type u_1}
[MeasurableSpace M]
[Inf M]
[MeasurableInf₂ M]
:
Equations
- ⋯ = ⋯
instance
OrderDual.instMeasurableInf₂
{M : Type u_1}
[MeasurableSpace M]
[Sup M]
[MeasurableSup₂ M]
:
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)
:
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]
:
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)
:
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]
:
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 : ∀ n ∈ s, 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 : ∀ k ≤ n, 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 : ∀ k ≤ n, Measurable (f k))
:
Measurable fun (x : δ) => (Finset.range (n + 1)).sup' ⋯ fun (k : ℕ) => f k x