LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.MeasureTheory.Measure.MeasureSpace

`MeasureTheory.ae_eq_bot` theorem MeasureTheory.ae_eq_bot : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.ae = ⊥ ↔ μ = 0 This theorem states that for any type `α`, any measurable space `m0` on `α`, and any measure `μ` on `α`, the "almost everywhere" filter of co-null sets of `μ` is equal to the bottom filter (denoted by `⊥`), if and only if the measure `μ` itself is zero. In other words, the measure `μ` is zero if and only if its "almost everywhere" filter, which consists of sets with complement of measure zero, is the trivial or bottom filter. More concisely: For any measure `μ` on a measurable space `(α, m0)`, the "almost everywhere" filter of co-null sets equals the bottom filter if and only if `μ` is the zero measure.
`MeasureTheory.ae_mono` theorem MeasureTheory.ae_mono : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ ≤ ν → μ.ae ≤ ν.ae The theorem `MeasureTheory.ae_mono` states that for any type `α`, given measurable space `m0` on `α` and two measures `μ` and `ν` from the measure theory on `α`, if `μ` is less than or equal to `ν`, then the "almost everywhere" filter of co-null sets of `μ` is less than or equal to the "almost everywhere" filter of co-null sets of `ν`. In other words, it establishes a monotonicity property for "almost everywhere" filters of co-null sets in the context of measure theory. More concisely: If `μ` is a measure less than or equal to `ν` on measurable space `(α, m0)`, then the filter of `μ`'s co-null sets is included in the filter of `ν`'s co-null sets.
`MeasureTheory.Measure.le_add_right` theorem MeasureTheory.Measure.le_add_right : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν ν' : MeasureTheory.Measure α}, μ ≤ ν → μ ≤ ν + ν' This theorem states that for any measurable space `α` and three measures `μ`, `ν`, and `ν'` on this space, if `μ` is less than or equal to `ν`, then `μ` is also less than or equal to the sum of `ν` and `ν'`. This result is a property of measures in measure theory, a branch of mathematics related to the concept of size or quantity. More concisely: For any measurable spaces `α` and measures `μ`, `ν`, `ν'` on `α` with `μ ≤ ν`, we have `μ ≤ ν + ν'`.
`MeasureTheory.exists_nonempty_inter_of_measure_univ_lt_tsum_measure` theorem MeasureTheory.exists_nonempty_inter_of_measure_univ_lt_tsum_measure : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) {s : ι → Set α}, (∀ (i : ι), MeasurableSet (s i)) → ↑↑μ Set.univ < ∑' (i : ι), ↑↑μ (s i) → ∃ i j, i ≠ j ∧ (s i ∩ s j).Nonempty The theorem `MeasureTheory.exists_nonempty_inter_of_measure_univ_lt_tsum_measure` represents the Pigeonhole Principle in the context of measure spaces. It asserts that for any type `α` and any index type `ι`, given a measurable space `m` on `α`, a measure `μ` on this measurable space, and a function `s` from `ι` to a set of `α`, if every set `s i` is a measurable set and the measure of the universal set is less than the sum of the measures of each set `s i`, then there exist two indices `i` and `j` such that `i` is not equal to `j` and the intersection of the sets `s i` and `s j` is not empty. In other words, if the total measure of the collection of sets exceeds the total measure of the universe, then at least two of these sets must overlap. More concisely: If `μ` is a finite measure on a measurable space `(α, Σ, m)`, and for every `i` in an index type `ι`, `s i` is a measurable subset of `α` with finite measure, then there exist distinct indices `i` and `j` such that `s i ∩ s j` is non-empty if the sum of the measures of `s i` over all `i` in `ι` exceeds the measure of the universal set `m α`.
`MeasureTheory.measure_compl` theorem MeasureTheory.measure_compl : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}, MeasurableSet s → ↑↑μ s ≠ ⊤ → ↑↑μ sᶜ = ↑↑μ Set.univ - ↑↑μ s The theorem `MeasureTheory.measure_compl` states that for any type `α`, any measurable space `m` on `α`, any measure `μ` in that measurable space, and any set `s` of type `α` that is measurable in the aforementioned measurable space, as long as the measure of the set `s` is not infinite, then the measure of the complement of the set `s` equals the measure of the universal set subtracted by the measure of the set `s`. In mathematical terms, this is stated as: if `s` is a measurable subset of a measurable space and μ(s) ≠ ∞, then μ(sᶜ) = μ(U) - μ(s), where U is the universal set, sᶜ is the complement of `s`, and μ() denotes the measure of a set. More concisely: For any measurable set `s` in a measurable space with finite measure `μ`, the measure of its complement is equal to the measure of the universal set minus the measure of `s`.
`MeasureTheory.Measure.QuasiMeasurePreserving.aemeasurable` theorem MeasureTheory.Measure.QuasiMeasurePreserving.aemeasurable : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : α → β}, MeasureTheory.Measure.QuasiMeasurePreserving f μa μb → AEMeasurable f μa The theorem `MeasureTheory.Measure.QuasiMeasurePreserving.aemeasurable` states that for all types `α` and `β`, given a measurable space `m0` on `α`, a measurable space instance on `β`, measures `μa` on `α` and `μb` on `β`, and a function `f` from `α` to `β`, if `f` is quasi-measure-preserving with respect to measures `μa` and `μb`, then `f` is almost everywhere measurable with respect to measure `μa`. In other words, if a function preserves the measure of subsets "almost everywhere" (except possibly on a subset of measure zero), then this function is also almost everywhere measurable, meaning it coincides almost everywhere with a measurable function. More concisely: A quasi-measure-preserving function between measurable spaces is almost everywhere measurable.
`MeasureTheory.Measure.le_iff'` theorem MeasureTheory.Measure.le_iff' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ μ₂ : MeasureTheory.Measure α}, μ₁ ≤ μ₂ ↔ ∀ (s : Set α), ↑↑μ₁ s ≤ ↑↑μ₂ s This theorem states that for any type `α`, measurable space `m0` of `α`, and two measures `μ₁` and `μ₂` of `α`, `μ₁` is less than or equal to `μ₂` if and only if for every set `s` of `α`, the measure of `s` under `μ₁` is less than or equal to the measure of `s` under `μ₂`. This theorem connects the order relation between two measures to the order relations of their measurements on all sets, which is a fundamental property in measure theory. More concisely: For any measurable spaces `(α, m0)` and measures `μ₁` and `μ₂` on `α`, `μ₁ ≤ μ₂` if and only if `μ₁(s) ≤ μ₂(s)` for all sets `s` in `α`.
`LE.le.absolutelyContinuous_of_ae` theorem LE.le.absolutelyContinuous_of_ae : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ.ae ≤ ν.ae → μ.AbsolutelyContinuous ν This theorem, named `LE.le.absolutelyContinuous_of_ae`, is an alias for the forward direction of `MeasureTheory.Measure.ae_le_iff_absolutelyContinuous`. It states that for any type `α`, any measurable space `m0` of type `α`, and any two measures `μ` and `ν` of the same type `α`, if the almost everywhere measure of `μ` is less than or equal to the almost everywhere measure of `ν`, then `μ` is absolutely continuous with respect to `ν`. More concisely: If `μ` and `ν` are measures of the same type on a measurable space, and the almost everywhere measure of `μ` is less than or equal to that of `ν`, then `μ` is absolutely continuous with respect to `ν`.
`MeasureTheory.Measure.AbsolutelyContinuous.rfl` theorem MeasureTheory.Measure.AbsolutelyContinuous.rfl : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.AbsolutelyContinuous μ The theorem states that for any type `α` and any measurable space `m0` on `α`, any measure `μ` is absolutely continuous with respect to itself. In other words, for any given set `s` in the measurable space, if the measure of `s` according to `μ` is zero, then the measure of `s` according to `μ` is also zero, which is trivially true since we are considering the same measure `μ`. More concisely: For any measurable space `(α, m0)` and measure `μ` on `α`, the measure `μ` is absolutely continuous with respect to itself.
`MeasureTheory.Measure.QuasiMeasurePreserving.mono` theorem MeasureTheory.Measure.QuasiMeasurePreserving.mono : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μa μa' : MeasureTheory.Measure α} {μb μb' : MeasureTheory.Measure β} {f : α → β}, μa'.AbsolutelyContinuous μa → μb.AbsolutelyContinuous μb' → MeasureTheory.Measure.QuasiMeasurePreserving f μa μb → MeasureTheory.Measure.QuasiMeasurePreserving f μa' μb' The theorem states that, for any two types `α` and `β` with associated measurable spaces `m0` and `inst`, and for any two pairs of measures (`μa`, `μa'`) on `α` and (`μb`, `μb'`) on `β`, along with a function `f` from `α` to `β`, if `μa'` is absolutely continuous with respect to `μa` and `μb` is absolutely continuous with respect to `μb'`, and if `f` is a quasi measure preserving function from `μa` to `μb`, then `f` is also a quasi measure preserving function from `μa'` to `μb'`. In other words, if a function preserves the measure from `μa` to `μb`, and if `μa'` and `μb` are dominated by `μa` and `μb'` respectively (meaning that any set with measure zero under `μa` or `μb` also has measure zero under `μa'` or `μb'`), then the function also preserves the measure from `μa'` to `μb'`. More concisely: If measures `μa'` and `μb'` are absolutely continuous with respect to `μa` and `μb` respectively, and `f` is a quasi measure preserving function from `(α, μa)` to `(β, μb)`, then `f` is also a quasi measure preserving function from `(α, μa')` to `(β, μb')`.
`MeasurableEquiv.map_apply` theorem MeasurableEquiv.map_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α} (f : α ≃ᵐ β) (s : Set β), ↑↑(MeasureTheory.Measure.map (⇑f) μ) s = ↑↑μ (⇑f ⁻¹' s) The theorem `MeasurableEquiv.map_apply` states that for any two types `α` and `β` that are both equipped with a measurable space structure, any measure `μ` on `α`, a measurable equivalence `f` from `α` to `β`, and any set `s` of type `β`, the measure of `s` when we pushforward the measure `μ` along `f` (which is denoted by `MeasureTheory.Measure.map (⇑f) μ`) is equal to the measure of the preimage of `s` under `f` with respect to the measure `μ` (which is denoted by `μ (⇑f ⁻¹' s)`). In other words, mapping a measure along a measurable equivalence allows us to compute the measure on all sets, not just the measurable ones, by using the original measure on the preimage of the sets. More concisely: For measurable spaces (α, μ) and (β), any measurable equivalence f : α → β, and any set s in β, the measure of s under the pushforward measure ⇑f μ is equal to the measure of f⁻¹(s) under the original measure μ.
`MeasureTheory.ae_uIoc_iff` theorem MeasureTheory.ae_uIoc_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : LinearOrder α] {a b : α} {P : α → Prop}, (∀ᵐ (x : α) ∂μ, x ∈ Ι a b → P x) ↔ (∀ᵐ (x : α) ∂μ, x ∈ Set.Ioc a b → P x) ∧ ∀ᵐ (x : α) ∂μ, x ∈ Set.Ioc b a → P x The theorem `MeasureTheory.ae_uIoc_iff` in Lean 4 states that for any measurable space `α`, measure `μ`, linear order `inst`, and two elements `a` and `b` of `α`, as well as a proposition `P` that applies to elements of `α`, the almost everywhere (with respect to measure `μ`) truth of the proposition `P` on the union of the intervals `(a, b]` and `(b, a]` is equivalent to the conjunction of the almost everywhere truth of `P` on the intervals `(a, b]` and `(b, a]` separately. Symbolically, it states the equivalence $(\mu$-almost everywhere $x \in (a, b] \cup (b, a] \Rightarrow P(x))$ iff $(\mu$-almost everywhere $x \in (a, b] \Rightarrow P(x))$ and $(\mu$-almost everywhere $x \in (b, a] \Rightarrow P(x))$. More concisely: The theorem asserts that the almost everywhere truth of a proposition on the union of two disjoint intervals with respect to a measure is equivalent to the conjunction of its almost everywhere truth on each interval.
`MeasureTheory.Measure.map_congr` theorem MeasureTheory.Measure.map_congr : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α} {f g : α → β}, μ.ae.EventuallyEq f g → MeasureTheory.Measure.map f μ = MeasureTheory.Measure.map g μ The theorem `MeasureTheory.Measure.map_congr` states that for any two functions `f` and `g` from a type `α` to a type `β`, and a measure `μ` on the measurable space `α`, if `f` and `g` are equal almost everywhere (i.e., they are equal except possibly on a set of measure zero), then the pushforward of the measure `μ` by the function `f` is equal to the pushforward of the measure `μ` by the function `g`. Here, a pushforward of a measure by a function is a new measure that counts how much of the original measure is sent by the function to each part of its range. More concisely: If measurable functions `f` and `g` from a measurable space `(α, Σ, μ)` to another measurable space `(β, τ)` are equal almost everywhere, then the pushforwards `f ♯ μ` and `g ♯ μ` of the measure `μ` under `f` and `g`, respectively, are equal.
`MeasureTheory.Measure.sum_cond` theorem MeasureTheory.Measure.sum_cond : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ ν : MeasureTheory.Measure α), (MeasureTheory.Measure.sum fun b => bif b then μ else ν) = μ + ν This theorem, `MeasureTheory.Measure.sum_cond`, states that for any given measurable space 'α' and any two measures 'μ' and 'ν' on that measurable space, the sum of an indexed family of measures, where each measure is 'μ' if the index is true and 'ν' if the index is false, is equal to the sum of 'μ' and 'ν'. This theorem essentially describes a condition under which the sum of a family of measures simplifies to the sum of two measures. More concisely: For measurable spaces 'α' and measures 'μ' and 'ν' on it, the sum of an indexed family of measures, where each measure is 'μ' for true indices and 'ν' for false indices, equals the sum of 'μ' and 'ν'.
`MeasureTheory.measure_biUnion₀` theorem MeasureTheory.measure_biUnion₀ : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set β} {f : β → Set α}, s.Countable → s.Pairwise (MeasureTheory.AEDisjoint μ on f) → (∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ) → ↑↑μ (⋃ b ∈ s, f b) = ∑' (p : ↑s), ↑↑μ (f ↑p) The theorem `MeasureTheory.measure_biUnion₀` states that for any types `α` and `β`, given a measurable space on `α` (denoted by `m`), a measure `μ` on `α`, a set `s` of elements of type `β`, and a function `f` mapping elements of `β` to sets of `α`, if the set `s` is countable, the measure `μ` is almost everywhere disjoint on the function `f` mapped over the set `s`, and for every element `b` in the set `s`, the set `f(b)` is null measurable with respect to the measure `μ`, then the measure `μ` of the union of all the sets `f(b)`, where `b` is in the set `s`, is equal to the sum of the measures of the sets `f(b)` for all `b` in the set `s`. In mathematical terms, this theorem is saying that if we have a countable set of null measurable sets that are pairwise almost everywhere disjoint, then the measure of the union of these sets is equal to the sum of their individual measures. More concisely: Given a countable family of null measurable, pairwise almost everywhere disjoint sets in a measurable space with respect to a measure, the measure of their union equals the sum of the measures of the individual sets.
`MeasureTheory.Measure.AbsolutelyContinuous.refl` theorem MeasureTheory.Measure.AbsolutelyContinuous.refl : ∀ {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α), μ.AbsolutelyContinuous μ This theorem states that for any measure `μ` in any measurable space `α`, `μ` is absolutely continuous with respect to itself. In other words, if a set `s` is a null set under measure `μ` (i.e., `μ(s) = 0`), then it is also a null set under the same measure `μ` (i.e., `μ(s) = 0`). This is a reflexive property of absolute continuity in the context of measure theory. More concisely: For any measure `μ` in a measurable space, the null sets under `μ` are invariant under `μ`, that is, a set is a null set if and only if its measure under `μ` is zero.
`MeasureTheory.Measure.AbsolutelyContinuous.map` theorem MeasureTheory.Measure.AbsolutelyContinuous.map : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ ν : MeasureTheory.Measure α}, μ.AbsolutelyContinuous ν → ∀ {f : α → β}, Measurable f → (MeasureTheory.Measure.map f μ).AbsolutelyContinuous (MeasureTheory.Measure.map f ν) This theorem states that if a measure `μ` is absolutely continuous with respect to another measure `ν` (in the sense that if `ν(A) = 0` then `μ(A) = 0`), and if a function `f` is measurable (meaning the preimage of every measurable set is also measurable), then the pushforward measure `f` applied to `μ` is also absolutely continuous with respect to the pushforward measure applied to `ν`. In simpler terms, the absolute continuity property is preserved under the mapping of a measurable function. More concisely: If `μ` is absolutely continuous with respect to `ν` and `f` is a measurable function, then the pushforward measure `f`��ˆ(`μ`) is absolutely continuous with respect to the pushforward measure `f`��ˆ(`ν`).
`MeasureTheory.Measure.absolutelyContinuous_rfl` theorem MeasureTheory.Measure.absolutelyContinuous_rfl : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.AbsolutelyContinuous μ This theorem, named `MeasureTheory.Measure.absolutelyContinuous_rfl`, states that for any given type `α`, measurable space `m0` over `α`, and measure `μ` on that measurable space, the measure `μ` is absolutely continuous with respect to itself. In mathematical terms, a measure `μ` is said to be absolutely continuous with respect to another measure if, whenever the second measure assigns zero size to a set, the first measure also assigns zero size to that set. In this case, since we are considering the same measure, it is trivially true. More concisely: A measure is absolutely continuous with respect to itself in Lean 4. (For a given measurable space and measure.)
`MeasureTheory.le_toOuterMeasure_caratheodory` theorem MeasureTheory.le_toOuterMeasure_caratheodory : ∀ {α : Type u_1} [ms : MeasurableSpace α] (μ : MeasureTheory.Measure α), ms ≤ μ.caratheodory This theorem states that for any given measurable space, denoted by 'ms', and a measure 'μ' on a type 'α', the measurable space 'ms' is less than or equal to the Carathéodory-measurable space associated with the outer measure associated with 'μ'. In other words, any set considered measurable in 'ms' is also deemed measurable in the Carathéodory-measurable space of 'μ'. More concisely: For any measurable space (ms, Σ, μ) and its associated Carathéodory-measurable space (msᵢ, Σ₊, μ₊), we have that ms ⇊ msᵢ, where ⇊ denotes inclusion up to a null set.
`MeasureTheory.Measure.AbsolutelyContinuous.mk` theorem MeasureTheory.Measure.AbsolutelyContinuous.mk : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, (∀ ⦃s : Set α⦄, MeasurableSet s → ↑↑ν s = 0 → ↑↑μ s = 0) → μ.AbsolutelyContinuous ν This theorem states that for any type `α` equipped with a `MeasurableSpace` structure, and any two measures `μ` and `ν` on `α`, if for every measurable set `s`, it holds that whenever `ν` assigns `0` to `s`, `μ` also assigns `0` to `s`, then `μ` is absolutely continuous with respect to `ν`. In other words, it provides a condition under which one measure is absolutely continuous with respect to another, which is that the first measure must assign measure zero to any set to which the second measure assigns measure zero. More concisely: If for all measurable sets `s` in a measurable space `α`, `ν(s) = 0` implies `μ(s) = 0`, then measure `μ` is absolutely continuous with respect to measure `ν`.
`MeasureTheory.Measure.QuasiMeasurePreserving.exists_preimage_eq_of_preimage_ae` theorem MeasureTheory.Measure.QuasiMeasurePreserving.exists_preimage_eq_of_preimage_ae : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → α}, MeasureTheory.Measure.QuasiMeasurePreserving f μ μ → MeasurableSet s → μ.ae.EventuallyEq (f ⁻¹' s) s → ∃ t, MeasurableSet t ∧ μ.ae.EventuallyEq t s ∧ f ⁻¹' t = t This theorem states that for any type `α` with a measurable space `m0` and a measure `μ`, given a set `s` in `α` and a function `f` from `α` to `α` that is quasi-measure-preserving, if the preimage of `s` under `f` is almost everywhere equal to `s`, then there exists a set `t` that is a measurable set, almost everywhere equal to `s`, and invariant under `f`, meaning the preimage of `t` under `f` is `t` itself. More concisely: Given a measurable space `(α, m0)`, measure `μ`, quasi-measure-preserving function `f: α → α`, and set `s ⊆ α` such that `s` and `f⁁⁻¹(s)` differ only on a set of measure zero, there exists a measurable set `t ⊆ α` equal to `s` almost everywhere and invariant under `f`.
`MeasureTheory.NullMeasurableSet.preimage` theorem MeasureTheory.NullMeasurableSet.preimage : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → β} {t : Set β}, MeasureTheory.NullMeasurableSet t ν → MeasureTheory.Measure.QuasiMeasurePreserving f μ ν → MeasureTheory.NullMeasurableSet (f ⁻¹' t) μ In terms of mathematics, the theorem states that for any given types `α` and `β` with measurable spaces, a measure `μ` on `α`, a measure `ν` on `β`, and a function `f` mapping `α` to `β`, if a set `t` of type `β` is a null measurable set with respect to the measure `ν`, and if `f` is a quasi measure preserving function from `μ` to `ν`, then the preimage of the set `t` under the function `f` is also a null measurable set with respect to the measure `μ`. In simpler words, it means the pre-image of a null measurable set under a measure-preserving transformation is also a null measurable set. More concisely: If `μ` is a measure on `α`, `ν` is a measure on `β`, `f` is a quasi-measure preserving function from `α` to `β`, and `t` is a null measurable set in `β` with respect to `ν`, then `f⁻¹(t)` is a null measurable set in `α` with respect to `μ`.
`MeasureTheory.Measure.comap_apply₀` theorem MeasureTheory.Measure.comap_apply₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace β] {s : Set α} [inst_1 : MeasurableSpace α] (f : α → β) (μ : MeasureTheory.Measure β), Function.Injective f → (∀ (s : Set α), MeasurableSet s → MeasureTheory.NullMeasurableSet (f '' s) μ) → MeasureTheory.NullMeasurableSet s (MeasureTheory.Measure.comap f μ) → ↑↑(MeasureTheory.Measure.comap f μ) s = ↑↑μ (f '' s) This theorem states that for any types `α` and `β` equipped with measurable spaces, a set `s` of type `α`, a function `f` from `α` to `β`, and a measure `μ` on `β`, if the function `f` is injective, and every measurable set in `α` is also null measurable when its image under `f` is considered in `β` with respect to measure `μ`, then if the set `s` is null measurable in the measure space obtained by pulling back `μ` along `f`, the measure of `s` in the pulled back measure equals the measure of the image of `s` under `f` in `β` with respect to `μ`. In other words, pullback preserves the measure of null measurable sets under certain conditions. More concisely: If `f: α → β` is an injective function between measurable spaces `(α, Σα, μα)` and `(β, Σβ, μβ)`, and every null measurable set in `α` maps to a null measurable set in `β`, then the measure of a null measurable set `s` in `α` with respect to the pulled back measure equals the measure of `f(s)` in `β`.
`MeasureTheory.Measure.map_of_not_aemeasurable` theorem MeasureTheory.Measure.map_of_not_aemeasurable : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β} {μ : MeasureTheory.Measure α}, ¬AEMeasurable f μ → MeasureTheory.Measure.map f μ = 0 The theorem `MeasureTheory.Measure.map_of_not_aemeasurable` states that for any two types `α` and `β`, where `α` is equipped with a measurable space `m0` and `β` is equipped with a measurable space, and for any function `f` from `α` to `β`, and any measure `μ` on `α`, if `f` is not almost everywhere measurable with respect to the measure `μ`, then the pushforward of the measure `μ` by the function `f` is equal to zero. In other words, in measure theory, if a function does not coincide almost everywhere with a measurable function, then the measure transformed by this function yields zero. More concisely: If a function between measurable spaces is not almost everywhere measurable with respect to a given measure, then the pushforward measure is zero.
`MeasureTheory.Measure.sum_fintype` theorem MeasureTheory.Measure.sum_fintype : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} [inst : Fintype ι] (μ : ι → MeasureTheory.Measure α), MeasureTheory.Measure.sum μ = Finset.univ.sum fun i => μ i This theorem, `MeasureTheory.Measure.sum_fintype`, is about the sum of measures over a finite index set. It says that for any measurable space `α`, any type `ι` that has a finite number of elements (`Fintype ι`), and a function `μ` that assigns to each element of `ι` a measure on `α`, the sum of these measures (`MeasureTheory.Measure.sum μ`) is equal to the sum of the measures for each element in the universal finite set (`Finset.univ`) of `ι` (i.e., `Finset.sum Finset.univ fun i => μ i`). In other words, we can compute the sum of an indexed family of measures by simply adding up the measures for each individual index in the family. More concisely: For any measurable space `α`, given a finite index set `ι` and a measurable function `μ : ι → α → ℝ` assigning a measure to each element-wise pair in `ι × α`, the sum of these measures equals the sum of measures for every index in `ι` over the universal set of `ι`: `MeasureTheory.Measure.sum μ = Finset.sum Finset.univ fun i => μ i`.
`MeasureTheory.measure_union` theorem MeasureTheory.measure_union : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α}, Disjoint s₁ s₂ → MeasurableSet s₂ → ↑↑μ (s₁ ∪ s₂) = ↑↑μ s₁ + ↑↑μ s₂ This theorem states that for any two sets `s₁` and `s₂` in a measurable space `α` with a measure `μ`, if `s₁` and `s₂` are disjoint and `s₂` is a measurable set, then the measure of the union of `s₁` and `s₂` is equal to the sum of the measures of `s₁` and `s₂`. In other words, the measure of the union of two disjoint measurable sets is the sum of their individual measures, which is a fundamental property in measure theory. More concisely: Given measurable sets `s₁` and `s₂` in a measurable space `α` with measure `μ`, if `s₁ ∩ s₂ = ∅` then `μ(s₁ ∪ s₂) = μ(s₁) + μ(s₂)`.
`MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint₀` theorem MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint₀ : ∀ {α : Type u_1} {ι : Type u_8} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {As : ι → Set α}, (∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ) → Pairwise (MeasureTheory.AEDisjoint μ on As) → ∑' (i : ι), ↑↑μ (As i) ≤ ↑↑μ (⋃ i, As i) The theorem `MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint₀` states that for any measurable space `α` and any index type `ι`, given a measure `μ` on `α` and a function `As` that maps from `ι` to the set of `α`, if every set `As i` is a null-measurable set with respect to the measure `μ`, and if the sets `As i` are pairwise almost everywhere disjoint (i.e., the measure of the intersection of any two distinct sets is zero), then the sum of the measures of all sets `As i` is less than or equal to the measure of the union of all such sets. This holds even for uncountably many sets. More concisely: For any measurable space, measure, and index type, if the indexed family of null-measurable, pairwise almost everywhere disjoint sets carries a measure that sums to the measure of their union, then the measure of their union is finite.
`MeasureTheory.measure_biUnion_finset` theorem MeasureTheory.measure_biUnion_finset : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Finset ι} {f : ι → Set α}, (↑s).PairwiseDisjoint f → (∀ b ∈ s, MeasurableSet (f b)) → ↑↑μ (⋃ b ∈ s, f b) = s.sum fun p => ↑↑μ (f p) This theorem, named `MeasureTheory.measure_biUnion_finset`, states that for any measurable space `α`, index type `ι`, a measure space defined on `α` by `μ`, a finite set `s` of the index type `ι`, and a function `f` that maps index to the set `α`, if the image of any two distinct elements in the set `s` under `f` are disjoint (i.e., `Set.PairwiseDisjoint` holds for `s` and `f`), and the set `f b` is measurable for every `b` in `s`, then the measure of the union of `f b` for every `b` in `s` (expressed as `↑↑μ (⋃ b ∈ s, f b)`) equals the sum (expressed as `Finset.sum s fun p => ↑↑μ (f p)`) of the measures of `f p` for every `p` in `s`. To put it simply, this theorem states that if you have a set of disjoint, measurable subsets of a measurable space, the measure of the union of these subsets is the sum of their individual measures. More concisely: If `α` is a measurable space, `μ` is a measure on `α`, `ι` is a finite index type, `s` is a finite set of `ι`, `f : ι → α` is a function such that `Set.PairwiseDisjoint s f` and `μ (f i)` is measurable for each `i` in `s`, then `μ (⋃ i ∈ s, f i) = Finset.sum s fun i => μ (f i)`.
`MeasureTheory.Measure.measure_univ_ne_zero` theorem MeasureTheory.Measure.measure_univ_ne_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, ↑↑μ Set.univ ≠ 0 ↔ μ ≠ 0 This theorem states that for any type `α`, any defined measurable space on `α` denoted by `m0`, and any measure `μ` on this measurable space, the measure of the universal set (which includes all elements of `α`) being non-zero is equivalent to the measure `μ` itself being non-zero. In other words, if the measure of every possible subset of `α` is not zero, then the measure itself cannot be zero, and vice versa. More concisely: If a measure `μ` on a measurable space `(α, m0)` is non-zero if and only if the measure of the universal set is non-zero.
`MeasureTheory.Measure.add_apply` theorem MeasureTheory.Measure.add_apply : ∀ {α : Type u_1} {_m : MeasurableSpace α} (μ₁ μ₂ : MeasureTheory.Measure α) (s : Set α), ↑↑(μ₁ + μ₂) s = ↑↑μ₁ s + ↑↑μ₂ s This theorem, `MeasureTheory.Measure.add_apply`, states that for any given type `α`, any measurable space over `α` (denoted as `_m`), two measures `μ₁` and `μ₂` over `α`, and a set `s` of `α`, the measure of the set `s` under the sum of the two measures `μ₁ + μ₂` is equal to the sum of the measures of the set `s` under `μ₁` and `μ₂` individually. In other words, it defines how addition of two measures acts on a set: the measure of the set with respect to the added measures is just the sum of the measures of the set with respect to each measure individually. More concisely: For any measurable spaces `(_m : MeasurableSpace α)`, measures `(μ₁ μ₂ : Measure α)`, and set `(s : Set α)`, the measure of `s` under the sum `(μ₁ + μ₂)` equals the sum of the measures of `s` under `μ₁` and `μ₂`.
`MeasureTheory.Measure.QuasiMeasurePreserving.comp` theorem MeasureTheory.Measure.QuasiMeasurePreserving.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {μc : MeasureTheory.Measure γ} {g : β → γ} {f : α → β}, MeasureTheory.Measure.QuasiMeasurePreserving g μb μc → MeasureTheory.Measure.QuasiMeasurePreserving f μa μb → MeasureTheory.Measure.QuasiMeasurePreserving (g ∘ f) μa μc This theorem states that if we have three types α, β, and γ with corresponding measurable spaces and measures μa, μb, and μc, and two functions f: α → β and g: β → γ, then if g is quasi-measure preserving between μb and μc, and f is quasi-measure preserving between μa and μb, the composition function (g ∘ f) is quasi-measure preserving between μa and μc. In other words, the property of being quasi-measure preserving is preserved under function composition. More concisely: If functions f: α → β and g: β → γ are quasi-measure preserving between measurable spaces with measures μa, μb, and μc, respectively, then the composition function g ∘ f is quasi-measure preserving between μa and μc.
`MeasurableEquiv.map_symm_map` theorem MeasurableEquiv.map_symm_map : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α} (e : α ≃ᵐ β), MeasureTheory.Measure.map (⇑e.symm) (MeasureTheory.Measure.map (⇑e) μ) = μ This theorem states that, for any measurable spaces `α` and `β`, and a measure `μ` on `α`, if we have a measurable equivalence `e` between `α` and `β`, then mapping the measure `μ` from `α` to `β` using `e`, and then mapping it back to `α` using the inverse of `e`, we get back the original measure `μ`. This is a kind of "undoing" property, showing that the process of mapping measures under a measurable equivalence and its inverse is reversible. More concisely: For measurable spaces `α`, `β`, a measure `μ` on `α`, and a measurable equivalence `e` between `α` and `β`, the pushforward and pullback measures of `μ` under `e` and its inverse respectively are equal: `μ` = `e.forwardMeasure` `∘` `e.inverse.measure` = `e.inverse.measure` `∘` `μ`.
`MeasureTheory.Measure.map_smul` theorem MeasureTheory.Measure.map_smul : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] (c : ENNReal) (μ : MeasureTheory.Measure α) (f : α → β), MeasureTheory.Measure.map f (c • μ) = c • MeasureTheory.Measure.map f μ The theorem `MeasureTheory.Measure.map_smul` states that for any types `α` and `β`, where `α` has a measurable space structure `m0` and `β` has a measurable space instance, and given an extended nonnegative real number `c`, a measure `μ` on `α`, and a function `f` from `α` to `β`, the measure of the image of the function `f` on the measure `μ` scaled by `c` is equal to the measure of the image of the function `f` on `μ` scaled by `c`. In simpler terms, it means that scaling a measure and then applying a function is the same as applying the function and then scaling the measure. More concisely: For measurable spaces `(α, m0)` and `(β)`, extended nonnegative real number `c`, measure `μ` on `α`, and function `f` from `α` to `β`, `μ(f "''" (c μ)) = c * μ(f "''" μ)`.*
`AEMeasurable.nullMeasurable` theorem AEMeasurable.nullMeasurable : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : α → β}, AEMeasurable f μ → MeasureTheory.NullMeasurable f μ This theorem states that for any types `α` and `β`, given a measurable space `α` and a measure `μ` on that space, any function `f` from `α` to `β` that is almost everywhere measurable is also null measurable. In other words, if a function coincides almost everywhere with a measurable function (it is almost everywhere measurable), then the preimage of a measurable set under this function is a null measurable set. More concisely: If `f: α → β` is almost everywhere measurable and `μ` is a measure on `α`, then for any measurable set `A ∈ σ(`α`)`, the preimage `f⁻¹(A) ∈ σ(`β`), and `μ(A) = 0` implies `μ(f⁻¹(A)) = 0`.
`MeasureTheory.Measure.map_apply` theorem MeasureTheory.Measure.map_apply : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : α → β}, Measurable f → ∀ {s : Set β}, MeasurableSet s → ↑↑(MeasureTheory.Measure.map f μ) s = ↑↑μ (f ⁻¹' s) This theorem, `MeasureTheory.Measure.map_apply`, states that for any two types `α` and `β`, if `f` is a function from `α` to `β` that is measurable and `s` is a measurable set in the `β` space, then the measure of `s` under the pushforward measure created by `f` is equal to the measure of the preimage of `s` under `f` in the `α` space. In other words, it is a property about the pushforward of measures: if you pushforward a measure using a measurable function, then measuring a set under this new measure is the same as measuring the preimage of the set under the original measure. More concisely: For measurable functions between measurable spaces, the pushforward measure of a set is equal to the measure of its preimage.
`MeasureTheory.Measure.measure_toMeasurable_inter` theorem MeasureTheory.Measure.measure_toMeasurable_inter : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, MeasurableSet s → ↑↑μ t ≠ ⊤ → ↑↑μ (MeasureTheory.toMeasurable μ t ∩ s) = ↑↑μ (t ∩ s) This theorem is titled "MeasureTheory.Measure.measure_toMeasurable_inter". It says that for any type `α`, given a measurable space `m0` on `α`, a measure `μ` on `α`, and two sets `s` and `t` of type `α`, if `s` is a measurable set and the measure of `t` is finite (i.e., not infinity), then the measure of the intersection of the measurable superset `toMeasurable μ t` of `t` and `s` is equal to the measure of the intersection of `t` and `s`. In other words, `μ (toMeasurable μ t ∩ s) = μ (t ∩ s)`. This conclusion also holds when the measure of `t` is s-finite, such as when it is σ-finite, as stated in the theorem `measure_toMeasurable_inter_of_sFinite`. More concisely: For any measurable space and measure, if a measurable set intersects a finite or s-finite measurable set, then their intersection's measure equals the measure of their intersection in the original sets.
`MeasurableEmbedding.map_apply` theorem MeasurableEmbedding.map_apply : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β}, MeasurableEmbedding f → ∀ (μ : MeasureTheory.Measure α) (s : Set β), ↑↑(MeasureTheory.Measure.map f μ) s = ↑↑μ (f ⁻¹' s) This theorem, `MeasurableEmbedding.map_apply`, states that for any two types `α` and `β`, any measurable spaces `m0` and `m1` over these types, a function `f` from `α` to `β`, and a `MeasurableEmbedding` of `f`, then for any measure `μ` over `α` and any set `s` of type `β`, the measure of the image of `f` applied to `μ` and `s` is equal to the measure of the pre-image of `s` under `f` with respect to `μ`. In simpler terms, it says that under a measurable embedding, the measure of a set and the measure of its pre-image are equal. More concisely: For any measurable spaces `(α, m0)` and `(β, m1)`, a measurable embedding of a function `f: α → β`, and a set `s ∈ β` with measure `μ(s) < ∞`, we have `μ(f⁻¹(s)) = m1(s)`.
`MeasureTheory.Measure.ae_le_iff_absolutelyContinuous` theorem MeasureTheory.Measure.ae_le_iff_absolutelyContinuous : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ.ae ≤ ν.ae ↔ μ.AbsolutelyContinuous ν The theorem `MeasureTheory.Measure.ae_le_iff_absolutelyContinuous` states that for any given type `α`, measurable space `m0`, and measures `μ` and `ν` on `α`, the measure `μ` is almost everywhere less than or equal to the measure `ν` if and only if `μ` is absolutely continuous with respect to `ν`. In other words, `μ` is dominated by `ν` (meaning if `ν(A) = 0` then `μ(A) = 0`) if and only if for almost every element under `μ`, it is also in `ν`. More concisely: A measurable set function $\mu$ is almost everywhere less than or equal to another measurable set function $\nu$ on the same measurable space if and only if $\mu$ is absolutely continuous with respect to $\nu$.
`MeasureTheory.Measure.QuasiMeasurePreserving.id` theorem MeasureTheory.Measure.QuasiMeasurePreserving.id : ∀ {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α), MeasureTheory.Measure.QuasiMeasurePreserving id μ μ This theorem states that for any given type `α` and a measurable space `_m0` of type `α`, the identity function is a quasi measure-preserving function for any measure `μ` on that measurable space. In mathematical terms, if we have a measure space `(α, _m0, μ)`, the identity map on `α` is always quasi measure-preserving with respect to the measure `μ`. More concisely: For any measurable space `(α, μ\_m0)` and measure `μ`, the identity function on `α` is a quasi measure-preserving function with respect to `μ`.
`MeasureTheory.measure_diff_null'` theorem MeasureTheory.measure_diff_null' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α}, ↑↑μ (s₁ ∩ s₂) = 0 → ↑↑μ (s₁ \ s₂) = ↑↑μ s₁ This theorem, named `MeasureTheory.measure_diff_null'`, is a statement about measure theory. It holds for any type `α`, a measurable space `m` of type `α`, a measure `μ` on this measurable space, and two sets `s₁` and `s₂` of elements of type `α`. The theorem states that if the measure of the intersection of `s₁` and `s₂` is 0, then the measure of the set difference "s₁ minus s₂" is equal to the measure of `s₁`. In mathematical terms, if μ(s₁ ∩ s₂) = 0, then μ(s₁ \ s₂) = μ(s₁), where μ represents the measure, ∩ represents intersection of sets, and \ represents set difference. More concisely: If two sets in a measurable space have zero intersection measure, then their set difference is measurably equal to the original set.
`MeasureTheory.Measure.le_sum` theorem MeasureTheory.Measure.le_sum : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} (μ : ι → MeasureTheory.Measure α) (i : ι), μ i ≤ MeasureTheory.Measure.sum μ This theorem states that for any type `α` and an index type `ι`, given a measurable space `m0` over `α`, and a function `μ` mapping each index `ι` to a measure on `α`, the measure for any particular index `i` is less than or equal to the sum of the measures for all indices. In other words, if you have a collection of measures indexed by `ι`, the measure of any one element is no greater than the sum of all measures in the collection. More concisely: For any measurable space `(α, Σ, m0)` and a family `(μ\_i : Σ -> ℝ)_i indexed by an index type `ι`, we have `μ_i ∣ᵢ α ∩ A ≤ ∑_j μ_j ∣ᵢ α ∩ A` for all `A ∈ Σ` and `i, j : ι`. (Here, `∣ᵢ` denotes the restriction of the measure `m0` to the sub-σ-algebra generated by `{A : Σ \| A ∩ supp μ_i ≠ ∅}`, where `supp μ_i` is the support of `μ_i`.)
`MeasureTheory.measure_diff` theorem MeasureTheory.measure_diff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α}, s₂ ⊆ s₁ → MeasurableSet s₂ → ↑↑μ s₂ ≠ ⊤ → ↑↑μ (s₁ \ s₂) = ↑↑μ s₁ - ↑↑μ s₂ The theorem `MeasureTheory.measure_diff` states that for any type `α`, given a measurable space `m` on `α`, a measure `μ` for this space, and two sets `s₁` and `s₂` of type `α`, if `s₂` is a subset of `s₁` and `s₂` is a measurable set, and the measure of `s₂` is not infinity, then the measure of the difference of the sets `s₁` and `s₂` (that is, the measure of the set of elements in `s₁` but not in `s₂`) is equal to the difference of the measures of `s₁` and `s₂`. In other words, the measure of the set elements in `s₁` excluding those in `s₂` is equal to the measure of `s₁` minus the measure of `s₂`. More concisely: If `μ` is a finite measure on the measurable space `(α, m)` and `s₁` is a set containing `s₂` with finite measure, then `μ(s₁ \ s₂) = μ(s₁) - μ(s₂)`.
`MeasureTheory.Ioo_ae_eq_Ioc'` theorem MeasureTheory.Ioo_ae_eq_Ioc' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PartialOrder α] {a b : α}, ↑↑μ {b} = 0 → μ.ae.EventuallyEq (Set.Ioo a b) (Set.Ioc a b) The theorem `MeasureTheory.Ioo_ae_eq_Ioc'` states that for any type `α` with a `PartialOrder`, a `MeasurableSpace` structure `m0`, a measure `μ`, and two elements `a` and `b` of `α`, if the measure of the singleton set `{b}` is zero, then the left-open right-open interval `(a, b)` is almost everywhere equal (in the measure theoretic sense) to the left-open right-closed interval `(a, b]` under the measure `μ`. In other words, the two intervals are identical except on a set of measure zero. More concisely: If `μ(`{`b`}`) = 0` in a measure space `(α, m0, μ)` with a `PartialOrder` on `α`, then `(a, b)` and `(a, b]` are almost equal in measure.
`MeasureTheory.Measure.le_iff` theorem MeasureTheory.Measure.le_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ μ₂ : MeasureTheory.Measure α}, μ₁ ≤ μ₂ ↔ ∀ (s : Set α), MeasurableSet s → ↑↑μ₁ s ≤ ↑↑μ₂ s This theorem, `MeasureTheory.Measure.le_iff`, states that for any type `α` equipped with a measurable space structure `m0` and any two measures `μ₁` and `μ₂` on `α`, the measure `μ₁` is less than or equal to the measure `μ₂` if and only if for all sets `s` of type `α` that are measurable, the measure of `s` under `μ₁` is less than or equal to the measure of `s` under `μ₂`. In other words, one measure is considered lesser or equal if it assigns a lesser or equal measure to every measurable set when compared with another measure. More concisely: For any measurable spaces (α, m0) and measures μ₁, μ₂ on α, μ₁ ≤ μ₂ if and only if μ₁(s) ≤ μ₂(s) for all measurable sets s ∈ α.
`MeasureTheory.tendsto_measure_iInter` theorem MeasureTheory.tendsto_measure_iInter : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Countable ι] [inst : Preorder ι] [inst_1 : IsDirected ι fun x x_1 => x ≤ x_1] {s : ι → Set α}, (∀ (n : ι), MeasurableSet (s n)) → Antitone s → (∃ i, ↑↑μ (s i) ≠ ⊤) → Filter.Tendsto (↑↑μ ∘ s) Filter.atTop (nhds (↑↑μ (⋂ n, s n))) This theorem, named `MeasureTheory.tendsto_measure_iInter`, states that in a measure space `α` with a measure `μ`, for a sequence of measurable sets indexed by a countable, directed and preordered set `ι` that is decreasing (antitone), the measure of the intersection of the sequence of sets is the limit of the measures of the sets. More formally, if each set `s n` in the sequence is measurable, the sequence is antitone, and there exists an index `i` such that the measure of `s i` is not infinity, then the measure of the intersection of all `s n` as `n` tends to infinity (expressed as `⋂ n, s n`), is the limit of the measures of the `s n` as `n` tends to infinity. This concept is often referred to as "continuity from above". More concisely: If `{Sn : ℕ → ℵ0 → Set α}`, `ι` is a countable, directed and preordered set, `μ` is a measure on `α`, and for each `n`, `Sn i` is measurable and `Sn j ⊇ Sn i` for `i ≤ j`, then `μ(⋂n, Sn) = ∏n, μ(Sn)`. (Note: `∏` denotes the product of a sequence of measurable sets.) This statement asserts that the measure of the intersection of a decreasing sequence of measurable sets, indexed by a countable and directed set, is the limit of their measures, under certain conditions.
`MeasureTheory.Measure.smul_toOuterMeasure` theorem MeasureTheory.Measure.smul_toOuterMeasure : ∀ {α : Type u_1} {R : Type u_6} [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal] {_m : MeasurableSpace α} (c : R) (μ : MeasureTheory.Measure α), ↑(c • μ) = c • ↑μ This theorem states that for any given type `α` and `R`, given that `R` is a type that allows scalar multiplication (`SMul`) with the type `ENNReal` (extended nonnegative real numbers), and `ENNReal` forms a scalar tower over `R` and `ENNReal`, for any measurable space `_m` of type `α`, scalar multiplication of a measure `μ` from the measurable space by a scalar `c` from `R` is equal to the scalar multiplication of the embedding of `μ` by `c`. In other words, it means that in the context of measures, scalar multiplication commutes with the embedding operation. More concisely: For any measurable space `(α, μ)`, `ENNReal`-valued measure `μ`, and `c` in an `ENNReal`-scalable type `R`, the scalar multiplication of `μ` by `c` is equal to the scalar multiplication of the embedding of `μ` by `c`.
`MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint` theorem MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint : ∀ {α : Type u_1} {ι : Type u_8} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {As : ι → Set α}, (∀ (i : ι), MeasurableSet (As i)) → Pairwise (Disjoint on As) → ∑' (i : ι), ↑↑μ (As i) ≤ ↑↑μ (⋃ i, As i) This theorem, `MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint`, states that for any type `α` with a measurable space structure, any index type `ι`, and any measure `μ` on `α`, given a sequence `As : ι → Set α` of measurable sets such that these sets are pairwise disjoint (meaning for any two distinct indices, the corresponding sets are disjoint), the total measure (or sum of measures) of these sets is less than or equal to the measure of the union of these sets. In other words, it asserts that the measure of a (possibly uncountable) disjoint union of measurable sets is at least the sum of the measures of the individual sets. More concisely: For any measurable space `(α, Σ, μ)`, any index type `ι`, and any sequence `A_i (i ∈ ι)` of pairwise disjoint measurable sets, we have `μ (⋃ i ∈ ι A_i) ≤ ∑ i ∈ ι mu A_i`.
`MeasureTheory.Measure.absolutelyContinuous_of_le` theorem MeasureTheory.Measure.absolutelyContinuous_of_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ ≤ ν → μ.AbsolutelyContinuous ν := by sorry This theorem states that, for any type `α` and any `MeasurableSpace` of `α`, and for any two measures `μ` and `ν` over `α`, if `μ` is less than or equal to `ν`, then `μ` is absolutely continuous with respect to `ν`. Here, being absolutely continuous means that for any set `s` of `α`, if `ν` measures `s` as having measure zero, then `μ` also measures `s` as having measure zero. More concisely: If `μ` is a measure that is less than or equal to `ν` for any two measures `μ` and `ν` over a `MeasurableSpace` `α`, then `μ` is absolutely continuous with respect to `ν`.
`MeasureTheory.Measure.AbsolutelyContinuous.ae_le` theorem MeasureTheory.Measure.AbsolutelyContinuous.ae_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ.AbsolutelyContinuous ν → μ.ae ≤ ν.ae This theorem states that for any type `α` with a `MeasurableSpace` `m0`, and any two measures `μ` and `ν` on that space, if `μ` is absolutely continuous with respect to `ν` (meaning that whenever `ν` of a set `A` is zero, then `μ` of `A` is also zero), then the "almost everywhere" filter of `μ` is less than or equal to the "almost everywhere" filter of `ν`. In terms of measure theory, this suggests that if one measure is absolutely continuous with respect to another, then almost all points that are measurable according to the first measure are also measurable according to the second. More concisely: If `μ` is absolutely continuous with respect to `ν` for measurable spaces `(α, m0)` and measures `μ` and `ν`, then the `μ`-almost everywhere filter is included in the `ν`-almost everywhere filter.
`MeasureTheory.Measure.ae_mono'` theorem MeasureTheory.Measure.ae_mono' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ.AbsolutelyContinuous ν → μ.ae ≤ ν.ae This theorem, `MeasureTheory.Measure.ae_mono'`, states that for any type `α` and any measurable space `α` has, if measure `μ` is absolutely continuous with respect to measure `ν`, then almost every value of `μ` is less than or equal to almost every value of `ν`. This is an alias for the reverse direction of the theorem `MeasureTheory.Measure.ae_le_iff_absolutelyContinuous`. More concisely: If measure `μ` is absolutely continuous with respect to measure `ν` on measurable space `α`, then almost every `μ`-measurable set has smaller `ν` measure than almost every set with the same `μ` measure.
`MeasureTheory.Measure.le_add_left` theorem MeasureTheory.Measure.le_add_left : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν ν' : MeasureTheory.Measure α}, μ ≤ ν → μ ≤ ν' + ν This theorem states that for any given type `α`, measurable space `m0`, and measures `μ`, `ν`, and `ν'`, if `μ` is less than or equal to `ν`, then `μ` is also less than or equal to the sum of `ν'` and `ν`. This is a statement in the context of measure theory. More concisely: For any measurable spaces `(α, m0)` and measures `μ ≤ ν`, `μ ≤ ν' + ν`.
`MeasureTheory.Measure.map_zero` theorem MeasureTheory.Measure.map_zero : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] (f : α → β), MeasureTheory.Measure.map f 0 = 0 This theorem states that for any function `f` from a measurable space `α` to another measurable space `β`, the pushforward of the zero measure (denoted as `0`) under `f` is always the zero measure. The pushforward of a measure gives a new measure on `β`, defined by applying the function `f` to the elements of `α`. However, when the original measure is `0`, the pushforward is also `0` regardless of the function `f`. More concisely: For any measurable function `f` from a measurable space `α` to a measurable space `β`, the pushforward of the zero measure on `α` is the zero measure on `β`.
`Mathlib.MeasureTheory.Measure.MeasureSpace._auxLemma.10` theorem Mathlib.MeasureTheory.Measure.MeasureSpace._auxLemma.10 : ∀ {α : Type u} {ι : Sort v} {x : α} {s : ι → Set α}, (x ∈ ⋃ i, s i) = ∃ i, x ∈ s i This theorem states that for any type `α`, any sort `ι`, any element `x` of type `α`, and any function `s` from `ι` to a set of `α`, `x` is in the union over `ι` of the sets `s i` if and only if there exists an `i` in `ι` such that `x` is in `s i`. In other words, an element belongs to the union of a collection of sets if and only if it belongs to at least one of the sets in that collection. This theorem is a fundamental principle of set theory, encapsulated within the context of measure theory in Lean. More concisely: For any type `α`, sort `ι`, element `x` of type `α`, and function `s` from `ι` to sets of `α`, `x` is in the set `⋃ i, s i` if and only if there exists an `i` in `ι` such that `x` is in `s i`.
`MeasureTheory.Measure.AbsolutelyContinuous.trans` theorem MeasureTheory.Measure.AbsolutelyContinuous.trans : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ μ₂ μ₃ : MeasureTheory.Measure α}, μ₁.AbsolutelyContinuous μ₂ → μ₂.AbsolutelyContinuous μ₃ → μ₁.AbsolutelyContinuous μ₃ The theorem `MeasureTheory.Measure.AbsolutelyContinuous.trans` states that the property of being absolutely continuous is transitive. In more detail, for any measurable space `α` and any three measures `μ₁`, `μ₂`, and `μ₃` defined on this space, if `μ₁` is absolutely continuous with respect to `μ₂`, and `μ₂` is absolutely continuous with respect to `μ₃`, then `μ₁` is also absolutely continuous with respect to `μ₃`. In mathematical terms, if for any set `s` such that `μ₃(s) = 0` implies `μ₂(s) = 0` and `μ₂(s) = 0` implies `μ₁(s) = 0`, then `μ₃(s) = 0` directly implies `μ₁(s) = 0`. This establishes the transitivity of absolute continuity for measures. More concisely: If measures `μ₁` is absolutely continuous with respect to `μ₂`, and `μ₂` is absolutely continuous with respect to `μ₃`, then `μ₁` is absolutely continuous with respect to `μ₃`.
`Mathlib.MeasureTheory.Measure.MeasureSpace._auxLemma.27` theorem Mathlib.MeasureTheory.Measure.MeasureSpace._auxLemma.27 : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, (↑↑μ Set.univ = 0) = (μ = 0) This theorem states that for any type `α`, any measurable space `m0` on `α`, and any measure `μ` on this measurable space, the measure of the universal set (i.e., the set containing all elements of the type `α`) being equal to zero is equivalent to the measure itself being zero. In other words, it says that if the total measure of all possible elements is zero, then the only possible measure is the zero measure. More concisely: For any measurable space `(α, m0)` and measure `μ` on `α`, `measure μ (univ α) = 0` if and only if `μ = 0`.
`Eq.absolutelyContinuous` theorem Eq.absolutelyContinuous : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ = ν → μ.AbsolutelyContinuous ν := by sorry The theorem `Eq.absolutelyContinuous` states that for any type `α`, measurable space `m0`, and measures `μ` and `ν`, if `μ` equals `ν`, then `μ` is absolutely continuous with respect to `ν`. In other words, if two measures are equal, then one measure is dominated by the other, meaning that if the second measure assigns zero to a set `s`, then the first measure also assigns zero to that set `s`. More concisely: If two measures are equal, then the larger measure is absolutely continuous with respect to the smaller measure.
`MeasureTheory.ae_eq_of_subset_of_measure_ge` theorem MeasureTheory.ae_eq_of_subset_of_measure_ge : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, s ⊆ t → ↑↑μ t ≤ ↑↑μ s → MeasurableSet s → ↑↑μ t ≠ ⊤ → μ.ae.EventuallyEq s t This theorem, `MeasureTheory.ae_eq_of_subset_of_measure_ge`, states that for any type `α` equipped with a measure space `m` and a measure `μ`, and for any two sets `s` and `t` of `α`, if `s` is a subset of `t`, the measure of `t` is less than or equal to the measure of `s`, `s` is a measurable set, and the measure of `t` is not infinite, then `s` is almost everywhere equal to `t` under the measure `μ`. In other words, the sets `s` and `t` are the same except for a set of measure zero. More concisely: If `s` is a measurable subset of `t` with finite measure in a measure space `(α, m, μ)` such that `μ(t) ≤ μ(s)`, then `s` and `t` are almost everywhere equal.
`MeasureTheory.exists_nonempty_inter_of_measure_univ_lt_sum_measure` theorem MeasureTheory.exists_nonempty_inter_of_measure_univ_lt_sum_measure : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) {s : Finset ι} {t : ι → Set α}, (∀ i ∈ s, MeasurableSet (t i)) → (↑↑μ Set.univ < s.sum fun i => ↑↑μ (t i)) → ∃ i ∈ s, ∃ j ∈ s, ∃ (_ : i ≠ j), (t i ∩ t j).Nonempty This theorem is a version of the Pigeonhole Principle for measure spaces. It states that if you have a finite set `s`, and a collection of measurable sets `t i` indexed by elements in `s`, in a measurable space `α` with measure `μ`, and if the total measure of the sets `t i` (the sum of `μ (t i)` for all `i` in `s`) is greater than the total measure of the entire space (`μ univ`), then there must exist two different elements `i` and `j` in `s` such that the intersection of `t i` and `t j` is not empty. In other words, if you have more "pigeons" (total measure of `t i`) than "holes" (total measure of the universe), then some "pigeons" must share a "hole" (the sets `t i` overlap). More concisely: If `μ (∑i in s) t i > μ univ` in a measure space `(α, Σ, μ)`, then there exist distinct `i, j` in `s` such that `t i ∩ t j ≠ ∅`.
`MeasureTheory.Measure.coe_zero` theorem MeasureTheory.Measure.coe_zero : ∀ {α : Type u_1} {_m : MeasurableSpace α}, ↑↑0 = 0 This theorem states that for any type `α` and any measurable space `_m` over this type, the measure of the empty set (represented by `0` in Lean) is `0`. In more mathematical terms, given any measurable space, the measure of the empty set is always zero. More concisely: For any measurable space, the measure of the empty set is 0.
`MeasureTheory.Measure.map_def` theorem MeasureTheory.Measure.map_def : ∀ {α : Type u_8} {β : Type u_9} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace α] (f : α → β) (μ : MeasureTheory.Measure α), MeasureTheory.Measure.map f μ = if hf : AEMeasurable f μ then (MeasureTheory.Measure.mapₗ (AEMeasurable.mk f hf)) μ else 0 The theorem `MeasureTheory.Measure.map_def` states that for any types `α` and `β` each equipped with a `MeasurableSpace` structure, and any function `f` from `α` to `β`, the pushforward of a measure `μ` under `f` is defined as follows: If `f` is almost everywhere measurable with respect to `μ`, then the pushforward is the same as applying the linear map version of the pushforward (`MeasureTheory.Measure.mapₗ`) to the measurable function that is equivalent to `f` almost everywhere. If `f` is not almost everywhere measurable, then the pushforward of `μ` is simply defined to be `0`. More concisely: If `f` is a almost everywhere measurable function between measurable spaces `(α, Σα, μ)` and `(β, Σβ, ν)`, then the pushforward measure `f_μ` is equal to the application of the linear map version of pushforward to the equivalent measurable function of `f`. Otherwise, `f_μ = 0`.
`MeasureTheory.ae_eq_of_ae_subset_of_measure_ge` theorem MeasureTheory.ae_eq_of_ae_subset_of_measure_ge : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, μ.ae.EventuallyLE s t → ↑↑μ t ≤ ↑↑μ s → MeasurableSet s → ↑↑μ t ≠ ⊤ → μ.ae.EventuallyEq s t The theorem `MeasureTheory.ae_eq_of_ae_subset_of_measure_ge` states that for any measure space `α` with a measurable space structure `m` and a measure `μ`, and any two sets `s` and `t` of `α`, if `s` is almost everywhere a subset of `t` (with respect to the measure `μ`), and the measure of `t` is less than or equal to the measure of `s`, and `s` is a measurable set, and the measure of `t` is not infinity, then `s` and `t` are almost equal everywhere (with respect to the measure `μ`). In other words, it means that if we have two sets such that one is mostly contained in the other and the potentially larger set doesn't have a larger measure and is measurable, then the two sets are almost everywhere the same. This theorem is related to the equality of sets in measure theory, particularly in the context of almost everywhere equality. More concisely: If two measurable sets in a measure space have almost everywhere subset relation and the larger set has finite measure less than or equal to the smaller set's measure, then they are almost everywhere equal.
`MeasureTheory.Ioi_ae_eq_Ici'` theorem MeasureTheory.Ioi_ae_eq_Ici' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PartialOrder α] {a : α}, ↑↑μ {a} = 0 → μ.ae.EventuallyEq (Set.Ioi a) (Set.Ici a) This theorem states that for any type `α` with a partial order, given a measurable space `m0`, a measure `μ`, and a value `a` of type `α`, if the measure of the singleton set `{a}` is zero, then the set of all elements greater than `a` (`Set.Ioi a`) is almost everywhere equal (in the measure-theoretic sense) to the set of all elements greater than or equal to `a` (`Set.Ici a`). In other words, if the measure of the set containing only the element `a` is zero, then for almost all elements, it doesn't matter whether we include `a` in the set or not; the two sets are almost everywhere the same. More concisely: For any measurable space and measure, if the measure of a singleton set is zero, then the sets of elements strictly greater and greater than or equal to the element have equal measure almost everywhere.
`MeasureTheory.Measure.map_id'` theorem MeasureTheory.Measure.map_id' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, MeasureTheory.Measure.map (fun x => x) μ = μ The theorem `MeasureTheory.Measure.map_id'` states that for any measurable space `α` and any measure `μ` defined on that space, the pushforward of `μ` under the identity function is equal to `μ` itself. In other words, applying the measure to the space without altering the elements (which is what the identity function does) doesn't change the measure. More concisely: For any measurable space `(α, Σ, μ)`, the pushforward measure of `μ` under the identity function is equal to `μ` itself.
`MeasureTheory.Measure.QuasiMeasurePreserving.preimage_ae_eq` theorem MeasureTheory.Measure.QuasiMeasurePreserving.preimage_ae_eq : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : α → β} {s t : Set β}, MeasureTheory.Measure.QuasiMeasurePreserving f μa μb → μb.ae.EventuallyEq s t → μa.ae.EventuallyEq (f ⁻¹' s) (f ⁻¹' t) This theorem states that for any two types `α` and `β`, with measurable spaces `m0` and `inst` respectively, and measures `μa` and `μb` on `α` and `β` respectively, and any function `f` from `α` to `β`, and any two sets `s` and `t` of `β`, if `f` is a quasi-measure preserving function from `μa` to `μb`, and the sets `s` and `t` are equal almost everywhere with respect to the measure `μb`, then the preimages of `s` and `t` under `f` are equal almost everywhere with respect to the measure `μa`. In other words, the preimage under a quasi-measure preserving function preserves the "almost everywhere" property from the codomain to the domain. More concisely: If `f` is a quasi-measure preserving function between measurable spaces `(α, m0, μa)` and `(β, inst, μb)`, and sets `s` and `t` in `β` are equal almost everywhere with respect to `μb`, then `f⁻¹(s)` and `f⁻¹(t)` are equal almost everywhere with respect to `μa`.
`MeasureTheory.measure_diff_lt_of_lt_add` theorem MeasureTheory.measure_diff_lt_of_lt_add : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, MeasurableSet s → s ⊆ t → ↑↑μ s ≠ ⊤ → ∀ {ε : ENNReal}, ↑↑μ t < ↑↑μ s + ε → ↑↑μ (t \ s) < ε This theorem is a statement in measure theory. It states that for any type `α`, measurable space `m`, measure `μ`, and two sets `s` and `t` of type `α`, if `s` is a measurable set that is a subset of `t`, and the measure of `s` is not infinite, then for any extended nonnegative real number `ε`, if the measure of `t` is less than the sum of the measure of `s` and `ε`, then the measure of the set difference `t \ s` (i.e., those elements of `t` that are not in `s`) is less than `ε`. This is a formal statement about the difference of measures of two sets in a measure space. More concisely: If `s` is a finite measurable subset of measurable space `(α, m)` with measure `μ` and `t` is any measurable set containing `s` such that `μ(t) < μ(s) + ε`, then `μ(t \ s) < ε`.
`MeasureTheory.measure_limsup_eq_zero` theorem MeasureTheory.measure_limsup_eq_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : ℕ → Set α}, ∑' (i : ℕ), ↑↑μ (s i) ≠ ⊤ → ↑↑μ (Filter.limsup s Filter.atTop) = 0 This theorem represents one direction of the Borel-Cantelli lemma, commonly known as the "first" Borel-Cantelli lemma. The theorem states that for any sequence of sets `(sᵢ)` in a measureable space with measure `μ`, if the series of the measures of the sets `(sᵢ)` is finite (i.e., `∑ μ sᵢ` is not infinite), then the measure of the limit superior of the sequence of sets `(sᵢ)` as it approaches infinity (i.e., `limsup sᵢ` as `i → ∞`) is equal to zero. This means that, under these conditions, the limit superior of the sequence of sets `(sᵢ)` is a null set. Please note that there is also a "second" Borel-Cantelli lemma which applies to independent sets in a probability space. For that, refer to `ProbabilityTheory.measure_limsup_eq_one`. More concisely: If `(sᵢ)` is a sequence of measurable sets in a measure space with finite sum of measures `∑ μ sᵢ`, then `limsup sᵢ` has measure zero.
`MeasureTheory.measure_biUnion` theorem MeasureTheory.measure_biUnion : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set β} {f : β → Set α}, s.Countable → s.PairwiseDisjoint f → (∀ b ∈ s, MeasurableSet (f b)) → ↑↑μ (⋃ b ∈ s, f b) = ∑' (p : ↑s), ↑↑μ (f ↑p) The theorem `MeasureTheory.measure_biUnion` states that for any type `α` and `β`, a measurable space `α`, a measure `μ` on `α`, a countable set `s` of type `β`, and a function `f` mapping from `β` to a set of `α`, if the images of any two distinct elements of `s` under `f` are disjoint, and each set `f b` for `b` in `s` is a measurable set, then the measure of the union of these sets is equal to the sum of their individual measures. In mathematical terms, if the sets `{f(b) : b ∈ s}` are pairwise disjoint and measurable, then `μ (⋃ b ∈ s, f b) = ∑' (p : s), μ (f p)`. More concisely: Given a measurable space `(α, μ)`, a countable set `s` of elements `β`, and a function `f : β → α` such that the images `{f(b) : b ∈ s}` are pairwise disjoint measurable sets, then `μ (⋃ b ∈ s, f(b)) = ∑' (b : s), μ (f(b))`.
`MeasureTheory.Measure.eq_zero_of_isEmpty` theorem MeasureTheory.Measure.eq_zero_of_isEmpty : ∀ {α : Type u_1} [inst : IsEmpty α] {_m : MeasurableSpace α} (μ : MeasureTheory.Measure α), μ = 0 This theorem states that for any type `α` that is empty (in other words, there are no values of this type), and any measurable space derived from this type `α`, any measure `μ` on that space is equal to zero. In simpler terms, if there are no elements in the set we're measuring, then the measure of that set is necessarily zero. More concisely: For any empty type `α` and measurable space derived from it, the measure of every set is zero.
`MeasureTheory.Measure.zero_le` theorem MeasureTheory.Measure.zero_le : ∀ {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α), 0 ≤ μ This theorem states that for any type `α` with a measurable space `_m0` and any measure `μ` from the measure theory, the measure `μ` is always greater than or equal to zero. In other words, in the context of measure theory, a measure defined on a measurable space cannot be negative. More concisely: For any measurable space `(α, _m0)` and measure `μ` defined on it, `μ : ∀ (A : set α), 0 ≤ μ A`.
`MeasureTheory.Measure.coe_add` theorem MeasureTheory.Measure.coe_add : ∀ {α : Type u_1} {_m : MeasurableSpace α} (μ₁ μ₂ : MeasureTheory.Measure α), ↑↑(μ₁ + μ₂) = ↑↑μ₁ + ↑↑μ₂ The theorem `MeasureTheory.Measure.coe_add` states that for any given measurable space `α`, and for any two measures `μ₁` and `μ₂` in that space, the measure (or the size) of the union of `μ₁` and `μ₂` is equal to the sum of the measures of `μ₁` and `μ₂`. This is essentially an application of the addition operation on measures in the context of Measure Theory. More concisely: For any measurable spaces `(α, Σ)` and measurable sets `A ∈ Σ` and `B ∈ Σ`, the measure of their union `A ∪ B` is equal to the sum of their individual measures, i.e., `μ(A ∪ B) = μ(A) + μ(B)`.
`MeasureTheory.Measure.absolutelyContinuous_refl` theorem MeasureTheory.Measure.absolutelyContinuous_refl : ∀ {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α), μ.AbsolutelyContinuous μ This theorem, `MeasureTheory.Measure.absolutelyContinuous_refl`, states that for any given measure space `α` and measure `μ`, the measure `μ` is absolutely continuous with respect to itself. In mathematical terms, a measure is said to be absolutely continuous with respect to another if any set of measure zero also has measure zero under the other measure. Here, since the two measures are the same, this property trivially holds. More concisely: A measure is absolutely continuous with respect to itself in a given measure space.
`MeasureTheory.Ioo_ae_eq_Ico'` theorem MeasureTheory.Ioo_ae_eq_Ico' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PartialOrder α] {a b : α}, ↑↑μ {a} = 0 → μ.ae.EventuallyEq (Set.Ioo a b) (Set.Ico a b) This theorem states that for any partially ordered type `α`, a given measurable space `m0` over that type, a measure `μ`, and any two elements `a` and `b` of type `α`, if the measure of the singleton set `{a}` is zero, then the left-open right-open interval `(a, b)` is almost everywhere equal to the left-closed right-open interval `[a, b)` with respect to the measure `μ`. "Almost everywhere" means that the set of points where the two intervals differ is a null set under the measure `μ`. More concisely: For any partially ordered type `α`, measurable space `m0` over `α`, measure `μ`, and elements `a` and `b` of `α` with `μ({a}) = 0`, the left-open right-open interval `(a, b)` is almost everywhere equal to the left-closed right-open interval `[a, b)` with respect to `μ`.
`MeasureTheory.Iio_ae_eq_Iic'` theorem MeasureTheory.Iio_ae_eq_Iic' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PartialOrder α] {a : α}, ↑↑μ {a} = 0 → μ.ae.EventuallyEq (Set.Iio a) (Set.Iic a) This theorem states that for any type `α` equipped with a measurable space structure `m0`, a measure `μ`, and a partial order, and for any element `a` of `α`, if the measure of the singleton set `{a}` is zero, then the left-infinite right-open interval ending at `a` (`Set.Iio a`) is almost everywhere equal (with respect to the measure `μ`) to the left-infinite right-closed interval ending at `a` (`Set.Iic a`). In other words, if the measure (or "size") of the set containing just the point `a` is zero, then the sets of all points less than `a` and all points less than or equal to `a` are essentially the same except possibly on a set of measure zero (a set that is negligible in terms of the measure `μ`), hence the term "almost everywhere". More concisely: Given a measurable space `(α, m0)` with measure `μ`, if the measure of the singleton `{a}` is zero for some `a` in `α`, then the left-infinite right-open interval `Set.Iio a` is almost everywhere equal to the left-infinite right-closed interval `Set.Iic a`.
`MeasureTheory.sum_measure_preimage_singleton` theorem MeasureTheory.sum_measure_preimage_singleton : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Finset β) {f : α → β}, (∀ y ∈ s, MeasurableSet (f ⁻¹' {y})) → (s.sum fun b => ↑↑μ (f ⁻¹' {b})) = ↑↑μ (f ⁻¹' ↑s) The theorem `MeasureTheory.sum_measure_preimage_singleton` states that for any given measure space `α`, measure `μ`, function `f : α → β`, and a finite set `s` of type `β`, if the preimage of every singleton set `{y}` such that `y` is in `s` is a measurable set, then the measure of the preimage of `s` is equal to the sum of the measures of these individual preimages. In other words, the measure of the preimage of the entire set `s` can be calculated by adding up the measures of the preimages of each element in `s`. More concisely: If `μ` is a measure on `α`, `f : α → β` is measurable, and for each `y ∈ s`, the preimage `{x ∈ α \| f(x) = y}` is measurable with measure `μ` having finite value, then `μ`(`f⁻¹(`s`)`) = ∑ₙ `μ`(`f⁻¹`({`yₙ`})) where `s = {`yₙ `\|` y ∈ β}`.
`MeasureTheory.Measure.AbsolutelyContinuous.smul` theorem MeasureTheory.Measure.AbsolutelyContinuous.smul : ∀ {α : Type u_1} {R : Type u_6} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : Monoid R] [inst_1 : DistribMulAction R ENNReal] [inst_2 : IsScalarTower R ENNReal ENNReal], μ.AbsolutelyContinuous ν → ∀ (c : R), (c • μ).AbsolutelyContinuous ν The theorem states that for any type `α`, any type `R`, any measurable space `m0` on `α`, and any two measures `μ` and `ν` on `α`, if `R` is a monoid and there are actions of `R` on extended nonnegative real numbers (`ENNReal`) that satisfy the distributive law and scalar tower property, then if measure `μ` is absolutely continuous with respect to measure `ν`, it implies that for any element `c` of type `R`, the measure `c • μ` (which is the scalar multiplication of `c` and `μ`) is also absolutely continuous with respect to measure `ν`. In simple terms, if a measure `μ` is dominated by another measure `ν` (meaning, if any set has measure zero under `ν`, it also has measure zero under `μ`), then any scaled version of `μ` (achieved by multiplying `μ` with any scalar `c`) is also dominated by the same measure `ν`. More concisely: If measure `μ` is absolutely continuous with respect to measure `ν` on measurable space `(α, m0)`, and `R` is a monoid with actions on `ENNReal` satisfying distributive law and scalar tower property, then for any `c` in `R`, the scaled measure `c • μ` is also absolutely continuous with respect to `ν`.
`MeasureTheory.Measure.measure_inter_eq_of_measure_eq` theorem MeasureTheory.Measure.measure_inter_eq_of_measure_eq : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t u : Set α}, MeasurableSet s → ↑↑μ t = ↑↑μ u → t ⊆ u → ↑↑μ t ≠ ⊤ → ↑↑μ (t ∩ s) = ↑↑μ (u ∩ s) The theorem, `MeasureTheory.Measure.measure_inter_eq_of_measure_eq`, states that for any type `α` with a measurable space `m0` and a measure `μ`, and for any sets `s`, `t`, and `u` of type `α`, if `s` is a measurable set, the measure of `t` is equal to the measure of `u`, `t` is a subset of `u`, and the measure of `t` is not infinite, then the measure of the intersection of `t` and `s` is equal to the measure of the intersection of `u` and `s`. In other words, if `u` is a superset of `t` and both sets have the same (finite) measure (even if the sets are not necessarily measurable), then for any measurable set `s`, the measure of the intersection of `t` and `s` will be equal to the measure of the intersection of `u` and `s`. More concisely: If `s` is a measurable set, `t` is a subset of `u`, `μ(t)` is finite, and `μ(s) < ∞`, then `μ(t ∩ s) = μ(u ∩ s)`.
`MeasureTheory.nonempty_inter_of_measure_lt_add'` theorem MeasureTheory.nonempty_inter_of_measure_lt_add' : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) {s t u : Set α}, MeasurableSet s → s ⊆ u → t ⊆ u → ↑↑μ u < ↑↑μ s + ↑↑μ t → (s ∩ t).Nonempty This theorem, titled `MeasureTheory.nonempty_inter_of_measure_lt_add'`, states that for any type `α`, given a measure space `m` and a measure `μ` on that space, and any three sets `s`, `t`, and `u` of type `α`, if set `s` is measurable and both sets `s` and `t` are included in set `u`, and the measure of `u` is less than the sum of measures of `s` and `t`, then the intersection of sets `s` and `t` is nonempty. In other words, `s` and `t` must have at least one element in common under these conditions. More concisely: If `μ(u) < μ(s) + μ(t)` and `s`, `t` are measurable subsets of a measure space `(α, Σ, m)` with `s ⊆ u` and `t ⊆ u`, then `s ∩ t` is nonempty.
`MeasureTheory.le_toMeasure_apply` theorem MeasureTheory.le_toMeasure_apply : ∀ {α : Type u_1} [ms : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (h : ms ≤ m.caratheodory) (s : Set α), ↑m s ≤ ↑↑(m.toMeasure h) s This theorem states that for any type `α` equipped with a `MeasurableSpace` structure, given an outer measure `m` on `α` and a set `s` of `α`, if all sets in the `MeasurableSpace` are Carathéodory measurable with respect to the outer measure `m` (denoted by `ms ≤ MeasureTheory.OuterMeasure.caratheodory m`), then the outer measure of `s` is less than or equal to the measure of `s` obtained by converting the outer measure to a measure (via `MeasureTheory.OuterMeasure.toMeasure m h`). In mathematical terms, we have `m(s) ≤ (MeasureTheory.OuterMeasure.toMeasure(m,h))(s)` for any such `s`. More concisely: For any Carathéodory measurable outer measure `m` on a measurable space `α`, the outer measure of a set `s` is less than or equal to the measure of `s` obtained by converting `m` to a measure. (i.e., `m(s) ≤ (MeasureTheory.OuterMeasure.toMeasure m h)(s)` for any Carathéodory measurable `s`.)
`MeasureTheory.Measure.preimage_null_of_map_null` theorem MeasureTheory.Measure.preimage_null_of_map_null : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : α → β}, AEMeasurable f μ → ∀ {s : Set β}, ↑↑(MeasureTheory.Measure.map f μ) s = 0 → ↑↑μ (f ⁻¹' s) = 0 This theorem states that for any types `α` and `β`, given a measurable space `α`, another measurable space `β`, a measure `μ` on `α`, and a function `f` from `α` to `β` that is almost everywhere measurable, if the image measure of any set `s` under the function `f` is zero, then the measure of the preimage of the set `s` under `f` is also zero. This holds even if the set `s` is not measurable. In mathematical terms, given an almost everywhere measurable function `f: α → β` and a measure `μ: α`, if `μ(f(s)) = 0` then `μ(f⁻¹(s)) = 0`, where `f⁻¹` denotes the preimage function of `f`. More concisely: If `f: α → β` is an almost everywhere measurable function and `μ` is a measure on `α` such that `μ(f(s)) = 0`, then `μ(f⁻¹(s)) = 0`.
`MeasureTheory.tsum_measure_preimage_singleton` theorem MeasureTheory.tsum_measure_preimage_singleton : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set β}, s.Countable → ∀ {f : α → β}, (∀ y ∈ s, MeasurableSet (f ⁻¹' {y})) → ∑' (b : ↑s), ↑↑μ (f ⁻¹' {↑b}) = ↑↑μ (f ⁻¹' s) The theorem `MeasureTheory.tsum_measure_preimage_singleton` states that for any countable set `s` in a space of type `β`, and for any function `f` from a measurable space `α` to `β`, provided that for every `y` in `s`, the preimage of the singleton set `{y}` under `f` is measurable, the measure of the preimage of `s` under `f` is equal to the sum of the measures of the preimages of the singleton sets `{y}` for all `y` in `s`. This measure is computed with respect to a specific measure `μ` on the measurable space `α`. More concisely: For any countable set `s` in a measurable space `β`, and measurable function `f` from a measurable space `(α, μ)` to `β`, if for every `y` in `s`, the preimage `f^(-1)({y})` is measurable, then `μ(f^(-1)(s)) = ∑ₙ μ(f^(-1)({y_n}))`, where `y_n` are the elements of `s`.
`MeasurableEquiv.map_ae` theorem MeasurableEquiv.map_ae : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (f : α ≃ᵐ β) (μ : MeasureTheory.Measure α), Filter.map (⇑f) μ.ae = (MeasureTheory.Measure.map (⇑f) μ).ae This theorem, `MeasurableEquiv.map_ae`, states that for any types `α` and `β` each equipped with a `MeasurableSpace` structure, for any measurable equivalence `f` between `α` and `β`, and any measure `μ` on `α`, the forward map of the filter of the "almost everywhere" filter of `μ` under `f` is equal to the "almost everywhere" filter of the pushforward measure under `f`. This illustrates how the "almost everywhere" property and the pushforward measure interact with each other under a measurable equivalence. More concisely: For any measurable spaces `(α, Σα)` and `(β, Σβ)`, measurable equivalence `f : α ≃ β`, and measure `μ : MeasurableDistribution Σα`, the forward image of `μ`'s almost everywhere filter under `f` equals the almost everywhere filter of the pushforward measure `f_# μ`.
`MeasureTheory.measure_diff_null` theorem MeasureTheory.measure_diff_null : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α}, ↑↑μ s₂ = 0 → ↑↑μ (s₁ \ s₂) = ↑↑μ s₁ This theorem, `MeasureTheory.measure_diff_null`, states that for any types `α`, any measurable space `m` on `α`, any measure `μ` in this measurable space, and any two sets `s₁` and `s₂` of type `α`, if the measure `μ` of set `s₂` is zero, then the measure of the difference `s₁ \ s₂` is equal to the measure of `s₁`. In simpler terms, if we subtract a set `s₂` with measure zero from another set `s₁`, the measure of the resulting set is the same as the original measure of `s₁`. More concisely: If `μ(s₂) = 0`, then `μ(s₁ \ s₂) = μ(s₁)`.
`MeasureTheory.Measure.comap_apply` theorem MeasureTheory.Measure.comap_apply : ∀ {α : Type u_1} {s : Set α} {β : Type u_8} [inst : MeasurableSpace α] {_mβ : MeasurableSpace β} (f : α → β), Function.Injective f → (∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)) → ∀ (μ : MeasureTheory.Measure β), MeasurableSet s → ↑↑(MeasureTheory.Measure.comap f μ) s = ↑↑μ (f '' s) The theorem `MeasureTheory.Measure.comap_apply` states that for any types `α` and `β`, a set `s` of type `α`, and a function `f` from `α` to `β` which is injective, if every measurable set in `α` is mapped to a measurable set in `β` by `f`, then for any measure `μ` on `β`, the measure of the set `s` under the comap of `f` and `μ` is equal to the measure of the image of `s` under `f` in the measure `μ`, provided `s` is a measurable set. In other words, the measure of a set under the comap of a measure corresponds to the measure of its image under the original measure, when considering injective functions that map measurable sets to measurable sets. More concisely: If `f: α → β` is injective and maps measurable sets to measurable sets, then for any measurable set `s ∈ α` and measure `μ` on `β`, `MeasureTheory.Measure.comap_apply μ f s` equals the measure of `f''s` under `μ`.
`MeasureTheory.Measure.map_map` theorem MeasureTheory.Measure.map_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {g : β → γ} {f : α → β}, Measurable g → Measurable f → MeasureTheory.Measure.map g (MeasureTheory.Measure.map f μ) = MeasureTheory.Measure.map (g ∘ f) μ This theorem states that for any three types `α`, `β`, and `γ` with associated measurable spaces, and any measure `μ` on the type `α`, if we have two measurable functions `f` from `α` to `β` and `g` from `β` to `γ`, then the pushforward measure obtained by first mapping `μ` through `f` and then through `g` is the same as the pushforward measure obtained by mapping `μ` through the composition of `g` and `f`. In other words, the operation of taking pushforward measures commutes with the operation of composing functions. This is often referred to as the change of variables theorem in measure theory. More concisely: Given measurable spaces `(α, Σα)`, `(β, Σβ)`, `(γ, Σγ)`, measures `μ` on `α`, and measurable functions `f: α → β` and `g: β → γ`, the pushforwards `f._measure_theory_.Pushforward μ f` and `g._measure_theory_.Pushforward (f._measure_theory_.Pushforward μ f) g` are equal.
`MeasureTheory.measure_iUnion_eq_iSup` theorem MeasureTheory.measure_iUnion_eq_iSup : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Countable ι] {s : ι → Set α}, Directed (fun x x_1 => x ⊆ x_1) s → ↑↑μ (⋃ i, s i) = ⨆ i, ↑↑μ (s i) The theorem `MeasureTheory.measure_iUnion_eq_iSup` states that for any types `α` and `ι`, a measurable space `m` over `α`, a measure `μ` on that measurable space, and a countable family of sets `s` indexed by `ι`, if the family of sets is directed with respect to the subset relation (i.e., for any two sets in the family, there is another set in the family that contains both), then the measure of the union of all sets in the family equals the supremum of the measures of the individual sets in the family. In terms for measure theory, this property is referred to as "continuity from below". More concisely: For any measurable space `(α, m)`, measure `μ`, and countable family `{S_i}_ι` of measurable sets directed by subset relation, `μ(⋃_ι S_i) = ‾⁡⁢⁢⁢sup_ι μ(S_i)`.
`MeasureTheory.Measure.measure_univ_pos` theorem MeasureTheory.Measure.measure_univ_pos : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, 0 < ↑↑μ Set.univ ↔ μ ≠ 0 This theorem, `MeasureTheory.Measure.measure_univ_pos`, states that for any given type `α`, given measurable space `m0` on `α`, and given measure `μ` on this measurable space, the measure of the universal set (which contains all elements of type `α`) is greater than zero if and only if the measure `μ` is not zero. Essentially, this means that a measure is non-zero if and only if it assigns a positive measure to the set of all possible outcomes. More concisely: For any measurable space `(α, m0)` and measure `μ` on `α`, `μ` is non-zero if and only if `μ` assigns positive measure to the universal set `α`.
`MeasureTheory.Measure.smul_apply` theorem MeasureTheory.Measure.smul_apply : ∀ {α : Type u_1} {R : Type u_6} [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal] {_m : MeasurableSpace α} (c : R) (μ : MeasureTheory.Measure α) (s : Set α), ↑↑(c • μ) s = c • ↑↑μ s This theorem, `MeasureTheory.Measure.smul_apply`, states that for any types `α` and `R`, where `R` is a type that can be scaled (multiplied) with the extended nonnegative real numbers (`ENNReal`), given a measurable space of type `α`, a scalar `c` of type `R`, a measure `μ` on that measurable space, and a set `s` of elements of type `α`, the measure of the set `s` under the scaled measure `c • μ` is equal to the scalar `c` scaled with the measure of the set `s` under the original measure `μ`. This establishes a property of scalar multiplication in the context of measures, essentially stating that scaling a measure and then applying it is the same as applying the measure and then scaling the result. More concisely: For any measurable space `(α, Σ, μ)`, scalar `c` in a type `R` with scalar multiplication `•`, and measurable set `s` in `α`, `c • μ(s) = μ(s) • c`.
`MeasureTheory.Measure.tendsto_ae_map` theorem MeasureTheory.Measure.tendsto_ae_map : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : α → β}, AEMeasurable f μ → Filter.Tendsto f μ.ae (MeasureTheory.Measure.map f μ).ae This theorem, `MeasureTheory.Measure.tendsto_ae_map`, states that for any two types `α` and `β` with `α` having a measurable space structure `m0` and `β` having a measurable space instance, given any measure `μ` on `α` and any function `f` from `α` to `β`, if the function `f` is almost everywhere measurable with respect to the measure `μ`, then the function `f` tends from the "almost everywhere" filter of the measure `μ` to the "almost everywhere" filter of the pushforward of the measure `μ` under the function `f`. In other words, if a function is almost everywhere measurable, then the pre-image under that function of almost every set in the target space is almost every set in the original space. More concisely: If `μ` is a measure on `α` and `f: α → β` is almost everywhere measurable, then for every `B ⊆ β` in the "almost everywhere" filter of `β` under the measure `μ` pushed forward by `f`, there exists a set `A ⊆ α` in the "almost everywhere" filter of `α` under `μ` such that `f(A) = B`.
`MeasureTheory.NullMeasurableSet.mono_ac` theorem MeasureTheory.NullMeasurableSet.mono_ac : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α}, MeasureTheory.NullMeasurableSet s μ → ν.AbsolutelyContinuous μ → MeasureTheory.NullMeasurableSet s ν The theorem `MeasureTheory.NullMeasurableSet.mono_ac` states that for any type `α`, given a measurable space `m0` over `α`, and two measures `μ` and `ν` over `α`, and a set `s` of type `α`, if `s` is a Null Measurable Set with respect to the measure `μ`, and if the measure `ν` is absolutely continuous with respect to `μ`, then `s` is a Null Measurable Set with respect to the measure `ν`. This means that a set's null measurability and a measure's absolute continuity are transitive properties across measures. More concisely: If `μ` is absolutely continuous with respect to `ν`, and `s` is a Null Measurable Set with respect to `μ` over measurable space `m0` on type `α`, then `s` is a Null Measurable Set with respect to `ν`.
`LE.le.absolutelyContinuous` theorem LE.le.absolutelyContinuous : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ ≤ ν → μ.AbsolutelyContinuous ν := by sorry The theorem `LE.le.absolutelyContinuous` states that for any type `α`, given a measurable space `m0` and two measures `μ` and `ν` on that space, if `μ` is less than or equal to `ν` (in the sense that for every set, the measure of the set according to `μ` is less than or equal to its measure according to `ν`), then `μ` is absolutely continuous with respect to `ν`. In other words, whenever `ν` assigns measure zero to a set, `μ` also assigns measure zero to the same set. This is an alias of the theorem `MeasureTheory.Measure.absolutelyContinuous_of_le`. More concisely: If `μ` is a measure that is less than or equal to another measure `ν` on a measurable space `(α, m0)`, then `μ` is absolutely continuous with respect to `ν`.
`MeasureTheory.nonempty_inter_of_measure_lt_add` theorem MeasureTheory.nonempty_inter_of_measure_lt_add : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) {s t u : Set α}, MeasurableSet t → s ⊆ u → t ⊆ u → ↑↑μ u < ↑↑μ s + ↑↑μ t → (s ∩ t).Nonempty This theorem, named `MeasureTheory.nonempty_inter_of_measure_lt_add`, states that for any measure space `α` with a measure `μ`, and sets `s`, `t`, and `u` within this measure space, if `t` is measurable and both `s` and `t` are subsets of `u`, and if the measure of `u` is less than the sum of the measures of `s` and `t`, then the intersection of `s` and `t` must be nonempty. In other words, the sets `s` and `t` must have at least one element in common. More concisely: If `μ(u) < μ(s) + μ(t)` and `s`, `t` are measurable subsets of a measure space `(α, μ)` with `s ⊆ u` and `t ⊆ u`, then `s ∩ t` is nonempty.
`MeasureTheory.Measure.sum_apply` theorem MeasureTheory.Measure.sum_apply : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} (f : ι → MeasureTheory.Measure α) {s : Set α}, MeasurableSet s → ↑↑(MeasureTheory.Measure.sum f) s = ∑' (i : ι), ↑↑(f i) s The theorem `MeasureTheory.Measure.sum_apply` states that for any given type `α` and index type `ι`, along with a measurable space `α` and a function `f` that maps `ι` to a measure on `α`, if `s` is a measurable set of `α`, then the measure of `s` under the sum of the measures defined by `f` is equal to the sum of the measures of `s` under each individual measure defined by `f`. This is an important property that keeps the behavior of measures consistent when dealing with indexed families of measures. Essentially, it says that the sum of measures of a set under different measures is equivalent to the measure of the set under the sum of those measures. More concisely: For any measurable space `(α, Σ, μ)` and index type `ι`, if `f : ι → μ(α)` is a family of measures on `α`, then for any measurable set `s ∈ Σ`, we have `∑ i : ι, mu s i = mu (∑ i : ι, s)`.
`MeasureTheory.Measure.map_id` theorem MeasureTheory.Measure.map_id : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, MeasureTheory.Measure.map id μ = μ := by sorry The theorem `MeasureTheory.Measure.map_id` states that for any type `α`, any measurable space `m0` on `α`, and any measure `μ` on this measurable space, the pushforward of the measure `μ` under the identity function (`id`) is the same as the original measure `μ`. This is essentially saying that applying the identity function doesn't change the measure, which aligns with our intuitive understanding of the identity function. More concisely: For any measurable space `(α, Σ, m)` and measure `μ:` `Σ → ℝ`, the pushforward `id.pushforward μ` of `μ` under the identity function is equal to `μ`.
`MeasureTheory.ae_zero` theorem MeasureTheory.ae_zero : ∀ {α : Type u_1} {_m0 : MeasurableSpace α}, MeasureTheory.Measure.ae 0 = ⊥ This theorem states that for any type `α` and any measurable space `_m0` on `α`, the "almost everywhere" filter of the zero measure is the bottom filter. In more mathematical terms, it means that in any measurable space, the set of all points where a null measure is non-zero is empty. More concisely: In any measurable space, the filter of sets of measure zero is the bottom filter.
`MeasureTheory.Measure.map_apply_of_aemeasurable` theorem MeasureTheory.Measure.map_apply_of_aemeasurable : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : α → β}, AEMeasurable f μ → ∀ {s : Set β}, MeasurableSet s → ↑↑(MeasureTheory.Measure.map f μ) s = ↑↑μ (f ⁻¹' s) This theorem, `MeasureTheory.Measure.map_apply_of_aemeasurable`, states that for any two types `α` and `β` with measure spaces `m0` and `inst` respectively, given a measure `μ` on type `α` and a function `f` that maps from `α` to `β` and is almost everywhere measurable relative to `μ`, if we have a set `s` of `β` that is measurable, then the measure of `s` under the pushforward of `μ` by `f` is equal to the measure of the preimage of `s` under `f` with respect to `μ`. In simpler terms, it explains how to measure a set in the target space of a function in terms of the measure of its preimage in the original space. More concisely: For any measurable functions f from a measurable space (α, m0) to a measurable space (β, m), and any measurable set s in (β), the measure of s under the pushforward measure m \* f is equal to the measure of the preimage of s under f with respect to m0.
`MeasureTheory.NullMeasurableSet.mono` theorem MeasureTheory.NullMeasurableSet.mono : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α}, MeasureTheory.NullMeasurableSet s μ → ν ≤ μ → MeasureTheory.NullMeasurableSet s ν This theorem states that for any given type `α` and a measurable space `m0` over `α`, if you have two measures `μ` and `ν` on this measurable space and a set `s` of type `α` such that `s` is a null measurable set with respect to measure `μ`, then if measure `ν` is less than or equal to measure `μ`, `s` is also a null measurable set with respect to measure `ν`. In other words, the null measurability of a set under a given measure is preserved under a smaller or equal measure. More concisely: If `μ` is a measure that is larger than or equal to `ν` on a measurable space `(α, m0)`, and `s` is a null measurable set with respect to `μ`, then `s` is also a null measurable set with respect to `ν`.
`MeasureTheory.tendsto_measure_biInter_gt` theorem MeasureTheory.tendsto_measure_biInter_gt : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_8} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] [inst_3 : DenselyOrdered ι] [inst_4 : FirstCountableTopology ι] {s : ι → Set α} {a : ι}, (∀ r > a, MeasurableSet (s r)) → (∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j) → (∃ r > a, ↑↑μ (s r) ≠ ⊤) → Filter.Tendsto (↑↑μ ∘ s) (nhdsWithin a (Set.Ioi a)) (nhds (↑↑μ (⋂ r, ⋂ (_ : r > a), s r))) This theorem, named `MeasureTheory.tendsto_measure_biInter_gt`, states that for a decreasing sequence of measurable sets indexed by a linear order with a first countable topology, the measure of the intersection of these sets is the limit of the measures. More specifically, given a measurable space `α`, a measure `μ` on this space, and a function `s` from a linear ordered index set `ι` (which is densely ordered, has a topological space structure, an order topology, and a first countable topology) to the set of subsets of `α`, if every set `s r` for `r` greater than a given `a` is measurable, and for any `i` and `j` greater than `a` with `i ≤ j` the set `s i` is a subset of `s j`, and there exists `r` greater than `a` such that the measure of `s r` is not infinite, then the function that maps `r` to the measure of `s r` tends to the measure of the intersection of all `s r` for `r` greater than `a`, when `r` tends to `a` within the set of values greater than `a`. More concisely: Given a measurable space, a measure, a decreasing sequence of measurable sets indexed by a first countable, densely ordered linear topology, if the measures of sets for indices greater than a certain value are finite and converge, then the limit is the measure of their intersection.
`MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq` theorem MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq : ∀ {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : α → β}, MeasureTheory.Measure.QuasiMeasurePreserving f μa μb → ∀ {g₁ g₂ : β → δ}, μb.ae.EventuallyEq g₁ g₂ → μa.ae.EventuallyEq (g₁ ∘ f) (g₂ ∘ f) The theorem `MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq` states that for any types `α`, `β`, and `δ`, with `α` and `β` equipped with measurable spaces, and `μa` and `μb` are measures on `α` and `β` respectively, if a function `f` from `α` to `β` is quasi measure preserving with respect to measures `μa` and `μb`, then for any two functions `g₁` and `g₂` from `β` to `δ`, if `g₁` is almost everywhere equal to `g₂` with respect to the measure `μb`, then the compositions `g₁ ∘ f` and `g₂ ∘ f` are also almost everywhere equal with respect to the measure `μa`. "Almost everywhere" means on all sets except a set of measure zero. More concisely: If `f: α → β` is quasi measure preserving between measurable spaces `(α, Σα, μa)` and `(β, Σβ, μb)`, and `g₁` and `g₂` are functions from `β` to a third type `δ` such that `g₁ = g₂` almost everywhere with respect to `μb`, then `g₁ ∘ f = g₂ ∘ f` almost everywhere with respect to `μa`.
`MeasureTheory.Measure.le_sum_apply` theorem MeasureTheory.Measure.le_sum_apply : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} (f : ι → MeasureTheory.Measure α) (s : Set α), ∑' (i : ι), ↑↑(f i) s ≤ ↑↑(MeasureTheory.Measure.sum f) s The theorem `MeasureTheory.Measure.le_sum_apply` establishes an inequality for the sum of measures in a measure space. Specifically, for any type `α` with the structure of a measurable space, any indexed family of measures `f : ι → MeasureTheory.Measure α`, and any set `s` in `α`, the theorem states that the infinite sum of the measures of `s` according to each measure in the family `f` is less than or equal to the measure of `s` under the sum of the entire family of measures. This is written mathematically as `∑' (i : ι), (f i) s ≤ (MeasureTheory.Measure.sum f) s`. More concisely: For any measurable space `α`, any indexed family `f : ι → MeasureTheory.Measure α`, and any set `s` in `α`, the sum of the measures of `s` according to each measure in `f` is less than or equal to the measure of `s` under the sum of the entire family of measures: `∑' (i : ι), (f i) s ≤ (MeasureTheory.Measure.sum f) s`.
`MeasureTheory.Measure.coe_smul` theorem MeasureTheory.Measure.coe_smul : ∀ {α : Type u_1} {R : Type u_6} [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal] {_m : MeasurableSpace α} (c : R) (μ : MeasureTheory.Measure α), ↑↑(c • μ) = c • ↑↑μ This theorem states that for any type `α`, type `R`, and a measurable space `_m` on `α`, given a scalar multiplication operation on `R` and `ENNReal`, and a scalar tower structure established over `R`, `ENNReal`, and `ENNReal`, for any real number `c` and a measure `μ` from the measure theory over `α`, the measure of the scalar multiplication of `c` and `μ` when lifted twice to an extended nonnegative real number (using the `↑↑` notation) equals the scalar multiplication of `c` and the twice lifted measure of `μ`. In other words, the process of lifting the result of scalar multiplication to the extended nonnegative real numbers is consistent with performing scalar multiplication after lifting to the extended nonnegative real numbers. This is an important property that maintains the consistency of operations in measure theory when extended to nonnegative real numbers. More concisely: For any measure `μ` on a measurable space `(_,_m)` over type `α`, scalar multiplication `c • μ` and lifting to extended nonnegative reals `↑↑(c • μ)` commute, i.e., `↑↑(c • μ) = c • ↑↑(μ)`.
`MeasureTheory.measure_inter_add_diff` theorem MeasureTheory.measure_inter_add_diff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α), MeasurableSet t → ↑↑μ (s ∩ t) + ↑↑μ (s \ t) = ↑↑μ s The theorem `MeasureTheory.measure_inter_add_diff` states that for any type `α`, any measurable space `m` over `α`, any measure `μ` in the measurable space, and any two sets `s` and `t` of type `α`, if `t` is a measurable set, then the measure of the intersection of `s` and `t` plus the measure of the difference of `s` and `t` is equal to the measure of `s`. In mathematical terms, it's saying that for all sets `s` and `t`, if `t` is measurable, then `μ(s ∩ t) + μ(s \ t) = μ(s)`. This is a fundamental property of measures, expressing that the measure of a set is completely determined by the measures of its measurable parts. More concisely: For any measurable space and measure, the measure of a set is equal to the measure of its intersection with a measurable set plus the measure of their difference.
`MeasureTheory.measure_iInter_eq_iInf` theorem MeasureTheory.measure_iInter_eq_iInf : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Countable ι] {s : ι → Set α}, (∀ (i : ι), MeasurableSet (s i)) → Directed (fun x x_1 => x ⊇ x_1) s → (∃ i, ↑↑μ (s i) ≠ ⊤) → ↑↑μ (⋂ i, s i) = ⨅ i, ↑↑μ (s i) This theorem, named `MeasureTheory.measure_iInter_eq_iInf`, states that in a measurable space `α` with a given measure `μ`, if you have a countable sequence of measurable sets `s : ι → Set α` (with `ι` as the indexing set), such that the sequence is decreasing (each set in the sequence is a superset of the following ones) and at least one of these sets does not have measure `⊤` (infinity), then the measure of the intersection of all these sets is equal to the infimum of the measures of the sets in the sequence. This concept is also known as "continuity from above" in measure theory. More concisely: If `α` is a measurable space with measure `μ`, and `s : ι → Set α` is a countable, decreasing sequence of measurable sets in `α` with at least one set of finite measure, then `μ (∩ₙ s i) = ∧ₙ i ∈ ι mi`.
`MeasureTheory.Measure.map_add` theorem MeasureTheory.Measure.map_add : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] (μ ν : MeasureTheory.Measure α) {f : α → β}, Measurable f → MeasureTheory.Measure.map f (μ + ν) = MeasureTheory.Measure.map f μ + MeasureTheory.Measure.map f ν The theorem `MeasureTheory.Measure.map_add` states that for any two measures `μ` and `ν` on a measurable space `α`, and a measurable function `f` from `α` to another measurable space `β`, the pushforward of the sum of `μ` and `ν` under `f` is the same as the sum of the pushforwards of `μ` and `ν` under `f`. In other words, the operation of measure pushforward distributes over the addition of measures. More concisely: For measurable functions between measurable spaces and measures thereon, the pushforward of the sum of two measures is equal to the sum of their pushforwards.
`MeasureTheory.tendsto_measure_iUnion` theorem MeasureTheory.tendsto_measure_iUnion : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Preorder ι] [inst_1 : IsDirected ι fun x x_1 => x ≤ x_1] [inst_2 : Countable ι] {s : ι → Set α}, Monotone s → Filter.Tendsto (↑↑μ ∘ s) Filter.atTop (nhds (↑↑μ (⋃ n, s n))) This theorem, named "MeasureTheory.tendsto_measure_iUnion", states that for a given measurable space `α`, an indexing type `ι` which is ordered via a preorder, a measure `μ` on `α`, and a sequence of sets `s` indexed by `ι`, if the sequence `s` is monotone (meaning that for any two elements `x` and `x_1` in `ι`, `x ≤ x_1` implies `s(x) ⊆ s(x_1)`), then the measure of the union of the sets in the sequence `s` (i.e., `μ(⋃ n, s n)`) is the limit of the measures of the sets in the sequence `s` as `n` tends to infinity (expressed as `Filter.Tendsto (μ ∘ s) Filter.atTop (nhds (μ (⋃ n, s n)))`). Here, `Filter.atTop` is the filter representing the limit `→ ∞`, and `nhds` is the neighborhood function which represents the collection of all neighborhoods of a point in a topological space. More concisely: Given a measurable space, an ordered indexing type, a measure, and a monotone sequence of measurable sets, the limit of the measures of the sets as the index tends to infinity is equal to the measure of the union of the sets.
`MeasureTheory.Measure.le_map_apply` theorem MeasureTheory.Measure.le_map_apply : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : α → β}, AEMeasurable f μ → ∀ (s : Set β), ↑↑μ (f ⁻¹' s) ≤ ↑↑(MeasureTheory.Measure.map f μ) s The theorem `MeasureTheory.Measure.le_map_apply` states that for any measurable space `α` and `β`, measure `μ` on `α`, and a function `f` from `α` to `β` that is almost everywhere measurable, for every set `s` of `β`, the measure of the preimage of `s` under `f` is less than or equal to the measure of `s` under the pushforward of `μ` by `f`. This holds true even if the set `s` is not measurable. In other words, the measure of the set of points in `α` that get mapped into `s` by `f` is always less than or equal to the measure of `s` itself under the pushforward measure. More concisely: For any measurable space (α, Σ\_α), measure μ on Σ\_α, almost everywhere measurable function f : α → β, and any set s ∈ Σ\_β, the measure μ(f⁻¹(s)) ≤ μ\_f(s), where μ\_f is the pushforward measure of μ by f.
`MeasureTheory.toMeasure_apply` theorem MeasureTheory.toMeasure_apply : ∀ {α : Type u_1} [ms : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (h : ms ≤ m.caratheodory) {s : Set α}, MeasurableSet s → ↑↑(m.toMeasure h) s = ↑m s The theorem `MeasureTheory.toMeasure_apply` states that for any type `α` with an associated measurable space `ms`, an outer measure `m` on `α`, and a set `s` of type `α`, if the measurable space `ms` is a subspace of the Carathéodory-measurable space associated with the outer measure `m` and the set `s` is a measurable set, then the measure of the set `s` under the measure induced by the outer measure `m` is equal to the outer measure of the set `s` under `m`. More concisely: If `ms` is a Carathéodory measurable space and `s` is a measurable set in the measurable space `ms` with respect to an outer measure `m`, then `m(s) = (m $\|$ ms)(s)`.
`MeasureTheory.Measure.measure_univ_eq_zero` theorem MeasureTheory.Measure.measure_univ_eq_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, ↑↑μ Set.univ = 0 ↔ μ = 0 This theorem states that for any type `α`, any measurable space `m0` over `α`, and any measure `μ` from the measure theory, the measure of the universal set `Set.univ` is equal to zero if and only if the measure `μ` itself is zero. In other words, a measure is zero if it assigns zero measure to the entire space it is defined on, and conversely, if a measure is zero, then the measure it assigns to the entire space is zero. This is an important property in measure theory, allowing us to identify trivial or empty measures. More concisely: For any measure `μ` on a measurable space `(α, m0)`, `μ` assigns measure zero to the universal set `Set.univ` if and only if `μ` is the zero measure.
`MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null` theorem MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : α → β}, MeasureTheory.Measure.QuasiMeasurePreserving f μa μb → ∀ {s : Set β}, ↑↑μb s = 0 → ↑↑μa (f ⁻¹' s) = 0 This theorem states that for any given types `α` and `β`, a measurable space `α` denoted by `m0`, another measurable space `β`, two measures `μa` and `μb` for spaces `α` and `β` respectively, and a function `f` mapping `α` to `β`: If the function `f` is quasi measure preserving from measure `μa` to `μb`, then for any set `s` of type `β`, if the measure of `s` with respect to `μb` is zero, then the measure of the preimage of `s` under `f` with respect to `μa` is also zero. In other words, if a function is quasi measure preserving and a set in the codomain has measure zero, then the measure of the set of all pre-images in the domain is also zero. More concisely: If `f: α → β` is a quasi-measure preserving function between measurable spaces `(α, μa)` and `(β, μb)`, then `μa(f⁻¹(S)) = 0` for any `S ⊆ β` with `μb(S) = 0`.

LeanAide GPT-4 documentation

Module: Mathlib.MeasureTheory.Measure.MeasureSpace

MeasureTheory.ae_eq_bot

theorem MeasureTheory.ae_eq_bot : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.ae = ⊥ ↔ μ = 0

MeasureTheory.ae_mono

theorem MeasureTheory.ae_mono : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ ≤ ν → μ.ae ≤ ν.ae

MeasureTheory.Measure.le_add_right

theorem MeasureTheory.Measure.le_add_right : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν ν' : MeasureTheory.Measure α}, μ ≤ ν → μ ≤ ν + ν'

MeasureTheory.exists_nonempty_inter_of_measure_univ_lt_tsum_measure

MeasureTheory.measure_compl

theorem MeasureTheory.measure_compl : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}, MeasurableSet s → ↑↑μ s ≠ ⊤ → ↑↑μ sᶜ = ↑↑μ Set.univ - ↑↑μ s

MeasureTheory.Measure.QuasiMeasurePreserving.aemeasurable

MeasureTheory.Measure.le_iff'

theorem MeasureTheory.Measure.le_iff' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ μ₂ : MeasureTheory.Measure α}, μ₁ ≤ μ₂ ↔ ∀ (s : Set α), ↑↑μ₁ s ≤ ↑↑μ₂ s

LE.le.absolutelyContinuous_of_ae

theorem LE.le.absolutelyContinuous_of_ae : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ.ae ≤ ν.ae → μ.AbsolutelyContinuous ν

MeasureTheory.Measure.AbsolutelyContinuous.rfl

theorem MeasureTheory.Measure.AbsolutelyContinuous.rfl : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.AbsolutelyContinuous μ

MeasureTheory.Measure.QuasiMeasurePreserving.mono

MeasurableEquiv.map_apply

theorem MeasurableEquiv.map_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α} (f : α ≃ᵐ β) (s : Set β), ↑↑(MeasureTheory.Measure.map (⇑f) μ) s = ↑↑μ (⇑f ⁻¹' s)

MeasureTheory.ae_uIoc_iff

MeasureTheory.Measure.map_congr

theorem MeasureTheory.Measure.map_congr : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α} {f g : α → β}, μ.ae.EventuallyEq f g → MeasureTheory.Measure.map f μ = MeasureTheory.Measure.map g μ

