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_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
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
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
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
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
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
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
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
Measurable.mul
{M : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[Mul M]
{m : MeasurableSpace α}
{f g : α → M}
[MeasurableMul₂ M]
(hf : Measurable f)
(hg : Measurable g)
:
Measurable fun (a : α) => f a * g a
theorem
Measurable.add
{M : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[Add M]
{m : MeasurableSpace α}
{f 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}
{β : Type u_4}
[MeasurableSpace M]
[Mul M]
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableMul₂ M]
{f g : α → β → M}
{h : α → β}
(hf : Measurable ↿f)
(hg : Measurable ↿g)
(hh : Measurable h)
:
Measurable fun (a : α) => (f a * g a) (h a)
Compositional version of Measurable.mul for use by fun_prop.
theorem
Measurable.add'
{M : Type u_2}
{α : Type u_3}
{β : Type u_4}
[MeasurableSpace M]
[Add M]
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableAdd₂ M]
{f g : α → β → M}
{h : α → β}
(hf : Measurable ↿f)
(hg : Measurable ↿g)
(hh : Measurable h)
:
Measurable fun (a : α) => (f a + g a) (h a)
Compositional version of Measurable.add for use by fun_prop.
theorem
AEMeasurable.mul'
{M : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[Mul M]
{m : MeasurableSpace α}
{f 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 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 g : α → M}
{μ : MeasureTheory.Measure α}
[MeasurableMul₂ M]
(hf : AEMeasurable f μ)
(hg : AEMeasurable g μ)
:
AEMeasurable (fun (a : α) => f a * g a) μ
theorem
AEMeasurable.add
{M : Type u_2}
{α : Type u_3}
[MeasurableSpace M]
[Add M]
{m : MeasurableSpace α}
{f g : α → M}
{μ : MeasureTheory.Measure α}
[MeasurableAdd₂ M]
(hf : AEMeasurable f μ)
(hg : AEMeasurable g μ)
:
AEMeasurable (fun (a : α) => f a + g a) μ
@[instance 100]
instance
MeasurableMul₂.toMeasurableMul
{M : Type u_2}
[MeasurableSpace M]
[Mul M]
[MeasurableMul₂ M]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
MeasurableAdd₂.toMeasurableAdd
{M : Type u_2}
[MeasurableSpace M]
[Add M]
[MeasurableAdd₂ M]
:
Equations
- ⋯ = ⋯
instance
Pi.measurableMul
{ι : Type u_5}
{α : ι → Type u_6}
[(i : ι) → Mul (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableMul (α i)]
:
MeasurableMul ((i : ι) → α i)
Equations
- ⋯ = ⋯
instance
Pi.measurableAdd
{ι : Type u_5}
{α : ι → Type u_6}
[(i : ι) → Add (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableAdd (α i)]
:
MeasurableAdd ((i : ι) → α i)
Equations
- ⋯ = ⋯
instance
Pi.measurableMul₂
{ι : Type u_5}
{α : ι → Type u_6}
[(i : ι) → Mul (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableMul₂ (α i)]
:
MeasurableMul₂ ((i : ι) → α i)
Equations
- ⋯ = ⋯
instance
Pi.measurableAdd₂
{ι : Type u_5}
{α : ι → Type u_6}
[(i : ι) → Add (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableAdd₂ (α i)]
:
MeasurableAdd₂ ((i : ι) → α i)
Equations
- ⋯ = ⋯
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.
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.
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
- ⋯ = ⋯
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_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
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
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
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
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
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
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
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
Measurable.div
{G : Type u_2}
{α : Type u_3}
[MeasurableSpace G]
[Div G]
{m : MeasurableSpace α}
{f g : α → G}
[MeasurableDiv₂ G]
(hf : Measurable f)
(hg : Measurable g)
:
Measurable fun (a : α) => f a / g a
theorem
Measurable.sub
{G : Type u_2}
{α : Type u_3}
[MeasurableSpace G]
[Sub G]
{m : MeasurableSpace α}
{f 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}
{β : Type u_4}
[MeasurableSpace G]
[Div G]
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableDiv₂ G]
{f g : α → β → G}
{h : α → β}
(hf : Measurable ↿f)
(hg : Measurable ↿g)
(hh : Measurable h)
:
Measurable fun (a : α) => (f a / g a) (h a)
theorem
Measurable.sub'
{G : Type u_2}
{α : Type u_3}
{β : Type u_4}
[MeasurableSpace G]
[Sub G]
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSub₂ G]
{f g : α → β → G}
{h : α → β}
(hf : Measurable ↿f)
(hg : Measurable ↿g)
(hh : Measurable h)
:
Measurable fun (a : α) => (f a - g a) (h a)
theorem
AEMeasurable.div'
{G : Type u_2}
{α : Type u_3}
[MeasurableSpace G]
[Div G]
{m : MeasurableSpace α}
{f 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}
{μ : 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}
{μ : MeasureTheory.Measure α}
[MeasurableDiv₂ G]
(hf : AEMeasurable f μ)
(hg : AEMeasurable g μ)
:
AEMeasurable (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}
{μ : MeasureTheory.Measure α}
[MeasurableSub₂ G]
(hf : AEMeasurable f μ)
(hg : AEMeasurable g μ)
:
AEMeasurable (fun (a : α) => f a - g a) μ
@[instance 100]
instance
MeasurableDiv₂.toMeasurableDiv
{G : Type u_2}
[MeasurableSpace G]
[Div G]
[MeasurableDiv₂ G]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
MeasurableSub₂.toMeasurableSub
{G : Type u_2}
[MeasurableSpace G]
[Sub G]
[MeasurableSub₂ G]
:
Equations
- ⋯ = ⋯
instance
Pi.measurableDiv
{ι : Type u_5}
{α : ι → Type u_6}
[(i : ι) → Div (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableDiv (α i)]
:
MeasurableDiv ((i : ι) → α i)
Equations
- ⋯ = ⋯
instance
Pi.measurableSub
{ι : Type u_5}
{α : ι → Type u_6}
[(i : ι) → Sub (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableSub (α i)]
:
MeasurableSub ((i : ι) → α i)
Equations
- ⋯ = ⋯
instance
Pi.measurableDiv₂
{ι : Type u_5}
{α : ι → Type u_6}
[(i : ι) → Div (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableDiv₂ (α i)]
:
MeasurableDiv₂ ((i : ι) → α i)
Equations
- ⋯ = ⋯
instance
Pi.measurableSub₂
{ι : Type u_5}
{α : ι → Type u_6}
[(i : ι) → Sub (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableSub₂ (α i)]
:
MeasurableSub₂ ((i : ι) → α i)
Equations
- ⋯ = ⋯
theorem
measurableSet_eq_fun
{α : Type u_3}
{m : MeasurableSpace α}
{E : Type u_5}
[MeasurableSpace E]
[AddGroup E]
[MeasurableSingletonClass E]
[MeasurableSub₂ E]
{f g : α → E}
(hf : Measurable f)
(hg : Measurable g)
:
MeasurableSet {x : α | f x = g x}
theorem
measurableSet_eq_fun'
{α : Type u_3}
{m : MeasurableSpace α}
{β : Type u_5}
[CanonicallyOrderedAddCommMonoid β]
[Sub β]
[OrderedSub β]
{x✝ : MeasurableSpace β}
[MeasurableSub₂ β]
[MeasurableSingletonClass β]
{f g : α → β}
(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_5}
[MeasurableSpace E]
[AddGroup E]
[MeasurableSingletonClass E]
[MeasurableSub₂ E]
{f 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_5}
[MeasurableSpace E]
[MeasurableSingletonClass E]
[Countable E]
{f g : α → E}
(hf : Measurable f)
(hg : Measurable g)
:
MeasurableSet {x : α | f x = g x}
theorem
ae_eq_trim_of_measurable
{α : Type u_5}
{E : Type u_6}
{m m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasurableSpace E]
[AddGroup E]
[MeasurableSingletonClass E]
[MeasurableSub₂ E]
(hm : m ≤ m0)
{f g : α → E}
(hf : Measurable f)
(hg : Measurable g)
(hfg : f =ᵐ[μ] 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 100]
instance
measurableDiv_of_mul_inv
(G : Type u_2)
[MeasurableSpace G]
[DivInvMonoid G]
[MeasurableMul G]
[MeasurableInv G]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
measurableSub_of_add_neg
(G : Type u_2)
[MeasurableSpace G]
[SubNegMonoid G]
[MeasurableAdd G]
[MeasurableNeg G]
:
Equations
- ⋯ = ⋯
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
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
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)⁻¹) μ
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) μ
@[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
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
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
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
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.measurableInv
{ι : Type u_4}
{α : ι → Type u_5}
[(i : ι) → Inv (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableInv (α i)]
:
MeasurableInv ((i : ι) → α i)
Equations
- ⋯ = ⋯
instance
Pi.measurableNeg
{ι : Type u_4}
{α : ι → Type u_5}
[(i : ι) → Neg (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableNeg (α i)]
:
MeasurableNeg ((i : ι) → α i)
Equations
- ⋯ = ⋯
theorem
MeasurableSet.inv
{G : Type u_2}
[Inv G]
[MeasurableSpace G]
[MeasurableInv G]
{s : Set G}
(hs : MeasurableSet s)
:
theorem
MeasurableSet.neg
{G : Type u_2}
[Neg G]
[MeasurableSpace G]
[MeasurableNeg G]
{s : Set G}
(hs : MeasurableSet s)
:
MeasurableSet (-s)
theorem
measurableEmbedding_inv
{α : Type u_3}
{m : MeasurableSpace α}
[InvolutiveInv α]
[MeasurableInv α]
:
MeasurableEmbedding Inv.inv
theorem
measurableEmbedding_neg
{α : Type u_3}
{m : MeasurableSpace α}
[InvolutiveNeg α]
[MeasurableNeg α]
:
MeasurableEmbedding Neg.neg
theorem
Measurable.mul_iff_right
{α : Type u_1}
{G : Type u_2}
[MeasurableSpace G]
[MeasurableSpace α]
[CommGroup G]
[MeasurableMul₂ G]
[MeasurableInv G]
{f g : α → G}
(hf : Measurable f)
:
Measurable (f * g) ↔ Measurable g
theorem
Measurable.add_iff_right
{α : Type u_1}
{G : Type u_2}
[MeasurableSpace G]
[MeasurableSpace α]
[AddCommGroup G]
[MeasurableAdd₂ G]
[MeasurableNeg G]
{f g : α → G}
(hf : Measurable f)
:
Measurable (f + g) ↔ Measurable g
theorem
AEMeasurable.mul_iff_right
{α : Type u_1}
{G : Type u_2}
[MeasurableSpace G]
[MeasurableSpace α]
[CommGroup G]
[MeasurableMul₂ G]
[MeasurableInv G]
{μ : MeasureTheory.Measure α}
{f g : α → G}
(hf : AEMeasurable f μ)
:
AEMeasurable (f * g) μ ↔ AEMeasurable g μ
theorem
AEMeasurable.add_iff_right
{α : Type u_1}
{G : Type u_2}
[MeasurableSpace G]
[MeasurableSpace α]
[AddCommGroup G]
[MeasurableAdd₂ G]
[MeasurableNeg G]
{μ : MeasureTheory.Measure α}
{f g : α → G}
(hf : AEMeasurable f μ)
:
AEMeasurable (f + g) μ ↔ AEMeasurable g μ
theorem
Measurable.mul_iff_left
{α : Type u_1}
{G : Type u_2}
[MeasurableSpace G]
[MeasurableSpace α]
[CommGroup G]
[MeasurableMul₂ G]
[MeasurableInv G]
{f g : α → G}
(hf : Measurable f)
:
Measurable (g * f) ↔ Measurable g
theorem
Measurable.add_iff_left
{α : Type u_1}
{G : Type u_2}
[MeasurableSpace G]
[MeasurableSpace α]
[AddCommGroup G]
[MeasurableAdd₂ G]
[MeasurableNeg G]
{f g : α → G}
(hf : Measurable f)
:
Measurable (g + f) ↔ Measurable g
theorem
AEMeasurable.mul_iff_left
{α : Type u_1}
{G : Type u_2}
[MeasurableSpace G]
[MeasurableSpace α]
[CommGroup G]
[MeasurableMul₂ G]
[MeasurableInv G]
{μ : MeasureTheory.Measure α}
{f g : α → G}
(hf : AEMeasurable f μ)
:
AEMeasurable (g * f) μ ↔ AEMeasurable g μ
theorem
AEMeasurable.add_iff_left
{α : Type u_1}
{G : Type u_2}
[MeasurableSpace G]
[MeasurableSpace α]
[AddCommGroup G]
[MeasurableAdd₂ G]
[MeasurableNeg G]
{μ : MeasureTheory.Measure α}
{f g : α → G}
(hf : AEMeasurable f μ)
:
AEMeasurable (g + f) μ ↔ AEMeasurable g μ
instance
DivInvMonoid.measurableZPow
(G : Type u)
[DivInvMonoid G]
[MeasurableSpace G]
[MeasurableMul₂ G]
[MeasurableInv G]
:
DivInvMonoid.Pow is measurable.
Equations
- ⋯ = ⋯
@[instance 100]
instance
measurableDiv₂_of_mul_inv
(G : Type u_2)
[MeasurableSpace G]
[DivInvMonoid G]
[MeasurableMul₂ G]
[MeasurableInv G]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
measurableDiv₂_of_add_neg
(G : Type u_2)
[MeasurableSpace G]
[SubNegMonoid G]
[MeasurableAdd₂ G]
[MeasurableNeg G]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
MeasurableDiv.toMeasurableInv
{α : Type u_1}
[MeasurableSpace α]
[Group α]
[MeasurableDiv α]
:
Equations
- ⋯ = ⋯
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 (x1 : M) (x2 : α) => x1 +ᵥ x2)
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 (x1 : M) (x2 : α) => x1 • x2)
Instances
instance
measurableSMul_of_mul
(M : Type u_2)
[Mul M]
[MeasurableSpace M]
[MeasurableMul M]
:
MeasurableSMul M M
Equations
- ⋯ = ⋯
instance
measurableVAdd_of_add
(M : Type u_2)
[Add M]
[MeasurableSpace M]
[MeasurableAdd M]
:
MeasurableVAdd M M
Equations
- ⋯ = ⋯
instance
measurableSMul₂_of_mul
(M : Type u_2)
[Mul M]
[MeasurableSpace M]
[MeasurableMul₂ M]
:
MeasurableSMul₂ M M
Equations
- ⋯ = ⋯
instance
measurableSMul₂_of_add
(M : Type u_2)
[Add M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
:
MeasurableVAdd₂ M M
Equations
- ⋯ = ⋯
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
- ⋯ = ⋯
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
- ⋯ = ⋯
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
- ⋯ = ⋯
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
- ⋯ = ⋯
theorem
Measurable.smul
{M : Type u_2}
{X : Type u_3}
{α : Type u_4}
[MeasurableSpace M]
[MeasurableSpace X]
[SMul M X]
{m : MeasurableSpace α}
{f : α → M}
{g : α → X}
[MeasurableSMul₂ M X]
(hf : Measurable f)
(hg : Measurable g)
:
Measurable fun (x : α) => f x • g x
theorem
Measurable.vadd
{M : Type u_2}
{X : Type u_3}
{α : Type u_4}
[MeasurableSpace M]
[MeasurableSpace X]
[VAdd M X]
{m : MeasurableSpace α}
{f : α → M}
{g : α → X}
[MeasurableVAdd₂ M X]
(hf : Measurable f)
(hg : Measurable g)
:
Measurable fun (x : α) => f x +ᵥ g x
theorem
Measurable.smul'
{M : Type u_2}
{X : Type u_3}
{α : Type u_4}
{β : Type u_5}
[MeasurableSpace M]
[MeasurableSpace X]
[SMul M X]
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSMul₂ M X]
{f : α → β → M}
{g : α → β → X}
{h : α → β}
(hf : Measurable ↿f)
(hg : Measurable ↿g)
(hh : Measurable h)
:
Measurable fun (a : α) => (f a • g a) (h a)
Compositional version of Measurable.smul for use by fun_prop.
theorem
Measurable.vadd'
{M : Type u_2}
{X : Type u_3}
{α : Type u_4}
{β : Type u_5}
[MeasurableSpace M]
[MeasurableSpace X]
[VAdd M X]
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableVAdd₂ M X]
{f : α → β → M}
{g : α → β → X}
{h : α → β}
(hf : Measurable ↿f)
(hg : Measurable ↿g)
(hh : Measurable h)
:
Measurable fun (a : α) => (f a +ᵥ g a) (h a)
Compositional version of Measurable.vadd for use by fun_prop.
theorem
AEMeasurable.smul
{M : Type u_2}
{X : Type u_3}
{α : Type u_4}
[MeasurableSpace M]
[MeasurableSpace X]
[SMul M X]
{m : MeasurableSpace α}
{f : α → M}
{g : α → X}
[MeasurableSMul₂ M X]
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f μ)
(hg : AEMeasurable g μ)
:
AEMeasurable (fun (x : α) => f x • g x) μ
theorem
AEMeasurable.vadd
{M : Type u_2}
{X : Type u_3}
{α : Type u_4}
[MeasurableSpace M]
[MeasurableSpace X]
[VAdd M X]
{m : MeasurableSpace α}
{f : α → M}
{g : α → X}
[MeasurableVAdd₂ M X]
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f μ)
(hg : AEMeasurable g μ)
:
AEMeasurable (fun (x : α) => f x +ᵥ g x) μ
@[instance 100]
instance
MeasurableSMul₂.toMeasurableSMul
{M : Type u_2}
{X : Type u_3}
[MeasurableSpace M]
[MeasurableSpace X]
[SMul M X]
[MeasurableSMul₂ M X]
:
MeasurableSMul M X
Equations
- ⋯ = ⋯
@[instance 100]
instance
MeasurableVAdd₂.toMeasurableVAdd
{M : Type u_2}
{X : Type u_3}
[MeasurableSpace M]
[MeasurableSpace X]
[VAdd M X]
[MeasurableVAdd₂ M X]
:
MeasurableVAdd M X
Equations
- ⋯ = ⋯
theorem
Measurable.smul_const
{M : Type u_2}
{X : Type u_3}
{α : Type u_4}
[MeasurableSpace M]
[MeasurableSpace X]
[SMul M X]
{m : MeasurableSpace α}
{f : α → M}
[MeasurableSMul M X]
(hf : Measurable f)
(y : X)
:
Measurable fun (x : α) => f x • y
theorem
Measurable.vadd_const
{M : Type u_2}
{X : Type u_3}
{α : Type u_4}
[MeasurableSpace M]
[MeasurableSpace X]
[VAdd M X]
{m : MeasurableSpace α}
{f : α → M}
[MeasurableVAdd M X]
(hf : Measurable f)
(y : X)
:
Measurable fun (x : α) => f x +ᵥ y
theorem
AEMeasurable.smul_const
{M : Type u_2}
{X : Type u_3}
{α : Type u_4}
[MeasurableSpace M]
[MeasurableSpace X]
[SMul M X]
{m : MeasurableSpace α}
{f : α → M}
[MeasurableSMul M X]
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f μ)
(y : X)
:
AEMeasurable (fun (x : α) => f x • y) μ
theorem
AEMeasurable.vadd_const
{M : Type u_2}
{X : Type u_3}
{α : Type u_4}
[MeasurableSpace M]
[MeasurableSpace X]
[VAdd M X]
{m : MeasurableSpace α}
{f : α → M}
[MeasurableVAdd M X]
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f μ)
(y : X)
:
AEMeasurable (fun (x : α) => f x +ᵥ y) μ
theorem
Measurable.const_smul
{M : Type u_2}
{X : Type u_3}
{α : Type u_4}
[MeasurableSpace M]
[MeasurableSpace X]
[SMul M X]
{m : MeasurableSpace α}
{g : α → X}
[MeasurableSMul M X]
(hg : Measurable g)
(c : M)
:
Measurable (c • g)
theorem
Measurable.const_vadd
{M : Type u_2}
{X : Type u_3}
{α : Type u_4}
[MeasurableSpace M]
[MeasurableSpace X]
[VAdd M X]
{m : MeasurableSpace α}
{g : α → X}
[MeasurableVAdd M X]
(hg : Measurable g)
(c : M)
:
Measurable (c +ᵥ g)
theorem
Measurable.const_smul'
{M : Type u_2}
{X : Type u_3}
{α : Type u_4}
{β : Type u_5}
[MeasurableSpace M]
[MeasurableSpace X]
[SMul M X]
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSMul M X]
{g : α → β → X}
{h : α → β}
(hg : Measurable ↿g)
(hh : Measurable h)
(c : M)
:
Measurable fun (a : α) => (c • g a) (h a)
Compositional version of Measurable.const_smul for use by fun_prop.
theorem
Measurable.const_vadd'
{M : Type u_2}
{X : Type u_3}
{α : Type u_4}
{β : Type u_5}
[MeasurableSpace M]
[MeasurableSpace X]
[VAdd M X]
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableVAdd M X]
{g : α → β → X}
{h : α → β}
(hg : Measurable ↿g)
(hh : Measurable h)
(c : M)
:
Measurable fun (a : α) => (c +ᵥ g a) (h a)
Compositional version of Measurable.const_vadd for use by fun_prop.
theorem
AEMeasurable.const_smul'
{M : Type u_2}
{X : Type u_3}
{α : Type u_4}
[MeasurableSpace M]
[MeasurableSpace X]
[SMul M X]
{m : MeasurableSpace α}
{g : α → X}
[MeasurableSMul M X]
{μ : MeasureTheory.Measure α}
(hg : AEMeasurable g μ)
(c : M)
:
AEMeasurable (fun (x : α) => c • g x) μ
theorem
AEMeasurable.const_vadd'
{M : Type u_2}
{X : Type u_3}
{α : Type u_4}
[MeasurableSpace M]
[MeasurableSpace X]
[VAdd M X]
{m : MeasurableSpace α}
{g : α → X}
[MeasurableVAdd M X]
{μ : MeasureTheory.Measure α}
(hg : AEMeasurable g μ)
(c : M)
:
AEMeasurable (fun (x : α) => c +ᵥ g x) μ
theorem
AEMeasurable.const_smul
{M : Type u_2}
{X : Type u_3}
{α : Type u_4}
[MeasurableSpace M]
[MeasurableSpace X]
[SMul M X]
{m : MeasurableSpace α}
{g : α → X}
[MeasurableSMul M X]
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable g μ)
(c : M)
:
AEMeasurable (c • g) μ
theorem
AEMeasurable.const_vadd
{M : Type u_2}
{X : Type u_3}
{α : Type u_4}
[MeasurableSpace M]
[MeasurableSpace X]
[VAdd M X]
{m : MeasurableSpace α}
{g : α → X}
[MeasurableVAdd M X]
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable g μ)
(c : M)
:
AEMeasurable (c +ᵥ g) μ
instance
Pi.measurableSMul
{M : Type u_2}
[MeasurableSpace M]
{ι : Type u_6}
{α : ι → Type u_7}
[(i : ι) → SMul M (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableSMul M (α i)]
:
MeasurableSMul M ((i : ι) → α i)
Equations
- ⋯ = ⋯
instance
Pi.measurableVAdd
{M : Type u_2}
[MeasurableSpace M]
{ι : Type u_6}
{α : ι → Type u_7}
[(i : ι) → VAdd M (α i)]
[(i : ι) → MeasurableSpace (α i)]
[∀ (i : ι), MeasurableVAdd M (α i)]
:
MeasurableVAdd M ((i : ι) → α i)
Equations
- ⋯ = ⋯
instance
AddMonoid.measurableSMul_nat₂
(M : Type u_6)
[AddMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
:
AddMonoid.SMul is measurable.
Equations
- ⋯ = ⋯
instance
SubNegMonoid.measurableSMul_int₂
(M : Type u_6)
[SubNegMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
[MeasurableNeg M]
:
SubNegMonoid.SMulInt is measurable.
Equations
- ⋯ = ⋯
theorem
Measurable.measurableSMul₂_iterateMulAct
{α : Type u_2}
{x✝ : MeasurableSpace α}
{f : α → α}
(h : Measurable f)
:
MeasurableSMul₂ (IterateMulAct f) α
theorem
Measurable.measurableSMul₂_iterateAddAct
{α : Type u_2}
{x✝ : MeasurableSpace α}
{f : α → α}
(h : Measurable f)
:
MeasurableVAdd₂ (IterateAddAct f) α
@[simp]
theorem
measurableSMul_iterateMulAct
{α : Type u_2}
{x✝ : MeasurableSpace α}
{f : α → α}
:
MeasurableSMul (IterateMulAct f) α ↔ Measurable f
@[simp]
theorem
measurableVAdd_iterateAddAct
{α : Type u_2}
{x✝ : MeasurableSpace α}
{f : α → α}
:
MeasurableVAdd (IterateAddAct f) α ↔ Measurable f
@[simp]
theorem
measurableSMul₂_iterateMulAct
{α : Type u_2}
{x✝ : MeasurableSpace α}
{f : α → α}
:
MeasurableSMul₂ (IterateMulAct f) α ↔ Measurable f
@[simp]
theorem
measurableSMul₂_iterateAddAct
{α : Type u_2}
{x✝ : MeasurableSpace α}
{f : α → α}
:
MeasurableVAdd₂ (IterateAddAct f) α ↔ 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
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
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 μ
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 μ
Equations
- Units.instMeasurableSpace = MeasurableSpace.comap Units.val inst✝
Equations
- AddUnits.instMeasurableSpace = MeasurableSpace.comap AddUnits.val inst✝
instance
Units.measurableSMul
{M : Type u_2}
{β : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[Monoid M]
[MulAction M β]
[MeasurableSMul M β]
:
MeasurableSMul Mˣ β
Equations
- ⋯ = ⋯
instance
AddUnits.measurableVAdd
{M : Type u_2}
{β : Type u_3}
[MeasurableSpace M]
[MeasurableSpace β]
[AddMonoid M]
[AddAction M β]
[MeasurableVAdd M β]
:
MeasurableVAdd (AddUnits M) β
Equations
- ⋯ = ⋯
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.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.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
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
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
- MulOpposite.instMeasurableSpace = MeasurableSpace.map MulOpposite.op h
Equations
- AddOpposite.instMeasurableSpace = MeasurableSpace.map AddOpposite.op h
instance
MulOpposite.instMeasurableMul
{M : Type u_2}
[Mul M]
[MeasurableSpace M]
[MeasurableMul M]
:
Equations
- ⋯ = ⋯
instance
AddOpposite.instMeasurableAdd
{M : Type u_2}
[Add M]
[MeasurableSpace M]
[MeasurableAdd M]
:
Equations
- ⋯ = ⋯
instance
MulOpposite.instMeasurableMul₂
{M : Type u_2}
[Mul M]
[MeasurableSpace M]
[MeasurableMul₂ M]
:
Equations
- ⋯ = ⋯
instance
AddOpposite.instMeasurableMul₂
{M : Type u_2}
[Add M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
:
Equations
- ⋯ = ⋯
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
- ⋯ = ⋯
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
- ⋯ = ⋯
instance
measurableSMul_opposite_of_mul
{M : Type u_2}
[Mul M]
[MeasurableSpace M]
[MeasurableMul M]
:
Equations
- ⋯ = ⋯
instance
measurableVAdd_opposite_of_add
{M : Type u_2}
[Add M]
[MeasurableSpace M]
[MeasurableAdd M]
:
Equations
- ⋯ = ⋯
instance
measurableSMul₂_opposite_of_mul
{M : Type u_2}
[Mul M]
[MeasurableSpace M]
[MeasurableMul₂ M]
:
Equations
- ⋯ = ⋯
instance
measurableSMul₂_opposite_of_add
{M : Type u_2}
[Add M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
:
Equations
- ⋯ = ⋯
Big operators: ∏ and ∑ #
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 l.prod
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 l.sum
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 l.prod μ
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 l.sum μ
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.map (fun (f : α → M) => f x) l).prod
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.map (fun (f : α → M) => f x) l).sum
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.map (fun (f : α → M) => f x) l).prod) μ
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.map (fun (f : α → M) => f x) l).sum) μ
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)
:
Measurable l.prod
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)
:
Measurable l.sum
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 μ)
:
AEMeasurable l.prod μ
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 μ)
:
AEMeasurable l.sum μ
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.map (fun (f : α → M) => f x) s).prod
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.map (fun (f : α → M) => f x) s).sum
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.map (fun (f : α → M) => f x) s).prod) μ
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.map (fun (f : α → M) => f x) s).sum) μ
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 : α) => ∏ i ∈ s, f i a
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 : α) => ∑ i ∈ s, f i a
theorem
Finset.measurable_prod'
{M : Type u_2}
{ι : Type u_3}
{α : Type u_4}
{β : Type u_5}
[CommMonoid M]
[MeasurableSpace M]
[MeasurableMul₂ M]
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : ι → α → β → M}
{g : α → β}
{s : Finset ι}
(hf : ∀ (i : ι), Measurable ↿(f i))
(hg : Measurable g)
:
Measurable fun (a : α) => (∏ i ∈ s, f i a) (g a)
Compositional version of Finset.measurable_prod for use by fun_prop.
theorem
Finset.measurable_sum'
{M : Type u_2}
{ι : Type u_3}
{α : Type u_4}
{β : Type u_5}
[AddCommMonoid M]
[MeasurableSpace M]
[MeasurableAdd₂ M]
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : ι → α → β → M}
{g : α → β}
{s : Finset ι}
(hf : ∀ (i : ι), Measurable ↿(f i))
(hg : Measurable g)
:
Measurable fun (a : α) => (∑ i ∈ s, f i a) (g a)
Compositional version of Finset.measurable_sum for use by fun_prop.
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 (∏ i ∈ s, 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 (∑ i ∈ s, 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 (fun (a : α) => ∏ i ∈ s, 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 (fun (a : α) => ∑ i ∈ s, f i a) μ
@[instance 100]
instance
DiscreteMeasurableSpace.toMeasurableMul
{α : Type u_1}
[MeasurableSpace α]
[Mul α]
[DiscreteMeasurableSpace α]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
DiscreteMeasurableSpace.toMeasurableAdd
{α : Type u_1}
[MeasurableSpace α]
[Add α]
[DiscreteMeasurableSpace α]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
DiscreteMeasurableSpace.toMeasurableMul₂
{α : Type u_1}
[MeasurableSpace α]
[Mul α]
[DiscreteMeasurableSpace (α × α)]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
DiscreteMeasurableSpace.toMeasurableAdd₂
{α : Type u_1}
[MeasurableSpace α]
[Add α]
[DiscreteMeasurableSpace (α × α)]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
DiscreteMeasurableSpace.toMeasurableInv
{α : Type u_1}
[MeasurableSpace α]
[Inv α]
[DiscreteMeasurableSpace α]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
DiscreteMeasurableSpace.toMeasurableNeg
{α : Type u_1}
[MeasurableSpace α]
[Neg α]
[DiscreteMeasurableSpace α]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
DiscreteMeasurableSpace.toMeasurableDiv
{α : Type u_1}
[MeasurableSpace α]
[Div α]
[DiscreteMeasurableSpace α]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
DiscreteMeasurableSpace.toMeasurableSub
{α : Type u_1}
[MeasurableSpace α]
[Sub α]
[DiscreteMeasurableSpace α]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
DiscreteMeasurableSpace.toMeasurableDiv₂
{α : Type u_1}
[MeasurableSpace α]
[Div α]
[DiscreteMeasurableSpace (α × α)]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
DiscreteMeasurableSpace.toMeasurableSub₂
{α : Type u_1}
[MeasurableSpace α]
[Sub α]
[DiscreteMeasurableSpace (α × α)]
:
Equations
- ⋯ = ⋯