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:
MeasurableMul
says that both left and right multiplication are measurable;MeasurableMul₂
says thatfun p : α × α => p.1 * p.2
is 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
pow
andsmul
. - Use
@[to_additive]
to sendMeasurablePow
toMeasurableSMul₂
. - 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
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
A version of measurable_sub_const
that assumes MeasurableAdd
instead of
MeasurableSub
. This can be nice to avoid unnecessary type-class assumptions.
A version of measurable_div_const
that assumes MeasurableMul
instead of
MeasurableDiv
. This can be nice to avoid unnecessary type-class assumptions.
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
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
DivInvMonoid.Pow
is measurable.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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
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
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
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
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
AddMonoid.SMul
is measurable.
Equations
- ⋯ = ⋯
SubNegMonoid.SMulInt
is measurable.
Equations
- ⋯ = ⋯
Equations
- AddUnits.instMeasurableSpace = MeasurableSpace.comap AddUnits.val inst✝
Equations
- Units.instMeasurableSpace = MeasurableSpace.comap Units.val inst✝
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Opposite monoid #
Equations
- AddOpposite.instMeasurableSpace = MeasurableSpace.map AddOpposite.op h
Equations
- MulOpposite.instMeasurableSpace = MeasurableSpace.map MulOpposite.op h
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
If a scalar is central, then its right action is measurable when its left action is.
Equations
- ⋯ = ⋯
If a scalar is central, then its right action is measurable when its left action is.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Big operators: ∏
and ∑
#
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