Documentation

Mathlib.MeasureTheory.Integral.Bochner

Bochner integral #

The Bochner integral extends the definition of the Lebesgue integral to functions that map from a measure space into a Banach space (complete normed vector space). It is constructed here by extending the integral on simple functions.

Main definitions #

The Bochner integral is defined through the extension process described in the file SetToL1, which follows these steps:

  1. Define the integral of the indicator of a set. This is weightedSMul μ s x = (μ s).toReal * x. weightedSMul μ is shown to be linear in the value x and DominatedFinMeasAdditive (defined in the file SetToL1) with respect to the set s.

  2. Define the integral on simple functions of the type SimpleFunc α E (notation : α →ₛ E) where E is a real normed space. (See SimpleFunc.integral for details.)

  3. Transfer this definition to define the integral on L1.simpleFunc α E (notation : α →₁ₛ[μ] E), see L1.simpleFunc.integral. Show that this integral is a continuous linear map from α →₁ₛ[μ] E to E.

  4. Define the Bochner integral on L1 functions by extending the integral on integrable simple functions α →₁ₛ[μ] E using ContinuousLinearMap.extend and the fact that the embedding of α →₁ₛ[μ] E into α →₁[μ] E is dense.

  5. Define the Bochner integral on functions as the Bochner integral of its equivalence class in L1 space, if it is in L1, and 0 otherwise.

The result of that construction is ∫ a, f a ∂μ, which is definitionally equal to setToFun (dominatedFinMeasAdditive_weightedSMul μ) f. Some basic properties of the integral (like linearity) are particular cases of the properties of setToFun (which are described in the file SetToL1).

Main statements #

  1. Basic properties of the Bochner integral on functions of type α → E, where α is a measure space and E is a real normed space.
  1. Basic properties of the Bochner integral on functions of type α → ℝ, where α is a measure space.
  1. Propositions connecting the Bochner integral with the integral on ℝ≥0∞-valued functions, which is called lintegral and has the notation ∫⁻.
  1. (In the file DominatedConvergence) tendsto_integral_of_dominated_convergence : the Lebesgue dominated convergence theorem

  2. (In the file SetIntegral) integration commutes with continuous linear maps.

Notes #

Some tips on how to prove a proposition if the API for the Bochner integral is not enough so that you need to unfold the definition of the Bochner integral and go back to simple functions.

One method is to use the theorem Integrable.induction in the file SimpleFuncDenseLp (or one of the related results, like Lp.induction for functions in Lp), which allows you to prove something for an arbitrary integrable function.

Another method is using the following steps. See integral_eq_lintegral_pos_part_sub_lintegral_neg_part for a complicated example, which proves that ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻, with the first integral sign being the Bochner integral of a real-valued function f : α → ℝ, and second and third integral sign being the integral on ℝ≥0∞-valued functions (called lintegral). The proof of integral_eq_lintegral_pos_part_sub_lintegral_neg_part is scattered in sections with the name posPart.

Here are the usual steps of proving that a property p, say ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻, holds for all functions :

  1. First go to the space.

    For example, if you see ENNReal.toReal (∫⁻ a, ENNReal.ofReal <| ‖f a‖), that is the norm of f in space. Rewrite using L1.norm_of_fun_eq_lintegral_norm.

  2. Show that the set {f ∈ L¹ | ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻} is closed in using isClosed_eq.

  3. Show that the property holds for all simple functions s in space.

    Typically, you need to convert various notions to their SimpleFunc counterpart, using lemmas like L1.integral_coe_eq_integral.

  4. Since simple functions are dense in ,

univ = closure {s simple}
     = closure {s simple | ∫ s = ∫⁻ s⁺ - ∫⁻ s⁻} : the property holds for all simple functions
     ⊆ closure {f | ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻}
     = {f | ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻} : closure of a closed set is itself

Use isClosed_property or DenseRange.induction_on for this argument.

Notations #

We also define notations for integral on a set, which are described in the file MeasureTheory/SetIntegral.

Note : is typed using \_s. Sometimes it shows as a box if the font is missing.

Tags #

Bochner integral, simple function, function space, Lebesgue dominated convergence theorem

Given a set s, return the continuous linear map fun x => (μ s).toReal • x. The extension of that set function through setToL1 gives the Bochner integral of L1 functions.

