[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
⊢ ↑{ val := 0, property := (_ : 0 ≤ 0 ∧ 0 ≤ 0) } ∈ Icc 0 0
[PROOFSTEP]
rw [Subtype.coe_mk, Icc_self]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
⊢ 0 ∈ {0}
[PROOFSTEP]
exact mem_singleton _
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
x✝¹ : E
x✝ : x✝¹ ∈ closedBall 0 ↑0
⊢ ContinuousOn (fun t => OfNat.ofNat 0 t x✝¹) (Icc 0 0)
[PROOFSTEP]
simpa only [Pi.zero_apply] using continuousOn_const
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
⊢ dist t v.t₀ ≤ tDist v
[PROOFSTEP]
rw [Subtype.dist_eq, Real.dist_eq]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
⊢ |↑t - ↑v.t₀| ≤ tDist v
[PROOFSTEP]
cases' le_total t v.t₀ with ht ht
[GOAL]
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
ht : t ≤ v.t₀
⊢ |↑t - ↑v.t₀| ≤ tDist v
[PROOFSTEP]
rw [abs_of_nonpos (sub_nonpos.2 <| Subtype.coe_le_coe.2 ht), neg_sub]
[GOAL]
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
ht : t ≤ v.t₀
⊢ ↑v.t₀ - ↑t ≤ tDist v
[PROOFSTEP]
exact (sub_le_sub_left t.2.1 _).trans (le_max_right _ _)
[GOAL]
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
ht : v.t₀ ≤ t
⊢ |↑t - ↑v.t₀| ≤ tDist v
[PROOFSTEP]
rw [abs_of_nonneg (sub_nonneg.2 <| Subtype.coe_le_coe.2 ht)]
[GOAL]
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
ht : v.t₀ ≤ t
⊢ ↑t - ↑v.t₀ ≤ tDist v
[PROOFSTEP]
exact (sub_le_sub_right t.2.2 _).trans (le_max_left _ _)
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ℝ
ht : t ∈ Icc v.tMin v.tMax
⊢ ↑(proj v t) = t
[PROOFSTEP]
simp only [proj, projIcc_of_mem v.tMin_le_tMax ht]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ f g : FunSpace v
h : (fun f => ContinuousMap.mk f.toFun) f = (fun f => ContinuousMap.mk f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f g : FunSpace v
toFun✝ : ↑(Icc v.tMin v.tMax) → E
map_t₀'✝ : toFun✝ v.t₀ = v.x₀
lipschitz'✝ : LipschitzWith v.C toFun✝
h :
  (fun f => ContinuousMap.mk f.toFun) { toFun := toFun✝, map_t₀' := map_t₀'✝, lipschitz' := lipschitz'✝ } =
    (fun f => ContinuousMap.mk f.toFun) g
⊢ { toFun := toFun✝, map_t₀' := map_t₀'✝, lipschitz' := lipschitz'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
toFun✝¹ : ↑(Icc v.tMin v.tMax) → E
map_t₀'✝¹ : toFun✝¹ v.t₀ = v.x₀
lipschitz'✝¹ : LipschitzWith v.C toFun✝¹
toFun✝ : ↑(Icc v.tMin v.tMax) → E
map_t₀'✝ : toFun✝ v.t₀ = v.x₀
lipschitz'✝ : LipschitzWith v.C toFun✝
h :
  (fun f => ContinuousMap.mk f.toFun) { toFun := toFun✝¹, map_t₀' := map_t₀'✝¹, lipschitz' := lipschitz'✝¹ } =
    (fun f => ContinuousMap.mk f.toFun) { toFun := toFun✝, map_t₀' := map_t₀'✝, lipschitz' := lipschitz'✝ }
⊢ { toFun := toFun✝¹, map_t₀' := map_t₀'✝¹, lipschitz' := lipschitz'✝¹ } =
    { toFun := toFun✝, map_t₀' := map_t₀'✝, lipschitz' := lipschitz'✝ }
[PROOFSTEP]
simpa using h
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
⊢ range ↑toContinuousMap = {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f}
[PROOFSTEP]
ext f
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : C(↑(Icc v.tMin v.tMax), E)
⊢ f ∈ range ↑toContinuousMap ↔ f ∈ {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f}
[PROOFSTEP]
constructor
[GOAL]
case h.mp
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : C(↑(Icc v.tMin v.tMax), E)
⊢ f ∈ range ↑toContinuousMap → f ∈ {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f}
[PROOFSTEP]
rintro ⟨⟨f, hf₀, hf_lip⟩, rfl⟩
[GOAL]
case h.mp.intro.mk
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : ↑(Icc v.tMin v.tMax) → E
hf₀ : f v.t₀ = v.x₀
hf_lip : LipschitzWith v.C f
⊢ ↑toContinuousMap { toFun := f, map_t₀' := hf₀, lipschitz' := hf_lip } ∈ {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f}
[PROOFSTEP]
exact ⟨hf₀, hf_lip⟩
[GOAL]
case h.mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : C(↑(Icc v.tMin v.tMax), E)
⊢ f ∈ {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f} → f ∈ range ↑toContinuousMap
[PROOFSTEP]
rcases f with ⟨f, hf⟩
[GOAL]
case h.mpr.mk
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : ↑(Icc v.tMin v.tMax) → E
hf : Continuous f
⊢ ContinuousMap.mk f ∈ {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f} → ContinuousMap.mk f ∈ range ↑toContinuousMap
[PROOFSTEP]
rintro ⟨hf₀, hf_lip⟩
[GOAL]
case h.mpr.mk.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : ↑(Icc v.tMin v.tMax) → E
hf : Continuous f
hf₀ : ↑(ContinuousMap.mk f) v.t₀ = v.x₀
hf_lip : LipschitzWith v.C ↑(ContinuousMap.mk f)
⊢ ContinuousMap.mk f ∈ range ↑toContinuousMap
[PROOFSTEP]
exact ⟨⟨f, hf₀, hf_lip⟩, rfl⟩
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
t : ↑(Icc v.tMin v.tMax)
⊢ dist (toFun f t) v.x₀ = dist (toFun f t) (toFun f v.t₀)
[PROOFSTEP]
rw [f.map_t₀']
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
t : ↑(Icc v.tMin v.tMax)
⊢ vComp f ↑t = PicardLindelof.toFun v (↑t) (toFun f t)
[PROOFSTEP]
simp only [vComp, proj_coe]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
⊢ Continuous (vComp f)
[PROOFSTEP]
have := (continuous_subtype_val.prod_mk f.continuous).comp v.continuous_proj
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
this : Continuous ((fun x => (↑x, toFun f x)) ∘ proj v)
⊢ Continuous (vComp f)
[PROOFSTEP]
refine' ContinuousOn.comp_continuous v.continuousOn this fun x => _
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
this : Continuous ((fun x => (↑x, toFun f x)) ∘ proj v)
x : ℝ
⊢ ((fun x => (↑x, toFun f x)) ∘ proj v) x ∈ Icc v.tMin v.tMax ×ˢ closedBall v.x₀ ↑v.R
[PROOFSTEP]
exact ⟨(v.proj x).2, f.mem_closedBall _⟩
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
⊢ CompleteSpace (FunSpace v)
[PROOFSTEP]
refine' (completeSpace_iff_isComplete_range uniformInducing_toContinuousMap).2 (IsClosed.isComplete _)
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
⊢ IsClosed (range ↑toContinuousMap)
[PROOFSTEP]
rw [range_toContinuousMap, setOf_and]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
⊢ IsClosed ({a | ↑a v.t₀ = v.x₀} ∩ {a | LipschitzWith v.C ↑a})
[PROOFSTEP]
refine' (isClosed_eq (ContinuousMap.continuous_eval_const _) continuous_const).inter _
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
⊢ IsClosed {a | LipschitzWith v.C ↑a}
[PROOFSTEP]
have : IsClosed {f : Icc v.tMin v.tMax → E | LipschitzWith v.C f} := isClosed_setOf_lipschitzWith v.C
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
this : IsClosed {f | LipschitzWith v.C f}
⊢ IsClosed {a | LipschitzWith v.C ↑a}
[PROOFSTEP]
exact this.preimage ContinuousMap.continuous_coe
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
inst✝ : CompleteSpace E
f : FunSpace v
⊢ (fun t => v.x₀ + ∫ (τ : ℝ) in ↑v.t₀..↑t, vComp f τ) v.t₀ = v.x₀
[PROOFSTEP]
simp only [integral_same, add_zero]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
inst✝ : CompleteSpace E
f : FunSpace v
t₁ t₂ : ↑(Icc v.tMin v.tMax)
⊢ dist (v.x₀ + ∫ (τ : ℝ) in ↑v.t₀..↑t₁, vComp f τ) (v.x₀ + ∫ (τ : ℝ) in ↑v.t₀..↑t₂, vComp f τ) ≤ ↑v.C * dist t₁ t₂
[PROOFSTEP]
rw [dist_add_left, dist_eq_norm,
  integral_interval_sub_left (f.intervalIntegrable_vComp _ _) (f.intervalIntegrable_vComp _ _)]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
inst✝ : CompleteSpace E
f : FunSpace v
t₁ t₂ : ↑(Icc v.tMin v.tMax)
⊢ ‖∫ (x : ℝ) in ↑t₂..↑t₁, vComp f x‖ ≤ ↑v.C * dist t₁ t₂
[PROOFSTEP]
exact norm_integral_le_of_norm_le_const fun t _ => f.norm_vComp_le _
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
⊢ HasDerivWithinAt ((next f).toFun ∘ proj v) (PicardLindelof.toFun v (↑t) (toFun f t)) (Icc v.tMin v.tMax) ↑t
[PROOFSTEP]
haveI : Fact ((t : ℝ) ∈ Icc v.tMin v.tMax) := ⟨t.2⟩
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
this : Fact (↑t ∈ Icc v.tMin v.tMax)
⊢ HasDerivWithinAt ((next f).toFun ∘ proj v) (PicardLindelof.toFun v (↑t) (toFun f t)) (Icc v.tMin v.tMax) ↑t
[PROOFSTEP]
simp only [(· ∘ ·), next_apply]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
this : Fact (↑t ∈ Icc v.tMin v.tMax)
⊢ HasDerivWithinAt (fun x => v.x₀ + ∫ (τ : ℝ) in ↑v.t₀..↑(proj v x), vComp f τ)
    (PicardLindelof.toFun v (↑t) (toFun f t)) (Icc v.tMin v.tMax) ↑t
[PROOFSTEP]
refine' HasDerivWithinAt.const_add _ _
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
this : Fact (↑t ∈ Icc v.tMin v.tMax)
⊢ HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..↑(proj v x), vComp f τ) (PicardLindelof.toFun v (↑t) (toFun f t))
    (Icc v.tMin v.tMax) ↑t
[PROOFSTEP]
have : HasDerivWithinAt (∫ τ in v.t₀..·, f.vComp τ) (f.vComp t) (Icc v.tMin v.tMax) t :=
  integral_hasDerivWithinAt_right (f.intervalIntegrable_vComp _ _) (f.continuous_vComp.stronglyMeasurableAtFilter _ _)
    f.continuous_vComp.continuousWithinAt
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
this✝ : Fact (↑t ∈ Icc v.tMin v.tMax)
this : HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..x, vComp f τ) (vComp f ↑t) (Icc v.tMin v.tMax) ↑t
⊢ HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..↑(proj v x), vComp f τ) (PicardLindelof.toFun v (↑t) (toFun f t))
    (Icc v.tMin v.tMax) ↑t
[PROOFSTEP]
rw [vComp_apply_coe] at this
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
this✝ : Fact (↑t ∈ Icc v.tMin v.tMax)
this :
  HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..x, vComp f τ) (PicardLindelof.toFun v (↑t) (toFun f t))
    (Icc v.tMin v.tMax) ↑t