MeasureTheory.Measure.sum_cond

theorem MeasureTheory.Measure.sum_cond : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ ν : MeasureTheory.Measure α), (MeasureTheory.Measure.sum fun b => bif b then μ else ν) = μ + ν

MeasureTheory.measure_biUnion₀

MeasureTheory.Measure.AbsolutelyContinuous.refl

theorem MeasureTheory.Measure.AbsolutelyContinuous.refl : ∀ {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α), μ.AbsolutelyContinuous μ

MeasureTheory.Measure.AbsolutelyContinuous.map

MeasureTheory.Measure.absolutelyContinuous_rfl

theorem MeasureTheory.Measure.absolutelyContinuous_rfl : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.AbsolutelyContinuous μ

MeasureTheory.le_toOuterMeasure_caratheodory

theorem MeasureTheory.le_toOuterMeasure_caratheodory : ∀ {α : Type u_1} [ms : MeasurableSpace α] (μ : MeasureTheory.Measure α), ms ≤ μ.caratheodory

MeasureTheory.Measure.AbsolutelyContinuous.mk

theorem MeasureTheory.Measure.AbsolutelyContinuous.mk : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, (∀ ⦃s : Set α⦄, MeasurableSet s → ↑↑ν s = 0 → ↑↑μ s = 0) → μ.AbsolutelyContinuous ν

