LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

`measurable_from_prod_countable` theorem measurable_from_prod_countable : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : Countable β] [inst : MeasurableSingletonClass β] {x : MeasurableSpace γ} {f : α × β → γ}, (∀ (y : β), Measurable fun x => f (x, y)) → Measurable f The theorem `measurable_from_prod_countable` states that given three types `α`, `β`, and `γ`, measurable spaces `α` and `β`, a countable type `β`, a measurable singleton class `β`, a measurable space `γ`, and a function `f` from the product of `α` and `β` to `γ`, if for every `y` in `β`, the function that takes an `x` in `α` and maps it to `f` applied to the pair `(x, y)` is measurable, then the function `f` itself is measurable. In other words, this theorem asserts that if a function from a product space is measurable when fixed by any element of a countable set, then the function is measurable. More concisely: If a function from the product of two measurable spaces, where one is countable, is measurable when fixed by each element in the countable space, then the function is measurable.
`MeasurableEquiv.symm_comp_self` theorem MeasurableEquiv.symm_comp_self : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β), ⇑e.symm ∘ ⇑e = id This theorem states that for any two types `α` and `β` equipped with a measurable space structure, given a measurable equivalence `e` from `α` to `β`, the composition of the inverse of `e` with `e` itself is the identity function. In other words, applying `e`, and then its inverse, to any element of `α` will yield the original element, which is the definition of an inverse in the context of functions. This is a fundamental property of all bijective (one-to-one and onto) functions, and it holds for measurable functions as well. More concisely: For any measurable equivalences `e : α ≡ β` between types `α` and `β` equipped with measurable space structures, `e ∘ e⁻¹ = id α`, where `id α` is the identity function on `α`.
`MeasurableEquiv.measurable` theorem MeasurableEquiv.measurable : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β), Measurable ⇑e This theorem states that for any two types `α` and `β` which are equipped with measurable spaces, any measurable equivalence `e` from `α` to `β` is a measurable function. In other words, if `e` is a bijective mapping from `α` to `β` such that both `e` and its inverse are measurable (i.e., the preimage of any measurable set under either function is measurable), then the function `e` itself is measurable. This means that for any measurable set in the codomain `β`, its preimage under `e` is a measurable set in the domain `α`. More concisely: If `α` and `β` are measurable spaces and `e: α → β` is a bijective measurable function with measurable inverse, then `e` is a measurable function.
`measurable_liftCover` theorem measurable_liftCover : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort uι} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : Countable ι] (t : ι → Set α), (∀ (i : ι), MeasurableSet (t i)) → ∀ (f : (i : ι) → ↑(t i) → β), (∀ (i : ι), Measurable (f i)) → ∀ (hf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩) (htU : ⋃ i, t i = Set.univ), Measurable (Set.liftCover t f hf htU) The theorem `measurable_liftCover` states that given a countable covering of a measurable space `α` by measurable sets, denoted by `t i` for each `i` in the countable index set `ι`, and a family of functions `f i` that agree on the intersections of the covering sets `t i ∩ t j`, the function `Set.liftCover t f _ _`, which is defined as `f i ⟨x, hx⟩` for `hx : x ∈ t i`, is measurable. The function `Set.liftCover t f _ _` is essentially a function that "glues" together the family of functions `f i` defined on each of the covering sets. The requirement that the `f i` agree on the intersections ensures that this "gluing" is well-defined. The countable covering is required to be a covering, i.e., the union of all the sets `t i` equals the entire space `α`. More concisely: Given a countable covering of a measurable space by measurable sets and a family of measurable functions agreeing on their intersections, the function obtained by lifting these functions using `Set.liftCover` is measurable.
`MeasurableSpace.generateFrom_singleton` theorem MeasurableSpace.generateFrom_singleton : ∀ {α : Type u_1} (s : Set α), MeasurableSpace.generateFrom {s} = MeasurableSpace.comap (fun x => x ∈ s) ⊤ := by sorry The theorem `MeasurableSpace.generateFrom_singleton` states that for any given set `s` of any type `α`, the sigma-algebra (which is a collection of subsets closed under countable unions and the complement operation) generated by a single set `s` is equal to the reverse image of the universal measurable space (represented by `⊤`) under the function that maps an element `x` to its membership in `s`. Here, the reverse image of a measurable space under a function contains the sets whose preimages under the function are measurable sets. This theorem thus equates two different ways of creating a measurable space: one by generating from a single set, and the other by mapping the universal space through "membership in `s`". More concisely: The sigma-algebra generated by a single set is equal to the reverse image of the universal measurable space under the function defining membership in that set.
`exists_measurable_piecewise` theorem exists_measurable_piecewise : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {ι : Type u_6} [inst : Countable ι] [inst : Nonempty ι] (t : ι → Set α), (∀ (n : ι), MeasurableSet (t n)) → ∀ (g : ι → α → β), (∀ (n : ι), Measurable (g n)) → (Pairwise fun i j => Set.EqOn (g i) (g j) (t i ∩ t j)) → ∃ f, Measurable f ∧ ∀ (n : ι), Set.EqOn f (g n) (t n) This theorem states that given a countable family of nonempty measurable sets `t i` in a measurable space `α`, and a family of measurable functions `g i : α → β` such that any two functions `g i` and `g j` agree on the intersection of their corresponding sets `t i` and `t j`, there exists a measurable function `f : α → β` that agrees with each function `g i` on its corresponding set `t i`. The existence of a nonempty index set `ι` is only required to prove the existence of the function `f`. More concisely: Given a countable family of nonempty measurable sets `{Ti : α \| i ∈ I}` and a family of measurable functions `{gi : α -> β \| i ∈ I}` with pairwise agreeing restrictions to their intersections `{gi \| Ti},` there exists a measurable function `f : α -> β` agreeing with each `gi` on `Ti`.
`MeasurableEquiv.coe_toEquiv` theorem MeasurableEquiv.coe_toEquiv : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β), ⇑e.toEquiv = ⇑e This theorem states that for any two types `α` and `β` that have associated measurable spaces, given a measurable equivalence `e` between `α` and `β`, the function representation of `e` as an equivalence (via `e.toEquiv`) is the same as the function representation of `e` itself. In other words, converting a measurable equivalence to a regular equivalence doesn't change how it behaves as a function. More concisely: For any measurable equivalences `e : α ≃ β`, the functions `e` and `e.toEquiv` represent the same relation between `α` and `β`.
`measurable_update` theorem measurable_update : ∀ {δ : Type u_4} {π : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (π a)] (f : (a : δ) → π a) {a : δ} [inst_1 : DecidableEq δ], Measurable (Function.update f a) The theorem `measurable_update` states that for all types `δ` and `π` which is a function from `δ` to some type, and for all functions `f` from `δ` to `π a`, and for a particular `a` of type `δ`, if we have decidable equality on `δ`, then the function `update f a` which replaces the value of `f` at `a` with a given value, is measurable. This means that the preimage of any measurable set under `update f a` is also measurable. This holds irrespective of whether the original function `f` was measurable. It's worth noting that this should not be confused with asserting that `update f a x` is measurable for a specific `x`. More concisely: For any decidable type `δ` and function `f : δ → π`, the update function `update f a : π` is measurable, meaning the preimage of any measurable set under `update f a` is also measurable.
`MeasurableSet.mem` theorem MeasurableSet.mem : ∀ {α : Type u_1} {s : Set α} [inst : MeasurableSpace α], MeasurableSet s → Measurable fun x => x ∈ s The theorem `MeasurableSet.mem` states that for any type `α` and set `s` of `α`, in a given measurable space over `α`, if `s` is a measurable set, then the function that maps elements `x` to the proposition "`x` is an element of `s`" is a measurable function. In terms of measure theory, this essentially means that the characteristic function (or indicator function) of a measurable set is always measurable. More concisely: The characteristic function of a measurable set in a measurable space is measurable.
`Measurable.find` theorem Measurable.find : ∀ {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {x : MeasurableSpace α} {f : ℕ → α → β} {p : ℕ → α → Prop} [inst : (n : ℕ) → DecidablePred (p n)], (∀ (n : ℕ), Measurable (f n)) → (∀ (n : ℕ), MeasurableSet {x \| p n x}) → ∀ (h : ∀ (x : α), ∃ n, p n x), Measurable fun x => f (Nat.find ⋯) x This theorem states that a piecewise defined function, across countably many pieces, is measurable if all the individual pieces (functions) are measurable and all the sets that define the pieces are measurable sets. Here, the function is divided based on a natural number indexed predicate 'p'. The piecewise function is defined as the function 'f' evaluated at the natural number 'n' satisfying the predicate 'p' for a given input from the domain. The existence of such 'n' for every input is guaranteed by the condition 'h'. The decision of whether a value satisfies the predicate 'p' for a given 'n' is determined by a decidable predicate. More concisely: If a piecewise function, defined over countably many measurable sets using a measurable predicate and measurable pieces, is such that for every input there exists a unique index satisfying the decidable predicate, then the function is measurable.
`MeasurableEmbedding.measurableSet_image` theorem MeasurableEmbedding.measurableSet_image : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}, MeasurableEmbedding f → ∀ {s : Set α}, MeasurableSet (f '' s) ↔ MeasurableSet s The theorem `MeasurableEmbedding.measurableSet_image` states that for any types `α` and `β`, a measurable space `mα` on `α`, a measurable space instance on `β`, and a function `f` from `α` to `β`, if `f` is a measurable embedding, then a set `s` of type `α` has a measurable image under `f` if and only if the set `s` itself is measurable. In other words, the measurability of the image of a set under a measurable embedding is equivalent to the measurability of the original set. More concisely: A measurable embedding of sets preserves measurability: if `f: α → β` is a measurable embedding between measurable spaces `(α, mα)` and `(β, mβ)`, then for any set `s ⊆ α`, `f``[s]` is measurable if and only if `s` is measurable.
`MeasurableEquiv.ext` theorem MeasurableEquiv.ext : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {e₁ e₂ : α ≃ᵐ β}, ⇑e₁ = ⇑e₂ → e₁ = e₂ The theorem `MeasurableEquiv.ext` states the following: Given two types `α` and `β` where `α` and `β` both have measurable spaces respectively, and given two measurable equivalences `e₁` and `e₂` between `α` and `β`, if the function of `e₁` is equal to the function of `e₂`, then `e₁` is equal to `e₂`. In other words, this is a statement about the uniqueness of a measurable equivalence between two measurable spaces - if two measurable equivalences have the same function, they are indeed the same measurable equivalence. More concisely: If `α` and `β` are measurable spaces and `e₁` and `e₂` are measurable equivalences from `α` to `β` with equal functions, then `e₁ = e₂`.
`Measurable.snd` theorem Measurable.snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β × γ}, Measurable f → Measurable fun a => (f a).2 The theorem `Measurable.snd` states that for any types `α`, `β`, and `γ`, and measurable spaces `m` over `α`, `mβ` over `β`, and `mγ` over `γ`, if we have a measurable function `f` mapping from `α` to a pair of elements in `β` and `γ`, then the function that takes an element from `α` and returns the second component from the pair produced by `f` is also measurable. In other words, if `f` is a measurable function, then the function that gets the second component (`.2`) of `f(a)` for any `a` in `α` is also measurable. More concisely: Given measurable spaces `m` over `α`, `mβ` over `β`, and `mγ` over `γ`, if `f` is a measurable function from `α` to the product `β × γ`, then the projection function to the second component `.2` is measurable.
`MeasurableEquiv.measurable_comp_iff` theorem MeasurableEquiv.measurable_comp_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [inst_2 : MeasurableSpace γ] {f : β → γ} (e : α ≃ᵐ β), Measurable (f ∘ ⇑e) ↔ Measurable f This theorem states that for any three types `α`, `β`, and `γ`, each with an associated measurable space, a function `f` that maps `β` to `γ`, and an equivalence `e` between `α` and `β` (denoted `α ≃ᵐ β`), the function `f` composed with the inverse of `e` is measurable if and only if `f` itself is measurable. In other words, the measurability of the composed function `f ∘ ⇑e` is equivalent to the measurability of the function `f`. Measurability here means that the preimage of every measurable set under the function is also a measurable set. More concisely: For any measurable functions `f: β → γ` and `e: α ≃ᵐ β` with `α, β, γ` being measurable spaces, the composed function `f ∘ e⁻¹` is measurable if and only if `f` is measurable.
`MeasurableEquiv.measurable_invFun` theorem MeasurableEquiv.measurable_invFun : ∀ {α : Type u_6} {β : Type u_7} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (self : α ≃ᵐ β), Measurable ⇑self.symm This theorem states that for any measurable spaces `α` and `β`, the inverse function of a measurable equivalence (a bijective function whose inverse is also measurable) from `α` to `β` is measurable. In other words, if we have a measurable equivalence `self` from `α` to `β`, then the inverse function of `self` (denoted as `self.symm` in Lean) is measurable. A function is considered measurable if the preimage of every measurable set under the function is also a measurable set. More concisely: If `self : α → β` is a bijective measurable function with measurable inverse, then `self.symm : β → α` is measurable.
`Measurable.ite` theorem Measurable.ite : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : α → Prop} {x : DecidablePred p}, MeasurableSet {a \| p a} → Measurable f → Measurable g → Measurable fun x_1 => if p x_1 then f x_1 else g x_1 This theorem, `Measurable.ite`, states that for any two types `α` and `β`, any two functions `f` and `g` from `α` to `β`, any measurable space `m` on `α`, any measurable space `mβ` on `β`, and any decidable predicate `p` on `α`, if the set `{a \| p a}` is a measurable set, and if both functions `f` and `g` are measurable, then the function which takes an input `x_1` and outputs `f x_1` if `p x_1` is true, else outputs `g x_1`, is also measurable. This theorem is slightly different from `Measurable.piecewise` and can be used to show that functions like `Measurable (ite (x=0) 0 1)` are measurable. More concisely: If `p` is a decidable predicate on measurable space `(α, m)`, `f` and `g` are measurable functions from `α` to `β`, and the set `{a \| p a}` is measurable, then the function `x ↦ if p x then f x else g x` is measurable from `(α, m)` to `(β, mβ)`.
`measurable_sum` theorem measurable_sum : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : MeasurableSpace γ} {f : α ⊕ β → γ}, Measurable (f ∘ Sum.inl) → Measurable (f ∘ Sum.inr) → Measurable f The theorem `measurable_sum` states that for all types `α`, `β`, and `γ` with measurable spaces `m`, `mβ`, and `x`, respectively, if a function `f` from the sum type `α ⊕ β` to `γ` is such that both the composition of `f` with `Sum.inl` and the composition of `f` with `Sum.inr` are measurable, then `f` itself is measurable. Here `Sum.inl` and `Sum.inr` cover the left and right inclusion maps from `α` and `β` into the sum type `α ⊕ β`. In other words, if `f` is measurable when restricted to both parts of the sum type, then it is measurable on the entire sum type. More concisely: If the restriction of a function between sum types to each summand is measurable, then the function is measurable.
`MeasurableEmbedding.comap_eq` theorem MeasurableEmbedding.comap_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β}, MeasurableEmbedding f → MeasurableSpace.comap f inst_1 = inst The theorem `MeasurableEmbedding.comap_eq` asserts that for any two types `α` and `β` equipped with measurable spaces, and a function `f : α → β`, if `f` is a measurable embedding, then the reverse image of the measurable space under the function `f` is the same as the original measurable space on `α`. In other words, if we take the measurable space of `β` and map it back along `f` to `α`, we get the same measurable space that `α` started with. This is significant in the context of measure theory, where measurable spaces are used to define measures. More concisely: If `f : α → β` is a measurable embedding between measurable spaces `(α, Σα)` and `(β, Σβ)`, then `f⁻¹(Σβ) = Σα`.
`MeasurableSpace.le_map_comap` theorem MeasurableSpace.le_map_comap : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {g : β → α}, m ≤ MeasurableSpace.map g (MeasurableSpace.comap g m) The theorem `MeasurableSpace.le_map_comap` says that for any types `α` and `β`, for any measurable space `m` on `α`, and for any function `g` from `β` to `α`, the measurable space `m` is a sub-measurable-space of the forward image under `g` of the reverse image under `g` of `m`. Here, `MeasurableSpace.map g (MeasurableSpace.comap g m)` creates a measurable space where the measurable sets are those whose preimage under `g` is a measurable set in the measurable space created by the reverse image of `m` under `g`. The inequality `m ≤ MeasurableSpace.map g (MeasurableSpace.comap g m)` means that every set which is measurable in `m` is also measurable in `MeasurableSpace.map g (MeasurableSpace.comap g m)`. More concisely: For any measurable space `m` on type `α` and any function `g` from type `β` to `α`, the reverse image of `m` under `g` is a measurable sub-set of `α`, so the forward image of `m` under `g` is a measurable space and every measurable set in `m` is measurable in this forward image under `g`.
`measurable_fst` theorem measurable_fst : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {x_1 : MeasurableSpace β}, Measurable Prod.fst The theorem `measurable_fst` states that for any types `α` and `β` and any measurable spaces over `α` and `β`, the first projection function, `Prod.fst`, is measurable. In mathematical terms, this means that for any measurable set in `α`, its preimage under the `Prod.fst` function (which projects an element of the product space `α × β` to `α`) is also a measurable set. More concisely: The first projection function `Prod.fst` of a product space is measurable, that is, for any measurable set in the first factor space, its preimage under `Prod.fst` is also measurable.
`exists_measurable_piecewise_nat` theorem exists_measurable_piecewise_nat : ∀ {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {m : MeasurableSpace α} (t : ℕ → Set β), (∀ (n : ℕ), MeasurableSet (t n)) → Pairwise (Disjoint on t) → ∀ (g : ℕ → β → α), (∀ (n : ℕ), Measurable (g n)) → ∃ f, Measurable f ∧ ∀ (n : ℕ), ∀ x ∈ t n, f x = g n x The theorem `exists_measurable_piecewise_nat` states that given countably many measurable sets `t n` that are pairwise disjoint, and countably many measurable functions `g n`, we can construct a measurable function `f` such that for each natural number `n`, the function `f` coincides with `g n` on the set `t n`. In other words, for every `n` and every `x` in the set `t n`, we have `f(x) = g(n)(x)`. This theorem is a form of the piecemeal construction of measurable functions, leveraging the fact that we can define a function by specifying its behavior on subsets of the domain. More concisely: Given countably many pairwise disjoint measurable sets and countably many measurable functions, there exists a measurable function coinciding with each given function on its respective set.
`MeasurableSet.pi` theorem MeasurableSet.pi : ∀ {δ : Type u_4} {π : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (π a)] {s : Set δ} {t : (i : δ) → Set (π i)}, s.Countable → (∀ i ∈ s, MeasurableSet (t i)) → MeasurableSet (s.pi t) The theorem `MeasurableSet.pi` states that for any type `δ`, a function `π` mapping `δ` to some type, and a given measurable space for each `δ`, if we have a countable set `s` of type `δ` and a family of sets `t` where each set `t i` is a set of type `π i`, then if all sets `t i` where `i` belongs to `s` are measurable sets, the set `Set.pi s t` of dependent functions `f : Πa, π a` such that `f a` belongs to `t a` whenever `a ∈ s` is also a measurable set. In simpler terms, it means if we have a collection of measurable sets indexed by a countable set, then the set of all functions that map each index to its corresponding set is also measurable. More concisely: If `π : δ →* X` is a function, `s : set δ` is countable, and `t i : set (π i)` is measurable for each `i ∈ s`, then `Set.image (λ a : s, t a) (λ a : δ, π a)` is a measurable subset of `X^s`.
`Subsingleton.measurable` theorem Subsingleton.measurable : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [inst_2 : Subsingleton α], Measurable f The theorem `Subsingleton.measurable` states that for any types `α` and `β`, and any function `f` from `α` to `β`, if `α` is a subsingleton type and both `α` and `β` are measurable spaces, then the function `f` is measurable. A type is a subsingleton if it has at most one element, and a function is measurable if the preimage of every measurable set is measurable. This means that for every measurable set in the codomain, the set of all elements in the domain that map to that set is also measurable. More concisely: If `α` is a subsingleton type and both `α` and `β` are measurable spaces, then the function `f` from `α` to `β` is measurable.
`measurable_indicator_const_iff` theorem measurable_indicator_const_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : Zero β] [inst_1 : MeasurableSingletonClass β] (b : β) [inst_2 : NeZero b], Measurable (s.indicator fun x => b) ↔ MeasurableSet s The theorem `measurable_indicator_const_iff` states that for any types `α` and `β`, a set `s` of type `α`, measurable spaces `m` and `mβ` for `α` and `β` respectively, a zero instance of type `β` and a non-zero constant `b` of type `β`, the measurability of the set `s` is equivalent to the measurability of the indicator function of the set `s` that takes on the constant value `b` for elements in the set `s` and `0` elsewhere. In other words, a set is measurable if and only if its indicator function, which outputs a constant non-zero value for elements within the set and zero for those outside, is also measurable. More concisely: A set is measurable if and only if its indicator function, which takes the constant value of a non-zero element for set elements and zero elsewhere, is measurable.
`measurable_swap_iff` theorem measurable_swap_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : MeasurableSpace γ} {f : α × β → γ}, Measurable (f ∘ Prod.swap) ↔ Measurable f This theorem, `measurable_swap_iff`, states that for any types `α`, `β`, and `γ` with measurable spaces `m`, `mβ`, and `x` respectively, and for any function `f` from the product of `α` and `β` to `γ`, the function `f` is measurable if and only if the function `f` composed with the product swap function is measurable. The product swap function `Prod.swap` takes a pair and switches the elements, so this theorem is about the measurability of a function under the rearrangement of its input variables. More concisely: For measurable spaces (m, α, β, γ) and a measurable function f : α × β → γ, the function f is measurable if and only if f ∘ Prod.swap is measurable, where Prod.swap is the product swap function.
`MeasurableEmbedding.injective` theorem MeasurableEmbedding.injective : ∀ {α : Type u_6} {β : Type u_7} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β}, MeasurableEmbedding f → Function.Injective f The theorem states that for any two types `α` and `β`, where `α` and `β` are both measurable spaces, any function `f` from `α` to `β` that is a measurable embedding is also injective. In mathematical terms, this means that if `f` is a measurable embedding (which implies that it is a function that preserves the structure of the measurable spaces), then for any two elements `a₁` and `a₂` in `α`, if `f(a₁)` equals `f(a₂)`, it must be the case that `a₁` equals `a₂`. The injectiveness of `f` ensures that no two distinct elements of `α` map to the same element in `β`, preserving the uniqueness of the elements under the function `f`. More concisely: If `f : α -> β` is a measurable embedding between measurable spaces `α` and `β`, then `f` is injective.
`MeasurableEmbedding.id` theorem MeasurableEmbedding.id : ∀ {α : Type u_1} {mα : MeasurableSpace α}, MeasurableEmbedding id This theorem states that, for any type `α` and any measurable space `mα` over `α`, the identity function is a measurable embedding. In other words, it ensures that the identity function, which leaves every input unchanged, preserves the measurable structure of a space. This means that it maps measurable sets to measurable sets and is injective, which is a property required for measurable embeddings. More concisely: The identity function is a measurable embedding for any measurable space.
`Measurable.of_le_map` theorem Measurable.of_le_map : ∀ {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β}, m₂ ≤ MeasurableSpace.map f m₁ → Measurable f This theorem, also known as the reverse direction of `measurable_iff_le_map`, states that for any two types `α` and `β`, and measurable spaces `m₁` and `m₂` on `α` and `β` respectively, and a function `f` mapping `α` to `β`, if `m₂` is less than or equal to the forward image of `m₁` under `f` (i.e., `m₂ ≤ MeasurableSpace.map f m₁`), then `f` is a measurable function. In other words, if the preimage of every set in `m₂` under `f` is a measurable set in `m₁`, then `f` is a measurable function. More concisely: If a function between measurable spaces satisfies the preimage of every measurable set under the function being measurable in the domain space, then the function is measurable.
`measurable_prod_mk_left` theorem measurable_prod_mk_left : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x) The theorem `measurable_prod_mk_left` states that for all types `α` and `β`, given measurable spaces `m` over `α` and `mβ` over `β`, and for any element `x` of type `α`, the function `Prod.mk x`, which creates a pair with `x` as the first element and a variable element of type `β` as the second, is a measurable function. In other words, the preimage of any measurable set under this function is also a measurable set. More concisely: For measurable spaces (m : MeasurableSpace α) and (mβ : MeasurableSpace β), the function Prod.mk : α → α × β is measurable.
`MeasurableSet.preimage` theorem MeasurableSet.preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {t : Set β}, MeasurableSet t → Measurable f → MeasurableSet (f ⁻¹' t) The theorem `MeasurableSet.preimage` states that for any two types `α` and `β`, a function `f` from `α` to `β`, and a set `t` of type `β`, if `t` is a measurable set and the function `f` is measurable, then the preimage of `t` under `f` is also a measurable set. In other words, it asserts that the preimage of a measurable set through a measurable function retains the property of measurability. Here, measurability of a set is defined in the context of a given measure space, and a function is considered measurable if the preimage of every measurable set is measurable. More concisely: If `f` is a measurable function and `t` is a measurable subset of `β`, then the preimage `f⁻¹(t)` is a measurable subset of `α`.
`Measurable.of_comap_le` theorem Measurable.of_comap_le : ∀ {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β}, MeasurableSpace.comap f m₂ ≤ m₁ → Measurable f This theorem, "Measurable.of_comap_le", states that for any types `α` and `β`, any measurable spaces `m₁` over `α` and `m₂` over `β`, and any function `f` from `α` to `β`, if the measurable space obtained by taking the reverse image of `m₂` under `f` is less than or equal to `m₁`, then `f` is a measurable function. In other words, if every set in `m₁` that is the preimage of a set in `m₂` under `f` is also in `m₂`, then `f` is measurable, i.e., the preimage of every measurable set under `f` is also measurable. More concisely: If a function between measurable spaces preserves measurable sets under reverse image, then the function is measurable.
`Measurable.fst` theorem Measurable.fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β × γ}, Measurable f → Measurable fun a => (f a).1 This theorem states that for any types `α`, `β`, and `γ`, and for any measurable spaces over these types denoted by `m`, `mβ`, and `mγ` respectively, if we have a measurable function `f` mapping from `α` to a pair of elements in `β` and `γ`, then the function that maps `α` to the first component of the pair `(f a).1` is also measurable. In mathematical terms, if `f : α → β × γ` is a measurable function, then the function `g : α → β` defined by `g(a) = (f(a)).1` is also measurable. More concisely: If `f : α → β × γ` is a measurable function, then the function `g : α → β` defined by `g(a) = (f(a)).1` is measurable.
`MeasurableEmbedding.measurableSet_range` theorem MeasurableEmbedding.measurableSet_range : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}, MeasurableEmbedding f → MeasurableSet (Set.range f) This theorem, named `MeasurableEmbedding.measurableSet_range`, states that for any two types `α` and `β`, given a measurable space on `α` and `β`, and a function `f` from `α` to `β`, if `f` is a measurable embedding, then the range of `f` is a measurable set. In other words, the theorem asserts that the image of the measurable space `α` under the function `f` is also measurable. This is a fundamental property in measure theory. More concisely: If `f` is a measurable embedding from the measurable space `(α, Σα)` to the measurable space `(β, Σβ)`, then the range of `f` is a measurable set in `(β, Σβ)`.
`MeasurableEmbedding.comp` theorem MeasurableEmbedding.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] {f : α → β} {g : β → γ}, MeasurableEmbedding g → MeasurableEmbedding f → MeasurableEmbedding (g ∘ f) This theorem states that for every three types `α`, `β`, and `γ` with associated measurable spaces `mα`, `inst`, and `inst_1` respectively, and for every two functions `f` from `α` to `β` and `g` from `β` to `γ`, if `g` and `f` are measurable embeddings, then the composition of `g` and `f` (denoted as `g ∘ f`) is also a measurable embedding. In other words, the composition of two measurable embeddings is always a measurable embedding. More concisely: If `f: α → β` and `g: β → γ` are measurable embeddings, then their composition `g ∘ f` is also a measurable embedding.
`MeasurableEmbedding.measurableSet_image'` theorem MeasurableEmbedding.measurableSet_image' : ∀ {α : Type u_6} {β : Type u_7} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β}, MeasurableEmbedding f → ∀ ⦃s : Set α⦄, MeasurableSet s → MeasurableSet (f '' s) The theorem `MeasurableEmbedding.measurableSet_image'` states that if we have a measurable set `s` in a measurable space `α`, and a measurable embedding function `f` from `α` to another measurable space `β`, then the image of the set `s` under the function `f` is also a measurable set in `β`. In other words, the image of a measurable set under a measurable embedding is itself measurable, preserving the measurability property under the function transformation. More concisely: If `s` is a measurable set in a measurable space `α` and `f` is a measurable embedding from `α` to a measurable space `β`, then `f''s` is a measurable set in `β`.
`measurable_of_measurable_on_compl_singleton` theorem measurable_of_measurable_on_compl_singleton : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : MeasurableSingletonClass α] {f : α → β} (a : α), Measurable ({x \| x ≠ a}.restrict f) → Measurable f The theorem `measurable_of_measurable_on_compl_singleton` states that for any types `α` and `β`, any measurable spaces `m` over `α` and `mβ` over `β`, any measurable singleton class over `α`, and any function `f` from `α` to `β`, if the restriction of the function `f` to the set of all elements in `α` that are not equal to a given element `a` (denoted as `{x \| x ≠ a}`) is measurable, then the function `f` itself is measurable. This means that if we know the behavior of a function on all elements except for one, and that behavior is measurable, then the function itself is measurable. More concisely: If a function between measurable spaces is measurable on the complement of a single element, then it is measurable.
`Measurable.piecewise` theorem Measurable.piecewise : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f g : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : DecidablePred fun x => x ∈ s}, MeasurableSet s → Measurable f → Measurable g → Measurable (s.piecewise f g) The theorem `Measurable.piecewise` states that for any types `α` and `β`, a set `s` of type `α`, functions `f` and `g` mapping from `α` to `β`, and measurable spaces `m` over `α` and `mβ` over `β`, if the set membership of `s` is a decidable predicate, and if the set `s` is measurable, and both functions `f` and `g` are measurable, then the `piecewise` function which is equal to `f` on the set `s`, and equal to `g` on the complement of `s`, is also measurable. In other words, creating a function that operates differently on a measurable set and its complement preserves measurability. More concisely: If a measurable set and its complement are given, and the set membership is decidable, then the piecewise function that is measurable on the set and another measurable function on its complement is also measurable.
`MeasurableSpace.gc_comap_map` theorem MeasurableSpace.gc_comap_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), GaloisConnection (MeasurableSpace.comap f) (MeasurableSpace.map f) The theorem `MeasurableSpace.gc_comap_map` states that for any function `f` from type `α` to type `β`, there exists a Galois connection between the reverse image function (`MeasurableSpace.comap f`) and the forward image function (`MeasurableSpace.map f`) of a measurable space. This essentially means that for any two sets `a` and `b` from the measurable spaces `α` and `β` respectively, the set `a` is a subset of the preimage of `b` under `f` if and only if the image of `a` under `f` is a subset of `b`. These conditions of the Galois connection establish a correspondence between the comap and map of the given function `f`. More concisely: The theorem `MeasurableSpace.gc_comap_map` asserts that for any function `f` between measurable spaces, the reverse image function `MeasurableSpace.comap f` and forward image function `MeasurableSpace.map f` form a Galois connection, that is, `a ⊆ f⁻¹[b] < Rav equiv b ⊆ f[a]`.
`MeasurableSet.inl_image` theorem MeasurableSet.inl_image : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α}, MeasurableSet s → MeasurableSet (Sum.inl '' s) The theorem `MeasurableSet.inl_image` states that for any type `α` and `β`, any measurable space `m` on `α` and `mβ` on `β`, and any set `s` of elements of type `α`, if `s` is a measurable set, then the image of `s` under the `Sum.inl` function, which is a set of elements of type `Sum α β`, is also a measurable set. This theorem is an alias of the reverse direction of the property `measurableSet_inl_image`, meaning that it represents the same concept but in a different direction. More concisely: If `s` is a measurable subset of type `α` in the measurable space `m`, then the image `Sum.inl[s]` is a measurable subset of type `Sum α β` in the product measurable space `m ⊤ x mβ`, where `m⊤` is the completion of `m`.
`Measurable.indicator` theorem Measurable.indicator : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : Zero β], Measurable f → MeasurableSet s → Measurable (s.indicator f) The theorem `Measurable.indicator` states that for any types `α` and `β`, a set `s` of type `α`, a function `f` mapping from `α` to `β`, and measurable spaces `m` over `α` and `mβ` over `β`, if the type `β` has a zero element (`inst : Zero β`), then if the function `f` is measurable and the set `s` is a measurable set, the function `Set.indicator s f` is also measurable. Here, `Set.indicator s f` is a function that takes an element of `α` and returns `f` of that element if the element is in set `s`, and returns `0` otherwise. More concisely: If `α` is a type, `s` is a measurable set of `α`, `f : α -> β` is a measurable function with `β` having a zero element, then `Set.indicator s f : α -> β` is a measurable function.
`measurable_pi_lambda` theorem measurable_pi_lambda : ∀ {α : Type u_1} {δ : Type u_4} {π : δ → Type u_6} [inst : MeasurableSpace α] [inst_1 : (a : δ) → MeasurableSpace (π a)] (f : α → (a : δ) → π a), (∀ (a : δ), Measurable fun c => f c a) → Measurable f This theorem, denoted as `measurable_pi_lambda`, states that for all types `α` and `δ`, and a type function `π : δ → Type`, given that `α` and `π a` (for each `a : δ`) are measurable spaces, if a function `f : α → (a : δ) → π a` has the property that for every `a : δ`, the function `fun c => f c a` is measurable, then the function `f` itself is measurable. In other words, if every "slice" of `f` along the `δ` direction is measurable, then `f` is measurable. Here, a function is defined as measurable if the preimage of every measurable set is also measurable. More concisely: If `f : α → δ → π a` is a function such that for all `a : δ`, the function `fun c => f c a` is measurable, then `f` is measurable with respect to the product measurable space `(α × δ, ℱα × ℱδ)`, where `ℱα` and `ℱδ` are the sigma-algebras on `α` and `δ` respectively.
`Measurable.subtype_mk` theorem Measurable.subtype_mk : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : β → Prop} {f : α → β}, Measurable f → ∀ {h : ∀ (x : α), p (f x)}, Measurable fun x => ⟨f x, ⋯⟩ The theorem `Measurable.subtype_mk` states that for all types `α` and `β` with measurable spaces `m` and `mβ` respectively, for any property `p` of `β` and any function `f` from `α` to `β`, if `f` is a measurable function and, for all `x` in `α`, `p (f x)` holds, then the function that maps `x` to the subtype `{ val := f x, property := ⋯ }` is also measurable. Here, the subtype `{ val := f x, property := ⋯ }` is the set of elements of `β` that satisfy the property `p` and its measurability means that the preimage of any measurable set under this function is also measurable. More concisely: If `f` is a measurable function from a measurable space `(α, m)` to another measurable space `(β, mβ)`, and for all `x` in `α`, `p(f x)` holds where `p` is a property of `β`, then the function that maps `x` to the subtype `{val := f x, property := p(f x)}` is also measurable.
`Mathlib.MeasureTheory.MeasurableSpace.Basic._auxLemma.25` theorem Mathlib.MeasureTheory.MeasurableSpace.Basic._auxLemma.25 : ∀ {α : Type u_1} {δ : Type u_4} {π : δ → Type u_6} [inst : MeasurableSpace α] [inst_1 : (a : δ) → MeasurableSpace (π a)] {g : α → (a : δ) → π a}, Measurable g = ∀ (a : δ), Measurable fun x => g x a This theorem states that for any types `α` and `β`, and for any measurable spaces `m` on `α` and `mβ` on `β`, a set `s` of the disjoint union of `α` and `β` is measurable if and only if the preimage of `s` under the left injection (`Sum.inl`) and the preimage of `s` under the right injection (`Sum.inr`) are both measurable. In other words, a set in the disjoint union space is measurable when its corresponding subsets in the original spaces are measurable. More concisely: A set in the disjoint union of two measurable spaces is measurable if and only if its subsets under the left and right injections are measurable.
`measurable_pi_iff` theorem measurable_pi_iff : ∀ {α : Type u_1} {δ : Type u_4} {π : δ → Type u_6} [inst : MeasurableSpace α] [inst_1 : (a : δ) → MeasurableSpace (π a)] {g : α → (a : δ) → π a}, Measurable g ↔ ∀ (a : δ), Measurable fun x => g x a The theorem `measurable_pi_iff` states that for any types `α`, `δ` and a type function `π : δ → Type`, given measurable spaces over `α` and each type `π a` for `a : δ`, a function `g : α → (a : δ) → π a` is measurable if and only if for every `a : δ`, the function `fun x => g x a` is measurable. In simpler words, a function `g` that maps a value from one measurable space to a function in another measurable space is measurable if all functions that result from fixing an argument `a` in the second space are measurable. This theorem connects the notion of measurability of a function in the context of measurable spaces with the measurability of its partial application functions. More concisely: A function `g : α → δ → π a` is measurable with respect to the measurable spaces over `α` and each `π a` if and only if for every `a : δ`, the function `fun x => g x a` is measurable.
`Measurable.iterate` theorem Measurable.iterate : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α}, Measurable f → ∀ (n : ℕ), Measurable f^[n] The theorem `Measurable.iterate` states that for any type `α` and a measurable space `m` defined over that type, if a function `f` from `α` to `α` is measurable, then for any natural number `n`, the `n`-th iteration of the function `f` is also measurable. In mathematical terms, it means that if the preimage of every measurable set under `f` is measurable, then the preimage of every measurable set under the `n`-th iteration of `f` is measurable as well. More concisely: If `α` is a type with a measurable space `m`, and `f : α -> α` is measurable, then for every natural number `n`, the `n`-th iteration `f^n` of `f` is also measurable. That is, for every measurable set `A`, the preimage `f^(-1)(A)` under `f^n` is measurable.
`measurable_to_countable` theorem measurable_to_countable : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Countable α] [inst_2 : MeasurableSpace β] {f : β → α}, (∀ (y : β), MeasurableSet (f ⁻¹' {f y})) → Measurable f The theorem `measurable_to_countable` states that for any types `α` and `β` with `α` being countable, and both being measurable spaces, if a function `f` from `β` to `α` has the property that the preimage of each singleton set `{f y}` under `f` is a measurable set for every `y` in `β`, then the function `f` itself is measurable. In other words, if for every `y` in the domain of `f`, the set of all points in `β` mapped to `f(y)` is a measurable set, then `f` is a measurable function. This theorem relates the measurability of a function to the measurability of preimages of singleton sets under it. More concisely: If a function between two countable and measurable spaces maps every singleton set to a measurable preimage, then the function itself is measurable.
`Measurable.le_map` theorem Measurable.le_map : ∀ {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β}, Measurable f → m₂ ≤ MeasurableSpace.map f m₁ The theorem `Measurable.le_map` states that for any two measurable spaces `α` and `β` (denoted as `m₁` and `m₂` respectively), and any function `f` from `α` to `β`, if the function `f` is measurable, then the measurable space `m₂` is less than or equal to the forward image of the measurable space `m₁` under the function `f`. Here, "less than or equal to" refers to the partial order on measurable spaces, where `m₁` is less than or equal to `m₂` if every set measurable in `m₁` is also measurable in `m₂`. Thus, the statement expresses a condition under which the preimage operation by a measurable function preserves the structure of a measurable space. More concisely: If `f` is a measurable function from measurable space `m₁` to measurable space `m₂`, then `m₂` is less than or equal to the forward image of `m₁` under `f`.
`MeasurableEquiv.measurable_toFun` theorem MeasurableEquiv.measurable_toFun : ∀ {α : Type u_6} {β : Type u_7} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (self : α ≃ᵐ β), Measurable ⇑self.toEquiv The theorem `MeasurableEquiv.measurable_toFun` states that for any measurable equivalence (a bijective function that preserves the structure of measurable sets) between two measurable spaces α and β, the forward function (obtained by applying the function to an element of the domain) of this equivalence is itself a measurable function. In other words, given any set in β that is measurable, the preimage of this set under the forward function is a measurable set in α. More concisely: Given a measurable equivalence between measurable spaces α and β, the forward function is a measurable function.
`measurable_from_top` theorem measurable_from_top : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace β] {f : α → β}, Measurable f := by sorry The theorem `measurable_from_top` states that for any two types `α` and `β` where `β` is a measurable space, and for any function `f` from `α` to `β`, the function `f` is measurable. In other words, for any set in `β` that is measurable, the preimage of that set under `f` is also measurable. This holds regardless of the measurable structure (or even the lack of it) on `α`, hence the name "from top". More concisely: If `β` is a measurable space and `f` is a function from type `α` to `β`, then `f` is measurable, meaning for any measurable set `S` in `β`, the preimage `f⁻¹(S)` in `α` is also measurable.
`measurable_inr` theorem measurable_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β], Measurable Sum.inr := by sorry The theorem `measurable_inr` states that for any types `α` and `β` which are equipped with measurable spaces, the function `Sum.inr` is measurable. Here, `Sum.inr` is the function that takes an element of type `β` and puts it in the right component of the sum type `α + β`. In terms of measure theory, a function is measurable if the preimage of any measurable set is also measurable. So, this theorem is asserting that if you take a measurable set in the sum type `α + β`, its preimage under `Sum.inr` is a measurable set in `β`. More concisely: The theorem `measurable_inr` asserts that the right injection `Sum.inr` of a measurable sum type `α + β` is a measurable function from `β` to `α + β`.
`measurableSet_setOf` theorem measurableSet_setOf : ∀ {α : Type u_1} [inst : MeasurableSpace α] {p : α → Prop}, MeasurableSet {a \| p a} ↔ Measurable p The theorem `measurableSet_setOf` states that, for any given type `α` and a property `p` that elements of `α` may or may not satisfy (expressed as a predicate `p : α → Prop`), the set `{a \| p a}` consisting of all elements in `α` that satisfy property `p` is a measurable set if and only if the predicate `p` is a measurable function. Here, "measurable" corresponds to the mathematical concept of measurability in the context of measure theory, which involves the structure of sets and their size. A function is considered measurable if the preimage of every measurable set is also measurable. More concisely: A set {a \| p a} of elements in type α is measurable if and only if the predicate p is a measurable function.
`MeasurableEquiv.symm_symm` theorem MeasurableEquiv.symm_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β), e.symm.symm = e This theorem states that for all types `α` and `β`, given that `α` and `β` are measurable spaces, the double application of the symmetry function (`.symm.symm`) on a measurable equivalence `e` between `α` and `β` results in `e` itself. In other words, it asserts that the symmetry of the symmetry of a measurable equivalence is the equivalence itself. More concisely: For all measurable spaces `α` and `β` and measurable equivalences `e` between them, `e.symm.symm` equals `e`.
`Measurable.mono` theorem Measurable.mono : ∀ {α : Type u_1} {β : Type u_2} {ma ma' : MeasurableSpace α} {mb mb' : MeasurableSpace β} {f : α → β}, Measurable f → ma ≤ ma' → mb' ≤ mb → Measurable f The theorem `Measurable.mono` states that for any two types `α` and `β`, if we have two measurable spaces `ma` and `ma'` over `α`, and two measurable spaces `mb` and `mb'` over `β`, and a function `f` from `α` to `β`, then if `f` is measurable, `ma` is a sub-measurable space of `ma'`, and `mb'` is a sub-measurable space of `mb`, then `f` is still measurable. Essentially, if a function is measurable in one set of spaces, it remains measurable in their superset spaces. More concisely: If `f` is a measurable function between measurable spaces `(α, ma)` and `(β, mb)`, and `ma' ⊆ ma` and `mb' ⊆ mb` are sub-measurable spaces, then `f` is measurable with respect to `(α, ma')` and `(β, mb')`.
`MeasurableSpace.comap_id` theorem MeasurableSpace.comap_id : ∀ {α : Type u_1} {m : MeasurableSpace α}, MeasurableSpace.comap id m = m This theorem states that for any type `α` and any measurable space `m` of type `α`, the reverse image (or preimage) of `m` under the identity function is equal to `m` itself. In other words, if we apply the identity function to every set in the measurable space, we get the same measurable space back. This highlights that the identity function, which leaves every element unchanged, also leaves the structure of the measurable space unchanged when applied to each element. More concisely: For any measurable space (α, m), the preimage of m under the identity function is equal to m.
`measurable_const'` theorem measurable_const' : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : β → α}, (∀ (x y : β), f x = f y) → Measurable f This theorem, `measurable_const'`, asserts that for all types `α` and `β` with respective measurable spaces, any function `f` from `β` to `α` is measurable if the function `f` is constant, i.e., the function `f` maps any two elements `x` and `y` of type `β` to the same element of type `α`. In other words, it's a theorem that ensures the measurability of constant functions between any two measurable spaces, even when these spaces are empty. More concisely: A constant function between any two measurable spaces is measurable.
`Measurable.prod_mk` theorem Measurable.prod_mk : ∀ {α : Type u_1} {m : MeasurableSpace α} {β : Type u_6} {γ : Type u_7} {x : MeasurableSpace β} {x_1 : MeasurableSpace γ} {f : α → β} {g : α → γ}, Measurable f → Measurable g → Measurable fun a => (f a, g a) The `Measurable.prod_mk` theorem states that for any two measurable functions, `f` mapping from type `α` to `β` and `g` mapping from `α` to `γ`, if both `f` and `g` are measurable functions, then a function that takes an element of type `α` and returns a pair consisting of the images of this element under `f` and `g` is also a measurable function. Here, measurability of a function is defined in the sense that the preimage of any measurable set under the function is also a measurable set. More concisely: If `f : α → β` and `g : α → γ` are measurable functions, then the function `x ↦ (f x, g x)` from `α` to `β × γ` is measurable.
`MeasurableSet.inr_image` theorem MeasurableSet.inr_image : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β}, MeasurableSet s → MeasurableSet (Sum.inr '' s) The theorem `MeasurableSet.inr_image` asserts that for any two types `α` and `β`, and any `MeasurableSpace` instances `m` and `mβ` on `α` and `β` respectively, if `s` is a measurable set in `β`, then the image of `s` under the injective function `Sum.inr` (which maps `s` into the sum type `α ⊕ β`) is also a measurable set. Essentially, this theorem is about the preservation of measurability under the mapping of a set to a sum type. More concisely: If `s` is a measurable set in a MeasurableSpace `mβ`, then the image of `s` under the injective function `Sum.inr` is a measurable set in the MeasurableSpace `m` on the sum type `α ⊕ β`.
`MeasurableEmbedding.measurable_rangeSplitting` theorem MeasurableEmbedding.measurable_rangeSplitting : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}, MeasurableEmbedding f → Measurable (Set.rangeSplitting f) The theorem `MeasurableEmbedding.measurable_rangeSplitting` states that for all types `α` and `β`, with `α` having a measurable space structure `mα` and `β` also having a measurable space structure, for any function `f` from `α` to `β` that is a measurable embedding, the function `Set.rangeSplitting f` is measurable. Here, `Set.rangeSplitting` is a function defined using the axiom of choice that selects a preimage for each element of the range of `f`. In other words, if you have a function that is a measurable embedding, then the function that assigns to each point in the range of this function a preimage under the original function is also measurable. More concisely: If `f: α → β` is a measurable embedding between measurable spaces `(α, mα)` and `(β, mβ)`, then `Set.rangeSplitting f: β → Set α` is a measurable function.
`measurable_zero` theorem measurable_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [inst_2 : Zero α], Measurable 0 The theorem `measurable_zero` states that for any types `α` and `β` that both have a `MeasurableSpace` structure and `α` also has a `Zero` structure, the constant zero function (which maps every element of its domain to zero) is a measurable function. In other words, the preimage of any measurable set under the zero function is also a measurable set. More concisely: If `α` and `β` are MeasurableSpaces and `α` has a Zero structure, then the constant zero function from `α` to `β` is measurable.
`measurable_swap` theorem measurable_swap : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β}, Measurable Prod.swap The `measurable_swap` theorem states that for any types `α` and `β` and for any measurable spaces `m` over `α` and `mβ` over `β`, the function `Prod.swap` is measurable. The function `Prod.swap` takes a pair `(a, b)` and returns a pair `(b, a)`, essentially swapping the elements of the pair. The `Measurable` property ensures that the preimage of a measurable set under the `Prod.swap` function is also measurable. More concisely: The `Prod.swap` function on measurable spaces is measurable.
`measurable_iUnionLift` theorem measurable_iUnionLift : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort uι} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : Countable ι] {t : ι → Set α} {f : (i : ι) → ↑(t i) → β} (htf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩) {T : Set α} (hT : T ⊆ ⋃ i, t i), (∀ (i : ι), MeasurableSet (t i)) → (∀ (i : ι), Measurable (f i)) → Measurable (Set.iUnionLift t f htf T hT) The theorem `measurable_iUnionLift` states that given a countable collection `{t i}` of measurable sets that covers a set `T`, and a family of functions `{f i : t i → β}` that agree on the intersections of the sets `t i` and `t j`, then the function defined as `Set.iUnionLift t f _ _ : T → β`, which maps `x` to `f i ⟨x, hx⟩` for `hx : x ∈ t i`, is measurable. This function is defined using `Set.iUnionLift` which constructs a function on the union of sets by defining it on each component, and proving that it agrees on the intersections. The measurability of each function `f i` and each set `t i` are given as hypotheses. More concisely: Given a countable collection of measurable sets {ti} covering T and a family of measurable functions {fi : Ti -> β} agreeing on intersections, the function defined by Set.iUnionLift on their union is measurable.
`measurable_of_restrict_of_restrict_compl` theorem measurable_of_restrict_of_restrict_compl : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} {s : Set α}, MeasurableSet s → Measurable (s.restrict f) → Measurable (sᶜ.restrict f) → Measurable f The theorem `measurable_of_restrict_of_restrict_compl` states for any two types `α` and `β`, a measurable space `m` over `α`, a measurable space `mβ` over `β`, a function `f` from `α` to `β`, and a set `s` of type `α`, if the set `s` is measurable, and the restrictions of the function `f` to the set `s` and its complement `sᶜ` are both measurable, then the original function `f` is measurable. In terms of measure theory, this means that the measurability of a function over a certain domain can be determined by checking its measurability over a subset of the domain and its complement. More concisely: If `m` is a measurable space over `α`, `mβ` is a measurable space over `β`, `f: α → β` is a measurable function, `s ⊆ α` is measurable, and the restrictions of `f` to `s` and `sᶜ` are measurable, then `f` is measurable.
`MeasurableEquiv.measurableEmbedding` theorem MeasurableEquiv.measurableEmbedding : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β), MeasurableEmbedding ⇑e This theorem states that for any two types `α` and `β` both equipped with a measurable space structure, any measurable equivalence `e` from `α` to `β` is also a measurable embedding. That is, if you can map between the two types such that both the function and its inverse are measurable functions, then that mapping also preserves the measurability of sets, that is, the preimage of a measurable set under the function is also measurable. More concisely: If `α` and `β` are measurable spaces and `e : α ≃ β` is a measurable equivalence, then `e` is a measurable embedding (i.e., the preimage of any measurable set in `β` under `e` is measurable in `α`).
`MeasurableSet.subtype_image` theorem MeasurableSet.subtype_image : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set ↑s}, MeasurableSet s → MeasurableSet t → MeasurableSet (Subtype.val '' t) The theorem `MeasurableSet.subtype_image` states that for any type `α` that is equipped with a measurable space `m`, a set `s` of `α`, and a set `t` that is a subset of `s` (expressed as `Set ↑s`), if both the set `s` and the set `t` are measurable sets, then the image of `t` under the function `Subtype.val` is also a measurable set. Here, `Subtype.val` refers to the function that takes an element of a subtype and returns the corresponding element of the base type. This theorem essentially deals with the measurability of a subset after a transformation (`Subtype.val`). More concisely: If `α` is a measurable space, `s` and `t` are measurable subsets of `α`, then the image of `t` under the `Subtype.val` function is a measurable subset of `α`.
`measurable_of_countable` theorem measurable_of_countable : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [inst_2 : Countable α] [inst_3 : MeasurableSingletonClass α] (f : α → β), Measurable f The theorem `measurable_of_countable` states that for any types `α` and `β`, given that `α` is a countable type and it has the structure of a `MeasurableSingletonClass`, and that `α` and `β` are both measurable spaces, any function `f` from `α` to `β` is measurable. In mathematical terms, this means that for any function `f : α → β` in such a context, the preimage of every measurable set in `β` under `f` is a measurable set in `α`. More concisely: If `α` is a countable measurable space with the structure of a `MeasurableSingletonClass`, and `f : α → β` is any function between measurable spaces `α` and `β`, then for every measurable set `M ∈ β`, the preimage `f⁻¹(M)` is a measurable set in `α`.
`Measurable.eval` theorem Measurable.eval : ∀ {α : Type u_1} {δ : Type u_4} {π : δ → Type u_6} [inst : MeasurableSpace α] [inst_1 : (a : δ) → MeasurableSpace (π a)] {a : δ} {g : α → (a : δ) → π a}, Measurable g → Measurable fun x => g x a The theorem `Measurable.eval` states that for any types `α`, `δ`, and `π`, where `α` and `π a` for some `a : δ` have measurable spaces, and there is a function `g : α → (a : δ) → π a`, if `g` is a measurable function, then the function that takes an element `x` from `α` and returns `g x a` is also a measurable function. This means that the preimage of every measurable set under this function is also a measurable set. More concisely: If `α`, `δ`, and `π` are measurable spaces, `a : δ`, and `g : α → (a : δ) → π a` is a measurable function, then the function `x ↦ g x a` is also a measurable function.
`Measurable.measurable_of_countable_ne` theorem Measurable.measurable_of_countable_ne : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : MeasurableSingletonClass α], Measurable f → {x \| f x ≠ g x}.Countable → Measurable g The theorem `Measurable.measurable_of_countable_ne` states that for any two functions `f` and `g` from a measurable space `α` to another measurable space `β`, if `f` is a measurable function and the set of points in `α` where `f` and `g` differ is countable, then `g` is also a measurable function. Here, a measurable function is defined as one where the preimage of any measurable set under the function is also measurable. More concisely: If `f` is a measurable function from measurable space `α` to measurable space `β` and the set where `f` and `g` differ is countable, then `g` is also measurable.
`MeasurableSet.univ_pi` theorem MeasurableSet.univ_pi : ∀ {δ : Type u_4} {π : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (π a)] [inst_1 : Countable δ] {t : (i : δ) → Set (π i)}, (∀ (i : δ), MeasurableSet (t i)) → MeasurableSet (Set.univ.pi t) The theorem `MeasurableSet.univ_pi` asserts that for any type `δ`, any function `π` from `δ` to another type, given that each `π a` has a measurable space structure and `δ` is countable, if we have a family of sets `t` indexed by `δ`, then if every set `t i` is measurable, the set of dependent functions from the universal set of `δ` to each `t i` is also measurable. This result is important in the theory of measure spaces and integration, especially when dealing with products of measurable spaces. More concisely: If `δ` is a countable type, `π: δ → Type`, and each `π a` has a measurable space structure, then the dependent family `{t i := t (π i)}` of measurable sets indexed by `δ` implies that the family `{f: δ → t i \| i ∈ δ}` of functions from `δ` to each `t i` is measurable.
`measurable_subtype_coe` theorem measurable_subtype_coe : ∀ {α : Type u_1} [inst : MeasurableSpace α] {p : α → Prop}, Measurable Subtype.val The theorem `measurable_subtype_coe` asserts that for any type `α` equipped with a measurable space structure, and for any predicate `p` on `α`, the function `Subtype.val` (which maps each subtype `s : {x // p x}` to the underlying element in the base type `α`) is measurable. In other words, the preimage of any measurable set under the `Subtype.val` function is a measurable set. More concisely: For any measurable space `(α, Σ)` and measurable predicate `p : α → Prop`, the function `Subtype.val : {x // p x} → α` is measurable, i.e., for any measurable set `M ∈ Σ`, the preimage `Subtype.val⁻¹[M]` is also measurable.
`measurable_update'` theorem measurable_update' : ∀ {δ : Type u_4} {π : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (π a)] {a : δ} [inst_1 : DecidableEq δ], Measurable fun p => Function.update p.1 a p.2 This theorem states that the function which updates the value of a function `f` at a specific point `a` with a new value `x`, represented mathematically as `(f, x) ↦ update f a x : (Π a, π a) × π a → Π a, π a`, is measurable. For any type `δ` and a function `π` mapping `δ` to another type, given a measurable space for each `a : δ` and decidable equality on `δ`, this update operation is indeed a measurable function. In measure theory, this is important for ensuring operations on functions retain properties related to measurability. More concisely: The function `update : ∀ {δ : Type} [decidable-eq δ], (Π a : δ, π a) → δ × π a → (Π a : δ, π a) measurable`, where `measure Theory δ` is a measurable space for each `a : δ`, is the measurable function that updates the value of a function `f` at a point `a` with a new value `x`.
`MeasurableSet.prod` theorem MeasurableSet.prod : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} {t : Set β}, MeasurableSet s → MeasurableSet t → MeasurableSet (s ×ˢ t) The theorem `MeasurableSet.prod` states that for any two types `α` and `β`, given measurable spaces `m` and `mβ` over these types respectively, and for any sets `s` of type `α` and `t` of type `β`, if `s` and `t` are both measurable sets, then their Cartesian product `s ×ˢ t` is also a measurable set. In other words, the measurability property is preserved under the operation of taking Cartesian products of sets. More concisely: If `α` and `β` are types, `m` and `mβ` are measurable spaces over `α` and `β` respectively, and `s` and `t` are measurable sets in `α` and `β` respectively, then their Cartesian product `s ×ˢ t` is a measurable set in `α × β`.
`measurable_iff_comap_le` theorem measurable_iff_comap_le : ∀ {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β}, Measurable f ↔ MeasurableSpace.comap f m₂ ≤ m₁ This theorem states that for any two types `α` and `β`, along with measurable spaces `m₁` and `m₂` defined over `α` and `β` respectively, and a function `f` from `α` to `β`, the function `f` is measurable if and only if the reverse image of the measurable space under `f` is a subset of `m₁`. In other words, a function between two measurable spaces is measurable if the preimage of every measurable set in the codomain space (as per `m₂`) is a measurable set in the domain space (as per `m₁`). This formalizes the connection between the measurability of a function and the structure of the measurable spaces it maps between. More concisely: A function between two measurable spaces is measurable if and only if the preimage of every measurable set in the codomain space is measurable in the domain space.
`measurable_id''` theorem measurable_id'' : ∀ {α : Type u_1} {m mα : MeasurableSpace α}, m ≤ mα → Measurable id This theorem states that for any type `α` and any two measurable spaces `m` and `mα` on `α`, if `m` is a subspace of `mα` (i.e., `m` is less than or equal to `mα`), then the identity function on `α` is measurable. In the context of measure theory, a function is "measurable" if the preimage of every measurable set is still measurable; hence, this theorem verifies that the identity function indeed satisfies this property given the conditions. More concisely: If `m` is a submeasure on `α` and `mα` is a measure on `α`, then the identity function on `α` is measurable with respect to `m` and `mα`.
`measurable_inl` theorem measurable_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β], Measurable Sum.inl := by sorry The theorem `measurable_inl` states that for any two types `α` and `β` each equipped with a measurable space structure, the function `Sum.inl`, which maps an element of type `α` to an element of the sum type `α ⊕ β` by placing it in the left component of the sum, is a measurable function. In other words, the preimage of any measurable set under the `Sum.inl` function is also a measurable set. More concisely: The function `Sum.inl : α → α ⊕ β` is measurable for any measurable spaces (α, Σα) and (β, Σβ).
`Measurable.prod` theorem Measurable.prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β × γ}, (Measurable fun a => (f a).1) → (Measurable fun a => (f a).2) → Measurable f The theorem `Measurable.prod` states that for any three types `α`, `β`, and `γ` with respective measurable spaces `m`, `mβ`, and `mγ`, and any function `f` from `α` to the product space `β × γ`, if the function that maps `a` to the first component of `f a` is measurable and the function mapping `a` to the second component of `f a` is also measurable, then the function `f` itself is measurable. In mathematical terms, if both projections of `f : α → β × γ` are measurable, then `f` is measurable. More concisely: If the projections of a function from a measurable space to the product of two measurable spaces are measurable, then the function itself is measurable.
`Measurable.subtype_val` theorem Measurable.subtype_val : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : β → Prop} {f : α → Subtype p}, Measurable f → Measurable fun a => ↑(f a) The theorem `Measurable.subtype_val` states that for any types `α` and `β`, given a measurable space over `α`, a measurable space over `β`, a property `p` on `β`, and a function `f` mapping an element of `α` to a subtype of `β` satisfying the property `p`, if the function `f` is measurable, then the function that maps an element of `α` to the underlying element of `β` in the image of `f` is also measurable. In other words, if `f` is a measurable function from `α` to a subtype of `β`, then the function that takes an element in `α` and returns the corresponding element in `β` (ignoring the subtype structure) is also measurable. More concisely: If `f : α → β` is a measurable function mapping each `x in α` to a subtype of `β` satisfying property `p`, then the function `x ↦ ⨆ (f x)` is measurable, where `⨆` denotes the underlying element of a subtype.
`measurable_pi_apply` theorem measurable_pi_apply : ∀ {δ : Type u_4} {π : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (π a)] (a : δ), Measurable fun f => f a := by sorry This theorem states that for any type `δ` and a function `π` from `δ` to another type, given an instance of a measurable space for every value of `δ` (denoted as `(a : δ) → MeasurableSpace (π a)`), and any element `a` of type `δ`, the function which applies `f` to `a` is measurable. In other words, if we have a function `f` from a set of elements of type `δ` to measurable spaces, and a specific element `a` of type `δ`, then the function that maps any such function `f` to the result of applying `f` to `a` is measurable. In terms of measure theory, this means the preimage of any measurable set under this function is also measurable. More concisely: Given a measurable space instance for every value of type `δ`, and a measurable function `f` from a set to measurable spaces, the application of `f` to any element `a` of type `δ` is a measurable function.
`measurable_of_subsingleton_codomain` theorem measurable_of_subsingleton_codomain : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [inst_2 : Subsingleton β] (f : α → β), Measurable f The theorem `measurable_of_subsingleton_codomain` states that for any two types `α` and `β` with respective measurable spaces, and a function `f` from `α` to `β`, if `β` is a subsingleton (i.e., has at most one element), then `f` is measurable. In other words, a function mapping to a type with at most one element is always measurable. A function is considered measurable if the preimage of every measurable set is measurable. More concisely: If `β` is a subsingleton type, then every function from a measurable space to `β` is measurable.
`Measurable.setOf` theorem Measurable.setOf : ∀ {α : Type u_1} [inst : MeasurableSpace α] {p : α → Prop}, Measurable p → MeasurableSet {a \| p a} This theorem, which is an alias of the reverse direction of `measurableSet_setOf`, asserts that for any type `α` equipped with a measurable space structure and any predicate `p` on `α`, if the function `p` is measurable, then the set of elements `a` in `α` such that `p a` holds is a measurable set. In other words, the set of elements satisfying a measurable predicate is itself measurable. More concisely: If `α` is a measurable space and `p : α → Prop` is a measurable predicate, then the set `{a : α \| p a}` is a measurable subset of `α`.
`measurable_prod_mk_right` theorem measurable_prod_mk_right : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {y : β}, Measurable fun x => (x, y) The theorem `measurable_prod_mk_right` states that for any types `α` and `β`, if `α` and `β` are both equipped with a measurable space structure, and for any fixed element `y` of type `β`, the function that takes an element `x` (of type `α`) and maps it to the pair `(x, y)` is a measurable function. In other words, the pre-image of any measurable set under this function is also a measurable set. More concisely: For any measurable types `α` and `β`, the function `x ↦ (x, y)` from `α` to `α × β` is measurable for any fixed `y` in `β`.
`Measurable.comap_le` theorem Measurable.comap_le : ∀ {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β}, Measurable f → MeasurableSpace.comap f m₂ ≤ m₁ The theorem `Measurable.comap_le` states that for any types `α` and `β`, and for any measurable spaces `m₁` of type `α` and `m₂` of type `β`, and for any function `f` from `α` to `β`, if `f` is a measurable function, then the measurable space obtained by taking the reverse image of `m₂` under `f` (i.e., `MeasurableSpace.comap f m₂`) is a sub-measurable space of `m₁`. This essentially implies that the preimages of the measurable sets in `m₂` under `f` are also measurable sets in `m₁`. More concisely: If `f` is a measurable function from the measurable space `(α, m₁)` to the measurable space `(β, m₂)`, then `MeasurableSpace.comap f m₂` is a sub-measurable space of `m₁`.
`MeasurableEmbedding.subtype_coe` theorem MeasurableEmbedding.subtype_coe : ∀ {α : Type u_1} {mα : MeasurableSpace α} {s : Set α}, MeasurableSet s → MeasurableEmbedding Subtype.val This theorem states that for any type `α` with a `MeasurableSpace` structure (denoted as `mα`), and any set `s` of type `Set α`, if `s` is a measurable set (i.e., `MeasurableSet s` is true), then the function `Subtype.val` (which retrieves the underlying element from a subtype) is a measurable embedding. In other words, if we have a set of elements that form a measurable subset in a measurable space, the operation of retrieving the underlying elements from this set is a measurable process according to the measure space structure. More concisely: For any measurable space `(α, mα)` and measurable set `s ∈ Set α`, the function `Subtype.val : s → α` is a measurable function.
`measurable_one` theorem measurable_one : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [inst_2 : One α], Measurable 1 The theorem `measurable_one` states that for any types `α` and `β`, given that `α` is a measurable space, `β` is a measurable space, and `α` has a `one` operator (essentially meaning that it has an identity element under multiplication), the constant function that always returns the `one` of `α` is measurable. In other words, the preimage of any measurable set under this function is also a measurable set. More concisely: For measurable spaces `α` and `β`, if `α` has a one operator, then the constant function from `α` to its one element is a measurable function.
`MeasurableEmbedding.measurable` theorem MeasurableEmbedding.measurable : ∀ {α : Type u_6} {β : Type u_7} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β}, MeasurableEmbedding f → Measurable f The theorem states that if we have a measurable embedding function `f` from a measurable space `α` to another measurable space `β`, then `f` is also a measurable function. Here, a measurable function is one where the preimage of every measurable set in `β` is also a measurable set in `α`. More concisely: If `f` is a measurable embedding from measurable space `α` to measurable space `β`, then `f` is a measurable function.
`MeasurableSet.principal_isMeasurablyGenerated` theorem MeasurableSet.principal_isMeasurablyGenerated : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α}, MeasurableSet s → (Filter.principal s).IsMeasurablyGenerated The theorem `MeasurableSet.principal_isMeasurablyGenerated` states that for any type `α` equipped with a `MeasurableSpace` structure and any set `s` of `α` that is a measurable set, the principal filter of `s` is measurably generated. In other words, if a set `s` is measurable in a given measurable space, then the collection of all supersets of `s` (which is defined as the principal filter) is such that it can be generated by countable unions of measurable sets. More concisely: If `α` is a type with a `MeasurableSpace` structure and `s ⊆ α` is measurable, then the principal filter of `s` is generated by countable unions of measurable sets.
`measurable_snd` theorem measurable_snd : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {x_1 : MeasurableSpace β}, Measurable Prod.snd The theorem `measurable_snd` states that for any given types `α` and `β` and any measurable spaces `x` over `α` and `x_1` over `β`, the second projection function `Prod.snd` is measurable. In other words, the function that takes an ordered pair and returns its second component is a measurable function. This means that for any measurable set in the co-domain, the preimage of that set under `Prod.snd` is also measurable. More concisely: The second projection function `Prod.snd` is measurable with respect to the product measurable space structure over types `α` and `β`.
`MeasurableSpace.comap_le_iff_le_map` theorem MeasurableSpace.comap_le_iff_le_map : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {m' : MeasurableSpace β} {f : α → β}, MeasurableSpace.comap f m' ≤ m ↔ m' ≤ MeasurableSpace.map f m This theorem states that for any two types `α` and `β`, any measurable spaces `m` over `α` and `m'` over `β`, and any function `f` from `α` to `β`, the reverse image of the measurable space `m'` under the function `f` is a sub-measurable-space of `m` if and only if `m'` is a sub-measurable-space of the forward image of the measurable space `m` under the function `f`. More concisely: For measurable spaces `m` over type `α` and `m'` over type `β`, and any function `f` from `α` to `β`, the reverse image `f⁺(m')` is a sub-measurable-space of `m` if and only if `m'` is a sub-measurable-space of the forward image `f⁻¹(m)`.

