Typeclasses for measurability of operations #
In this file we define classes MeasurableMul etc and prove dot-style lemmas
(Measurable.mul, AEMeasurable.mul etc). For binary operations we define two typeclasses:
MeasurableMulsays that both left and right multiplication are measurable;MeasurableMul₂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 MeasurableMul₂
etc require α to have a second countable topology.
We define separate classes for MeasurableDiv/MeasurableSub
because on some types (e.g., ℕ, ℝ≥0∞) division and/or subtraction are not defined as a * b⁻¹ /
a + (-b).
For instances relating, e.g., ContinuousMul to MeasurableMul see file
MeasureTheory.BorelSpace.
Implementation notes #
For the heuristics of @[to_additive] it is important that the type with a multiplication
(or another multiplicative operations) is the first (implicit) argument of all declarations.
Tags #
measurable function, arithmetic operator
Todo #
- Uniformize the treatment of
powandsmul. - Use
@[to_additive]to sendMeasurablePowtoMeasurableSMul₂. - This might require changing the definition (swapping the arguments in the function that is
in the conclusion of
MeasurableSMul.)
Binary operations: (· + ·), (· * ·), (· - ·), (· / ·) #
- measurable_const_add : ∀ (c : M), Measurable fun x => c + x
- measurable_add_const : ∀ (c : M), Measurable fun x => x + c
We say that a type has MeasurableAdd if (· + c) and (· + c) are measurable functions.
For a typeclass assuming measurability of uncurry (· + ·) see MeasurableAdd₂.
Instances
- measurable_add : Measurable fun p => p.fst + p.snd
We say that a type has MeasurableAdd₂ if uncurry (· + ·) is a measurable functions.
For a typeclass assuming measurability of (c + ·) and (· + c) see MeasurableAdd.
Instances
- measurable_const_mul : ∀ (c : M), Measurable fun x => c * x
- measurable_mul_const : ∀ (c : M), Measurable fun x => x * c
We say that a type has MeasurableMul if (c * ·) and (· * c) are measurable functions.
For a typeclass assuming measurability of uncurry (*) see MeasurableMul₂.
Instances
- measurable_mul : Measurable fun p => p.fst * p.snd
We say that a type has MeasurableMul₂ if uncurry (· * ·) is a measurable functions.
For a typeclass assuming measurability of (c * ·) and (· * c) see MeasurableMul.
Instances
theorem
Measurable.const_add
{M : Type u_1}
{α : Type u_2}
[MeasurableSpace M]
[Add M]
{m : MeasurableSpace α}
{f : α → M}
[MeasurableAdd M]
(hf : Measurable f)
(c : M)
:
Measurable fun x => c + f x
theorem
Measurable.const_mul
{M : Type u_1}
{α : Type u_2}
[MeasurableSpace M]
[Mul M]
{m : MeasurableSpace α}
{f : α → M}
[MeasurableMul M]
(hf : Measurable f)
(c : M)
:
Measurable fun x => c * f x
theorem
AEMeasurable.const_add
{M : Type u_1}
{α : Type u_2}
[MeasurableSpace M]
[Add M]
{m : MeasurableSpace α}
{f : α → M}
{μ : MeasureTheory.Measure α}
[MeasurableAdd M]
(hf : AEMeasurable f)
(c : M)
:
AEMeasurable fun x => c + f x
theorem
AEMeasurable.const_mul
{M : Type u_1}
{α : Type u_2}
[MeasurableSpace M]
[Mul M]
{m : MeasurableSpace α}
{f : α → M}
{μ : MeasureTheory.Measure α}
[MeasurableMul M]
(hf : AEMeasurable f)
(c : M)
:
AEMeasurable fun x => c * f x
theorem
Measurable.add_const
{M : Type u_1}
{α : Type u_2}
[MeasurableSpace M]
[Add M]
{m : MeasurableSpace α}
{f : α → M}
[MeasurableAdd M]
(hf : Measurable f)
(c : M)
:
Measurable fun x => f x + c
theorem
Measurable.mul_const
{M : Type u_1}
{α : Type u_2}
[MeasurableSpace M]
[Mul M]
{m : MeasurableSpace α}
{f : α → M}
[MeasurableMul M]
(hf : Measurable f)
(c : M)
:
Measurable fun x => f x * c
theorem
AEMeasurable.add_const
{M : Type u_1}
{α : Type u_2}
[MeasurableSpace M]
[Add M]
{m : MeasurableSpace α}
{f : α → M}
{μ : MeasureTheory.Measure α}
[MeasurableAdd M]
(hf : AEMeasurable f)
(c : M)
:
AEMeasurable fun x => f x + c
theorem
AEMeasurable.mul_const
{M : Type u_1}
{α : Type u_2}
[MeasurableSpace M]
[Mul M]
{m : MeasurableSpace α}
{f : α → M}
{μ : MeasureTheory.Measure α}
[MeasurableMul M]
(hf : AEMeasurable f)
(c : M)
:
AEMeasurable fun x => f x * c
theorem
Measurable.add'
{M : Type u_1}
{α : Type u_2}
[MeasurableSpace M]
[Add M]
{m : MeasurableSpace α}
{f : α → M}
{g : α → M}
[MeasurableAdd₂ M]
(hf : Measurable f)
(hg : Measurable g)
:
Measurable (f + g)
theorem
Measurable.mul'
{M : Type u_1}
{α : Type u_2}
[MeasurableSpace M]
[Mul M]
{m : MeasurableSpace α}
{f : α → M}
{g : α → M}
[MeasurableMul₂ M]
(hf : Measurable f)
(hg : Measurable g)
:
Measurable (f * g)
theorem
Measurable.add
{M : Type u_1}
{α : Type u_2}
[MeasurableSpace M]
[Add M]
{m : MeasurableSpace α}
{f : α → M}
{g : α → M}
[MeasurableAdd₂ M]
(hf : Measurable f)
(hg : Measurable g)
:
Measurable fun a => f a + g a
theorem
Measurable.mul
{M : Type u_1}
{α : Type u_2}
[MeasurableSpace M]
[Mul M]
{m : MeasurableSpace α}
{f : α → M}
{g : α → M}
[MeasurableMul₂ M]
(hf : Measurable f)
(hg : Measurable g)
:
Measurable fun a => f a * g a
theorem
AEMeasurable.add'
{M : Type u_1}
{α : Type u_2}
[MeasurableSpace M]
[Add M]
{m : MeasurableSpace α}
{f : α → M}
{g : α → M}
{μ : MeasureTheory.Measure α}
[MeasurableAdd₂ M]
(hf : AEMeasurable f)
(hg : AEMeasurable g)
:
AEMeasurable (f + g)
theorem
AEMeasurable.mul'
{M : Type u_1}
{α : Type u_2}
[MeasurableSpace M]
[Mul M]
{m : MeasurableSpace α}
{f : α → M}
{g : α → M}
{μ : MeasureTheory.Measure α}
[MeasurableMul₂ M]
(hf : AEMeasurable f)
(hg : AEMeasurable g)
:
AEMeasurable (f * g)
theorem
AEMeasurable.add
{M : Type u_1}
{α : Type u_2}
[MeasurableSpace M]
[Add M]
{m : MeasurableSpace α}
{f : α → M}
{g : α → M}
{μ : MeasureTheory.Measure α}
[MeasurableAdd₂ M]
(hf : AEMeasurable f)
(hg : AEMeasurable g)
:
AEMeasurable fun a => f a + g a
theorem
AEMeasurable.mul
{M : Type u_1}
{α : Type u_2}
[MeasurableSpace M]
[Mul M]
{m : MeasurableSpace α}
{f : α → M}
{g : α → M}
{μ : MeasureTheory.Measure α}
[MeasurableMul₂ M]
(hf : AEMeasurable f)
(hg : AEMeasurable g)
:
AEMeasurable fun a => f a * g a
instance
MeasurableAdd₂.toMeasurableAdd
{M : Type u_1}
[MeasurableSpace M]
[Add M]
[MeasurableAdd₂ M]
:
theorem
MeasurableAdd₂.toMeasurableAdd.proof_1
{M : Type u_1}
[MeasurableSpace M]
[Add M]
[MeasurableAdd₂ M]
:
instance
MeasurableMul₂.toMeasurableMul
{M : Type u_1}
[MeasurableSpace M]
[Mul M]
[MeasurableMul₂ M]
:
theorem
Pi.measurableAdd.proof_1
{ι : Type u_1}
{α : ι → Type u_2}
[(i : ι) → Add (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableAdd (α i)]
:
MeasurableAdd ((i : ι) → α i)
instance
Pi.measurableAdd
{ι : Type u_3}
{α : ι → Type u_4}
[(i : ι) → Add (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableAdd (α i)]
:
MeasurableAdd ((i : ι) → α i)
Equations
instance
Pi.measurableMul
{ι : Type u_3}
{α : ι → Type u_4}
[(i : ι) → Mul (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableMul (α i)]
:
MeasurableMul ((i : ι) → α i)
Equations
theorem
Pi.measurableAdd₂.proof_1
{ι : Type u_1}
{α : ι → Type u_2}
[(i : ι) → Add (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableAdd₂ (α i)]
:
MeasurableAdd₂ ((i : ι) → α i)
instance
Pi.measurableAdd₂
{ι : Type u_3}
{α : ι → Type u_4}
[(i : ι) → Add (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableAdd₂ (α i)]
:
MeasurableAdd₂ ((i : ι) → α i)
instance
Pi.measurableMul₂
{ι : Type u_3}
{α : ι → Type u_4}
[(i : ι) → Mul (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableMul₂ (α i)]
:
MeasurableMul₂ ((i : ι) → α i)
theorem
measurable_sub_const'
{G : Type u_1}
[SubNegMonoid G]
[MeasurableSpace G]
[MeasurableAdd G]
(g : G)
:
Measurable fun h => h - g
A version of measurable_sub_const that assumes MeasurableAdd instead of
MeasurableSub. This can be nice to avoid unnecessary type-class assumptions.
theorem
measurable_div_const'
{G : Type u_1}
[DivInvMonoid G]
[MeasurableSpace G]
[MeasurableMul G]
(g : G)
:
Measurable fun h => h / g
A version of measurable_div_const that assumes MeasurableMul instead of
MeasurableDiv. This can be nice to avoid unnecessary type-class assumptions.
class
MeasurablePow
(β : Type u_1)
(γ : Type u_2)
[MeasurableSpace β]
[MeasurableSpace γ]
[Pow β γ]
:
- measurable_pow : Measurable fun p => p.fst ^ p.snd
This class assumes that the map β × γ → β given by (x, y) ↦ x ^ y is measurable.
Instances
Monoid.Pow is measurable.
theorem
Measurable.pow
{β : Type u_1}
{γ : Type u_2}
{α : Type u_3}
[MeasurableSpace β]
[MeasurableSpace γ]
[Pow β γ]
[MeasurablePow β γ]
{m : MeasurableSpace α}
{f : α → β}
{g : α → γ}
(hf : Measurable f)
(hg : Measurable g)
:
Measurable fun x => f x ^ g x
theorem
AEMeasurable.pow
{β : Type u_1}
{γ : Type u_2}
{α : Type u_3}
[MeasurableSpace β]
[MeasurableSpace γ]
[Pow β γ]
[MeasurablePow β γ]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → β}
{g : α → γ}
(hf : AEMeasurable f)
(hg : AEMeasurable g)
:
AEMeasurable fun x => f x ^ g x
theorem
Measurable.pow_const
{β : Type u_1}
{γ : Type u_2}
{α : Type u_3}
[MeasurableSpace β]
[MeasurableSpace γ]
[Pow β γ]
[MeasurablePow β γ]
{m : MeasurableSpace α}
{f : α → β}
(hf : Measurable f)
(c : γ)
:
Measurable fun x => f x ^ c
theorem
AEMeasurable.pow_const
{β : Type u_1}
{γ : Type u_2}
{α : Type u_3}
[MeasurableSpace β]
[MeasurableSpace γ]
[Pow β γ]
[MeasurablePow β γ]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f)
(c : γ)
:
AEMeasurable fun x => f x ^ c
theorem
Measurable.const_pow
{β : Type u_1}
{γ : Type u_2}
{α : Type u_3}
[MeasurableSpace β]
[MeasurableSpace γ]
[Pow β γ]
[MeasurablePow β γ]
{m : MeasurableSpace α}
{g : α → γ}
(hg : Measurable g)
(c : β)
:
Measurable fun x => c ^ g x
theorem
AEMeasurable.const_pow
{β : Type u_1}
{γ : Type u_2}
{α : Type u_3}
[MeasurableSpace β]
[MeasurableSpace γ]
[Pow β γ]
[MeasurablePow β γ]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{g : α → γ}
(hg : AEMeasurable g)
(c : β)
:
AEMeasurable fun x => c ^ g x
- measurable_const_sub : ∀ (c : G), Measurable fun x => c - x
- measurable_sub_const : ∀ (c : G), Measurable fun x => x - c
We say that a type has MeasurableSub if (c - ·) and (· - c) are measurable
functions. For a typeclass assuming measurability of uncurry (-) see MeasurableSub₂.
Instances
- measurable_sub : Measurable fun p => p.fst - p.snd
We say that a type has MeasurableSub₂ if uncurry (· - ·) is a measurable functions.
For a typeclass assuming measurability of (c - ·) and (· - c) see MeasurableSub.
Instances
- measurable_const_div : ∀ (c : G₀), Measurable fun x => c / x
- measurable_div_const : ∀ (c : G₀), Measurable fun x => x / c
We say that a type has MeasurableDiv if (c / ·) and (· / c) are measurable functions.
For a typeclass assuming measurability of uncurry (· / ·) see MeasurableDiv₂.
Instances
- measurable_div : Measurable fun p => p.fst / p.snd
We say that a type has MeasurableDiv₂ if uncurry (· / ·) is a measurable functions.
For a typeclass assuming measurability of (c / ·) and (· / c) see MeasurableDiv.
Instances
theorem
Measurable.const_sub
{G : Type u_1}
{α : Type u_2}
[MeasurableSpace G]
[Sub G]
{m : MeasurableSpace α}
{f : α → G}
[MeasurableSub G]
(hf : Measurable f)
(c : G)
:
Measurable fun x => c - f x
theorem
Measurable.const_div
{G : Type u_1}
{α : Type u_2}
[MeasurableSpace G]
[Div G]
{m : MeasurableSpace α}
{f : α → G}
[MeasurableDiv G]
(hf : Measurable f)
(c : G)
:
Measurable fun x => c / f x
theorem
AEMeasurable.const_sub
{G : Type u_1}
{α : Type u_2}
[MeasurableSpace G]
[Sub G]
{m : MeasurableSpace α}
{f : α → G}
{μ : MeasureTheory.Measure α}
[MeasurableSub G]
(hf : AEMeasurable f)
(c : G)
:
AEMeasurable fun x => c - f x
theorem
AEMeasurable.const_div
{G : Type u_1}
{α : Type u_2}
[MeasurableSpace G]
[Div G]
{m : MeasurableSpace α}
{f : α → G}
{μ : MeasureTheory.Measure α}
[MeasurableDiv G]
(hf : AEMeasurable f)
(c : G)
:
AEMeasurable fun x => c / f x
theorem
Measurable.sub_const
{G : Type u_1}
{α : Type u_2}
[MeasurableSpace G]
[Sub G]
{m : MeasurableSpace α}
{f : α → G}
[MeasurableSub G]
(hf : Measurable f)
(c : G)
:
Measurable fun x => f x - c
theorem
Measurable.div_const
{G : Type u_1}
{α : Type u_2}
[MeasurableSpace G]
[Div G]
{m : MeasurableSpace α}
{f : α → G}
[MeasurableDiv G]
(hf : Measurable f)
(c : G)
:
Measurable fun x => f x / c
theorem
AEMeasurable.sub_const
{G : Type u_1}
{α : Type u_2}
[MeasurableSpace G]
[Sub G]
{m : MeasurableSpace α}
{f : α → G}
{μ : MeasureTheory.Measure α}
[MeasurableSub G]
(hf : AEMeasurable f)
(c : G)
:
AEMeasurable fun x => f x - c
theorem
AEMeasurable.div_const
{G : Type u_1}
{α : Type u_2}
[MeasurableSpace G]
[Div G]
{m : MeasurableSpace α}
{f : α → G}
{μ : MeasureTheory.Measure α}
[MeasurableDiv G]
(hf : AEMeasurable f)
(c : G)
:
AEMeasurable fun x => f x / c
theorem
Measurable.sub'
{G : Type u_1}
{α : Type u_2}
[MeasurableSpace G]
[Sub G]
{m : MeasurableSpace α}
{f : α → G}
{g : α → G}
[MeasurableSub₂ G]
(hf : Measurable f)
(hg : Measurable g)
:
Measurable (f - g)
theorem
Measurable.div'
{G : Type u_1}
{α : Type u_2}
[MeasurableSpace G]
[Div G]
{m : MeasurableSpace α}
{f : α → G}
{g : α → G}
[MeasurableDiv₂ G]
(hf : Measurable f)
(hg : Measurable g)
:
Measurable (f / g)
theorem
Measurable.sub
{G : Type u_1}
{α : Type u_2}
[MeasurableSpace G]
[Sub G]
{m : MeasurableSpace α}
{f : α → G}
{g : α → G}
[MeasurableSub₂ G]
(hf : Measurable f)
(hg : Measurable g)
:
Measurable fun a => f a - g a
theorem
Measurable.div
{G : Type u_1}
{α : Type u_2}
[MeasurableSpace G]
[Div G]
{m : MeasurableSpace α}
{f : α → G}
{g : α → G}
[MeasurableDiv₂ G]
(hf : Measurable f)
(hg : Measurable g)
:
Measurable fun a => f a / g a
theorem
AEMeasurable.sub'
{G : Type u_1}
{α : Type u_2}
[MeasurableSpace G]
[Sub G]
{m : MeasurableSpace α}
{f : α → G}
{g : α → G}
{μ : MeasureTheory.Measure α}
[MeasurableSub₂ G]
(hf : AEMeasurable f)
(hg : AEMeasurable g)
:
AEMeasurable (f - g)
theorem
AEMeasurable.div'
{G : Type u_1}
{α : Type u_2}
[MeasurableSpace G]
[Div G]
{m : MeasurableSpace α}
{f : α → G}
{g : α → G}
{μ : MeasureTheory.Measure α}
[MeasurableDiv₂ G]
(hf : AEMeasurable f)
(hg : AEMeasurable g)
:
AEMeasurable (f / g)
theorem
AEMeasurable.sub
{G : Type u_1}
{α : Type u_2}
[MeasurableSpace G]
[Sub G]
{m : MeasurableSpace α}
{f : α → G}
{g : α → G}
{μ : MeasureTheory.Measure α}
[MeasurableSub₂ G]
(hf : AEMeasurable f)
(hg : AEMeasurable g)
:
AEMeasurable fun a => f a - g a
theorem
AEMeasurable.div
{G : Type u_1}
{α : Type u_2}
[MeasurableSpace G]
[Div G]
{m : MeasurableSpace α}
{f : α → G}
{g : α → G}
{μ : MeasureTheory.Measure α}
[MeasurableDiv₂ G]
(hf : AEMeasurable f)
(hg : AEMeasurable g)
:
AEMeasurable fun a => f a / g a
theorem
MeasurableSub₂.toMeasurableSub.proof_1
{G : Type u_1}
[MeasurableSpace G]
[Sub G]
[MeasurableSub₂ G]
:
instance
MeasurableSub₂.toMeasurableSub
{G : Type u_1}
[MeasurableSpace G]
[Sub G]
[MeasurableSub₂ G]
:
instance
MeasurableDiv₂.toMeasurableDiv
{G : Type u_1}
[MeasurableSpace G]
[Div G]
[MeasurableDiv₂ G]
:
theorem
Pi.measurableSub.proof_1
{ι : Type u_1}
{α : ι → Type u_2}
[(i : ι) → Sub (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableSub (α i)]
:
MeasurableSub ((i : ι) → α i)
instance
Pi.measurableSub
{ι : Type u_3}
{α : ι → Type u_4}
[(i : ι) → Sub (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableSub (α i)]
:
MeasurableSub ((i : ι) → α i)
Equations
instance
Pi.measurableDiv
{ι : Type u_3}
{α : ι → Type u_4}
[(i : ι) → Div (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableDiv (α i)]
:
MeasurableDiv ((i : ι) → α i)
Equations
theorem
Pi.measurableSub₂.proof_1
{ι : Type u_1}
{α : ι → Type u_2}
[(i : ι) → Sub (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableSub₂ (α i)]
:
MeasurableSub₂ ((i : ι) → α i)
instance
Pi.measurableSub₂
{ι : Type u_3}
{α : ι → Type u_4}
[(i : ι) → Sub (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableSub₂ (α i)]
:
MeasurableSub₂ ((i : ι) → α i)
instance
Pi.measurableDiv₂
{ι : Type u_3}
{α : ι → Type u_4}
[(i : ι) → Div (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableDiv₂ (α i)]
:
MeasurableDiv₂ ((i : ι) → α i)
theorem
measurableSet_eq_fun
{α : Type u_2}
{m : MeasurableSpace α}
{E : Type u_3}
[MeasurableSpace E]
[AddGroup E]
[MeasurableSingletonClass E]
[MeasurableSub₂ E]
{f : α → E}
{g : α → E}
(hf : Measurable f)
(hg : Measurable g)
:
MeasurableSet {x | f x = g x}
theorem
nullMeasurableSet_eq_fun
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_3}
[MeasurableSpace E]
[AddGroup E]
[MeasurableSingletonClass E]
[MeasurableSub₂ E]
{f : α → E}
{g : α → E}
(hf : AEMeasurable f)
(hg : AEMeasurable g)
:
MeasureTheory.NullMeasurableSet {x | f x = g x}
theorem
measurableSet_eq_fun_of_countable
{α : Type u_2}
{m : MeasurableSpace α}
{E : Type u_3}
[MeasurableSpace E]
[MeasurableSingletonClass E]
[Countable E]
{f : α → E}
{g : α → E}
(hf : Measurable f)
(hg : Measurable g)
:
MeasurableSet {x | f x = g x}
theorem
ae_eq_trim_of_measurable
{α : Type u_3}
{E : Type u_4}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasurableSpace E]
[AddGroup E]
[MeasurableSingletonClass E]
[MeasurableSub₂ E]
(hm : m ≤ m0)
{f : α → E}
{g : α → E}
(hf : Measurable f)
(hg : Measurable g)
(hfg : f =ᶠ[MeasureTheory.Measure.ae μ] g)
:
- measurable_neg : Measurable Neg.neg
We say that a type has MeasurableNeg if x ↦ -x is a measurable function.
Instances
- measurable_inv : Measurable Inv.inv
We say that a type has MeasurableInv if x ↦ x⁻¹ is a measurable function.
Instances
instance
measurableSub_of_add_neg
(G : Type u_1)
[MeasurableSpace G]
[SubNegMonoid G]
[MeasurableAdd G]
[MeasurableNeg G]
:
theorem
measurableSub_of_add_neg.proof_1
(G : Type u_1)
[MeasurableSpace G]
[SubNegMonoid G]
[MeasurableAdd G]
[MeasurableNeg G]
:
instance
measurableDiv_of_mul_inv
(G : Type u_1)
[MeasurableSpace G]
[DivInvMonoid G]
[MeasurableMul G]
[MeasurableInv G]
:
theorem
Measurable.neg
{G : Type u_1}
{α : Type u_2}
[Neg G]
[MeasurableSpace G]
[MeasurableNeg G]
{m : MeasurableSpace α}
{f : α → G}
(hf : Measurable f)
:
Measurable fun x => -f x
theorem
Measurable.inv
{G : Type u_1}
{α : Type u_2}
[Inv G]
[MeasurableSpace G]
[MeasurableInv G]
{m : MeasurableSpace α}
{f : α → G}
(hf : Measurable f)
:
Measurable fun x => (f x)⁻¹
theorem
AEMeasurable.neg
{G : Type u_1}
{α : Type u_2}
[Neg G]
[MeasurableSpace G]
[MeasurableNeg G]
{m : MeasurableSpace α}
{f : α → G}
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f)
:
AEMeasurable fun x => -f x
theorem
AEMeasurable.inv
{G : Type u_1}
{α : Type u_2}
[Inv G]
[MeasurableSpace G]
[MeasurableInv G]
{m : MeasurableSpace α}
{f : α → G}
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f)
:
AEMeasurable fun x => (f x)⁻¹
@[simp]
theorem
measurable_neg_iff
{α : Type u_2}
{m : MeasurableSpace α}
{G : Type u_3}
[AddGroup G]
[MeasurableSpace G]
[MeasurableNeg G]
{f : α → G}
:
(Measurable fun x => -f x) ↔ Measurable f
@[simp]
theorem
measurable_inv_iff
{α : Type u_2}
{m : MeasurableSpace α}
{G : Type u_3}
[Group G]
[MeasurableSpace G]
[MeasurableInv G]
{f : α → G}
:
(Measurable fun x => (f x)⁻¹) ↔ Measurable f
@[simp]
theorem
aemeasurable_neg_iff
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G : Type u_3}
[AddGroup G]
[MeasurableSpace G]
[MeasurableNeg G]
{f : α → G}
:
(AEMeasurable fun x => -f x) ↔ AEMeasurable f
@[simp]
theorem
aemeasurable_inv_iff
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G : Type u_3}
[Group G]
[MeasurableSpace G]
[MeasurableInv G]
{f : α → G}
:
(AEMeasurable fun x => (f x)⁻¹) ↔ AEMeasurable f
@[simp]
theorem
measurable_inv_iff₀
{α : Type u_2}
{m : MeasurableSpace α}
{G₀ : Type u_3}
[GroupWithZero G₀]
[MeasurableSpace G₀]
[MeasurableInv G₀]
{f : α → G₀}
:
(Measurable fun x => (f x)⁻¹) ↔ Measurable f
@[simp]
theorem
aemeasurable_inv_iff₀
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G₀ : Type u_3}
[GroupWithZero G₀]
[MeasurableSpace G₀]
[MeasurableInv G₀]
{f : α → G₀}
:
(AEMeasurable fun x => (f x)⁻¹) ↔ AEMeasurable f
instance
Pi.measurableNeg
{ι : Type u_3}
{α : ι → Type u_4}
[(i : ι) → Neg (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableNeg (α i)]
:
MeasurableNeg ((i : ι) → α i)
Equations
theorem
Pi.measurableNeg.proof_1
{ι : Type u_1}
{α : ι → Type u_2}
[(i : ι) → Neg (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableNeg (α i)]
:
MeasurableNeg ((i : ι) → α i)
instance
Pi.measurableInv
{ι : Type u_3}
{α : ι → Type u_4}
[(i : ι) → Inv (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableInv (α i)]
:
MeasurableInv ((i : ι) → α i)
Equations
theorem
MeasurableSet.neg
{G : Type u_1}
[Neg G]
[MeasurableSpace G]
[MeasurableNeg G]
{s : Set G}
(hs : MeasurableSet s)
:
MeasurableSet (-s)
theorem
MeasurableSet.inv
{G : Type u_1}
[Inv G]
[MeasurableSpace G]
[MeasurableInv G]
{s : Set G}
(hs : MeasurableSet s)
:
instance
DivInvMonoid.measurableZpow
(G : Type u)
[DivInvMonoid G]
[MeasurableSpace G]
[MeasurableMul₂ G]
[MeasurableInv G]
:
DivInvMonoid.Pow is measurable.
instance
measurableDiv₂_of_add_neg
(G : Type u_1)
[MeasurableSpace G]
[SubNegMonoid G]
[MeasurableAdd₂ G]
[MeasurableNeg G]
:
theorem
measurableDiv₂_of_add_neg.proof_1
(G : Type u_1)
[MeasurableSpace G]
[SubNegMonoid G]
[MeasurableAdd₂ G]
[MeasurableNeg G]
:
instance
measurableDiv₂_of_mul_inv
(G : Type u_1)
[MeasurableSpace G]
[DivInvMonoid G]
[MeasurableMul₂ G]
[MeasurableInv G]
:
class
MeasurableVAdd
(M : Type u_1)
(α : Type u_2)
[VAdd M α]
[MeasurableSpace M]
[MeasurableSpace α]
:
- measurable_const_vadd : ∀ (c : M), Measurable ((fun x x_1 => x +ᵥ x_1) c)
- measurable_vadd_const : ∀ (x : α), Measurable fun c => c +ᵥ x
We say that the action of M on α has MeasurableVAdd if for each c the map x ↦ c +ᵥ x
is a measurable function and for each x the map c ↦ c +ᵥ x is a measurable function.
Instances
class
MeasurableSMul
(M : Type u_1)
(α : Type u_2)
[SMul M α]
[MeasurableSpace M]
[MeasurableSpace α]
:
- measurable_const_smul : ∀ (c : M), Measurable ((fun x x_1 => x • x_1) c)
- measurable_smul_const : ∀ (x : α), Measurable fun c => c • x
We say that the action of M on α has MeasurableSMul if for each c the map x ↦ c • x
is a measurable function and for each x the map c ↦ c • x is a measurable function.
Instances
class
MeasurableVAdd₂
(M : Type u_1)
(α : Type u_2)
[VAdd M α]
[MeasurableSpace M]
[MeasurableSpace α]
:
- measurable_vadd : Measurable (Function.uncurry fun x x_1 => x +ᵥ x_1)
We say that the action of M on α has MeasurableVAdd₂ if the map
(c, x) ↦ c +ᵥ x is a measurable function.
Instances
class
MeasurableSMul₂
(M : Type u_1)
(α : Type u_2)
[SMul M α]
[MeasurableSpace M]
[MeasurableSpace α]
:
- measurable_smul : Measurable (Function.uncurry fun x x_1 => x • x_1)
We say that the action of M on α has Measurable_SMul₂ if the map
(c, x) ↦ c • x is a measurable function.
Instances
theorem
measurableVAdd_of_add.proof_1
(M : Type u_1)
[Add M]
[MeasurableSpace M]
[MeasurableAdd M]
:
MeasurableVAdd M M
instance
measurableVAdd_of_add
(M : Type u_1)
[Add M]
[MeasurableSpace M]
[MeasurableAdd M]
:
MeasurableVAdd M M
instance
measurableSMul_of_mul
(M : Type u_1)
[Mul M]
[MeasurableSpace M]
[MeasurableMul M]
:
MeasurableSMul M M
instance
measurableSMul₂_of_add
(M : Type u_1)
[Add M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
:
MeasurableVAdd₂ M M
theorem
measurableSMul₂_of_add.proof_1
(M : Type u_1)
[Add M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
:
MeasurableVAdd₂ M M
instance
measurableSMul₂_of_mul
(M : Type u_1)
[Mul M]
[MeasurableSpace M]
[MeasurableMul₂ M]
:
MeasurableSMul₂ M M
instance
AddSubmonoid.measurableVAdd
{M : Type u_1}
{α : Type u_2}
[MeasurableSpace M]
[MeasurableSpace α]
[AddMonoid M]
[AddAction M α]
[MeasurableVAdd M α]
(s : AddSubmonoid M)
:
MeasurableVAdd { x // x ∈ s } α
theorem
AddSubmonoid.measurableVAdd.proof_1
{M : Type u_1}
{α : Type u_2}
[MeasurableSpace M]
[MeasurableSpace α]
[AddMonoid M]
[AddAction M α]
[MeasurableVAdd M α]
(s : AddSubmonoid M)
:
MeasurableVAdd { x // x ∈ s } α
instance
Submonoid.measurableSMul
{M : Type u_1}
{α : Type u_2}
[MeasurableSpace M]
[MeasurableSpace α]
[Monoid M]
[MulAction M α]
[MeasurableSMul M α]
(s : Submonoid M)
:
MeasurableSMul { x // x ∈ s } α
instance
AddSubgroup.measurableVAdd
{G : Type u_1}
{α : Type u_2}
[MeasurableSpace G]
[MeasurableSpace α]
[AddGroup G]
[AddAction G α]
[MeasurableVAdd G α]
(s : AddSubgroup G)
:
MeasurableVAdd { x // x ∈ s } α
theorem
AddSubgroup.measurableVAdd.proof_1
{G : Type u_1}
{α : Type u_2}
[MeasurableSpace G]
[MeasurableSpace α]
[AddGroup G]
[AddAction G α]
[MeasurableVAdd G α]
(s : AddSubgroup G)
:
MeasurableVAdd { x // x ∈ s.toAddSubmonoid } α
instance
Subgroup.measurableSMul
{G : Type u_1}
{α : Type u_2}
[MeasurableSpace G]
[MeasurableSpace α]
[Group G]
[MulAction G α]
[MeasurableSMul G α]
(s : Subgroup G)
:
MeasurableSMul { x // x ∈ s } α
theorem
Measurable.vadd
{M : Type u_1}
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[VAdd M β]
{m : MeasurableSpace α}
{f : α → M}
{g : α → β}
[MeasurableVAdd₂ M β]
(hf : Measurable f)
(hg : Measurable g)
:
Measurable fun x => f x +ᵥ g x
theorem
Measurable.smul
{M : Type u_1}
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[SMul M β]
{m : MeasurableSpace α}
{f : α → M}
{g : α → β}
[MeasurableSMul₂ M β]
(hf : Measurable f)
(hg : Measurable g)
:
Measurable fun x => f x • g x
theorem
AEMeasurable.vadd
{M : Type u_1}
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[VAdd M β]
{m : MeasurableSpace α}
{f : α → M}
{g : α → β}
[MeasurableVAdd₂ M β]
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f)
(hg : AEMeasurable g)
:
AEMeasurable fun x => f x +ᵥ g x
theorem
AEMeasurable.smul
{M : Type u_1}
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[SMul M β]
{m : MeasurableSpace α}
{f : α → M}
{g : α → β}
[MeasurableSMul₂ M β]
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f)
(hg : AEMeasurable g)
:
AEMeasurable fun x => f x • g x
instance
MeasurableVAdd₂.toMeasurableVAdd
{M : Type u_1}
{β : Type u_2}
[MeasurableSpace M]
[MeasurableSpace β]
[VAdd M β]
[MeasurableVAdd₂ M β]
:
MeasurableVAdd M β
theorem
MeasurableVAdd₂.toMeasurableVAdd.proof_1
{M : Type u_1}
{β : Type u_2}
[MeasurableSpace M]
[MeasurableSpace β]
[VAdd M β]
[MeasurableVAdd₂ M β]
:
MeasurableVAdd M β
instance
MeasurableSMul₂.toMeasurableSMul
{M : Type u_1}
{β : Type u_2}
[MeasurableSpace M]
[MeasurableSpace β]
[SMul M β]
[MeasurableSMul₂ M β]
:
MeasurableSMul M β
theorem
Measurable.vadd_const
{M : Type u_1}
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[VAdd M β]
{m : MeasurableSpace α}
{f : α → M}
[MeasurableVAdd M β]
(hf : Measurable f)
(y : β)
:
Measurable fun x => f x +ᵥ y
theorem
Measurable.smul_const
{M : Type u_1}
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[SMul M β]
{m : MeasurableSpace α}
{f : α → M}
[MeasurableSMul M β]
(hf : Measurable f)
(y : β)
:
Measurable fun x => f x • y
theorem
AEMeasurable.vadd_const
{M : Type u_1}
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[VAdd M β]
{m : MeasurableSpace α}
{f : α → M}
[MeasurableVAdd M β]
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f)
(y : β)
:
AEMeasurable fun x => f x +ᵥ y
theorem
AEMeasurable.smul_const
{M : Type u_1}
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[SMul M β]
{m : MeasurableSpace α}
{f : α → M}
[MeasurableSMul M β]
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f)
(y : β)
:
AEMeasurable fun x => f x • y
theorem
Measurable.const_vadd'
{M : Type u_1}
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[VAdd M β]
{m : MeasurableSpace α}
{g : α → β}
[MeasurableVAdd M β]
(hg : Measurable g)
(c : M)
:
Measurable fun x => c +ᵥ g x
theorem
Measurable.const_smul'
{M : Type u_1}
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[SMul M β]
{m : MeasurableSpace α}
{g : α → β}
[MeasurableSMul M β]
(hg : Measurable g)
(c : M)
:
Measurable fun x => c • g x
theorem
Measurable.const_vadd
{M : Type u_1}
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[VAdd M β]
{m : MeasurableSpace α}
{g : α → β}
[MeasurableVAdd M β]
(hg : Measurable g)
(c : M)
:
Measurable (c +ᵥ g)
theorem
Measurable.const_smul
{M : Type u_1}
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[SMul M β]
{m : MeasurableSpace α}
{g : α → β}
[MeasurableSMul M β]
(hg : Measurable g)
(c : M)
:
Measurable (c • g)
theorem
AEMeasurable.const_vadd'
{M : Type u_1}
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[VAdd M β]
{m : MeasurableSpace α}
{g : α → β}
[MeasurableVAdd M β]
{μ : MeasureTheory.Measure α}
(hg : AEMeasurable g)
(c : M)
:
AEMeasurable fun x => c +ᵥ g x
theorem
AEMeasurable.const_smul'
{M : Type u_1}
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[SMul M β]
{m : MeasurableSpace α}
{g : α → β}
[MeasurableSMul M β]
{μ : MeasureTheory.Measure α}
(hg : AEMeasurable g)
(c : M)
:
AEMeasurable fun x => c • g x
theorem
AEMeasurable.const_vadd
{M : Type u_1}
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[VAdd M β]
{m : MeasurableSpace α}
{g : α → β}
[MeasurableVAdd M β]
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable g)
(c : M)
:
AEMeasurable (c +ᵥ g)
theorem
AEMeasurable.const_smul
{M : Type u_1}
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[SMul M β]
{m : MeasurableSpace α}
{g : α → β}
[MeasurableSMul M β]
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable g)
(c : M)
:
AEMeasurable (c • g)
instance
Pi.measurableVAdd
{M : Type u_1}
[MeasurableSpace M]
{ι : Type u_4}
{α : ι → Type u_5}
[(i : ι) → VAdd M (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableVAdd M (α i)]
:
MeasurableVAdd M ((i : ι) → α i)
theorem
Pi.measurableVAdd.proof_1
{M : Type u_1}
[MeasurableSpace M]
{ι : Type u_2}
{α : ι → Type u_3}
[(i : ι) → VAdd M (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableVAdd M (α i)]
:
MeasurableVAdd M ((i : ι) → α i)
instance
Pi.measurableSMul
{M : Type u_1}
[MeasurableSpace M]
{ι : Type u_4}
{α : ι → Type u_5}
[(i : ι) → SMul M (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableSMul M (α i)]
:
MeasurableSMul M ((i : ι) → α i)
instance
AddMonoid.measurableSMul_nat₂
(M : Type u_4)
[AddMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
:
AddMonoid.SMul is measurable.
instance
SubNegMonoid.measurableSMul_int₂
(M : Type u_4)
[SubNegMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
[MeasurableNeg M]
:
SubNegMonoid.SMulInt is measurable.
theorem
measurable_const_vadd_iff
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace β]
[MeasurableSpace α]
{f : α → β}
{G : Type u_4}
[AddGroup G]
[MeasurableSpace G]
[AddAction G β]
[MeasurableVAdd G β]
(c : G)
:
(Measurable fun x => c +ᵥ f x) ↔ Measurable f
theorem
measurable_const_smul_iff
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace β]
[MeasurableSpace α]
{f : α → β}
{G : Type u_4}
[Group G]
[MeasurableSpace G]
[MulAction G β]
[MeasurableSMul G β]
(c : G)
:
(Measurable fun x => c • f x) ↔ Measurable f
theorem
aemeasurable_const_vadd_iff
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace β]
[MeasurableSpace α]
{f : α → β}
{μ : MeasureTheory.Measure α}
{G : Type u_4}
[AddGroup G]
[MeasurableSpace G]
[AddAction G β]
[MeasurableVAdd G β]
(c : G)
:
(AEMeasurable fun x => c +ᵥ f x) ↔ AEMeasurable f
theorem
aemeasurable_const_smul_iff
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace β]
[MeasurableSpace α]
{f : α → β}
{μ : MeasureTheory.Measure α}
{G : Type u_4}
[Group G]
[MeasurableSpace G]
[MulAction G β]
[MeasurableSMul G β]
(c : G)
:
(AEMeasurable fun x => c • f x) ↔ AEMeasurable f
Equations
- AddUnits.instMeasurableSpace = MeasurableSpace.comap AddUnits.val inst
Equations
- Units.instMeasurableSpace = MeasurableSpace.comap Units.val inst
theorem
AddUnits.measurableVAdd.proof_1
{M : Type u_1}
{β : Type u_2}
[MeasurableSpace M]
[MeasurableSpace β]
[AddMonoid M]
[AddAction M β]
[MeasurableVAdd M β]
:
MeasurableVAdd (AddUnits M) β
instance
AddUnits.measurableVAdd
{M : Type u_1}
{β : Type u_2}
[MeasurableSpace M]
[MeasurableSpace β]
[AddMonoid M]
[AddAction M β]
[MeasurableVAdd M β]
:
MeasurableVAdd (AddUnits M) β
instance
Units.measurableSMul
{M : Type u_1}
{β : Type u_2}
[MeasurableSpace M]
[MeasurableSpace β]
[Monoid M]
[MulAction M β]
[MeasurableSMul M β]
:
MeasurableSMul Mˣ β
abbrev
IsAddUnit.measurable_const_vadd_iff.match_1
{M : Type u_1}
[AddMonoid M]
{c : M}
(motive : IsAddUnit c → Prop)
:
Equations
- IsAddUnit.measurable_const_vadd_iff.match_1 motive hc h_1 = Exists.casesOn hc fun w h => h_1 w h
Instances For
theorem
IsAddUnit.measurable_const_vadd_iff
{M : Type u_1}
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[AddMonoid M]
[AddAction M β]
[MeasurableVAdd M β]
[MeasurableSpace α]
{f : α → β}
{c : M}
(hc : IsAddUnit c)
:
(Measurable fun x => c +ᵥ f x) ↔ Measurable f
theorem
IsUnit.measurable_const_smul_iff
{M : Type u_1}
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[Monoid M]
[MulAction M β]
[MeasurableSMul M β]
[MeasurableSpace α]
{f : α → β}
{c : M}
(hc : IsUnit c)
:
(Measurable fun x => c • f x) ↔ Measurable f
theorem
IsAddUnit.aemeasurable_const_vadd_iff
{M : Type u_1}
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[AddMonoid M]
[AddAction M β]
[MeasurableVAdd M β]
[MeasurableSpace α]
{f : α → β}
{μ : MeasureTheory.Measure α}
{c : M}
(hc : IsAddUnit c)
:
(AEMeasurable fun x => c +ᵥ f x) ↔ AEMeasurable f
theorem
IsUnit.aemeasurable_const_smul_iff
{M : Type u_1}
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[Monoid M]
[MulAction M β]
[MeasurableSMul M β]
[MeasurableSpace α]
{f : α → β}
{μ : MeasureTheory.Measure α}
{c : M}
(hc : IsUnit c)
:
(AEMeasurable fun x => c • f x) ↔ AEMeasurable f
theorem
measurable_const_smul_iff₀
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace β]
[MeasurableSpace α]
{f : α → β}
{G₀ : Type u_5}
[GroupWithZero G₀]
[MeasurableSpace G₀]
[MulAction G₀ β]
[MeasurableSMul G₀ β]
{c : G₀}
(hc : c ≠ 0)
:
(Measurable fun x => c • f x) ↔ Measurable f
theorem
aemeasurable_const_smul_iff₀
{β : Type u_2}
{α : Type u_3}
[MeasurableSpace β]
[MeasurableSpace α]
{f : α → β}
{μ : MeasureTheory.Measure α}
{G₀ : Type u_5}
[GroupWithZero G₀]
[MeasurableSpace G₀]
[MulAction G₀ β]
[MeasurableSMul G₀ β]
{c : G₀}
(hc : c ≠ 0)
:
(AEMeasurable fun x => c • f x) ↔ AEMeasurable f
Opposite monoid #
Equations
- AddOpposite.instMeasurableSpace = MeasurableSpace.map AddOpposite.op h
Equations
- MulOpposite.instMeasurableSpace = MeasurableSpace.map MulOpposite.op h
instance
AddOpposite.instMeasurableAdd
{M : Type u_1}
[Add M]
[MeasurableSpace M]
[MeasurableAdd M]
:
theorem
AddOpposite.instMeasurableAdd.proof_1
{M : Type u_1}
[Add M]
[MeasurableSpace M]
[MeasurableAdd M]
:
instance
MulOpposite.instMeasurableMul
{M : Type u_1}
[Mul M]
[MeasurableSpace M]
[MeasurableMul M]
:
theorem
AddOpposite.instMeasurableMul₂.proof_1
{M : Type u_1}
[Add M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
:
instance
AddOpposite.instMeasurableMul₂
{M : Type u_1}
[Add M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
:
instance
MulOpposite.instMeasurableMul₂
{M : Type u_1}
[Mul M]
[MeasurableSpace M]
[MeasurableMul₂ M]
:
instance
MeasurableSMul.op
{M : Type u_1}
{α : Type u_2}
[MeasurableSpace M]
[MeasurableSpace α]
[SMul M α]
[SMul Mᵐᵒᵖ α]
[IsCentralScalar M α]
[MeasurableSMul M α]
:
If a scalar is central, then its right action is measurable when its left action is.
instance
MeasurableSMul₂.op
{M : Type u_1}
{α : Type u_2}
[MeasurableSpace M]
[MeasurableSpace α]
[SMul M α]
[SMul Mᵐᵒᵖ α]
[IsCentralScalar M α]
[MeasurableSMul₂ M α]
:
If a scalar is central, then its right action is measurable when its left action is.
theorem
measurableVAdd_opposite_of_add.proof_1
{M : Type u_1}
[Add M]
[MeasurableSpace M]
[MeasurableAdd M]
:
instance
measurableVAdd_opposite_of_add
{M : Type u_1}
[Add M]
[MeasurableSpace M]
[MeasurableAdd M]
:
instance
measurableSMul_opposite_of_mul
{M : Type u_1}
[Mul M]
[MeasurableSpace M]
[MeasurableMul M]
:
theorem
measurableSMul₂_opposite_of_add.proof_1
{M : Type u_1}
[Add M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
:
instance
measurableSMul₂_opposite_of_add
{M : Type u_1}
[Add M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
:
instance
measurableSMul₂_opposite_of_mul
{M : Type u_1}
[Mul M]
[MeasurableSpace M]
[MeasurableMul₂ M]
:
Big operators: ∏ and ∑ #
theorem
List.measurable_sum'
{M : Type u_1}
{α : Type u_2}
[AddMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
(l : List (α → M))
(hl : ∀ (f : α → M), f ∈ l → Measurable f)
:
Measurable (List.sum l)
theorem
List.measurable_prod'
{M : Type u_1}
{α : Type u_2}
[Monoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
(l : List (α → M))
(hl : ∀ (f : α → M), f ∈ l → Measurable f)
:
Measurable (List.prod l)
theorem
List.aemeasurable_sum'
{M : Type u_1}
{α : Type u_2}
[AddMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(l : List (α → M))
(hl : ∀ (f : α → M), f ∈ l → AEMeasurable f)
:
AEMeasurable (List.sum l)
theorem
List.aemeasurable_prod'
{M : Type u_1}
{α : Type u_2}
[Monoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(l : List (α → M))
(hl : ∀ (f : α → M), f ∈ l → AEMeasurable f)
:
theorem
List.measurable_sum
{M : Type u_1}
{α : Type u_2}
[AddMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
(l : List (α → M))
(hl : ∀ (f : α → M), f ∈ l → Measurable f)
:
Measurable fun x => List.sum (List.map (fun f => f x) l)
theorem
List.measurable_prod
{M : Type u_1}
{α : Type u_2}
[Monoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
(l : List (α → M))
(hl : ∀ (f : α → M), f ∈ l → Measurable f)
:
Measurable fun x => List.prod (List.map (fun f => f x) l)
theorem
List.aemeasurable_sum
{M : Type u_1}
{α : Type u_2}
[AddMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(l : List (α → M))
(hl : ∀ (f : α → M), f ∈ l → AEMeasurable f)
:
AEMeasurable fun x => List.sum (List.map (fun f => f x) l)
theorem
List.aemeasurable_prod
{M : Type u_1}
{α : Type u_2}
[Monoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(l : List (α → M))
(hl : ∀ (f : α → M), f ∈ l → AEMeasurable f)
:
AEMeasurable fun x => List.prod (List.map (fun f => f x) l)
theorem
Multiset.measurable_sum'
{M : Type u_1}
{α : Type u_3}
[AddCommMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
(l : Multiset (α → M))
(hl : ∀ (f : α → M), f ∈ l → Measurable f)
:
theorem
Multiset.measurable_prod'
{M : Type u_1}
{α : Type u_3}
[CommMonoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
(l : Multiset (α → M))
(hl : ∀ (f : α → M), f ∈ l → Measurable f)
:
theorem
Multiset.aemeasurable_sum'
{M : Type u_1}
{α : Type u_3}
[AddCommMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(l : Multiset (α → M))
(hl : ∀ (f : α → M), f ∈ l → AEMeasurable f)
:
theorem
Multiset.aemeasurable_prod'
{M : Type u_1}
{α : Type u_3}
[CommMonoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(l : Multiset (α → M))
(hl : ∀ (f : α → M), f ∈ l → AEMeasurable f)
:
theorem
Multiset.measurable_sum
{M : Type u_1}
{α : Type u_3}
[AddCommMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
(s : Multiset (α → M))
(hs : ∀ (f : α → M), f ∈ s → Measurable f)
:
Measurable fun x => Multiset.sum (Multiset.map (fun f => f x) s)
theorem
Multiset.measurable_prod
{M : Type u_1}
{α : Type u_3}
[CommMonoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
(s : Multiset (α → M))
(hs : ∀ (f : α → M), f ∈ s → Measurable f)
:
Measurable fun x => Multiset.prod (Multiset.map (fun f => f x) s)
theorem
Multiset.aemeasurable_sum
{M : Type u_1}
{α : Type u_3}
[AddCommMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(s : Multiset (α → M))
(hs : ∀ (f : α → M), f ∈ s → AEMeasurable f)
:
AEMeasurable fun x => Multiset.sum (Multiset.map (fun f => f x) s)
theorem
Multiset.aemeasurable_prod
{M : Type u_1}
{α : Type u_3}
[CommMonoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(s : Multiset (α → M))
(hs : ∀ (f : α → M), f ∈ s → AEMeasurable f)
:
AEMeasurable fun x => Multiset.prod (Multiset.map (fun f => f x) s)
theorem
Finset.measurable_sum'
{M : Type u_1}
{ι : Type u_2}
{α : Type u_3}
[AddCommMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
{f : ι → α → M}
(s : Finset ι)
(hf : ∀ (i : ι), i ∈ s → Measurable (f i))
:
Measurable (Finset.sum s fun i => f i)
theorem
Finset.measurable_prod'
{M : Type u_1}
{ι : Type u_2}
{α : Type u_3}
[CommMonoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
{f : ι → α → M}
(s : Finset ι)
(hf : ∀ (i : ι), i ∈ s → Measurable (f i))
:
Measurable (Finset.prod s fun i => f i)
theorem
Finset.measurable_sum
{M : Type u_1}
{ι : Type u_2}
{α : Type u_3}
[AddCommMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
{f : ι → α → M}
(s : Finset ι)
(hf : ∀ (i : ι), i ∈ s → Measurable (f i))
:
Measurable fun a => Finset.sum s fun i => f i a
theorem
Finset.measurable_prod
{M : Type u_1}
{ι : Type u_2}
{α : Type u_3}
[CommMonoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
{f : ι → α → M}
(s : Finset ι)
(hf : ∀ (i : ι), i ∈ s → Measurable (f i))
:
Measurable fun a => Finset.prod s fun i => f i a
abbrev
Finset.aemeasurable_sum'.match_1
{M : Type u_2}
{ι : Type u_1}
{α : Type u_3}
{f : ι → α → M}
(s : Finset ι)
(_g : α → M)
(motive : (∃ a, a ∈ s.val ∧ f a = _g) → Prop)
:
Equations
- Finset.aemeasurable_sum'.match_1 s _g motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right
Instances For
theorem
Finset.aemeasurable_sum'
{M : Type u_1}
{ι : Type u_2}
{α : Type u_3}
[AddCommMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : ι → α → M}
(s : Finset ι)
(hf : ∀ (i : ι), i ∈ s → AEMeasurable (f i))
:
AEMeasurable (Finset.sum s fun i => f i)
theorem
Finset.aemeasurable_prod'
{M : Type u_1}
{ι : Type u_2}
{α : Type u_3}
[CommMonoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : ι → α → M}
(s : Finset ι)
(hf : ∀ (i : ι), i ∈ s → AEMeasurable (f i))
:
AEMeasurable (Finset.prod s fun i => f i)
theorem
Finset.aemeasurable_sum
{M : Type u_1}
{ι : Type u_2}
{α : Type u_3}
[AddCommMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : ι → α → M}
(s : Finset ι)
(hf : ∀ (i : ι), i ∈ s → AEMeasurable (f i))
:
AEMeasurable fun a => Finset.sum s fun i => f i a
theorem
Finset.aemeasurable_prod
{M : Type u_1}
{ι : Type u_2}
{α : Type u_3}
[CommMonoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : ι → α → M}
(s : Finset ι)
(hf : ∀ (i : ι), i ∈ s → AEMeasurable (f i))
:
AEMeasurable fun a => Finset.prod s fun i => f i a