Revision #3220 → #3774 · back to history
modifiedMean value theorem (informal statement)c058c1d5034f
| Field | From #3220 | To #3774 |
|---|
| note | Mathlib's `exists_hasDerivAt_eq_slope` directly states the existence of c ∈ Ioo a b with f' c = (f b − f a)/(b − a) under continuity on Icc a b and differentiability on Ioo a b. | Verified: `exists_hasDerivAt_eq_slope` directly states the existence of c ∈ Ioo a b with f' c = (f b − f a)/(b − a) under continuity on Icc a b and differentiability on Ioo a b. |
modifiedMean value theorem2cf30cd129cd
| Field | From #3220 | To #3774 |
|---|
| note | Exact formalization of Lagrange's MVT with `ContinuousOn (Icc a b)` and `HasDerivAt` on `Ioo a b` hypotheses. | Verified: exact formalization of Lagrange's MVT with `ContinuousOn (Icc a b)` and `HasDerivAt` on `Ioo a b` hypotheses. |
modifiedZero derivative implies constant4a1703fe8a59
| Field | From #3220 | To #3774 |
|---|
| note | `constant_of_derivWithin_zero` shows a function with zero derivative on `Icc a b` is constant; `is_const_of_deriv_eq_zero` gives the global version. | Verified: `constant_of_derivWithin_zero` shows a function with zero derivative on `Icc a b` is constant. |
modifiedEqual derivatives differ by constant1ae231a283ce
| Field | From #3220 | To #3774 |
|---|
| note | `eq_of_derivWithin_eq` (and `IsOpen.exists_eq_add_of_deriv_eq`) states that two functions with equal derivatives differ by a constant. | Verified: `eq_of_derivWithin_eq` states that two functions with equal derivatives on a set are equal (up to a constant), and `IsOpen.exists_eq_add_of_deriv_eq` gives the additive version. |
modifiedGeneral antiderivativedf2c76486324
| Field | From #3220 | To #3774 |
|---|
| note | The 'most general antiderivative' statement follows directly from `IsOpen.exists_eq_add_of_deriv_eq`/`eq_of_derivWithin_eq`. | Verified: the 'most general antiderivative' statement follows directly from `IsOpen.exists_eq_add_of_deriv_eq`. |
modifiedCauchy's mean value theorem64ba8c033bf6
| Field | From #3220 | To #3774 |
|---|
| note | `exists_ratio_hasDerivAt_eq_ratio_slope` exactly formalizes Cauchy's MVT: (g b − g a)·f' c = (f b − f a)·g' c. | Verified: `exists_ratio_hasDerivAt_eq_ratio_slope` exactly formalizes Cauchy's MVT: (g b − g a)·f' c = (f b − f a)·g' c. |
modifiedMean value theorem in several variables815a520ec42a
| Field | From #3220 | To #3774 |
|---|
| note | `domain_mvt` formalizes the multivariate MVT for `f : E → ℝ` on a convex set: there is z on the segment with `f y − f x = f' z (y − x)`. | Verified: `domain_mvt` formalizes the multivariate MVT for `f : E → ℝ` on a convex set: there is z on the segment with `f y − f x = f' z (y − x)`. |
modifiedLipschitz continuity on convex domain with bounded partials1285b180181b
| Field | From #3220 | To #3774 |
|---|
| note | `Convex.lipschitzOnWith_of_nnnorm_fderiv_le` gives `LipschitzOnWith C f s` from a bound on `‖fderiv 𝕜 f x‖₊` on a convex set. | Verified: `Convex.lipschitzOnWith_of_nnnorm_fderiv_le` gives `LipschitzOnWith C f s` from a bound on `‖fderiv 𝕜 f x‖₊` on a convex set. |
modifiedVanishing partial derivatives on connected open set imply constantbc36cf21759b
| Field | From #3220 | To #3774 |
|---|
| note | `IsOpen.is_const_of_fderiv_eq_zero` requires `IsOpen s` and `IsPreconnected s` plus vanishing Fréchet derivative, concluding `f` is constant on `s`. | Verified: `IsOpen.is_const_of_fderiv_eq_zero` requires `IsOpen s` and `IsPreconnected s` plus vanishing Fréchet derivative, concluding `f` is constant on `s`. |
modifiedMean value theorem for vector-valued functionse27b74dd575a
| Field | From #3220 | To #3774 |
|---|
| note | Vector-valued MVT (inequality form) is `norm_image_sub_le_of_norm_deriv_le_segment`: `‖f x − f a‖ ≤ C·(x − a)` when `‖f'‖ ≤ C` on `[a, b]`. | Verified: vector-valued MVT (inequality form) is `norm_image_sub_le_of_norm_deriv_le_segment`: `‖f x − f a‖ ≤ C·(x − a)` when `‖f'‖ ≤ C` on `[a, b]`. |
modifiedMean value inequality7d4f7d1d06d7
| Field | From #3220 | To #3774 |
|---|
| note | `Convex.norm_image_sub_le_of_norm_fderiv_le` states `‖f y − f x‖ ≤ C·‖y − x‖` on a convex set when the Fréchet derivative is bounded by `C`. | Verified: `Convex.norm_image_sub_le_of_norm_fderiv_le` states `‖f y − f x‖ ≤ C·‖y − x‖` on a convex set when the Fréchet derivative is bounded by `C`. |
modifiedFirst mean value theorem for definite integralsef1feebc7ecb
| Field | From #3220 | To #3774 |
|---|
| note | Specializing `exists_eq_const_mul_intervalIntegral_of_nonneg` with `g = 1` gives the basic first integral MVT `∫ f = f c · (b − a)`. | Verified: specializing `exists_eq_const_mul_intervalIntegral_of_nonneg` with `g = 1` gives the basic first integral MVT `∫ f = f c · (b − a)`. |
modifiedFirst mean value theorem (weighted form)ab890c932193
| Field | From #3220 | To #3774 |
|---|
| note | `exists_eq_const_mul_intervalIntegral_of_nonneg` (and its a.e. variant) is exactly the weighted first MVT for integrals. | Verified: `exists_eq_const_mul_intervalIntegral_of_nonneg` is exactly the weighted first MVT for integrals with nonneg weight. |
modifiedRolle's theorem4cfd7f4cfe97
| Field | From #3220 | To #3774 |
|---|
| note | Rolle's theorem is `exists_hasDerivAt_eq_zero` in `Mathlib.Analysis.Calculus.LocalExtr.Rolle` (module corrected from `Deriv.MeanValue`): with `f a = f b`, continuity on `Icc a b`, and `HasDerivAt` on `Ioo a b`, there exists `c ∈ Ioo a b` with `f' c = 0`. | Verified: Rolle's theorem is `exists_hasDerivAt_eq_zero` in `Mathlib.Analysis.Calculus.LocalExtr.Rolle`. |
modifiedCauchy–Schwarz inequality (used in vector MVT bound)2bd1728af8e4
| Field | From #3220 | To #3774 |
|---|
| note | Cauchy–Schwarz is `norm_inner_le_norm` in Mathlib (the previously cited `inner_mul_le_norm_mul_norm` does not exist; `abs_real_inner_le_norm` is the real-valued variant). | Verified: Cauchy–Schwarz is `norm_inner_le_norm` in `Mathlib.Analysis.InnerProductSpace.Basic`. |
addedRolle's theorem (used in Cauchy MVT proof)ac63c930aec2
addedL'Hôpital's rule (consequence of Cauchy MVT)daf7437148af
addedFundamental theorem of calculus (used in first integral MVT)e458cacfac84