LeanAide GPT-4 documentation

Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

measurable_from_prod_countable

MeasurableEquiv.symm_comp_self

theorem MeasurableEquiv.symm_comp_self : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β), ⇑e.symm ∘ ⇑e = id

MeasurableEquiv.measurable

theorem MeasurableEquiv.measurable : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β), Measurable ⇑e

measurable_liftCover

MeasurableSpace.generateFrom_singleton

theorem MeasurableSpace.generateFrom_singleton : ∀ {α : Type u_1} (s : Set α), MeasurableSpace.generateFrom {s} = MeasurableSpace.comap (fun x => x ∈ s) ⊤ := by sorry

exists_measurable_piecewise

MeasurableEquiv.coe_toEquiv

theorem MeasurableEquiv.coe_toEquiv : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β), ⇑e.toEquiv = ⇑e

measurable_update

theorem measurable_update : ∀ {δ : Type u_4} {π : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (π a)] (f : (a : δ) → π a) {a : δ} [inst_1 : DecidableEq δ], Measurable (Function.update f a)

MeasurableSet.mem

theorem MeasurableSet.mem : ∀ {α : Type u_1} {s : Set α} [inst : MeasurableSpace α], MeasurableSet s → Measurable fun x => x ∈ s

Measurable.find

MeasurableEmbedding.measurableSet_image

