Skip to content

Commit 5ac3430

Browse files
kim-emkim-em
committed
chore: split Mathlib.Analysis.Calculus.ContDiff.Basic (#8344)
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
1 parent 1cb42bf commit 5ac3430

File tree

11 files changed

+799
-725
lines changed

11 files changed

+799
-725
lines changed

‎Mathlib.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -567,7 +567,10 @@ import Mathlib.Analysis.Calculus.BumpFunction.Normed
567567
import Mathlib.Analysis.Calculus.Conformal.InnerProduct
568568
import Mathlib.Analysis.Calculus.Conformal.NormedSpace
569569
import Mathlib.Analysis.Calculus.ContDiff.Basic
570+
import Mathlib.Analysis.Calculus.ContDiff.Bounds
570571
import Mathlib.Analysis.Calculus.ContDiff.Defs
572+
import Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
573+
import Mathlib.Analysis.Calculus.ContDiff.IsROrC
571574
import Mathlib.Analysis.Calculus.Darboux
572575
import Mathlib.Analysis.Calculus.Deriv.Add
573576
import Mathlib.Analysis.Calculus.Deriv.AffineMap

‎Mathlib/Analysis/Calculus/ContDiff/Basic.lean‎

Lines changed: 0 additions & 721 deletions
Large diffs are not rendered by default.

‎Mathlib/Analysis/Calculus/ContDiff/Bounds.lean‎

Lines changed: 550 additions & 0 deletions
Large diffs are not rendered by default.

‎Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean‎

Lines changed: 78 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,78 @@
1+
/-
2+
Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Sébastien Gouëzel, Floris van Doorn
5+
-/
6+
import Mathlib.Analysis.Calculus.ContDiff.Basic
7+
import Mathlib.Analysis.NormedSpace.FiniteDimension
8+
9+
10+
#align_import analysis.calculus.cont_diff from "leanprover-community/mathlib"@"3bce8d800a6f2b8f63fe1e588fd76a9ff4adcebe"
11+
12+
/-!
13+
# Higher differentiability in finite dimensions.
14+
15+
-/
16+
17+
18+
noncomputable section
19+
20+
universe uD uE uF uG
21+
22+
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {D : Type uD} [NormedAddCommGroup D]
23+
[NormedSpace 𝕜 D] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF}
24+
[NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
25+
26+
/-! ### Finite dimensional results -/
27+
28+
section FiniteDimensional
29+
30+
open Function FiniteDimensional
31+
32+
variable [CompleteSpace 𝕜]
33+
34+
/-- A family of continuous linear maps is `C^n` on `s` if all its applications are. -/
35+
theorem contDiffOn_clm_apply {n : ℕ∞} {f : E → F →L[𝕜] G} {s : Set E} [FiniteDimensional 𝕜 F] :
36+
ContDiffOn 𝕜 n f s ↔ ∀ y, ContDiffOn 𝕜 n (fun x => f x y) s := by
37+
refine' ⟨fun h y => h.clm_apply contDiffOn_const, fun h => _⟩
38+
let d := finrank 𝕜 F
39+
have hd : d = finrank 𝕜 (Fin d → 𝕜) := (finrank_fin_fun 𝕜).symm
40+
let e₁ := ContinuousLinearEquiv.ofFinrankEq hd
41+
let e₂ := (e₁.arrowCongr (1 : G ≃L[𝕜] G)).trans (ContinuousLinearEquiv.piRing (Fin d))
42+
rw [← comp.left_id f, ← e₂.symm_comp_self]
43+
exact e₂.symm.contDiff.comp_contDiffOn (contDiffOn_pi.mpr fun i => h _)
44+
#align cont_diff_on_clm_apply contDiffOn_clm_apply
45+
46+
theorem contDiff_clm_apply_iff {n : ℕ∞} {f : E → F →L[𝕜] G} [FiniteDimensional 𝕜 F] :
47+
ContDiff 𝕜 n f ↔ ∀ y, ContDiff 𝕜 n fun x => f x y := by
48+
simp_rw [← contDiffOn_univ, contDiffOn_clm_apply]
49+
#align cont_diff_clm_apply_iff contDiff_clm_apply_iff
50+
51+
/-- This is a useful lemma to prove that a certain operation preserves functions being `C^n`.
52+
When you do induction on `n`, this gives a useful characterization of a function being `C^(n+1)`,
53+
assuming you have already computed the derivative. The advantage of this version over
54+
`contDiff_succ_iff_fderiv` is that both occurrences of `ContDiff` are for functions with the same
55+
domain and codomain (`E` and `F`). This is not the case for `contDiff_succ_iff_fderiv`, which
56+
often requires an inconvenient need to generalize `F`, which results in universe issues
57+
(see the discussion in the section of `ContDiff.comp`).
58+
59+
This lemma avoids these universe issues, but only applies for finite dimensional `E`. -/
60+
theorem contDiff_succ_iff_fderiv_apply [FiniteDimensional 𝕜 E] {n : ℕ} {f : E → F} :
61+
ContDiff 𝕜 (n + 1 : ℕ) f ↔ Differentiable 𝕜 f ∧ ∀ y, ContDiff 𝕜 n fun x => fderiv 𝕜 f x y := by
62+
rw [contDiff_succ_iff_fderiv, contDiff_clm_apply_iff]
63+
#align cont_diff_succ_iff_fderiv_apply contDiff_succ_iff_fderiv_apply
64+
65+
theorem contDiffOn_succ_of_fderiv_apply [FiniteDimensional 𝕜 E] {n : ℕ} {f : E → F} {s : Set E}
66+
(hf : DifferentiableOn 𝕜 f s) (h : ∀ y, ContDiffOn 𝕜 n (fun x => fderivWithin 𝕜 f s x y) s) :
67+
ContDiffOn 𝕜 (n + 1 : ℕ) f s :=
68+
contDiffOn_succ_of_fderivWithin hf <| contDiffOn_clm_apply.mpr h
69+
#align cont_diff_on_succ_of_fderiv_apply contDiffOn_succ_of_fderiv_apply
70+
71+
theorem contDiffOn_succ_iff_fderiv_apply [FiniteDimensional 𝕜 E] {n : ℕ} {f : E → F} {s : Set E}
72+
(hs : UniqueDiffOn 𝕜 s) :
73+
ContDiffOn 𝕜 (n + 1 : ℕ) f s ↔
74+
DifferentiableOn 𝕜 f s ∧ ∀ y, ContDiffOn 𝕜 n (fun x => fderivWithin 𝕜 f s x y) s :=
75+
by rw [contDiffOn_succ_iff_fderivWithin hs, contDiffOn_clm_apply]
76+
#align cont_diff_on_succ_iff_fderiv_apply contDiffOn_succ_iff_fderiv_apply
77+
78+
end FiniteDimensional

‎Mathlib/Analysis/Calculus/ContDiff/IsROrC.lean‎

Lines changed: 159 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,159 @@
1+
/-
2+
Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Sébastien Gouëzel, Floris van Doorn
5+
-/
6+
import Mathlib.Analysis.Calculus.ContDiff.Basic
7+
import Mathlib.Analysis.Calculus.MeanValue
8+
9+
#align_import analysis.calculus.cont_diff from "leanprover-community/mathlib"@"3bce8d800a6f2b8f63fe1e588fd76a9ff4adcebe"
10+
11+
/-!
12+
# Higher differentiability over `ℝ` or `ℂ`
13+
-/
14+
15+
noncomputable section
16+
17+
open Set Fin Filter Function
18+
19+
open scoped NNReal Topology
20+
21+
section Real
22+
23+
/-!
24+
### Results over `ℝ` or `ℂ`
25+
The results in this section rely on the Mean Value Theorem, and therefore hold only over `ℝ` (and
26+
its extension fields such as `ℂ`).
27+
-/
28+
29+
variable {n : ℕ∞} {𝕂 : Type*} [IsROrC 𝕂] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕂 E']
30+
{F' : Type*} [NormedAddCommGroup F'] [NormedSpace 𝕂 F']
31+
32+
/-- If a function has a Taylor series at order at least 1, then at points in the interior of the
33+
domain of definition, the term of order 1 of this series is a strict derivative of `f`. -/
34+
theorem HasFTaylorSeriesUpToOn.hasStrictFDerivAt {s : Set E'} {f : E' → F'} {x : E'}
35+
{p : E' → FormalMultilinearSeries 𝕂 E' F'} (hf : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n)
36+
(hs : s ∈ 𝓝 x) : HasStrictFDerivAt f ((continuousMultilinearCurryFin1 𝕂 E' F') (p x 1)) x :=
37+
hasStrictFDerivAt_of_hasFDerivAt_of_continuousAt (hf.eventually_hasFDerivAt hn hs) <|
38+
(continuousMultilinearCurryFin1 𝕂 E' F').continuousAt.comp <| (hf.cont 1 hn).continuousAt hs
39+
#align has_ftaylor_series_up_to_on.has_strict_fderiv_at HasFTaylorSeriesUpToOn.hasStrictFDerivAt
40+
41+
/-- If a function is `C^n` with `1 ≤ n` around a point, and its derivative at that point is given to
42+
us as `f'`, then `f'` is also a strict derivative. -/
43+
theorem ContDiffAt.hasStrictFDerivAt' {f : E' → F'} {f' : E' →L[𝕂] F'} {x : E'}
44+
(hf : ContDiffAt 𝕂 n f x) (hf' : HasFDerivAt f f' x) (hn : 1 ≤ n) :
45+
HasStrictFDerivAt f f' x := by
46+
rcases hf 1 hn with ⟨u, H, p, hp⟩
47+
simp only [nhdsWithin_univ, mem_univ, insert_eq_of_mem] at H
48+
have := hp.hasStrictFDerivAt le_rfl H
49+
rwa [hf'.unique this.hasFDerivAt]
50+
#align cont_diff_at.has_strict_fderiv_at' ContDiffAt.hasStrictFDerivAt'
51+
52+
/-- If a function is `C^n` with `1 ≤ n` around a point, and its derivative at that point is given to
53+
us as `f'`, then `f'` is also a strict derivative. -/
54+
theorem ContDiffAt.hasStrictDerivAt' {f : 𝕂 → F'} {f' : F'} {x : 𝕂} (hf : ContDiffAt 𝕂 n f x)
55+
(hf' : HasDerivAt f f' x) (hn : 1 ≤ n) : HasStrictDerivAt f f' x :=
56+
hf.hasStrictFDerivAt' hf' hn
57+
#align cont_diff_at.has_strict_deriv_at' ContDiffAt.hasStrictDerivAt'
58+
59+
/-- If a function is `C^n` with `1 ≤ n` around a point, then the derivative of `f` at this point
60+
is also a strict derivative. -/
61+
theorem ContDiffAt.hasStrictFDerivAt {f : E' → F'} {x : E'} (hf : ContDiffAt 𝕂 n f x) (hn : 1 ≤ n) :
62+
HasStrictFDerivAt f (fderiv 𝕂 f x) x :=
63+
hf.hasStrictFDerivAt' (hf.differentiableAt hn).hasFDerivAt hn
64+
#align cont_diff_at.has_strict_fderiv_at ContDiffAt.hasStrictFDerivAt
65+
66+
/-- If a function is `C^n` with `1 ≤ n` around a point, then the derivative of `f` at this point
67+
is also a strict derivative. -/
68+
theorem ContDiffAt.hasStrictDerivAt {f : 𝕂 → F'} {x : 𝕂} (hf : ContDiffAt 𝕂 n f x) (hn : 1 ≤ n) :
69+
HasStrictDerivAt f (deriv f x) x :=
70+
(hf.hasStrictFDerivAt hn).hasStrictDerivAt
71+
#align cont_diff_at.has_strict_deriv_at ContDiffAt.hasStrictDerivAt
72+
73+
/-- If a function is `C^n` with `1 ≤ n`, then the derivative of `f` is also a strict derivative. -/
74+
theorem ContDiff.hasStrictFDerivAt {f : E' → F'} {x : E'} (hf : ContDiff 𝕂 n f) (hn : 1 ≤ n) :
75+
HasStrictFDerivAt f (fderiv 𝕂 f x) x :=
76+
hf.contDiffAt.hasStrictFDerivAt hn
77+
#align cont_diff.has_strict_fderiv_at ContDiff.hasStrictFDerivAt
78+
79+
/-- If a function is `C^n` with `1 ≤ n`, then the derivative of `f` is also a strict derivative. -/
80+
theorem ContDiff.hasStrictDerivAt {f : 𝕂 → F'} {x : 𝕂} (hf : ContDiff 𝕂 n f) (hn : 1 ≤ n) :
81+
HasStrictDerivAt f (deriv f x) x :=
82+
hf.contDiffAt.hasStrictDerivAt hn
83+
#align cont_diff.has_strict_deriv_at ContDiff.hasStrictDerivAt
84+
85+
/-- If `f` has a formal Taylor series `p` up to order `1` on `{x} ∪ s`, where `s` is a convex set,
86+
and `‖p x 1‖₊ < K`, then `f` is `K`-Lipschitz in a neighborhood of `x` within `s`. -/
87+
theorem HasFTaylorSeriesUpToOn.exists_lipschitzOnWith_of_nnnorm_lt {E F : Type*}
88+
[NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F}
89+
{p : E → FormalMultilinearSeries ℝ E F} {s : Set E} {x : E}
90+
(hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)) (hs : Convex ℝ s) (K : ℝ≥0)
91+
(hK : ‖p x 1‖₊ < K) : ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t := by
92+
set f' := fun y => continuousMultilinearCurryFin1 ℝ E F (p y 1)
93+
have hder : ∀ y ∈ s, HasFDerivWithinAt f (f' y) s y := fun y hy =>
94+
(hf.hasFDerivWithinAt le_rfl (subset_insert x s hy)).mono (subset_insert x s)
95+
have hcont : ContinuousWithinAt f' s x :=
96+
(continuousMultilinearCurryFin1 ℝ E F).continuousAt.comp_continuousWithinAt
97+
((hf.cont _ le_rfl _ (mem_insert _ _)).mono (subset_insert x s))
98+
replace hK : ‖f' x‖₊ < K; · simpa only [LinearIsometryEquiv.nnnorm_map]
99+
exact
100+
hs.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt
101+
(eventually_nhdsWithin_iff.2 <| eventually_of_forall hder) hcont K hK
102+
#align has_ftaylor_series_up_to_on.exists_lipschitz_on_with_of_nnnorm_lt HasFTaylorSeriesUpToOn.exists_lipschitzOnWith_of_nnnorm_lt
103+
104+
/-- If `f` has a formal Taylor series `p` up to order `1` on `{x} ∪ s`, where `s` is a convex set,
105+
then `f` is Lipschitz in a neighborhood of `x` within `s`. -/
106+
theorem HasFTaylorSeriesUpToOn.exists_lipschitzOnWith {E F : Type*} [NormedAddCommGroup E]
107+
[NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F}
108+
{p : E → FormalMultilinearSeries ℝ E F} {s : Set E} {x : E}
109+
(hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)) (hs : Convex ℝ s) :
110+
∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t :=
111+
(exists_gt _).imp <| hf.exists_lipschitzOnWith_of_nnnorm_lt hs
112+
#align has_ftaylor_series_up_to_on.exists_lipschitz_on_with HasFTaylorSeriesUpToOn.exists_lipschitzOnWith
113+
114+
/-- If `f` is `C^1` within a convex set `s` at `x`, then it is Lipschitz on a neighborhood of `x`
115+
within `s`. -/
116+
theorem ContDiffWithinAt.exists_lipschitzOnWith {E F : Type*} [NormedAddCommGroup E]
117+
[NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {s : Set E} {x : E}
118+
(hf : ContDiffWithinAt ℝ 1 f s x) (hs : Convex ℝ s) :
119+
∃ K : ℝ≥0, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t := by
120+
rcases hf 1 le_rfl with ⟨t, hst, p, hp⟩
121+
rcases Metric.mem_nhdsWithin_iff.mp hst with ⟨ε, ε0, hε⟩
122+
replace hp : HasFTaylorSeriesUpToOn 1 f p (Metric.ball x ε ∩ insert x s) := hp.mono hε
123+
clear hst hε t
124+
rw [← insert_eq_of_mem (Metric.mem_ball_self ε0), ← insert_inter_distrib] at hp
125+
rcases hp.exists_lipschitzOnWith ((convex_ball _ _).inter hs) with ⟨K, t, hst, hft⟩
126+
rw [inter_comm, ← nhdsWithin_restrict' _ (Metric.ball_mem_nhds _ ε0)] at hst
127+
exact ⟨K, t, hst, hft⟩
128+
#align cont_diff_within_at.exists_lipschitz_on_with ContDiffWithinAt.exists_lipschitzOnWith
129+
130+
/-- If `f` is `C^1` at `x` and `K > ‖fderiv 𝕂 f x‖`, then `f` is `K`-Lipschitz in a neighborhood of
131+
`x`. -/
132+
theorem ContDiffAt.exists_lipschitzOnWith_of_nnnorm_lt {f : E' → F'} {x : E'}
133+
(hf : ContDiffAt 𝕂 1 f x) (K : ℝ≥0) (hK : ‖fderiv 𝕂 f x‖₊ < K) :
134+
∃ t ∈ 𝓝 x, LipschitzOnWith K f t :=
135+
(hf.hasStrictFDerivAt le_rfl).exists_lipschitzOnWith_of_nnnorm_lt K hK
136+
#align cont_diff_at.exists_lipschitz_on_with_of_nnnorm_lt ContDiffAt.exists_lipschitzOnWith_of_nnnorm_lt
137+
138+
/-- If `f` is `C^1` at `x`, then `f` is Lipschitz in a neighborhood of `x`. -/
139+
theorem ContDiffAt.exists_lipschitzOnWith {f : E' → F'} {x : E'} (hf : ContDiffAt 𝕂 1 f x) :
140+
∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K f t :=
141+
(hf.hasStrictFDerivAt le_rfl).exists_lipschitzOnWith
142+
#align cont_diff_at.exists_lipschitz_on_with ContDiffAt.exists_lipschitzOnWith
143+
144+
/-- If `f` is `C^1`, it is locally Lipschitz. -/
145+
lemma ContDiff.locallyLipschitz {f : E' → F'} (hf : ContDiff 𝕂 1 f) : LocallyLipschitz f := by
146+
intro x
147+
rcases hf.contDiffAt.exists_lipschitzOnWith with ⟨K, t, ht, hf⟩
148+
use K, t
149+
150+
/-- A `C^1` function with compact support is Lipschitz. -/
151+
theorem ContDiff.lipschitzWith_of_hasCompactSupport {f : E' → F'} {n : ℕ∞}
152+
(hf : HasCompactSupport f) (h'f : ContDiff 𝕂 n f) (hn : 1 ≤ n) :
153+
∃ C, LipschitzWith C f := by
154+
obtain ⟨C, hC⟩ := (hf.fderiv 𝕂).exists_bound_of_continuous (h'f.continuous_fderiv hn)
155+
refine ⟨⟨max C 0, le_max_right _ _⟩, ?_⟩
156+
apply lipschitzWith_of_nnnorm_fderiv_le (h'f.differentiable hn) (fun x ↦ ?_)
157+
simp [← NNReal.coe_le_coe, hC x]
158+
159+
end Real

‎Mathlib/Analysis/Calculus/Inverse.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,8 @@ Copyright (c) 2020 Yury Kudryashov. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yury Kudryashov, Heather Macbeth, Sébastien Gouëzel
55
-/
6-
import Mathlib.Analysis.Calculus.ContDiff.Basic
6+
import Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
7+
import Mathlib.Analysis.Calculus.ContDiff.IsROrC
78
import Mathlib.Analysis.NormedSpace.Banach
89

910
#align_import analysis.calculus.inverse from "leanprover-community/mathlib"@"2c1d8ca2812b64f88992a5294ea3dba144755cd1"

‎Mathlib/Analysis/Calculus/Series.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Sébastien Gouëzel
55
-/
66
import Mathlib.Analysis.Calculus.UniformLimitsDeriv
7-
import Mathlib.Analysis.Calculus.ContDiff.Basic
7+
import Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
88
import Mathlib.Data.Nat.Cast.WithTop
99

1010
#align_import analysis.calculus.series from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982"

‎Mathlib/Analysis/Distribution/SchwartzSpace.lean‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,9 @@ Copyright (c) 2022 Moritz Doll. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Moritz Doll
55
-/
6-
import Mathlib.Analysis.Calculus.ContDiff.Basic
6+
import Mathlib.Analysis.Calculus.Deriv.Add
7+
import Mathlib.Analysis.Calculus.Deriv.Mul
8+
import Mathlib.Analysis.Calculus.ContDiff.Bounds
79
import Mathlib.Analysis.Calculus.IteratedDeriv
810
import Mathlib.Analysis.LocallyConvex.WithSeminorms
911
import Mathlib.Topology.Algebra.UniformFilterBasis

‎Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne
55
-/
66
import Mathlib.Analysis.Complex.RealDeriv
7+
import Mathlib.Analysis.Calculus.ContDiff.IsROrC
78

89
#align_import analysis.special_functions.exp_deriv from "leanprover-community/mathlib"@"6a5c85000ab93fe5dcfdf620676f614ba8e18c26"
910

‎Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Authors: Sébastien Gouëzel
66
import Mathlib.Analysis.Analytic.Basic
77
import Mathlib.Analysis.Analytic.Composition
88
import Mathlib.Analysis.Analytic.Linear
9-
import Mathlib.Analysis.Calculus.ContDiff.Basic
9+
import Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
1010
import Mathlib.Analysis.Calculus.FDeriv.Analytic
1111
import Mathlib.Geometry.Manifold.ChartedSpace
1212

0 commit comments

Comments
 (0)