MeasureTheory.Measure.QuasiMeasurePreserving.exists_preimage_eq_of_preimage_ae

MeasureTheory.NullMeasurableSet.preimage

MeasureTheory.Measure.comap_apply₀

MeasureTheory.Measure.map_of_not_aemeasurable

theorem MeasureTheory.Measure.map_of_not_aemeasurable : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β} {μ : MeasureTheory.Measure α}, ¬AEMeasurable f μ → MeasureTheory.Measure.map f μ = 0

MeasureTheory.Measure.sum_fintype

theorem MeasureTheory.Measure.sum_fintype : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} [inst : Fintype ι] (μ : ι → MeasureTheory.Measure α), MeasureTheory.Measure.sum μ = Finset.univ.sum fun i => μ i

MeasureTheory.measure_union

theorem MeasureTheory.measure_union : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α}, Disjoint s₁ s₂ → MeasurableSet s₂ → ↑↑μ (s₁ ∪ s₂) = ↑↑μ s₁ + ↑↑μ s₂

MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint₀

MeasureTheory.measure_biUnion_finset

MeasureTheory.Measure.measure_univ_ne_zero

theorem MeasureTheory.Measure.measure_univ_ne_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, ↑↑μ Set.univ ≠ 0 ↔ μ ≠ 0