theorem MeasurableEmbedding.measurableSet_image : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}, MeasurableEmbedding f → ∀ {s : Set α}, MeasurableSet (f '' s) ↔ MeasurableSet s

MeasurableEquiv.ext

theorem MeasurableEquiv.ext : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {e₁ e₂ : α ≃ᵐ β}, ⇑e₁ = ⇑e₂ → e₁ = e₂

Measurable.snd

theorem Measurable.snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β × γ}, Measurable f → Measurable fun a => (f a).2

MeasurableEquiv.measurable_comp_iff

theorem MeasurableEquiv.measurable_comp_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [inst_2 : MeasurableSpace γ] {f : β → γ} (e : α ≃ᵐ β), Measurable (f ∘ ⇑e) ↔ Measurable f

MeasurableEquiv.measurable_invFun

theorem MeasurableEquiv.measurable_invFun : ∀ {α : Type u_6} {β : Type u_7} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (self : α ≃ᵐ β), Measurable ⇑self.symm

Measurable.ite

theorem Measurable.ite : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : α → Prop} {x : DecidablePred p}, MeasurableSet {a | p a} → Measurable f → Measurable g → Measurable fun x_1 => if p x_1 then f x_1 else g x_1

measurable_sum

theorem measurable_sum : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : MeasurableSpace γ} {f : α ⊕ β → γ}, Measurable (f ∘ Sum.inl) → Measurable (f ∘ Sum.inr) → Measurable f

