Documentation

Mathlib.MeasureTheory.Integral.Average

Integral average of a function #

In this file we define MeasureTheory.average μ f (notation: ⨍ x, f x ∂μ) to be the average value of f with respect to measure μ. It is defined as ∫ x, f x ∂((μ univ)⁻¹ • μ), so it is equal to zero if f is not integrable or if μ is an infinite measure. If μ is a probability measure, then the average of any function is equal to its integral.

For the average on a set, we use ⨍ x in s, f x ∂μ (notation for ⨍ x, f x ∂(μ.restrict s)). For average w.r.t. the volume, one can omit ∂volume.

Both have a version for the Lebesgue integral rather than Bochner.

We prove several version of the first moment method: An integrable function is below/above its average on a set of positive measure:

Implementation notes #

The average is defined as an integral over (μ univ)⁻¹ • μ so that all theorems about Bochner integrals work for the average without modifications. For theorems that require integrability of a function, we provide a convenience lemma MeasureTheory.Integrable.to_average.

Tags #

integral, center mass, average value

Average value of a function w.r.t. a measure #

The (Bochner, Lebesgue) average value of a function f w.r.t. a measure μ (notation: ⨍ x, f x ∂μ, ⨍⁻ x, f x ∂μ) is defined as the (Bochner, Lebesgue) integral divided by the total measure, so it is equal to zero if μ is an infinite measure, and (typically) equal to infinity if f is not integrable. If μ is a probability measure, then the average of any function is equal to its integral.

noncomputable def MeasureTheory.laverage {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : αENNReal) :

Average value of an ℝ≥0∞-valued function f w.r.t. a measure μ, denoted ⨍⁻ x, f x ∂μ.

It is equal to (μ univ)⁻¹ * ∫⁻ x, f x ∂μ, so it takes value zero if μ is an infinite measure. If μ is a probability measure, then the average of any function is equal to its integral.

For the average on a set, use ⨍⁻ x in s, f x ∂μ, defined as ⨍⁻ x, f x ∂(μ.restrict s). For the average w.r.t. the volume, one can omit ∂volume.