MeasureTheory.Measure.add_apply

theorem MeasureTheory.Measure.add_apply : ∀ {α : Type u_1} {_m : MeasurableSpace α} (μ₁ μ₂ : MeasureTheory.Measure α) (s : Set α), ↑↑(μ₁ + μ₂) s = ↑↑μ₁ s + ↑↑μ₂ s

MeasureTheory.Measure.QuasiMeasurePreserving.comp

MeasurableEquiv.map_symm_map

theorem MeasurableEquiv.map_symm_map : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α} (e : α ≃ᵐ β), MeasureTheory.Measure.map (⇑e.symm) (MeasureTheory.Measure.map (⇑e) μ) = μ

MeasureTheory.Measure.map_smul

theorem MeasureTheory.Measure.map_smul : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] (c : ENNReal) (μ : MeasureTheory.Measure α) (f : α → β), MeasureTheory.Measure.map f (c • μ) = c • MeasureTheory.Measure.map f μ

AEMeasurable.nullMeasurable

theorem AEMeasurable.nullMeasurable : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : α → β}, AEMeasurable f μ → MeasureTheory.NullMeasurable f μ

MeasureTheory.Measure.map_apply

MeasureTheory.Measure.measure_toMeasurable_inter

theorem MeasureTheory.Measure.measure_toMeasurable_inter : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, MeasurableSet s → ↑↑μ t ≠ ⊤ → ↑↑μ (MeasureTheory.toMeasurable μ t ∩ s) = ↑↑μ (t ∩ s)