⊢ HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..↑(proj v x), vComp f τ) (PicardLindelof.toFun v (↑t) (toFun f t))
    (Icc v.tMin v.tMax) ↑t
[PROOFSTEP]
refine' this.congr_of_eventuallyEq_of_mem _ t.coe_prop
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
this✝ : Fact (↑t ∈ Icc v.tMin v.tMax)
this :
  HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..x, vComp f τ) (PicardLindelof.toFun v (↑t) (toFun f t))
    (Icc v.tMin v.tMax) ↑t
⊢ (fun x => ∫ (τ : ℝ) in ↑v.t₀..↑(proj v x), vComp f τ) =ᶠ[𝓝[Icc v.tMin v.tMax] ↑t] fun x =>
    ∫ (τ : ℝ) in ↑v.t₀..x, vComp f τ
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin] with _ ht'
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
this✝ : Fact (↑t ∈ Icc v.tMin v.tMax)
this :
  HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..x, vComp f τ) (PicardLindelof.toFun v (↑t) (toFun f t))
    (Icc v.tMin v.tMax) ↑t
a✝ : ℝ
ht' : a✝ ∈ Icc v.tMin v.tMax
⊢ ∫ (τ : ℝ) in ↑v.t₀..↑(proj v a✝), vComp f τ = ∫ (τ : ℝ) in ↑v.t₀..a✝, vComp f τ
[PROOFSTEP]
rw [v.proj_of_mem ht']
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
d : ℝ
h : ∀ (t : ↑(Icc v.tMin v.tMax)), dist (toFun f₁ t) (toFun f₂ t) ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
t : ↑(Icc v.tMin v.tMax)
⊢ dist (toFun (next f₁) t) (toFun (next f₂) t) ≤ (↑v.L * |↑t - ↑v.t₀|) ^ (n + 1) / ↑(n + 1)! * d
[PROOFSTEP]
simp only [dist_eq_norm, next_apply, add_sub_add_left_eq_sub, ←
  intervalIntegral.integral_sub (intervalIntegrable_vComp _ _ _) (intervalIntegrable_vComp _ _ _),
  norm_integral_eq_norm_integral_Ioc] at *
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖toFun f₁ t - toFun f₂ t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
⊢ ‖∫ (x : ℝ) in Ι ↑v.t₀ ↑t, vComp f₁ x - vComp f₂ x‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ (n + 1) / ↑(n + 1)! * d
[PROOFSTEP]
calc
  ‖∫ τ in Ι (v.t₀ : ℝ) t, f₁.vComp τ - f₂.vComp τ‖ ≤ ∫ τ in Ι (v.t₀ : ℝ) t, v.L * ((v.L * |τ - v.t₀|) ^ n / n ! * d) :=
    by
    refine' norm_integral_le_of_norm_le (Continuous.integrableOn_uIoc _) _
    ·
      -- porting note: was `continuity`
      refine .mul continuous_const <| .mul (.div_const ?_ _) continuous_const
      refine .pow (.mul continuous_const <| .abs <| ?_) _
      exact .sub continuous_id continuous_const
    · refine' (ae_restrict_mem measurableSet_Ioc).mono fun τ hτ => _
      refine'
        (v.lipschitzOnWith (v.proj τ).2).norm_sub_le_of_le (f₁.mem_closedBall _) (f₂.mem_closedBall _)
          ((h _).trans_eq _)
      rw [v.proj_of_mem]
      exact uIcc_subset_Icc v.t₀.2 t.2 <| Ioc_subset_Icc_self hτ
  _ = (v.L * |t.1 - v.t₀|) ^ (n + 1) / (n + 1)! * d := by
    simp_rw [mul_pow, div_eq_mul_inv, mul_assoc, MeasureTheory.integral_mul_left, MeasureTheory.integral_mul_right,
      integral_pow_abs_sub_uIoc, div_eq_mul_inv, pow_succ (v.L : ℝ), Nat.factorial_succ, Nat.cast_mul, Nat.cast_succ,
      mul_inv, mul_assoc]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖toFun f₁ t - toFun f₂ t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
⊢ ‖∫ (τ : ℝ) in Ι ↑v.t₀ ↑t, vComp f₁ τ - vComp f₂ τ‖ ≤
    ∫ (τ : ℝ) in Ι ↑v.t₀ ↑t, ↑v.L * ((↑v.L * |τ - ↑v.t₀|) ^ n / ↑n ! * d)
[PROOFSTEP]
refine' norm_integral_le_of_norm_le (Continuous.integrableOn_uIoc _) _
[GOAL]
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖toFun f₁ t - toFun f₂ t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
⊢ Continuous fun τ => ↑v.L * ((↑v.L * |τ - ↑v.t₀|) ^ n / ↑n ! * d)
[PROOFSTEP]
refine .mul continuous_const <| .mul (.div_const ?_ _) continuous_const
[GOAL]
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖toFun f₁ t - toFun f₂ t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
⊢ Continuous fun τ => (↑v.L * |τ - ↑v.t₀|) ^ n
[PROOFSTEP]
refine .pow (.mul continuous_const <| .abs <| ?_) _
[GOAL]
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖toFun f₁ t - toFun f₂ t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
⊢ Continuous fun τ => τ - ↑v.t₀
[PROOFSTEP]
exact .sub continuous_id continuous_const
[GOAL]
case refine'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖toFun f₁ t - toFun f₂ t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι ↑v.t₀ ↑t),
    ‖vComp f₁ x - vComp f₂ x‖ ≤ ↑v.L * ((↑v.L * |x - ↑v.t₀|) ^ n / ↑n ! * d)
[PROOFSTEP]
refine' (ae_restrict_mem measurableSet_Ioc).mono fun τ hτ => _
[GOAL]
case refine'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖toFun f₁ t - toFun f₂ t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
τ : ℝ
hτ : τ ∈ Ioc (min ↑v.t₀ ↑t) (max ↑v.t₀ ↑t)
⊢ ‖vComp f₁ τ - vComp f₂ τ‖ ≤ ↑v.L * ((↑v.L * |τ - ↑v.t₀|) ^ n / ↑n ! * d)
[PROOFSTEP]
refine'
  (v.lipschitzOnWith (v.proj τ).2).norm_sub_le_of_le (f₁.mem_closedBall _) (f₂.mem_closedBall _) ((h _).trans_eq _)
[GOAL]
case refine'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖toFun f₁ t - toFun f₂ t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
τ : ℝ
hτ : τ ∈ Ioc (min ↑v.t₀ ↑t) (max ↑v.t₀ ↑t)
⊢ (↑v.L * |↑(proj v τ) - ↑v.t₀|) ^ n / ↑n ! * d = (↑v.L * |τ - ↑v.t₀|) ^ n / ↑n ! * d
[PROOFSTEP]
rw [v.proj_of_mem]
[GOAL]
case refine'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖toFun f₁ t - toFun f₂ t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
τ : ℝ
hτ : τ ∈ Ioc (min ↑v.t₀ ↑t) (max ↑v.t₀ ↑t)
⊢ τ ∈ Icc v.tMin v.tMax
[PROOFSTEP]
exact uIcc_subset_Icc v.t₀.2 t.2 <| Ioc_subset_Icc_self hτ
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖toFun f₁ t - toFun f₂ t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
⊢ ∫ (τ : ℝ) in Ι ↑v.t₀ ↑t, ↑v.L * ((↑v.L * |τ - ↑v.t₀|) ^ n / ↑n ! * d) =
    (↑v.L * |↑t - ↑v.t₀|) ^ (n + 1) / ↑(n + 1)! * d
[PROOFSTEP]
simp_rw [mul_pow, div_eq_mul_inv, mul_assoc, MeasureTheory.integral_mul_left, MeasureTheory.integral_mul_right,
  integral_pow_abs_sub_uIoc, div_eq_mul_inv, pow_succ (v.L : ℝ), Nat.factorial_succ, Nat.cast_mul, Nat.cast_succ,
  mul_inv, mul_assoc]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
t : ↑(Icc v.tMin v.tMax)
⊢ dist (toFun (next^[n] f₁) t) (toFun (next^[n] f₂) t) ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * dist f₁ f₂
[PROOFSTEP]
induction' n with n ihn generalizing t
[GOAL]
case zero
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
t✝ t : ↑(Icc v.tMin v.tMax)
⊢ dist (toFun (next^[Nat.zero] f₁) t) (toFun (next^[Nat.zero] f₂) t) ≤
    (↑v.L * |↑t - ↑v.t₀|) ^ Nat.zero / ↑Nat.zero ! * dist f₁ f₂
[PROOFSTEP]
rw [Nat.zero_eq, pow_zero, Nat.factorial_zero, Nat.cast_one, div_one, one_mul]
[GOAL]
case zero
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
t✝ t : ↑(Icc v.tMin v.tMax)
⊢ dist (toFun (next^[0] f₁) t) (toFun (next^[0] f₂) t) ≤ dist f₁ f₂
[PROOFSTEP]
exact dist_apply_le_dist f₁ f₂ t
[GOAL]
case succ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
t✝ : ↑(Icc v.tMin v.tMax)
n : ℕ
ihn :
  ∀ (t : ↑(Icc v.tMin v.tMax)),
    dist (toFun (next^[n] f₁) t) (toFun (next^[n] f₂) t) ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * dist f₁ f₂
t : ↑(Icc v.tMin v.tMax)
⊢ dist (toFun (next^[Nat.succ n] f₁) t) (toFun (next^[Nat.succ n] f₂) t) ≤
    (↑v.L * |↑t - ↑v.t₀|) ^ Nat.succ n / ↑(Nat.succ n)! * dist f₁ f₂
[PROOFSTEP]
rw [iterate_succ_apply', iterate_succ_apply']
[GOAL]
case succ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
t✝ : ↑(Icc v.tMin v.tMax)
n : ℕ
ihn :
  ∀ (t : ↑(Icc v.tMin v.tMax)),
    dist (toFun (next^[n] f₁) t) (toFun (next^[n] f₂) t) ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * dist f₁ f₂
t : ↑(Icc v.tMin v.tMax)
⊢ dist (toFun (next (next^[n] f₁)) t) (toFun (next (next^[n] f₂)) t) ≤
    (↑v.L * |↑t - ↑v.t₀|) ^ Nat.succ n / ↑(Nat.succ n)! * dist f₁ f₂
[PROOFSTEP]
exact dist_next_apply_le_of_le ihn _
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
⊢ dist (next^[n] f₁) (next^[n] f₂) ≤ (↑v.L * tDist v) ^ n / ↑n ! * dist f₁ f₂
[PROOFSTEP]
refine' dist_le_of_forall fun t => (dist_iterate_next_apply_le _ _ _ _).trans _
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
t : ↑(Icc v.tMin v.tMax)
⊢ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * dist f₁ f₂ ≤ (↑v.L * tDist v) ^ n / ↑n ! * dist f₁ f₂
[PROOFSTEP]
have : |(t - v.t₀ : ℝ)| ≤ v.tDist := v.dist_t₀_le t
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
t : ↑(Icc v.tMin v.tMax)
this : |↑t - ↑v.t₀| ≤ tDist v
⊢ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * dist f₁ f₂ ≤ (↑v.L * tDist v) ^ n / ↑n ! * dist f₁ f₂
[PROOFSTEP]
gcongr
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
⊢ ∃ N K, ContractingWith K FunSpace.next^[N]
[PROOFSTEP]
rcases((Real.tendsto_pow_div_factorial_atTop (v.L * v.tDist)).eventually (gt_mem_nhds zero_lt_one)).exists with ⟨N, hN⟩
[GOAL]
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
N : ℕ
hN : (↑v.L * tDist v) ^ N / ↑N ! < 1
⊢ ∃ N K, ContractingWith K FunSpace.next^[N]
[PROOFSTEP]
have : (0 : ℝ) ≤ (v.L * v.tDist) ^ N / N ! :=
  div_nonneg (pow_nonneg (mul_nonneg v.L.2 v.tDist_nonneg) _) (Nat.cast_nonneg _)
[GOAL]
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
N : ℕ
hN : (↑v.L * tDist v) ^ N / ↑N ! < 1
this : 0 ≤ (↑v.L * tDist v) ^ N / ↑N !
⊢ ∃ N K, ContractingWith K FunSpace.next^[N]
[PROOFSTEP]
exact ⟨N, ⟨_, this⟩, hN, LipschitzWith.of_dist_le_mul fun f g => FunSpace.dist_iterate_next_le f g N⟩
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
⊢ ∃ f, f ↑v.t₀ = v.x₀ ∧ ∀ (t : ℝ), t ∈ Icc v.tMin v.tMax → HasDerivWithinAt f (toFun v t (f t)) (Icc v.tMin v.tMax) t
[PROOFSTEP]
rcases v.exists_fixed with ⟨f, hf⟩
[GOAL]
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
f : FunSpace v
hf : FunSpace.next f = f
⊢ ∃ f, f ↑v.t₀ = v.x₀ ∧ ∀ (t : ℝ), t ∈ Icc v.tMin v.tMax → HasDerivWithinAt f (toFun v t (f t)) (Icc v.tMin v.tMax) t
[PROOFSTEP]
refine' ⟨f ∘ v.proj, _, fun t ht => _⟩
[GOAL]
case intro.refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
f : FunSpace v
hf : FunSpace.next f = f
⊢ (f.toFun ∘ proj v) ↑v.t₀ = v.x₀
[PROOFSTEP]
simp only [(· ∘ ·), proj_coe, f.map_t₀]
[GOAL]
case intro.refine'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
f : FunSpace v
hf : FunSpace.next f = f
t : ℝ
ht : t ∈ Icc v.tMin v.tMax
⊢ HasDerivWithinAt (f.toFun ∘ proj v) (toFun v t ((f.toFun ∘ proj v) t)) (Icc v.tMin v.tMax) t
[PROOFSTEP]
simp only [(· ∘ ·), v.proj_of_mem ht]
[GOAL]
case intro.refine'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
f : FunSpace v
hf : FunSpace.next f = f
t : ℝ
ht : t ∈ Icc v.tMin v.tMax
⊢ HasDerivWithinAt (fun x => FunSpace.toFun f (proj v x)) (toFun v t (FunSpace.toFun f (proj v t))) (Icc v.tMin v.tMax)
    t
[PROOFSTEP]
lift t to Icc v.tMin v.tMax using ht
[GOAL]
case intro.refine'_2.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
f : FunSpace v
hf : FunSpace.next f = f
t : { x // x ∈ Icc v.tMin v.tMax }
⊢ HasDerivWithinAt (fun x => FunSpace.toFun f (proj v x)) (toFun v (↑t) (FunSpace.toFun f (proj v ↑t)))
    (Icc v.tMin v.tMax) ↑t
[PROOFSTEP]
simpa only [hf, v.proj_coe] using f.hasDerivWithinAt_next t
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
v : ℝ → E → E
tMin t₀ tMax : ℝ
x₀ : E
C R : ℝ
L : ℝ≥0
hpl : IsPicardLindelof v tMin t₀ tMax x₀ L R C
⊢ ∃ f, f t₀ = x₀ ∧ ∀ (t : ℝ), t ∈ Icc tMin tMax → HasDerivWithinAt f (v t (f t)) (Icc tMin tMax) t
[PROOFSTEP]
lift C to ℝ≥0 using (norm_nonneg _).trans hpl.norm_le₀
[GOAL]
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
v : ℝ → E → E
tMin t₀ tMax : ℝ
x₀ : E
R : ℝ
L C : ℝ≥0
hpl : IsPicardLindelof v tMin t₀ tMax x₀ L R ↑C
⊢ ∃ f, f t₀ = x₀ ∧ ∀ (t : ℝ), t ∈ Icc tMin tMax → HasDerivWithinAt f (v t (f t)) (Icc tMin tMax) t
[PROOFSTEP]
lift t₀ to Icc tMin tMax using hpl.ht₀
[GOAL]
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
v : ℝ → E → E
tMin tMax : ℝ
x₀ : E
R : ℝ
L C : ℝ≥0
t₀ : { x // x ∈ Icc tMin tMax }
hpl : IsPicardLindelof v tMin (↑t₀) tMax x₀ L R ↑C
⊢ ∃ f, f ↑t₀ = x₀ ∧ ∀ (t : ℝ), t ∈ Icc tMin tMax → HasDerivWithinAt f (v t (f t)) (Icc tMin tMax) t
[PROOFSTEP]
exact PicardLindelof.exists_solution ⟨v, tMin, tMax, t₀, x₀, C, ⟨R, hpl.hR⟩, L, { hpl with ht₀ := t₀.property }⟩
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
[PROOFSTEP]
obtain ⟨L, s', hs', hlip⟩ :=
  ContDiffAt.exists_lipschitzOnWith
    ((hv.contDiffWithinAt (mem_of_mem_nhds hs)).contDiffAt hs)
      -- radius of closed ball in which v is bounded
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
[PROOFSTEP]
obtain ⟨r, hr : 0 < r, hball⟩ := Metric.mem_nhds_iff.mp (inter_sets (𝓝 x₀) hs hs')
[GOAL]
case intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
[PROOFSTEP]
have hr' := (half_pos hr).le
[GOAL]
case intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
[PROOFSTEP]
obtain ⟨C, hC⟩ :=
  (isCompact_closedBall x₀ (r / 2)).bddAbove_image <|
    hv.continuousOn.norm.mono (subset_inter_iff.mp ((closedBall_subset_ball (half_lt_self hr)).trans hball)).left
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
[PROOFSTEP]
have hC' : 0 ≤ C := by
  apply (norm_nonneg (v x₀)).trans
  apply hC
  exact ⟨x₀, ⟨mem_closedBall_self hr', rfl⟩⟩
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
⊢ 0 ≤ C
[PROOFSTEP]
apply (norm_nonneg (v x₀)).trans
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
⊢ ‖v x₀‖ ≤ C
[PROOFSTEP]
apply hC
[GOAL]
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
⊢ ‖v x₀‖ ∈ (fun x => ‖v x‖) '' closedBall x₀ (r / 2)
[PROOFSTEP]
exact ⟨x₀, ⟨mem_closedBall_self hr', rfl⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
[PROOFSTEP]
set ε := if C = 0 then 1 else r / 2 / C with hε
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
[PROOFSTEP]
have hε0 : 0 < ε := by
  rw [hε]
  split_ifs with h
  · exact zero_lt_one
  · exact div_pos (half_pos hr) (lt_of_le_of_ne hC' (Ne.symm h))
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
⊢ 0 < ε
[PROOFSTEP]
rw [hε]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
⊢ 0 < if C = 0 then 1 else r / 2 / C
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
h : C = 0
⊢ 0 < 1
[PROOFSTEP]
exact zero_lt_one
[GOAL]
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
h : ¬C = 0
⊢ 0 < r / 2 / C
[PROOFSTEP]
exact div_pos (half_pos hr) (lt_of_le_of_ne hC' (Ne.symm h))
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
[PROOFSTEP]
refine' ⟨ε, hε0, L, r / 2, C, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
⊢ IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L (r / 2) C
[PROOFSTEP]
exact
  { ht₀ := by rw [← Real.closedBall_eq_Icc]; exact mem_closedBall_self hε0.le
    hR := (half_pos hr).le
    lipschitz := fun t _ =>
      hlip.mono (subset_inter_iff.mp (Subset.trans (closedBall_subset_ball (half_lt_self hr)) hball)).2
    cont := fun x _ => continuousOn_const
    norm_le := fun t _ x hx => hC ⟨x, hx, rfl⟩
    C_mul_le_R := by
      rw [add_sub_cancel', sub_sub_cancel, max_self, mul_ite, mul_one]
      split_ifs with h
      · rwa [← h] at hr'
      · exact (mul_div_cancel' (r / 2) h).le }
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
⊢ t₀ ∈ Icc (t₀ - ε) (t₀ + ε)
[PROOFSTEP]
rw [← Real.closedBall_eq_Icc]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
⊢ t₀ ∈ closedBall t₀ ε
[PROOFSTEP]
exact mem_closedBall_self hε0.le
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
⊢ C * max (t₀ + ε - t₀) (t₀ - (t₀ - ε)) ≤ r / 2
[PROOFSTEP]
rw [add_sub_cancel', sub_sub_cancel, max_self, mul_ite, mul_one]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
⊢ (if C = 0 then C else C * (r / 2 / C)) ≤ r / 2
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
h : C = 0
⊢ C ≤ r / 2
[PROOFSTEP]
rwa [← h] at hr'
[GOAL]
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
h : ¬C = 0
⊢ C * (r / 2 / C) ≤ r / 2
[PROOFSTEP]
exact (mul_div_cancel' (r / 2) h).le
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
⊢ ∃ ε, ε > 0 ∧ ∃ f, f t₀ = x₀ ∧ ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → f t ∈ s ∧ HasDerivAt f (v (f t)) t
[PROOFSTEP]
obtain ⟨ε, hε, L, R, C, hpl⟩ := exists_isPicardLindelof_const_of_contDiffOn_nhds t₀ x₀ hv hs
[GOAL]
case intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
⊢ ∃ ε, ε > 0 ∧ ∃ f, f t₀ = x₀ ∧ ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → f t ∈ s ∧ HasDerivAt f (v (f t)) t
[PROOFSTEP]
obtain ⟨f, hf1, hf2⟩ := hpl.exists_forall_hasDerivWithinAt_Icc_eq x₀
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
⊢ ∃ ε, ε > 0 ∧ ∃ f, f t₀ = x₀ ∧ ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → f t ∈ s ∧ HasDerivAt f (v (f t)) t
[PROOFSTEP]
have hf2' : ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt f (v (f t)) t := fun t ht =>
  (hf2 t (Ioo_subset_Icc_self ht)).hasDerivAt (Icc_mem_nhds ht.1 ht.2)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
⊢ ∃ ε, ε > 0 ∧ ∃ f, f t₀ = x₀ ∧ ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → f t ∈ s ∧ HasDerivAt f (v (f t)) t
[PROOFSTEP]
have h : f ⁻¹' s ∈ 𝓝 t₀ :=
  by
  have := hf2' t₀ (mem_Ioo.mpr ⟨sub_lt_self _ hε, lt_add_of_pos_right _ hε⟩)
  apply ContinuousAt.preimage_mem_nhds this.continuousAt
  rw [hf1]
  exact hs
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
⊢ f ⁻¹' s ∈ 𝓝 t₀
[PROOFSTEP]
have := hf2' t₀ (mem_Ioo.mpr ⟨sub_lt_self _ hε, lt_add_of_pos_right _ hε⟩)
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
this : HasDerivAt f (v (f t₀)) t₀
⊢ f ⁻¹' s ∈ 𝓝 t₀
[PROOFSTEP]
apply ContinuousAt.preimage_mem_nhds this.continuousAt
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
this : HasDerivAt f (v (f t₀)) t₀
⊢ s ∈ 𝓝 (f t₀)
[PROOFSTEP]
rw [hf1]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
this : HasDerivAt f (v (f t₀)) t₀
⊢ s ∈ 𝓝 x₀
[PROOFSTEP]
exact hs
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
h : f ⁻¹' s ∈ 𝓝 t₀
⊢ ∃ ε, ε > 0 ∧ ∃ f, f t₀ = x₀ ∧ ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → f t ∈ s ∧ HasDerivAt f (v (f t)) t
[PROOFSTEP]
rw [Metric.mem_nhds_iff] at h
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
h : ∃ ε, ε > 0 ∧ ball t₀ ε ⊆ f ⁻¹' s
⊢ ∃ ε, ε > 0 ∧ ∃ f, f t₀ = x₀ ∧ ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → f t ∈ s ∧ HasDerivAt f (v (f t)) t
[PROOFSTEP]
obtain ⟨r, hr1, hr2⟩ := h
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
r : ℝ
hr1 : r > 0
hr2 : ball t₀ r ⊆ f ⁻¹' s
⊢ ∃ ε, ε > 0 ∧ ∃ f, f t₀ = x₀ ∧ ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → f t ∈ s ∧ HasDerivAt f (v (f t)) t
[PROOFSTEP]
refine
  ⟨min r ε, lt_min hr1 hε, f, hf1, fun t ht =>
    ⟨?_,
      hf2' t
        (mem_of_mem_of_subset ht
          (Ioo_subset_Ioo (sub_le_sub_left (min_le_right _ _) _) (add_le_add_left (min_le_right _ _) _)))⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
r : ℝ
hr1 : r > 0
hr2 : ball t₀ r ⊆ f ⁻¹' s
t : ℝ
ht : t ∈ Ioo (t₀ - min r ε) (t₀ + min r ε)
⊢ f t ∈ s
[PROOFSTEP]
rw [← Set.mem_preimage]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
r : ℝ
hr1 : r > 0
hr2 : ball t₀ r ⊆ f ⁻¹' s
t : ℝ
ht : t ∈ Ioo (t₀ - min r ε) (t₀ + min r ε)
⊢ t ∈ f ⁻¹' s
[PROOFSTEP]
apply Set.mem_of_mem_of_subset _ hr2
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
r : ℝ
hr1 : r > 0
hr2 : ball t₀ r ⊆ f ⁻¹' s
t : ℝ
ht : t ∈ Ioo (t₀ - min r ε) (t₀ + min r ε)
⊢ t ∈ ball t₀ r
[PROOFSTEP]
apply Set.mem_of_mem_of_subset ht
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
r : ℝ
hr1 : r > 0
hr2 : ball t₀ r ⊆ f ⁻¹' s
t : ℝ
ht : t ∈ Ioo (t₀ - min r ε) (t₀ + min r ε)
⊢ Ioo (t₀ - min r ε) (t₀ + min r ε) ⊆ ball t₀ r
[PROOFSTEP]
rw [← Real.ball_eq_Ioo]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
r : ℝ
hr1 : r > 0
hr2 : ball t₀ r ⊆ f ⁻¹' s
t : ℝ
ht : t ∈ Ioo (t₀ - min r ε) (t₀ + min r ε)
⊢ ball t₀ (min r ε) ⊆ ball t₀ r
[PROOFSTEP]
exact Metric.ball_subset_ball (min_le_left _ _)


[GOAL]
⊢ NoncompactSpace ℍ
[PROOFSTEP]
refine' ⟨fun h => _⟩
[GOAL]
h : IsCompact univ
⊢ False
[PROOFSTEP]
have : IsCompact (Complex.im ⁻¹' Ioi 0) := isCompact_iff_isCompact_univ.2 h
[GOAL]
h : IsCompact univ
this : IsCompact (Complex.im ⁻¹' Ioi 0)
⊢ False
[PROOFSTEP]
replace := this.isClosed.closure_eq
[GOAL]
h : IsCompact univ
this : closure (Complex.im ⁻¹' Ioi 0) = Complex.im ⁻¹' Ioi 0
⊢ False
[PROOFSTEP]
rw [closure_preimage_im, closure_Ioi, Set.ext_iff] at this
[GOAL]
h : IsCompact univ
this : ∀ (x : ℂ), x ∈ Complex.im ⁻¹' Ici 0 ↔ x ∈ Complex.im ⁻¹' Ioi 0
⊢ False
[PROOFSTEP]
exact absurd ((this 0).1 (@left_mem_Ici ℝ _ 0)) (@lt_irrefl ℝ _ 0)


[GOAL]
S : Set ℍ
⊢ S ∈ atImInfty ↔ ∃ A, ∀ (z : ℍ), A ≤ im z → z ∈ S
[PROOFSTEP]
simp only [atImInfty_basis.mem_iff, true_and]
[GOAL]
S : Set ℍ
⊢ (∃ i, im ⁻¹' Set.Ici i ⊆ S) ↔ ∃ A, ∀ (z : ℍ), A ≤ im z → z ∈ S
[PROOFSTEP]
rfl
[GOAL]
f g : ℍ → ℂ
hf : IsBoundedAtImInfty f
hg : IsBoundedAtImInfty g
⊢ IsBoundedAtImInfty (f * g)
[PROOFSTEP]
simpa only [Pi.one_apply, mul_one, norm_eq_abs] using hf.mul hg
[GOAL]
f : ℍ → ℂ
⊢ IsBoundedAtImInfty f ↔ ∃ M A, ∀ (z : ℍ), A ≤ im z → ↑Complex.abs (f z) ≤ M
[PROOFSTEP]
simp [IsBoundedAtImInfty, BoundedAtFilter, Asymptotics.isBigO_iff, Filter.Eventually, atImInfty_mem]
[GOAL]
f : ℍ → ℂ
⊢ (∀ (ib : ℝ), 0 < ib → ∃ ia, True ∧ ∀ (x : ℍ), x ∈ im ⁻¹' Set.Ici ia → f x ∈ Metric.closedBall 0 ib) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ A, ∀ (z : ℍ), A ≤ im z → ↑Complex.abs (f z) ≤ ε
[PROOFSTEP]
simp only [true_and, mem_closedBall_zero_iff]
[GOAL]
f : ℍ → ℂ
⊢ (∀ (ib : ℝ), 0 < ib → ∃ ia, ∀ (x : ℍ), x ∈ im ⁻¹' Set.Ici ia → ‖f x‖ ≤ ib) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ A, ∀ (z : ℍ), A ≤ im z → ↑Complex.abs (f z) ≤ ε
[PROOFSTEP]
rfl


[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
⊢ ‖cderiv r f z‖ ≤ M / r
[PROOFSTEP]
have hM : 0 ≤ M := by
  obtain ⟨w, hw⟩ : (sphere z r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le
  exact (norm_nonneg _).trans (hf w hw)
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
⊢ 0 ≤ M
[PROOFSTEP]
obtain ⟨w, hw⟩ : (sphere z r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le
[GOAL]
case intro
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
w : ℂ
hw : w ∈ sphere z r
⊢ 0 ≤ M
[PROOFSTEP]
exact (norm_nonneg _).trans (hf w hw)
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
hM : 0 ≤ M
⊢ ‖cderiv r f z‖ ≤ M / r
[PROOFSTEP]
have h1 : ∀ w ∈ sphere z r, ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2 :=
  by
  intro w hw
  simp only [mem_sphere_iff_norm, norm_eq_abs] at hw
  simp only [norm_smul, inv_mul_eq_div, hw, norm_eq_abs, map_inv₀, Complex.abs_pow]
  exact div_le_div hM (hf w hw) (sq_pos_of_pos hr) le_rfl
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
hM : 0 ≤ M
⊢ ∀ (w : ℂ), w ∈ sphere z r → ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2
[PROOFSTEP]
intro w hw
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
hM : 0 ≤ M
w : ℂ
hw : w ∈ sphere z r
⊢ ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2
[PROOFSTEP]
simp only [mem_sphere_iff_norm, norm_eq_abs] at hw
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
hM : 0 ≤ M
w : ℂ
hw : ↑abs (w - z) = r
⊢ ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2
[PROOFSTEP]
simp only [norm_smul, inv_mul_eq_div, hw, norm_eq_abs, map_inv₀, Complex.abs_pow]
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
hM : 0 ≤ M
w : ℂ
hw : ↑abs (w - z) = r
⊢ ‖f w‖ / r ^ 2 ≤ M / r ^ 2
[PROOFSTEP]
exact div_le_div hM (hf w hw) (sq_pos_of_pos hr) le_rfl
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
hM : 0 ≤ M
h1 : ∀ (w : ℂ), w ∈ sphere z r → ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2
⊢ ‖cderiv r f z‖ ≤ M / r
[PROOFSTEP]
have h2 := circleIntegral.norm_integral_le_of_norm_le_const hr.le h1
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
hM : 0 ≤ M
h1 : ∀ (w : ℂ), w ∈ sphere z r → ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2
h2 : ‖∮ (z_1 : ℂ) in C(z, r), ((z_1 - z) ^ 2)⁻¹ • f z_1‖ ≤ 2 * π * r * (M / r ^ 2)
⊢ ‖cderiv r f z‖ ≤ M / r
[PROOFSTEP]
simp only [cderiv, norm_smul]
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
hM : 0 ≤ M
h1 : ∀ (w : ℂ), w ∈ sphere z r → ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2
h2 : ‖∮ (z_1 : ℂ) in C(z, r), ((z_1 - z) ^ 2)⁻¹ • f z_1‖ ≤ 2 * π * r * (M / r ^ 2)
⊢ ‖(2 * ↑π * I)⁻¹‖ * ‖∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r
[PROOFSTEP]
refine' (mul_le_mul le_rfl h2 (norm_nonneg _) (norm_nonneg _)).trans (le_of_eq _)
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
hM : 0 ≤ M
h1 : ∀ (w : ℂ), w ∈ sphere z r → ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2
h2 : ‖∮ (z_1 : ℂ) in C(z, r), ((z_1 - z) ^ 2)⁻¹ • f z_1‖ ≤ 2 * π * r * (M / r ^ 2)
⊢ ‖(2 * ↑π * I)⁻¹‖ * (2 * π * r * (M / r ^ 2)) = M / r
[PROOFSTEP]
field_simp [_root_.abs_of_nonneg Real.pi_pos.le, Real.pi_pos.ne.symm, hr.ne.symm]
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
hM : 0 ≤ M
h1 : ∀ (w : ℂ), w ∈ sphere z r → ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2
h2 : ‖∮ (z_1 : ℂ) in C(z, r), ((z_1 - z) ^ 2)⁻¹ • f z_1‖ ≤ 2 * π * r * (M / r ^ 2)
⊢ 2 * π * r * M * r = M * (2 * π * r ^ 2)
[PROOFSTEP]
ring
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
⊢ cderiv r (f - g) z = cderiv r f z - cderiv r g z
[PROOFSTEP]
have h1 : ContinuousOn (fun w : ℂ => ((w - z) ^ 2)⁻¹) (sphere z r) :=
  by
  refine' ((continuous_id'.sub continuous_const).pow 2).continuousOn.inv₀ fun w hw h => hr.ne _
  rwa [mem_sphere_iff_norm, sq_eq_zero_iff.mp h, norm_zero] at hw
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
⊢ ContinuousOn (fun w => ((w - z) ^ 2)⁻¹) (sphere z r)
[PROOFSTEP]
refine' ((continuous_id'.sub continuous_const).pow 2).continuousOn.inv₀ fun w hw h => hr.ne _
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
w : ℂ
hw : w ∈ sphere z r
h : (w - z) ^ 2 = 0
⊢ 0 = r
[PROOFSTEP]
rwa [mem_sphere_iff_norm, sq_eq_zero_iff.mp h, norm_zero] at hw
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
h1 : ContinuousOn (fun w => ((w - z) ^ 2)⁻¹) (sphere z r)
⊢ cderiv r (f - g) z = cderiv r f z - cderiv r g z
[PROOFSTEP]
simp_rw [cderiv, ← smul_sub]
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
h1 : ContinuousOn (fun w => ((w - z) ^ 2)⁻¹) (sphere z r)
⊢ ((2 * ↑π * I)⁻¹ • ∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • (f - g) w) =
    (2 * ↑π * I)⁻¹ • ((∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • f w) - ∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • g w)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
h1 : ContinuousOn (fun w => ((w - z) ^ 2)⁻¹) (sphere z r)
⊢ (∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • (f - g) w) =
    (∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • f w) - ∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • g w
[PROOFSTEP]
simpa only [Pi.sub_apply, smul_sub] using
  circleIntegral.integral_sub ((h1.smul hf).circleIntegrable hr.le) ((h1.smul hg).circleIntegrable hr.le)
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hfM : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
⊢ ‖cderiv r f z‖ < M / r
[PROOFSTEP]
obtain ⟨L, hL1, hL2⟩ : ∃ L < M, ∀ w ∈ sphere z r, ‖f w‖ ≤ L :=
  by
  have e1 : (sphere z r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le
  have e2 : ContinuousOn (fun w => ‖f w‖) (sphere z r) := continuous_norm.comp_continuousOn hf
  obtain ⟨x, hx, hx'⟩ := (isCompact_sphere z r).exists_forall_ge e1 e2
  exact ⟨‖f x‖, hfM x hx, hx'⟩
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hfM : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
⊢ ∃ L, L < M ∧ ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ L
[PROOFSTEP]
have e1 : (sphere z r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hfM : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
e1 : Set.Nonempty (sphere z r)
⊢ ∃ L, L < M ∧ ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ L
[PROOFSTEP]
have e2 : ContinuousOn (fun w => ‖f w‖) (sphere z r) := continuous_norm.comp_continuousOn hf
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hfM : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
e1 : Set.Nonempty (sphere z r)
e2 : ContinuousOn (fun w => ‖f w‖) (sphere z r)
⊢ ∃ L, L < M ∧ ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ L
[PROOFSTEP]
obtain ⟨x, hx, hx'⟩ := (isCompact_sphere z r).exists_forall_ge e1 e2
[GOAL]
case intro.intro
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hfM : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
e1 : Set.Nonempty (sphere z r)
e2 : ContinuousOn (fun w => ‖f w‖) (sphere z r)
x : ℂ
hx : x ∈ sphere z r
hx' : ∀ (y : ℂ), y ∈ sphere z r → ‖f y‖ ≤ ‖f x‖
⊢ ∃ L, L < M ∧ ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ L
[PROOFSTEP]
exact ⟨‖f x‖, hfM x hx, hx'⟩
[GOAL]
case intro.intro
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hfM : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
L : ℝ
hL1 : L < M
hL2 : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ L
⊢ ‖cderiv r f z‖ < M / r
[PROOFSTEP]
exact (norm_cderiv_le hr hL2).trans_lt ((div_lt_div_right hr).mpr hL1)
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hF : TendstoUniformlyOn F f φ (cthickening δ K)
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
⊢ TendstoUniformlyOn (Complex.cderiv δ ∘ F) (Complex.cderiv δ f) φ K
[PROOFSTEP]
rcases φ.eq_or_neBot with rfl | hne
[GOAL]
case inl
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
F : ι → ℂ → E
f g : ℂ → E
hδ : 0 < δ
hF : TendstoUniformlyOn F f ⊥ (cthickening δ K)
hFn : ∀ᶠ (n : ι) in ⊥, ContinuousOn (F n) (cthickening δ K)
⊢ TendstoUniformlyOn (cderiv δ ∘ F) (cderiv δ f) ⊥ K
[PROOFSTEP]
simp only [TendstoUniformlyOn, eventually_bot, imp_true_iff]
[GOAL]
case inr
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hF : TendstoUniformlyOn F f φ (cthickening δ K)
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : NeBot φ
⊢ TendstoUniformlyOn (Complex.cderiv δ ∘ F) (Complex.cderiv δ f) φ K
[PROOFSTEP]
have e1 : ContinuousOn f (cthickening δ K) := TendstoUniformlyOn.continuousOn hF hFn
[GOAL]
case inr
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hF : TendstoUniformlyOn F f φ (cthickening δ K)
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : NeBot φ
e1 : ContinuousOn f (cthickening δ K)
⊢ TendstoUniformlyOn (Complex.cderiv δ ∘ F) (Complex.cderiv δ f) φ K
[PROOFSTEP]
rw [tendstoUniformlyOn_iff] at hF ⊢
[GOAL]
case inr
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hF : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι) in φ, ∀ (x : ℂ), x ∈ cthickening δ K → dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : NeBot φ
e1 : ContinuousOn f (cthickening δ K)
⊢ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι) in φ, ∀ (x : ℂ), x ∈ K → dist (Complex.cderiv δ f x) ((Complex.cderiv δ ∘ F) n x) < ε
[PROOFSTEP]
rintro ε hε
[GOAL]
case inr
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hF : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι) in φ, ∀ (x : ℂ), x ∈ cthickening δ K → dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : NeBot φ
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (n : ι) in φ, ∀ (x : ℂ), x ∈ K → dist (Complex.cderiv δ f x) ((Complex.cderiv δ ∘ F) n x) < ε
[PROOFSTEP]
filter_upwards [hF (ε * δ) (mul_pos hε hδ), hFn] with n h h' z hz
[GOAL]
case h
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z✝ : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hF : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι) in φ, ∀ (x : ℂ), x ∈ cthickening δ K → dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : NeBot φ
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
n : ι
h : ∀ (x : ℂ), x ∈ cthickening δ K → dist (f x) (F n x) < ε * δ
h' : ContinuousOn (F n) (cthickening δ K)
z : ℂ
hz : z ∈ K
⊢ dist (Complex.cderiv δ f z) ((Complex.cderiv δ ∘ F) n z) < ε
[PROOFSTEP]
simp_rw [dist_eq_norm] at h ⊢
[GOAL]
case h
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z✝ : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hF : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι) in φ, ∀ (x : ℂ), x ∈ cthickening δ K → dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : NeBot φ
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
n : ι
h' : ContinuousOn (F n) (cthickening δ K)
z : ℂ
hz : z ∈ K
h : ∀ (x : ℂ), x ∈ cthickening δ K → ‖f x - F n x‖ < ε * δ
⊢ ‖Complex.cderiv δ f z - (Complex.cderiv δ ∘ F) n z‖ < ε
[PROOFSTEP]
have e2 : ∀ w ∈ sphere z δ, ‖f w - F n w‖ < ε * δ := fun w hw1 =>
  h w (closedBall_subset_cthickening hz δ (sphere_subset_closedBall hw1))
[GOAL]
case h
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z✝ : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hF : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι) in φ, ∀ (x : ℂ), x ∈ cthickening δ K → dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : NeBot φ
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
n : ι
h' : ContinuousOn (F n) (cthickening δ K)
z : ℂ
hz : z ∈ K
h : ∀ (x : ℂ), x ∈ cthickening δ K → ‖f x - F n x‖ < ε * δ
e2 : ∀ (w : ℂ), w ∈ sphere z δ → ‖f w - F n w‖ < ε * δ
⊢ ‖Complex.cderiv δ f z - (Complex.cderiv δ ∘ F) n z‖ < ε
[PROOFSTEP]
have e3 := sphere_subset_closedBall.trans (closedBall_subset_cthickening hz δ)
[GOAL]
case h
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z✝ : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hF : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι) in φ, ∀ (x : ℂ), x ∈ cthickening δ K → dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : NeBot φ
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
n : ι
h' : ContinuousOn (F n) (cthickening δ K)
z : ℂ
hz : z ∈ K
h : ∀ (x : ℂ), x ∈ cthickening δ K → ‖f x - F n x‖ < ε * δ
e2 : ∀ (w : ℂ), w ∈ sphere z δ → ‖f w - F n w‖ < ε * δ
e3 : sphere z δ ⊆ cthickening δ K
⊢ ‖Complex.cderiv δ f z - (Complex.cderiv δ ∘ F) n z‖ < ε
[PROOFSTEP]
have hf : ContinuousOn f (sphere z δ) := e1.mono (sphere_subset_closedBall.trans (closedBall_subset_cthickening hz δ))
[GOAL]
case h
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z✝ : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hF : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι) in φ, ∀ (x : ℂ), x ∈ cthickening δ K → dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : NeBot φ
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
n : ι
h' : ContinuousOn (F n) (cthickening δ K)
z : ℂ
hz : z ∈ K
h : ∀ (x : ℂ), x ∈ cthickening δ K → ‖f x - F n x‖ < ε * δ
e2 : ∀ (w : ℂ), w ∈ sphere z δ → ‖f w - F n w‖ < ε * δ
e3 : sphere z δ ⊆ cthickening δ K
hf : ContinuousOn f (sphere z δ)
⊢ ‖Complex.cderiv δ f z - (Complex.cderiv δ ∘ F) n z‖ < ε
[PROOFSTEP]
simpa only [mul_div_cancel _ hδ.ne.symm] using norm_cderiv_sub_lt hδ e2 hf (h'.mono e3)
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
⊢ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
[PROOFSTEP]
have h1 : ∀ᶠ n in φ, ContinuousOn (F n) (cthickening δ K) := by
  filter_upwards [hF] with n h using h.continuousOn.mono hKU
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
⊢ ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
[PROOFSTEP]
filter_upwards [hF] with n h using h.continuousOn.mono hKU
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
h1 : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
⊢ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
[PROOFSTEP]
have h2 : IsCompact (cthickening δ K) := isCompact_of_isClosed_bounded isClosed_cthickening hK.bounded.cthickening
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
h1 : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
h2 : IsCompact (cthickening δ K)
⊢ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
[PROOFSTEP]
have h3 : TendstoUniformlyOn F f φ (cthickening δ K) :=
  (tendstoLocallyUniformlyOn_iff_forall_isCompact hU).mp hf (cthickening δ K) hKU h2
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
h1 : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
h2 : IsCompact (cthickening δ K)
h3 : TendstoUniformlyOn F f φ (cthickening δ K)
⊢ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
[PROOFSTEP]
apply (h3.cderiv hδ h1).congr
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
h1 : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
h2 : IsCompact (cthickening δ K)
h3 : TendstoUniformlyOn F f φ (cthickening δ K)
⊢ ∀ᶠ (n : ι) in φ, EqOn ((cderiv δ ∘ F) n) ((deriv ∘ F) n) K
[PROOFSTEP]
filter_upwards [hF] with n h z hz
[GOAL]
case h
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z✝ : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
h1 : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
h2 : IsCompact (cthickening δ K)
h3 : TendstoUniformlyOn F f φ (cthickening δ K)
n : ι
h : DifferentiableOn ℂ (F n) U
z : ℂ
hz : z ∈ K
⊢ (cderiv δ ∘ F) n z = (deriv ∘ F) n z
[PROOFSTEP]
exact cderiv_eq_deriv hU h hδ ((closedBall_subset_cthickening hz δ).trans hKU)
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∃ δ, δ > 0 ∧ cthickening δ K ⊆ U ∧ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
[PROOFSTEP]
obtain ⟨δ, hδ, hKδ⟩ := hK.exists_cthickening_subset_open hU hKU
[GOAL]
case intro.intro
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
δ : ℝ
hδ : 0 < δ
hKδ : cthickening δ K ⊆ U
⊢ ∃ δ, δ > 0 ∧ cthickening δ K ⊆ U ∧ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
[PROOFSTEP]
exact ⟨δ, hδ, hKδ, tendstoUniformlyOn_deriv_of_cthickening_subset hf hF hδ hK hU hKδ⟩
[GOAL]
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
⊢ DifferentiableOn ℂ f U
[PROOFSTEP]
rintro x hx
[GOAL]
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
⊢ DifferentiableWithinAt ℂ f U x
[PROOFSTEP]
obtain ⟨K, ⟨hKx, hK⟩, hKU⟩ := (compact_basis_nhds x).mem_iff.mp (hU.mem_nhds hx)
[GOAL]
case intro.intro.intro
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
⊢ DifferentiableWithinAt ℂ f U x
[PROOFSTEP]
obtain ⟨δ, _, _, h1⟩ := exists_cthickening_tendstoUniformlyOn hf hF hK hU hKU
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left✝¹ : δ > 0
left✝ : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
⊢ DifferentiableWithinAt ℂ f U x
[PROOFSTEP]
have h2 : interior K ⊆ U := interior_subset.trans hKU
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left✝¹ : δ > 0
left✝ : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
⊢ DifferentiableWithinAt ℂ f U x
[PROOFSTEP]
have h3 : ∀ᶠ n in φ, DifferentiableOn ℂ (F n) (interior K)
[GOAL]
case h3
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left✝¹ : δ > 0
left✝ : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
⊢ ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
case intro.intro.intro.intro.intro.intro
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left✝¹ : δ > 0
left✝ : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
h3 : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
⊢ DifferentiableWithinAt ℂ f U x
[PROOFSTEP]
filter_upwards [hF] with n h using h.mono h2
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left✝¹ : δ > 0
left✝ : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
h3 : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
⊢ DifferentiableWithinAt ℂ f U x
[PROOFSTEP]
have h4 : TendstoLocallyUniformlyOn F f φ (interior K) := hf.mono h2
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left✝¹ : δ > 0
left✝ : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
h3 : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
h4 : TendstoLocallyUniformlyOn F f φ (interior K)
⊢ DifferentiableWithinAt ℂ f U x
[PROOFSTEP]
have h5 : TendstoLocallyUniformlyOn (deriv ∘ F) (cderiv δ f) φ (interior K) :=
  h1.tendstoLocallyUniformlyOn.mono interior_subset
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left✝¹ : δ > 0
left✝ : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
h3 : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
h4 : TendstoLocallyUniformlyOn F f φ (interior K)
h5 : TendstoLocallyUniformlyOn (deriv ∘ F) (cderiv δ f) φ (interior K)
⊢ DifferentiableWithinAt ℂ f U x
[PROOFSTEP]
have h6 : ∀ x ∈ interior K, HasDerivAt f (cderiv δ f x) x := fun x h =>
  hasDerivAt_of_tendsto_locally_uniformly_on' isOpen_interior h5 h3 (fun _ => h4.tendsto_at) h
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left✝¹ : δ > 0
left✝ : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
h3 : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
h4 : TendstoLocallyUniformlyOn F f φ (interior K)
h5 : TendstoLocallyUniformlyOn (deriv ∘ F) (cderiv δ f) φ (interior K)
h6 : ∀ (x : ℂ), x ∈ interior K → HasDerivAt f (cderiv δ f x) x
⊢ DifferentiableWithinAt ℂ f U x
[PROOFSTEP]
have h7 : DifferentiableOn ℂ f (interior K) := fun x hx => (h6 x hx).differentiableAt.differentiableWithinAt
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left✝¹ : δ > 0
left✝ : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
h3 : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
h4 : TendstoLocallyUniformlyOn F f φ (interior K)
h5 : TendstoLocallyUniformlyOn (deriv ∘ F) (cderiv δ f) φ (interior K)
h6 : ∀ (x : ℂ), x ∈ interior K → HasDerivAt f (cderiv δ f x) x
h7 : DifferentiableOn ℂ f (interior K)
⊢ DifferentiableWithinAt ℂ f U x
[PROOFSTEP]
exact (h7.differentiableAt (interior_mem_nhds.mpr hKx)).differentiableWithinAt
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
⊢ TendstoLocallyUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ U
[PROOFSTEP]
rw [tendstoLocallyUniformlyOn_iff_forall_isCompact hU]
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
⊢ ∀ (K : Set ℂ), K ⊆ U → IsCompact K → TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
[PROOFSTEP]
rcases φ.eq_or_neBot with rfl | hne
[GOAL]
case inl
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
F : ι → ℂ → E
f g : ℂ → E
hU : IsOpen U
hf : TendstoLocallyUniformlyOn F f ⊥ U
hF : ∀ᶠ (n : ι) in ⊥, DifferentiableOn ℂ (F n) U
⊢ ∀ (K : Set ℂ), K ⊆ U → IsCompact K → TendstoUniformlyOn (deriv ∘ F) (deriv f) ⊥ K
[PROOFSTEP]
simp only [TendstoUniformlyOn, eventually_bot, imp_true_iff]
[GOAL]
case inr
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
hne : NeBot φ
⊢ ∀ (K : Set ℂ), K ⊆ U → IsCompact K → TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
[PROOFSTEP]
rintro K hKU hK
[GOAL]
case inr
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
hne : NeBot φ
K : Set ℂ
hKU : K ⊆ U
hK : IsCompact K
⊢ TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
[PROOFSTEP]
obtain ⟨δ, hδ, hK4, h⟩ := exists_cthickening_tendstoUniformlyOn hf hF hK hU hKU
[GOAL]
case inr.intro.intro.intro
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
hne : NeBot φ
K : Set ℂ
hKU : K ⊆ U
hK : IsCompact K
δ : ℝ
hδ : δ > 0
hK4 : cthickening δ K ⊆ U
h : TendstoUniformlyOn (_root_.deriv ∘ F) (cderiv δ f) φ K
⊢ TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
[PROOFSTEP]
refine' h.congr_right fun z hz => cderiv_eq_deriv hU (hf.differentiableOn hF hU) hδ _
[GOAL]
case inr.intro.intro.intro
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K✝ : Set ℂ
z✝ : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
hne : NeBot φ
K : Set ℂ
hKU : K ⊆ U
hK : IsCompact K
δ : ℝ
hδ : δ > 0
hK4 : cthickening δ K ⊆ U
h : TendstoUniformlyOn (_root_.deriv ∘ F) (cderiv δ f) φ K
z : ℂ
hz : z ∈ K
⊢ closedBall z δ ⊆ U
[PROOFSTEP]
exact (closedBall_subset_cthickening hz δ).trans hK4
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
⊢ DifferentiableOn ℂ (fun w => ∑' (i : ι), F i w) U
[PROOFSTEP]
classical
have hc := (tendstoUniformlyOn_tsum hu hF_le).tendstoLocallyUniformlyOn
refine' hc.differentiableOn (eventually_of_forall fun s => _) hU
exact DifferentiableOn.sum fun i _ => hf i
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
⊢ DifferentiableOn ℂ (fun w => ∑' (i : ι), F i w) U
[PROOFSTEP]
have hc := (tendstoUniformlyOn_tsum hu hF_le).tendstoLocallyUniformlyOn
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
hc : TendstoLocallyUniformlyOn (fun t x => Finset.sum t fun n => F n x) (fun x => ∑' (n : ι), F n x) atTop U
⊢ DifferentiableOn ℂ (fun w => ∑' (i : ι), F i w) U
[PROOFSTEP]
refine' hc.differentiableOn (eventually_of_forall fun s => _) hU
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
hc : TendstoLocallyUniformlyOn (fun t x => Finset.sum t fun n => F n x) (fun x => ∑' (n : ι), F n x) atTop U
s : Finset ι
⊢ DifferentiableOn ℂ (fun x => Finset.sum s fun n => F n x) U
[PROOFSTEP]
exact DifferentiableOn.sum fun i _ => hf i
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
hz : z ∈ U
⊢ HasSum (fun i => deriv (F i) z) (deriv (fun w => ∑' (i : ι), F i w) z)
[PROOFSTEP]
rw [HasSum]
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
hz : z ∈ U
⊢ Tendsto (fun s => Finset.sum s fun b => deriv (F b) z) atTop (𝓝 (deriv (fun w => ∑' (i : ι), F i w) z))
[PROOFSTEP]
have hc := (tendstoUniformlyOn_tsum hu hF_le).tendstoLocallyUniformlyOn
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
hz : z ∈ U
hc : TendstoLocallyUniformlyOn (fun t x => Finset.sum t fun n => F n x) (fun x => ∑' (n : ι), F n x) atTop U
⊢ Tendsto (fun s => Finset.sum s fun b => deriv (F b) z) atTop (𝓝 (deriv (fun w => ∑' (i : ι), F i w) z))
[PROOFSTEP]
convert (hc.deriv (eventually_of_forall fun s => DifferentiableOn.sum fun i _ => hf i) hU).tendsto_at hz using 1
[GOAL]
case h.e'_3
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
hz : z ∈ U
hc : TendstoLocallyUniformlyOn (fun t x => Finset.sum t fun n => F n x) (fun x => ∑' (n : ι), F n x) atTop U
⊢ (fun s => Finset.sum s fun b => deriv (F b) z) = fun i => (deriv ∘ fun t x => Finset.sum t fun n => F n x) i z
[PROOFSTEP]
ext1 s
[GOAL]
case h.e'_3.h
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
hz : z ∈ U
hc : TendstoLocallyUniformlyOn (fun t x => Finset.sum t fun n => F n x) (fun x => ∑' (n : ι), F n x) atTop U
s : Finset ι
⊢ (Finset.sum s fun b => deriv (F b) z) = (deriv ∘ fun t x => Finset.sum t fun n => F n x) s z
[PROOFSTEP]
exact (deriv_sum fun i _ => (hf i).differentiableAt (hU.mem_nhds hz)).symm