Documentation

Mathlib.MeasureTheory.Group.Arithmetic

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:

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 #

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

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

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
    theorem MeasurableAdd.measurable_const_add {M : Type u_2} :
    ∀ {inst : MeasurableSpace M} {inst_1 : Add M} [self : MeasurableAdd M] (c : M), Measurable fun (x : M) => c + x
    theorem MeasurableAdd.measurable_add_const {M : Type u_2} :
    ∀ {inst : MeasurableSpace M} {inst_1 : Add M} [self : MeasurableAdd M] (c : M), Measurable fun (x : M) => x + c
    class MeasurableAdd₂ (M : Type u_2) [MeasurableSpace M] [Add M] :

    We say that a type has MeasurableAdd₂ if uncurry (· + ·) is a measurable functions. For a typeclass assuming measurability of (c + ·) and (· + c) see MeasurableAdd.

    Instances
      theorem MeasurableAdd₂.measurable_add {M : Type u_2} :
      ∀ {inst : MeasurableSpace M} {inst_1 : Add M} [self : MeasurableAdd₂ M], Measurable fun (p : M × M) => p.1 + p.2
      class MeasurableMul (M : Type u_2) [MeasurableSpace M] [Mul M] :

      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
        theorem MeasurableMul.measurable_const_mul {M : Type u_2} :
        ∀ {inst : MeasurableSpace M} {inst_1 : Mul M} [self : MeasurableMul M] (c : M), Measurable fun (x : M) => c * x
        theorem MeasurableMul.measurable_mul_const {M : Type u_2} :
        ∀ {inst : MeasurableSpace M} {inst_1 : Mul M} [self : MeasurableMul M] (c : M), Measurable fun (x : M) => x * c
        class MeasurableMul₂ (M : Type u_2) [MeasurableSpace M] [Mul M] :

        We say that a type has MeasurableMul₂ if uncurry (· * ·) is a measurable functions. For a typeclass assuming measurability of (c * ·) and (· * c) see MeasurableMul.

        Instances
          theorem MeasurableMul₂.measurable_mul {M : Type u_2} :
          ∀ {inst : MeasurableSpace M} {inst_1 : Mul M} [self : MeasurableMul₂ M], Measurable fun (p : M × M) => p.1 * p.2
          theorem Measurable.const_add {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [Add M] {m : MeasurableSpace α} {f : αM} [MeasurableAdd M] (hf : Measurable f) (c : M) :
          Measurable fun (x : α) => c + f x
          theorem Measurable.const_mul {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [Mul M] {m : MeasurableSpace α} {f : αM} [MeasurableMul M] (hf : Measurable f) (c : M) :
          Measurable fun (x : α) => c * f x
          theorem AEMeasurable.const_add {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [Add M] {m : MeasurableSpace α} {f : αM} {μ : MeasureTheory.Measure α} [MeasurableAdd M] (hf : AEMeasurable f μ) (c : M) :
          AEMeasurable (fun (x : α) => c + f x) μ
          theorem AEMeasurable.const_mul {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [Mul M] {m : MeasurableSpace α} {f : αM} {μ : MeasureTheory.Measure α} [MeasurableMul M] (hf : AEMeasurable f μ) (c : M) :
          AEMeasurable (fun (x : α) => c * f x) μ
          theorem Measurable.add_const {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [Add M] {m : MeasurableSpace α} {f : αM} [MeasurableAdd M] (hf : Measurable f) (c : M) :
          Measurable fun (x : α) => f x + c
          theorem Measurable.mul_const {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [Mul M] {m : MeasurableSpace α} {f : αM} [MeasurableMul M] (hf : Measurable f) (c : M) :
          Measurable fun (x : α) => f x * c
          theorem AEMeasurable.add_const {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [Add M] {m : MeasurableSpace α} {f : αM} {μ : MeasureTheory.Measure α} [MeasurableAdd M] (hf : AEMeasurable f μ) (c : M) :
          AEMeasurable (fun (x : α) => f x + c) μ
          theorem AEMeasurable.mul_const {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [Mul M] {m : MeasurableSpace α} {f : αM} {μ : MeasureTheory.Measure α} [MeasurableMul M] (hf : AEMeasurable f μ) (c : M) :
          AEMeasurable (fun (x : α) => f x * c) μ
          theorem Measurable.add {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [Add M] {m : MeasurableSpace α} {f : αM} {g : αM} [MeasurableAdd₂ M] (hf : Measurable f) (hg : Measurable g) :
          Measurable fun (a : α) => f a + g a
          theorem Measurable.mul {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [Mul M] {m : MeasurableSpace α} {f : αM} {g : αM} [MeasurableMul₂ M] (hf : Measurable f) (hg : Measurable g) :
          Measurable fun (a : α) => f a * g a
          theorem Measurable.add' {M : Type u_2} {α : Type u_3} {β : Type u_4} [MeasurableSpace M] [Add M] {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableAdd₂ M] {f : αβM} {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 Measurable.mul' {M : Type u_2} {α : Type u_3} {β : Type u_4} [MeasurableSpace M] [Mul M] {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableMul₂ M] {f : αβM} {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 AEMeasurable.add' {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [Add M] {m : MeasurableSpace α} {f : αM} {g : αM} {μ : MeasureTheory.Measure α} [MeasurableAdd₂ M] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
          AEMeasurable (f + g) μ
          theorem AEMeasurable.mul' {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [Mul M] {m : MeasurableSpace α} {f : αM} {g : αM} {μ : MeasureTheory.Measure α} [MeasurableMul₂ M] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
          AEMeasurable (f * g) μ
          theorem AEMeasurable.add {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [Add M] {m : MeasurableSpace α} {f : αM} {g : αM} {μ : MeasureTheory.Measure α} [MeasurableAdd₂ M] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
          AEMeasurable (fun (a : α) => f a + g a) μ
          theorem AEMeasurable.mul {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [Mul M] {m : MeasurableSpace α} {f : αM} {g : αM} {μ : MeasureTheory.Measure α} [MeasurableMul₂ M] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
          AEMeasurable (fun (a : α) => f a * g a) μ
          @[instance 100]
          Equations
          • =
          @[instance 100]
          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
          • =
          instance Pi.measurableMul₂ {ι : Type u_5} {α : ιType u_6} [(i : ι) → Mul (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableMul₂ (α i)] :
          MeasurableMul₂ ((i : ι) → α i)
          Equations
          • =
          theorem measurable_sub_const' {G : Type u_2} [SubNegMonoid G] [MeasurableSpace G] [MeasurableAdd G] (g : G) :
          Measurable fun (h : G) => h - g

          A version of measurable_sub_const that assumes MeasurableAdd instead of MeasurableSub. This can be nice to avoid unnecessary type-class assumptions.

          theorem measurable_div_const' {G : Type u_2} [DivInvMonoid G] [MeasurableSpace G] [MeasurableMul G] (g : G) :
          Measurable fun (h : G) => h / g

          A version of measurable_div_const that assumes MeasurableMul instead of MeasurableDiv. This can be nice to avoid unnecessary type-class assumptions.

          class MeasurablePow (β : Type u_2) (γ : Type u_3) [MeasurableSpace β] [MeasurableSpace γ] [Pow β γ] :

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

          Instances
            theorem MeasurablePow.measurable_pow {β : Type u_2} {γ : Type u_3} :
            ∀ {inst : MeasurableSpace β} {inst_1 : MeasurableSpace γ} {inst_2 : Pow β γ} [self : MeasurablePow β γ], Measurable fun (p : β × γ) => p.1 ^ p.2

            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) μ
            class MeasurableSub (G : Type u_2) [MeasurableSpace G] [Sub G] :

            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
              theorem MeasurableSub.measurable_const_sub {G : Type u_2} :
              ∀ {inst : MeasurableSpace G} {inst_1 : Sub G} [self : MeasurableSub G] (c : G), Measurable fun (x : G) => c - x
              theorem MeasurableSub.measurable_sub_const {G : Type u_2} :
              ∀ {inst : MeasurableSpace G} {inst_1 : Sub G} [self : MeasurableSub G] (c : G), Measurable fun (x : G) => x - c
              class MeasurableSub₂ (G : Type u_2) [MeasurableSpace G] [Sub G] :

              We say that a type has MeasurableSub₂ if uncurry (· - ·) is a measurable functions. For a typeclass assuming measurability of (c - ·) and (· - c) see MeasurableSub.

              Instances
                theorem MeasurableSub₂.measurable_sub {G : Type u_2} :
                ∀ {inst : MeasurableSpace G} {inst_1 : Sub G} [self : MeasurableSub₂ G], Measurable fun (p : G × G) => p.1 - p.2
                class MeasurableDiv (G₀ : Type u_2) [MeasurableSpace G₀] [Div G₀] :

                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
                  theorem MeasurableDiv.measurable_const_div {G₀ : Type u_2} :
                  ∀ {inst : MeasurableSpace G₀} {inst_1 : Div G₀} [self : MeasurableDiv G₀] (c : G₀), Measurable fun (x : G₀) => c / x
                  theorem MeasurableDiv.measurable_div_const {G₀ : Type u_2} :
                  ∀ {inst : MeasurableSpace G₀} {inst_1 : Div G₀} [self : MeasurableDiv G₀] (c : G₀), Measurable fun (x : G₀) => x / c
                  class MeasurableDiv₂ (G₀ : Type u_2) [MeasurableSpace G₀] [Div G₀] :

                  We say that a type has MeasurableDiv₂ if uncurry (· / ·) is a measurable functions. For a typeclass assuming measurability of (c / ·) and (· / c) see MeasurableDiv.

                  Instances
                    theorem MeasurableDiv₂.measurable_div {G₀ : Type u_2} :
                    ∀ {inst : MeasurableSpace G₀} {inst_1 : Div G₀} [self : MeasurableDiv₂ G₀], Measurable fun (p : G₀ × G₀) => p.1 / p.2
                    theorem Measurable.const_sub {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [Sub G] {m : MeasurableSpace α} {f : αG} [MeasurableSub G] (hf : Measurable f) (c : G) :
                    Measurable fun (x : α) => c - f x
                    theorem Measurable.const_div {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [Div G] {m : MeasurableSpace α} {f : αG} [MeasurableDiv G] (hf : Measurable f) (c : G) :
                    Measurable fun (x : α) => c / f x
                    theorem AEMeasurable.const_sub {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [Sub G] {m : MeasurableSpace α} {f : αG} {μ : MeasureTheory.Measure α} [MeasurableSub G] (hf : AEMeasurable f μ) (c : G) :
                    AEMeasurable (fun (x : α) => c - f x) μ
                    theorem AEMeasurable.const_div {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [Div G] {m : MeasurableSpace α} {f : αG} {μ : MeasureTheory.Measure α} [MeasurableDiv G] (hf : AEMeasurable f μ) (c : G) :
                    AEMeasurable (fun (x : α) => c / f x) μ
                    theorem Measurable.sub_const {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [Sub G] {m : MeasurableSpace α} {f : αG} [MeasurableSub G] (hf : Measurable f) (c : G) :
                    Measurable fun (x : α) => f x - c
                    theorem Measurable.div_const {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [Div G] {m : MeasurableSpace α} {f : αG} [MeasurableDiv G] (hf : Measurable f) (c : G) :
                    Measurable fun (x : α) => f x / c
                    theorem AEMeasurable.sub_const {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [Sub G] {m : MeasurableSpace α} {f : αG} {μ : MeasureTheory.Measure α} [MeasurableSub G] (hf : AEMeasurable f μ) (c : G) :
                    AEMeasurable (fun (x : α) => f x - c) μ
                    theorem AEMeasurable.div_const {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [Div G] {m : MeasurableSpace α} {f : αG} {μ : MeasureTheory.Measure α} [MeasurableDiv G] (hf : AEMeasurable f μ) (c : G) :
                    AEMeasurable (fun (x : α) => f x / c) μ
                    theorem Measurable.sub {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [Sub G] {m : MeasurableSpace α} {f : αG} {g : αG} [MeasurableSub₂ G] (hf : Measurable f) (hg : Measurable g) :
                    Measurable fun (a : α) => f a - g a
                    theorem Measurable.div {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [Div G] {m : MeasurableSpace α} {f : αG} {g : αG} [MeasurableDiv₂ G] (hf : Measurable f) (hg : Measurable g) :
                    Measurable fun (a : α) => f a / g a
                    theorem 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 : αβG} {h : αβ} (hf : Measurable f) (hg : Measurable g) (hh : Measurable h) :
                    Measurable fun (a : α) => (f a - g a) (h 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 : αβG} {h : αβ} (hf : Measurable f) (hg : Measurable g) (hh : Measurable h) :
                    Measurable fun (a : α) => (f a / g a) (h a)
                    theorem AEMeasurable.sub' {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [Sub G] {m : MeasurableSpace α} {f : αG} {g : αG} {μ : MeasureTheory.Measure α} [MeasurableSub₂ G] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
                    AEMeasurable (f - g) μ
                    theorem AEMeasurable.div' {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [Div G] {m : MeasurableSpace α} {f : αG} {g : αG} {μ : MeasureTheory.Measure α} [MeasurableDiv₂ G] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
                    AEMeasurable (f / g) μ
                    theorem AEMeasurable.sub {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [Sub G] {m : MeasurableSpace α} {f : αG} {g : αG} {μ : MeasureTheory.Measure α} [MeasurableSub₂ G] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
                    AEMeasurable (fun (a : α) => f a - g a) μ
                    theorem AEMeasurable.div {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [Div G] {m : MeasurableSpace α} {f : αG} {g : αG} {μ : MeasureTheory.Measure α} [MeasurableDiv₂ G] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
                    AEMeasurable (fun (a : α) => f a / g a) μ
                    @[instance 100]
                    Equations
                    • =
                    @[instance 100]
                    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
                    • =
                    instance Pi.measurableDiv₂ {ι : Type u_5} {α : ιType u_6} [(i : ι) → Div (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableDiv₂ (α i)] :
                    MeasurableDiv₂ ((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 : αE} {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 β} [inst : MeasurableSub₂ β] [inst : MeasurableSingletonClass β] {f g : αβ}, Measurable fMeasurable gMeasurableSet {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 : αE} {g : αE} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
                    MeasureTheory.NullMeasurableSet {x : α | f x = g x} μ
                    theorem measurableSet_eq_fun_of_countable {α : Type u_3} {m : MeasurableSpace α} {E : Type u_5} [MeasurableSpace E] [MeasurableSingletonClass E] [Countable E] {f : αE} {g : αE} (hf : Measurable f) (hg : Measurable g) :
                    MeasurableSet {x : α | f x = g x}
                    theorem ae_eq_trim_of_measurable {α : Type u_5} {E : Type u_6} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSpace E] [AddGroup E] [MeasurableSingletonClass E] [MeasurableSub₂ E] (hm : m m0) {f : αE} {g : αE} (hf : Measurable f) (hg : Measurable g) (hfg : f =ᵐ[μ] g) :
                    f =ᵐ[μ.trim hm] g
                    class MeasurableNeg (G : Type u_2) [Neg G] [MeasurableSpace G] :

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

                    Instances
                      theorem MeasurableNeg.measurable_neg {G : Type u_2} :
                      ∀ {inst : Neg G} {inst_1 : MeasurableSpace G} [self : MeasurableNeg G], Measurable Neg.neg
                      class MeasurableInv (G : Type u_2) [Inv G] [MeasurableSpace G] :

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

                      Instances
                        theorem MeasurableInv.measurable_inv {G : Type u_2} :
                        ∀ {inst : Inv G} {inst_1 : MeasurableSpace G} [self : MeasurableInv G], Measurable Inv.inv
                        @[instance 100]
                        Equations
                        • =
                        @[instance 100]
                        Equations
                        • =
                        theorem Measurable.neg {G : Type u_2} {α : Type u_3} [Neg G] [MeasurableSpace G] [MeasurableNeg G] {m : MeasurableSpace α} {f : αG} (hf : Measurable f) :
                        Measurable fun (x : α) => -f x
                        theorem Measurable.inv {G : Type u_2} {α : Type u_3} [Inv G] [MeasurableSpace G] [MeasurableInv G] {m : MeasurableSpace α} {f : αG} (hf : Measurable f) :
                        Measurable fun (x : α) => (f x)⁻¹
                        theorem AEMeasurable.neg {G : Type u_2} {α : Type u_3} [Neg G] [MeasurableSpace G] [MeasurableNeg G] {m : MeasurableSpace α} {f : αG} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) :
                        AEMeasurable (fun (x : α) => -f x) μ
                        theorem AEMeasurable.inv {G : Type u_2} {α : Type u_3} [Inv G] [MeasurableSpace G] [MeasurableInv G] {m : MeasurableSpace α} {f : αG} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) :
                        AEMeasurable (fun (x : α) => (f x)⁻¹) μ
                        @[simp]
                        theorem measurable_neg_iff {α : Type u_3} {m : MeasurableSpace α} {G : Type u_4} [AddGroup G] [MeasurableSpace G] [MeasurableNeg G] {f : αG} :
                        (Measurable fun (x : α) => -f x) Measurable f
                        @[simp]
                        theorem measurable_inv_iff {α : Type u_3} {m : MeasurableSpace α} {G : Type u_4} [Group G] [MeasurableSpace G] [MeasurableInv G] {f : αG} :
                        (Measurable fun (x : α) => (f x)⁻¹) Measurable f
                        @[simp]
                        theorem aemeasurable_neg_iff {α : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G : Type u_4} [AddGroup G] [MeasurableSpace G] [MeasurableNeg G] {f : αG} :
                        AEMeasurable (fun (x : α) => -f x) μ AEMeasurable f μ
                        @[simp]
                        theorem aemeasurable_inv_iff {α : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G : Type u_4} [Group G] [MeasurableSpace G] [MeasurableInv G] {f : αG} :
                        AEMeasurable (fun (x : α) => (f x)⁻¹) μ AEMeasurable f μ
                        @[simp]
                        theorem measurable_inv_iff₀ {α : Type u_3} {m : MeasurableSpace α} {G₀ : Type u_4} [GroupWithZero G₀] [MeasurableSpace G₀] [MeasurableInv G₀] {f : αG₀} :
                        (Measurable fun (x : α) => (f x)⁻¹) Measurable f
                        @[simp]
                        theorem aemeasurable_inv_iff₀ {α : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G₀ : Type u_4} [GroupWithZero G₀] [MeasurableSpace G₀] [MeasurableInv G₀] {f : αG₀} :
                        AEMeasurable (fun (x : α) => (f x)⁻¹) μ AEMeasurable f μ
                        instance Pi.measurableNeg {ι : Type u_4} {α : ιType u_5} [(i : ι) → Neg (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableNeg (α i)] :
                        MeasurableNeg ((i : ι) → α i)
                        Equations
                        • =
                        instance Pi.measurableInv {ι : Type u_4} {α : ιType u_5} [(i : ι) → Inv (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableInv (α i)] :
                        MeasurableInv ((i : ι) → α i)
                        Equations
                        • =
                        theorem MeasurableSet.neg {G : Type u_2} [Neg G] [MeasurableSpace G] [MeasurableNeg G] {s : Set G} (hs : MeasurableSet s) :
                        theorem Measurable.add_iff_right {α : Type u_1} {G : Type u_2} [MeasurableSpace G] [MeasurableSpace α] [AddCommGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] {f : αG} {g : αG} (hf : Measurable f) :
                        theorem Measurable.mul_iff_right {α : Type u_1} {G : Type u_2} [MeasurableSpace G] [MeasurableSpace α] [CommGroup G] [MeasurableMul₂ G] [MeasurableInv G] {f : αG} {g : αG} (hf : Measurable f) :
                        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 : αG} (hf : AEMeasurable f μ) :
                        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 : αG} (hf : AEMeasurable f μ) :
                        theorem Measurable.add_iff_left {α : Type u_1} {G : Type u_2} [MeasurableSpace G] [MeasurableSpace α] [AddCommGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] {f : αG} {g : αG} (hf : Measurable f) :
                        theorem Measurable.mul_iff_left {α : Type u_1} {G : Type u_2} [MeasurableSpace G] [MeasurableSpace α] [CommGroup G] [MeasurableMul₂ G] [MeasurableInv G] {f : αG} {g : αG} (hf : Measurable f) :
                        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 : αG} (hf : AEMeasurable f μ) :
                        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 : αG} (hf : AEMeasurable f μ) :
                        @[instance 100]
                        Equations
                        • =
                        @[instance 100]
                        Equations
                        • =
                        @[instance 100]
                        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
                          theorem MeasurableVAdd.measurable_const_vadd {M : Type u_2} {α : Type u_3} :
                          ∀ {inst : VAdd M α} {inst_1 : MeasurableSpace M} {inst_2 : MeasurableSpace α} [self : MeasurableVAdd M α] (c : M), Measurable fun (x : α) => c +ᵥ x
                          theorem MeasurableVAdd.measurable_vadd_const {M : Type u_2} {α : Type u_3} :
                          ∀ {inst : VAdd M α} {inst_1 : MeasurableSpace M} {inst_2 : MeasurableSpace α} [self : MeasurableVAdd M α] (x : α), Measurable fun (x_1 : M) => x_1 +ᵥ x
                          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
                            theorem MeasurableSMul.measurable_const_smul {M : Type u_2} {α : Type u_3} :
                            ∀ {inst : SMul M α} {inst_1 : MeasurableSpace M} {inst_2 : MeasurableSpace α} [self : MeasurableSMul M α] (c : M), Measurable fun (x : α) => c x
                            theorem MeasurableSMul.measurable_smul_const {M : Type u_2} {α : Type u_3} :
                            ∀ {inst : SMul M α} {inst_1 : MeasurableSpace M} {inst_2 : MeasurableSpace α} [self : MeasurableSMul M α] (x : α), Measurable fun (x_1 : M) => x_1 x
                            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.

                            Instances
                              theorem MeasurableVAdd₂.measurable_vadd {M : Type u_2} {α : Type u_3} :
                              ∀ {inst : VAdd M α} {inst_1 : MeasurableSpace M} {inst_2 : MeasurableSpace α} [self : MeasurableVAdd₂ M α], Measurable (Function.uncurry fun (x1 : M) (x2 : α) => x1 +ᵥ x2)
                              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.

                              Instances
                                theorem MeasurableSMul₂.measurable_smul {M : Type u_2} {α : Type u_3} :
                                ∀ {inst : SMul M α} {inst_1 : MeasurableSpace M} {inst_2 : MeasurableSpace α} [self : MeasurableSMul₂ M α], Measurable (Function.uncurry fun (x1 : M) (x2 : α) => x1 x2)
                                Equations
                                • =
                                Equations
                                • =
                                Equations
                                • =
                                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 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 AddSubgroup.measurableVAdd {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [MeasurableSpace α] [AddGroup G] [AddAction G α] [MeasurableVAdd G α] (s : AddSubgroup G) :
                                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
                                • =
                                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} [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} {β : 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 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 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) μ
                                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) μ
                                @[instance 100]
                                Equations
                                • =
                                @[instance 100]
                                Equations
                                • =
                                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 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 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 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 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) :
                                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) :
                                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 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 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 α} (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 α} (hf : AEMeasurable g μ) (c : M) :
                                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) μ
                                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 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
                                • =

                                AddMonoid.SMul is measurable.

                                Equations
                                • =
                                @[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
                                @[simp]
                                theorem measurableSMul₂_iterateMulAct {α : Type u_2} :
                                ∀ {x : MeasurableSpace α} {f : αα}, MeasurableSMul₂ (IterateMulAct f) α 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 measurable_const_smul_iff {β : Type u_3} {α : Type u_4} [MeasurableSpace β] [MeasurableSpace α] {f : αβ} {G : Type u_5} [Group G] [MeasurableSpace G] [MulAction G β] [MeasurableSMul G β] (c : G) :
                                (Measurable fun (x : α) => c f x) Measurable f
                                theorem aemeasurable_const_vadd_iff {β : Type u_3} {α : Type u_4} [MeasurableSpace β] [MeasurableSpace α] {f : αβ} {μ : MeasureTheory.Measure α} {G : Type u_5} [AddGroup G] [MeasurableSpace G] [AddAction G β] [MeasurableVAdd G β] (c : G) :
                                AEMeasurable (fun (x : α) => c +ᵥ f x) μ AEMeasurable f μ
                                theorem aemeasurable_const_smul_iff {β : Type u_3} {α : Type u_4} [MeasurableSpace β] [MeasurableSpace α] {f : αβ} {μ : MeasureTheory.Measure α} {G : Type u_5} [Group G] [MeasurableSpace G] [MulAction G β] [MeasurableSMul G β] (c : G) :
                                AEMeasurable (fun (x : α) => c f x) μ AEMeasurable f μ
                                Equations
                                Equations
                                Equations
                                • =
                                instance Units.measurableSMul {M : Type u_2} {β : Type u_3} [MeasurableSpace M] [MeasurableSpace β] [Monoid M] [MulAction M β] [MeasurableSMul M β] :
                                Equations
                                • =
                                theorem IsAddUnit.measurable_const_vadd_iff {M : Type u_2} {β : Type u_3} {α : Type u_4} [MeasurableSpace M] [MeasurableSpace β] [AddMonoid M] [AddAction M β] [MeasurableVAdd M β] [MeasurableSpace α] {f : αβ} {c : M} (hc : IsAddUnit c) :
                                (Measurable fun (x : α) => c +ᵥ f x) Measurable f
                                theorem IsUnit.measurable_const_smul_iff {M : Type u_2} {β : Type u_3} {α : Type u_4} [MeasurableSpace M] [MeasurableSpace β] [Monoid M] [MulAction M β] [MeasurableSMul M β] [MeasurableSpace α] {f : αβ} {c : M} (hc : IsUnit c) :
                                (Measurable fun (x : α) => c f x) Measurable f
                                theorem IsAddUnit.aemeasurable_const_vadd_iff {M : Type u_2} {β : Type u_3} {α : Type u_4} [MeasurableSpace M] [MeasurableSpace β] [AddMonoid M] [AddAction M β] [MeasurableVAdd M β] [MeasurableSpace α] {f : αβ} {μ : MeasureTheory.Measure α} {c : M} (hc : IsAddUnit c) :
                                AEMeasurable (fun (x : α) => c +ᵥ f x) μ AEMeasurable f μ
                                theorem IsUnit.aemeasurable_const_smul_iff {M : Type u_2} {β : Type u_3} {α : Type u_4} [MeasurableSpace M] [MeasurableSpace β] [Monoid M] [MulAction M β] [MeasurableSMul M β] [MeasurableSpace α] {f : αβ} {μ : MeasureTheory.Measure α} {c : M} (hc : IsUnit c) :
                                AEMeasurable (fun (x : α) => c f x) μ AEMeasurable f μ
                                theorem measurable_const_smul_iff₀ {β : Type u_3} {α : Type u_4} [MeasurableSpace β] [MeasurableSpace α] {f : αβ} {G₀ : Type u_6} [GroupWithZero G₀] [MeasurableSpace G₀] [MulAction G₀ β] [MeasurableSMul G₀ β] {c : G₀} (hc : c 0) :
                                (Measurable fun (x : α) => c f x) Measurable f
                                theorem aemeasurable_const_smul_iff₀ {β : Type u_3} {α : Type u_4} [MeasurableSpace β] [MeasurableSpace α] {f : αβ} {μ : MeasureTheory.Measure α} {G₀ : Type u_6} [GroupWithZero G₀] [MeasurableSpace G₀] [MulAction G₀ β] [MeasurableSMul G₀ β] {c : G₀} (hc : c 0) :
                                AEMeasurable (fun (x : α) => c f x) μ AEMeasurable f μ

                                Opposite monoid #

                                Equations
                                Equations
                                theorem measurable_add_op {α : Type u_2} [MeasurableSpace α] :
                                Measurable AddOpposite.op
                                theorem measurable_mul_op {α : Type u_2} [MeasurableSpace α] :
                                Measurable MulOpposite.op
                                theorem measurable_add_unop {α : Type u_2} [MeasurableSpace α] :
                                Measurable AddOpposite.unop
                                theorem measurable_mul_unop {α : Type u_2} [MeasurableSpace α] :
                                Measurable MulOpposite.unop

                                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
                                • =

                                Big operators: and #

                                theorem List.measurable_sum' {M : Type u_2} {α : Type u_3} [AddMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] {m : MeasurableSpace α} (l : List (αM)) (hl : fl, Measurable f) :
                                theorem List.measurable_prod' {M : Type u_2} {α : Type u_3} [Monoid M] [MeasurableSpace M] [MeasurableMul₂ M] {m : MeasurableSpace α} (l : List (αM)) (hl : fl, Measurable f) :
                                Measurable 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 : fl, AEMeasurable f μ) :
                                AEMeasurable 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 : fl, AEMeasurable f μ) :
                                AEMeasurable 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 : fl, Measurable f) :
                                Measurable fun (x : α) => (List.map (fun (f : αM) => f x) 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 : fl, Measurable f) :
                                Measurable 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 : fl, AEMeasurable f μ) :
                                AEMeasurable (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 : fl, AEMeasurable f μ) :
                                AEMeasurable (fun (x : α) => (List.map (fun (f : αM) => f x) 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 : fl, Measurable f) :
                                theorem Multiset.measurable_prod' {M : Type u_2} {α : Type u_4} [CommMonoid M] [MeasurableSpace M] [MeasurableMul₂ M] {m : MeasurableSpace α} (l : Multiset (αM)) (hl : fl, Measurable f) :
                                Measurable 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 : fl, AEMeasurable f μ) :
                                AEMeasurable 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 : fl, AEMeasurable f μ) :
                                AEMeasurable l.prod μ
                                theorem Multiset.measurable_sum {M : Type u_2} {α : Type u_4} [AddCommMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] {m : MeasurableSpace α} (s : Multiset (αM)) (hs : fs, Measurable f) :
                                Measurable fun (x : α) => (Multiset.map (fun (f : αM) => f x) s).sum
                                theorem Multiset.measurable_prod {M : Type u_2} {α : Type u_4} [CommMonoid M] [MeasurableSpace M] [MeasurableMul₂ M] {m : MeasurableSpace α} (s : Multiset (αM)) (hs : fs, Measurable f) :
                                Measurable 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 : fs, AEMeasurable f μ) :
                                AEMeasurable (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 : fs, AEMeasurable f μ) :
                                AEMeasurable (fun (x : α) => (Multiset.map (fun (f : αM) => f x) s).prod) μ
                                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 : is, Measurable (f i)) :
                                Measurable fun (a : α) => is, 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 : is, Measurable (f i)) :
                                Measurable fun (a : α) => is, f i a
                                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 : α) => (∑ is, f i a) (g a)

                                Compositional version of Finset.measurable_sum for use by fun_prop.

                                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 : α) => (∏ is, f i a) (g a)

                                Compositional version of Finset.measurable_prod for use by fun_prop.

                                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 : is, AEMeasurable (f i) μ) :
                                AEMeasurable (∑ is, 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 : is, AEMeasurable (f i) μ) :
                                AEMeasurable (∏ is, 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 : is, AEMeasurable (f i) μ) :
                                AEMeasurable (fun (a : α) => is, f i a) μ
                                theorem Finset.aemeasurable_prod {M : Type u_2} {ι : Type u_3} {α : Type u_4} [CommMonoid M] [MeasurableSpace M] [MeasurableMul₂ M] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ιαM} (s : Finset ι) (hf : is, AEMeasurable (f i) μ) :
                                AEMeasurable (fun (a : α) => is, f i a) μ
                                @[instance 100]
                                Equations
                                • =
                                @[instance 100]
                                Equations
                                • =
                                @[instance 100]
                                Equations
                                • =
                                @[instance 100]
                                Equations
                                • =
                                @[instance 100]
                                Equations
                                • =
                                @[instance 100]
                                Equations
                                • =
                                @[instance 100]
                                Equations
                                • =
                                @[instance 100]
                                Equations
                                • =
                                @[instance 100]
                                Equations
                                • =
                                @[instance 100]
                                Equations
                                • =