From bdd7632ed5c4ca79a2c668ec7cf3a7842a787516 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Tue, 9 Jan 2024 18:26:11 +0000 Subject: [PATCH] chore(*): fix more names (#9593) Grep for `^[^#].*deriv_within` and fix all occurrences. --- Mathlib/Analysis/Calculus/ContDiff/Defs.lean | 2 +- Mathlib/Analysis/Calculus/FDeriv/Basic.lean | 6 +++--- Mathlib/Analysis/Calculus/Taylor.lean | 6 +++--- Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean | 6 +++--- 4 files changed, 10 insertions(+), 10 deletions(-) diff --git a/Mathlib/Analysis/Calculus/ContDiff/Defs.lean b/Mathlib/Analysis/Calculus/ContDiff/Defs.lean index 393452d43b22d..965b57d8093cd 100644 --- a/Mathlib/Analysis/Calculus/ContDiff/Defs.lean +++ b/Mathlib/Analysis/Calculus/ContDiff/Defs.lean @@ -892,7 +892,7 @@ theorem Filter.EventuallyEq.iteratedFDerivWithin' (h : fโ‚ =แถ [๐“[s] x] f) ( iteratedFDerivWithin ๐•œ n fโ‚ t =แถ [๐“[s] x] iteratedFDerivWithin ๐•œ n f t := by induction' n with n ihn ยท exact h.mono fun y hy => FunLike.ext _ _ fun _ => hy - ยท have : fderivWithin ๐•œ _ t =แถ [๐“[s] x] fderivWithin ๐•œ _ t := ihn.fderiv_within' ht + ยท have : fderivWithin ๐•œ _ t =แถ [๐“[s] x] fderivWithin ๐•œ _ t := ihn.fderivWithin' ht apply this.mono intro y hy simp only [iteratedFDerivWithin_succ_eq_comp_left, hy, (ยท โˆ˜ ยท)] diff --git a/Mathlib/Analysis/Calculus/FDeriv/Basic.lean b/Mathlib/Analysis/Calculus/FDeriv/Basic.lean index 00478ed34a603..72825d3b97d31 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Basic.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Basic.lean @@ -1026,17 +1026,17 @@ theorem Filter.EventuallyEq.fderivWithin_eq (hs : fโ‚ =แถ [๐“[s] x] f) (hx : simp only [fderivWithin, hs.hasFDerivWithinAt_iff hx] #align filter.eventually_eq.fderiv_within_eq Filter.EventuallyEq.fderivWithin_eq -theorem Filter.EventuallyEq.fderiv_within' (hs : fโ‚ =แถ [๐“[s] x] f) (ht : t โŠ† s) : +theorem Filter.EventuallyEq.fderivWithin' (hs : fโ‚ =แถ [๐“[s] x] f) (ht : t โŠ† s) : fderivWithin ๐•œ fโ‚ t =แถ [๐“[s] x] fderivWithin ๐•œ f t := (eventually_nhdsWithin_nhdsWithin.2 hs).mp <| eventually_mem_nhdsWithin.mono fun _y hys hs => EventuallyEq.fderivWithin_eq (hs.filter_mono <| nhdsWithin_mono _ ht) (hs.self_of_nhdsWithin hys) -#align filter.eventually_eq.fderiv_within' Filter.EventuallyEq.fderiv_within' +#align filter.eventually_eq.fderiv_within' Filter.EventuallyEq.fderivWithin' protected theorem Filter.EventuallyEq.fderivWithin (hs : fโ‚ =แถ [๐“[s] x] f) : fderivWithin ๐•œ fโ‚ s =แถ [๐“[s] x] fderivWithin ๐•œ f s := - hs.fderiv_within' Subset.rfl + hs.fderivWithin' Subset.rfl #align filter.eventually_eq.fderiv_within Filter.EventuallyEq.fderivWithin theorem Filter.EventuallyEq.fderivWithin_eq_nhds (h : fโ‚ =แถ [๐“ x] f) : diff --git a/Mathlib/Analysis/Calculus/Taylor.lean b/Mathlib/Analysis/Calculus/Taylor.lean index 78fe076ec705e..09acadf675310 100644 --- a/Mathlib/Analysis/Calculus/Taylor.lean +++ b/Mathlib/Analysis/Calculus/Taylor.lean @@ -214,14 +214,14 @@ theorem taylorWithinEval_hasDerivAt_Ioo {f : โ„ โ†’ E} {a b t : โ„} (x : โ„) /-- Calculate the derivative of the Taylor polynomial with respect to `xโ‚€`. Version for closed intervals -/ -theorem has_deriv_within_taylorWithinEval_at_Icc {f : โ„ โ†’ E} {a b t : โ„} (x : โ„) {n : โ„•} +theorem hasDerivWithinAt_taylorWithinEval_at_Icc {f : โ„ โ†’ E} {a b t : โ„} (x : โ„) {n : โ„•} (hx : a < b) (ht : t โˆˆ Icc a b) (hf : ContDiffOn โ„ n f (Icc a b)) (hf' : DifferentiableOn โ„ (iteratedDerivWithin n f (Icc a b)) (Icc a b)) : HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x) (((n ! : โ„)โปยน * (x - t) ^ n) โ€ข iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a b) t := hasDerivWithinAt_taylorWithinEval (uniqueDiffOn_Icc hx t ht) (uniqueDiffOn_Icc hx) self_mem_nhdsWithin ht rfl.subset hf (hf' t ht) -#align has_deriv_within_taylor_within_eval_at_Icc has_deriv_within_taylorWithinEval_at_Icc +#align has_deriv_within_taylor_within_eval_at_Icc hasDerivWithinAt_taylorWithinEval_at_Icc /-! ### Taylor's theorem with mean value type remainder estimate -/ @@ -343,7 +343,7 @@ theorem taylor_mean_remainder_bound {f : โ„ โ†’ E} {a b C x : โ„} {n : โ„•} (h (((โ†‘n !)โปยน * (x - t) ^ n) โ€ข iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t := by intro t ht have I : Icc a x โŠ† Icc a b := Icc_subset_Icc_right hx.2 - exact (has_deriv_within_taylorWithinEval_at_Icc x h (I ht) hf.of_succ hf').mono I + exact (hasDerivWithinAt_taylorWithinEval_at_Icc x h (I ht) hf.of_succ hf').mono I have := norm_image_sub_le_of_norm_deriv_le_segment' A h' x (right_mem_Icc.2 hx.1) simp only [taylorWithinEval_self] at this refine' this.trans_eq _ diff --git a/Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean b/Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean index 735bce0dda645..ec37eb5003b74 100644 --- a/Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean +++ b/Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean @@ -376,7 +376,7 @@ See also * `interval_integral.integral_eq_sub_of_has_deriv_right_of_le` for a version that only assumes right differentiability of `f`; -* `MeasureTheory.integral_eq_of_has_deriv_within_at_off_countable` for a version that works both +* `MeasureTheory.integral_eq_of_hasDerivWithinAt_off_countable` for a version that works both for `a โ‰ค b` and `b โ‰ค a` at the expense of using unordered intervals instead of `Set.Icc`. -/ theorem integral_eq_of_hasDerivWithinAt_off_countable_of_le (f f' : โ„ โ†’ E) {a b : โ„} (hle : a โ‰ค b) {s : Set โ„} (hs : s.Countable) (Hc : ContinuousOn f (Icc a b)) @@ -415,7 +415,7 @@ interval and is differentiable off a countable set `s`. See also `measure_theory.interval_integral.integral_eq_sub_of_has_deriv_right` for a version that only assumes right differentiability of `f`. -/ -theorem integral_eq_of_has_deriv_within_at_off_countable (f f' : โ„ โ†’ E) {a b : โ„} {s : Set โ„} +theorem integral_eq_of_hasDerivWithinAt_off_countable (f f' : โ„ โ†’ E) {a b : โ„} {s : Set โ„} (hs : s.Countable) (Hc : ContinuousOn f [[a, b]]) (Hd : โˆ€ x โˆˆ Ioo (min a b) (max a b) \ s, HasDerivAt f (f' x) x) (Hi : IntervalIntegrable f' volume a b) : โˆซ x in a..b, f' x = f b - f a := by @@ -425,7 +425,7 @@ theorem integral_eq_of_has_deriv_within_at_off_countable (f f' : โ„ โ†’ E) {a b ยท simp only [uIcc_of_ge hab, min_eq_right hab, max_eq_left hab] at * rw [intervalIntegral.integral_symm, neg_eq_iff_eq_neg, neg_sub] exact integral_eq_of_hasDerivWithinAt_off_countable_of_le f f' hab hs Hc Hd Hi.symm -#align measure_theory.integral_eq_of_has_deriv_within_at_off_countable MeasureTheory.integral_eq_of_has_deriv_within_at_off_countable +#align measure_theory.integral_eq_of_has_deriv_within_at_off_countable MeasureTheory.integral_eq_of_hasDerivWithinAt_off_countable /-- **Divergence theorem** for functions on the plane along rectangles. It is formulated in terms of two functions `f g : โ„ ร— โ„ โ†’ E` and an integral over `Icc a b = [a.1, b.1] ร— [a.2, b.2]`, where