Equations
Instances For
    theorem MeasureTheory.weightedSMul_apply {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α) (x : F) :
    (MeasureTheory.weightedSMul μ s) x = (μ s).toReal x
    theorem MeasureTheory.weightedSMul_congr {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (t : Set α) (hst : μ s = μ t) :
    theorem MeasureTheory.weightedSMul_null {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (h_zero : μ s = 0) :
    theorem MeasureTheory.weightedSMul_union' {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (t : Set α) (ht : MeasurableSet t) (hs_finite : μ s ) (ht_finite : μ t ) (h_inter : s t = ) :
    theorem MeasureTheory.weightedSMul_union {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (t : Set α) (_hs : MeasurableSet s) (ht : MeasurableSet t) (hs_finite : μ s ) (ht_finite : μ t ) (h_inter : s t = ) :
    theorem MeasureTheory.weightedSMul_smul {α : Type u_1} {F : Type u_3} {𝕜 : Type u_4} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass 𝕜 F] (c : 𝕜) (s : Set α) (x : F) :
    theorem MeasureTheory.weightedSMul_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (x : ) (hx : 0 x) :

    Positive part of a simple function.

    Equations
    Instances For

      Negative part of a simple function.

      Equations
      • f.negPart = (-f).posPart
      Instances For

        The Bochner integral of simple functions #

        Define the Bochner integral of simple functions of the type α →ₛ β where β is a normed group, and prove basic property of this integral.

        Bochner integral of simple functions whose codomain is a real NormedSpace. This is equal to ∑ x ∈ f.range, (μ (f ⁻¹' {x})).toReal • x (see integral_eq).

        Equations
        Instances For
          theorem MeasureTheory.SimpleFunc.integral_eq {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : MeasureTheory.SimpleFunc α F) :
          MeasureTheory.SimpleFunc.integral μ f = xf.range, (μ (f ⁻¹' {x})).toReal x
          theorem MeasureTheory.SimpleFunc.integral_eq_sum_filter {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] [DecidablePred fun (x : F) => x 0] {m : MeasurableSpace α} (f : MeasureTheory.SimpleFunc α F) (μ : MeasureTheory.Measure α) :
          MeasureTheory.SimpleFunc.integral μ f = xFinset.filter (fun (x : F) => x 0) f.range, (μ (f ⁻¹' {x})).toReal x
          theorem MeasureTheory.SimpleFunc.integral_eq_sum_of_subset {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [DecidablePred fun (x : F) => x 0] {f : MeasureTheory.SimpleFunc α F} {s : Finset F} (hs : Finset.filter (fun (x : F) => x 0) f.range s) :
          MeasureTheory.SimpleFunc.integral μ f = xs, (μ (f ⁻¹' {x})).toReal x

          The Bochner integral is equal to a sum over any set that includes f.range (except 0).

          theorem MeasureTheory.SimpleFunc.map_integral {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α E) (g : EF) (hf : MeasureTheory.Integrable (⇑f) μ) (hg : g 0 = 0) :
          MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.map g f) = xf.range, (μ (f ⁻¹' {x})).toReal g x

          Calculate the integral of g ∘ f : α →ₛ F, where f is an integrable function from α to E and g is a function from E to F. We require g 0 = 0 so that g ∘ f is integrable.

          theorem MeasureTheory.SimpleFunc.integral_eq_lintegral' {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α E} {g : EENNReal} (hf : MeasureTheory.Integrable (⇑f) μ) (hg0 : g 0 = 0) (ht : ∀ (b : E), g b ) :
          MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.map (ENNReal.toReal g) f) = (∫⁻ (a : α), g (f a)μ).toReal

          SimpleFunc.integral and SimpleFunc.lintegral agree when the integrand has type α →ₛ ℝ≥0∞. But since ℝ≥0∞ is not a NormedSpace, we need some form of coercion. See integral_eq_lintegral for a simpler version.

          theorem MeasureTheory.SimpleFunc.integral_eq_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α } (hf : MeasureTheory.Integrable (⇑f) μ) (h_pos : 0 ≤ᵐ[μ] f) :
          MeasureTheory.SimpleFunc.integral μ f = (∫⁻ (a : α), ENNReal.ofReal (f a)μ).toReal

          SimpleFunc.bintegral and SimpleFunc.integral agree when the integrand has type α →ₛ ℝ≥0∞. But since ℝ≥0∞ is not a NormedSpace, we need some form of coercion.

          Positive part of a simple function in L1 space.

          Equations
          Instances For

            Negative part of a simple function in L1 space.

            Equations
            Instances For

              The Bochner integral of L1 #

              Define the Bochner integral on α →₁ₛ[μ] E by extension from the simple functions α →₁ₛ[μ] E, and prove basic properties of this integral.

              The Bochner integral over simple functions in L1 space.

              Equations
              Instances For

                The Bochner integral over simple functions in L1 space as a continuous linear map.

                Equations
                Instances For

                  The Bochner integral over simple functions in L1 space as a continuous linear map over ℝ.

                  Equations
                  Instances For

                    The Bochner integral in L1 space as a continuous linear map.

                    Equations
                    Instances For

                      The Bochner integral in L1 space as a continuous linear map over ℝ.

                      Equations
                      Instances For
                        @[irreducible]

                        The Bochner integral in L1 space

                        Equations
                        Instances For
                          theorem MeasureTheory.L1.integral_def {α : Type u_5} {E : Type u_6} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedSpace E] [CompleteSpace E] :
                          MeasureTheory.L1.integral = MeasureTheory.L1.integralCLM
                          theorem MeasureTheory.L1.integral_eq {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedSpace E] [CompleteSpace E] (f : (MeasureTheory.Lp E 1 μ)) :
                          MeasureTheory.L1.integral f = MeasureTheory.L1.integralCLM f
                          theorem MeasureTheory.L1.norm_Integral_le_one {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedSpace E] [CompleteSpace E] :
                          MeasureTheory.L1.integralCLM 1
                          theorem MeasureTheory.L1.nnnorm_Integral_le_one {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedSpace E] [CompleteSpace E] :
                          MeasureTheory.L1.integralCLM‖₊ 1

                          The Bochner integral on functions #

                          Define the Bochner integral on functions generally to be the L1 Bochner integral, for integrable functions, and 0 otherwise; prove its basic properties.

                          theorem MeasureTheory.integral_def {α : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace G] :
                          ∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : αG), MeasureTheory.integral μ f = if x_1 : CompleteSpace G then if hf : MeasureTheory.Integrable f μ then MeasureTheory.L1.integral (MeasureTheory.Integrable.toL1 f hf) else 0 else 0
                          @[irreducible]
                          def MeasureTheory.integral {α : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace G] :
                          {x : MeasurableSpace α} → MeasureTheory.Measure α(αG)G

                          The Bochner integral

                          Equations
                          Instances For

                            In the notation for integrals, an expression like ∫ x, g ‖x‖ ∂μ will not be parsed correctly, and needs parentheses. We do not set the binding power of r to 0, because then ∫ x, f x = 0 will be parsed incorrectly.

                            Pretty printer defined by notation3 command.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

                              The Bochner integral

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For

                                The Bochner integral

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  Pretty printer defined by notation3 command.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    Pretty printer defined by notation3 command.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For

                                      The Bochner integral

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

                                        The Bochner integral

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For

                                          Pretty printer defined by notation3 command.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            theorem MeasureTheory.integral_eq {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [hE : CompleteSpace E] [NormedSpace E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : αE) (hf : MeasureTheory.Integrable f μ) :
                                            theorem MeasureTheory.integral_eq_setToFun {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [hE : CompleteSpace E] [NormedSpace E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : αE) :
                                            ∫ (a : α), f aμ = MeasureTheory.setToFun μ (MeasureTheory.weightedSMul μ) f
                                            theorem MeasureTheory.L1.integral_eq_integral {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [hE : CompleteSpace E] [NormedSpace E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : (MeasureTheory.Lp E 1 μ)) :
                                            MeasureTheory.L1.integral f = ∫ (a : α), f aμ
                                            theorem MeasureTheory.integral_undef {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αG} (h : ¬MeasureTheory.Integrable f μ) :
                                            ∫ (a : α), f aμ = 0
                                            theorem MeasureTheory.Integrable.of_integral_ne_zero {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αG} (h : ∫ (a : α), f aμ 0) :
                                            theorem MeasureTheory.integral_non_aestronglyMeasurable {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αG} (h : ¬MeasureTheory.AEStronglyMeasurable f μ) :
                                            ∫ (a : α), f aμ = 0
                                            @[simp]
                                            theorem MeasureTheory.integral_zero (α : Type u_1) (G : Type u_5) [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} :
                                            ∫ (x : α), 0μ = 0
                                            theorem MeasureTheory.integrable_of_integral_eq_one {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (h : ∫ (x : α), f xμ = 1) :
                                            theorem MeasureTheory.integral_add {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αG} {g : αG} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) :
                                            ∫ (a : α), f a + g aμ = ∫ (a : α), f aμ + ∫ (a : α), g aμ
                                            theorem MeasureTheory.integral_add' {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αG} {g : αG} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) :
                                            ∫ (a : α), (f + g) aμ = ∫ (a : α), f aμ + ∫ (a : α), g aμ
                                            theorem MeasureTheory.integral_finset_sum {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_6} (s : Finset ι) {f : ιαG} (hf : is, MeasureTheory.Integrable (f i) μ) :
                                            ∫ (a : α), is, f i aμ = is, ∫ (a : α), f i aμ
                                            theorem MeasureTheory.integral_neg {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : αG) :
                                            ∫ (a : α), -f aμ = -∫ (a : α), f aμ
                                            theorem MeasureTheory.integral_neg' {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : αG) :
                                            ∫ (a : α), (-f) aμ = -∫ (a : α), f aμ
                                            theorem MeasureTheory.integral_sub {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αG} {g : αG} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) :
                                            ∫ (a : α), f a - g aμ = ∫ (a : α), f aμ - ∫ (a : α), g aμ
                                            theorem MeasureTheory.integral_sub' {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αG} {g : αG} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) :
                                            ∫ (a : α), (f - g) aμ = ∫ (a : α), f aμ - ∫ (a : α), g aμ
                                            theorem MeasureTheory.integral_smul {α : Type u_1} {𝕜 : Type u_4} [NontriviallyNormedField 𝕜] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedSpace 𝕜 G] [SMulCommClass 𝕜 G] (c : 𝕜) (f : αG) :
                                            ∫ (a : α), c f aμ = c ∫ (a : α), f aμ
                                            theorem MeasureTheory.integral_mul_left {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {L : Type u_6} [RCLike L] (r : L) (f : αL) :
                                            ∫ (a : α), r * f aμ = r * ∫ (a : α), f aμ
                                            theorem MeasureTheory.integral_mul_right {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {L : Type u_6} [RCLike L] (r : L) (f : αL) :
                                            ∫ (a : α), f a * rμ = (∫ (a : α), f aμ) * r
                                            theorem MeasureTheory.integral_div {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {L : Type u_6} [RCLike L] (r : L) (f : αL) :
                                            ∫ (a : α), f a / rμ = (∫ (a : α), f aμ) / r
                                            theorem MeasureTheory.integral_congr_ae {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αG} {g : αG} (h : f =ᵐ[μ] g) :
                                            ∫ (a : α), f aμ = ∫ (a : α), g aμ
                                            theorem MeasureTheory.integral_congr_ae₂ {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_6} :
                                            ∀ {x : MeasurableSpace β} {ν : MeasureTheory.Measure β} {f g : αβG}, (∀ᵐ (a : α) ∂μ, f a =ᵐ[ν] g a)∫ (a : α), ∫ (b : β), f a bνμ = ∫ (a : α), ∫ (b : β), g a bνμ
                                            @[simp]
                                            theorem MeasureTheory.L1.integral_of_fun_eq_integral {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αG} (hf : MeasureTheory.Integrable f μ) :
                                            ∫ (a : α), (MeasureTheory.Integrable.toL1 f hf) aμ = ∫ (a : α), f aμ
                                            theorem MeasureTheory.continuous_integral {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} :
                                            Continuous fun (f : (MeasureTheory.Lp G 1 μ)) => ∫ (a : α), f aμ
                                            theorem MeasureTheory.norm_integral_le_lintegral_norm {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : αG) :
                                            ∫ (a : α), f aμ (∫⁻ (a : α), ENNReal.ofReal f aμ).toReal
                                            theorem MeasureTheory.ennnorm_integral_le_lintegral_ennnorm {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : αG) :
                                            ∫ (a : α), f aμ‖₊ ∫⁻ (a : α), f a‖₊μ
                                            theorem MeasureTheory.integral_eq_zero_of_ae {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αG} (hf : f =ᵐ[μ] 0) :
                                            ∫ (a : α), f aμ = 0
                                            theorem MeasureTheory.HasFiniteIntegral.tendsto_setIntegral_nhds_zero {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_6} {f : αG} (hf : MeasureTheory.HasFiniteIntegral f μ) {l : Filter ι} {s : ιSet α} (hs : Filter.Tendsto (μ s) l (nhds 0)) :
                                            Filter.Tendsto (fun (i : ι) => ∫ (x : α) in s i, f xμ) l (nhds 0)

                                            If f has finite integral, then ∫ x in s, f x ∂μ is absolutely continuous in s: it tends to zero as μ s tends to zero.

                                            @[deprecated MeasureTheory.HasFiniteIntegral.tendsto_setIntegral_nhds_zero]
                                            theorem MeasureTheory.HasFiniteIntegral.tendsto_set_integral_nhds_zero {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_6} {f : αG} (hf : MeasureTheory.HasFiniteIntegral f μ) {l : Filter ι} {s : ιSet α} (hs : Filter.Tendsto (μ s) l (nhds 0)) :
                                            Filter.Tendsto (fun (i : ι) => ∫ (x : α) in s i, f xμ) l (nhds 0)

                                            Alias of MeasureTheory.HasFiniteIntegral.tendsto_setIntegral_nhds_zero.


                                            If f has finite integral, then ∫ x in s, f x ∂μ is absolutely continuous in s: it tends to zero as μ s tends to zero.

                                            theorem MeasureTheory.Integrable.tendsto_setIntegral_nhds_zero {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_6} {f : αG} (hf : MeasureTheory.Integrable f μ) {l : Filter ι} {s : ιSet α} (hs : Filter.Tendsto (μ s) l (nhds 0)) :
                                            Filter.Tendsto (fun (i : ι) => ∫ (x : α) in s i, f xμ) l (nhds 0)

                                            If f is integrable, then ∫ x in s, f x ∂μ is absolutely continuous in s: it tends to zero as μ s tends to zero.

                                            @[deprecated MeasureTheory.Integrable.tendsto_setIntegral_nhds_zero]
                                            theorem MeasureTheory.Integrable.tendsto_set_integral_nhds_zero {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_6} {f : αG} (hf : MeasureTheory.Integrable f μ) {l : Filter ι} {s : ιSet α} (hs : Filter.Tendsto (μ s) l (nhds 0)) :
                                            Filter.Tendsto (fun (i : ι) => ∫ (x : α) in s i, f xμ) l (nhds 0)

                                            Alias of MeasureTheory.Integrable.tendsto_setIntegral_nhds_zero.


                                            If f is integrable, then ∫ x in s, f x ∂μ is absolutely continuous in s: it tends to zero as μ s tends to zero.

                                            theorem MeasureTheory.tendsto_integral_of_L1 {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_6} (f : αG) (hfi : MeasureTheory.Integrable f μ) {F : ιαG} {l : Filter ι} (hFi : ∀ᶠ (i : ι) in l, MeasureTheory.Integrable (F i) μ) (hF : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : α), F i x - f x‖₊μ) l (nhds 0)) :
                                            Filter.Tendsto (fun (i : ι) => ∫ (x : α), F i xμ) l (nhds (∫ (x : α), f xμ))

                                            If F i → f in L1, then ∫ x, F i x ∂μ → ∫ x, f x ∂μ.

                                            theorem MeasureTheory.tendsto_integral_of_L1' {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_6} (f : αG) (hfi : MeasureTheory.Integrable f μ) {F : ιαG} {l : Filter ι} (hFi : ∀ᶠ (i : ι) in l, MeasureTheory.Integrable (F i) μ) (hF : Filter.Tendsto (fun (i : ι) => MeasureTheory.eLpNorm (F i - f) 1 μ) l (nhds 0)) :
                                            Filter.Tendsto (fun (i : ι) => ∫ (x : α), F i xμ) l (nhds (∫ (x : α), f xμ))

                                            If F i → f in L1, then ∫ x, F i x ∂μ → ∫ x, f x ∂μ.

                                            theorem MeasureTheory.tendsto_setIntegral_of_L1 {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_6} (f : αG) (hfi : MeasureTheory.Integrable f μ) {F : ιαG} {l : Filter ι} (hFi : ∀ᶠ (i : ι) in l, MeasureTheory.Integrable (F i) μ) (hF : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : α), F i x - f x‖₊μ) l (nhds 0)) (s : Set α) :
                                            Filter.Tendsto (fun (i : ι) => ∫ (x : α) in s, F i xμ) l (nhds (∫ (x : α) in s, f xμ))

                                            If F i → f in L1, then ∫ x in s, F i x ∂μ → ∫ x in s, f x ∂μ.

                                            @[deprecated MeasureTheory.tendsto_setIntegral_of_L1]
                                            theorem MeasureTheory.tendsto_set_integral_of_L1 {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_6} (f : αG) (hfi : MeasureTheory.Integrable f μ) {F : ιαG} {l : Filter ι} (hFi : ∀ᶠ (i : ι) in l, MeasureTheory.Integrable (F i) μ) (hF : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : α), F i x - f x‖₊μ) l (nhds 0)) (s : Set α) :
                                            Filter.Tendsto (fun (i : ι) => ∫ (x : α) in s, F i xμ) l (nhds (∫ (x : α) in s, f xμ))

                                            Alias of MeasureTheory.tendsto_setIntegral_of_L1.


                                            If F i → f in L1, then ∫ x in s, F i x ∂μ → ∫ x in s, f x ∂μ.

                                            theorem MeasureTheory.tendsto_setIntegral_of_L1' {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_6} (f : αG) (hfi : MeasureTheory.Integrable f μ) {F : ιαG} {l : Filter ι} (hFi : ∀ᶠ (i : ι) in l, MeasureTheory.Integrable (F i) μ) (hF : Filter.Tendsto (fun (i : ι) => MeasureTheory.eLpNorm (F i - f) 1 μ) l (nhds 0)) (s : Set α) :
                                            Filter.Tendsto (fun (i : ι) => ∫ (x : α) in s, F i xμ) l (nhds (∫ (x : α) in s, f xμ))

                                            If F i → f in L1, then ∫ x in s, F i x ∂μ → ∫ x in s, f x ∂μ.

                                            @[deprecated MeasureTheory.tendsto_setIntegral_of_L1']
                                            theorem MeasureTheory.tendsto_set_integral_of_L1' {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_6} (f : αG) (hfi : MeasureTheory.Integrable f μ) {F : ιαG} {l : Filter ι} (hFi : ∀ᶠ (i : ι) in l, MeasureTheory.Integrable (F i) μ) (hF : Filter.Tendsto (fun (i : ι) => MeasureTheory.eLpNorm (F i - f) 1 μ) l (nhds 0)) (s : Set α) :
                                            Filter.Tendsto (fun (i : ι) => ∫ (x : α) in s, F i xμ) l (nhds (∫ (x : α) in s, f xμ))

                                            Alias of MeasureTheory.tendsto_setIntegral_of_L1'.


                                            If F i → f in L1, then ∫ x in s, F i x ∂μ → ∫ x in s, f x ∂μ.

                                            theorem MeasureTheory.continuousWithinAt_of_dominated {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {X : Type u_6} [TopologicalSpace X] [FirstCountableTopology X] {F : XαG} {x₀ : X} {bound : α} {s : Set X} (hF_meas : ∀ᶠ (x : X) in nhdsWithin x₀ s, MeasureTheory.AEStronglyMeasurable (F x) μ) (h_bound : ∀ᶠ (x : X) in nhdsWithin x₀ s, ∀ᵐ (a : α) ∂μ, F x a bound a) (bound_integrable : MeasureTheory.Integrable bound μ) (h_cont : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun (x : X) => F x a) s x₀) :
                                            ContinuousWithinAt (fun (x : X) => ∫ (a : α), F x aμ) s x₀
                                            theorem MeasureTheory.continuousAt_of_dominated {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {X : Type u_6} [TopologicalSpace X] [FirstCountableTopology X] {F : XαG} {x₀ : X} {bound : α} (hF_meas : ∀ᶠ (x : X) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) μ) (h_bound : ∀ᶠ (x : X) in nhds x₀, ∀ᵐ (a : α) ∂μ, F x a bound a) (bound_integrable : MeasureTheory.Integrable bound μ) (h_cont : ∀ᵐ (a : α) ∂μ, ContinuousAt (fun (x : X) => F x a) x₀) :
                                            ContinuousAt (fun (x : X) => ∫ (a : α), F x aμ) x₀
                                            theorem MeasureTheory.continuousOn_of_dominated {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {X : Type u_6} [TopologicalSpace X] [FirstCountableTopology X] {F : XαG} {bound : α} {s : Set X} (hF_meas : xs, MeasureTheory.AEStronglyMeasurable (F x) μ) (h_bound : xs, ∀ᵐ (a : α) ∂μ, F x a bound a) (bound_integrable : MeasureTheory.Integrable bound μ) (h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun (x : X) => F x a) s) :
                                            ContinuousOn (fun (x : X) => ∫ (a : α), F x aμ) s
                                            theorem MeasureTheory.continuous_of_dominated {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {X : Type u_6} [TopologicalSpace X] [FirstCountableTopology X] {F : XαG} {bound : α} (hF_meas : ∀ (x : X), MeasureTheory.AEStronglyMeasurable (F x) μ) (h_bound : ∀ (x : X), ∀ᵐ (a : α) ∂μ, F x a bound a) (bound_integrable : MeasureTheory.Integrable bound μ) (h_cont : ∀ᵐ (a : α) ∂μ, Continuous fun (x : X) => F x a) :
                                            Continuous fun (x : X) => ∫ (a : α), F x aμ
                                            theorem MeasureTheory.integral_eq_lintegral_pos_part_sub_lintegral_neg_part {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (hf : MeasureTheory.Integrable f μ) :
                                            ∫ (a : α), f aμ = (∫⁻ (a : α), ENNReal.ofReal (f a)μ).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a)μ).toReal

                                            The Bochner integral of a real-valued function f : α → ℝ is the difference between the integral of the positive part of f and the integral of the negative part of f.

                                            theorem MeasureTheory.integral_eq_lintegral_of_nonneg_ae {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (hf : 0 ≤ᵐ[μ] f) (hfm : MeasureTheory.AEStronglyMeasurable f μ) :
                                            ∫ (a : α), f aμ = (∫⁻ (a : α), ENNReal.ofReal (f a)μ).toReal
                                            theorem MeasureTheory.integral_norm_eq_lintegral_nnnorm {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {P : Type u_7} [NormedAddCommGroup P] {f : αP} (hf : MeasureTheory.AEStronglyMeasurable f μ) :
                                            ∫ (x : α), f xμ = (∫⁻ (x : α), f x‖₊μ).toReal
                                            theorem MeasureTheory.ofReal_integral_norm_eq_lintegral_nnnorm {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {P : Type u_7} [NormedAddCommGroup P] {f : αP} (hf : MeasureTheory.Integrable f μ) :
                                            ENNReal.ofReal (∫ (x : α), f xμ) = ∫⁻ (x : α), f x‖₊μ
                                            theorem MeasureTheory.integral_eq_integral_pos_part_sub_integral_neg_part {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (hf : MeasureTheory.Integrable f μ) :
                                            ∫ (a : α), f aμ = ∫ (a : α), (f a).toNNRealμ - ∫ (a : α), (-f a).toNNRealμ
                                            theorem MeasureTheory.integral_nonneg_of_ae {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (hf : 0 ≤ᵐ[μ] f) :
                                            0 ∫ (a : α), f aμ
                                            theorem MeasureTheory.lintegral_coe_eq_integral {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : αNNReal) (hfi : MeasureTheory.Integrable (fun (x : α) => (f x)) μ) :
                                            ∫⁻ (a : α), (f a)μ = ENNReal.ofReal (∫ (a : α), (f a)μ)
                                            theorem MeasureTheory.ofReal_integral_eq_lintegral_ofReal {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (hfi : MeasureTheory.Integrable f μ) (f_nn : 0 ≤ᵐ[μ] f) :
                                            ENNReal.ofReal (∫ (x : α), f xμ) = ∫⁻ (x : α), ENNReal.ofReal (f x)μ
                                            theorem MeasureTheory.integral_toReal {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} (hfm : AEMeasurable f μ) (hf : ∀ᵐ (x : α) ∂μ, f x < ) :
                                            ∫ (a : α), (f a).toRealμ = (∫⁻ (a : α), f aμ).toReal
                                            theorem MeasureTheory.lintegral_coe_le_coe_iff_integral_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αNNReal} (hfi : MeasureTheory.Integrable (fun (x : α) => (f x)) μ) {b : NNReal} :
                                            ∫⁻ (a : α), (f a)μ b ∫ (a : α), (f a)μ b
                                            theorem MeasureTheory.integral_coe_le_of_lintegral_coe_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αNNReal} {b : NNReal} (h : ∫⁻ (a : α), (f a)μ b) :
                                            ∫ (a : α), (f a)μ b
                                            theorem MeasureTheory.integral_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (hf : 0 f) :
                                            0 ∫ (a : α), f aμ
                                            theorem MeasureTheory.integral_nonpos_of_ae {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (hf : f ≤ᵐ[μ] 0) :
                                            ∫ (a : α), f aμ 0
                                            theorem MeasureTheory.integral_nonpos {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (hf : f 0) :
                                            ∫ (a : α), f aμ 0
                                            theorem MeasureTheory.integral_eq_zero_iff_of_nonneg_ae {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (hf : 0 ≤ᵐ[μ] f) (hfi : MeasureTheory.Integrable f μ) :
                                            ∫ (x : α), f xμ = 0 f =ᵐ[μ] 0
                                            theorem MeasureTheory.integral_eq_zero_iff_of_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (hf : 0 f) (hfi : MeasureTheory.Integrable f μ) :
                                            ∫ (x : α), f xμ = 0 f =ᵐ[μ] 0
                                            theorem MeasureTheory.integral_eq_iff_of_ae_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {g : α} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) (hfg : f ≤ᵐ[μ] g) :
                                            ∫ (a : α), f aμ = ∫ (a : α), g aμ f =ᵐ[μ] g
                                            theorem MeasureTheory.integral_pos_iff_support_of_nonneg_ae {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (hf : 0 ≤ᵐ[μ] f) (hfi : MeasureTheory.Integrable f μ) :
                                            0 < ∫ (x : α), f xμ 0 < μ (Function.support f)
                                            theorem MeasureTheory.integral_pos_iff_support_of_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (hf : 0 f) (hfi : MeasureTheory.Integrable f μ) :
                                            0 < ∫ (x : α), f xμ 0 < μ (Function.support f)
                                            theorem MeasureTheory.integral_exp_pos {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} [hμ : NeZero μ] (hf : MeasureTheory.Integrable (fun (x : α) => Real.exp (f x)) μ) :
                                            0 < ∫ (x : α), Real.exp (f x)μ
                                            theorem MeasureTheory.integral_tendsto_of_tendsto_of_monotone {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {F : α} (hf : ∀ (n : ), MeasureTheory.Integrable (f n) μ) (hF : MeasureTheory.Integrable F μ) (h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun (n : ) => f n x) (h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ) => f n x) Filter.atTop (nhds (F x))) :
                                            Filter.Tendsto (fun (n : ) => ∫ (x : α), f n xμ) Filter.atTop (nhds (∫ (x : α), F xμ))

                                            Monotone convergence theorem for real-valued functions and Bochner integrals

                                            theorem MeasureTheory.integral_tendsto_of_tendsto_of_antitone {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {F : α} (hf : ∀ (n : ), MeasureTheory.Integrable (f n) μ) (hF : MeasureTheory.Integrable F μ) (h_mono : ∀ᵐ (x : α) ∂μ, Antitone fun (n : ) => f n x) (h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ) => f n x) Filter.atTop (nhds (F x))) :
                                            Filter.Tendsto (fun (n : ) => ∫ (x : α), f n xμ) Filter.atTop (nhds (∫ (x : α), F xμ))

                                            Monotone convergence theorem for real-valued functions and Bochner integrals

                                            theorem MeasureTheory.tendsto_of_integral_tendsto_of_monotone {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {F : α} (hf_int : ∀ (n : ), MeasureTheory.Integrable (f n) μ) (hF_int : MeasureTheory.Integrable F μ) (hf_tendsto : Filter.Tendsto (fun (i : ) => ∫ (a : α), f i aμ) Filter.atTop (nhds (∫ (a : α), F aμ))) (hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun (i : ) => f i a) (hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ), f i a F a) :
                                            ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (i : ) => f i a) Filter.atTop (nhds (F a))

                                            If a monotone sequence of functions has an upper bound and the sequence of integrals of these functions tends to the integral of the upper bound, then the sequence of functions converges almost everywhere to the upper bound.

                                            theorem MeasureTheory.tendsto_of_integral_tendsto_of_antitone {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {F : α} (hf_int : ∀ (n : ), MeasureTheory.Integrable (f n) μ) (hF_int : MeasureTheory.Integrable F μ) (hf_tendsto : Filter.Tendsto (fun (i : ) => ∫ (a : α), f i aμ) Filter.atTop (nhds (∫ (a : α), F aμ))) (hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun (i : ) => f i a) (hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ), F a f i a) :
                                            ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (i : ) => f i a) Filter.atTop (nhds (F a))

                                            If an antitone sequence of functions has a lower bound and the sequence of integrals of these functions tends to the integral of the lower bound, then the sequence of functions converges almost everywhere to the lower bound.

                                            theorem MeasureTheory.L1.norm_eq_integral_norm {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {H : Type u_7} [NormedAddCommGroup H] (f : (MeasureTheory.Lp H 1 μ)) :
                                            f = ∫ (a : α), f aμ
                                            theorem MeasureTheory.L1.dist_eq_integral_dist {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {H : Type u_7} [NormedAddCommGroup H] (f : (MeasureTheory.Lp H 1 μ)) (g : (MeasureTheory.Lp H 1 μ)) :
                                            dist f g = ∫ (a : α), dist (f a) (g a)μ
                                            theorem MeasureTheory.Memℒp.eLpNorm_eq_integral_rpow_norm {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {H : Type u_7} [NormedAddCommGroup H] {f : αH} {p : ENNReal} (hp1 : p 0) (hp2 : p ) (hf : MeasureTheory.Memℒp f p μ) :
                                            MeasureTheory.eLpNorm f p μ = ENNReal.ofReal ((∫ (a : α), f a ^ p.toRealμ) ^ p.toReal⁻¹)
                                            @[deprecated MeasureTheory.Memℒp.eLpNorm_eq_integral_rpow_norm]
                                            theorem MeasureTheory.Memℒp.snorm_eq_integral_rpow_norm {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {H : Type u_7} [NormedAddCommGroup H] {f : αH} {p : ENNReal} (hp1 : p 0) (hp2 : p ) (hf : MeasureTheory.Memℒp f p μ) :
                                            MeasureTheory.eLpNorm f p μ = ENNReal.ofReal ((∫ (a : α), f a ^ p.toRealμ) ^ p.toReal⁻¹)

                                            Alias of MeasureTheory.Memℒp.eLpNorm_eq_integral_rpow_norm.

                                            theorem MeasureTheory.integral_mono_ae {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {g : α} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) (h : f ≤ᵐ[μ] g) :
                                            ∫ (a : α), f aμ ∫ (a : α), g aμ
                                            theorem MeasureTheory.integral_mono {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {g : α} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) (h : f g) :
                                            ∫ (a : α), f aμ ∫ (a : α), g aμ
                                            theorem MeasureTheory.integral_mono_of_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {g : α} (hf : 0 ≤ᵐ[μ] f) (hgi : MeasureTheory.Integrable g μ) (h : f ≤ᵐ[μ] g) :
                                            ∫ (a : α), f aμ ∫ (a : α), g aμ
                                            theorem MeasureTheory.integral_mono_measure {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {ν : MeasureTheory.Measure α} (hle : μ ν) (hf : 0 ≤ᵐ[ν] f) (hfi : MeasureTheory.Integrable f ν) :
                                            ∫ (a : α), f aμ ∫ (a : α), f aν
                                            theorem MeasureTheory.norm_integral_le_integral_norm {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : αG) :
                                            ∫ (a : α), f aμ ∫ (a : α), f aμ
                                            theorem MeasureTheory.norm_integral_le_of_norm_le {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αG} {g : α} (hg : MeasureTheory.Integrable g μ) (h : ∀ᵐ (x : α) ∂μ, f x g x) :
                                            ∫ (x : α), f xμ ∫ (x : α), g xμ
                                            theorem MeasureTheory.SimpleFunc.integral_eq_sum {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [hE : CompleteSpace E] [NormedSpace E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α E) (hfi : MeasureTheory.Integrable (⇑f) μ) :
                                            ∫ (x : α), f xμ = xf.range, (μ (f ⁻¹' {x})).toReal x
                                            @[simp]
                                            theorem MeasureTheory.integral_const {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [hE : CompleteSpace E] [NormedSpace E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (c : E) :
                                            ∫ (x : α), cμ = (μ Set.univ).toReal c
                                            theorem MeasureTheory.norm_integral_le_of_norm_le_const {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {f : αG} {C : } (h : ∀ᵐ (x : α) ∂μ, f x C) :
                                            ∫ (x : α), f xμ C * (μ Set.univ).toReal
                                            theorem MeasureTheory.tendsto_integral_approxOn_of_measurable {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [hE : CompleteSpace E] [NormedSpace E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSpace E] [BorelSpace E] {f : αE} {s : Set E} [TopologicalSpace.SeparableSpace s] (hfi : MeasureTheory.Integrable f μ) (hfm : Measurable f) (hs : ∀ᵐ (x : α) ∂μ, f x closure s) {y₀ : E} (h₀ : y₀ s) (h₀i : MeasureTheory.Integrable (fun (x : α) => y₀) μ) :
                                            Filter.Tendsto (fun (n : ) => MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.approxOn f hfm s y₀ h₀ n)) Filter.atTop (nhds (∫ (x : α), f xμ))
                                            theorem MeasureTheory.tendsto_integral_approxOn_of_measurable_of_range_subset {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [hE : CompleteSpace E] [NormedSpace E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSpace E] [BorelSpace E] {f : αE} (fmeas : Measurable f) (hf : MeasureTheory.Integrable f μ) (s : Set E) [TopologicalSpace.SeparableSpace s] (hs : Set.range f {0} s) :
                                            Filter.Tendsto (fun (n : ) => MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.approxOn f fmeas s 0 n)) Filter.atTop (nhds (∫ (x : α), f xμ))
                                            theorem MeasureTheory.tendsto_integral_norm_approxOn_sub {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_7} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] {f : αE} (fmeas : Measurable f) (hf : MeasureTheory.Integrable f μ) [TopologicalSpace.SeparableSpace (Set.range f {0})] :
                                            Filter.Tendsto (fun (n : ) => ∫ (x : α), (MeasureTheory.SimpleFunc.approxOn f fmeas (Set.range f {0}) 0 n) x - f xμ) Filter.atTop (nhds 0)
                                            theorem MeasureTheory.integral_add_measure {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : αG} (hμ : MeasureTheory.Integrable f μ) (hν : MeasureTheory.Integrable f ν) :
                                            ∫ (x : α), f x(μ + ν) = ∫ (x : α), f xμ + ∫ (x : α), f xν
                                            @[simp]
                                            theorem MeasureTheory.integral_zero_measure {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} (f : αG) :
                                            ∫ (x : α), f x0 = 0
                                            @[simp]
                                            theorem MeasureTheory.setIntegral_zero_measure {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} (f : αG) {μ : MeasureTheory.Measure α} {s : Set α} (hs : μ s = 0) :
                                            ∫ (x : α) in s, f xμ = 0
                                            theorem MeasureTheory.integral_of_isEmpty {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [IsEmpty α] {f : αG} :
                                            ∫ (x : α), f xμ = 0
                                            theorem MeasureTheory.integral_finset_sum_measure {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {ι : Type u_7} {m : MeasurableSpace α} {f : αG} {μ : ιMeasureTheory.Measure α} {s : Finset ι} (hf : is, MeasureTheory.Integrable f (μ i)) :
                                            ∫ (a : α), f ais, μ i = is, ∫ (a : α), f aμ i
                                            theorem MeasureTheory.nndist_integral_add_measure_le_lintegral {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : αG} (h₁ : MeasureTheory.Integrable f μ) (h₂ : MeasureTheory.Integrable f ν) :
                                            (nndist (∫ (x : α), f xμ) (∫ (x : α), f x(μ + ν))) ∫⁻ (x : α), f x‖₊ν
                                            theorem MeasureTheory.hasSum_integral_measure {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {ι : Type u_7} {m : MeasurableSpace α} {f : αG} {μ : ιMeasureTheory.Measure α} (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.sum μ)) :
                                            HasSum (fun (i : ι) => ∫ (a : α), f aμ i) (∫ (a : α), f aMeasureTheory.Measure.sum μ)
                                            theorem MeasureTheory.integral_sum_measure {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {ι : Type u_7} :
                                            ∀ {x : MeasurableSpace α} {f : αG} {μ : ιMeasureTheory.Measure α}, MeasureTheory.Integrable f (MeasureTheory.Measure.sum μ)∫ (a : α), f aMeasureTheory.Measure.sum μ = ∑' (i : ι), ∫ (a : α), f aμ i
                                            @[simp]
                                            theorem MeasureTheory.integral_smul_measure {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : αG) (c : ENNReal) :
                                            ∫ (x : α), f xc μ = c.toReal ∫ (x : α), f xμ
                                            @[simp]
                                            theorem MeasureTheory.integral_smul_nnreal_measure {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : αG) (c : NNReal) :
                                            ∫ (x : α), f xc μ = c ∫ (x : α), f xμ
                                            theorem MeasureTheory.integral_map_of_stronglyMeasurable {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [MeasurableSpace β] {φ : αβ} (hφ : Measurable φ) {f : βG} (hfm : MeasureTheory.StronglyMeasurable f) :
                                            ∫ (y : β), f yMeasureTheory.Measure.map φ μ = ∫ (x : α), f (φ x)μ
                                            theorem MeasureTheory.integral_map {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [MeasurableSpace β] {φ : αβ} (hφ : AEMeasurable φ μ) {f : βG} (hfm : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map φ μ)) :
                                            ∫ (y : β), f yMeasureTheory.Measure.map φ μ = ∫ (x : α), f (φ x)μ
                                            theorem MeasurableEmbedding.integral_map {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} :
                                            ∀ {x : MeasurableSpace β} {f : αβ}, MeasurableEmbedding f∀ (g : βG), ∫ (y : β), g yMeasureTheory.Measure.map f μ = ∫ (x : α), g (f x)μ
                                            theorem ClosedEmbedding.integral_map {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [TopologicalSpace α] [BorelSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] {φ : αβ} (hφ : ClosedEmbedding φ) (f : βG) :
                                            ∫ (y : β), f yMeasureTheory.Measure.map φ μ = ∫ (x : α), f (φ x)μ
                                            theorem MeasureTheory.integral_map_equiv {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [MeasurableSpace β] (e : α ≃ᵐ β) (f : βG) :
                                            ∫ (y : β), f yMeasureTheory.Measure.map (⇑e) μ = ∫ (x : α), f (e x)μ
                                            theorem MeasureTheory.MeasurePreserving.integral_comp {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} :
                                            ∀ {x : MeasurableSpace β} {f : αβ} {ν : MeasureTheory.Measure β}, MeasureTheory.MeasurePreserving f μ νMeasurableEmbedding f∀ (g : βG), ∫ (x : α), g (f x)μ = ∫ (y : β), g yν
                                            theorem MeasureTheory.MeasurePreserving.integral_comp' {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [MeasurableSpace β] {ν : MeasureTheory.Measure β} {f : α ≃ᵐ β} (h : MeasureTheory.MeasurePreserving (⇑f) μ ν) (g : βG) :
                                            ∫ (x : α), g (f x)μ = ∫ (y : β), g yν
                                            theorem MeasureTheory.integral_subtype_comap {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {α : Type u_7} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) (f : αG) :
                                            ∫ (x : s), f xMeasureTheory.Measure.comap Subtype.val μ = ∫ (x : α) in s, f xμ
                                            theorem MeasureTheory.integral_subtype {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {α : Type u_7} [MeasureTheory.MeasureSpace α] {s : Set α} (hs : MeasurableSet s) (f : αG) :
                                            ∫ (x : s), f x = ∫ (x : α) in s, f x
                                            @[simp]
                                            theorem MeasureTheory.integral_dirac' {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [hE : CompleteSpace E] [NormedSpace E] [MeasurableSpace α] (f : αE) (a : α) (hfm : MeasureTheory.StronglyMeasurable f) :
                                            ∫ (x : α), f xMeasureTheory.Measure.dirac a = f a
                                            @[simp]
                                            theorem MeasureTheory.integral_dirac {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [hE : CompleteSpace E] [NormedSpace E] [MeasurableSpace α] [MeasurableSingletonClass α] (f : αE) (a : α) :
                                            ∫ (x : α), f xMeasureTheory.Measure.dirac a = f a
                                            theorem MeasureTheory.setIntegral_dirac' {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [hE : CompleteSpace E] [NormedSpace E] {mα : MeasurableSpace α} {f : αE} (hf : MeasureTheory.StronglyMeasurable f) (a : α) {s : Set α} (hs : MeasurableSet s) [Decidable (a s)] :
                                            ∫ (x : α) in s, f xMeasureTheory.Measure.dirac a = if a s then f a else 0
                                            @[deprecated MeasureTheory.setIntegral_dirac']
                                            theorem MeasureTheory.set_integral_dirac' {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [hE : CompleteSpace E] [NormedSpace E] {mα : MeasurableSpace α} {f : αE} (hf : MeasureTheory.StronglyMeasurable f) (a : α) {s : Set α} (hs : MeasurableSet s) [Decidable (a s)] :
                                            ∫ (x : α) in s, f xMeasureTheory.Measure.dirac a = if a s then f a else 0

                                            Alias of MeasureTheory.setIntegral_dirac'.

                                            theorem MeasureTheory.setIntegral_dirac {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [hE : CompleteSpace E] [NormedSpace E] [MeasurableSpace α] [MeasurableSingletonClass α] (f : αE) (a : α) (s : Set α) [Decidable (a s)] :
                                            ∫ (x : α) in s, f xMeasureTheory.Measure.dirac a = if a s then f a else 0
                                            @[deprecated MeasureTheory.setIntegral_dirac]
                                            theorem MeasureTheory.set_integral_dirac {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [hE : CompleteSpace E] [NormedSpace E] [MeasurableSpace α] [MeasurableSingletonClass α] (f : αE) (a : α) (s : Set α) [Decidable (a s)] :
                                            ∫ (x : α) in s, f xMeasureTheory.Measure.dirac a = if a s then f a else 0

                                            Alias of MeasureTheory.setIntegral_dirac.

                                            theorem MeasureTheory.mul_meas_ge_le_integral_of_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (hf_nonneg : 0 ≤ᵐ[μ] f) (hf_int : MeasureTheory.Integrable f μ) (ε : ) :
                                            ε * (μ {x : α | ε f x}).toReal ∫ (x : α), f xμ

                                            Markov's inequality also known as Chebyshev's first inequality.

                                            theorem MeasureTheory.integral_mul_norm_le_Lp_mul_Lq {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_7} [NormedAddCommGroup E] {f : αE} {g : αE} {p : } {q : } (hpq : p.IsConjExponent q) (hf : MeasureTheory.Memℒp f (ENNReal.ofReal p) μ) (hg : MeasureTheory.Memℒp g (ENNReal.ofReal q) μ) :
                                            ∫ (a : α), f a * g aμ (∫ (a : α), f a ^ pμ) ^ (1 / p) * (∫ (a : α), g a ^ qμ) ^ (1 / q)

                                            Hölder's inequality for the integral of a product of norms. The integral of the product of two norms of functions is bounded by the product of their ℒp and ℒq seminorms when p and q are conjugate exponents.

                                            theorem MeasureTheory.integral_mul_le_Lp_mul_Lq_of_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : } {q : } (hpq : p.IsConjExponent q) {f : α} {g : α} (hf_nonneg : 0 ≤ᵐ[μ] f) (hg_nonneg : 0 ≤ᵐ[μ] g) (hf : MeasureTheory.Memℒp f (ENNReal.ofReal p) μ) (hg : MeasureTheory.Memℒp g (ENNReal.ofReal q) μ) :
                                            ∫ (a : α), f a * g aμ (∫ (a : α), f a ^ pμ) ^ (1 / p) * (∫ (a : α), g a ^ qμ) ^ (1 / q)

                                            Hölder's inequality for functions α → ℝ. The integral of the product of two nonnegative functions is bounded by the product of their ℒp and ℒq seminorms when p and q are conjugate exponents.

                                            theorem MeasureTheory.integral_countable' {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [hE : CompleteSpace E] [NormedSpace E] {m : MeasurableSpace α} [Countable α] [MeasurableSingletonClass α] {μ : MeasureTheory.Measure α} {f : αE} (hf : MeasureTheory.Integrable f μ) :
                                            ∫ (a : α), f aμ = ∑' (a : α), (μ {a}).toReal f a
                                            theorem MeasureTheory.integral_singleton' {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [hE : CompleteSpace E] [NormedSpace E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αE} (hf : MeasureTheory.StronglyMeasurable f) (a : α) :
                                            ∫ (a : α) in {a}, f aμ = (μ {a}).toReal f a
                                            theorem MeasureTheory.integral_singleton {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [hE : CompleteSpace E] [NormedSpace E] {m : MeasurableSpace α} [MeasurableSingletonClass α] {μ : MeasureTheory.Measure α} (f : αE) (a : α) :
                                            ∫ (a : α) in {a}, f aμ = (μ {a}).toReal f a
                                            theorem MeasureTheory.integral_countable {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [hE : CompleteSpace E] [NormedSpace E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSingletonClass α] (f : αE) {s : Set α} (hs : s.Countable) (hf : MeasureTheory.Integrable f (μ.restrict s)) :
                                            ∫ (a : α) in s, f aμ = ∑' (a : s), (μ {a}).toReal f a
                                            theorem MeasureTheory.integral_finset {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [hE : CompleteSpace E] [NormedSpace E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSingletonClass α] (s : Finset α) (f : αE) (hf : MeasureTheory.Integrable f (μ.restrict s)) :
                                            ∫ (x : α) in s, f xμ = xs, (μ {x}).toReal f x
                                            theorem MeasureTheory.integral_fintype {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [hE : CompleteSpace E] [NormedSpace E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSingletonClass α] [Fintype α] (f : αE) (hf : MeasureTheory.Integrable f μ) :
                                            ∫ (x : α), f xμ = x : α, (μ {x}).toReal f x
                                            theorem MeasureTheory.integral_unique {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [hE : CompleteSpace E] [NormedSpace E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Unique α] (f : αE) :
                                            ∫ (x : α), f xμ = (μ Set.univ).toReal f default
                                            theorem MeasureTheory.integral_pos_of_integrable_nonneg_nonzero {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.IsOpenPosMeasure] {f : α} {x : α} (f_cont : Continuous f) (f_int : MeasureTheory.Integrable f μ) (f_nonneg : 0 f) (f_x : f x 0) :
                                            0 < ∫ (x : α), f xμ

                                            Simple function seen as simple function of a larger MeasurableSpace.

                                            Equations
                                            Instances For
                                              theorem MeasureTheory.integral_simpleFunc_larger_space {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] [CompleteSpace F] {β : Type u_7} {m : MeasurableSpace β} {m0 : MeasurableSpace β} {μ : MeasureTheory.Measure β} (hm : m m0) (f : MeasureTheory.SimpleFunc β F) (hf_int : MeasureTheory.Integrable (⇑f) μ) :
                                              ∫ (x : β), f xμ = xf.range, (μ (f ⁻¹' {x})).toReal x
                                              theorem MeasureTheory.integral_trim_simpleFunc {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] [CompleteSpace F] {β : Type u_7} {m : MeasurableSpace β} {m0 : MeasurableSpace β} {μ : MeasureTheory.Measure β} (hm : m m0) (f : MeasureTheory.SimpleFunc β F) (hf_int : MeasureTheory.Integrable (⇑f) μ) :
                                              ∫ (x : β), f xμ = ∫ (x : β), f xμ.trim hm
                                              theorem MeasureTheory.integral_trim {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {β : Type u_7} {m : MeasurableSpace β} {m0 : MeasurableSpace β} {μ : MeasureTheory.Measure β} (hm : m m0) {f : βG} (hf : MeasureTheory.StronglyMeasurable f) :
                                              ∫ (x : β), f xμ = ∫ (x : β), f xμ.trim hm
                                              theorem MeasureTheory.integral_trim_ae {G : Type u_5} [NormedAddCommGroup G] [NormedSpace G] {β : Type u_7} {m : MeasurableSpace β} {m0 : MeasurableSpace β} {μ : MeasureTheory.Measure β} (hm : m m0) {f : βG} (hf : MeasureTheory.AEStronglyMeasurable f (μ.trim hm)) :
                                              ∫ (x : β), f xμ = ∫ (x : β), f xμ.trim hm
                                              theorem MeasureTheory.ae_eq_trim_of_stronglyMeasurable {β : Type u_7} {γ : Type u_8} {m : MeasurableSpace β} {m0 : MeasurableSpace β} {μ : MeasureTheory.Measure β} [TopologicalSpace γ] [TopologicalSpace.MetrizableSpace γ] (hm : m m0) {f : βγ} {g : βγ} (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g) (hfg : f =ᵐ[μ] g) :
                                              f =ᵐ[μ.trim hm] g
                                              theorem MeasureTheory.ae_eq_trim_iff {β : Type u_7} {γ : Type u_8} {m : MeasurableSpace β} {m0 : MeasurableSpace β} {μ : MeasureTheory.Measure β} [TopologicalSpace γ] [TopologicalSpace.MetrizableSpace γ] (hm : m m0) {f : βγ} {g : βγ} (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g) :
                                              f =ᵐ[μ.trim hm] g f =ᵐ[μ] g
                                              theorem MeasureTheory.ae_le_trim_iff {β : Type u_7} {γ : Type u_8} {m : MeasurableSpace β} {m0 : MeasurableSpace β} {μ : MeasureTheory.Measure β} [LinearOrder γ] [TopologicalSpace γ] [OrderClosedTopology γ] [TopologicalSpace.PseudoMetrizableSpace γ] (hm : m m0) {f : βγ} {g : βγ} (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g) :
                                              f ≤ᵐ[μ.trim hm] g f ≤ᵐ[μ] g
                                              theorem MeasureTheory.eLpNorm_one_le_of_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {r : NNReal} (hfint : MeasureTheory.Integrable f μ) (hfint' : 0 ∫ (x : α), f xμ) (hf : ∀ᵐ (ω : α) ∂μ, f ω r) :
                                              MeasureTheory.eLpNorm f 1 μ 2 * μ Set.univ * r
                                              @[deprecated MeasureTheory.eLpNorm_one_le_of_le]
                                              theorem MeasureTheory.snorm_one_le_of_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {r : NNReal} (hfint : MeasureTheory.Integrable f μ) (hfint' : 0 ∫ (x : α), f xμ) (hf : ∀ᵐ (ω : α) ∂μ, f ω r) :
                                              MeasureTheory.eLpNorm f 1 μ 2 * μ Set.univ * r

                                              Alias of MeasureTheory.eLpNorm_one_le_of_le.

                                              theorem MeasureTheory.eLpNorm_one_le_of_le' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {r : } (hfint : MeasureTheory.Integrable f μ) (hfint' : 0 ∫ (x : α), f xμ) (hf : ∀ᵐ (ω : α) ∂μ, f ω r) :
                                              MeasureTheory.eLpNorm f 1 μ 2 * μ Set.univ * ENNReal.ofReal r
                                              @[deprecated MeasureTheory.eLpNorm_one_le_of_le']
                                              theorem MeasureTheory.snorm_one_le_of_le' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {r : } (hfint : MeasureTheory.Integrable f μ) (hfint' : 0 ∫ (x : α), f xμ) (hf : ∀ᵐ (ω : α) ∂μ, f ω r) :
                                              MeasureTheory.eLpNorm f 1 μ 2 * μ Set.univ * ENNReal.ofReal r

                                              Alias of MeasureTheory.eLpNorm_one_le_of_le'.

                                              Positivity extension for integrals.

                                              This extension only proves non-negativity, strict positivity is more delicate for integration and requires more assumptions.

                                              Instances For