Monotone.ae_hasDerivAt
theorem Monotone.ae_hasDerivAt :
∀ {f : ℝ → ℝ} (hf : Monotone f),
∀ᵐ (x : ℝ), HasDerivAt f (hf.stieltjesFunction.measure.rnDeriv MeasureTheory.volume x).toReal x
This theorem states that for any real-valued monotone function `f`, the function is almost everywhere differentiable. Moreover, the derivative of `f` at almost every point `x` is equal to the real part of the Radon-Nikodym derivative of the Stieltjes measure associated with the monotone function `f` with respect to the Lebesgue measure, at that point. The phrase "almost everywhere" means that the set of points where the statement is not true has Lebesgue measure zero.
More concisely: A real-valued monotone function `f` is almost everywhere differentiable, and its derivative at almost every point `x` equals the real part of the Radon-Nikodym derivative of `f`'s Stieltjes measure with respect to the Lebesgue measure.
|
Monotone.ae_differentiableAt
theorem Monotone.ae_differentiableAt : ∀ {f : ℝ → ℝ}, Monotone f → ∀ᵐ (x : ℝ), DifferentiableAt ℝ f x
This theorem states that if a function `f` mapping real numbers to real numbers is monotone, then the function is differentiable at almost every point in the real number space with respect to the Lebesgue measure. In mathematical terms, for almost all `x` in the set of real numbers (denoted as ℝ), the function `f` has a derivative at that point `x`. The "almost everywhere" term is used in the sense of Lebesgue measure, meaning that the set of points where the property (in this case, differentiability) fails has measure zero.
More concisely: A monotone real-valued function is differentiable almost everywhere with respect to Lebesgue measure.
|
MonotoneOn.ae_differentiableWithinAt
theorem MonotoneOn.ae_differentiableWithinAt :
∀ {f : ℝ → ℝ} {s : Set ℝ},
MonotoneOn f s → MeasurableSet s → ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict s, DifferentiableWithinAt ℝ f s x
This theorem states that a real-valued function, which is monotone on a given set, is differentiable almost everywhere on this set in the sense of Lebesgue measure. This version of the theorem assumes that the set is measurable and uses the volume measure restricted to this set. In other words, for all such functions `f` and sets `s`, if `f` is monotone on `s` and `s` is a measurable set, then for almost every real number `x` with respect to the measure `MeasureTheory.volume.restrict s`, `f` is differentiable at `x` within the set `s`.
An 'almost everywhere' statement signifies that the property holds for all elements except for a set of measure zero. Essentially, this theorem sheds light on the fact that monotone functions are "mostly" differentiable, with potential exceptions only on a set of zero measure. There is also a version of this theorem that doesn't require the measurability of the set, referred to as `MonotoneOn.ae_differentiableWithinAt_of_mem`.
More concisely: A monotone real-valued function is differentiable almost everywhere on a measurable set with respect to Lebesgue measure.
|
tendsto_apply_add_mul_sq_div_sub
theorem tendsto_apply_add_mul_sq_div_sub :
∀ {f : ℝ → ℝ} {x a c d : ℝ} {l : Filter ℝ},
l ≤ nhdsWithin x {x}ᶜ →
Filter.Tendsto (fun y => (f y - d) / (y - x)) l (nhds a) →
Filter.Tendsto (fun y => y + c * (y - x) ^ 2) l l →
Filter.Tendsto (fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)) l (nhds a)
This theorem states that if the expression `(f y - f x) / (y - x)` tends to a certain limit as `y` approaches `x` (possibly only from one side or along certain lines), then the same limiting behavior holds for the expression `(f (y + c * (y - x) ^ 2) - d) / (y - x)`. This is essentially saying that adding a small perturbation `(c * (y - x) ^ 2)` to the argument of `f` in the numerator doesn't change the limiting behavior. This theorem is particularly useful in the study of almost everywhere differentiability of monotone functions, where such perturbations often arise.
More concisely: If `f` is a function for which `(f y - f x) / (y - x)` converges to a limit as `y` approaches `x`, then `(f (y + c * (y - x) ^ 2) - d) / (y - x)` also converges to the same limit as `y` approaches `x`.
|
StieltjesFunction.ae_hasDerivAt
theorem StieltjesFunction.ae_hasDerivAt :
∀ (f : StieltjesFunction), ∀ᵐ (x : ℝ), HasDerivAt (↑f) (f.measure.rnDeriv MeasureTheory.volume x).toReal x := by
sorry
The theorem `StieltjesFunction.ae_hasDerivAt` states that for any Stieltjes function `f`, almost everywhere (i.e., except on a set of measure zero) on the real line, the function `f` has a derivative at point `x`. Furthermore, the derivative of `f` at `x` equals the Radon-Nikodym derivative of the measure associated with `f` (that is, `f.measure`) with respect to the Lebesgue measure, converted to a real number.
More concisely: For any Stieltjes function `f`, almost everywhere on the real line, the derivative of `f` exists and is equal to the Radon-Nikodym derivative of `f.measure` with respect to the Lebesgue measure.
|
MonotoneOn.ae_differentiableWithinAt_of_mem
theorem MonotoneOn.ae_differentiableWithinAt_of_mem :
∀ {f : ℝ → ℝ} {s : Set ℝ}, MonotoneOn f s → ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
This theorem states that for any real-valued function `f` and any set `s` of real numbers, if the function `f` is monotone on the set `s`, then the function `f` is differentiable almost everywhere within set `s`. In other words, there exists a derivative of `f` at almost every point in `s`. Note that the theorem does not require the set `s` to be measurable. There is another version of this theorem that deals with the measure-theoretic concept of `volume.restrict s`, which requires `s` to be measurable.
More concisely: If a real-valued function `f` is monotone on a set `s` of real numbers, then `f` is differentiable almost everywhere in `s`.
|