[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


[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : CompleteSpace 𝕜
f : E →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 { x // x ∈ range f }
⊢ Submodule.ClosedComplemented (ker f)
[PROOFSTEP]
set f' : E →L[𝕜] range f := f.codRestrict _ (LinearMap.mem_range_self (f : E →ₗ[𝕜] F))
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : CompleteSpace 𝕜
f : E →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 { x // x ∈ range f }
f' : E →L[𝕜] { x // x ∈ range f } := codRestrict f (range f) (_ : ∀ (x : E), ↑↑f x ∈ range ↑f)
⊢ Submodule.ClosedComplemented (ker f)
[PROOFSTEP]
rcases f'.exists_right_inverse_of_surjective (f : E →ₗ[𝕜] F).range_rangeRestrict with ⟨g, hg⟩
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : CompleteSpace 𝕜
f : E →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 { x // x ∈ range f }
f' : E →L[𝕜] { x // x ∈ range f } := codRestrict f (range f) (_ : ∀ (x : E), ↑↑f x ∈ range ↑f)
g : { x // x ∈ range f } →L[𝕜] E
hg : comp f' g = id 𝕜 { x // x ∈ range f }
⊢ Submodule.ClosedComplemented (ker f)
[PROOFSTEP]
simpa only [ker_codRestrict] using f'.closedComplemented_ker_of_rightInverse g (ext_iff.1 hg)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace E
p q : Subspace 𝕜 E
h : IsCompl p q
hp : IsClosed ↑p
hq : IsClosed ↑q
⊢ ({ x // x ∈ p } × { x // x ∈ q }) ≃L[𝕜] E
[PROOFSTEP]
haveI := hp.completeSpace_coe
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace E
p q : Subspace 𝕜 E
h : IsCompl p q
hp : IsClosed ↑p
hq : IsClosed ↑q
this : CompleteSpace ↑↑p
⊢ ({ x // x ∈ p } × { x // x ∈ q }) ≃L[𝕜] E
[PROOFSTEP]
haveI := hq.completeSpace_coe
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace E
p q : Subspace 𝕜 E
h : IsCompl p q
hp : IsClosed ↑p
hq : IsClosed ↑q
this✝ : CompleteSpace ↑↑p
this : CompleteSpace ↑↑q
⊢ ({ x // x ∈ p } × { x // x ∈ q }) ≃L[𝕜] E
[PROOFSTEP]
refine' (p.prodEquivOfIsCompl q h).toContinuousLinearEquivOfContinuous _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace E
p q : Subspace 𝕜 E
h : IsCompl p q
hp : IsClosed ↑p
hq : IsClosed ↑q
this✝ : CompleteSpace ↑↑p
this : CompleteSpace ↑↑q
⊢ Continuous ↑(Submodule.prodEquivOfIsCompl p q h)
[PROOFSTEP]
exact (p.subtypeL.coprod q.subtypeL).continuous
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : CompleteSpace E
p q : Subspace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 (E ⧸ p)
hp : IsClosed ↑p
⊢ Submodule.ClosedComplemented p
[PROOFSTEP]
obtain ⟨q, hq⟩ : ∃ q, IsCompl p q := p.exists_isCompl
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : CompleteSpace E
p q✝ : Subspace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 (E ⧸ p)
hp : IsClosed ↑p
q : Subspace 𝕜 E
hq : IsCompl p q
⊢ Submodule.ClosedComplemented p
[PROOFSTEP]
haveI : FiniteDimensional 𝕜 q := (p.quotientEquivOfIsCompl q hq).finiteDimensional
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : CompleteSpace E
p q✝ : Subspace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 (E ⧸ p)
hp : IsClosed ↑p
q : Subspace 𝕜 E
hq : IsCompl p q
this : FiniteDimensional 𝕜 { x // x ∈ q }
⊢ Submodule.ClosedComplemented p
[PROOFSTEP]
exact closedComplemented_of_closed_compl hq hp q.closed_of_finiteDimensional


[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e e₁ e₂ : ENorm 𝕜 V
h : ↑e₁ = ↑e₂
⊢ e₁ = e₂
[PROOFSTEP]
cases e₁
[GOAL]
case mk
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e e₂ : ENorm 𝕜 V
toFun✝ : V → ℝ≥0∞
eq_zero'✝ : ∀ (x : V), toFun✝ x = 0 → x = 0
map_add_le'✝ : ∀ (x y : V), toFun✝ (x + y) ≤ toFun✝ x + toFun✝ y
map_smul_le'✝ : ∀ (c : 𝕜) (x : V), toFun✝ (c • x) ≤ ↑‖c‖₊ * toFun✝ x
h : ↑{ toFun := toFun✝, eq_zero' := eq_zero'✝, map_add_le' := map_add_le'✝, map_smul_le' := map_smul_le'✝ } = ↑e₂
⊢ { toFun := toFun✝, eq_zero' := eq_zero'✝, map_add_le' := map_add_le'✝, map_smul_le' := map_smul_le'✝ } = e₂
[PROOFSTEP]
cases e₂
[GOAL]
case mk.mk
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
toFun✝¹ : V → ℝ≥0∞
eq_zero'✝¹ : ∀ (x : V), toFun✝¹ x = 0 → x = 0
map_add_le'✝¹ : ∀ (x y : V), toFun✝¹ (x + y) ≤ toFun✝¹ x + toFun✝¹ y
map_smul_le'✝¹ : ∀ (c : 𝕜) (x : V), toFun✝¹ (c • x) ≤ ↑‖c‖₊ * toFun✝¹ x
toFun✝ : V → ℝ≥0∞
eq_zero'✝ : ∀ (x : V), toFun✝ x = 0 → x = 0
map_add_le'✝ : ∀ (x y : V), toFun✝ (x + y) ≤ toFun✝ x + toFun✝ y
map_smul_le'✝ : ∀ (c : 𝕜) (x : V), toFun✝ (c • x) ≤ ↑‖c‖₊ * toFun✝ x
h :
  ↑{ toFun := toFun✝¹, eq_zero' := eq_zero'✝¹, map_add_le' := map_add_le'✝¹, map_smul_le' := map_smul_le'✝¹ } =
    ↑{ toFun := toFun✝, eq_zero' := eq_zero'✝, map_add_le' := map_add_le'✝, map_smul_le' := map_smul_le'✝ }
⊢ { toFun := toFun✝¹, eq_zero' := eq_zero'✝¹, map_add_le' := map_add_le'✝¹, map_smul_le' := map_smul_le'✝¹ } =
    { toFun := toFun✝, eq_zero' := eq_zero'✝, map_add_le' := map_add_le'✝, map_smul_le' := map_smul_le'✝ }
[PROOFSTEP]
congr
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
⊢ ↑e (c • x) = ↑‖c‖₊ * ↑e x
[PROOFSTEP]
apply le_antisymm (e.map_smul_le' c x)
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
⊢ ↑‖c‖₊ * ↑e x ≤ ↑e (c • x)
[PROOFSTEP]
by_cases hc : c = 0
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hc : c = 0
⊢ ↑‖c‖₊ * ↑e x ≤ ↑e (c • x)
[PROOFSTEP]
simp [hc]
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hc : ¬c = 0
⊢ ↑‖c‖₊ * ↑e x ≤ ↑e (c • x)
[PROOFSTEP]
calc
  (‖c‖₊ : ℝ≥0∞) * e x = ‖c‖₊ * e (c⁻¹ • c • x) := by rw [inv_smul_smul₀ hc]
  _ ≤ ‖c‖₊ * (‖c⁻¹‖₊ * e (c • x)) := (mul_le_mul_left' (e.map_smul_le' _ _) _)
  _ = e (c • x) := by
    rw [← mul_assoc, nnnorm_inv, ENNReal.coe_inv, ENNReal.mul_inv_cancel _ ENNReal.coe_ne_top, one_mul] <;> simp [hc]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hc : ¬c = 0
⊢ ↑‖c‖₊ * ↑e x = ↑‖c‖₊ * ↑e (c⁻¹ • c • x)
[PROOFSTEP]
rw [inv_smul_smul₀ hc]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hc : ¬c = 0
⊢ ↑‖c‖₊ * (↑‖c⁻¹‖₊ * ↑e (c • x)) = ↑e (c • x)
[PROOFSTEP]
rw [← mul_assoc, nnnorm_inv, ENNReal.coe_inv, ENNReal.mul_inv_cancel _ ENNReal.coe_ne_top, one_mul]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hc : ¬c = 0
⊢ ↑‖c‖₊ ≠ 0
[PROOFSTEP]
simp [hc]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hc : ¬c = 0
⊢ ‖c‖₊ ≠ 0
[PROOFSTEP]
simp [hc]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
⊢ ↑e 0 = 0
[PROOFSTEP]
rw [← zero_smul 𝕜 (0 : V), e.map_smul]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
⊢ ↑‖0‖₊ * ↑e 0 = 0
[PROOFSTEP]
norm_num
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x : V
⊢ ↑e (-x) = ↑‖-1‖₊ * ↑e x
[PROOFSTEP]
rw [← map_smul, neg_one_smul]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x : V
⊢ ↑‖-1‖₊ * ↑e x = ↑e x
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
⊢ ↑e (x - y) = ↑e (y - x)
[PROOFSTEP]
rw [← neg_sub, e.map_neg]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
⊢ ↑e (x - y) = ↑e (x + -y)
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
⊢ ↑e x + ↑e (-y) = ↑e x + ↑e y
[PROOFSTEP]
rw [e.map_neg]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x : V
⊢ (fun x => if x = 0 then 0 else ⊤) x = 0 → x = 0
[PROOFSTEP]
simp only
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x : V
⊢ (if x = 0 then 0 else ⊤) = 0 → x = 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x : V
h✝ : x = 0
⊢ 0 = 0 → x = 0
[PROOFSTEP]
simp [*]
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x : V
h✝ : ¬x = 0
⊢ ⊤ = 0 → x = 0
[PROOFSTEP]
simp [*]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
⊢ (fun x => if x = 0 then 0 else ⊤) (x + y) ≤ (fun x => if x = 0 then 0 else ⊤) x + (fun x => if x = 0 then 0 else ⊤) y
[PROOFSTEP]
simp only
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
⊢ (if x + y = 0 then 0 else ⊤) ≤ (if x = 0 then 0 else ⊤) + if y = 0 then 0 else ⊤
[PROOFSTEP]
split_ifs with hxy hx hy hy hx hy hy
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : x + y = 0
hx : x = 0
hy : y = 0
⊢ 0 ≤ 0 + 0
[PROOFSTEP]
try simp [*]
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : x + y = 0
hx : x = 0
hy : y = 0
⊢ 0 ≤ 0 + 0
[PROOFSTEP]
simp [*]
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : x + y = 0
hx : x = 0
hy : ¬y = 0
⊢ 0 ≤ 0 + ⊤
[PROOFSTEP]
try simp [*]
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : x + y = 0
hx : x = 0
hy : ¬y = 0
⊢ 0 ≤ 0 + ⊤
[PROOFSTEP]
simp [*]
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : x + y = 0
hx : ¬x = 0
hy : y = 0
⊢ 0 ≤ ⊤ + 0
[PROOFSTEP]
try simp [*]
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : x + y = 0
hx : ¬x = 0
hy : y = 0
⊢ 0 ≤ ⊤ + 0
[PROOFSTEP]
simp [*]
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ 0 ≤ ⊤ + ⊤
[PROOFSTEP]
try simp [*]
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ 0 ≤ ⊤ + ⊤
[PROOFSTEP]
simp [*]
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : ¬x + y = 0
hx : x = 0
hy : y = 0
⊢ ⊤ ≤ 0 + 0
[PROOFSTEP]
try simp [*]
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : ¬x + y = 0
hx : x = 0
hy : y = 0
⊢ ⊤ ≤ 0 + 0
[PROOFSTEP]
simp [*]
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : ¬x + y = 0
hx : x = 0
hy : ¬y = 0
⊢ ⊤ ≤ 0 + ⊤
[PROOFSTEP]
try simp [*]
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : ¬x + y = 0
hx : x = 0
hy : ¬y = 0
⊢ ⊤ ≤ 0 + ⊤
[PROOFSTEP]
simp [*]
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : ¬x + y = 0
hx : ¬x = 0
hy : y = 0
⊢ ⊤ ≤ ⊤ + 0
[PROOFSTEP]
try simp [*]
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : ¬x + y = 0
hx : ¬x = 0
hy : y = 0
⊢ ⊤ ≤ ⊤ + 0
[PROOFSTEP]
simp [*]
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ ⊤ ≤ ⊤ + ⊤
[PROOFSTEP]
try simp [*]
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ ⊤ ≤ ⊤ + ⊤
[PROOFSTEP]
simp [*]
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : ¬x + y = 0
hx : x = 0
hy : y = 0
⊢ False
[PROOFSTEP]
simp [hx, hy] at hxy
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
⊢ (fun x => if x = 0 then 0 else ⊤) (c • x) ≤ ↑‖c‖₊ * (fun x => if x = 0 then 0 else ⊤) x
[PROOFSTEP]
simp only
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
⊢ (if c • x = 0 then 0 else ⊤) ≤ ↑‖c‖₊ * if x = 0 then 0 else ⊤
[PROOFSTEP]
split_ifs with hcx hx hx
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hcx : c • x = 0
hx : x = 0
⊢ 0 ≤ ↑‖c‖₊ * 0
[PROOFSTEP]
simp only [smul_eq_zero, not_or] at hcx
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hcx : c • x = 0
hx : ¬x = 0
⊢ 0 ≤ ↑‖c‖₊ * ⊤
[PROOFSTEP]
simp only [smul_eq_zero, not_or] at hcx
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hcx : ¬c • x = 0
hx : x = 0
⊢ ⊤ ≤ ↑‖c‖₊ * 0
[PROOFSTEP]
simp only [smul_eq_zero, not_or] at hcx
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hcx : ¬c • x = 0
hx : ¬x = 0
⊢ ⊤ ≤ ↑‖c‖₊ * ⊤
[PROOFSTEP]
simp only [smul_eq_zero, not_or] at hcx
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hx : x = 0
hcx : c = 0 ∨ x = 0
⊢ 0 ≤ ↑‖c‖₊ * 0
[PROOFSTEP]
simp only [mul_zero, le_refl]
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hx : ¬x = 0
hcx : c = 0 ∨ x = 0
⊢ 0 ≤ ↑‖c‖₊ * ⊤
[PROOFSTEP]
have : c = 0 := by tauto
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hx : ¬x = 0
hcx : c = 0 ∨ x = 0
⊢ c = 0
[PROOFSTEP]
tauto
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hx : ¬x = 0
hcx : c = 0 ∨ x = 0
this : c = 0
⊢ 0 ≤ ↑‖c‖₊ * ⊤
[PROOFSTEP]
simp [this]
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hx : x = 0
hcx : ¬c = 0 ∧ ¬x = 0
⊢ ⊤ ≤ ↑‖c‖₊ * 0
[PROOFSTEP]
tauto
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hx : ¬x = 0
hcx : ¬c = 0 ∧ ¬x = 0
⊢ ⊤ ≤ ↑‖c‖₊ * ⊤
[PROOFSTEP]
simpa [mul_top'] using hcx.1
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e✝ e : ENorm 𝕜 V
x : V
h : x = 0
⊢ ↑e x ≤ ↑⊤ x
[PROOFSTEP]
simp [h]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e✝ e : ENorm 𝕜 V
x : V
h : ¬x = 0
⊢ ↑e x ≤ ↑⊤ x
[PROOFSTEP]
simp [top_map h]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
src✝ : PartialOrder (ENorm 𝕜 V) := partialOrder
e₁ e₂ : ENorm 𝕜 V
c : 𝕜
x : V
⊢ (fun x => max (↑e₁ x) (↑e₂ x)) (c • x) = ↑‖c‖₊ * (fun x => max (↑e₁ x) (↑e₂ x)) x
[PROOFSTEP]
simp only [map_smul, ENNReal.mul_max]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x : V
⊢ edist x x = 0
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y z : V
⊢ ↑e (x - z) = ↑e (x - y + (y - z))
[PROOFSTEP]
rw [sub_add_sub_cancel]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
⊢ edist x y = 0 → x = y
[PROOFSTEP]
simp [sub_eq_zero]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
⊢ 0 ∈
    { carrier := {x | ↑e x < ⊤},
        add_mem' := (_ : ∀ {x y : V}, x ∈ {x | ↑e x < ⊤} → y ∈ {x | ↑e x < ⊤} → ↑e (x + y) < ⊤) }.carrier
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
⊢ MetricSpace { x // x ∈ finiteSubspace e }
[PROOFSTEP]
letI := e.emetricSpace
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
this : EMetricSpace V := emetricSpace e
⊢ MetricSpace { x // x ∈ finiteSubspace e }
[PROOFSTEP]
refine' EMetricSpace.toMetricSpace fun x y => _
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
this : EMetricSpace V := emetricSpace e
x y : { x // x ∈ finiteSubspace e }
⊢ edist x y ≠ ⊤
[PROOFSTEP]
change e (x - y) ≠ ⊤
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
this : EMetricSpace V := emetricSpace e
x y : { x // x ∈ finiteSubspace e }
⊢ ↑e (↑x - ↑y) ≠ ⊤
[PROOFSTEP]
exact ne_top_of_le_ne_top (ENNReal.add_lt_top.2 ⟨x.2, y.2⟩).ne (e.map_sub_le x y)
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : { x // x ∈ finiteSubspace e }
⊢ ‖c • x‖ = ‖c‖ * ‖x‖
[PROOFSTEP]
simp [finite_norm_eq, ENNReal.toReal_mul]