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 that fun 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 and smul.
• Use @[to_additive] to send MeasurablePow to MeasurableSMul₂.
• This might require changing the definition (swapping the arguments in the function that is in the conclusion of MeasurableSMul.)

Binary operations: (· + ·), (· * ·), (· - ·), (· / ·)

class MeasurableAdd (M : Type u_2) [MeasurableSpace M] [Add M] : Prop

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

class MeasurableAdd₂ (M : Type u_2) [MeasurableSpace M] [Add M] : Prop

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

class MeasurableMul (M : Type u_2) [MeasurableSpace M] [Mul M] : Prop

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

class MeasurableMul₂ (M : Type u_2) [MeasurableSpace M] [Mul M] : Prop

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

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] : MeasurableMul M

@[instance 100]

instance MeasurableAdd₂.toMeasurableAdd {M : Type u_2} [MeasurableSpace M] [Add M] [MeasurableAdd₂ M] : MeasurableAdd M

instance Pi.measurableMul {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → Mul (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableMul (α i)] : MeasurableMul ((i : ι) → α i)

instance Pi.measurableAdd {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → Add (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableAdd (α i)] : MeasurableAdd ((i : ι) → α i)

instance Pi.measurableMul₂ {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → Mul (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableMul₂ (α i)] : MeasurableMul₂ ((i : ι) → α i)

instance Pi.measurableAdd₂ {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → Add (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableAdd₂ (α i)] : MeasurableAdd₂ ((i : ι) → α i)

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 β γ] : Prop

This class assumes that the map β × γ → β given by (x, y) ↦ x ^ y is measurable.

• measurable_pow : Measurable fun (p : β × γ) => p.1 ^ p.2

instance Monoid.measurablePow (M : Type u_2) [Monoid M] [MeasurableSpace M] [MeasurableMul₂ M] : MeasurablePow M ℕ

Monoid.Pow is measurable.

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) μ

class MeasurableSub (G : Type u_2) [MeasurableSpace G] [Sub G] : Prop

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

class MeasurableSub₂ (G : Type u_2) [MeasurableSpace G] [Sub G] : Prop

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

class MeasurableDiv (G₀ : Type u_2) [MeasurableSpace G₀] [Div G₀] : Prop

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

class MeasurableDiv₂ (G₀ : Type u_2) [MeasurableSpace G₀] [Div G₀] : Prop

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

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] : MeasurableDiv G

@[instance 100]

instance MeasurableSub₂.toMeasurableSub {G : Type u_2} [MeasurableSpace G] [Sub G] [MeasurableSub₂ G] : MeasurableSub G

instance Pi.measurableDiv {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → Div (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableDiv (α i)] : MeasurableDiv ((i : ι) → α i)

instance Pi.measurableSub {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → Sub (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableSub (α i)] : MeasurableSub ((i : ι) → α i)

instance Pi.measurableDiv₂ {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → Div (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableDiv₂ (α i)] : MeasurableDiv₂ ((i : ι) → α i)

instance Pi.measurableSub₂ {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → Sub (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableSub₂ (α i)] : MeasurableSub₂ ((i : ι) → α i)

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} [AddCommMonoid β] [PartialOrder β] [CanonicallyOrderedAdd β] [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) : f =ᵐ[μ.trim hm] g

class MeasurableNeg (G : Type u_2) [Neg G] [MeasurableSpace G] : Prop

We say that a type has MeasurableNeg if x ↦ -x is a measurable function.

• measurable_neg : Measurable Neg.neg

class MeasurableInv (G : Type u_2) [Inv G] [MeasurableSpace G] : Prop

We say that a type has MeasurableInv if x ↦ x⁻¹ is a measurable function.

• measurable_inv : Measurable Inv.inv

@[instance 100]

instance measurableDiv_of_mul_inv (G : Type u_2) [MeasurableSpace G] [DivInvMonoid G] [MeasurableMul G] [MeasurableInv G] : MeasurableDiv G

@[instance 100]

instance measurableSub_of_add_neg (G : Type u_2) [MeasurableSpace G] [SubNegMonoid G] [MeasurableAdd G] [MeasurableNeg G] : MeasurableSub G

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} [InvolutiveInv 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} [InvolutiveNeg 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} [InvolutiveInv 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} [InvolutiveNeg G] [MeasurableSpace G] [MeasurableNeg G] {f : α → G} : AEMeasurable (fun (x : α) => -f x) μ ↔ AEMeasurable f μ

@[deprecated measurable_inv_iff (since := "2025-04-09")]

theorem measurable_inv_iff₀ {α : Type u_3} {m : MeasurableSpace α} {G : Type u_4} [InvolutiveInv G] [MeasurableSpace G] [MeasurableInv G] {f : α → G} : (Measurable fun (x : α) => (f x)⁻¹) ↔ Measurable f

Alias of measurable_inv_iff.

@[deprecated aemeasurable_inv_iff (since := "2025-04-09")]

theorem aemeasurable_inv_iff₀ {α : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G : Type u_4} [InvolutiveInv G] [MeasurableSpace G] [MeasurableInv G] {f : α → G} : AEMeasurable (fun (x : α) => (f x)⁻¹) μ ↔ AEMeasurable f μ

Alias of aemeasurable_inv_iff.

instance Pi.measurableInv {ι : Type u_4} {α : ι → Type u_5} [(i : ι) → Inv (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableInv (α i)] : MeasurableInv ((i : ι) → α i)

instance Pi.measurableNeg {ι : Type u_4} {α : ι → Type u_5} [(i : ι) → Neg (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableNeg (α i)] : MeasurableNeg ((i : ι) → α i)

theorem MeasurableSet.inv {G : Type u_2} [Inv G] [MeasurableSpace G] [MeasurableInv G] {s : Set G} (hs : MeasurableSet s) : 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] : MeasurablePow G ℤ

DivInvMonoid.Pow is measurable.

@[instance 100]

instance measurableDiv₂_of_mul_inv (G : Type u_2) [MeasurableSpace G] [DivInvMonoid G] [MeasurableMul₂ G] [MeasurableInv G] : MeasurableDiv₂ G

@[instance 100]

instance measurableDiv₂_of_add_neg (G : Type u_2) [MeasurableSpace G] [SubNegMonoid G] [MeasurableAdd₂ G] [MeasurableNeg G] : MeasurableSub₂ G

@[instance 100]

instance MeasurableDiv.toMeasurableInv {α : Type u_1} [MeasurableSpace α] [Group α] [MeasurableDiv α] : MeasurableInv α

class MeasurableConstVAdd (M : Type u_2) (α : Type u_3) [VAdd M α] [MeasurableSpace α] : Prop

We say that the action of M on α has MeasurableConstVAdd if for each c the map x ↦ c +ᵥ x is a measurable function.

• measurable_const_vadd (c : M) : Measurable fun (x : α) => c +ᵥ x

class MeasurableConstSMul (M : Type u_2) (α : Type u_3) [SMul M α] [MeasurableSpace α] : Prop

We say that the action of M on α has MeasurableConstSMul if for each c the map x ↦ c • x is a measurable function.

• measurable_const_smul (c : M) : Measurable fun (x : α) => c • x

class MeasurableVAdd (M : Type u_2) (α : Type u_3) [VAdd M α] [MeasurableSpace M] [MeasurableSpace α] extends MeasurableConstVAdd M α : Prop

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

class MeasurableSMul (M : Type u_2) (α : Type u_3) [SMul M α] [MeasurableSpace M] [MeasurableSpace α] extends MeasurableConstSMul M α : Prop

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

class MeasurableVAdd₂ (M : Type u_2) (α : Type u_3) [VAdd M α] [MeasurableSpace M] [MeasurableSpace α] : Prop

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)

class MeasurableSMul₂ (M : Type u_2) (α : Type u_3) [SMul M α] [MeasurableSpace M] [MeasurableSpace α] : Prop

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)

instance measurableSMul_of_mul (M : Type u_2) [Mul M] [MeasurableSpace M] [MeasurableMul M] : MeasurableSMul M M

instance measurableVAdd_of_add (M : Type u_2) [Add M] [MeasurableSpace M] [MeasurableAdd M] : MeasurableVAdd M M

instance measurableSMul₂_of_mul (M : Type u_2) [Mul M] [MeasurableSpace M] [MeasurableMul₂ M] : MeasurableSMul₂ M M

instance measurableSMul₂_of_add (M : Type u_2) [Add M] [MeasurableSpace M] [MeasurableAdd₂ M] : MeasurableVAdd₂ M M

instance Submonoid.instMeasurableConstSMul {M : Type u_2} {α : Type u_3} [MeasurableSpace α] [Monoid M] [MulAction M α] [MeasurableConstSMul M α] (s : Submonoid M) : MeasurableConstSMul (↥s) α

instance AddSubmonoid.instMeasurableConstVAdd {M : Type u_2} {α : Type u_3} [MeasurableSpace α] [AddMonoid M] [AddAction M α] [MeasurableConstVAdd M α] (s : AddSubmonoid M) : MeasurableConstVAdd (↥s) α

instance Submonoid.instMeasurableSMul {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [MeasurableSpace α] [Monoid M] [MulAction M α] [MeasurableSMul M α] (s : Submonoid M) : MeasurableSMul (↥s) α

instance AddSubmonoid.instMeasurableVAdd {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [MeasurableSpace α] [AddMonoid M] [AddAction M α] [MeasurableVAdd M α] (s : AddSubmonoid M) : MeasurableVAdd (↥s) α

instance Subgroup.instMeasurableConstSMul {G : Type u_2} {α : Type u_3} [MeasurableSpace α] [Group G] [MulAction G α] [MeasurableConstSMul G α] (s : Subgroup G) : MeasurableConstSMul (↥s) α

instance AddSubgroup.instMeasurableConstVAdd {G : Type u_2} {α : Type u_3} [MeasurableSpace α] [AddGroup G] [AddAction G α] [MeasurableConstVAdd G α] (s : AddSubgroup G) : MeasurableConstVAdd (↥s) α

instance Subgroup.instMeasurableSMul {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [MeasurableSpace α] [Group G] [MulAction G α] [MeasurableSMul G α] (s : Subgroup G) : MeasurableSMul (↥s) α

instance AddSubgroup.instMeasurableVAdd {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [MeasurableSpace α] [AddGroup G] [AddAction G α] [MeasurableVAdd G α] (s : AddSubgroup G) : MeasurableVAdd (↥s) α

theorem Measurable.const_smul {M : Type u_2} {X : Type u_3} {α : Type u_4} [MeasurableSpace X] [SMul M X] {m : MeasurableSpace α} {g : α → X} [MeasurableConstSMul 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 X] [VAdd M X] {m : MeasurableSpace α} {g : α → X} [MeasurableConstVAdd M X] (hg : Measurable g) (c : M) : Measurable (c +ᵥ g)

theorem Measurable.fun_const_smul {M : Type u_2} {X : Type u_3} {α : Type u_4} {β : Type u_5} [MeasurableSpace X] [SMul M X] {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableConstSMul 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.fun_const_vadd {M : Type u_2} {X : Type u_3} {α : Type u_4} {β : Type u_5} [MeasurableSpace X] [VAdd M X] {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableConstVAdd 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.

@[deprecated Measurable.fun_const_smul (since := "2025-04-23")]

theorem Measurable.const_smul' {M : Type u_2} {X : Type u_3} {α : Type u_4} {β : Type u_5} [MeasurableSpace X] [SMul M X] {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableConstSMul M X] {g : α → β → X} {h : α → β} (hg : Measurable ↿g) (hh : Measurable h) (c : M) : Measurable fun (a : α) => (c • g a) (h a)

Alias of Measurable.fun_const_smul.

---

Compositional version of Measurable.const_smul for use by fun_prop.

theorem AEMeasurable.fun_const_smul {M : Type u_2} {X : Type u_3} {α : Type u_4} [MeasurableSpace X] [SMul M X] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {g : α → X} [MeasurableConstSMul M X] (hg : AEMeasurable g μ) (c : M) : AEMeasurable (fun (x : α) => c • g x) μ

theorem AEMeasurable.fun_const_vadd {M : Type u_2} {X : Type u_3} {α : Type u_4} [MeasurableSpace X] [VAdd M X] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {g : α → X} [MeasurableConstVAdd M X] (hg : AEMeasurable g μ) (c : M) : AEMeasurable (fun (x : α) => c +ᵥ g x) μ

@[deprecated AEMeasurable.fun_const_smul (since := "2025-04-23")]

theorem AEMeasurable.const_smul' {M : Type u_2} {X : Type u_3} {α : Type u_4} [MeasurableSpace X] [SMul M X] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {g : α → X} [MeasurableConstSMul M X] (hg : AEMeasurable g μ) (c : M) : AEMeasurable (fun (x : α) => c • g x) μ

Alias of AEMeasurable.fun_const_smul.

theorem AEMeasurable.const_smul {M : Type u_2} {X : Type u_3} {α : Type u_4} [MeasurableSpace X] [SMul M X] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {g : α → X} [MeasurableConstSMul M X] (hf : AEMeasurable g μ) (c : M) : AEMeasurable (c • g) μ

theorem AEMeasurable.const_vadd {M : Type u_2} {X : Type u_3} {α : Type u_4} [MeasurableSpace X] [VAdd M X] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {g : α → X} [MeasurableConstVAdd M X] (hf : AEMeasurable g μ) (c : M) : AEMeasurable (c +ᵥ g) μ

instance Pi.instMeasurableConstSMul {M : Type u_2} {ι : Type u_6} {α : ι → Type u_7} [(i : ι) → SMul M (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableConstSMul M (α i)] : MeasurableConstSMul M ((i : ι) → α i)

instance Pi.instMeasurableConstVAdd {M : Type u_2} {ι : Type u_6} {α : ι → Type u_7} [(i : ι) → VAdd M (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableConstVAdd M (α i)] : MeasurableConstVAdd M ((i : ι) → α i)

instance MulOpposite.instMeasurableConstSMul {M : Type u_2} {α : Type u_4} {m : MeasurableSpace α} [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] [MeasurableConstSMul M α] : MeasurableConstSMul Mᵐᵒᵖ α

If a scalar is central, then its right action is measurable when its left action is.

instance AddOpposite.instMeasurableConstVAdd {M : Type u_2} {α : Type u_4} {m : MeasurableSpace α} [VAdd M α] [VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α] [MeasurableConstVAdd M α] : MeasurableConstVAdd Mᵃᵒᵖ α

theorem Measurable.smul {M : Type u_2} {X : Type u_3} {α : Type u_4} [MeasurableSpace X] [SMul M X] {m : MeasurableSpace α} {f : α → M} {g : α → X} [MeasurableSpace M] [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 X] [VAdd M X] {m : MeasurableSpace α} {f : α → M} {g : α → X} [MeasurableSpace M] [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 X] [SMul M X] {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace M] [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 X] [VAdd M X] {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace M] [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 X] [SMul M X] {m : MeasurableSpace α} {f : α → M} {g : α → X} [MeasurableSpace M] [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 X] [VAdd M X] {m : MeasurableSpace α} {f : α → M} {g : α → X} [MeasurableSpace M] [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 X] [SMul M X] [MeasurableSpace M] [MeasurableSMul₂ M X] : MeasurableSMul M X

@[instance 100]

instance MeasurableVAdd₂.toMeasurableVAdd {M : Type u_2} {X : Type u_3} [MeasurableSpace X] [VAdd M X] [MeasurableSpace M] [MeasurableVAdd₂ M X] : MeasurableVAdd M X

theorem Measurable.smul_const {M : Type u_2} {X : Type u_3} {α : Type u_4} [MeasurableSpace X] [SMul M X] {m : MeasurableSpace α} {f : α → M} [MeasurableSpace 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 X] [VAdd M X] {m : MeasurableSpace α} {f : α → M} [MeasurableSpace 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 X] [SMul M X] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → M} [MeasurableSpace M] [MeasurableSMul M X] (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 X] [VAdd M X] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → M} [MeasurableSpace M] [MeasurableVAdd M X] (hf : AEMeasurable f μ) (y : X) : AEMeasurable (fun (x : α) => f x +ᵥ y) μ

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)

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)

instance AddMonoid.measurableSMul_nat₂ (M : Type u_6) [AddMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] : MeasurableSMul₂ ℕ M

AddMonoid.SMul is measurable.

instance SubNegMonoid.measurableSMul_int₂ (M : Type u_6) [SubNegMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] [MeasurableNeg M] : MeasurableSMul₂ ℤ M

SubNegMonoid.SMulInt is measurable.

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_5} {α : Type u_6} [MeasurableSpace β] [MeasurableSpace α] {f : α → β} {G : Type u_7} [Group G] [MulAction G β] [MeasurableConstSMul G β] (c : G) : (Measurable fun (x : α) => c • f x) ↔ Measurable f

theorem measurable_const_vadd_iff {β : Type u_5} {α : Type u_6} [MeasurableSpace β] [MeasurableSpace α] {f : α → β} {G : Type u_7} [AddGroup G] [AddAction G β] [MeasurableConstVAdd G β] (c : G) : (Measurable fun (x : α) => c +ᵥ f x) ↔ Measurable f

theorem aemeasurable_const_smul_iff {β : Type u_5} {α : Type u_6} [MeasurableSpace β] [MeasurableSpace α] {f : α → β} {μ : MeasureTheory.Measure α} {G : Type u_7} [Group G] [MulAction G β] [MeasurableConstSMul G β] (c : G) : AEMeasurable (fun (x : α) => c • f x) μ ↔ AEMeasurable f μ

theorem aemeasurable_const_vadd_iff {β : Type u_5} {α : Type u_6} [MeasurableSpace β] [MeasurableSpace α] {f : α → β} {μ : MeasureTheory.Measure α} {G : Type u_7} [AddGroup G] [AddAction G β] [MeasurableConstVAdd G β] (c : G) : AEMeasurable (fun (x : α) => c +ᵥ f x) μ ↔ AEMeasurable f μ

instance Units.instMeasurableConstSMul {M : Type u_4} {β : Type u_5} [MeasurableSpace β] [Monoid M] [MulAction M β] [MeasurableConstSMul M β] : MeasurableConstSMul Mˣ β

instance AddUnits.instMeasurableConstVAdd {M : Type u_4} {β : Type u_5} [MeasurableSpace β] [AddMonoid M] [AddAction M β] [MeasurableConstVAdd M β] : MeasurableConstVAdd (AddUnits M) β

theorem IsUnit.measurable_const_smul_iff {M : Type u_4} {β : Type u_5} {α : Type u_6} [MeasurableSpace β] [MeasurableSpace α] {f : α → β} [Monoid M] [MulAction M β] [MeasurableConstSMul M β] {c : M} (hc : IsUnit c) : (Measurable fun (x : α) => c • f x) ↔ Measurable f

theorem IsAddUnit.measurable_const_vadd_iff {M : Type u_4} {β : Type u_5} {α : Type u_6} [MeasurableSpace β] [MeasurableSpace α] {f : α → β} [AddMonoid M] [AddAction M β] [MeasurableConstVAdd M β] {c : M} (hc : IsAddUnit c) : (Measurable fun (x : α) => c +ᵥ f x) ↔ Measurable f

theorem IsUnit.aemeasurable_const_smul_iff {M : Type u_4} {β : Type u_5} {α : Type u_6} [MeasurableSpace β] [MeasurableSpace α] {f : α → β} {μ : MeasureTheory.Measure α} [Monoid M] [MulAction M β] [MeasurableConstSMul M β] {c : M} (hc : IsUnit c) : AEMeasurable (fun (x : α) => c • f x) μ ↔ AEMeasurable f μ

theorem IsAddUnit.aemeasurable_const_vadd_iff {M : Type u_4} {β : Type u_5} {α : Type u_6} [MeasurableSpace β] [MeasurableSpace α] {f : α → β} {μ : MeasureTheory.Measure α} [AddMonoid M] [AddAction M β] [MeasurableConstVAdd M β] {c : M} (hc : IsAddUnit c) : AEMeasurable (fun (x : α) => c +ᵥ f x) μ ↔ AEMeasurable f μ

instance Units.instMeasurableSpace {M : Type u_4} [Monoid M] [MeasurableSpace M] : MeasurableSpace Mˣ

Equations

• Units.instMeasurableSpace = MeasurableSpace.comap Units.val inst✝

instance AddUnits.instMeasurableSpace {M : Type u_4} [AddMonoid M] [MeasurableSpace M] : MeasurableSpace (AddUnits M)

Equations

• AddUnits.instMeasurableSpace = MeasurableSpace.comap AddUnits.val inst✝

instance Units.measurableSMul {M : Type u_4} {β : Type u_5} [MeasurableSpace β] [Monoid M] [MulAction M β] [MeasurableSpace M] [MeasurableSMul M β] : MeasurableSMul Mˣ β

instance AddUnits.measurableVAdd {M : Type u_4} {β : Type u_5} [MeasurableSpace β] [AddMonoid M] [AddAction M β] [MeasurableSpace M] [MeasurableVAdd M β] : MeasurableVAdd (AddUnits M) β

theorem measurable_const_smul_iff₀ {G₀ : Type u_3} {β : Type u_5} {α : Type u_6} [MeasurableSpace β] [MeasurableSpace α] {f : α → β} [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₀ {G₀ : Type u_3} {β : Type u_5} {α : Type u_6} [MeasurableSpace β] [MeasurableSpace α] {f : α → β} {μ : MeasureTheory.Measure α} [GroupWithZero G₀] [MeasurableSpace G₀] [MulAction G₀ β] [MeasurableSMul G₀ β] {c : G₀} (hc : c ≠ 0) : AEMeasurable (fun (x : α) => c • f x) μ ↔ AEMeasurable f μ

Opposite monoid

instance MulOpposite.instMeasurableSpace {α : Type u_2} [h : MeasurableSpace α] : MeasurableSpace αᵐᵒᵖ

Equations

• MulOpposite.instMeasurableSpace = MeasurableSpace.map MulOpposite.op h

instance AddOpposite.instMeasurableSpace {α : Type u_2} [h : MeasurableSpace α] : MeasurableSpace αᵃᵒᵖ

Equations

• AddOpposite.instMeasurableSpace = MeasurableSpace.map AddOpposite.op h

theorem measurable_mul_op {α : Type u_2} [MeasurableSpace α] : Measurable MulOpposite.op

theorem measurable_add_op {α : Type u_2} [MeasurableSpace α] : Measurable AddOpposite.op

theorem measurable_mul_unop {α : Type u_2} [MeasurableSpace α] : Measurable MulOpposite.unop

theorem measurable_add_unop {α : Type u_2} [MeasurableSpace α] : Measurable AddOpposite.unop

instance MulOpposite.instMeasurableMul {M : Type u_2} [Mul M] [MeasurableSpace M] [MeasurableMul M] : MeasurableMul Mᵐᵒᵖ

instance AddOpposite.instMeasurableAdd {M : Type u_2} [Add M] [MeasurableSpace M] [MeasurableAdd M] : MeasurableAdd Mᵃᵒᵖ

instance MulOpposite.instMeasurableMul₂ {M : Type u_2} [Mul M] [MeasurableSpace M] [MeasurableMul₂ M] : MeasurableMul₂ Mᵐᵒᵖ

instance AddOpposite.instMeasurableMul₂ {M : Type u_2} [Add M] [MeasurableSpace M] [MeasurableAdd₂ M] : MeasurableAdd₂ Mᵃᵒᵖ

instance MeasurableSMul.op {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [MeasurableSpace α] [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] [MeasurableSMul M α] : MeasurableSMul Mᵐᵒᵖ α

If a scalar is central, then its right action is measurable when its left action is.

instance MeasurableVAdd.op {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [MeasurableSpace α] [VAdd M α] [VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α] [MeasurableVAdd M α] : MeasurableVAdd Mᵃᵒᵖ α

instance MeasurableSMul₂.op {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [MeasurableSpace α] [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] [MeasurableSMul₂ M α] : MeasurableSMul₂ Mᵐᵒᵖ α

If a scalar is central, then its right action is measurable when its left action is.

instance measurableSMul_opposite_of_mul {M : Type u_2} [Mul M] [MeasurableSpace M] [MeasurableMul M] : MeasurableSMul Mᵐᵒᵖ M

instance measurableVAdd_opposite_of_add {M : Type u_2} [Add M] [MeasurableSpace M] [MeasurableAdd M] : MeasurableVAdd Mᵃᵒᵖ M

instance measurableSMul₂_opposite_of_mul {M : Type u_2} [Mul M] [MeasurableSpace M] [MeasurableMul₂ M] : MeasurableSMul₂ Mᵐᵒᵖ M

instance measurableSMul₂_opposite_of_add {M : Type u_2} [Add M] [MeasurableSpace M] [MeasurableAdd₂ M] : MeasurableVAdd₂ Mᵃᵒᵖ M

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

@[deprecated List.measurable_sum (since := "2025-05-30")]

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

Alias of List.measurable_sum.

@[deprecated List.measurable_prod (since := "2025-05-30")]

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

Alias of List.measurable_prod.

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 μ

@[deprecated List.aemeasurable_sum (since := "2025-05-30")]

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 μ

Alias of List.aemeasurable_sum.

@[deprecated List.aemeasurable_prod (since := "2025-05-30")]

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 μ

Alias of List.aemeasurable_prod.

theorem List.measurable_fun_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 : α) => (map (fun (f : α → M) => f x) l).prod

theorem List.measurable_fun_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 : α) => (map (fun (f : α → M) => f x) l).sum

theorem List.aemeasurable_fun_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 : α) => (map (fun (f : α → M) => f x) l).prod) μ

theorem List.aemeasurable_fun_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 : α) => (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

@[deprecated Multiset.measurable_sum (since := "2025-05-30")]

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

Alias of Multiset.measurable_sum.

@[deprecated Multiset.measurable_prod (since := "2025-05-30")]

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

Alias of Multiset.measurable_prod.

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 μ

@[deprecated Multiset.aemeasurable_sum (since := "2025-05-30")]

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 μ

Alias of Multiset.aemeasurable_sum.

@[deprecated Multiset.aemeasurable_prod (since := "2025-05-30")]

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 μ

Alias of Multiset.aemeasurable_prod.

theorem Multiset.measurable_fun_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 : α) => (map (fun (f : α → M) => f x) s).prod

theorem Multiset.measurable_fun_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 : α) => (map (fun (f : α → M) => f x) s).sum

theorem Multiset.aemeasurable_fun_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 : α) => (map (fun (f : α → M) => f x) s).prod) μ

theorem Multiset.aemeasurable_fun_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 : α) => (map (fun (f : α → M) => f x) s).sum) μ

