LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

`measurableSet_of_differentiableAt` theorem measurableSet_of_differentiableAt : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F) [inst_5 : MeasurableSpace E] [inst_6 : OpensMeasurableSpace E] [inst_7 : CompleteSpace F], MeasurableSet {x \| DifferentiableAt 𝕜 f x} The theorem `measurableSet_of_differentiableAt` states that, for any function `f` mapping from a normed vector space `E` over a nontrivially normed field `𝕜` to another normed vector space `F` over the same field (where `F` is a complete space), the set of points in `E` at which `f` is differentiable is a measurable set. Here, measurability is defined in the sense of Borel-measurable spaces. This theorem asserts a fundamental property linking the concepts of differentiability and measure theory, specifically that differentiability points can be measured. More concisely: The set of points in a normed vector space where a function mapping between two normed vector spaces is differentiable is a Borel measurable set.
`RightDerivMeasurableAux.differentiable_set_subset_D` theorem RightDerivMeasurableAux.differentiable_set_subset_D : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f : ℝ → F} (K : Set F), {x \| DifferentiableWithinAt ℝ f (Set.Ici x) x ∧ derivWithin f (Set.Ici x) x ∈ K} ⊆ RightDerivMeasurableAux.D f K This theorem states that for any real-valued function `f` and any set `K` of the same type as the output of `f`, the set of points `x` where `f` is differentiable on the interval `[x, ∞)` (i.e., the set `Set.Ici x`) and the derivative of `f` at `x` within this interval is an element of `K`, is a subset of the set `RightDerivMeasurableAux.D f K`. `RightDerivMeasurableAux.D f K`, as defined above, is a complex set constructed using countable intersections and unions. When `K` is complete, it is exactly the set of points where `f` is differentiable, with a derivative in `K`. The theorem essentially states that if a point `x` is such that `f` is differentiable at `x` on the interval `[x, ∞)` and its derivative is in `K`, then `x` must belong to the set `RightDerivMeasurableAux.D f K`. More concisely: If `f` is a real-valued function, `K` is a set of reals, and for all `x`, `f` is differentiable on `[x, ∞)` with derivative in `K`, then `x` is in the set `RightDerivMeasurableAux.D f K`.
`measurable_deriv_with_param` theorem measurable_deriv_with_param : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_3} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] {α : Type u_4} [inst_3 : TopologicalSpace α] [inst_4 : MeasurableSpace α] [inst_5 : OpensMeasurableSpace α] [inst_6 : CompleteSpace F] [inst_7 : LocallyCompactSpace 𝕜] [inst_8 : MeasurableSpace 𝕜] [inst_9 : OpensMeasurableSpace 𝕜] [inst_10 : MeasurableSpace F] [inst_11 : BorelSpace F] {f : α → 𝕜 → F}, Continuous (Function.uncurry f) → Measurable fun p => deriv (f p.1) p.2 This theorem, `measurable_deriv_with_param`, asserts that for every function `f` that maps a pair of types `α` and `𝕜` to type `F`, if the function `f` is continuous when uncurried, i.e., treated as a function on pairs `(α × 𝕜) → F`, then the function that maps a pair `p` to the derivative of `f` at the point `p.1` evaluated at `p.2` is measurable. Here, `𝕜` is a nontrivial normed field, `F` is a normed additive commutative group and also a normed space over `𝕜`, `α` is a topological space and a measurable space that is both open and complete, and `𝕜` and `F` are measurable spaces with `F` being a Borel space. Measurable refers to the property that the pre-image of every measurable set under the function is measurable. The derivative of a function at a point exists if the function is differentiable at that point and is zero otherwise. More concisely: If `f` is a continuous, uncurried function from the product of a measurable, open and complete topological space `α` and a nontrivial normed field `𝕜` to a normed additive commutative group and normed space `F` over `𝕜`, then the function that maps a pair `p` to the derivative of `f` at `p.1` evaluated at `p.2` is measurable.
`FDerivMeasurableAux.differentiable_set_subset_D` theorem FDerivMeasurableAux.differentiable_set_subset_D : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} (K : Set (E →L[𝕜] F)), {x \| DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K} ⊆ FDerivMeasurableAux.D f K This theorem states that for any nontrivial normed field `𝕜`, normed additive commutative groups `E` and `F`, and a function `f` from `E` to `F`, if `K` is a set of linear continuous transformations from `E` to `F`, then the set of points `x` at which `f` is differentiable and the derivative of `f` at `x` belongs to `K`, is a subset of the set `D` of points where `f`'s derivative is measurable and belongs to `K`. In other words, if 'f' is differentiable at a point and its derivative at that point is in 'K', then this point will be included in the set of points where the derivative of 'f' is measurable and in 'K'. More concisely: If `f` is a differentiable function from a normed additive commutative group `E` to another `F` over a nontrivial normed field, and if the derivative of `f` at each differentiability point lies in a set `K` of linear continuous transformations from `E` to `F`, then the set of differentiability points of `f` is contained in the set where `f`'s derivative is measurable and lies in `K`.
`measurableSet_of_differentiableWithinAt_Ici_of_isComplete` theorem measurableSet_of_differentiableWithinAt_Ici_of_isComplete : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (f : ℝ → F) {K : Set F}, IsComplete K → MeasurableSet {x \| DifferentiableWithinAt ℝ f (Set.Ici x) x ∧ derivWithin f (Set.Ici x) x ∈ K} This theorem states that for any real-valued function `f` and any set `K` of the type of the function's output (denoted as `F`), if `K` is a complete set, then the set of all real numbers `x` for which `f` is right differentiable at `x` and the derivative of `f` at `x` within the right-closed, right-infinite interval starting at `x` belongs to `K`, is a Borel-measurable set. In mathematical terms, if `f : ℝ → F` and `K` is a complete subset of `F`, then the set `{x ∈ ℝ \| DifferentiableWithinAt ℝ f [x, ∞) x and derivWithin f [x, ∞) x ∈ K}` is a Borel-measurable set. More concisely: If `f : ℝ → F` is a real-valued function and `K` is a complete subset of `F`, then the set of all `x ∈ ℝ` where `f` is right differentiable at `x` with derivative in `K` is a Borel-measurable set.
`measurableSet_of_differentiableAt_of_isComplete` theorem measurableSet_of_differentiableAt_of_isComplete : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F) [inst_5 : MeasurableSpace E] [inst_6 : OpensMeasurableSpace E] {K : Set (E →L[𝕜] F)}, IsComplete K → MeasurableSet {x \| DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K} This theorem states that, for any function `f` from some normed space `E` to another normed space `F`, both over a non-trivially normed field `𝕜`, the set of points at which `f` is differentiable and its derivative at those points lies in a given complete set `K` is a Borel-measurable set. Here, a set is said to be complete if any Cauchy filter that contains the set has a limit within the set. The notion of differentiability used here is that there exists a derivative at a given point. The derivative of a function at a point, if it exists, is given by `fderiv 𝕜 f x`, otherwise, it's set to zero. More concisely: The set of points in a normed space where a given function between two normed spaces has a differentiable decomposition with derivative in a complete set is a Borel-measurable set.
`measurable_derivWithin_Ici` theorem measurable_derivWithin_Ici : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (f : ℝ → F) [inst_2 : CompleteSpace F] [inst_3 : MeasurableSpace F] [inst_4 : BorelSpace F], Measurable fun x => derivWithin f (Set.Ici x) x This theorem, `measurable_derivWithin_Ici`, states that for any function `f` from real numbers to a normed additively commutative group `F`, that also forms a normed space over real numbers, and which is a complete and measureable space, the function that maps each real number `x` to the derivative of `f` at the point `x` within the set of real numbers greater than or equal to `x` (denoted by `Set.Ici x`), is a measurable function. Here, a measurable function is defined as a function whose preimage of every measurable set is also measurable. The derivative of `f` at `x` within `Set.Ici x` is defined as the rate at which `f` changes at `x`, considering only the values of `f` for inputs greater than or equal to `x`. More concisely: The derivative function of a complete, measureable, and normed function from real numbers to a normed additively commutative group, restricted to the set of real numbers greater than or equal to a given point, is a measurable function.
`stronglyMeasurable_deriv_with_param` theorem stronglyMeasurable_deriv_with_param : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_3} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] {α : Type u_4} [inst_3 : TopologicalSpace α] [inst_4 : MeasurableSpace α] [inst_5 : OpensMeasurableSpace α] [inst_6 : CompleteSpace F] [inst_7 : LocallyCompactSpace 𝕜] [inst_8 : MeasurableSpace 𝕜] [inst_9 : OpensMeasurableSpace 𝕜] [h : SecondCountableTopologyEither α F] {f : α → 𝕜 → F}, Continuous (Function.uncurry f) → MeasureTheory.StronglyMeasurable fun p => deriv (f p.1) p.2 This theorem, named `stronglyMeasurable_deriv_with_param`, states that for all types `𝕜` and `F` such that `𝕜` is a non-trivially normed field, `F` is a normed add commutative group and a normed space over `𝕜`, and a type `α` having the structure of a topological space, measurable space, open measurable space, and having a second countable topology with `F`, for any function `f` from `α` to `𝕜` to `F` (interpreted as a function on `α × 𝕜` to `F`), if `f` is continuous, then the function that takes a pair `p` and gives the derivative of `f` at the point `p.1` in direction `p.2` is strongly measurable. In more mathematical terms, if we have a continuous function $f : \alpha \times \kappa \rightarrow F$, then the function $g: \alpha \times \kappa \rightarrow F$ defined by $g(p) = \frac{df}{d\kappa}(p)$, where $\frac{df}{d\kappa}(p)$ denotes the derivative of $f$ at point $p.1$ in direction $p.2$, is strongly measurable. Strongly measurable functions are those that can be considered as the limit of a sequence of simple functions. More concisely: If `α` is a topological space, `F` is a normed add commutative group and a normed space over a non-trivially normed field `𝕜`, and `f : α × 𝕜 → F` is a continuous function, then the derivative function `g : α × 𝕜 → F` given by `g(p) = df/dκ(p)` is strongly measurable.
`measurableSet_of_differentiableAt_with_param` theorem measurableSet_of_differentiableAt_with_param : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : LocallyCompactSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] {α : Type u_4} [inst_6 : TopologicalSpace α] [inst_7 : MeasurableSpace α] [inst_8 : MeasurableSpace E] [inst_9 : OpensMeasurableSpace α] [inst_10 : OpensMeasurableSpace E] {f : α → E → F} [inst_11 : CompleteSpace F], Continuous (Function.uncurry f) → MeasurableSet {p \| DifferentiableAt 𝕜 (f p.1) p.2} The theorem `measurableSet_of_differentiableAt_with_param` states that for any non-trivially normed field 𝕜 and sets E and F that are normed additive commutative groups and also normed spaces over 𝕜, where E is a locally compact space and F is a complete space, if α is a topological space which is measurable, and if E and α are open measurable spaces, then for a function `f` that takes an argument in α and returns a function from E to F, if the uncurried version of this function is continuous, then the set of points at which the function `f` is differentiable is a measurable set. This result connects differentiability with measurability, two central concepts in analysis. More concisely: If 𝕜 is a non-trivially normed field, E and F are locally compact, normed additive commutative groups and complete spaces over 𝕜, α is a measurable topological space, E and α are open measurable, and the uncurried version of the function `f : α → (E → F)` is continuous, then the set of points in α where `f` is differentiable from E to F is a measurable subset of α.
`measurableSet_of_differentiableWithinAt_Ici` theorem measurableSet_of_differentiableWithinAt_Ici : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (f : ℝ → F) [inst_2 : CompleteSpace F], MeasurableSet {x \| DifferentiableWithinAt ℝ f (Set.Ici x) x} The theorem `measurableSet_of_differentiableWithinAt_Ici` states that for any function `f` mapping real numbers to a normed additive commutative group `F`, which is also a complete space, the set of all points at which `f` is right differentiable is a measurable set. Here, right differentiability at a point `x` is defined as the existence of a derivative of `f` within the set of all real numbers greater than or equal to `x`. The concept of measurability in this context is associated with the inherent measure space on the set of real numbers. More concisely: The set of real numbers at which a real-valued, right differentiable function `f` has a derivative is a measurable set.
`RightDerivMeasurableAux.D_subset_differentiable_set` theorem RightDerivMeasurableAux.D_subset_differentiable_set : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f : ℝ → F} {K : Set F}, IsComplete K → RightDerivMeasurableAux.D f K ⊆ {x \| DifferentiableWithinAt ℝ f (Set.Ici x) x ∧ derivWithin f (Set.Ici x) x ∈ K} The theorem `RightDerivMeasurableAux.D_subset_differentiable_set` states that for every function `f` from real numbers to a normed add commutative group `F` and for every complete set `K` of `F`, any point within the set `D f K` (which is a complex set constructed using countable intersections and unions) satisfies two properties: the function `f` is differentiable at that point within the set of all real numbers greater than or equal to that point, and the derivative of `f` at that point within the set of all real numbers greater than or equal to that point belongs to the set `K`. In other words, this theorem asserts that the set `D f K` is a subset of the set of points where the function `f` has a derivative in `K`. More concisely: The theorem `RightDerivMeasurableAux.D_subset_differentiable_set` asserts that for every function `f` from real numbers to a normed add commutative group `F` and every complete set `K` of `F`, the set `D f K` consists only of points where `f` is differentiable and its derivative belongs to `K`.
`FDerivMeasurableAux.D_subset_differentiable_set` theorem FDerivMeasurableAux.D_subset_differentiable_set : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {K : Set (E →L[𝕜] F)}, IsComplete K → FDerivMeasurableAux.D f K ⊆ {x \| DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K} The theorem `FDerivMeasurableAux.D_subset_differentiable_set` states that for any non-trivially normed field `𝕜`, normed add commutative group `E`, normed space over `𝕜` and `E`, normed add commutative group `F`, and normed space over `𝕜` and `F`, if `K` is a set of linear continuous maps from `E` to `F` which is complete, then the set `D` of points at which the function `f` from `E` to `F` is differentiable with respect to `K` is a subset of the set of points at which `f` is differentiable and its derivative at that point is in `K`. In short, at a point in `D f K`, the function `f` has a derivative that belongs to `K`. More concisely: For a complete set `K` of linear, continuous maps from a normed add commutative group `E` to another normed add commutative group `F` over a non-trivially normed field `𝕜`, the set of points in `E` where `f` is both differentiable and its derivative belongs to `K` is a subset of the set of points in `E` where `f` is differentiable.
`measurableSet_of_differentiableWithinAt_Ioi` theorem measurableSet_of_differentiableWithinAt_Ioi : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (f : ℝ → F) [inst_2 : CompleteSpace F], MeasurableSet {x \| DifferentiableWithinAt ℝ f (Set.Ioi x) x} The theorem `measurableSet_of_differentiableWithinAt_Ioi` states that for any real-valued function `f` taking values in a complete normed additive commutative group `F`, the set of points where `f` is right-differentiable is a Borel-measurable set. Here, a function is said to be right-differentiable at a point `x` if it admits a derivative for values greater than `x`. Being Borel-measurable means the set belongs to the smallest σ-algebra containing all open sets, which is a natural generalization of intervals for real numbers. More concisely: The set of points where a real-valued, right-differentiable function defines a derivative is a Borel-measurable subset of the real numbers.