MeasurableEmbedding.map_apply

theorem MeasurableEmbedding.map_apply : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β}, MeasurableEmbedding f → ∀ (μ : MeasureTheory.Measure α) (s : Set β), ↑↑(MeasureTheory.Measure.map f μ) s = ↑↑μ (f ⁻¹' s)

MeasureTheory.Measure.ae_le_iff_absolutelyContinuous

theorem MeasureTheory.Measure.ae_le_iff_absolutelyContinuous : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ.ae ≤ ν.ae ↔ μ.AbsolutelyContinuous ν

MeasureTheory.Measure.QuasiMeasurePreserving.id

theorem MeasureTheory.Measure.QuasiMeasurePreserving.id : ∀ {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α), MeasureTheory.Measure.QuasiMeasurePreserving id μ μ

MeasureTheory.measure_diff_null'

theorem MeasureTheory.measure_diff_null' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α}, ↑↑μ (s₁ ∩ s₂) = 0 → ↑↑μ (s₁ \ s₂) = ↑↑μ s₁

MeasureTheory.Measure.le_sum

theorem MeasureTheory.Measure.le_sum : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} (μ : ι → MeasureTheory.Measure α) (i : ι), μ i ≤ MeasureTheory.Measure.sum μ

MeasureTheory.measure_diff