MeasurableEmbedding.comap_eq

theorem MeasurableEmbedding.comap_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β}, MeasurableEmbedding f → MeasurableSpace.comap f inst_1 = inst

MeasurableSpace.le_map_comap

theorem MeasurableSpace.le_map_comap : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {g : β → α}, m ≤ MeasurableSpace.map g (MeasurableSpace.comap g m)

measurable_fst

theorem measurable_fst : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {x_1 : MeasurableSpace β}, Measurable Prod.fst

exists_measurable_piecewise_nat

MeasurableSet.pi

theorem MeasurableSet.pi : ∀ {δ : Type u_4} {π : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (π a)] {s : Set δ} {t : (i : δ) → Set (π i)}, s.Countable → (∀ i ∈ s, MeasurableSet (t i)) → MeasurableSet (s.pi t)

Subsingleton.measurable

theorem Subsingleton.measurable : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [inst_2 : Subsingleton α], Measurable f

measurable_indicator_const_iff

theorem measurable_indicator_const_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : Zero β] [inst_1 : MeasurableSingletonClass β] (b : β) [inst_2 : NeZero b], Measurable (s.indicator fun x => b) ↔ MeasurableSet s

measurable_swap_iff

theorem measurable_swap_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : MeasurableSpace γ} {f : α × β → γ}, Measurable (f ∘ Prod.swap) ↔ Measurable f

