exists_partition_approximatesLinearOn_of_hasFDerivWithinAt
theorem exists_partition_approximatesLinearOn_of_hasFDerivWithinAt :
∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : FiniteDimensional ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F]
[inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E] [inst_7 : SecondCountableTopology F] (f : E → F) (s : Set E)
(f' : E → E →L[ℝ] F),
(∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
∀ (r : (E →L[ℝ] F) → NNReal),
(∀ (A : E →L[ℝ] F), r A ≠ 0) →
∃ t A,
Pairwise (Disjoint on t) ∧
(∀ (n : ℕ), MeasurableSet (t n)) ∧
s ⊆ ⋃ n, t n ∧
(∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧
(s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)
This theorem states that given a function `f` that has a derivative at every point of a set `s`, we can divide `s` into countably many disjoint, measurable sets (`t n`) such that `f` is well approximated by linear maps `A n` on each of these sets. This partitioning of `s` is such that each of the partition sets (`t n`) is measurable, they together cover all of `s`, and on each `t n`, `f` behaves close to a linear map `A n` with a non-zero error controlled by a real function `r` on the set of linear maps. Furthermore, when `s` is non-empty, for each `n`, there exists a point `y` in `s` such that `A n` equals the derivative of `f` at `y`.
More concisely: Given a continuous function `f` with a derivative at every point of a measurable set `s`, there exists a countable partition `(t\_n)` of `s` into measurable sets, such that for each `n`, `f` is approximately linear with error `r(A\_n)` on `t\_n`, where `A\_n` is the derivative of `f` at some point in `t\_n`, and the `t\_n` cover `s`.
|
MeasureTheory.integrableOn_image_iff_integrableOn_abs_det_fderiv_smul
theorem MeasureTheory.integrableOn_image_iff_integrableOn_abs_det_fderiv_smul :
∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : FiniteDimensional ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {s : Set E}
{f : E → E} {f' : E → E →L[ℝ] E} [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E]
(μ : MeasureTheory.Measure E) [inst_7 : μ.IsAddHaarMeasure],
MeasurableSet s →
(∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
Set.InjOn f s →
∀ (g : E → F),
MeasureTheory.IntegrableOn g (f '' s) μ ↔
MeasureTheory.IntegrableOn (fun x => |(f' x).det| • g (f x)) s μ
This theorem states that for any finite-dimensional real vector space `E`, a measure space `E` with its Borel σ-algebra, and a measure `μ` that is an additive Haar measure, if you have a measurable set `s` in this space and an injective function `f` that is differentiable on `s`, then another function `g : E → F` is integrable over the image of `s` under `f` if and only if the function obtained by multiplying the determinant of the derivative of `f` by `g` composed with `f` is integrable over `s`. In other words, it provides a condition for the integrability of a function under a change of variables in terms of the integrability of a transformed function over the original domain. This theorem could be used to justify the change of variables in an integral in certain conditions.
More concisely: For a finite-dimensional real vector space `E` equipped with an additive Haar measure `μ`, if `s` is a measurable set, `f : s → E` is injective and differentiable, and `g : E → F` is integrable over the image `f[s]`, then `g ∘ f` and the determinant of `df/dx` are integrable over `s`.
|
MeasureTheory.measurable_image_of_fderivWithin
theorem MeasureTheory.measurable_image_of_fderivWithin :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E],
MeasurableSet s → (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) → Set.InjOn f s → MeasurableSet (f '' s)
The theorem `MeasureTheory.measurable_image_of_fderivWithin` states that if a function, `f`, is differentiable and injective on a measurable set, `s`, in a finite-dimensional real vector space, then the image of the set under the function, marked as `f '' s`, is also a measurable set. Here, a function is said to be differentiable at a point in the set if it has a derivative at that point within the set, defined by `HasFDerivWithinAt`. The function being injective on the set is defined by `Set.InjOn`, meaning that no two different points in the set map to the same point under the function. The space is equipped with the structure of a normed additive commutative group and a normed space over the reals, and also has a given measurable space structure that makes it a Borel space.
More concisely: If a differentiable and injective function defines a map between a measurable subset of a finite-dimensional real normed vector space and preserves the structure of a Borel space, then its image is also a measurable subset.
|
MeasureTheory.integrableOn_image_iff_integrableOn_abs_deriv_smul
theorem MeasureTheory.integrableOn_image_iff_integrableOn_abs_deriv_smul :
∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {s : Set ℝ} {f f' : ℝ → ℝ},
MeasurableSet s →
(∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
Set.InjOn f s →
∀ (g : ℝ → F),
MeasureTheory.IntegrableOn g (f '' s) MeasureTheory.volume ↔
MeasureTheory.IntegrableOn (fun x => |f' x| • g (f x)) s MeasureTheory.volume
This theorem states that for a function `f` that is injective and differentiable on a measurable set `s` in the real numbers, another function `g` is integrable over the image of `s` under `f` if and only if the absolute value of `f'` (the derivative of `f`) times `g` composed with `f` is integrable on `s`. This is a form of the change of variable formula for integrability in the setting of differentiable functions. The theorem requires that `f` is measurable on `s`, each point in `s` has a derivative within `s`, and `f` is injective on `s`. The space `F` is a normed group over the real numbers.
More concisely: For a differentiable, injective, and measurable function `f` from a measurable set `s` in the real numbers into a normed group `F`, `g` is integrable over `f[s]` if and only if the product of the absolute value of `f'` and `g ∘ f` is integrable on `s`.
|
MeasureTheory.map_withDensity_abs_det_fderiv_eq_addHaar
theorem MeasureTheory.map_withDensity_abs_det_fderiv_eq_addHaar :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E]
(μ : MeasureTheory.Measure E) [inst_5 : μ.IsAddHaarMeasure],
MeasurableSet s →
(∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
Set.InjOn f s →
Measurable f →
MeasureTheory.Measure.map f ((μ.restrict s).withDensity fun x => ENNReal.ofReal |(f' x).det|) =
μ.restrict (f '' s)
This theorem, known as the Change of Variables formula for differentiable functions, states that if we have a function `f` that is injective and differentiable on a measurable set `s` in a finite-dimensional real vector space `E`, then the pushforward of the measure with density equal to the absolute value of the determinant of the derivative of `f` at `x`, denoted as `|(f' x).det|`, is equal to the Lebesgue measure on the image of set `s` under the function `f`. This version of the theorem requires that `f` is measurable because, according to our definitions, the pushforward would be zero if `f` was not measurable.
This theorem can be used to transform integrals over `s` to integrals over `f(s)` with a change of density, which is particularly useful in probability theory and mathematical physics where one encounters change of variables in integrals frequently.
More concisely: If a differentiable, injective function `f` maps a measurable set `s` in a finite-dimensional real vector space to another measurable set and has a non-vanishing determinant of its derivative on `s`, then the pushforward measure of the Lebesgue measure on `s` under `f` is equal to the Lebesgue measure on `f(s)` with density `|det(f' x)|`.
|
MeasureTheory.measurableEmbedding_of_fderivWithin
theorem MeasureTheory.measurableEmbedding_of_fderivWithin :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E],
MeasurableSet s →
(∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) → Set.InjOn f s → MeasurableEmbedding (s.restrict f)
The theorem `MeasureTheory.measurableEmbedding_of_fderivWithin` states that if a function `f` is differentiable on a measurable set `s` and injective when restricted to `s`, then the restriction of `f` to `s` is a measurable embedding. Here, `s` and `f` are from a finite-dimensional normed addcomm group `E` with its normed space over the real numbers `ℝ`. The differentiability of `f` on `s` is expressed by the existence of the Frechet derivative `f'` at each point in `s`. The measurability of `s` and `f` are with respect to the measurable space structure of `E` and Borel sigma-algebra respectively. The concept of a measurable embedding in this context means that the restriction of `f` to `s` is both a measurable function and an embedding.
More concisely: If a differentiable and injective function `f` is defined on a measurable set `s` in a finite-dimensional normed addcomm group `E`, then the restriction of `f` to `s` is a measurable embedding.
|
MeasureTheory.aemeasurable_fderivWithin
theorem MeasureTheory.aemeasurable_fderivWithin :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E]
(μ : MeasureTheory.Measure E) [inst_5 : μ.IsAddHaarMeasure],
MeasurableSet s → (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) → AEMeasurable f' (μ.restrict s)
The theorem `MeasureTheory.aemeasurable_fderivWithin` states that for a function `f` defined on a measurable set `s` in a finite-dimensional normed additive commutative group `E` over the reals ℝ, if the derivative of `f` at every point `x` in `s` exists and equals `f'(x)`, then this derivative function `f'` is almost everywhere measurable on `s` with respect to the restriction of a measure `μ` to `s`. Here, "almost everywhere measurable" means that `f'` is equal to a measurable function except possibly on a set of measure zero. Also, the measure `μ` is assumed to be an additive Haar measure and the space `E` is equipped with a Borel measurable structure.
More concisely: If a function `f` with derivative `f'` is pointwise defined on a measurable set `s` in a finite-dimensional normed additive commutative group `E` over the reals, and the derivative exists at every point in `s` and is equal to `f'(x)`, then the derivative function `f'` is almost everywhere equal to a measurable function with respect to the restriction of an additive Haar measure to `s`.
|
MeasureTheory.addHaar_image_eq_zero_of_det_fderivWithin_eq_zero
theorem MeasureTheory.addHaar_image_eq_zero_of_det_fderivWithin_eq_zero :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E]
(μ : MeasureTheory.Measure E) [inst_5 : μ.IsAddHaarMeasure],
(∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) → (∀ x ∈ s, (f' x).det = 0) → ↑↑μ (f '' s) = 0
The theorem `MeasureTheory.addHaar_image_eq_zero_of_det_fderivWithin_eq_zero` represents a version of the Sard's Lemma, which is a statement in differential topology. It states that given a differentiable function `f` from a normed additive commutative group `E` to `E`, and a set `s` where the differential of `f` is not invertible (i.e., the determinant of the derivative at any point in `s` equals zero), then the image of this set under `f` has zero measure with respect to a given Add Haar measure `μ`. This theorem requires `E` to be a finite-dimensional real vector space, and the measures to be defined on a Borel space.
More concisely: If `f` is a differentiable function from a finite-dimensional real vector space `E` to `E` with a non-invertible derivative at every point in a set `s`, then the image of `s` under `f` has zero Haar measure.
|
MeasureTheory.mul_le_addHaar_image_of_lt_det
theorem MeasureTheory.mul_le_addHaar_image_of_lt_det :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
[inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (μ : MeasureTheory.Measure E) [inst_5 : μ.IsAddHaarMeasure]
(A : E →L[ℝ] E) {m : NNReal},
↑m < ENNReal.ofReal |A.det| →
∀ᶠ (δ : NNReal) in nhdsWithin 0 (Set.Ioi 0),
∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)
This theorem states that if a function `f` closely approximates a given linear map `A` in the Lipschitz sense, it expands the volume of any set by at least a factor of `m`, for any `m` less than the determinant of `A`. Here, the approximation and volume expansion are evaluated within an infinitesimally small neighborhood of `0`, excluding `0` itself.
The volume expansion is relative to a particular measure `μ`, which must satisfy the properties of an additive Haar measure. The theorem applies to any set within a finite-dimensional normed vector space over the real numbers, whose elements are measurable and respect the Borel sigma algebra.
More concisely: If a function `f` Lipschitz-approximates a linear map `A` and `μ` is an additive Haar measure, then `f` expands the volume of any measurable set by a factor of at least `m` within an infinitesimal neighborhood of `0`, for any `m` less than `det(A)`.
|
MeasureTheory.lintegral_abs_det_fderiv_eq_addHaar_image
theorem MeasureTheory.lintegral_abs_det_fderiv_eq_addHaar_image :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E]
(μ : MeasureTheory.Measure E) [inst_5 : μ.IsAddHaarMeasure],
MeasurableSet s →
(∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
Set.InjOn f s → ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ = ↑↑μ (f '' s)
This theorem, `MeasureTheory.lintegral_abs_det_fderiv_eq_addHaar_image`, states the change of variable formula for differentiable functions in the case of sets. Specifically, let `E` be a Normed Additive Commutative Group with a Normed Space structure over the real numbers and also a Finite Dimensional vector space over the real numbers. If `f` is a function from `E` to `E` that is injective and differentiable on a measurable set `s` (where differentiability is given by the derivative `f'`), and `μ` is an Add Haar measure on `E`, then the measure of the image of `s` under `f`, denoted `f '' s`, equals the non-negative extended real-valued Lebesgue integral over `s` of the absolute value of the determinant of `f'`, denoted `|(f' x).det|`, with respect to the measure `μ`. This result assumes that `E` is equipped with a Measurable Space structure making it a Borel Space. Note that the measurability of `f '' s` is provided by `measurable_image_of_fderivWithin`.
More concisely: The measure of the image of a measurable set under an injective, differentiable function with a determinable derivative is equal to the Lebesgue integral of the absolute value of the determinant of the derivative over the set with respect to the Add Haar measure.
|
MeasureTheory.addHaar_image_eq_zero_of_det_fderivWithin_eq_zero_aux
theorem MeasureTheory.addHaar_image_eq_zero_of_det_fderivWithin_eq_zero_aux :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E]
(μ : MeasureTheory.Measure E) [inst_5 : μ.IsAddHaarMeasure],
(∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
∀ (R : ℝ),
s ⊆ Metric.closedBall 0 R →
∀ (ε : NNReal), 0 < ε → (∀ x ∈ s, (f' x).det = 0) → ↑↑μ (f '' s) ≤ ↑ε * ↑↑μ (Metric.closedBall 0 R)
This theorem is an auxiliary statement towards a version of Sard's lemma in fixed dimension. It states that given a normed additive commutative group `E` that is also a normed space over real numbers `ℝ` and has a finite dimension, along with a set `s` in `E`, a function `f` from `E` to `E`, and a measurable space `E` that is also a Borel space, with a measure `μ` that is an additive Haar measure, if for every `x` in `s`, there exists a differential function `f'` at `x` within `s`, then for any real number `R` such that `s` is a subset of the closed ball of radius `R` centered at origin, and for any nonnegative real number `ε` that is greater than zero, if the determinant of `f'` at any `x` in `s` is zero, then the measure of the image of `s` under the function `f` is less than or equal to `ε` times the measure of the closed ball of radius `R` centered at origin.
More concisely: Given a finite-dimensional normed space `E` over `ℝ`, a measurable set `s` with Haar measure `μ`, a measurable function `f : E → E` such that `f'` exists at every `x` in `s`, if the determinant of `f'` is zero at some `x` in `s`, then the measure of `f(s)` is less than or equal to `εμ(B(0, R))`, where `ε > 0` and `B(0, R)` is the closed ball of radius `R` centered at the origin.
|
MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul
theorem MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul :
∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : FiniteDimensional ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {s : Set E}
{f : E → E} {f' : E → E →L[ℝ] E} [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E]
(μ : MeasureTheory.Measure E) [inst_7 : μ.IsAddHaarMeasure],
MeasurableSet s →
(∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
Set.InjOn f s → ∀ (g : E → F), ∫ (x : E) in f '' s, g x ∂μ = ∫ (x : E) in s, |(f' x).det| • g (f x) ∂μ
This is a theorem about the change of variables in integration for differentiable functions. It states that if you have a function `f` which is injective and differentiable on a measurable set `s`, then the integral of any function `g : E → F` over the image of `s` under `f` is equal to the integral of the absolute value of the determinant of the derivative of `f` scaled by `g ∘ f` over `s`. This theorem is essentially a generalization of the substitution rule from single-variable calculus to the context of functions between finite-dimensional real normed spaces.
More concisely: If `f : E → F` is injective and differentiable on a measurable set `s ⊆ E`, then ∫g(f(x)) d(m\_E)(x) = |∥DF(x)∥⁻¹∫|g(y)∥∥DF(x)∥⁴ d(m\_F)(y), where `m_E` and `m_F` are Lebesgue measures on `E` and `F` respectively, and `DF(x)` is the Jacobian matrix of `f` at `x`.
|
MeasureTheory.restrict_map_withDensity_abs_det_fderiv_eq_addHaar
theorem MeasureTheory.restrict_map_withDensity_abs_det_fderiv_eq_addHaar :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E]
(μ : MeasureTheory.Measure E) [inst_5 : μ.IsAddHaarMeasure],
MeasurableSet s →
(∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
Set.InjOn f s →
MeasureTheory.Measure.map (s.restrict f)
(MeasureTheory.Measure.comap Subtype.val (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) =
μ.restrict (f '' s)
This theorem states that, given a normed addative commutative group `E` that also forms a normed vector space over the real numbers ℝ and is finite-dimensional, along with a measure `μ` that is an additive Haar measure, a set `s` in `E`, and a function `f` mapping `E` to `E` with a derivative `f'`. If the set `s` is measurable, the function `f` has a derivative `f'` at every point in `s`, and `f` is injective on `s`, then the pushforward of the measure with density `|(f' x).det|` on `s` is equal to the restriction of the original measure `μ` to the image of `s` under `f`. This is expressed in terms of the restriction of `f` to `s`. The theorem essentially provides a change of variable formula for differentiable functions.
More concisely: Given a finite-dimensional, normed additive commutative group `E` over ℝ with a measurable, additive Haar measure `μ`, if a differentiable, injective function `f: E → E` has a measurable domain `s` and `|(f' x).det|` is integrable on `s`, then `μ` and the pushforward measure of `μ` under `f` on `f(s)` are equal.
|
MeasureTheory.addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero
theorem MeasureTheory.addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{s : Set E} {f : E → E} [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (μ : MeasureTheory.Measure E)
[inst_5 : μ.IsAddHaarMeasure], DifferentiableOn ℝ f s → ↑↑μ s = 0 → ↑↑μ (f '' s) = 0
The theorem `MeasureTheory.addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero` states that for any set `s` in a real finite-dimensional normed additive commutative group `E` and any function `f` from `E` to `E`, if `f` is differentiable on `s` and `s` has an Add Haar measure of zero (under a given measure `μ` which is an Add Haar measure), then the image of `s` under `f` also has an Add Haar measure of zero. In other words, a differentiable function maps sets of measure zero to sets of measure zero in the context of Add Haar measures.
More concisely: If a differentiable function maps a set of measure zero in a finite-dimensional real normed additive commutative group under Add Haar measure, then the image of that set has measure zero.
|
MeasureTheory.integral_image_eq_integral_abs_deriv_smul
theorem MeasureTheory.integral_image_eq_integral_abs_deriv_smul :
∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {s : Set ℝ} {f f' : ℝ → ℝ},
MeasurableSet s →
(∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
Set.InjOn f s → ∀ (g : ℝ → F), ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in s, |f' x| • g (f x)
The theorem `MeasureTheory.integral_image_eq_integral_abs_deriv_smul` states the change of variable formula for differentiable functions in one variable. Specifically, it states that if a function `f` is injective and differentiable on a measurable subset `s` of the real numbers, then the Bochner integral of a function `g` on the image of `s` under `f` is equal to the integral of the absolute value of the derivative of `f` at `x` scaled by `g` composed with `f` on `s`. This theorem is an important result in measure theory and provides a foundation for substitutions in integration.
More concisely: If a differentiable, injective function `f` maps a measurable set `s` to a new measurable set `t`, then the Bochner integral of `g(y)` over `t` equals the integral over `s` of the absolute value of `f'(x)` multiplied by `g(f(x))`.
|
exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt
theorem exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt :
∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : FiniteDimensional ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F]
[inst_5 : SecondCountableTopology F] (f : E → F) (s : Set E) (f' : E → E →L[ℝ] F),
(∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
∀ (r : (E →L[ℝ] F) → NNReal),
(∀ (A : E →L[ℝ] F), r A ≠ 0) →
∃ t A,
(∀ (n : ℕ), IsClosed (t n)) ∧
s ⊆ ⋃ n, t n ∧
(∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧
(s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)
This theorem states that if a function `f` has a derivative at every point of a set `s` in a finite-dimensional normed vector space over the real numbers, then it is possible to cover the set `s` with countably many closed subsets `t n`. On each of these subsets, `f` can be well approximated by a sequence of linear maps `A n`. More specifically, for any function `r` from the linear maps to the nonnegative real numbers (where `r` never equals zero), there exist such a sequence of closed sets `t` and a sequence of linear maps `A`, such that the set `s` is a subset of the union of all these `t n`, and for each natural number `n`, `f` approximates the linear map `A n` on the intersection of `s` and `t n` within a radius of `r (A n)`. Furthermore, if `s` is not empty, for each natural number `n`, there exists a point `y` in `s` where the derivative of `f` is equal to `A n`.
More concisely: Given a function `f` with a derivative at every point of a set `s` in a finite-dimensional normed vector space over the real numbers, there exist countably many closed sets `t n` and a sequence of linear maps `An` such that `s` is covered by the `tn`, and for each `n` and `x` in `sn`, `|f(x) - An(x)| < r(An)` for some non-zero function `r`. Furthermore, for each non-empty `sn`, there exists a point `y` in `sn` with `f'(y) = An`.
|
MeasureTheory.addHaar_image_le_mul_of_det_lt
theorem MeasureTheory.addHaar_image_le_mul_of_det_lt :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
[inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (μ : MeasureTheory.Measure E) [inst_5 : μ.IsAddHaarMeasure]
(A : E →L[ℝ] E) {m : NNReal},
ENNReal.ofReal |A.det| < ↑m →
∀ᶠ (δ : NNReal) in nhdsWithin 0 (Set.Ioi 0),
∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑↑μ (f '' s) ≤ ↑m * ↑↑μ s
The theorem `MeasureTheory.addHaar_image_le_mul_of_det_lt` states that for a given function `f`, which is close to a linear map `A` in the Lipschitz sense, it expands the volume of any set by at most `m` for any `m` greater than the determinant of `A`. This is true for any normed additive commutative group `E` that is also a finite-dimensional real vector space, equipped with a borel measure `μ` that has the additivity property of Haar measures. The closeness of `f` to `A` is measured by a non-negative real number `δ` that is arbitrarily close to `0` but not including `0`. The theorem states that the measure of the image of the set under `f` is less than or equal to `m` times the measure of the original set.
More concisely: For a Lipschitz close function `f` to a linear map `A` on a finite-dimensional real vector space `E` with Haar measure `μ`, the image measure of any set under `f` is less than or equal to the determinant of `A` times the measure of the original set.
|
ApproximatesLinearOn.norm_fderiv_sub_le
theorem ApproximatesLinearOn.norm_fderiv_sub_le :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{s : Set E} {f : E → E} [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (μ : MeasureTheory.Measure E)
[inst_5 : μ.IsAddHaarMeasure] {A : E →L[ℝ] E} {δ : NNReal},
ApproximatesLinearOn f A s δ →
MeasurableSet s →
∀ (f' : E → E →L[ℝ] E),
(∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) → ∀ᵐ (x : E) ∂μ.restrict s, ‖f' x - A‖₊ ≤ δ
The theorem `ApproximatesLinearOn.norm_fderiv_sub_le` states that for a differentiable function `f` that is approximated by a linear map `A` within a finite-dimensional vector space `E` over the field of real numbers, on a measurable set `s` up to some non-negative real number `δ`, the norm of the difference between the derivative of `f` at each point `x` in `s` and `A` is less than or equal to `δ` almost everywhere in `s` under the restriction of measure `μ`. This means, in simpler terms, that the difference between the derivative of `f` and linear map `A` is typically bounded by `δ` within the boundaries of `s`.
More concisely: Given a differentiable function `f` approximated by a linear map `A` within a finite-dimensional vector space `E` over the real numbers, and a measurable set `s` with measure `μ`, the norm of the difference between `f'` and `A` is less than or equal to `δ` almost everywhere in `s`.
|