[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
h : HasFPowerSeriesAt f p x
⊢ HasStrictFDerivAt f (↑(continuousMultilinearCurryFin1 𝕜 E F) (p 1)) x
[PROOFSTEP]
refine' h.isBigO_image_sub_norm_mul_norm_sub.trans_isLittleO (IsLittleO.of_norm_right _)
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
h : HasFPowerSeriesAt f p x
⊢ (fun y => ‖y - (x, x)‖ * ‖y.fst - y.snd‖) =o[nhds (x, x)] fun x => ‖x.fst - x.snd‖
[PROOFSTEP]
refine' isLittleO_iff_exists_eq_mul.2 ⟨fun y => ‖y - (x, x)‖, _, EventuallyEq.rfl⟩
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
h : HasFPowerSeriesAt f p x
⊢ Tendsto (fun y => ‖y - (x, x)‖) (nhds (x, x)) (nhds 0)
[PROOFSTEP]
refine' (continuous_id.sub continuous_const).norm.tendsto' _ _ _
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
h : HasFPowerSeriesAt f p x
⊢ ‖id (x, x) - (x, x)‖ = 0
[PROOFSTEP]
rw [_root_.id, sub_self, norm_zero]
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesOnBall (_root_.fderiv 𝕜 f)
    (ContinuousLinearMap.compFormalMultilinearSeries
      (↑(ContinuousLinearEquiv.mk (continuousMultilinearCurryFin1 𝕜 E F).toLinearEquiv))
      (FormalMultilinearSeries.changeOriginSeries p 1))
    x r
[PROOFSTEP]
suffices A :
  HasFPowerSeriesOnBall (fun z => continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin (z - x) 1))
    ((continuousMultilinearCurryFin1 𝕜 E F : (E[×1]→L[𝕜] F) →L[𝕜] E →L[𝕜] F).compFormalMultilinearSeries
      (p.changeOriginSeries 1))
    x r
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
A :
  HasFPowerSeriesOnBall
    (fun z => ↑(continuousMultilinearCurryFin1 𝕜 E F) (FormalMultilinearSeries.changeOrigin p (z - x) 1))
    (ContinuousLinearMap.compFormalMultilinearSeries
      (↑(ContinuousLinearEquiv.mk (continuousMultilinearCurryFin1 𝕜 E F).toLinearEquiv))
      (FormalMultilinearSeries.changeOriginSeries p 1))
    x r
⊢ HasFPowerSeriesOnBall (_root_.fderiv 𝕜 f)
    (ContinuousLinearMap.compFormalMultilinearSeries
      (↑(ContinuousLinearEquiv.mk (continuousMultilinearCurryFin1 𝕜 E F).toLinearEquiv))
      (FormalMultilinearSeries.changeOriginSeries p 1))
    x r
[PROOFSTEP]
apply A.congr
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
A :
  HasFPowerSeriesOnBall
    (fun z => ↑(continuousMultilinearCurryFin1 𝕜 E F) (FormalMultilinearSeries.changeOrigin p (z - x) 1))
    (ContinuousLinearMap.compFormalMultilinearSeries
      (↑(ContinuousLinearEquiv.mk (continuousMultilinearCurryFin1 𝕜 E F).toLinearEquiv))
      (FormalMultilinearSeries.changeOriginSeries p 1))
    x r
⊢ Set.EqOn (fun z => ↑(continuousMultilinearCurryFin1 𝕜 E F) (FormalMultilinearSeries.changeOrigin p (z - x) 1))
    (_root_.fderiv 𝕜 f) (EMetric.ball x r)
[PROOFSTEP]
intro z hz
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
A :
  HasFPowerSeriesOnBall
    (fun z => ↑(continuousMultilinearCurryFin1 𝕜 E F) (FormalMultilinearSeries.changeOrigin p (z - x) 1))
    (ContinuousLinearMap.compFormalMultilinearSeries
      (↑(ContinuousLinearEquiv.mk (continuousMultilinearCurryFin1 𝕜 E F).toLinearEquiv))
      (FormalMultilinearSeries.changeOriginSeries p 1))
    x r
z : E
hz : z ∈ EMetric.ball x r
⊢ (fun z => ↑(continuousMultilinearCurryFin1 𝕜 E F) (FormalMultilinearSeries.changeOrigin p (z - x) 1)) z =
    _root_.fderiv 𝕜 f z