theorem Finset.measurable_fun_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_fun_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} [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_apply {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 ∈ s, 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_apply {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 ∈ s, 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.

@[deprecated Finset.measurable_sum_apply (since := "2025-05-30")]

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 ∈ s, Measurable ↿(f i)) (hg : Measurable g) : Measurable fun (a : α) => (∑ i ∈ s, f i a) (g a)

Alias of Finset.measurable_sum_apply.

---

Compositional version of Finset.measurable_sum for use by fun_prop.

@[deprecated Finset.measurable_prod_apply (since := "2025-05-30")]

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 ∈ s, Measurable ↿(f i)) (hg : Measurable g) : Measurable fun (a : α) => (∏ i ∈ s, f i a) (g a)

Alias of Finset.measurable_prod_apply.

---

Compositional version of Finset.measurable_prod 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) μ

@[deprecated Finset.aemeasurable_sum (since := "2025-05-30")]

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) μ

Alias of Finset.aemeasurable_sum.

@[deprecated Finset.aemeasurable_prod (since := "2025-05-30")]

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) μ

Alias of Finset.aemeasurable_prod.

theorem Finset.aemeasurable_fun_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_fun_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 α] : MeasurableMul α

@[instance 100]

instance DiscreteMeasurableSpace.toMeasurableAdd {α : Type u_1} [MeasurableSpace α] [Add α] [DiscreteMeasurableSpace α] : MeasurableAdd α