theorem MeasureTheory.measure_diff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α}, s₂ ⊆ s₁ → MeasurableSet s₂ → ↑↑μ s₂ ≠ ⊤ → ↑↑μ (s₁ \ s₂) = ↑↑μ s₁ - ↑↑μ s₂

MeasureTheory.Ioo_ae_eq_Ioc'

theorem MeasureTheory.Ioo_ae_eq_Ioc' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PartialOrder α] {a b : α}, ↑↑μ {b} = 0 → μ.ae.EventuallyEq (Set.Ioo a b) (Set.Ioc a b)

MeasureTheory.Measure.le_iff

theorem MeasureTheory.Measure.le_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ μ₂ : MeasureTheory.Measure α}, μ₁ ≤ μ₂ ↔ ∀ (s : Set α), MeasurableSet s → ↑↑μ₁ s ≤ ↑↑μ₂ s

MeasureTheory.tendsto_measure_iInter

MeasureTheory.Measure.smul_toOuterMeasure

theorem MeasureTheory.Measure.smul_toOuterMeasure : ∀ {α : Type u_1} {R : Type u_6} [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal] {_m : MeasurableSpace α} (c : R) (μ : MeasureTheory.Measure α), ↑(c • μ) = c • ↑μ

`MeasureTheory.ae_eq_bot`