[PROOFSTEP]
dsimp
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
A :
  HasFPowerSeriesOnBall
    (fun z => ↑(continuousMultilinearCurryFin1 𝕜 E F) (FormalMultilinearSeries.changeOrigin p (z - x) 1))
    (ContinuousLinearMap.compFormalMultilinearSeries
      (↑(ContinuousLinearEquiv.mk (continuousMultilinearCurryFin1 𝕜 E F).toLinearEquiv))
      (FormalMultilinearSeries.changeOriginSeries p 1))
    x r
z : E
hz : z ∈ EMetric.ball x r
⊢ ↑(continuousMultilinearCurryFin1 𝕜 E F) (FormalMultilinearSeries.changeOrigin p (z - x) 1) = _root_.fderiv 𝕜 f z
[PROOFSTEP]
rw [← h.fderiv_eq, add_sub_cancel'_right]
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
A :
  HasFPowerSeriesOnBall
    (fun z => ↑(continuousMultilinearCurryFin1 𝕜 E F) (FormalMultilinearSeries.changeOrigin p (z - x) 1))
    (ContinuousLinearMap.compFormalMultilinearSeries
      (↑(ContinuousLinearEquiv.mk (continuousMultilinearCurryFin1 𝕜 E F).toLinearEquiv))
      (FormalMultilinearSeries.changeOriginSeries p 1))
    x r
z : E
hz : z ∈ EMetric.ball x r
⊢ ↑‖z - x‖₊ < r
[PROOFSTEP]
simpa only [edist_eq_coe_nnnorm_sub, EMetric.mem_ball] using hz
[GOAL]
case A
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesOnBall
    (fun z => ↑(continuousMultilinearCurryFin1 𝕜 E F) (FormalMultilinearSeries.changeOrigin p (z - x) 1))
    (ContinuousLinearMap.compFormalMultilinearSeries
      (↑(ContinuousLinearEquiv.mk (continuousMultilinearCurryFin1 𝕜 E F).toLinearEquiv))
      (FormalMultilinearSeries.changeOriginSeries p 1))
    x r
[PROOFSTEP]
suffices B : HasFPowerSeriesOnBall (fun z => p.changeOrigin (z - x) 1) (p.changeOriginSeries 1) x r
[GOAL]
case A
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
B :
  HasFPowerSeriesOnBall (fun z => FormalMultilinearSeries.changeOrigin p (z - x) 1)
    (FormalMultilinearSeries.changeOriginSeries p 1) x r
⊢ HasFPowerSeriesOnBall
    (fun z => ↑(continuousMultilinearCurryFin1 𝕜 E F) (FormalMultilinearSeries.changeOrigin p (z - x) 1))
    (ContinuousLinearMap.compFormalMultilinearSeries
      (↑(ContinuousLinearEquiv.mk (continuousMultilinearCurryFin1 𝕜 E F).toLinearEquiv))
      (FormalMultilinearSeries.changeOriginSeries p 1))
    x r
case B
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesOnBall (fun z => FormalMultilinearSeries.changeOrigin p (z - x) 1)
    (FormalMultilinearSeries.changeOriginSeries p 1) x r
[PROOFSTEP]
exact (continuousMultilinearCurryFin1 𝕜 E F).toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesOnBall B
[GOAL]
case B
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesOnBall (fun z => FormalMultilinearSeries.changeOrigin p (z - x) 1)
    (FormalMultilinearSeries.changeOriginSeries p 1) x r
[PROOFSTEP]
simpa using ((p.hasFPowerSeriesOnBall_changeOrigin 1 (h.r_pos.trans_le h.r_le)).mono h.r_pos h.r_le).comp_sub x
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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
⊢ AnalyticOn 𝕜 (_root_.fderiv 𝕜 f) s
[PROOFSTEP]
intro y hy
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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
y : E
hy : y ∈ s
⊢ AnalyticAt 𝕜 (_root_.fderiv 𝕜 f) y
[PROOFSTEP]
rcases h y hy with ⟨p, r, hp⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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
y : E
hy : y ∈ s
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p y r
⊢ AnalyticAt 𝕜 (_root_.fderiv 𝕜 f) y
[PROOFSTEP]
exact hp.fderiv.analyticAt
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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 : ℕ
⊢ AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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
⊢ AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 Nat.zero f) s
[PROOFSTEP]
rw [iteratedFDeriv_zero_eq_comp]
[GOAL]
case zero
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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
⊢ AnalyticOn 𝕜 (↑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) ∘ f) s
[PROOFSTEP]
exact ((continuousMultilinearCurryFin0 𝕜 E F).symm : F →L[𝕜] E[×0]→L[𝕜] F).comp_analyticOn h
[GOAL]
case succ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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 : ℕ
IH : AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 (Nat.succ n) f) s
[PROOFSTEP]
rw [iteratedFDeriv_succ_eq_comp_left]
  -- Porting note: for reasons that I do not understand at all, `?g` cannot be inlined.