MeasurableEmbedding.injective

theorem MeasurableEmbedding.injective : ∀ {α : Type u_6} {β : Type u_7} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β}, MeasurableEmbedding f → Function.Injective f

MeasurableEmbedding.id

theorem MeasurableEmbedding.id : ∀ {α : Type u_1} {mα : MeasurableSpace α}, MeasurableEmbedding id

Measurable.of_le_map

theorem Measurable.of_le_map : ∀ {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β}, m₂ ≤ MeasurableSpace.map f m₁ → Measurable f

measurable_prod_mk_left

theorem measurable_prod_mk_left : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)

MeasurableSet.preimage

theorem MeasurableSet.preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {t : Set β}, MeasurableSet t → Measurable f → MeasurableSet (f ⁻¹' t)

Measurable.of_comap_le

theorem Measurable.of_comap_le : ∀ {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β}, MeasurableSpace.comap f m₂ ≤ m₁ → Measurable f

Measurable.fst

theorem Measurable.fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β × γ}, Measurable f → Measurable fun a => (f a).1

MeasurableEmbedding.measurableSet_range

theorem MeasurableEmbedding.measurableSet_range : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}, MeasurableEmbedding f → MeasurableSet (Set.range f)

MeasurableEmbedding.comp

theorem MeasurableEmbedding.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] {f : α → β} {g : β → γ}, MeasurableEmbedding g → MeasurableEmbedding f → MeasurableEmbedding (g ∘ f)