@[instance 100]

instance DiscreteMeasurableSpace.toMeasurableMul₂ {α : Type u_1} [MeasurableSpace α] [Mul α] [DiscreteMeasurableSpace (α × α)] : MeasurableMul₂ α

@[instance 100]

instance DiscreteMeasurableSpace.toMeasurableAdd₂ {α : Type u_1} [MeasurableSpace α] [Add α] [DiscreteMeasurableSpace (α × α)] : MeasurableAdd₂ α

@[instance 100]

instance DiscreteMeasurableSpace.toMeasurableInv {α : Type u_1} [MeasurableSpace α] [Inv α] [DiscreteMeasurableSpace α] : MeasurableInv α

@[instance 100]

instance DiscreteMeasurableSpace.toMeasurableNeg {α : Type u_1} [MeasurableSpace α] [Neg α] [DiscreteMeasurableSpace α] : MeasurableNeg α

@[instance 100]

instance DiscreteMeasurableSpace.toMeasurableDiv {α : Type u_1} [MeasurableSpace α] [Div α] [DiscreteMeasurableSpace α] : MeasurableDiv α

@[instance 100]

instance DiscreteMeasurableSpace.toMeasurableSub {α : Type u_1} [MeasurableSpace α] [Sub α] [DiscreteMeasurableSpace α] : MeasurableSub α

@[instance 100]

instance DiscreteMeasurableSpace.toMeasurableDiv₂ {α : Type u_1} [MeasurableSpace α] [Div α] [DiscreteMeasurableSpace (α × α)] : MeasurableDiv₂ α

@[instance 100]

instance DiscreteMeasurableSpace.toMeasurableSub₂ {α : Type u_1} [MeasurableSpace α] [Sub α] [DiscreteMeasurableSpace (α × α)] : MeasurableSub₂ α