`MeasureTheory.ae_mono`

`MeasureTheory.Measure.le_add_right`

`MeasureTheory.exists_nonempty_inter_of_measure_univ_lt_tsum_measure`

`MeasureTheory.measure_compl`

`MeasureTheory.Measure.QuasiMeasurePreserving.aemeasurable`

`MeasureTheory.Measure.le_iff'`

`LE.le.absolutelyContinuous_of_ae`

`MeasureTheory.Measure.AbsolutelyContinuous.rfl`

`MeasureTheory.Measure.QuasiMeasurePreserving.mono`

`MeasurableEquiv.map_apply`

`MeasureTheory.ae_uIoc_iff`

`MeasureTheory.Measure.map_congr`

`MeasureTheory.Measure.sum_cond`

`MeasureTheory.measure_biUnion₀`

`MeasureTheory.Measure.AbsolutelyContinuous.refl`

`MeasureTheory.Measure.AbsolutelyContinuous.map`

`MeasureTheory.Measure.absolutelyContinuous_rfl`

`MeasureTheory.le_toOuterMeasure_caratheodory`

`MeasureTheory.Measure.AbsolutelyContinuous.mk`

`MeasureTheory.Measure.QuasiMeasurePreserving.exists_preimage_eq_of_preimage_ae`

`MeasureTheory.NullMeasurableSet.preimage`