[GOAL]
case succ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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 : ℕ
IH : AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ AnalyticOn 𝕜 (↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) ∘ _root_.fderiv 𝕜 (_root_.iteratedFDeriv 𝕜 n f))
    s
[PROOFSTEP]
convert
  @ContinuousLinearMap.comp_analyticOn 𝕜 E ?_ (ContinuousMultilinearMap 𝕜 (fun _ : Fin (n + 1) ↦ E) F) ?_ ?_ ?_ ?_ ?_ ?_
    ?_ ?_ s ?g IH.fderiv
[GOAL]
case h.e'_9.h.e'_4
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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 : ℕ
IH : AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) = ↑?g
case g
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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 : ℕ
IH : AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ (E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E) F) →L[𝕜] ContinuousMultilinearMap 𝕜 (fun x => E) F
[PROOFSTEP]
case g => exact ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) => E) F)
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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 : ℕ
IH : AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ (E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E) F) →L[𝕜] ContinuousMultilinearMap 𝕜 (fun x => E) F
[PROOFSTEP]
case g => exact ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) => E) F)
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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 : ℕ
IH : AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ (E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E) F) →L[𝕜] ContinuousMultilinearMap 𝕜 (fun x => E) F
[PROOFSTEP]
exact ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) => E) F)
[GOAL]
case h.e'_9.h.e'_4
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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 : ℕ
IH : AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) =
    ↑↑(ContinuousLinearEquiv.mk (continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).toLinearEquiv)
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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
[PROOFSTEP]
let t := {x | AnalyticAt 𝕜 f x}
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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
[PROOFSTEP]
suffices : ContDiffOn 𝕜 n f t
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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
[PROOFSTEP]
exact this.mono h
[GOAL]
case this
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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
[PROOFSTEP]
have H : AnalyticOn 𝕜 f t := fun x hx => hx
[GOAL]
case this
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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
[PROOFSTEP]
have t_open : IsOpen t := isOpen_analyticAt 𝕜 f
[GOAL]
case this
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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
[PROOFSTEP]
apply contDiffOn_of_continuousOn_differentiableOn
[GOAL]
case this.Hcont
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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
[PROOFSTEP]
rintro m -
[GOAL]
case this.Hcont
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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
[PROOFSTEP]
apply (H.iteratedFDeriv m).continuousOn.congr
[GOAL]
case this.Hcont
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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
[PROOFSTEP]
intro x hx
[GOAL]
case this.Hcont
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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
[PROOFSTEP]
exact iteratedFDerivWithin_of_isOpen _ t_open hx
[GOAL]
case this.Hdiff
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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
[PROOFSTEP]
rintro m -
[GOAL]
case this.Hdiff
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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
[PROOFSTEP]
apply (H.iteratedFDeriv m).differentiableOn.congr
[GOAL]
case this.Hdiff
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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
[PROOFSTEP]
intro x hx
[GOAL]
case this.Hdiff
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
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
[PROOFSTEP]
exact iteratedFDerivWithin_of_isOpen _ t_open hx
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticAt 𝕜 f x
n : ℕ∞
⊢ ContDiffAt 𝕜 n f x
[PROOFSTEP]
obtain ⟨s, hs, hf⟩ := h.exists_mem_nhds_analyticOn
[GOAL]
case intro.intro
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s✝ : Set E
inst✝ : CompleteSpace F
h : AnalyticAt 𝕜 f x
n : ℕ∞
s : Set E
hs : s ∈ nhds x
hf : AnalyticOn 𝕜 f s
⊢ ContDiffAt 𝕜 n f x
[PROOFSTEP]
exact hf.contDiffOn.contDiffAt hs
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 𝕜 F
r : ℝ≥0∞
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ
⊢ AnalyticOn 𝕜 (_root_.deriv^[n] f) s
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 𝕜 F
r : ℝ≥0∞
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
⊢ AnalyticOn 𝕜 (_root_.deriv^[Nat.zero] f) s
[PROOFSTEP]
exact h
[GOAL]
case succ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 𝕜 F
r : ℝ≥0∞
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ
IH : AnalyticOn 𝕜 (_root_.deriv^[n] f) s
⊢ AnalyticOn 𝕜 (_root_.deriv^[Nat.succ n] f) s
[PROOFSTEP]
simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv
