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: (· + ·), (· * ·), (· - ·), (· / ·) #
We say that a type has MeasurableAdd if (· + c) and (· + c) are measurable functions.
For a typeclass assuming measurability of uncurry (· + ·) see MeasurableAdd₂.
- measurable_const_add : ∀ (c : M), Measurable fun (x : M) => c + x
- measurable_add_const : ∀ (c : M), Measurable fun (x : M) => x + c
Instances
We say that a type has MeasurableAdd₂ if uncurry (· + ·) is a measurable functions.
For a typeclass assuming measurability of (c + ·) and (· + c) see MeasurableAdd.
- measurable_add : Measurable fun (p : M × M) => p.1 + p.2
Instances
We say that a type has MeasurableMul if (c * ·) and (· * c) are measurable functions.
For a typeclass assuming measurability of uncurry (*) see MeasurableMul₂.
- measurable_const_mul : ∀ (c : M), Measurable fun (x : M) => c * x
- measurable_mul_const : ∀ (c : M), Measurable fun (x : M) => x * c
Instances
We say that a type has MeasurableMul₂ if uncurry (· * ·) is a measurable functions.
For a typeclass assuming measurability of (c * ·) and (· * c) see MeasurableMul.
- measurable_mul : Measurable fun (p : M × M) => p.1 * p.2
Instances
theorem
Measurable.const_add
{M : Type u_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
[MeasurableSpace M]
[Add M]
[MeasurableAdd₂ M]
:
Equations
- (_ : MeasurableAdd M) = (_ : MeasurableAdd M)
instance
MeasurableMul₂.toMeasurableMul
{M : Type u_2}
[MeasurableSpace M]
[Mul M]
[MeasurableMul₂ M]
:
Equations
- (_ : MeasurableMul M) = (_ : MeasurableMul M)
instance
Pi.measurableAdd
{ι : Type u_4}
{α : ι → Type u_5}
[(i : ι) → Add (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableAdd (α i)]
:
MeasurableAdd ((i : ι) → α i)
Equations
- (_ : MeasurableAdd ((i : ι) → α i)) = (_ : MeasurableAdd ((i : ι) → α i))
instance
Pi.measurableMul
{ι : Type u_4}
{α : ι → Type u_5}
[(i : ι) → Mul (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableMul (α i)]
:
MeasurableMul ((i : ι) → α i)
Equations
- (_ : MeasurableMul ((i : ι) → α i)) = (_ : MeasurableMul ((i : ι) → α i))
instance
Pi.measurableAdd₂
{ι : Type u_4}
{α : ι → Type u_5}
[(i : ι) → Add (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableAdd₂ (α i)]
:
MeasurableAdd₂ ((i : ι) → α i)
Equations
- (_ : MeasurableAdd₂ ((i : ι) → α i)) = (_ : MeasurableAdd₂ ((i : ι) → α i))
instance
Pi.measurableMul₂
{ι : Type u_4}
{α : ι → Type u_5}
[(i : ι) → Mul (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableMul₂ (α i)]
:
MeasurableMul₂ ((i : ι) → α i)
Equations
- (_ : MeasurableMul₂ ((i : ι) → α i)) = (_ : MeasurableMul₂ ((i : ι) → α i))
theorem
measurable_sub_const'
{G : Type u_2}
[SubNegMonoid G]
[MeasurableSpace G]
[MeasurableAdd G]
(g : G)
:
Measurable fun (h : G) => 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_2}
[DivInvMonoid G]
[MeasurableSpace G]
[MeasurableMul G]
(g : G)
:
Measurable fun (h : G) => 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_2)
(γ : Type u_3)
[MeasurableSpace β]
[MeasurableSpace γ]
[Pow β γ]
:
This class assumes that the map β × γ → β given by (x, y) ↦ x ^ y is measurable.
- measurable_pow : Measurable fun (p : β × γ) => p.1 ^ p.2
Instances
Monoid.Pow is measurable.
Equations
- (_ : MeasurablePow M ℕ) = (_ : MeasurablePow M ℕ)
theorem
Measurable.pow
{β : Type u_2}
{γ : Type u_3}
{α : Type u_4}
[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_2}
{γ : Type u_3}
{α : Type u_4}
[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_2}
{γ : Type u_3}
{α : Type u_4}
[MeasurableSpace β]
[MeasurableSpace γ]
[Pow β γ]
[MeasurablePow β γ]
{m : MeasurableSpace α}
{f : α → β}
(hf : Measurable f)
(c : γ)
:
Measurable fun (x : α) => f x ^ c
theorem
AEMeasurable.pow_const
{β : Type u_2}
{γ : Type u_3}
{α : Type u_4}
[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_2}
{γ : Type u_3}
{α : Type u_4}
[MeasurableSpace β]
[MeasurableSpace γ]
[Pow β γ]
[MeasurablePow β γ]
{m : MeasurableSpace α}
{g : α → γ}
(hg : Measurable g)
(c : β)
:
Measurable fun (x : α) => c ^ g x
theorem
AEMeasurable.const_pow
{β : Type u_2}
{γ : Type u_3}
{α : Type u_4}
[MeasurableSpace β]
[MeasurableSpace γ]
[Pow β γ]
[MeasurablePow β γ]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{g : α → γ}
(hg : AEMeasurable g)
(c : β)
:
AEMeasurable fun (x : α) => c ^ g x
We say that a type has MeasurableSub if (c - ·) and (· - c) are measurable
functions. For a typeclass assuming measurability of uncurry (-) see MeasurableSub₂.
- measurable_const_sub : ∀ (c : G), Measurable fun (x : G) => c - x
- measurable_sub_const : ∀ (c : G), Measurable fun (x : G) => x - c
Instances
We say that a type has MeasurableSub₂ if uncurry (· - ·) is a measurable functions.
For a typeclass assuming measurability of (c - ·) and (· - c) see MeasurableSub.
- measurable_sub : Measurable fun (p : G × G) => p.1 - p.2
Instances
We say that a type has MeasurableDiv if (c / ·) and (· / c) are measurable functions.
For a typeclass assuming measurability of uncurry (· / ·) see MeasurableDiv₂.
- measurable_const_div : ∀ (c : G₀), Measurable fun (x : G₀) => c / x
- measurable_div_const : ∀ (c : G₀), Measurable fun (x : G₀) => x / c
Instances
We say that a type has MeasurableDiv₂ if uncurry (· / ·) is a measurable functions.
For a typeclass assuming measurability of (c / ·) and (· / c) see MeasurableDiv.
- measurable_div : Measurable fun (p : G₀ × G₀) => p.1 / p.2
Instances
theorem
Measurable.const_sub
{G : Type u_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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
instance
MeasurableSub₂.toMeasurableSub
{G : Type u_2}
[MeasurableSpace G]
[Sub G]
[MeasurableSub₂ G]
:
Equations
- (_ : MeasurableSub G) = (_ : MeasurableSub G)
instance
MeasurableDiv₂.toMeasurableDiv
{G : Type u_2}
[MeasurableSpace G]
[Div G]
[MeasurableDiv₂ G]
:
Equations
- (_ : MeasurableDiv G) = (_ : MeasurableDiv G)
instance
Pi.measurableSub
{ι : Type u_4}
{α : ι → Type u_5}
[(i : ι) → Sub (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableSub (α i)]
:
MeasurableSub ((i : ι) → α i)
Equations
- (_ : MeasurableSub ((i : ι) → α i)) = (_ : MeasurableSub ((i : ι) → α i))
instance
Pi.measurableDiv
{ι : Type u_4}
{α : ι → Type u_5}
[(i : ι) → Div (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableDiv (α i)]
:
MeasurableDiv ((i : ι) → α i)
Equations
- (_ : MeasurableDiv ((i : ι) → α i)) = (_ : MeasurableDiv ((i : ι) → α i))
instance
Pi.measurableSub₂
{ι : Type u_4}
{α : ι → Type u_5}
[(i : ι) → Sub (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableSub₂ (α i)]
:
MeasurableSub₂ ((i : ι) → α i)
Equations
- (_ : MeasurableSub₂ ((i : ι) → α i)) = (_ : MeasurableSub₂ ((i : ι) → α i))
instance
Pi.measurableDiv₂
{ι : Type u_4}
{α : ι → Type u_5}
[(i : ι) → Div (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableDiv₂ (α i)]
:
MeasurableDiv₂ ((i : ι) → α i)
Equations
- (_ : MeasurableDiv₂ ((i : ι) → α i)) = (_ : MeasurableDiv₂ ((i : ι) → α i))
theorem
measurableSet_eq_fun
{α : Type u_3}
{m : MeasurableSpace α}
{E : Type u_4}
[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_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_4}
[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_3}
{m : MeasurableSpace α}
{E : Type u_4}
[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_4}
{E : Type u_5}
{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)
:
We say that a type has MeasurableNeg if x ↦ -x is a measurable function.
- measurable_neg : Measurable Neg.neg
Instances
We say that a type has MeasurableInv if x ↦ x⁻¹ is a measurable function.
- measurable_inv : Measurable Inv.inv
Instances
instance
measurableSub_of_add_neg
(G : Type u_2)
[MeasurableSpace G]
[SubNegMonoid G]
[MeasurableAdd G]
[MeasurableNeg G]
:
Equations
- (_ : MeasurableSub G) = (_ : MeasurableSub G)
instance
measurableDiv_of_mul_inv
(G : Type u_2)
[MeasurableSpace G]
[DivInvMonoid G]
[MeasurableMul G]
[MeasurableInv G]
:
Equations
- (_ : MeasurableDiv G) = (_ : MeasurableDiv G)
theorem
Measurable.neg
{G : Type u_2}
{α : Type u_3}
[Neg G]
[MeasurableSpace G]
[MeasurableNeg G]
{m : MeasurableSpace α}
{f : α → G}
(hf : Measurable f)
:
Measurable fun (x : α) => -f x
theorem
Measurable.inv
{G : Type u_2}
{α : Type u_3}
[Inv G]
[MeasurableSpace G]
[MeasurableInv G]
{m : MeasurableSpace α}
{f : α → G}
(hf : Measurable f)
:
Measurable fun (x : α) => (f x)⁻¹
theorem
AEMeasurable.neg
{G : Type u_2}
{α : Type u_3}
[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_2}
{α : Type u_3}
[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_3}
{m : MeasurableSpace α}
{G : Type u_4}
[AddGroup G]
[MeasurableSpace G]
[MeasurableNeg G]
{f : α → G}
:
(Measurable fun (x : α) => -f x) ↔ Measurable f
@[simp]
theorem
measurable_inv_iff
{α : Type u_3}
{m : MeasurableSpace α}
{G : Type u_4}
[Group G]
[MeasurableSpace G]
[MeasurableInv G]
{f : α → G}
:
(Measurable fun (x : α) => (f x)⁻¹) ↔ Measurable f
@[simp]
theorem
aemeasurable_neg_iff
{α : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G : Type u_4}
[AddGroup G]
[MeasurableSpace G]
[MeasurableNeg G]
{f : α → G}
:
(AEMeasurable fun (x : α) => -f x) ↔ AEMeasurable f
@[simp]
theorem
aemeasurable_inv_iff
{α : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G : Type u_4}
[Group G]
[MeasurableSpace G]
[MeasurableInv G]
{f : α → G}
:
(AEMeasurable fun (x : α) => (f x)⁻¹) ↔ AEMeasurable f
@[simp]
theorem
measurable_inv_iff₀
{α : Type u_3}
{m : MeasurableSpace α}
{G₀ : Type u_4}
[GroupWithZero G₀]
[MeasurableSpace G₀]
[MeasurableInv G₀]
{f : α → G₀}
:
(Measurable fun (x : α) => (f x)⁻¹) ↔ Measurable f
@[simp]
theorem
aemeasurable_inv_iff₀
{α : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G₀ : Type u_4}
[GroupWithZero G₀]
[MeasurableSpace G₀]
[MeasurableInv G₀]
{f : α → G₀}
:
(AEMeasurable fun (x : α) => (f x)⁻¹) ↔ AEMeasurable f
instance
Pi.measurableNeg
{ι : Type u_4}
{α : ι → Type u_5}
[(i : ι) → Neg (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableNeg (α i)]
:
MeasurableNeg ((i : ι) → α i)
Equations
- (_ : MeasurableNeg ((i : ι) → α i)) = (_ : MeasurableNeg ((i : ι) → α i))
instance
Pi.measurableInv
{ι : Type u_4}
{α : ι → Type u_5}
[(i : ι) → Inv (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableInv (α i)]
:
MeasurableInv ((i : ι) → α i)
Equations
- (_ : MeasurableInv ((i : ι) → α i)) = (_ : MeasurableInv ((i : ι) → α i))
theorem
MeasurableSet.neg
{G : Type u_2}
[Neg G]
[MeasurableSpace G]
[MeasurableNeg G]
{s : Set G}
(hs : MeasurableSet s)
:
MeasurableSet (-s)
theorem
MeasurableSet.inv
{G : Type u_2}
[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.
Equations
- (_ : MeasurablePow G ℤ) = (_ : MeasurablePow G ℤ)
instance
measurableDiv₂_of_add_neg
(G : Type u_2)
[MeasurableSpace G]
[SubNegMonoid G]
[MeasurableAdd₂ G]
[MeasurableNeg G]
:
Equations
- (_ : MeasurableSub₂ G) = (_ : MeasurableSub₂ G)
instance
measurableDiv₂_of_mul_inv
(G : Type u_2)
[MeasurableSpace G]
[DivInvMonoid G]
[MeasurableMul₂ G]
[MeasurableInv G]
:
Equations
- (_ : MeasurableDiv₂ G) = (_ : MeasurableDiv₂ G)
instance
MeasurableDiv.toMeasurableInv
{α : Type u_1}
[MeasurableSpace α]
[Group α]
[MeasurableDiv α]
:
Equations
- (_ : MeasurableInv α) = (_ : MeasurableInv α)
class
MeasurableVAdd
(M : Type u_2)
(α : Type u_3)
[VAdd M α]
[MeasurableSpace M]
[MeasurableSpace α]
:
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.
- measurable_const_vadd : ∀ (c : M), Measurable fun (x : α) => c +ᵥ x
- measurable_vadd_const : ∀ (x : α), Measurable fun (x_1 : M) => x_1 +ᵥ x
Instances
class
MeasurableSMul
(M : Type u_2)
(α : Type u_3)
[SMul M α]
[MeasurableSpace M]
[MeasurableSpace α]
:
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.
- measurable_const_smul : ∀ (c : M), Measurable fun (x : α) => c • x
- measurable_smul_const : ∀ (x : α), Measurable fun (x_1 : M) => x_1 • x
Instances
class
MeasurableVAdd₂
(M : Type u_2)
(α : Type u_3)
[VAdd M α]
[MeasurableSpace M]
[MeasurableSpace α]
:
We say that the action of M on α has MeasurableVAdd₂ if the map
(c, x) ↦ c +ᵥ x is a measurable function.
- measurable_vadd : Measurable (Function.uncurry fun (x : M) (x_1 : α) => x +ᵥ x_1)
Instances
class
MeasurableSMul₂
(M : Type u_2)
(α : Type u_3)
[SMul M α]
[MeasurableSpace M]
[MeasurableSpace α]
:
We say that the action of M on α has Measurable_SMul₂ if the map
(c, x) ↦ c • x is a measurable function.
- measurable_smul : Measurable (Function.uncurry fun (x : M) (x_1 : α) => x • x_1)
Instances
instance
measurableVAdd_of_add
(M : Type u_2)
[Add M]
[MeasurableSpace M]
[MeasurableAdd M]
:
MeasurableVAdd M M
Equations
- (_ : MeasurableVAdd M M) = (_ : MeasurableVAdd M M)
instance
measurableSMul_of_mul
(M : Type u_2)
[Mul M]
[MeasurableSpace M]
[MeasurableMul M]
:
MeasurableSMul M M
Equations
- (_ : MeasurableSMul M M) = (_ : MeasurableSMul M M)
instance
measurableSMul₂_of_add
(M : Type u_2)
[Add M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
:
MeasurableVAdd₂ M M
Equations
- (_ : MeasurableVAdd₂ M M) = (_ : MeasurableVAdd₂ M M)
instance
measurableSMul₂_of_mul
(M : Type u_2)
[Mul M]
[MeasurableSpace M]
[MeasurableMul₂ M]
:
MeasurableSMul₂ M M
Equations
- (_ : MeasurableSMul₂ M M) = (_ : MeasurableSMul₂ M M)
instance
AddSubmonoid.measurableVAdd
{M : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[MeasurableSpace α]
[AddMonoid M]
[AddAction M α]
[MeasurableVAdd M α]
(s : AddSubmonoid M)
:
MeasurableVAdd (↥s) α
Equations
- (_ : MeasurableVAdd (↥s) α) = (_ : MeasurableVAdd (↥s) α)
instance
Submonoid.measurableSMul
{M : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[MeasurableSpace α]
[Monoid M]
[MulAction M α]
[MeasurableSMul M α]
(s : Submonoid M)
:
MeasurableSMul (↥s) α
Equations
- (_ : MeasurableSMul (↥s) α) = (_ : MeasurableSMul (↥s) α)
instance
AddSubgroup.measurableVAdd
{G : Type u_2}
{α : Type u_3}
[MeasurableSpace G]
[MeasurableSpace α]
[AddGroup G]
[AddAction G α]
[MeasurableVAdd G α]
(s : AddSubgroup G)
:
MeasurableVAdd (↥s) α
Equations
- (_ : MeasurableVAdd (↥s) α) = (_ : MeasurableVAdd (↥s.toAddSubmonoid) α)
instance
Subgroup.measurableSMul
{G : Type u_2}
{α : Type u_3}
[MeasurableSpace G]
[MeasurableSpace α]
[Group G]
[MulAction G α]
[MeasurableSMul G α]
(s : Subgroup G)
:
MeasurableSMul (↥s) α
Equations
- (_ : MeasurableSMul (↥s) α) = (_ : MeasurableSMul (↥s.toSubmonoid) α)
theorem
Measurable.vadd
{M : Type u_2}
{β : Type u_3}
{α : Type u_4}
[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_2}
{β : Type u_3}
{α : Type u_4}
[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_2}
{β : Type u_3}
{α : Type u_4}
[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_2}
{β : Type u_3}
{α : Type u_4}
[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_2}
{β : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[VAdd M β]
[MeasurableVAdd₂ M β]
:
MeasurableVAdd M β
Equations
- (_ : MeasurableVAdd M β) = (_ : MeasurableVAdd M β)
instance
MeasurableSMul₂.toMeasurableSMul
{M : Type u_2}
{β : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[SMul M β]
[MeasurableSMul₂ M β]
:
MeasurableSMul M β
Equations
- (_ : MeasurableSMul M β) = (_ : MeasurableSMul M β)
theorem
Measurable.vadd_const
{M : Type u_2}
{β : Type u_3}
{α : Type u_4}
[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_2}
{β : Type u_3}
{α : Type u_4}
[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_2}
{β : Type u_3}
{α : Type u_4}
[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_2}
{β : Type u_3}
{α : Type u_4}
[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_2}
{β : Type u_3}
{α : Type u_4}
[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_2}
{β : Type u_3}
{α : Type u_4}
[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_2}
{β : Type u_3}
{α : Type u_4}
[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_2}
{β : Type u_3}
{α : Type u_4}
[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_2}
{β : Type u_3}
{α : Type u_4}
[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_2}
{β : Type u_3}
{α : Type u_4}
[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_2}
{β : Type u_3}
{α : Type u_4}
[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_2}
{β : Type u_3}
{α : Type u_4}
[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_2}
[MeasurableSpace M]
{ι : Type u_5}
{α : ι → Type u_6}
[(i : ι) → VAdd M (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableVAdd M (α i)]
:
MeasurableVAdd M ((i : ι) → α i)
Equations
- (_ : MeasurableVAdd M ((i : ι) → α i)) = (_ : MeasurableVAdd M ((i : ι) → α i))
instance
Pi.measurableSMul
{M : Type u_2}
[MeasurableSpace M]
{ι : Type u_5}
{α : ι → Type u_6}
[(i : ι) → SMul M (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableSMul M (α i)]
:
MeasurableSMul M ((i : ι) → α i)
Equations
- (_ : MeasurableSMul M ((i : ι) → α i)) = (_ : MeasurableSMul M ((i : ι) → α i))
instance
AddMonoid.measurableSMul_nat₂
(M : Type u_5)
[AddMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
:
AddMonoid.SMul is measurable.
Equations
- (_ : MeasurableSMul₂ ℕ M) = (_ : MeasurableSMul₂ ℕ M)
instance
SubNegMonoid.measurableSMul_int₂
(M : Type u_5)
[SubNegMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
[MeasurableNeg M]
:
SubNegMonoid.SMulInt is measurable.
Equations
- (_ : MeasurableSMul₂ ℤ M) = (_ : MeasurableSMul₂ ℤ M)
theorem
measurable_const_vadd_iff
{β : Type u_3}
{α : Type u_4}
[MeasurableSpace β]
[MeasurableSpace α]
{f : α → β}
{G : Type u_5}
[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_3}
{α : Type u_4}
[MeasurableSpace β]
[MeasurableSpace α]
{f : α → β}
{G : Type u_5}
[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_3}
{α : Type u_4}
[MeasurableSpace β]
[MeasurableSpace α]
{f : α → β}
{μ : MeasureTheory.Measure α}
{G : Type u_5}
[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_3}
{α : Type u_4}
[MeasurableSpace β]
[MeasurableSpace α]
{f : α → β}
{μ : MeasureTheory.Measure α}
{G : Type u_5}
[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✝
instance
AddUnits.measurableVAdd
{M : Type u_2}
{β : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[AddMonoid M]
[AddAction M β]
[MeasurableVAdd M β]
:
MeasurableVAdd (AddUnits M) β
Equations
- (_ : MeasurableVAdd (AddUnits M) β) = (_ : MeasurableVAdd (AddUnits M) β)
instance
Units.measurableSMul
{M : Type u_2}
{β : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[Monoid M]
[MulAction M β]
[MeasurableSMul M β]
:
MeasurableSMul Mˣ β
Equations
- (_ : MeasurableSMul Mˣ β) = (_ : MeasurableSMul Mˣ β)
theorem
IsAddUnit.measurable_const_vadd_iff
{M : Type u_2}
{β : Type u_3}
{α : Type u_4}
[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_2}
{β : Type u_3}
{α : Type u_4}
[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_2}
{β : Type u_3}
{α : Type u_4}
[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_2}
{β : Type u_3}
{α : Type u_4}
[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_3}
{α : Type u_4}
[MeasurableSpace β]
[MeasurableSpace α]
{f : α → β}
{G₀ : Type u_6}
[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_3}
{α : Type u_4}
[MeasurableSpace β]
[MeasurableSpace α]
{f : α → β}
{μ : MeasureTheory.Measure α}
{G₀ : Type u_6}
[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_2}
[Add M]
[MeasurableSpace M]
[MeasurableAdd M]
:
Equations
- (_ : MeasurableAdd Mᵃᵒᵖ) = (_ : MeasurableAdd Mᵃᵒᵖ)
instance
MulOpposite.instMeasurableMul
{M : Type u_2}
[Mul M]
[MeasurableSpace M]
[MeasurableMul M]
:
Equations
- (_ : MeasurableMul Mᵐᵒᵖ) = (_ : MeasurableMul Mᵐᵒᵖ)
instance
AddOpposite.instMeasurableMul₂
{M : Type u_2}
[Add M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
:
Equations
- (_ : MeasurableAdd₂ Mᵃᵒᵖ) = (_ : MeasurableAdd₂ Mᵃᵒᵖ)
instance
MulOpposite.instMeasurableMul₂
{M : Type u_2}
[Mul M]
[MeasurableSpace M]
[MeasurableMul₂ M]
:
Equations
- (_ : MeasurableMul₂ Mᵐᵒᵖ) = (_ : MeasurableMul₂ Mᵐᵒᵖ)
instance
MeasurableSMul.op
{M : Type u_2}
{α : Type u_3}
[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.
Equations
- (_ : MeasurableSMul Mᵐᵒᵖ α) = (_ : MeasurableSMul Mᵐᵒᵖ α)
instance
MeasurableSMul₂.op
{M : Type u_2}
{α : Type u_3}
[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.
Equations
- (_ : MeasurableSMul₂ Mᵐᵒᵖ α) = (_ : MeasurableSMul₂ Mᵐᵒᵖ α)
instance
measurableVAdd_opposite_of_add
{M : Type u_2}
[Add M]
[MeasurableSpace M]
[MeasurableAdd M]
:
Equations
- (_ : MeasurableVAdd Mᵃᵒᵖ M) = (_ : MeasurableVAdd Mᵃᵒᵖ M)
instance
measurableSMul_opposite_of_mul
{M : Type u_2}
[Mul M]
[MeasurableSpace M]
[MeasurableMul M]
:
Equations
- (_ : MeasurableSMul Mᵐᵒᵖ M) = (_ : MeasurableSMul Mᵐᵒᵖ M)
instance
measurableSMul₂_opposite_of_add
{M : Type u_2}
[Add M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
:
Equations
- (_ : MeasurableVAdd₂ Mᵃᵒᵖ M) = (_ : MeasurableVAdd₂ Mᵃᵒᵖ M)
instance
measurableSMul₂_opposite_of_mul
{M : Type u_2}
[Mul M]
[MeasurableSpace M]
[MeasurableMul₂ M]
:
Equations
- (_ : MeasurableSMul₂ Mᵐᵒᵖ M) = (_ : MeasurableSMul₂ Mᵐᵒᵖ M)
Big operators: ∏ and ∑ #
theorem
List.measurable_sum'
{M : Type u_2}
{α : Type u_3}
[AddMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
(l : List (α → M))
(hl : ∀ f ∈ l, Measurable f)
:
Measurable (List.sum l)
theorem
List.measurable_prod'
{M : Type u_2}
{α : Type u_3}
[Monoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
(l : List (α → M))
(hl : ∀ f ∈ l, Measurable f)
:
Measurable (List.prod l)
theorem
List.aemeasurable_sum'
{M : Type u_2}
{α : Type u_3}
[AddMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(l : List (α → M))
(hl : ∀ f ∈ l, AEMeasurable f)
:
AEMeasurable (List.sum l)
theorem
List.aemeasurable_prod'
{M : Type u_2}
{α : Type u_3}
[Monoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(l : List (α → M))
(hl : ∀ f ∈ l, AEMeasurable f)
:
theorem
List.measurable_sum
{M : Type u_2}
{α : Type u_3}
[AddMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
(l : List (α → M))
(hl : ∀ f ∈ l, Measurable f)
:
Measurable fun (x : α) => List.sum (List.map (fun (f : α → M) => f x) l)
theorem
List.measurable_prod
{M : Type u_2}
{α : Type u_3}
[Monoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
(l : List (α → M))
(hl : ∀ f ∈ l, Measurable f)
:
Measurable fun (x : α) => List.prod (List.map (fun (f : α → M) => f x) l)
theorem
List.aemeasurable_sum
{M : Type u_2}
{α : Type u_3}
[AddMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(l : List (α → M))
(hl : ∀ f ∈ l, AEMeasurable f)
:
AEMeasurable fun (x : α) => List.sum (List.map (fun (f : α → M) => f x) l)
theorem
List.aemeasurable_prod
{M : Type u_2}
{α : Type u_3}
[Monoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(l : List (α → M))
(hl : ∀ f ∈ l, AEMeasurable f)
:
AEMeasurable fun (x : α) => List.prod (List.map (fun (f : α → M) => f x) l)
theorem
Multiset.measurable_sum'
{M : Type u_2}
{α : Type u_4}
[AddCommMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
(l : Multiset (α → M))
(hl : ∀ f ∈ l, Measurable f)
:
theorem
Multiset.measurable_prod'
{M : Type u_2}
{α : Type u_4}
[CommMonoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
(l : Multiset (α → M))
(hl : ∀ f ∈ l, Measurable f)
:
theorem
Multiset.aemeasurable_sum'
{M : Type u_2}
{α : Type u_4}
[AddCommMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(l : Multiset (α → M))
(hl : ∀ f ∈ l, AEMeasurable f)
:
theorem
Multiset.aemeasurable_prod'
{M : Type u_2}
{α : Type u_4}
[CommMonoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(l : Multiset (α → M))
(hl : ∀ f ∈ l, AEMeasurable f)
:
theorem
Multiset.measurable_sum
{M : Type u_2}
{α : Type u_4}
[AddCommMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
(s : Multiset (α → M))
(hs : ∀ f ∈ s, Measurable f)
:
Measurable fun (x : α) => Multiset.sum (Multiset.map (fun (f : α → M) => f x) s)
theorem
Multiset.measurable_prod
{M : Type u_2}
{α : Type u_4}
[CommMonoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
(s : Multiset (α → M))
(hs : ∀ f ∈ s, Measurable f)
:
Measurable fun (x : α) => Multiset.prod (Multiset.map (fun (f : α → M) => f x) s)
theorem
Multiset.aemeasurable_sum
{M : Type u_2}
{α : Type u_4}
[AddCommMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(s : Multiset (α → M))
(hs : ∀ f ∈ s, AEMeasurable f)
:
AEMeasurable fun (x : α) => Multiset.sum (Multiset.map (fun (f : α → M) => f x) s)
theorem
Multiset.aemeasurable_prod
{M : Type u_2}
{α : Type u_4}
[CommMonoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(s : Multiset (α → M))
(hs : ∀ f ∈ s, AEMeasurable f)
:
AEMeasurable fun (x : α) => Multiset.prod (Multiset.map (fun (f : α → M) => f x) s)
theorem
Finset.measurable_sum'
{M : Type u_2}
{ι : Type u_3}
{α : Type u_4}
[AddCommMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
{f : ι → α → M}
(s : Finset ι)
(hf : ∀ i ∈ s, Measurable (f i))
:
Measurable (Finset.sum s fun (i : ι) => f i)
theorem
Finset.measurable_prod'
{M : Type u_2}
{ι : Type u_3}
{α : Type u_4}
[CommMonoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
{f : ι → α → M}
(s : Finset ι)
(hf : ∀ i ∈ s, Measurable (f i))
:
Measurable (Finset.prod s fun (i : ι) => f i)
theorem
Finset.measurable_sum
{M : Type u_2}
{ι : Type u_3}
{α : Type u_4}
[AddCommMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
{f : ι → α → M}
(s : Finset ι)
(hf : ∀ i ∈ s, Measurable (f i))
:
Measurable fun (a : α) => Finset.sum s fun (i : ι) => f i a
theorem
Finset.measurable_prod
{M : Type u_2}
{ι : Type u_3}
{α : Type u_4}
[CommMonoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
{f : ι → α → M}
(s : Finset ι)
(hf : ∀ i ∈ s, Measurable (f i))
:
Measurable fun (a : α) => Finset.prod s fun (i : ι) => f i a
theorem
Finset.aemeasurable_sum'
{M : Type u_2}
{ι : Type u_3}
{α : Type u_4}
[AddCommMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : ι → α → M}
(s : Finset ι)
(hf : ∀ i ∈ s, AEMeasurable (f i))
:
AEMeasurable (Finset.sum s fun (i : ι) => f i)
theorem
Finset.aemeasurable_prod'
{M : Type u_2}
{ι : Type u_3}
{α : Type u_4}
[CommMonoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : ι → α → M}
(s : Finset ι)
(hf : ∀ i ∈ s, AEMeasurable (f i))
:
AEMeasurable (Finset.prod s fun (i : ι) => f i)
theorem
Finset.aemeasurable_sum
{M : Type u_2}
{ι : Type u_3}
{α : Type u_4}
[AddCommMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : ι → α → M}
(s : Finset ι)
(hf : ∀ i ∈ s, AEMeasurable (f i))
:
AEMeasurable fun (a : α) => Finset.sum s fun (i : ι) => f i a
theorem
Finset.aemeasurable_prod
{M : Type u_2}
{ι : Type u_3}
{α : Type u_4}
[CommMonoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : ι → α → M}
(s : Finset ι)
(hf : ∀ i ∈ s, AEMeasurable (f i))
:
AEMeasurable fun (a : α) => Finset.prod s fun (i : ι) => f i a
instance
DiscreteMeasurableSpace.toMeasurableAdd
{α : Type u_1}
[MeasurableSpace α]
[Add α]
[DiscreteMeasurableSpace α]
:
Equations
- (_ : MeasurableAdd α) = (_ : MeasurableAdd α)
instance
DiscreteMeasurableSpace.toMeasurableMul
{α : Type u_1}
[MeasurableSpace α]
[Mul α]
[DiscreteMeasurableSpace α]
:
Equations
- (_ : MeasurableMul α) = (_ : MeasurableMul α)
instance
DiscreteMeasurableSpace.toMeasurableAdd₂
{α : Type u_1}
[MeasurableSpace α]
[Add α]
[DiscreteMeasurableSpace (α × α)]
:
Equations
- (_ : MeasurableAdd₂ α) = (_ : MeasurableAdd₂ α)
instance
DiscreteMeasurableSpace.toMeasurableMul₂
{α : Type u_1}
[MeasurableSpace α]
[Mul α]
[DiscreteMeasurableSpace (α × α)]
:
Equations
- (_ : MeasurableMul₂ α) = (_ : MeasurableMul₂ α)
instance
DiscreteMeasurableSpace.toMeasurableNeg
{α : Type u_1}
[MeasurableSpace α]
[Neg α]
[DiscreteMeasurableSpace α]
:
Equations
- (_ : MeasurableNeg α) = (_ : MeasurableNeg α)
instance
DiscreteMeasurableSpace.toMeasurableInv
{α : Type u_1}
[MeasurableSpace α]
[Inv α]
[DiscreteMeasurableSpace α]
:
Equations
- (_ : MeasurableInv α) = (_ : MeasurableInv α)
instance
DiscreteMeasurableSpace.toMeasurableSub
{α : Type u_1}
[MeasurableSpace α]
[Sub α]
[DiscreteMeasurableSpace α]
:
Equations
- (_ : MeasurableSub α) = (_ : MeasurableSub α)
instance
DiscreteMeasurableSpace.toMeasurableDiv
{α : Type u_1}
[MeasurableSpace α]
[Div α]
[DiscreteMeasurableSpace α]
:
Equations
- (_ : MeasurableDiv α) = (_ : MeasurableDiv α)
instance
DiscreteMeasurableSpace.toMeasurableSub₂
{α : Type u_1}
[MeasurableSpace α]
[Sub α]
[DiscreteMeasurableSpace (α × α)]
:
Equations
- (_ : MeasurableSub₂ α) = (_ : MeasurableSub₂ α)
instance
DiscreteMeasurableSpace.toMeasurableDiv₂
{α : Type u_1}
[MeasurableSpace α]
[Div α]
[DiscreteMeasurableSpace (α × α)]
:
Equations
- (_ : MeasurableDiv₂ α) = (_ : MeasurableDiv₂ α)