From 7be0b061420738ad8eb3e73c6476b2c5353dd48d Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Fri, 3 Jan 2025 03:30:45 -0600 Subject: [PATCH] Fix --- Mathlib/Analysis/Analytic/IteratedFDeriv.lean | 12 +++--- Mathlib/Analysis/Calculus/ContDiff/Basic.lean | 26 ++++++------- .../Analysis/Calculus/ContDiff/Bounds.lean | 20 ++++------ Mathlib/Analysis/Calculus/ContDiff/Defs.lean | 37 ++++++++++--------- .../Calculus/ContDiff/FTaylorSeries.lean | 4 +- Mathlib/Analysis/Calculus/Deriv/Abs.lean | 4 +- Mathlib/Analysis/Calculus/Deriv/Add.lean | 3 +- Mathlib/Analysis/Calculus/Deriv/Basic.lean | 2 +- Mathlib/Analysis/Calculus/FDeriv/Add.lean | 6 +-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean | 2 +- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean | 4 +- .../Analysis/Calculus/FDeriv/Measurable.lean | 2 +- .../Calculus/FDeriv/RestrictScalars.lean | 3 +- .../Analysis/Calculus/FDeriv/Symmetric.lean | 6 +-- .../Analysis/Calculus/IteratedDeriv/Defs.lean | 4 +- .../Calculus/IteratedDeriv/Lemmas.lean | 14 +++---- Mathlib/Analysis/Calculus/MeanValue.lean | 4 +- Mathlib/Analysis/Calculus/Taylor.lean | 6 +-- Mathlib/Analysis/Calculus/VectorField.lean | 10 ++--- .../Manifold/SmoothManifoldWithCorners.lean | 7 ++-- .../Integral/FundThmCalculus.lean | 2 +- 21 files changed, 85 insertions(+), 93 deletions(-) diff --git a/Mathlib/Analysis/Analytic/IteratedFDeriv.lean b/Mathlib/Analysis/Analytic/IteratedFDeriv.lean index 69e172e6759ef..6f163354d8dcf 100644 --- a/Mathlib/Analysis/Analytic/IteratedFDeriv.lean +++ b/Mathlib/Analysis/Analytic/IteratedFDeriv.lean @@ -207,7 +207,7 @@ theorem HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum (h : HasFPowerSeriesOnBall f p x r) (h' : AnalyticOn π•œ f univ) {n : β„•} (v : Fin n β†’ E) : iteratedFDeriv π•œ n f x v = βˆ‘ Οƒ : Perm (Fin n), p n (fun i ↦ v (Οƒ i)) := by simp only [← iteratedFDerivWithin_univ, ← hasFPowerSeriesWithinOnBall_univ] at h ⊒ - exact h.iteratedFDerivWithin_eq_sum h' uniqueDiffOn_univ (mem_univ x) v + exact h.iteratedFDerivWithin_eq_sum h' .univ (mem_univ x) v /-- If a function has a power series in a ball, then its `n`-th iterated derivative is given by `(v₁, ..., vβ‚™) ↦ βˆ‘ pβ‚™ (v_{Οƒ (1)}, ..., v_{Οƒ (n)})` where the sum is over all @@ -224,7 +224,7 @@ theorem HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_completeSpace Β· exact h.mono inter_subset_left Β· apply h.analyticOn.mono rw [insert_eq_of_mem hx] - Β· exact hs.inter EMetric.isOpen_ball + Β· exact hs.inter_isOpen EMetric.isOpen_ball Β· exact ⟨hx, EMetric.mem_ball_self h.r_pos⟩ Β· exact inter_subset_right @@ -235,7 +235,7 @@ theorem HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum_of_completeSpace [CompleteSp (h : HasFPowerSeriesOnBall f p x r) {n : β„•} (v : Fin n β†’ E) : iteratedFDeriv π•œ n f x v = βˆ‘ Οƒ : Perm (Fin n), p n (fun i ↦ v (Οƒ i)) := by simp only [← iteratedFDerivWithin_univ, ← hasFPowerSeriesWithinOnBall_univ] at h ⊒ - exact h.iteratedFDerivWithin_eq_sum_of_completeSpace uniqueDiffOn_univ (mem_univ _) v + exact h.iteratedFDerivWithin_eq_sum_of_completeSpace .univ (mem_univ _) v /-- The `n`-th iterated derivative of an analytic function on a set is symmetric. -/ theorem AnalyticOn.iteratedFDerivWithin_comp_perm @@ -257,18 +257,18 @@ theorem ContDiffWithinAt.iteratedFDerivWithin_comp_perm have : iteratedFDerivWithin π•œ n f (s ∩ u) x = iteratedFDerivWithin π•œ n f s x := iteratedFDerivWithin_inter_open u_open xu rw [← this] - exact AnalyticOn.iteratedFDerivWithin_comp_perm hu.analyticOn (hs.inter u_open) ⟨hx, xu⟩ _ _ + exact hu.analyticOn.iteratedFDerivWithin_comp_perm (hs.inter_isOpen u_open) ⟨hx, xu⟩ _ _ /-- The `n`-th iterated derivative of an analytic function is symmetric. -/ theorem AnalyticOn.iteratedFDeriv_comp_perm (h : AnalyticOn π•œ f univ) {n : β„•} (v : Fin n β†’ E) (Οƒ : Perm (Fin n)) : iteratedFDeriv π•œ n f x (v ∘ Οƒ) = iteratedFDeriv π•œ n f x v := by rw [← iteratedFDerivWithin_univ] - exact h.iteratedFDerivWithin_comp_perm uniqueDiffOn_univ (mem_univ x) _ _ + exact h.iteratedFDerivWithin_comp_perm .univ (mem_univ x) _ _ /-- The `n`-th iterated derivative of an analytic function is symmetric. -/ theorem ContDiffAt.iteratedFDeriv_comp_perm (h : ContDiffAt π•œ Ο‰ f x) {n : β„•} (v : Fin n β†’ E) (Οƒ : Perm (Fin n)) : iteratedFDeriv π•œ n f x (v ∘ Οƒ) = iteratedFDeriv π•œ n f x v := by rw [← iteratedFDerivWithin_univ] - exact h.iteratedFDerivWithin_comp_perm uniqueDiffOn_univ (mem_univ x) _ _ + exact h.iteratedFDerivWithin_comp_perm .univ (mem_univ x) _ _ diff --git a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean index 87efceee82a5c..b17494d5088ef 100644 --- a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean +++ b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean @@ -222,7 +222,7 @@ theorem ContinuousLinearMap.iteratedFDeriv_comp_left {f : E β†’ F} (g : F β†’L[ (hf : ContDiff π•œ n f) (x : E) {i : β„•} (hi : i ≀ n) : iteratedFDeriv π•œ i (g ∘ f) x = g.compContinuousMultilinearMap (iteratedFDeriv π•œ i f x) := by simp only [← iteratedFDerivWithin_univ] - exact g.iteratedFDerivWithin_comp_left hf.contDiffOn uniqueDiffOn_univ (mem_univ x) hi + exact g.iteratedFDerivWithin_comp_left hf.contDiffOn .univ (mem_univ x) hi /-- The iterated derivative within a set of the composition with a linear equiv on the left is obtained by applying the linear equiv to the iterated derivative. This is true without @@ -266,7 +266,7 @@ theorem LinearIsometry.norm_iteratedFDeriv_comp_left {f : E β†’ F} (g : F β†’β‚— (hf : ContDiff π•œ n f) (x : E) {i : β„•} (hi : i ≀ n) : β€–iteratedFDeriv π•œ i (g ∘ f) xβ€– = β€–iteratedFDeriv π•œ i f xβ€– := by simp only [← iteratedFDerivWithin_univ] - exact g.norm_iteratedFDerivWithin_comp_left hf.contDiffOn uniqueDiffOn_univ (mem_univ x) hi + exact g.norm_iteratedFDerivWithin_comp_left hf.contDiffOn .univ (mem_univ x) hi /-- Composition with a linear isometry equiv on the left preserves the norm of the iterated derivative within a set. -/ @@ -285,7 +285,7 @@ derivative. -/ theorem LinearIsometryEquiv.norm_iteratedFDeriv_comp_left (g : F ≃ₗᡒ[π•œ] G) (f : E β†’ F) (x : E) (i : β„•) : β€–iteratedFDeriv π•œ i (g ∘ f) xβ€– = β€–iteratedFDeriv π•œ i f xβ€– := by rw [← iteratedFDerivWithin_univ, ← iteratedFDerivWithin_univ] - apply g.norm_iteratedFDerivWithin_comp_left f uniqueDiffOn_univ (mem_univ x) i + apply g.norm_iteratedFDerivWithin_comp_left f .univ (mem_univ x) i /-- Composition by continuous linear equivs on the left respects higher differentiability at a point in a domain. -/ @@ -412,7 +412,7 @@ theorem ContinuousLinearMap.iteratedFDeriv_comp_right (g : G β†’L[π•œ] E) {f : iteratedFDeriv π•œ i (f ∘ g) x = (iteratedFDeriv π•œ i f (g x)).compContinuousLinearMap fun _ => g := by simp only [← iteratedFDerivWithin_univ] - exact g.iteratedFDerivWithin_comp_right hf.contDiffOn uniqueDiffOn_univ uniqueDiffOn_univ + exact g.iteratedFDerivWithin_comp_right hf.contDiffOn .univ .univ (mem_univ _) hi /-- Composition with a linear isometry on the right preserves the norm of the iterated derivative @@ -430,7 +430,7 @@ within a set. -/ theorem LinearIsometryEquiv.norm_iteratedFDeriv_comp_right (g : G ≃ₗᡒ[π•œ] E) (f : E β†’ F) (x : G) (i : β„•) : β€–iteratedFDeriv π•œ i (f ∘ g) xβ€– = β€–iteratedFDeriv π•œ i f (g x)β€– := by simp only [← iteratedFDerivWithin_univ] - apply g.norm_iteratedFDerivWithin_comp_right f uniqueDiffOn_univ (mem_univ (g x)) i + apply g.norm_iteratedFDerivWithin_comp_right f .univ (mem_univ (g x)) i /-- Composition by continuous linear equivs on the right respects higher differentiability at a point in a domain. -/ @@ -950,7 +950,7 @@ theorem iteratedFDeriv_clm_apply_const_apply {i : β„•} (hi : i ≀ n) {x : E} {u : F} {m : Fin i β†’ E} : (iteratedFDeriv π•œ i (fun y ↦ (c y) u) x) m = (iteratedFDeriv π•œ i c x) m u := by simp only [← iteratedFDerivWithin_univ] - exact iteratedFDerivWithin_clm_apply_const_apply uniqueDiffOn_univ hc.contDiffOn hi (mem_univ _) + exact iteratedFDerivWithin_clm_apply_const_apply .univ hc.contDiffOn hi (mem_univ _) end ClmApplyConst @@ -1109,7 +1109,7 @@ protected theorem ContDiffAt.fderiv {f : E β†’ F β†’ G} {g : E β†’ F} (hf : ContDiffAt π•œ n (Function.uncurry f) (xβ‚€, g xβ‚€)) (hg : ContDiffAt π•œ m g xβ‚€) (hmn : m + 1 ≀ n) : ContDiffAt π•œ m (fun x => fderiv π•œ (f x) (g x)) xβ‚€ := by simp_rw [← fderivWithin_univ] - refine (ContDiffWithinAt.fderivWithin hf.contDiffWithinAt hg.contDiffWithinAt uniqueDiffOn_univ + refine (ContDiffWithinAt.fderivWithin hf.contDiffWithinAt hg.contDiffWithinAt .univ hmn (mem_univ xβ‚€) ?_).contDiffAt univ_mem rw [preimage_univ] @@ -1121,7 +1121,7 @@ theorem ContDiffAt.fderiv_right (hf : ContDiffAt π•œ n f xβ‚€) (hmn : m + 1 ≀ theorem ContDiffAt.iteratedFDeriv_right {i : β„•} (hf : ContDiffAt π•œ n f xβ‚€) (hmn : m + i ≀ n) : ContDiffAt π•œ m (iteratedFDeriv π•œ i f) xβ‚€ := by rw [← iteratedFDerivWithin_univ, ← contDiffWithinAt_univ] at * - exact hf.iteratedFderivWithin_right uniqueDiffOn_univ hmn trivial + exact hf.iteratedFderivWithin_right .univ hmn trivial /-- `x ↦ fderiv π•œ (f x) (g x)` is smooth. -/ protected theorem ContDiff.fderiv {f : E β†’ F β†’ G} {g : E β†’ F} @@ -1169,7 +1169,7 @@ theorem ContDiff.contDiff_fderiv_apply {f : E β†’ F} (hf : ContDiff π•œ n f) (h ContDiff π•œ m fun p : E Γ— E => (fderiv π•œ f p.1 : E β†’L[π•œ] F) p.2 := by rw [← contDiffOn_univ] at hf ⊒ rw [← fderivWithin_univ, ← univ_prod_univ] - exact contDiffOn_fderivWithin_apply hf uniqueDiffOn_univ hmn + exact contDiffOn_fderivWithin_apply hf .univ hmn /-! ### Smoothness of functions `f : E β†’ Ξ  i, F' i` @@ -1320,7 +1320,7 @@ theorem iteratedFDerivWithin_add_apply' {f g : E β†’ F} (hf : ContDiffOn π•œ i theorem iteratedFDeriv_add_apply {i : β„•} {f g : E β†’ F} (hf : ContDiff π•œ i f) (hg : ContDiff π•œ i g) : iteratedFDeriv π•œ i (f + g) x = iteratedFDeriv π•œ i f x + iteratedFDeriv π•œ i g x := by simp_rw [← contDiffOn_univ, ← iteratedFDerivWithin_univ] at hf hg ⊒ - exact iteratedFDerivWithin_add_apply hf hg uniqueDiffOn_univ (Set.mem_univ _) + exact iteratedFDerivWithin_add_apply hf hg .univ (Set.mem_univ _) theorem iteratedFDeriv_add_apply' {i : β„•} {f g : E β†’ F} (hf : ContDiff π•œ i f) (hg : ContDiff π•œ i g) : @@ -1377,7 +1377,7 @@ theorem iteratedFDerivWithin_neg_apply {f : E β†’ F} (hu : UniqueDiffOn π•œ s) theorem iteratedFDeriv_neg_apply {i : β„•} {f : E β†’ F} : iteratedFDeriv π•œ i (-f) x = -iteratedFDeriv π•œ i f x := by simp_rw [← iteratedFDerivWithin_univ] - exact iteratedFDerivWithin_neg_apply uniqueDiffOn_univ (Set.mem_univ _) + exact iteratedFDerivWithin_neg_apply .univ (Set.mem_univ _) end Neg @@ -1443,7 +1443,7 @@ theorem iteratedFDeriv_sum {ΞΉ : Type*} {f : ΞΉ β†’ E β†’ F} {u : Finset ΞΉ} {i (h : βˆ€ j ∈ u, ContDiff π•œ i (f j)) : iteratedFDeriv π•œ i (βˆ‘ j ∈ u, f j Β·) = βˆ‘ j ∈ u, iteratedFDeriv π•œ i (f j) := funext fun x ↦ by simpa [iteratedFDerivWithin_univ] using - iteratedFDerivWithin_sum_apply uniqueDiffOn_univ (mem_univ x) fun j hj ↦ (h j hj).contDiffOn + iteratedFDerivWithin_sum_apply .univ (mem_univ x) fun j hj ↦ (h j hj).contDiffOn /-! ### Product of two functions -/ @@ -1619,7 +1619,7 @@ theorem iteratedFDerivWithin_const_smul_apply (hf : ContDiffOn π•œ i f s) (hu : theorem iteratedFDeriv_const_smul_apply {x : E} (hf : ContDiff π•œ i f) : iteratedFDeriv π•œ i (a β€’ f) x = a β€’ iteratedFDeriv π•œ i f x := by simp_rw [← contDiffOn_univ, ← iteratedFDerivWithin_univ] at * - exact iteratedFDerivWithin_const_smul_apply hf uniqueDiffOn_univ (Set.mem_univ _) + exact iteratedFDerivWithin_const_smul_apply hf .univ (Set.mem_univ _) theorem iteratedFDeriv_const_smul_apply' {x : E} (hf : ContDiff π•œ i f) : iteratedFDeriv π•œ i (fun x ↦ a β€’ f x) x = a β€’ iteratedFDeriv π•œ i f x := diff --git a/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean b/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean index c869df9c43a51..faf266069468b 100644 --- a/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean +++ b/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean @@ -210,8 +210,7 @@ theorem ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear (B : E β†’L[π•œ] β€–iteratedFDeriv π•œ n (fun y => B (f y) (g y)) xβ€– ≀ β€–Bβ€– * βˆ‘ i ∈ Finset.range (n + 1), (n.choose i : ℝ) * β€–iteratedFDeriv π•œ i f xβ€– * β€–iteratedFDeriv π•œ (n - i) g xβ€– := by simp_rw [← iteratedFDerivWithin_univ] - exact B.norm_iteratedFDerivWithin_le_of_bilinear hf.contDiffOn hg.contDiffOn uniqueDiffOn_univ - (mem_univ x) hn + exact B.norm_iteratedFDerivWithin_le_of_bilinear hf.contDiffOn hg.contDiffOn .univ (mem_univ x) hn /-- Bounding the norm of the iterated derivative of `B (f x) (g x)` within a set in terms of the iterated derivatives of `f` and `g` when `B` is bilinear of norm at most `1`: @@ -236,7 +235,7 @@ theorem ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear_of_le_one (B : E (n.choose i : ℝ) * β€–iteratedFDeriv π•œ i f xβ€– * β€–iteratedFDeriv π•œ (n - i) g xβ€– := by simp_rw [← iteratedFDerivWithin_univ] exact B.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one hf.contDiffOn hg.contDiffOn - uniqueDiffOn_univ (mem_univ x) hn hB + .univ (mem_univ x) hn hB section @@ -282,7 +281,7 @@ theorem norm_iteratedFDeriv_mul_le {f : E β†’ A} {g : E β†’ A} {N : WithTop β„• (n.choose i : ℝ) * β€–iteratedFDeriv π•œ i f xβ€– * β€–iteratedFDeriv π•œ (n - i) g xβ€– := by simp_rw [← iteratedFDerivWithin_univ] exact norm_iteratedFDerivWithin_mul_le - hf.contDiffOn hg.contDiffOn uniqueDiffOn_univ (mem_univ x) hn + hf.contDiffOn hg.contDiffOn .univ (mem_univ x) hn -- TODO: Add `norm_iteratedFDeriv[Within]_list_prod_le` for non-commutative `NormedRing A`. @@ -337,8 +336,7 @@ theorem norm_iteratedFDeriv_prod_le [DecidableEq ΞΉ] [NormOneClass A'] {u : Fins βˆ‘ p ∈ u.sym n, (p : Multiset ΞΉ).multinomial * ∏ j ∈ u, β€–iteratedFDeriv π•œ ((p : Multiset ΞΉ).count j) (f j) xβ€– := by simpa [iteratedFDerivWithin_univ] using - norm_iteratedFDerivWithin_prod_le (fun i hi ↦ (hf i hi).contDiffOn) uniqueDiffOn_univ - (mem_univ x) hn + norm_iteratedFDerivWithin_prod_le (fun i hi ↦ (hf i hi).contDiffOn) .univ (mem_univ x) hn end @@ -518,8 +516,8 @@ theorem norm_iteratedFDeriv_comp_le {g : F β†’ G} {f : E β†’ F} {n : β„•} {N : W (hD : βˆ€ i, 1 ≀ i β†’ i ≀ n β†’ β€–iteratedFDeriv π•œ i f xβ€– ≀ D ^ i) : β€–iteratedFDeriv π•œ n (g ∘ f) xβ€– ≀ n ! * C * D ^ n := by simp_rw [← iteratedFDerivWithin_univ] at hC hD ⊒ - exact norm_iteratedFDerivWithin_comp_le hg.contDiffOn hf.contDiffOn hn uniqueDiffOn_univ - uniqueDiffOn_univ (mapsTo_univ _ _) (mem_univ x) hC hD + exact norm_iteratedFDerivWithin_comp_le hg.contDiffOn hf.contDiffOn hn .univ .univ + (mapsTo_univ _ _) (mem_univ x) hC hD section Apply @@ -542,8 +540,7 @@ theorem norm_iteratedFDeriv_clm_apply {f : E β†’ F β†’L[π•œ] G} {g : E β†’ F} { β€–iteratedFDeriv π•œ n (fun y : E => (f y) (g y)) xβ€– ≀ βˆ‘ i ∈ Finset.range (n + 1), ↑(n.choose i) * β€–iteratedFDeriv π•œ i f xβ€– * β€–iteratedFDeriv π•œ (n - i) g xβ€– := by simp only [← iteratedFDerivWithin_univ] - exact norm_iteratedFDerivWithin_clm_apply hf.contDiffOn hg.contDiffOn uniqueDiffOn_univ - (Set.mem_univ x) hn + exact norm_iteratedFDerivWithin_clm_apply hf.contDiffOn hg.contDiffOn .univ (Set.mem_univ x) hn theorem norm_iteratedFDerivWithin_clm_apply_const {f : E β†’ F β†’L[π•œ] G} {c : F} {s : Set E} {x : E} {N : WithTop β„•βˆž} {n : β„•} (hf : ContDiffOn π•œ N f s) (hs : UniqueDiffOn π•œ s) @@ -562,7 +559,6 @@ theorem norm_iteratedFDeriv_clm_apply_const {f : E β†’ F β†’L[π•œ] G} {c : F} { {N : WithTop β„•βˆž} {n : β„•} (hf : ContDiff π•œ N f) (hn : n ≀ N) : β€–iteratedFDeriv π•œ n (fun y : E => (f y) c) xβ€– ≀ β€–cβ€– * β€–iteratedFDeriv π•œ n f xβ€– := by simp only [← iteratedFDerivWithin_univ] - exact norm_iteratedFDerivWithin_clm_apply_const hf.contDiffOn uniqueDiffOn_univ - (Set.mem_univ x) hn + exact norm_iteratedFDerivWithin_clm_apply_const hf.contDiffOn .univ (Set.mem_univ x) hn end Apply diff --git a/Mathlib/Analysis/Calculus/ContDiff/Defs.lean b/Mathlib/Analysis/Calculus/ContDiff/Defs.lean index eabcdff56fab9..c045a9cc98e26 100644 --- a/Mathlib/Analysis/Calculus/ContDiff/Defs.lean +++ b/Mathlib/Analysis/Calculus/ContDiff/Defs.lean @@ -661,15 +661,15 @@ protected theorem ContDiffOn.ftaylorSeriesWithin have : p x m.succ = ftaylorSeriesWithin π•œ f s x m.succ := by change p x m.succ = iteratedFDerivWithin π•œ m.succ f s x rw [← iteratedFDerivWithin_inter_open o_open xo] - exact (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl (hs.inter o_open) ⟨hx, xo⟩ + exact (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl + (hs.inter_isOpen o_open) ⟨hx, xo⟩ rw [← this, ← hasFDerivWithinAt_inter (IsOpen.mem_nhds o_open xo)] have A : βˆ€ y ∈ s ∩ o, p y m = ftaylorSeriesWithin π•œ f s y m := by rintro y ⟨hy, yo⟩ change p y m = iteratedFDerivWithin π•œ m f s y rw [← iteratedFDerivWithin_inter_open o_open yo] - exact - (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn (mod_cast Nat.le_succ m) - (hs.inter o_open) ⟨hy, yo⟩ + exact (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn (mod_cast Nat.le_succ m) + (hs.inter_isOpen o_open) ⟨hy, yo⟩ exact ((Hp.mono ho).fderivWithin m (mod_cast lt_add_one m) x ⟨hx, xo⟩).congr (fun y hy => (A y hy).symm) (A x ⟨hx, xo⟩).symm @@ -685,7 +685,8 @@ protected theorem ContDiffOn.ftaylorSeriesWithin rintro y ⟨hy, yo⟩ change p y m = iteratedFDerivWithin π•œ m f s y rw [← iteratedFDerivWithin_inter_open o_open yo] - exact (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl (hs.inter o_open) ⟨hy, yo⟩ + exact (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl + (hs.inter_isOpen o_open) ⟨hy, yo⟩ exact ((Hp.mono ho).cont m le_rfl).congr fun y hy => (A y hy).symm theorem iteratedFDerivWithin_subset {n : β„•} (st : s βŠ† t) (hs : UniqueDiffOn π•œ s) @@ -797,7 +798,7 @@ theorem ContDiffWithinAt.differentiableWithinAt_iteratedFDerivWithin {m : β„•} have B : iteratedFDerivWithin π•œ m f s =αΆ [𝓝 x] iteratedFDerivWithin π•œ m f t := iteratedFDerivWithin_eventually_congr_set' _ A.symm _ have C : DifferentiableWithinAt π•œ (iteratedFDerivWithin π•œ m f t) t x := - hu.differentiableOn_iteratedFDerivWithin (Nat.cast_lt.2 m.lt_succ_self) (hs.inter uo) x + hu.differentiableOn_iteratedFDerivWithin (Nat.cast_lt.2 m.lt_succ_self) (hs.inter_isOpen uo) x ⟨mem_insert _ _, xu⟩ rw [differentiableWithinAt_congr_set' _ A] at C exact C.congr_of_eventuallyEq (B.filter_mono inf_le_left) B.self_of_nhds @@ -861,7 +862,7 @@ theorem contDiffOn_succ_iff_fderivWithin (hs : UniqueDiffOn π•œ s) : rw [inter_comm] at this refine Filter.eventuallyEq_of_mem this fun y hy => ?_ have A : fderivWithin π•œ f (s ∩ o) y = f' y := - ((hff' y (ho hy)).mono ho).fderivWithin (hs.inter o_open y hy) + ((hff' y (ho hy)).mono ho).fderivWithin (hs.inter_isOpen o_open y hy) rwa [fderivWithin_inter (o_open.mem_nhds hy.2)] at A match n with | Ο‰ => exact (H.analyticOn.fderivWithin hs).contDiffOn hs (n := Ο‰) x hx @@ -1028,8 +1029,8 @@ theorem iteratedFDerivWithin_eq_iteratedFDeriv {n : β„•} ← iteratedFDerivWithin_inter_open u_open xu (s := univ)] apply iteratedFDerivWithin_subset Β· exact inter_subset_inter_left _ (subset_univ _) - Β· exact hs.inter u_open - Β· apply uniqueDiffOn_univ.inter u_open + Β· exact hs.inter_isOpen u_open + Β· exact .inter_isOpen .univ u_open Β· simpa using hu Β· exact ⟨hx, xu⟩ @@ -1058,9 +1059,9 @@ theorem contDiffOn_univ : ContDiffOn π•œ n f univ ↔ ContDiff π•œ n f := by Β· intro H use ftaylorSeriesWithin π•œ f univ rw [← hasFTaylorSeriesUpToOn_univ_iff] - refine ⟨H.ftaylorSeriesWithin uniqueDiffOn_univ, fun i ↦ ?_⟩ + refine ⟨H.ftaylorSeriesWithin .univ, fun i ↦ ?_⟩ rw [← analyticOn_univ] - exact H.analyticOn.iteratedFDerivWithin uniqueDiffOn_univ _ + exact H.analyticOn.iteratedFDerivWithin .univ _ Β· rintro ⟨p, hp, h'p⟩ x _ exact ⟨univ, Filter.univ_sets _, p, (hp.hasFTaylorSeriesUpToOn univ).of_le le_top, fun i ↦ (h'p i).analyticOn⟩ @@ -1069,7 +1070,7 @@ theorem contDiffOn_univ : ContDiffOn π•œ n f univ ↔ ContDiff π•œ n f := by Β· intro H use ftaylorSeriesWithin π•œ f univ rw [← hasFTaylorSeriesUpToOn_univ_iff] - exact H.ftaylorSeriesWithin uniqueDiffOn_univ + exact H.ftaylorSeriesWithin .univ Β· rintro ⟨p, hp⟩ x _ m hm exact ⟨univ, Filter.univ_sets _, p, (hp.hasFTaylorSeriesUpToOn univ).of_le (mod_cast hm)⟩ @@ -1136,7 +1137,7 @@ theorem contDiff_succ_iff_hasFDerivAt {n : β„•} : ContDiff π•œ (n + 1) f ↔ βˆƒ f' : E β†’ E β†’L[π•œ] F, ContDiff π•œ n f' ∧ βˆ€ x, HasFDerivAt f (f' x) x := by simp only [← contDiffOn_univ, ← hasFDerivWithinAt_univ, Set.mem_univ, forall_true_left, - contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn uniqueDiffOn_univ, + contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn .univ, WithTop.natCast_ne_top, analyticOn_univ, false_implies, true_and] theorem contDiff_one_iff_hasFDerivAt : ContDiff π•œ 1 f ↔ @@ -1145,7 +1146,7 @@ theorem contDiff_one_iff_hasFDerivAt : ContDiff π•œ 1 f ↔ theorem AnalyticOn.contDiff (hf : AnalyticOn π•œ f univ) : ContDiff π•œ n f := by rw [← contDiffOn_univ] - exact hf.contDiffOn (n := n) uniqueDiffOn_univ + exact hf.contDiffOn (n := n) .univ theorem AnalyticOnNhd.contDiff (hf : AnalyticOnNhd π•œ f univ) : ContDiff π•œ n f := hf.analyticOn.contDiff @@ -1168,7 +1169,7 @@ theorem ContDiff.ftaylorSeries (hf : ContDiff π•œ n f) : HasFTaylorSeriesUpTo n f (ftaylorSeries π•œ f) := by simp only [← contDiffOn_univ, ← hasFTaylorSeriesUpToOn_univ_iff, ← ftaylorSeriesWithin_univ] at hf ⊒ - exact ContDiffOn.ftaylorSeriesWithin hf uniqueDiffOn_univ + exact ContDiffOn.ftaylorSeriesWithin hf .univ /-- For `n : β„•βˆž`, a function is `C^n` iff it admits `ftaylorSeries π•œ f` as a Taylor series up to order `n`. -/ @@ -1176,7 +1177,7 @@ theorem contDiff_iff_ftaylorSeries {n : β„•βˆž} : ContDiff π•œ n f ↔ HasFTaylorSeriesUpTo n f (ftaylorSeries π•œ f) := by constructor Β· rw [← contDiffOn_univ, ← hasFTaylorSeriesUpToOn_univ_iff, ← ftaylorSeriesWithin_univ] - exact fun h ↦ ContDiffOn.ftaylorSeriesWithin h uniqueDiffOn_univ + exact fun h ↦ ContDiffOn.ftaylorSeriesWithin h .univ Β· exact fun h ↦ ⟨ftaylorSeries π•œ f, h⟩ theorem contDiff_iff_continuous_differentiable {n : β„•βˆž} : @@ -1184,7 +1185,7 @@ theorem contDiff_iff_continuous_differentiable {n : β„•βˆž} : (βˆ€ m : β„•, m ≀ n β†’ Continuous fun x => iteratedFDeriv π•œ m f x) ∧ βˆ€ m : β„•, m < n β†’ Differentiable π•œ fun x => iteratedFDeriv π•œ m f x := by simp [contDiffOn_univ.symm, continuous_iff_continuousOn_univ, differentiableOn_univ.symm, - iteratedFDerivWithin_univ, contDiffOn_iff_continuousOn_differentiableOn uniqueDiffOn_univ] + iteratedFDerivWithin_univ, contDiffOn_iff_continuousOn_differentiableOn .univ] theorem contDiff_nat_iff_continuous_differentiable {n : β„•} : ContDiff π•œ n f ↔ @@ -1215,7 +1216,7 @@ theorem contDiff_succ_iff_fderiv : ContDiff π•œ (n + 1) f ↔ Differentiable π•œ f ∧ (n = Ο‰ β†’ AnalyticOnNhd π•œ f univ) ∧ ContDiff π•œ n (fderiv π•œ f) := by simp only [← contDiffOn_univ, ← differentiableOn_univ, ← fderivWithin_univ, - contDiffOn_succ_iff_fderivWithin uniqueDiffOn_univ, analyticOn_univ] + contDiffOn_succ_iff_fderivWithin .univ, analyticOn_univ] theorem contDiff_one_iff_fderiv : ContDiff π•œ 1 f ↔ Differentiable π•œ f ∧ Continuous (fderiv π•œ f) := by diff --git a/Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean b/Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean index 400df9cb52915..586cc643c812a 100644 --- a/Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean +++ b/Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean @@ -865,7 +865,7 @@ theorem HasFTaylorSeriesUpTo.eq_iteratedFDeriv p x m = iteratedFDeriv π•œ m f x := by rw [← iteratedFDerivWithin_univ] rw [← hasFTaylorSeriesUpToOn_univ_iff] at h - exact h.eq_iteratedFDerivWithin_of_uniqueDiffOn hmn uniqueDiffOn_univ (mem_univ _) + exact h.eq_iteratedFDerivWithin_of_uniqueDiffOn hmn .univ (mem_univ _) /-- In an open set, the iterated derivative within this set coincides with the global iterated derivative. -/ @@ -895,7 +895,7 @@ theorem iteratedFDeriv_succ_apply_right {n : β„•} (m : Fin (n + 1) β†’ E) : (iteratedFDeriv π•œ (n + 1) f x : (Fin (n + 1) β†’ E) β†’ F) m = iteratedFDeriv π•œ n (fun y => fderiv π•œ f y) x (init m) (m (last n)) := by rw [← iteratedFDerivWithin_univ, ← iteratedFDerivWithin_univ, ← fderivWithin_univ] - exact iteratedFDerivWithin_succ_apply_right uniqueDiffOn_univ (mem_univ _) _ + exact iteratedFDerivWithin_succ_apply_right .univ (mem_univ _) _ /-- Writing explicitly the `n+1`-th derivative as the composition of a currying linear equiv, and the `n`-th derivative of the derivative. -/ diff --git a/Mathlib/Analysis/Calculus/Deriv/Abs.lean b/Mathlib/Analysis/Calculus/Deriv/Abs.lean index a5f01ae326dcf..96576bff5ca1d 100644 --- a/Mathlib/Analysis/Calculus/Deriv/Abs.lean +++ b/Mathlib/Analysis/Calculus/Deriv/Abs.lean @@ -180,10 +180,10 @@ theorem Differentiable.abs (hf : Differentiable ℝ f) (hβ‚€ : βˆ€ x, f x β‰  0) theorem not_differentiableAt_abs_zero : Β¬ DifferentiableAt ℝ (abs : ℝ β†’ ℝ) 0 := by intro h have h₁ : deriv abs (0 : ℝ) = 1 := - (uniqueDiffOn_Ici _ _ Set.left_mem_Ici).eq_deriv _ h.hasDerivAt.hasDerivWithinAt <| + (UniqueDiffOn.Ici _ _ Set.left_mem_Ici).eq_deriv _ h.hasDerivAt.hasDerivWithinAt <| (hasDerivWithinAt_id _ _).congr_of_mem (fun _ h ↦ abs_of_nonneg h) Set.left_mem_Ici have hβ‚‚ : deriv abs (0 : ℝ) = -1 := - (uniqueDiffOn_Iic _ _ Set.right_mem_Iic).eq_deriv _ h.hasDerivAt.hasDerivWithinAt <| + (UniqueDiffOn.Iic _ _ Set.right_mem_Iic).eq_deriv _ h.hasDerivAt.hasDerivWithinAt <| (hasDerivWithinAt_neg _ _).congr_of_mem (fun _ h ↦ abs_of_nonpos h) Set.right_mem_Iic linarith diff --git a/Mathlib/Analysis/Calculus/Deriv/Add.lean b/Mathlib/Analysis/Calculus/Deriv/Add.lean index 3d6b994ca666b..6865a91830b00 100644 --- a/Mathlib/Analysis/Calculus/Deriv/Add.lean +++ b/Mathlib/Analysis/Calculus/Deriv/Add.lean @@ -326,8 +326,7 @@ theorem derivWithin_const_sub (hxs : UniqueDiffWithinAt π•œ s x) (c : F) : simp [derivWithin, fderivWithin_const_sub hxs] theorem deriv_const_sub (c : F) : deriv (fun y => c - f y) x = -deriv f x := by - simp only [← derivWithin_univ, - derivWithin_const_sub (uniqueDiffWithinAt_univ : UniqueDiffWithinAt π•œ _ _)] + simpa only [← derivWithin_univ] using derivWithin_const_sub .univ c lemma differentiableAt_comp_sub_const {a b : π•œ} : DifferentiableAt π•œ (fun x ↦ f (x - b)) a ↔ DifferentiableAt π•œ f (a - b) := by diff --git a/Mathlib/Analysis/Calculus/Deriv/Basic.lean b/Mathlib/Analysis/Calculus/Deriv/Basic.lean index d0e6db0c4bcf9..8bdf0efae1efa 100644 --- a/Mathlib/Analysis/Calculus/Deriv/Basic.lean +++ b/Mathlib/Analysis/Calculus/Deriv/Basic.lean @@ -504,7 +504,7 @@ theorem derivWithin_Ioi_eq_Ici {E : Type*} [NormedAddCommGroup E] [NormedSpace by_cases H : DifferentiableWithinAt ℝ f (Ioi x) x Β· have A := H.hasDerivWithinAt.Ici_of_Ioi have B := (differentiableWithinAt_Ioi_iff_Ici.1 H).hasDerivWithinAt - simpa using (uniqueDiffOn_Ici x).eq left_mem_Ici A B + simpa using (UniqueDiffOn.Ici x).eq left_mem_Ici A B Β· rw [derivWithin_zero_of_not_differentiableWithinAt H, derivWithin_zero_of_not_differentiableWithinAt] rwa [differentiableWithinAt_Ioi_iff_Ici] at H diff --git a/Mathlib/Analysis/Calculus/FDeriv/Add.lean b/Mathlib/Analysis/Calculus/FDeriv/Add.lean index 2677296a22c2e..bec999b74ca8d 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Add.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Add.lean @@ -236,7 +236,7 @@ theorem fderivWithin_add_const (hxs : UniqueDiffWithinAt π•œ s x) (c : F) : simpa theorem fderiv_add_const (c : F) : fderiv π•œ (fun y => f y + c) x = fderiv π•œ f x := by - simp only [← fderivWithin_univ, fderivWithin_add_const uniqueDiffWithinAt_univ] + simp only [← fderivWithin_univ, fderivWithin_add_const .univ] @[fun_prop] theorem HasStrictFDerivAt.const_add (hf : HasStrictFDerivAt f f' x) (c : F) : @@ -438,7 +438,7 @@ theorem fderivWithin_neg' (hxs : UniqueDiffWithinAt π•œ s x) : @[simp] theorem fderiv_neg : fderiv π•œ (fun y => -f y) x = -fderiv π•œ f x := by - simp only [← fderivWithin_univ, fderivWithin_neg uniqueDiffWithinAt_univ] + simp only [← fderivWithin_univ, fderivWithin_neg .univ] /-- Version of `fderiv_neg` where the function is written `-f` instead of `fun y ↦ - f y`. -/ theorem fderiv_neg' : fderiv π•œ (-f) x = -fderiv π•œ f x := @@ -707,7 +707,7 @@ theorem fderivWithin_const_sub (hxs : UniqueDiffWithinAt π•œ s x) (c : F) : simp only [sub_eq_add_neg, fderivWithin_const_add, fderivWithin_neg, hxs] theorem fderiv_const_sub (c : F) : fderiv π•œ (fun y => c - f y) x = -fderiv π•œ f x := by - simp only [← fderivWithin_univ, fderivWithin_const_sub uniqueDiffWithinAt_univ] + simp only [← fderivWithin_univ, fderivWithin_const_sub .univ] end Sub diff --git a/Mathlib/Analysis/Calculus/FDeriv/Basic.lean b/Mathlib/Analysis/Calculus/FDeriv/Basic.lean index c22d0f09c8255..18dc95d8a271e 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Basic.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Basic.lean @@ -456,7 +456,7 @@ theorem HasFDerivAt.lim (hf : HasFDerivAt f f' x) (v : E) {Ξ± : Type*} {c : Ξ± theorem HasFDerivAt.unique (hβ‚€ : HasFDerivAt f fβ‚€' x) (h₁ : HasFDerivAt f f₁' x) : fβ‚€' = f₁' := by rw [← hasFDerivWithinAt_univ] at hβ‚€ h₁ - exact uniqueDiffWithinAt_univ.eq hβ‚€ h₁ + exact UniqueDiffWithinAt.univ.eq hβ‚€ h₁ theorem hasFDerivWithinAt_inter' (h : t ∈ 𝓝[s] x) : HasFDerivWithinAt f f' (s ∩ t) x ↔ HasFDerivWithinAt f f' s x := by diff --git a/Mathlib/Analysis/Calculus/FDeriv/Equiv.lean b/Mathlib/Analysis/Calculus/FDeriv/Equiv.lean index b859dc97ba096..a0f9d6cf4a613 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Equiv.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Equiv.lean @@ -137,7 +137,7 @@ theorem comp_fderivWithin {f : G β†’ E} {s : Set G} {x : G} (hxs : UniqueDiffWit theorem comp_fderiv {f : G β†’ E} {x : G} : fderiv π•œ (iso ∘ f) x = (iso : E β†’L[π•œ] F).comp (fderiv π•œ f x) := by rw [← fderivWithin_univ, ← fderivWithin_univ] - exact iso.comp_fderivWithin uniqueDiffWithinAt_univ + exact iso.comp_fderivWithin .univ lemma _root_.fderivWithin_continuousLinearEquiv_comp (L : G ≃L[π•œ] G') (f : E β†’ (F β†’L[π•œ] G)) (hs : UniqueDiffWithinAt π•œ s x) : @@ -228,7 +228,7 @@ theorem comp_right_fderivWithin {f : F β†’ G} {s : Set F} {x : E} theorem comp_right_fderiv {f : F β†’ G} {x : E} : fderiv π•œ (f ∘ iso) x = (fderiv π•œ f (iso x)).comp (iso : E β†’L[π•œ] F) := by rw [← fderivWithin_univ, ← fderivWithin_univ, ← iso.comp_right_fderivWithin, preimage_univ] - exact uniqueDiffWithinAt_univ + exact .univ end ContinuousLinearEquiv diff --git a/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean b/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean index 120f173913015..05f24faf04d7d 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean @@ -671,7 +671,7 @@ theorem D_subset_differentiable_set {K : Set F} (hK : IsComplete K) : _ ≀ 16 * β€–y - xβ€– * (Ξ΅ / 16) := by gcongr _ = Ξ΅ * β€–y - xβ€– := by ring - rw [← this.derivWithin (uniqueDiffOn_Ici x x Set.left_mem_Ici)] at f'K + rw [← this.derivWithin (UniqueDiffOn.Ici x x Set.left_mem_Ici)] at f'K exact ⟨this.differentiableWithinAt, f'K⟩ theorem differentiable_set_eq_D (hK : IsComplete K) : diff --git a/Mathlib/Analysis/Calculus/FDeriv/RestrictScalars.lean b/Mathlib/Analysis/Calculus/FDeriv/RestrictScalars.lean index cac15836bc67a..d70e2a428cc5c 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/RestrictScalars.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/RestrictScalars.lean @@ -103,7 +103,6 @@ theorem differentiableWithinAt_iff_restrictScalars (hf : DifferentiableWithinAt theorem differentiableAt_iff_restrictScalars (hf : DifferentiableAt π•œ f x) : DifferentiableAt π•œ' f x ↔ βˆƒ g' : E β†’L[π•œ'] F, g'.restrictScalars π•œ = fderiv π•œ f x := by rw [← differentiableWithinAt_univ, ← fderivWithin_univ] - exact - differentiableWithinAt_iff_restrictScalars π•œ hf.differentiableWithinAt uniqueDiffWithinAt_univ + exact differentiableWithinAt_iff_restrictScalars π•œ hf.differentiableWithinAt .univ end RestrictScalars diff --git a/Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean b/Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean index b518f82c09cb7..3ff9fcf8b7dd5 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean @@ -153,7 +153,7 @@ theorem IsSymmSndFDerivAt.isSymmSndFDerivWithinAt (h : IsSymmSndFDerivAt π•œ f (hf : ContDiffAt π•œ 2 f x) (hs : UniqueDiffOn π•œ s) (hx : x ∈ s) : IsSymmSndFDerivWithinAt π•œ f s x := by simp only [← isSymmSndFDerivWithinAt_univ, ← contDiffWithinAt_univ] at h hf - exact h.mono_of_mem_nhdsWithin univ_mem hf hs uniqueDiffOn_univ hx + exact h.mono_of_mem_nhdsWithin univ_mem hf hs .univ hx /-- If a function is analytic within a set at a point, then its second derivative is symmetric. -/ theorem ContDiffWithinAt.isSymmSndFDerivWithinAt_of_omega (hf : ContDiffWithinAt π•œ Ο‰ f s x) @@ -170,7 +170,7 @@ theorem ContDiffWithinAt.isSymmSndFDerivWithinAt_of_omega (hf : ContDiffWithinAt theorem ContDiffAt.isSymmSndFDerivAt_of_omega (hf : ContDiffAt π•œ Ο‰ f x) : IsSymmSndFDerivAt π•œ f x := by simp only [← isSymmSndFDerivWithinAt_univ, ← contDiffWithinAt_univ] at hf ⊒ - exact hf.isSymmSndFDerivWithinAt_of_omega uniqueDiffOn_univ (mem_univ _) + exact hf.isSymmSndFDerivWithinAt_of_omega .univ (mem_univ _) end General @@ -537,7 +537,7 @@ theorem ContDiffWithinAt.isSymmSndFDerivWithinAt {n : WithTop β„•βˆž} obtain ⟨m, hm, hmn, m_ne⟩ := exist_minSmoothness_le_ne_infty hn rcases (hf.of_le hmn).contDiffOn' le_rfl (by simp [m_ne]) with ⟨u, u_open, xu, hu⟩ simp only [insert_eq_of_mem h'x] at hu - have h'u : UniqueDiffOn π•œ (s ∩ u) := hs.inter u_open + have h'u : UniqueDiffOn π•œ (s ∩ u) := hs.inter_isOpen u_open obtain ⟨y, hy, y_lim⟩ : βˆƒ y, (βˆ€ (n : β„•), y n ∈ interior s) ∧ Tendsto y atTop (𝓝 x) := mem_closure_iff_seq_limit.1 hx have L : βˆ€αΆ  k in atTop, y k ∈ u := y_lim (u_open.mem_nhds xu) diff --git a/Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean b/Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean index a013a881fc12f..51f29e6610632 100644 --- a/Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean +++ b/Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean @@ -270,14 +270,14 @@ iterated derivative. -/ theorem iteratedDeriv_succ : iteratedDeriv (n + 1) f = deriv (iteratedDeriv n f) := by ext x rw [← iteratedDerivWithin_univ, ← iteratedDerivWithin_univ, ← derivWithin_univ] - exact iteratedDerivWithin_succ uniqueDiffWithinAt_univ + exact iteratedDerivWithin_succ .univ /-- The `n`-th iterated derivative can be obtained by iterating `n` times the differentiation operation. -/ theorem iteratedDeriv_eq_iterate : iteratedDeriv n f = deriv^[n] f := by ext x rw [← iteratedDerivWithin_univ] - convert iteratedDerivWithin_eq_iterate uniqueDiffOn_univ (F := F) (mem_univ x) + convert iteratedDerivWithin_eq_iterate .univ (F := F) (mem_univ x) simp [derivWithin_univ] /-- The `n+1`-th iterated derivative can be obtained by taking the `n`-th derivative of the diff --git a/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean b/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean index c10db8c308277..cf9fd3575ba49 100644 --- a/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean +++ b/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean @@ -123,35 +123,33 @@ end lemma iteratedDeriv_add (hf : ContDiff π•œ n f) (hg : ContDiff π•œ n g) : iteratedDeriv n (f + g) x = iteratedDeriv n f x + iteratedDeriv n g x := by simpa only [iteratedDerivWithin_univ] using - iteratedDerivWithin_add (Set.mem_univ _) uniqueDiffOn_univ - (contDiffOn_univ.mpr hf) (contDiffOn_univ.mpr hg) + iteratedDerivWithin_add (Set.mem_univ _) .univ hf.contDiffOn hg.contDiffOn theorem iteratedDeriv_const_add (hn : 0 < n) (c : F) : iteratedDeriv n (fun z => c + f z) x = iteratedDeriv n f x := by simpa only [iteratedDerivWithin_univ] using - iteratedDerivWithin_const_add (Set.mem_univ _) uniqueDiffOn_univ hn c + iteratedDerivWithin_const_add (Set.mem_univ _) .univ hn c theorem iteratedDeriv_const_sub (hn : 0 < n) (c : F) : iteratedDeriv n (fun z => c - f z) x = iteratedDeriv n (-f) x := by simpa only [iteratedDerivWithin_univ] using - iteratedDerivWithin_const_sub (Set.mem_univ _) uniqueDiffOn_univ hn c + iteratedDerivWithin_const_sub (Set.mem_univ _) .univ hn c lemma iteratedDeriv_neg (n : β„•) (f : π•œ β†’ F) (a : π•œ) : iteratedDeriv n (fun x ↦ -(f x)) a = -(iteratedDeriv n f a) := by simpa only [iteratedDerivWithin_univ] using - iteratedDerivWithin_neg (Set.mem_univ a) uniqueDiffOn_univ f + iteratedDerivWithin_neg (Set.mem_univ a) .univ f lemma iteratedDeriv_sub (hf : ContDiff π•œ n f) (hg : ContDiff π•œ n g) : iteratedDeriv n (f - g) x = iteratedDeriv n f x - iteratedDeriv n g x := by simpa only [iteratedDerivWithin_univ] using - iteratedDerivWithin_sub (Set.mem_univ _) uniqueDiffOn_univ - (contDiffOn_univ.mpr hf) (contDiffOn_univ.mpr hg) + iteratedDerivWithin_sub (Set.mem_univ _) .univ hf.contDiffOn hg.contDiffOn theorem iteratedDeriv_comp_const_smul {n : β„•} {f : π•œ β†’ F} (h : ContDiff π•œ n f) (c : π•œ) : iteratedDeriv n (fun x => f (c * x)) = fun x => c ^ n β€’ iteratedDeriv n f (c * x) := by funext x simpa only [iteratedDerivWithin_univ] using - iteratedDerivWithin_comp_const_smul (Set.mem_univ x) uniqueDiffOn_univ (contDiffOn_univ.mpr h) + iteratedDerivWithin_comp_const_smul (Set.mem_univ x) .univ (contDiffOn_univ.mpr h) c (Set.mapsTo_univ _ _) @[deprecated (since := "2024-12-20")] diff --git a/Mathlib/Analysis/Calculus/MeanValue.lean b/Mathlib/Analysis/Calculus/MeanValue.lean index 8194a4e3aa8f5..2104c665e01f9 100644 --- a/Mathlib/Analysis/Calculus/MeanValue.lean +++ b/Mathlib/Analysis/Calculus/MeanValue.lean @@ -603,8 +603,8 @@ theorem _root_.eq_of_fderiv_eq letI : RCLike π•œ := IsRCLikeNormedField.rclike π•œ let A : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ π•œ E suffices Set.univ.EqOn f g from funext fun x => this <| mem_univ x - exact convex_univ.eqOn_of_fderivWithin_eq hf.differentiableOn hg.differentiableOn - uniqueDiffOn_univ (fun x _ => by simpa using hf' _) (mem_univ _) hfgx + exact convex_univ.eqOn_of_fderivWithin_eq hf.differentiableOn hg.differentiableOn .univ + (fun x _ => by simpa using hf' _) (mem_univ _) hfgx end Convex diff --git a/Mathlib/Analysis/Calculus/Taylor.lean b/Mathlib/Analysis/Calculus/Taylor.lean index 7d6b563e1c66a..7288644378e31 100644 --- a/Mathlib/Analysis/Calculus/Taylor.lean +++ b/Mathlib/Analysis/Calculus/Taylor.lean @@ -195,7 +195,7 @@ theorem taylorWithinEval_hasDerivAt_Ioo {f : ℝ β†’ E} {a b t : ℝ} (x : ℝ) (((n ! : ℝ)⁻¹ * (x - t) ^ n) β€’ iteratedDerivWithin (n + 1) f (Icc a b) t) t := have h_nhds : Ioo a b ∈ 𝓝 t := isOpen_Ioo.mem_nhds ht have h_nhds' : Ioo a b ∈ 𝓝[Icc a b] t := nhdsWithin_le_nhds h_nhds - (hasDerivWithinAt_taylorWithinEval (uniqueDiffWithinAt_Ioo ht) (uniqueDiffOn_Icc hx) h_nhds' ht + (hasDerivWithinAt_taylorWithinEval (.Ioo ht) (.Icc hx) h_nhds' ht Ioo_subset_Icc_self hf <| (hf' t ht).mono_of_mem_nhdsWithin h_nhds').hasDerivAt h_nhds /-- Calculate the derivative of the Taylor polynomial with respect to `xβ‚€`. @@ -206,7 +206,7 @@ theorem hasDerivWithinAt_taylorWithinEval_at_Icc {f : ℝ β†’ E} {a b t : ℝ} ( (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) + hasDerivWithinAt_taylorWithinEval (UniqueDiffOn.Icc hx t ht) (UniqueDiffOn.Icc hx) self_mem_nhdsWithin ht rfl.subset hf (hf' t ht) /-! ### Taylor's theorem with mean value type remainder estimate -/ @@ -230,7 +230,7 @@ theorem taylor_mean_remainder {f : ℝ β†’ ℝ} {g g' : ℝ β†’ ℝ} {x xβ‚€ : -- We apply the mean value theorem rcases exists_ratio_hasDerivAt_eq_ratio_slope (fun t => taylorWithinEval f n (Icc xβ‚€ x) t x) (fun t => ((n ! : ℝ)⁻¹ * (x - t) ^ n) β€’ iteratedDerivWithin (n + 1) f (Icc xβ‚€ x) t) hx - (continuousOn_taylorWithinEval (uniqueDiffOn_Icc hx) hf) + (continuousOn_taylorWithinEval (.Icc hx) hf) (fun _ hy => taylorWithinEval_hasDerivAt_Ioo x hx hy hf hf') g g' gcont gdiff with ⟨y, hy, h⟩ use y, hy -- The rest is simplifications and trivial calculations diff --git a/Mathlib/Analysis/Calculus/VectorField.lean b/Mathlib/Analysis/Calculus/VectorField.lean index fca2dcf3812bd..cb2cf311e056f 100644 --- a/Mathlib/Analysis/Calculus/VectorField.lean +++ b/Mathlib/Analysis/Calculus/VectorField.lean @@ -105,7 +105,7 @@ lemma lieBracketWithin_smul_right {c : π•œ} (hW : DifferentiableWithinAt π•œ W lemma lieBracket_smul_right {c : π•œ} (hW : DifferentiableAt π•œ W x) : lieBracket π•œ V (c β€’ W) x = c β€’ lieBracket π•œ V W x := by simp only [← differentiableWithinAt_univ, ← lieBracketWithin_univ] at hW ⊒ - exact lieBracketWithin_smul_right hW uniqueDiffWithinAt_univ + exact lieBracketWithin_smul_right hW .univ lemma lieBracketWithin_add_left (hV : DifferentiableWithinAt π•œ V s x) (hV₁ : DifferentiableWithinAt π•œ V₁ s x) (hs : UniqueDiffWithinAt π•œ s x) : @@ -164,7 +164,7 @@ lemma _root_.ContDiffAt.lieBracket_vectorField {m n : WithTop β„•βˆž} (hV : Cont ContDiffAt π•œ m (lieBracket π•œ V W) x := by rw [← contDiffWithinAt_univ] at hV hW ⊒ simp_rw [← lieBracketWithin_univ] - exact hV.lieBracketWithin_vectorField hW uniqueDiffOn_univ hmn (mem_univ _) + exact hV.lieBracketWithin_vectorField hW .univ hmn (mem_univ _) lemma _root_.ContDiffOn.lieBracketWithin_vectorField {m n : WithTop β„•βˆž} (hV : ContDiffOn π•œ n V s) (hW : ContDiffOn π•œ n W s) (hs : UniqueDiffOn π•œ s) (hmn : m + 1 ≀ n) : @@ -347,7 +347,7 @@ lemma leibniz_identity_lieBracket (hn : minSmoothness π•œ 2 ≀ n) {U V W : E lieBracket π•œ U (lieBracket π•œ V W) x = lieBracket π•œ (lieBracket π•œ U V) W x + lieBracket π•œ V (lieBracket π•œ U W) x := by simp only [← lieBracketWithin_univ, ← contDiffWithinAt_univ] at hU hV hW ⊒ - exact leibniz_identity_lieBracketWithin hn uniqueDiffOn_univ (by simp) (mem_univ _) hU hV hW + exact leibniz_identity_lieBracketWithin hn .univ (by simp) (mem_univ _) hU hV hW /-! @@ -492,7 +492,7 @@ lemma _root_.exists_continuousLinearEquiv_fderiv_symm_eq ∧ βˆ€ v, fderiv π•œ (fun y ↦ ((N y).symm : F β†’L[π•œ] E)) x v = - (N x).symm ∘L ((fderiv π•œ (fderiv π•œ f) x v)) ∘L (N x).symm := by simp only [← fderivWithin_univ, ← contDiffWithinAt_univ, ← nhdsWithin_univ] at hf h'f ⊒ - exact exists_continuousLinearEquiv_fderivWithin_symm_eq h'f hf uniqueDiffOn_univ (mem_univ _) + exact exists_continuousLinearEquiv_fderivWithin_symm_eq h'f hf .univ (mem_univ _) /-- The Lie bracket commutes with taking pullbacks. This requires the function to have symmetric second derivative. Version in a complete space. One could also give a version avoiding @@ -568,7 +568,7 @@ lemma pullback_lieBracket_of_isSymmSndFDerivAt {f : E β†’ F} {V W : F β†’ F} {x pullback π•œ f (lieBracket π•œ V W) x = lieBracket π•œ (pullback π•œ f V) (pullback π•œ f W) x := by simp only [← lieBracketWithin_univ, ← pullbackWithin_univ, ← isSymmSndFDerivWithinAt_univ, ← differentiableWithinAt_univ] at hf h'f hV hW ⊒ - exact pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt hf h'f hV hW uniqueDiffOn_univ + exact pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt hf h'f hV hW .univ (mem_univ _) (mapsTo_univ _ _) /-- The Lie bracket commutes with taking pullbacks. This requires the function to have symmetric diff --git a/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean b/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean index d3b381f0c0511..f35c7452bcf9b 100644 --- a/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean +++ b/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean @@ -168,7 +168,7 @@ def modelWithCornersSelf (π•œ : Type*) [NontriviallyNormedField π•œ] (E : Type [NormedAddCommGroup E] [NormedSpace π•œ E] : ModelWithCorners π•œ E E where toPartialEquiv := PartialEquiv.refl E source_eq := rfl - uniqueDiffOn' := uniqueDiffOn_univ + uniqueDiffOn' := .univ target_subset_closure_interior := by simp continuous_toFun := continuous_id continuous_invFun := continuous_id @@ -324,9 +324,8 @@ theorem symm_map_nhdsWithin_range (x : H) : map I.symm (𝓝[range I] I x) = rw [← I.map_nhds_eq, map_map, I.symm_comp_self, map_id] theorem uniqueDiffOn_preimage {s : Set H} (hs : IsOpen s) : - UniqueDiffOn π•œ (I.symm ⁻¹' s ∩ range I) := by - rw [inter_comm] - exact I.uniqueDiffOn.inter (hs.preimage I.continuous_invFun) + UniqueDiffOn π•œ (I.symm ⁻¹' s ∩ range I) := + (hs.preimage I.continuous_invFun).inter_uniqueDiffOn I.uniqueDiffOn @[deprecated (since := "2024-09-30")] alias unique_diff_preimage := uniqueDiffOn_preimage diff --git a/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean b/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean index 7dbef7d066822..98349ee832e5c 100644 --- a/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean +++ b/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean @@ -1211,7 +1211,7 @@ theorem integrableOn_deriv_right_of_nonneg (hcont : ContinuousOn g (Icc a b)) have meas_g' : AEMeasurable g' (volume.restrict (Ioo a b)) := by apply (aemeasurable_derivWithin_Ioi g _).congr refine (ae_restrict_mem measurableSet_Ioo).mono fun x hx => ?_ - exact (hderiv x hx).derivWithin (uniqueDiffWithinAt_Ioi _) + exact (hderiv x hx).derivWithin (.Ioi _) suffices H : (∫⁻ x in Ioo a b, β€–g' xβ€–β‚Š) ≀ ENNReal.ofReal (g b - g a) from ⟨meas_g'.aestronglyMeasurable, H.trans_lt ENNReal.ofReal_lt_top⟩ by_contra! H