MeasurableEmbedding.measurableSet_image'

theorem MeasurableEmbedding.measurableSet_image' : ∀ {α : Type u_6} {β : Type u_7} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β}, MeasurableEmbedding f → ∀ ⦃s : Set α⦄, MeasurableSet s → MeasurableSet (f '' s)

measurable_of_measurable_on_compl_singleton

theorem measurable_of_measurable_on_compl_singleton : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : MeasurableSingletonClass α] {f : α → β} (a : α), Measurable ({x | x ≠ a}.restrict f) → Measurable f

Measurable.piecewise

theorem Measurable.piecewise : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f g : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : DecidablePred fun x => x ∈ s}, MeasurableSet s → Measurable f → Measurable g → Measurable (s.piecewise f g)

MeasurableSpace.gc_comap_map

theorem MeasurableSpace.gc_comap_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), GaloisConnection (MeasurableSpace.comap f) (MeasurableSpace.map f)

MeasurableSet.inl_image

theorem MeasurableSet.inl_image : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α}, MeasurableSet s → MeasurableSet (Sum.inl '' s)

Measurable.indicator

theorem Measurable.indicator : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : Zero β], Measurable f → MeasurableSet s → Measurable (s.indicator f)

measurable_pi_lambda

theorem measurable_pi_lambda : ∀ {α : Type u_1} {δ : Type u_4} {π : δ → Type u_6} [inst : MeasurableSpace α] [inst_1 : (a : δ) → MeasurableSpace (π a)] (f : α → (a : δ) → π a), (∀ (a : δ), Measurable fun c => f c a) → Measurable f

