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
    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
      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
        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 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) :
          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) :
          theorem Measurable.add {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [Add M] {m : MeasurableSpace α} {f : αM} {g : αM} [MeasurableAdd₂ M] (hf : Measurable f) (hg : Measurable g) :
          Measurable fun (a : α) => f a + g a
          theorem Measurable.mul {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [Mul M] {m : MeasurableSpace α} {f : αM} {g : αM} [MeasurableMul₂ M] (hf : Measurable f) (hg : Measurable g) :
          Measurable fun (a : α) => f a * g a
          theorem AEMeasurable.add' {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [Add M] {m : MeasurableSpace α} {f : αM} {g : αM} {μ : MeasureTheory.Measure α} [MeasurableAdd₂ M] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
          AEMeasurable (f + g) μ
          theorem AEMeasurable.mul' {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [Mul M] {m : MeasurableSpace α} {f : αM} {g : αM} {μ : MeasureTheory.Measure α} [MeasurableMul₂ M] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
          AEMeasurable (f * g) μ
          theorem AEMeasurable.add {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [Add M] {m : MeasurableSpace α} {f : αM} {g : αM} {μ : MeasureTheory.Measure α} [MeasurableAdd₂ M] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
          AEMeasurable (fun (a : α) => f a + g a) μ
          theorem AEMeasurable.mul {M : Type u_2} {α : Type u_3} [MeasurableSpace M] [Mul M] {m : MeasurableSpace α} {f : αM} {g : αM} {μ : MeasureTheory.Measure α} [MeasurableMul₂ M] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
          AEMeasurable (fun (a : α) => f a * g a) μ
          instance Pi.measurableAdd {ι : Type u_4} {α : ιType u_5} [(i : ι) → Add (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableAdd (α i)] :
          MeasurableAdd ((i : ι) → α i)
          Equations
          • =
          instance Pi.measurableMul {ι : Type u_4} {α : ιType u_5} [(i : ι) → Mul (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableMul (α i)] :
          MeasurableMul ((i : ι) → α i)
          Equations
          • =
          instance Pi.measurableAdd₂ {ι : Type u_4} {α : ιType u_5} [(i : ι) → Add (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableAdd₂ (α i)] :
          MeasurableAdd₂ ((i : ι) → α i)
          Equations
          • =
          instance Pi.measurableMul₂ {ι : Type u_4} {α : ιType u_5} [(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

            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
              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
                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
                  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 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) :
                    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) :
                    theorem Measurable.sub {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [Sub G] {m : MeasurableSpace α} {f : αG} {g : αG} [MeasurableSub₂ G] (hf : Measurable f) (hg : Measurable g) :
                    Measurable fun (a : α) => f a - g a
                    theorem Measurable.div {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [Div G] {m : MeasurableSpace α} {f : αG} {g : αG} [MeasurableDiv₂ G] (hf : Measurable f) (hg : Measurable g) :
                    Measurable fun (a : α) => f a / g a
                    theorem AEMeasurable.sub' {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [Sub G] {m : MeasurableSpace α} {f : αG} {g : αG} {μ : MeasureTheory.Measure α} [MeasurableSub₂ G] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
                    AEMeasurable (f - g) μ
                    theorem AEMeasurable.div' {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [Div G] {m : MeasurableSpace α} {f : αG} {g : αG} {μ : MeasureTheory.Measure α} [MeasurableDiv₂ G] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
                    AEMeasurable (f / g) μ
                    theorem AEMeasurable.sub {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [Sub G] {m : MeasurableSpace α} {f : αG} {g : αG} {μ : MeasureTheory.Measure α} [MeasurableSub₂ G] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
                    AEMeasurable (fun (a : α) => f a - g a) μ
                    theorem AEMeasurable.div {G : Type u_2} {α : Type u_3} [MeasurableSpace G] [Div G] {m : MeasurableSpace α} {f : αG} {g : αG} {μ : MeasureTheory.Measure α} [MeasurableDiv₂ G] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
                    AEMeasurable (fun (a : α) => f a / g a) μ
                    instance Pi.measurableSub {ι : Type u_4} {α : ιType u_5} [(i : ι) → Sub (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableSub (α i)] :
                    MeasurableSub ((i : ι) → α i)
                    Equations
                    • =
                    instance Pi.measurableDiv {ι : Type u_4} {α : ιType u_5} [(i : ι) → Div (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableDiv (α i)] :
                    MeasurableDiv ((i : ι) → α i)
                    Equations
                    • =
                    instance Pi.measurableSub₂ {ι : Type u_4} {α : ιType u_5} [(i : ι) → Sub (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableSub₂ (α i)] :
                    MeasurableSub₂ ((i : ι) → α i)
                    Equations
                    • =
                    instance Pi.measurableDiv₂ {ι : Type u_4} {α : ιType u_5} [(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_4} [MeasurableSpace E] [AddGroup E] [MeasurableSingletonClass E] [MeasurableSub₂ E] {f : αE} {g : αE} (hf : Measurable f) (hg : Measurable g) :
                    MeasurableSet {x : α | f x = g x}
                    theorem measurableSet_eq_fun' {α : Type u_3} {m : MeasurableSpace α} {β : Type u_4} [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_4} [MeasurableSpace E] [AddGroup E] [MeasurableSingletonClass E] [MeasurableSub₂ E] {f : αE} {g : αE} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
                    MeasureTheory.NullMeasurableSet {x : α | f x = g x} μ
                    theorem measurableSet_eq_fun_of_countable {α : Type u_3} {m : MeasurableSpace α} {E : Type u_4} [MeasurableSpace E] [MeasurableSingletonClass E] [Countable E] {f : αE} {g : αE} (hf : Measurable f) (hg : Measurable g) :
                    MeasurableSet {x : α | f x = g x}
                    theorem ae_eq_trim_of_measurable {α : Type u_4} {E : Type u_5} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSpace E] [AddGroup E] [MeasurableSingletonClass E] [MeasurableSub₂ E] (hm : m m0) {f : αE} {g : αE} (hf : Measurable f) (hg : Measurable g) (hfg : f =ᶠ[MeasureTheory.Measure.ae μ] g) :
                    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
                      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 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) :
                        Equations
                        • =
                        class MeasurableVAdd (M : Type u_2) (α : Type u_3) [VAdd M α] [MeasurableSpace M] [MeasurableSpace α] :

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

                        • measurable_const_vadd : ∀ (c : M), Measurable fun (x : α) => c +ᵥ x
                        • measurable_vadd_const : ∀ (x : α), Measurable fun (x_1 : M) => x_1 +ᵥ x
                        Instances
                          class MeasurableSMul (M : Type u_2) (α : Type u_3) [SMul M α] [MeasurableSpace M] [MeasurableSpace α] :

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

                          • measurable_const_smul : ∀ (c : M), Measurable fun (x : α) => c x
                          • measurable_smul_const : ∀ (x : α), Measurable fun (x_1 : M) => x_1 x
                          Instances
                            class MeasurableVAdd₂ (M : Type u_2) (α : Type u_3) [VAdd M α] [MeasurableSpace M] [MeasurableSpace α] :

                            We say that the action of M on α has MeasurableVAdd₂ if the map (c, x) ↦ c +ᵥ x is a measurable function.

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

                              We say that the action of M on α has Measurable_SMul₂ if the map (c, x) ↦ c • x is a measurable function.

                              Instances
                                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} {β : Type u_3} {α : Type u_4} [MeasurableSpace M] [MeasurableSpace β] [VAdd M β] {m : MeasurableSpace α} {f : αM} {g : αβ} [MeasurableVAdd₂ M β] (hf : Measurable f) (hg : Measurable g) :
                                Measurable fun (x : α) => f x +ᵥ g x
                                theorem Measurable.smul {M : Type u_2} {β : Type u_3} {α : Type u_4} [MeasurableSpace M] [MeasurableSpace β] [SMul M β] {m : MeasurableSpace α} {f : αM} {g : αβ} [MeasurableSMul₂ M β] (hf : Measurable f) (hg : Measurable g) :
                                Measurable fun (x : α) => f x g x
                                theorem AEMeasurable.vadd {M : Type u_2} {β : Type u_3} {α : Type u_4} [MeasurableSpace M] [MeasurableSpace β] [VAdd M β] {m : MeasurableSpace α} {f : αM} {g : αβ} [MeasurableVAdd₂ M β] {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
                                AEMeasurable (fun (x : α) => f x +ᵥ g x) μ
                                theorem AEMeasurable.smul {M : Type u_2} {β : Type u_3} {α : Type u_4} [MeasurableSpace M] [MeasurableSpace β] [SMul M β] {m : MeasurableSpace α} {f : αM} {g : αβ} [MeasurableSMul₂ M β] {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
                                AEMeasurable (fun (x : α) => f x g x) μ
                                Equations
                                • =
                                Equations
                                • =
                                theorem Measurable.vadd_const {M : Type u_2} {β : Type u_3} {α : Type u_4} [MeasurableSpace M] [MeasurableSpace β] [VAdd M β] {m : MeasurableSpace α} {f : αM} [MeasurableVAdd M β] (hf : Measurable f) (y : β) :
                                Measurable fun (x : α) => f x +ᵥ y
                                theorem Measurable.smul_const {M : Type u_2} {β : Type u_3} {α : Type u_4} [MeasurableSpace M] [MeasurableSpace β] [SMul M β] {m : MeasurableSpace α} {f : αM} [MeasurableSMul M β] (hf : Measurable f) (y : β) :
                                Measurable fun (x : α) => f x y
                                theorem AEMeasurable.vadd_const {M : Type u_2} {β : Type u_3} {α : Type u_4} [MeasurableSpace M] [MeasurableSpace β] [VAdd M β] {m : MeasurableSpace α} {f : αM} [MeasurableVAdd M β] {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) (y : β) :
                                AEMeasurable (fun (x : α) => f x +ᵥ y) μ
                                theorem AEMeasurable.smul_const {M : Type u_2} {β : Type u_3} {α : Type u_4} [MeasurableSpace M] [MeasurableSpace β] [SMul M β] {m : MeasurableSpace α} {f : αM} [MeasurableSMul M β] {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) (y : β) :
                                AEMeasurable (fun (x : α) => f x y) μ
                                theorem Measurable.const_vadd' {M : Type u_2} {β : Type u_3} {α : Type u_4} [MeasurableSpace M] [MeasurableSpace β] [VAdd M β] {m : MeasurableSpace α} {g : αβ} [MeasurableVAdd M β] (hg : Measurable g) (c : M) :
                                Measurable fun (x : α) => c +ᵥ g x
                                theorem Measurable.const_smul' {M : Type u_2} {β : Type u_3} {α : Type u_4} [MeasurableSpace M] [MeasurableSpace β] [SMul M β] {m : MeasurableSpace α} {g : αβ} [MeasurableSMul M β] (hg : Measurable g) (c : M) :
                                Measurable fun (x : α) => c g x
                                theorem Measurable.const_vadd {M : Type u_2} {β : Type u_3} {α : Type u_4} [MeasurableSpace M] [MeasurableSpace β] [VAdd M β] {m : MeasurableSpace α} {g : αβ} [MeasurableVAdd M β] (hg : Measurable g) (c : M) :
                                theorem Measurable.const_smul {M : Type u_2} {β : Type u_3} {α : Type u_4} [MeasurableSpace M] [MeasurableSpace β] [SMul M β] {m : MeasurableSpace α} {g : αβ} [MeasurableSMul M β] (hg : Measurable g) (c : M) :
                                theorem AEMeasurable.const_vadd' {M : Type u_2} {β : Type u_3} {α : Type u_4} [MeasurableSpace M] [MeasurableSpace β] [VAdd M β] {m : MeasurableSpace α} {g : αβ} [MeasurableVAdd M β] {μ : MeasureTheory.Measure α} (hg : AEMeasurable g μ) (c : M) :
                                AEMeasurable (fun (x : α) => c +ᵥ g x) μ
                                theorem AEMeasurable.const_smul' {M : Type u_2} {β : Type u_3} {α : Type u_4} [MeasurableSpace M] [MeasurableSpace β] [SMul M β] {m : MeasurableSpace α} {g : αβ} [MeasurableSMul M β] {μ : MeasureTheory.Measure α} (hg : AEMeasurable g μ) (c : M) :
                                AEMeasurable (fun (x : α) => c g x) μ
                                theorem AEMeasurable.const_vadd {M : Type u_2} {β : Type u_3} {α : Type u_4} [MeasurableSpace M] [MeasurableSpace β] [VAdd M β] {m : MeasurableSpace α} {g : αβ} [MeasurableVAdd M β] {μ : MeasureTheory.Measure α} (hf : AEMeasurable g μ) (c : M) :
                                theorem AEMeasurable.const_smul {M : Type u_2} {β : Type u_3} {α : Type u_4} [MeasurableSpace M] [MeasurableSpace β] [SMul M β] {m : MeasurableSpace α} {g : αβ} [MeasurableSMul M β] {μ : MeasureTheory.Measure α} (hf : AEMeasurable g μ) (c : M) :
                                AEMeasurable (c g) μ
                                instance Pi.measurableVAdd {M : Type u_2} [MeasurableSpace M] {ι : Type u_5} {α : ιType u_6} [(i : ι) → VAdd M (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableVAdd M (α i)] :
                                MeasurableVAdd M ((i : ι) → α i)
                                Equations
                                • =
                                instance Pi.measurableSMul {M : Type u_2} [MeasurableSpace M] {ι : Type u_5} {α : ιType u_6} [(i : ι) → SMul M (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableSMul M (α i)] :
                                MeasurableSMul M ((i : ι) → α i)
                                Equations
                                • =

                                AddMonoid.SMul is measurable.

                                Equations
                                • =
                                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
                                abbrev IsAddUnit.measurable_const_vadd_iff.match_1 {M : Type u_1} [AddMonoid M] {c : M} (motive : IsAddUnit cProp) :
                                ∀ (hc : IsAddUnit c), (∀ (u : AddUnits M) (hu : u = c), motive )motive hc
                                Equations
                                • =
                                Instances For
                                  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) :
                                  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 μ) :
                                  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 μ) :
                                  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.sum (List.map (fun (f : αM) => f x) l)
                                  theorem List.measurable_prod {M : Type u_2} {α : Type u_3} [Monoid M] [MeasurableSpace M] [MeasurableMul₂ M] {m : MeasurableSpace α} (l : List (αM)) (hl : fl, Measurable f) :
                                  Measurable fun (x : α) => List.prod (List.map (fun (f : αM) => f x) l)
                                  theorem List.aemeasurable_sum {M : Type u_2} {α : Type u_3} [AddMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (l : List (αM)) (hl : fl, AEMeasurable f μ) :
                                  AEMeasurable (fun (x : α) => List.sum (List.map (fun (f : αM) => f x) l)) μ
                                  theorem List.aemeasurable_prod {M : Type u_2} {α : Type u_3} [Monoid M] [MeasurableSpace M] [MeasurableMul₂ M] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (l : List (αM)) (hl : fl, AEMeasurable f μ) :
                                  AEMeasurable (fun (x : α) => List.prod (List.map (fun (f : αM) => f x) l)) μ
                                  theorem Multiset.measurable_sum' {M : Type u_2} {α : Type u_4} [AddCommMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] {m : MeasurableSpace α} (l : Multiset (αM)) (hl : 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) :
                                  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 μ) :
                                  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 μ) :
                                  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.sum (Multiset.map (fun (f : αM) => f x) s)
                                  theorem Multiset.measurable_prod {M : Type u_2} {α : Type u_4} [CommMonoid M] [MeasurableSpace M] [MeasurableMul₂ M] {m : MeasurableSpace α} (s : Multiset (αM)) (hs : fs, Measurable f) :
                                  Measurable fun (x : α) => Multiset.prod (Multiset.map (fun (f : αM) => f x) s)
                                  theorem Multiset.aemeasurable_sum {M : Type u_2} {α : Type u_4} [AddCommMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Multiset (αM)) (hs : fs, AEMeasurable f μ) :
                                  AEMeasurable (fun (x : α) => Multiset.sum (Multiset.map (fun (f : αM) => f x) s)) μ
                                  theorem Multiset.aemeasurable_prod {M : Type u_2} {α : Type u_4} [CommMonoid M] [MeasurableSpace M] [MeasurableMul₂ M] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Multiset (αM)) (hs : fs, AEMeasurable f μ) :
                                  AEMeasurable (fun (x : α) => Multiset.prod (Multiset.map (fun (f : αM) => f x) s)) μ
                                  theorem Finset.measurable_sum' {M : Type u_2} {ι : Type u_3} {α : Type u_4} [AddCommMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] {m : MeasurableSpace α} {f : ιαM} (s : Finset ι) (hf : is, Measurable (f i)) :
                                  Measurable (Finset.sum s fun (i : ι) => f i)
                                  theorem Finset.measurable_prod' {M : Type u_2} {ι : Type u_3} {α : Type u_4} [CommMonoid M] [MeasurableSpace M] [MeasurableMul₂ M] {m : MeasurableSpace α} {f : ιαM} (s : Finset ι) (hf : is, Measurable (f i)) :
                                  Measurable (Finset.prod s fun (i : ι) => f i)
                                  theorem Finset.measurable_sum {M : Type u_2} {ι : Type u_3} {α : Type u_4} [AddCommMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] {m : MeasurableSpace α} {f : ιαM} (s : Finset ι) (hf : is, Measurable (f i)) :
                                  Measurable fun (a : α) => Finset.sum s fun (i : ι) => f i a
                                  theorem Finset.measurable_prod {M : Type u_2} {ι : Type u_3} {α : Type u_4} [CommMonoid M] [MeasurableSpace M] [MeasurableMul₂ M] {m : MeasurableSpace α} {f : ιαM} (s : Finset ι) (hf : is, Measurable (f i)) :
                                  Measurable fun (a : α) => Finset.prod s fun (i : ι) => f i a
                                  theorem Finset.aemeasurable_sum' {M : Type u_2} {ι : Type u_3} {α : Type u_4} [AddCommMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ιαM} (s : Finset ι) (hf : is, AEMeasurable (f i) μ) :
                                  AEMeasurable (Finset.sum s fun (i : ι) => f i) μ
                                  abbrev Finset.aemeasurable_sum'.match_1 {M : Type u_2} {ι : Type u_1} {α : Type u_3} {f : ιαM} (s : Finset ι) (_g : αM) (motive : (∃ a ∈ s.val, f a = _g)Prop) :
                                  ∀ (x : ∃ a ∈ s.val, f a = _g), (∀ (_i : ι) (hi : _i s.val) (hg : f _i = _g), motive )motive x
                                  Equations
                                  • =
                                  Instances For
                                    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 (Finset.prod s fun (i : ι) => f i) μ
                                    theorem Finset.aemeasurable_sum {M : Type u_2} {ι : Type u_3} {α : Type u_4} [AddCommMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ιαM} (s : Finset ι) (hf : is, AEMeasurable (f i) μ) :
                                    AEMeasurable (fun (a : α) => Finset.sum s fun (i : ι) => f i a) μ
                                    theorem Finset.aemeasurable_prod {M : Type u_2} {ι : Type u_3} {α : Type u_4} [CommMonoid M] [MeasurableSpace M] [MeasurableMul₂ M] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ιαM} (s : Finset ι) (hf : is, AEMeasurable (f i) μ) :
                                    AEMeasurable (fun (a : α) => Finset.prod s fun (i : ι) => f i a) μ