𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
⊢ ContDiffOn 𝕜 n f s
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
⊢ ContDiffOn 𝕜 n f s
let t := { x | AnalyticAt 𝕜 f x }
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
this : ContDiffOn 𝕜 n f t
⊢ ContDiffOn 𝕜 n f s

case this
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
⊢ ContDiffOn 𝕜 n f t
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
⊢ ContDiffOn 𝕜 n f s
suffices : ContDiffOn 𝕜 n f t
case this
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
⊢ ContDiffOn 𝕜 n f t
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
this : ContDiffOn 𝕜 n f t
⊢ ContDiffOn 𝕜 n f s

case this
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
⊢ ContDiffOn 𝕜 n f t
exact this.mono h
case this
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
H : AnalyticOn 𝕜 f t
⊢ ContDiffOn 𝕜 n f t
case this
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
⊢ ContDiffOn 𝕜 n f t
have H : AnalyticOn 𝕜 f t := fun x hx => hx
case this
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
H : AnalyticOn 𝕜 f t
t_open : IsOpen t
⊢ ContDiffOn 𝕜 n f t
case this
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
H : AnalyticOn 𝕜 f t
⊢ ContDiffOn 𝕜 n f t
have t_open : IsOpen t := isOpen_analyticAt 𝕜 f
case this.Hcont
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
H : AnalyticOn 𝕜 f t
t_open : IsOpen t
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f t x) t

case this.Hdiff
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
H : AnalyticOn 𝕜 f t
t_open : IsOpen t
⊢ ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f t x) t
case this
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
H : AnalyticOn 𝕜 f t
t_open : IsOpen t
⊢ ContDiffOn 𝕜 n f t
apply contDiffOn_of_continuousOn_differentiableOn
case this.Hcont
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
H : AnalyticOn 𝕜 f t
t_open : IsOpen t
m : ℕ
⊢ ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f t x) t
case this.Hcont
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
H : AnalyticOn 𝕜 f t
t_open : IsOpen t
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f t x) t
rintro m -
case this.Hcont
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
H : AnalyticOn 𝕜 f t
t_open : IsOpen t
m : ℕ
⊢ Set.EqOn (fun x => iteratedFDerivWithin 𝕜 m f t x) (_root_.iteratedFDeriv 𝕜 m f) t
case this.Hcont
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
H : AnalyticOn 𝕜 f t
t_open : IsOpen t
m : ℕ
⊢ ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f t x) t
apply (H.iteratedFDeriv m).continuousOn.congr
case this.Hcont
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x✝ : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
H : AnalyticOn 𝕜 f t
t_open : IsOpen t
m : ℕ
x : E
hx : x ∈ t
⊢ (fun x => iteratedFDerivWithin 𝕜 m f t x) x = _root_.iteratedFDeriv 𝕜 m f x
case this.Hcont
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
H : AnalyticOn 𝕜 f t
t_open : IsOpen t
m : ℕ
⊢ Set.EqOn (fun x => iteratedFDerivWithin 𝕜 m f t x) (_root_.iteratedFDeriv 𝕜 m f) t
intro x hx
no goals
case this.Hcont
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x✝ : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
H : AnalyticOn 𝕜 f t
t_open : IsOpen t
m : ℕ
x : E
hx : x ∈ t
⊢ (fun x => iteratedFDerivWithin 𝕜 m f t x) x = _root_.iteratedFDeriv 𝕜 m f x
exact iteratedFDerivWithin_of_isOpen _ t_open hx
case this.Hdiff
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
H : AnalyticOn 𝕜 f t
t_open : IsOpen t
m : ℕ
⊢ DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f t x) t
case this.Hdiff
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
H : AnalyticOn 𝕜 f t
t_open : IsOpen t
⊢ ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f t x) t
rintro m -
case this.Hdiff
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
H : AnalyticOn 𝕜 f t
t_open : IsOpen t
m : ℕ
⊢ ∀ (x : E), x ∈ t → iteratedFDerivWithin 𝕜 m f t x = _root_.iteratedFDeriv 𝕜 m f x
case this.Hdiff
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
H : AnalyticOn 𝕜 f t
t_open : IsOpen t
m : ℕ
⊢ DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f t x) t
apply (H.iteratedFDeriv m).differentiableOn.congr
case this.Hdiff
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x✝ : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
H : AnalyticOn 𝕜 f t
t_open : IsOpen t
m : ℕ
x : E
hx : x ∈ t
⊢ iteratedFDerivWithin 𝕜 m f t x = _root_.iteratedFDeriv 𝕜 m f x
case this.Hdiff
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
H : AnalyticOn 𝕜 f t
t_open : IsOpen t
m : ℕ
⊢ ∀ (x : E), x ∈ t → iteratedFDerivWithin 𝕜 m f t x = _root_.iteratedFDeriv 𝕜 m f x
intro x hx
no goals
case this.Hdiff
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x✝ : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ∞
t : Set E := {x | AnalyticAt 𝕜 f x}
H : AnalyticOn 𝕜 f t
t_open : IsOpen t
m : ℕ
x : E
hx : x ∈ t
⊢ iteratedFDerivWithin 𝕜 m f t x = _root_.iteratedFDeriv 𝕜 m f x
exact iteratedFDerivWithin_of_isOpen _ t_open hx