Measurable.subtype_mk

`measurable_from_prod_countable`

`MeasurableEquiv.symm_comp_self`

`MeasurableEquiv.measurable`

`measurable_liftCover`

`MeasurableSpace.generateFrom_singleton`

`exists_measurable_piecewise`

`MeasurableEquiv.coe_toEquiv`

`measurable_update`

`MeasurableSet.mem`

`Measurable.find`

`MeasurableEmbedding.measurableSet_image`

`MeasurableEquiv.ext`

`Measurable.snd`

`MeasurableEquiv.measurable_comp_iff`

`MeasurableEquiv.measurable_invFun`

`Measurable.ite`

`measurable_sum`

`MeasurableEmbedding.comap_eq`

`MeasurableSpace.le_map_comap`

`measurable_fst`

`exists_measurable_piecewise_nat`

`MeasurableSet.pi`

`Subsingleton.measurable`

`measurable_indicator_const_iff`

`measurable_swap_iff`

`MeasurableEmbedding.injective`

`MeasurableEmbedding.id`

`Measurable.of_le_map`

`measurable_prod_mk_left`

`MeasurableSet.preimage`

`Measurable.of_comap_le`

`Measurable.fst`

`MeasurableEmbedding.measurableSet_range`

`MeasurableEmbedding.comp`