Equations
Instances For

    Pretty printer defined by notation3 command.

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

      Average value of an ℝ≥0∞-valued function f w.r.t. a measure μ.

      It is equal to (μ univ)⁻¹ * ∫⁻ x, f x ∂μ, so it takes value zero if μ is an infinite measure. If μ is a probability measure, then the average of any function is equal to its integral.

      For the average on a set, use ⨍⁻ x in s, f x ∂μ, defined as ⨍⁻ x, f x ∂(μ.restrict s). For the average w.r.t. the volume, one can omit ∂volume.

      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

          Average value of an ℝ≥0∞-valued function f w.r.t. to the standard measure.

          It is equal to (volume univ)⁻¹ * ∫⁻ x, f x, so it takes value zero if the space has infinite measure. In a probability space, the average of any function is equal to its integral.

          For the average on a set, use ⨍⁻ x in s, f x, defined as ⨍⁻ x, f x ∂(volume.restrict s).

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

            Average value of an ℝ≥0∞-valued function f w.r.t. a measure μ on a set s.

            It is equal to (μ s)⁻¹ * ∫⁻ x, f x ∂μ, so it takes value zero if s has infinite measure. If s has measure 1, then the average of any function is equal to its integral.

            For the average w.r.t. the volume, one can omit ∂volume.

            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

                Average value of an ℝ≥0∞-valued function f w.r.t. to the standard measure on a set s.

                It is equal to (volume s)⁻¹ * ∫⁻ x, f x, so it takes value zero if s has infinite measure. If s has measure 1, then the average of any function is equal to its integral.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem MeasureTheory.laverage_zero {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) :
                  ⨍⁻ (_x : α), 0μ = 0
                  @[simp]
                  theorem MeasureTheory.laverage_zero_measure {α : Type u_1} {m0 : MeasurableSpace α} (f : αENNReal) :
                  ⨍⁻ (x : α), f x0 = 0
                  theorem MeasureTheory.laverage_eq' {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : αENNReal) :
                  ⨍⁻ (x : α), f xμ = ∫⁻ (x : α), f x(μ Set.univ)⁻¹ μ
                  theorem MeasureTheory.laverage_eq {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : αENNReal) :
                  ⨍⁻ (x : α), f xμ = (∫⁻ (x : α), f xμ) / μ Set.univ
                  theorem MeasureTheory.laverage_eq_lintegral {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] (f : αENNReal) :
                  ⨍⁻ (x : α), f xμ = ∫⁻ (x : α), f xμ
                  @[simp]
                  theorem MeasureTheory.measure_mul_laverage {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (f : αENNReal) :
                  μ Set.univ * ⨍⁻ (x : α), f xμ = ∫⁻ (x : α), f xμ
                  theorem MeasureTheory.setLaverage_eq {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : αENNReal) (s : Set α) :
                  ⨍⁻ (x : α) in s, f xμ = (∫⁻ (x : α) in s, f xμ) / μ s
                  theorem MeasureTheory.setLaverage_eq' {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : αENNReal) (s : Set α) :
                  ⨍⁻ (x : α) in s, f xμ = ∫⁻ (x : α), f x(μ s)⁻¹ μ.restrict s
                  theorem MeasureTheory.laverage_congr {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} {g : αENNReal} (h : f =ᵐ[μ] g) :
                  ⨍⁻ (x : α), f xμ = ⨍⁻ (x : α), g xμ
                  theorem MeasureTheory.setLaverage_congr {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {f : αENNReal} (h : s =ᵐ[μ] t) :
                  ⨍⁻ (x : α) in s, f xμ = ⨍⁻ (x : α) in t, f xμ
                  theorem MeasureTheory.setLaverage_congr_fun {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : αENNReal} {g : αENNReal} (hs : MeasurableSet s) (h : ∀ᵐ (x : α) ∂μ, x sf x = g x) :
                  ⨍⁻ (x : α) in s, f xμ = ⨍⁻ (x : α) in s, g xμ
                  theorem MeasureTheory.laverage_lt_top {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} (hf : ∫⁻ (x : α), f xμ ) :
                  ⨍⁻ (x : α), f xμ <
                  theorem MeasureTheory.setLaverage_lt_top {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : αENNReal} :
                  ∫⁻ (x : α) in s, f xμ ⨍⁻ (x : α) in s, f xμ <
                  theorem MeasureTheory.laverage_add_measure {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : αENNReal} :
                  ⨍⁻ (x : α), f x(μ + ν) = μ Set.univ / (μ Set.univ + ν Set.univ) * ⨍⁻ (x : α), f xμ + ν Set.univ / (μ Set.univ + ν Set.univ) * ⨍⁻ (x : α), f xν
                  theorem MeasureTheory.measure_mul_setLaverage {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (f : αENNReal) (h : μ s ) :
                  μ s * ⨍⁻ (x : α) in s, f xμ = ∫⁻ (x : α) in s, f xμ
                  theorem MeasureTheory.laverage_union {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {f : αENNReal} (hd : MeasureTheory.AEDisjoint μ s t) (ht : MeasureTheory.NullMeasurableSet t μ) :
                  ⨍⁻ (x : α) in s t, f xμ = μ s / (μ s + μ t) * ⨍⁻ (x : α) in s, f xμ + μ t / (μ s + μ t) * ⨍⁻ (x : α) in t, f xμ
                  theorem MeasureTheory.laverage_union_mem_openSegment {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {f : αENNReal} (hd : MeasureTheory.AEDisjoint μ s t) (ht : MeasureTheory.NullMeasurableSet t μ) (hs₀ : μ s 0) (ht₀ : μ t 0) (hsμ : μ s ) (htμ : μ t ) :
                  ⨍⁻ (x : α) in s t, f xμ openSegment ENNReal (⨍⁻ (x : α) in s, f xμ) (⨍⁻ (x : α) in t, f xμ)
                  theorem MeasureTheory.laverage_union_mem_segment {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {f : αENNReal} (hd : MeasureTheory.AEDisjoint μ s t) (ht : MeasureTheory.NullMeasurableSet t μ) (hsμ : μ s ) (htμ : μ t ) :
                  ⨍⁻ (x : α) in s t, f xμ segment ENNReal (⨍⁻ (x : α) in s, f xμ) (⨍⁻ (x : α) in t, f xμ)
                  theorem MeasureTheory.laverage_mem_openSegment_compl_self {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : αENNReal} [MeasureTheory.IsFiniteMeasure μ] (hs : MeasureTheory.NullMeasurableSet s μ) (hs₀ : μ s 0) (hsc₀ : μ s 0) :
                  ⨍⁻ (x : α), f xμ openSegment ENNReal (⨍⁻ (x : α) in s, f xμ) (⨍⁻ (x : α) in s, f xμ)
                  @[simp]
                  theorem MeasureTheory.laverage_const {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [h : NeZero μ] (c : ENNReal) :
                  ⨍⁻ (_x : α), cμ = c
                  theorem MeasureTheory.setLaverage_const {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs₀ : μ s 0) (hs : μ s ) (c : ENNReal) :
                  ⨍⁻ (_x : α) in s, cμ = c
                  theorem MeasureTheory.laverage_one {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [NeZero μ] :
                  ⨍⁻ (_x : α), 1μ = 1
                  theorem MeasureTheory.setLaverage_one {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs₀ : μ s 0) (hs : μ s ) :
                  ⨍⁻ (_x : α) in s, 1μ = 1
                  theorem MeasureTheory.lintegral_laverage {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (f : αENNReal) :
                  ∫⁻ (_x : α), ⨍⁻ (a : α), f aμμ = ∫⁻ (x : α), f xμ
                  theorem MeasureTheory.setLintegral_setLaverage {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (f : αENNReal) (s : Set α) :
                  ∫⁻ (_x : α) in s, ⨍⁻ (a : α) in s, f aμμ = ∫⁻ (x : α) in s, f xμ
                  noncomputable def MeasureTheory.average {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] (μ : MeasureTheory.Measure α) (f : αE) :
                  E

                  Average value of a function f w.r.t. a measure μ, denoted ⨍ x, f x ∂μ.

                  It is equal to (μ univ).toReal⁻¹ • ∫ x, f x ∂μ, so it takes value zero if f is not integrable or if μ is an infinite measure. If μ is a probability measure, then the average of any function is equal to its integral.

                  For the average on a set, use ⨍ x in s, f x ∂μ, defined as ⨍ x, f x ∂(μ.restrict s). For the average w.r.t. the volume, one can omit ∂volume.

                  Equations
                  Instances For

                    Average value of a function f w.r.t. a measure μ.

                    It is equal to (μ univ).toReal⁻¹ • ∫ x, f x ∂μ, so it takes value zero if f is not integrable or if μ is an infinite measure. If μ is a probability measure, then the average of any function is equal to its integral.

                    For the average on a set, use ⨍ x in s, f x ∂μ, defined as ⨍ x, f x ∂(μ.restrict s). For the average w.r.t. the volume, one can omit ∂volume.

                    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

                          Average value of a function f w.r.t. to the standard measure.

                          It is equal to (volume univ).toReal⁻¹ * ∫ x, f x, so it takes value zero if f is not integrable or if the space has infinite measure. In a probability space, the average of any function is equal to its integral.

                          For the average on a set, use ⨍ x in s, f x, defined as ⨍ x, f x ∂(volume.restrict s).

                          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

                              Average value of a function f w.r.t. a measure μ on a set s.

                              It is equal to (μ s).toReal⁻¹ * ∫ x, f x ∂μ, so it takes value zero if f is not integrable on s or if s has infinite measure. If s has measure 1, then the average of any function is equal to its integral.

                              For the average w.r.t. the volume, one can omit ∂volume.

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

                                Average value of a function f w.r.t. to the standard measure on a set s.

                                It is equal to (volume s).toReal⁻¹ * ∫ x, f x, so it takes value zero f is not integrable on s or if s has infinite measure. If s has measure 1, then the average of any function is equal to its 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
                                    @[simp]
                                    theorem MeasureTheory.average_zero {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] (μ : MeasureTheory.Measure α) :
                                    ⨍ (x : α), 0μ = 0
                                    @[simp]
                                    theorem MeasureTheory.average_zero_measure {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] (f : αE) :
                                    ⨍ (x : α), f x0 = 0
                                    @[simp]
                                    theorem MeasureTheory.average_neg {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] (μ : MeasureTheory.Measure α) (f : αE) :
                                    ⨍ (x : α), -f xμ = -⨍ (x : α), f xμ
                                    theorem MeasureTheory.average_eq' {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] (μ : MeasureTheory.Measure α) (f : αE) :
                                    ⨍ (x : α), f xμ = ∫ (x : α), f x(μ Set.univ)⁻¹ μ
                                    theorem MeasureTheory.average_eq {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] (μ : MeasureTheory.Measure α) (f : αE) :
                                    ⨍ (x : α), f xμ = (μ Set.univ).toReal⁻¹ ∫ (x : α), f xμ
                                    theorem MeasureTheory.average_eq_integral {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] (f : αE) :
                                    ⨍ (x : α), f xμ = ∫ (x : α), f xμ
                                    @[simp]
                                    theorem MeasureTheory.measure_smul_average {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (f : αE) :
                                    (μ Set.univ).toReal ⨍ (x : α), f xμ = ∫ (x : α), f xμ
                                    theorem MeasureTheory.setAverage_eq {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] (μ : MeasureTheory.Measure α) (f : αE) (s : Set α) :
                                    ⨍ (x : α) in s, f xμ = (μ s).toReal⁻¹ ∫ (x : α) in s, f xμ
                                    theorem MeasureTheory.setAverage_eq' {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] (μ : MeasureTheory.Measure α) (f : αE) (s : Set α) :
                                    ⨍ (x : α) in s, f xμ = ∫ (x : α), f x(μ s)⁻¹ μ.restrict s
                                    theorem MeasureTheory.average_congr {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] {μ : MeasureTheory.Measure α} {f : αE} {g : αE} (h : f =ᵐ[μ] g) :
                                    ⨍ (x : α), f xμ = ⨍ (x : α), g xμ
                                    theorem MeasureTheory.setAverage_congr {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {f : αE} (h : s =ᵐ[μ] t) :
                                    ⨍ (x : α) in s, f xμ = ⨍ (x : α) in t, f xμ
                                    theorem MeasureTheory.setAverage_congr_fun {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] {μ : MeasureTheory.Measure α} {s : Set α} {f : αE} {g : αE} (hs : MeasurableSet s) (h : ∀ᵐ (x : α) ∂μ, x sf x = g x) :
                                    ⨍ (x : α) in s, f xμ = ⨍ (x : α) in s, g xμ
                                    theorem MeasureTheory.average_add_measure {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure ν] {f : αE} (hμ : MeasureTheory.Integrable f μ) (hν : MeasureTheory.Integrable f ν) :
                                    ⨍ (x : α), f x(μ + ν) = ((μ Set.univ).toReal / ((μ Set.univ).toReal + (ν Set.univ).toReal)) ⨍ (x : α), f xμ + ((ν Set.univ).toReal / ((μ Set.univ).toReal + (ν Set.univ).toReal)) ⨍ (x : α), f xν
                                    theorem MeasureTheory.average_pair {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] [CompleteSpace F] {μ : MeasureTheory.Measure α} [CompleteSpace E] {f : αE} {g : αF} (hfi : MeasureTheory.Integrable f μ) (hgi : MeasureTheory.Integrable g μ) :
                                    ⨍ (x : α), (f x, g x)μ = (⨍ (x : α), f xμ, ⨍ (x : α), g xμ)
                                    theorem MeasureTheory.measure_smul_setAverage {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] {μ : MeasureTheory.Measure α} (f : αE) {s : Set α} (h : μ s ) :
                                    (μ s).toReal ⨍ (x : α) in s, f xμ = ∫ (x : α) in s, f xμ
                                    theorem MeasureTheory.average_union {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] {μ : MeasureTheory.Measure α} {f : αE} {s : Set α} {t : Set α} (hd : MeasureTheory.AEDisjoint μ s t) (ht : MeasureTheory.NullMeasurableSet t μ) (hsμ : μ s ) (htμ : μ t ) (hfs : MeasureTheory.IntegrableOn f s μ) (hft : MeasureTheory.IntegrableOn f t μ) :
                                    ⨍ (x : α) in s t, f xμ = ((μ s).toReal / ((μ s).toReal + (μ t).toReal)) ⨍ (x : α) in s, f xμ + ((μ t).toReal / ((μ s).toReal + (μ t).toReal)) ⨍ (x : α) in t, f xμ
                                    theorem MeasureTheory.average_union_mem_openSegment {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] {μ : MeasureTheory.Measure α} {f : αE} {s : Set α} {t : Set α} (hd : MeasureTheory.AEDisjoint μ s t) (ht : MeasureTheory.NullMeasurableSet t μ) (hs₀ : μ s 0) (ht₀ : μ t 0) (hsμ : μ s ) (htμ : μ t ) (hfs : MeasureTheory.IntegrableOn f s μ) (hft : MeasureTheory.IntegrableOn f t μ) :
                                    ⨍ (x : α) in s t, f xμ openSegment (⨍ (x : α) in s, f xμ) (⨍ (x : α) in t, f xμ)
                                    theorem MeasureTheory.average_union_mem_segment {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] {μ : MeasureTheory.Measure α} {f : αE} {s : Set α} {t : Set α} (hd : MeasureTheory.AEDisjoint μ s t) (ht : MeasureTheory.NullMeasurableSet t μ) (hsμ : μ s ) (htμ : μ t ) (hfs : MeasureTheory.IntegrableOn f s μ) (hft : MeasureTheory.IntegrableOn f t μ) :
                                    ⨍ (x : α) in s t, f xμ segment (⨍ (x : α) in s, f xμ) (⨍ (x : α) in t, f xμ)
                                    theorem MeasureTheory.average_mem_openSegment_compl_self {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {f : αE} {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) (hs₀ : μ s 0) (hsc₀ : μ s 0) (hfi : MeasureTheory.Integrable f μ) :
                                    ⨍ (x : α), f xμ openSegment (⨍ (x : α) in s, f xμ) (⨍ (x : α) in s, f xμ)
                                    @[simp]
                                    theorem MeasureTheory.average_const {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [h : NeZero μ] (c : E) :
                                    ⨍ (_x : α), cμ = c
                                    theorem MeasureTheory.setAverage_const {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] {μ : MeasureTheory.Measure α} [CompleteSpace E] {s : Set α} (hs₀ : μ s 0) (hs : μ s ) (c : E) :
                                    ⨍ (x : α) in s, cμ = c
                                    theorem MeasureTheory.integral_average {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (f : αE) :
                                    ∫ (x : α), ⨍ (a : α), f aμμ = ∫ (x : α), f xμ
                                    theorem MeasureTheory.setIntegral_setAverage {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (f : αE) (s : Set α) :
                                    ∫ (x : α) in s, ⨍ (a : α) in s, f aμμ = ∫ (x : α) in s, f xμ
                                    theorem MeasureTheory.integral_sub_average {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (f : αE) :
                                    ∫ (x : α), f x - ⨍ (a : α), f aμμ = 0
                                    theorem MeasureTheory.setAverage_sub_setAverage {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] {μ : MeasureTheory.Measure α} {s : Set α} [CompleteSpace E] (hs : μ s ) (f : αE) :
                                    ∫ (x : α) in s, f x - ⨍ (a : α) in s, f aμμ = 0
                                    theorem MeasureTheory.integral_average_sub {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] {μ : MeasureTheory.Measure α} {f : αE} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Integrable f μ) :
                                    ∫ (x : α), ⨍ (a : α), f aμ - f xμ = 0
                                    theorem MeasureTheory.setIntegral_setAverage_sub {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] {μ : MeasureTheory.Measure α} {s : Set α} {f : αE} [CompleteSpace E] (hs : μ s ) (hf : MeasureTheory.IntegrableOn f s μ) :
                                    ∫ (x : α) in s, ⨍ (a : α) in s, f aμ - f xμ = 0
                                    theorem MeasureTheory.ofReal_average {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (hf : MeasureTheory.Integrable f μ) (hf₀ : 0 ≤ᵐ[μ] f) :
                                    ENNReal.ofReal (⨍ (x : α), f xμ) = (∫⁻ (x : α), ENNReal.ofReal (f x)μ) / μ Set.univ
                                    theorem MeasureTheory.ofReal_setAverage {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α} (hf : MeasureTheory.IntegrableOn f s μ) (hf₀ : 0 ≤ᵐ[μ.restrict s] f) :
                                    ENNReal.ofReal (⨍ (x : α) in s, f xμ) = (∫⁻ (x : α) in s, ENNReal.ofReal (f x)μ) / μ s
                                    theorem MeasureTheory.toReal_laverage {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} (hf : AEMeasurable f μ) (hf' : ∀ᵐ (x : α) ∂μ, f x ) :
                                    (⨍⁻ (x : α), f xμ).toReal = ⨍ (x : α), (f x).toRealμ
                                    theorem MeasureTheory.toReal_setLaverage {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : αENNReal} (hf : AEMeasurable f (μ.restrict s)) (hf' : ∀ᵐ (x : α) ∂μ.restrict s, f x ) :
                                    (⨍⁻ (x : α) in s, f xμ).toReal = ⨍ (x : α) in s, (f x).toRealμ

                                    First moment method #

                                    theorem MeasureTheory.measure_le_setAverage_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α} (hμ : μ s 0) (hμ₁ : μ s ) (hf : MeasureTheory.IntegrableOn f s μ) :
                                    0 < μ {x : α | x s f x ⨍ (a : α) in s, f aμ}

                                    First moment method. An integrable function is smaller than its mean on a set of positive measure.

                                    theorem MeasureTheory.measure_setAverage_le_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α} (hμ : μ s 0) (hμ₁ : μ s ) (hf : MeasureTheory.IntegrableOn f s μ) :
                                    0 < μ {x : α | x s ⨍ (a : α) in s, f aμ f x}

                                    First moment method. An integrable function is greater than its mean on a set of positive measure.

                                    theorem MeasureTheory.exists_le_setAverage {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α} (hμ : μ s 0) (hμ₁ : μ s ) (hf : MeasureTheory.IntegrableOn f s μ) :
                                    xs, f x ⨍ (a : α) in s, f aμ

                                    First moment method. The minimum of an integrable function is smaller than its mean.

                                    theorem MeasureTheory.exists_setAverage_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α} (hμ : μ s 0) (hμ₁ : μ s ) (hf : MeasureTheory.IntegrableOn f s μ) :
                                    xs, ⨍ (a : α) in s, f aμ f x

                                    First moment method. The maximum of an integrable function is greater than its mean.

                                    theorem MeasureTheory.measure_le_average_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} [MeasureTheory.IsFiniteMeasure μ] (hμ : μ 0) (hf : MeasureTheory.Integrable f μ) :
                                    0 < μ {x : α | f x ⨍ (a : α), f aμ}

                                    First moment method. An integrable function is smaller than its mean on a set of positive measure.

                                    theorem MeasureTheory.measure_average_le_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} [MeasureTheory.IsFiniteMeasure μ] (hμ : μ 0) (hf : MeasureTheory.Integrable f μ) :
                                    0 < μ {x : α | ⨍ (a : α), f aμ f x}

                                    First moment method. An integrable function is greater than its mean on a set of positive measure.

                                    theorem MeasureTheory.exists_le_average {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} [MeasureTheory.IsFiniteMeasure μ] (hμ : μ 0) (hf : MeasureTheory.Integrable f μ) :
                                    ∃ (x : α), f x ⨍ (a : α), f aμ

                                    First moment method. The minimum of an integrable function is smaller than its mean.

                                    theorem MeasureTheory.exists_average_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} [MeasureTheory.IsFiniteMeasure μ] (hμ : μ 0) (hf : MeasureTheory.Integrable f μ) :
                                    ∃ (x : α), ⨍ (a : α), f aμ f x

                                    First moment method. The maximum of an integrable function is greater than its mean.

                                    theorem MeasureTheory.exists_not_mem_null_le_average {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : α} [MeasureTheory.IsFiniteMeasure μ] (hμ : μ 0) (hf : MeasureTheory.Integrable f μ) (hN : μ N = 0) :
                                    xN, f x ⨍ (a : α), f aμ

                                    First moment method. The minimum of an integrable function is smaller than its mean, while avoiding a null set.

                                    theorem MeasureTheory.exists_not_mem_null_average_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : α} [MeasureTheory.IsFiniteMeasure μ] (hμ : μ 0) (hf : MeasureTheory.Integrable f μ) (hN : μ N = 0) :
                                    xN, ⨍ (a : α), f aμ f x

                                    First moment method. The maximum of an integrable function is greater than its mean, while avoiding a null set.

                                    theorem MeasureTheory.measure_le_integral_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} [MeasureTheory.IsProbabilityMeasure μ] (hf : MeasureTheory.Integrable f μ) :
                                    0 < μ {x : α | f x ∫ (a : α), f aμ}

                                    First moment method. An integrable function is smaller than its integral on a set of positive measure.

                                    theorem MeasureTheory.measure_integral_le_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} [MeasureTheory.IsProbabilityMeasure μ] (hf : MeasureTheory.Integrable f μ) :
                                    0 < μ {x : α | ∫ (a : α), f aμ f x}

                                    First moment method. An integrable function is greater than its integral on a set of positive measure.

                                    theorem MeasureTheory.exists_le_integral {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} [MeasureTheory.IsProbabilityMeasure μ] (hf : MeasureTheory.Integrable f μ) :
                                    ∃ (x : α), f x ∫ (a : α), f aμ

                                    First moment method. The minimum of an integrable function is smaller than its integral.

                                    theorem MeasureTheory.exists_integral_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} [MeasureTheory.IsProbabilityMeasure μ] (hf : MeasureTheory.Integrable f μ) :
                                    ∃ (x : α), ∫ (a : α), f aμ f x

                                    First moment method. The maximum of an integrable function is greater than its integral.

                                    theorem MeasureTheory.exists_not_mem_null_le_integral {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : α} [MeasureTheory.IsProbabilityMeasure μ] (hf : MeasureTheory.Integrable f μ) (hN : μ N = 0) :
                                    xN, f x ∫ (a : α), f aμ

                                    First moment method. The minimum of an integrable function is smaller than its integral, while avoiding a null set.

                                    theorem MeasureTheory.exists_not_mem_null_integral_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : α} [MeasureTheory.IsProbabilityMeasure μ] (hf : MeasureTheory.Integrable f μ) (hN : μ N = 0) :
                                    xN, ∫ (a : α), f aμ f x

                                    First moment method. The maximum of an integrable function is greater than its integral, while avoiding a null set.

                                    theorem MeasureTheory.measure_le_setLaverage_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : αENNReal} (hμ : μ s 0) (hμ₁ : μ s ) (hf : AEMeasurable f (μ.restrict s)) :
                                    0 < μ {x : α | x s f x ⨍⁻ (a : α) in s, f aμ}

                                    First moment method. A measurable function is smaller than its mean on a set of positive measure.

                                    theorem MeasureTheory.measure_setLaverage_le_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : αENNReal} (hμ : μ s 0) (hs : MeasureTheory.NullMeasurableSet s μ) (hint : ∫⁻ (a : α) in s, f aμ ) :
                                    0 < μ {x : α | x s ⨍⁻ (a : α) in s, f aμ f x}

                                    First moment method. A measurable function is greater than its mean on a set of positive measure.

                                    theorem MeasureTheory.exists_le_setLaverage {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : αENNReal} (hμ : μ s 0) (hμ₁ : μ s ) (hf : AEMeasurable f (μ.restrict s)) :
                                    xs, f x ⨍⁻ (a : α) in s, f aμ

                                    First moment method. The minimum of a measurable function is smaller than its mean.

                                    theorem MeasureTheory.exists_setLaverage_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : αENNReal} (hμ : μ s 0) (hs : MeasureTheory.NullMeasurableSet s μ) (hint : ∫⁻ (a : α) in s, f aμ ) :
                                    xs, ⨍⁻ (a : α) in s, f aμ f x

                                    First moment method. The maximum of a measurable function is greater than its mean.

                                    theorem MeasureTheory.measure_laverage_le_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} (hμ : μ 0) (hint : ∫⁻ (a : α), f aμ ) :
                                    0 < μ {x : α | ⨍⁻ (a : α), f aμ f x}

                                    First moment method. A measurable function is greater than its mean on a set of positive measure.

                                    theorem MeasureTheory.exists_laverage_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} (hμ : μ 0) (hint : ∫⁻ (a : α), f aμ ) :
                                    ∃ (x : α), ⨍⁻ (a : α), f aμ f x

                                    First moment method. The maximum of a measurable function is greater than its mean.

                                    theorem MeasureTheory.exists_not_mem_null_laverage_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : αENNReal} (hμ : μ 0) (hint : ∫⁻ (a : α), f aμ ) (hN : μ N = 0) :
                                    xN, ⨍⁻ (a : α), f aμ f x

                                    First moment method. The maximum of a measurable function is greater than its mean, while avoiding a null set.

                                    theorem MeasureTheory.measure_le_laverage_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} [MeasureTheory.IsFiniteMeasure μ] (hμ : μ 0) (hf : AEMeasurable f μ) :
                                    0 < μ {x : α | f x ⨍⁻ (a : α), f aμ}

                                    First moment method. A measurable function is smaller than its mean on a set of positive measure.

                                    theorem MeasureTheory.exists_le_laverage {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} [MeasureTheory.IsFiniteMeasure μ] (hμ : μ 0) (hf : AEMeasurable f μ) :
                                    ∃ (x : α), f x ⨍⁻ (a : α), f aμ

                                    First moment method. The minimum of a measurable function is smaller than its mean.

                                    theorem MeasureTheory.exists_not_mem_null_le_laverage {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : αENNReal} [MeasureTheory.IsFiniteMeasure μ] (hμ : μ 0) (hf : AEMeasurable f μ) (hN : μ N = 0) :
                                    xN, f x ⨍⁻ (a : α), f aμ

                                    First moment method. The minimum of a measurable function is smaller than its mean, while avoiding a null set.

                                    theorem MeasureTheory.measure_le_lintegral_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} [MeasureTheory.IsProbabilityMeasure μ] (hf : AEMeasurable f μ) :
                                    0 < μ {x : α | f x ∫⁻ (a : α), f aμ}

                                    First moment method. A measurable function is smaller than its integral on a set f positive measure.

                                    theorem MeasureTheory.measure_lintegral_le_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} [MeasureTheory.IsProbabilityMeasure μ] (hint : ∫⁻ (a : α), f aμ ) :
                                    0 < μ {x : α | ∫⁻ (a : α), f aμ f x}

                                    First moment method. A measurable function is greater than its integral on a set f positive measure.

                                    theorem MeasureTheory.exists_le_lintegral {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} [MeasureTheory.IsProbabilityMeasure μ] (hf : AEMeasurable f μ) :
                                    ∃ (x : α), f x ∫⁻ (a : α), f aμ

                                    First moment method. The minimum of a measurable function is smaller than its integral.

                                    theorem MeasureTheory.exists_lintegral_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} [MeasureTheory.IsProbabilityMeasure μ] (hint : ∫⁻ (a : α), f aμ ) :
                                    ∃ (x : α), ∫⁻ (a : α), f aμ f x

                                    First moment method. The maximum of a measurable function is greater than its integral.

                                    theorem MeasureTheory.exists_not_mem_null_le_lintegral {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : αENNReal} [MeasureTheory.IsProbabilityMeasure μ] (hf : AEMeasurable f μ) (hN : μ N = 0) :
                                    xN, f x ∫⁻ (a : α), f aμ

                                    First moment method. The minimum of a measurable function is smaller than its integral, while avoiding a null set.

                                    theorem MeasureTheory.exists_not_mem_null_lintegral_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : αENNReal} [MeasureTheory.IsProbabilityMeasure μ] (hint : ∫⁻ (a : α), f aμ ) (hN : μ N = 0) :
                                    xN, ∫⁻ (a : α), f aμ f x

                                    First moment method. The maximum of a measurable function is greater than its integral, while avoiding a null set.

                                    theorem MeasureTheory.tendsto_integral_smul_of_tendsto_average_norm_sub {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace E] {μ : MeasureTheory.Measure α} [CompleteSpace E] {ι : Type u_4} {a : ιSet α} {l : Filter ι} {f : αE} {c : E} {g : ια} (K : ) (hf : Filter.Tendsto (fun (i : ι) => ⨍ (y : α) in a i, f y - cμ) l (nhds 0)) (f_int : ∀ᶠ (i : ι) in l, MeasureTheory.IntegrableOn f (a i) μ) (hg : Filter.Tendsto (fun (i : ι) => ∫ (y : α), g i yμ) l (nhds 1)) (g_supp : ∀ᶠ (i : ι) in l, Function.support (g i) a i) (g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| K / (μ (a i)).toReal) :
                                    Filter.Tendsto (fun (i : ι) => ∫ (y : α), g i y f yμ) l (nhds c)

                                    If the average of a function f along a sequence of sets aₙ converges to c (more precisely, we require that ⨍ y in a i, ‖f y - c‖ ∂μ tends to 0), then the integral of gₙ • f also tends to c if gₙ is supported in aₙ, has integral converging to one and supremum at most K / μ aₙ.