`MeasureTheory.Measure.comap_apply₀`

`MeasureTheory.Measure.map_of_not_aemeasurable`

`MeasureTheory.Measure.sum_fintype`

`MeasureTheory.measure_union`

`MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint₀`

`MeasureTheory.measure_biUnion_finset`

`MeasureTheory.Measure.measure_univ_ne_zero`

`MeasureTheory.Measure.add_apply`

`MeasureTheory.Measure.QuasiMeasurePreserving.comp`

`MeasurableEquiv.map_symm_map`

`MeasureTheory.Measure.map_smul`

`AEMeasurable.nullMeasurable`

`MeasureTheory.Measure.map_apply`

`MeasureTheory.Measure.measure_toMeasurable_inter`

`MeasurableEmbedding.map_apply`

`MeasureTheory.Measure.ae_le_iff_absolutelyContinuous`

`MeasureTheory.Measure.QuasiMeasurePreserving.id`

`MeasureTheory.measure_diff_null'`

`MeasureTheory.Measure.le_sum`

`MeasureTheory.measure_diff`

`MeasureTheory.Ioo_ae_eq_Ioc'`

`MeasureTheory.Measure.le_iff`

`MeasureTheory.tendsto_measure_iInter`

`MeasureTheory.Measure.smul_toOuterMeasure`

`MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint`

`MeasureTheory.Measure.absolutelyContinuous_of_le`

`MeasureTheory.Measure.AbsolutelyContinuous.ae_le`

`MeasureTheory.Measure.ae_mono'`

`MeasureTheory.Measure.le_add_left`

`MeasureTheory.Measure.map_zero`

`Mathlib.MeasureTheory.Measure.MeasureSpace._auxLemma.10`

`MeasureTheory.Measure.AbsolutelyContinuous.trans`

`Mathlib.MeasureTheory.Measure.MeasureSpace._auxLemma.27`

`Eq.absolutelyContinuous`

`MeasureTheory.ae_eq_of_subset_of_measure_ge`

`MeasureTheory.exists_nonempty_inter_of_measure_univ_lt_sum_measure`

`MeasureTheory.Measure.coe_zero`

`MeasureTheory.Measure.map_def`

`MeasureTheory.ae_eq_of_ae_subset_of_measure_ge`

`MeasureTheory.Ioi_ae_eq_Ici'`

`MeasureTheory.Measure.map_id'`

`MeasureTheory.Measure.QuasiMeasurePreserving.preimage_ae_eq`

`MeasureTheory.measure_diff_lt_of_lt_add`

`MeasureTheory.measure_limsup_eq_zero`

`MeasureTheory.measure_biUnion`

`MeasureTheory.Measure.eq_zero_of_isEmpty`

`MeasureTheory.Measure.zero_le`

`MeasureTheory.Measure.coe_add`

`MeasureTheory.Measure.absolutelyContinuous_refl`

`MeasureTheory.Ioo_ae_eq_Ico'`

`MeasureTheory.Iio_ae_eq_Iic'`

`MeasureTheory.sum_measure_preimage_singleton`