`MeasurableEmbedding.measurableSet_image'`

`measurable_of_measurable_on_compl_singleton`

`Measurable.piecewise`

`MeasurableSpace.gc_comap_map`

`MeasurableSet.inl_image`

`Measurable.indicator`

`measurable_pi_lambda`

`Measurable.subtype_mk`

`Mathlib.MeasureTheory.MeasurableSpace.Basic._auxLemma.25`

`measurable_pi_iff`

`Measurable.iterate`

`measurable_to_countable`

`Measurable.le_map`

`MeasurableEquiv.measurable_toFun`

`measurable_from_top`

`measurable_inr`

`measurableSet_setOf`

`MeasurableEquiv.symm_symm`

`Measurable.mono`

`MeasurableSpace.comap_id`

`measurable_const'`

`Measurable.prod_mk`

`MeasurableSet.inr_image`

`MeasurableEmbedding.measurable_rangeSplitting`

`measurable_zero`

`measurable_swap`

`measurable_iUnionLift`

`measurable_of_restrict_of_restrict_compl`

`MeasurableEquiv.measurableEmbedding`

`MeasurableSet.subtype_image`

`measurable_of_countable`

`Measurable.eval`

`Measurable.measurable_of_countable_ne`

`MeasurableSet.univ_pi`

`measurable_subtype_coe`

`measurable_update'`

`MeasurableSet.prod`

`measurable_iff_comap_le`

`measurable_id''`

`measurable_inl`