LipschitzOnWith.ae_differentiableWithinAt
theorem LipschitzOnWith.ae_differentiableWithinAt :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
[inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {F : Type u_2} [inst_5 : NormedAddCommGroup F]
[inst_6 : NormedSpace ℝ F] {C : NNReal} {s : Set E} {μ : MeasureTheory.Measure E} [inst_7 : μ.IsAddHaarMeasure]
[inst_8 : FiniteDimensional ℝ F] {f : E → F},
LipschitzOnWith C f s → MeasurableSet s → ∀ᵐ (x : E) ∂μ.restrict s, DifferentiableWithinAt ℝ f s x
Rademacher's theorem states that if a function, which maps between finite-dimensional real vector spaces, is Lipschitz continuous on a set, then the function is differentiable almost everywhere within that set. In other words, for almost every point in the set, we can find a derivative of the function at that point. This theorem applies under the additional conditions that the measure on the domain is an add-Haar measure and the domain is a measurable set in the Borel space.
More concisely: Rademacher's theorem asserts that a Lipschitz continuous function between finite-dimensional real vector spaces is differentiable almost everywhere with respect to an add-Haar measure on a measurable set in the Borel space.
|
LipschitzWith.integral_lineDeriv_mul_eq
theorem LipschitzWith.integral_lineDeriv_mul_eq :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
[inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {C D : NNReal} {f g : E → ℝ} {μ : MeasureTheory.Measure E}
[inst_5 : μ.IsAddHaarMeasure],
LipschitzWith C f →
LipschitzWith D g →
HasCompactSupport g →
∀ (v : E), ∫ (x : E), lineDeriv ℝ f x v * g x ∂μ = ∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ
This theorem, called `LipschitzWith.integral_lineDeriv_mul_eq`, states the integration by parts formula for the line derivative of Lipschitz continuous functions, assuming one of them has compact support. More formally, for any normed add-commutative group `E` that is a finite-dimensional real normed space and has a Borel structure, given any two non-negative real numbers `C` and `D`, any two functions `f` and `g` from `E` to the real numbers, and a measure `μ` that is an additive Haar measure, if `f` is Lipschitz continuous with constant `C`, `g` is Lipschitz continuous with constant `D`, and `g` has compact support, then for every `v` in `E`, the integral over `E` of the product of the line derivative of `f` at `x` in the direction `v` and `g` at `x`, with respect to `μ`, equals the integral over `E` of the product of the line derivative of `g` at `x` in the direction `-v` and `f` at `x`, with respect to `μ`.
More concisely: For Lipschitz continuous functions `f` and `g` with compact support on a finite-dimensional real normed space `E` endowed with an additive Haar measure `μ`, the integration by parts formula holds: ∫(v.DF(x)⋅g(x) dμ) = ∫(-v.Dg(x)⋅f(x) dμ), where `v` is any vector in `E` and `DP` denotes the line derivative.
|
LipschitzOnWith.ae_differentiableWithinAt_of_mem_pi
theorem LipschitzOnWith.ae_differentiableWithinAt_of_mem_pi :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
[inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {C : NNReal} {μ : MeasureTheory.Measure E}
[inst_5 : μ.IsAddHaarMeasure] {ι : Type u_3} [inst_6 : Fintype ι] {f : E → ι → ℝ} {s : Set E},
LipschitzOnWith C f s → ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
This theorem states that a function defined on a finite-dimensional space, which is Lipschitz continuous on a set and takes values in a product space, is differentiable almost everywhere within this set. The key conditions for this theorem are that the function is Lipschitz continuous on the set and that the space is finite-dimensional. Note that this theorem has been superseded by the more general `LipschitzOnWith.ae_differentiableWithinAt_of_mem` which applies to functions taking values in any finite-dimensional space.
More concisely: A Lipschitz continuous function on a finite-dimensional set is almost everywhere differentiable.
|
LipschitzOnWith.ae_differentiableWithinAt_of_mem
theorem LipschitzOnWith.ae_differentiableWithinAt_of_mem :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
[inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {F : Type u_2} [inst_5 : NormedAddCommGroup F]
[inst_6 : NormedSpace ℝ F] {C : NNReal} {s : Set E} {μ : MeasureTheory.Measure E} [inst_7 : μ.IsAddHaarMeasure]
[inst_8 : FiniteDimensional ℝ F] {f : E → F},
LipschitzOnWith C f s → ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
This is Rademacher's theorem, which states that if a function operates between finite-dimensional real vector spaces and is Lipschitz continuous on a set, then it is differentiable almost everywhere on that set. Here, "almost everywhere" means that the function is differentiable at all points in the set, except possibly for a subset of measure zero. The theorem applies to functions which are Lipschitz continuous with respect to a nonnegative real constant. This property of Lipschitz continuity requires that the distance between the images of any two points in the set does not exceed the constant times the distance between the points themselves.
More concisely: If a real-valued function between finite-dimensional real vector spaces is Lipschitz continuous on a set, then it is differentiable almost everywhere on that set.
|
LipschitzOnWith.ae_differentiableWithinAt_of_mem_of_real
theorem LipschitzOnWith.ae_differentiableWithinAt_of_mem_of_real :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
[inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {C : NNReal} {f : E → ℝ} {s : Set E}
{μ : MeasureTheory.Measure E} [inst_5 : μ.IsAddHaarMeasure],
LipschitzOnWith C f s → ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
This theorem states that for a real-valued function defined on a finite-dimensional space, if it exhibits Lipschitz continuity over a set, then the function is differentiable almost everywhere within this set. The theorem is superseded by `LipschitzOnWith.ae_differentiableWithinAt_of_mem` which can handle functions that take values in any finite-dimensional space, not just the real numbers. In this context, "almost everywhere" means that the set of points where the function is not differentiable has measure zero with respect to the underlying measure on the space.
More concisely: A real-valued function that is Lipschitz continuous on a set in a finite-dimensional space is differentiable almost everywhere within that set.
|
LipschitzWith.hasFderivAt_of_hasLineDerivAt_of_closure
theorem LipschitzWith.hasFderivAt_of_hasLineDerivAt_of_closure :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {C : NNReal} {f : E → F},
LipschitzWith C f →
∀ {s : Set E},
Metric.sphere 0 1 ⊆ closure s →
∀ {L : E →L[ℝ] F} {x : E}, (∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v) → HasFDerivAt f L x
The theorem `LipschitzWith.hasFderivAt_of_hasLineDerivAt_of_closure` states that if a Lipschitz continuous function, `f`, has line derivatives at a point `x` in a dense set of directions `s` all given by a single continuous linear map `L`, then the function `f` admits `L` as its Fréchet derivative at `x`. Here, 'dense set of directions' is defined as the set `s` such that the unit sphere is contained within the closure of `s`. The Lipschitz continuity of `f` is guaranteed by a nonnegative real number `C`. In other words, if `f` is Lipschitz continuous and for all vectors `v` in a dense set of directions, the line derivative of `f` at `x` in the direction `v` is given by `L v`, then the Fréchet derivative of `f` at `x` is `L`. The theorem is set in the context of a finite-dimensional real normed vector space.
More concisely: If a Lipschitz continuous function `f` on a finite-dimensional real normed vector space has line derivatives at a point `x` in the direction of a dense set of vectors `s`, all given by a single continuous linear map `L`, then `f` has `L` as its Fréchet derivative at `x`.
|
LipschitzWith.ae_differentiableAt
theorem LipschitzWith.ae_differentiableAt :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
[inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {F : Type u_2} [inst_5 : NormedAddCommGroup F]
[inst_6 : NormedSpace ℝ F] {C : NNReal} {μ : MeasureTheory.Measure E} [inst_7 : μ.IsAddHaarMeasure]
[inst_8 : FiniteDimensional ℝ F] {f : E → F}, LipschitzWith C f → ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x
Rademacher's theorem states that a Lipschitz function, which is a function whose difference between the values at two different points is at most a certain constant times the distance between the two points, between finite-dimensional real vector spaces is differentiable almost everywhere. In other words, for any function `f` from a real finite-dimensional vector space `E` into another `F`, if `f` is Lipschitz continuous, then `f` is differentiable at almost every point in `E` with respect to the Haar measure `μ` (a measure that is invariant under shifts and scaling). Here, almost everywhere means except on a set of measure zero.
More concisely: A Lipschitz function between finite-dimensional real vector spaces is almost everywhere differentiable with respect to Haar measure.
|
LipschitzWith.ae_differentiableAt_of_real
theorem LipschitzWith.ae_differentiableAt_of_real :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
[inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {C : NNReal} {f : E → ℝ} {μ : MeasureTheory.Measure E}
[inst_5 : μ.IsAddHaarMeasure], LipschitzWith C f → ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x
This theorem states that a real-valued function (`f : E → ℝ`), defined on a finite-dimensional space (`E`) that is equipped with a normed additive commutative group structure and a normed space structure over the real numbers, is differentiable almost everywhere if it is Lipschitz continuous. The context includes a nonnegative real number `C`, a measure `μ` on `E` that is an additive Haar measure, and the Borel sigma-algebra on `E`. The statement "almost everywhere" means that the set of points in `E` where `f` is not differentiable has measure zero with respect to the measure `μ`. This theorem has been superseded by a more general one, `LipschitzWith.ae_differentiableAt`, which applies not just to real-valued functions but to functions taking values in any finite-dimensional space.
More concisely: A real-valued function on a finite-dimensional normed space is differentiable almost everywhere if it is Lipschitz continuous.
|
LipschitzWith.ae_lineDeriv_sum_eq
theorem LipschitzWith.ae_lineDeriv_sum_eq :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
[inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {C : NNReal} {f : E → ℝ} {μ : MeasureTheory.Measure E}
[inst_5 : μ.IsAddHaarMeasure],
LipschitzWith C f →
∀ {ι : Type u_3} (s : Finset ι) (a : ι → ℝ) (v : ι → E),
∀ᵐ (x : E) ∂μ, lineDeriv ℝ f x (s.sum fun i => a i • v i) = s.sum fun i => a i • lineDeriv ℝ f x (v i)
This theorem states that for a Lipschitz continuous function `f` from a normed additive commutative group `E` to the real numbers `ℝ`, where `E` is also a finite-dimensional `ℝ`-module and a measurable space with Borel sigma-algebra, if the function `f` is Lipschitz continuous with a nonnegative constant `C`, then almost everywhere (with respect to a given add-Haar measure `μ` on `E`), the linear derivative of `f` with respect to a sum of scaled vectors is equal to the sum of the scaled linear derivatives of `f` with respect to each individual vector. The sum and the scaling factors are indexed by elements `i` of a finite set `s`, and the vectors are provided by a function `v` mapping these indices `i` to vectors in `E`.
More concisely: For a Lipschitz continuous function `f` from a finite-dimensional normed additive commutative group `E` with a Borel sigma-algebra and a given add-Haar measure `μ`, if `f` is Lipschitz with constant `C` and almost everywhere, then the linear derivative of `f` with respect to the sum of scaled vectors equals the sum of the scaled linear derivatives with respect to each individual vector.
|