[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
⊢ HasFDerivWithinAt f f' (closure s) x
[PROOFSTEP]
classical
  -- one can assume without loss of generality that `x` belongs to the closure of `s`, as the
      -- statement is empty otherwise
by_cases hx : x ∉ closure s
· rw [← closure_closure] at hx ; exact hasFDerivWithinAt_of_not_mem_closure hx
push_neg at hx
rw [HasFDerivWithinAt, HasFDerivAtFilter, Asymptotics.isLittleO_iff]
  /- One needs to show that `‖f y - f x - f' (y - x)‖ ≤ ε ‖y - x‖` for `y` close to `x` in
        `closure s`, where `ε` is an arbitrary positive constant. By continuity of the functions, it
        suffices to prove this for nearby points inside `s`. In a neighborhood of `x`, the derivative
        of `f` is arbitrarily close to `f'` by assumption. The mean value inequality completes the
        proof. -/
intro ε ε_pos
obtain ⟨δ, δ_pos, hδ⟩ : ∃ δ > 0, ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε := by
  simpa [dist_zero_right] using tendsto_nhdsWithin_nhds.1 h ε ε_pos
set B := ball x δ
suffices : ∀ y ∈ B ∩ closure s, ‖f y - f x - (f' y - f' x)‖ ≤ ε * ‖y - x‖
exact mem_nhdsWithin_iff.2 ⟨δ, δ_pos, fun y hy => by simpa using this y hy⟩
suffices ∀ p : E × E, p ∈ closure ((B ∩ s) ×ˢ (B ∩ s)) → ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
  by
  rw [closure_prod_eq] at this
  intro y y_in
  apply this ⟨x, y⟩
  have : B ∩ closure s ⊆ closure (B ∩ s) := isOpen_ball.inter_closure
  exact ⟨this ⟨mem_ball_self δ_pos, hx⟩, this y_in⟩
have key : ∀ p : E × E, p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖ :=
  by
  rintro ⟨u, v⟩ ⟨u_in, v_in⟩
  have conv : Convex ℝ (B ∩ s) := (convex_ball _ _).inter s_conv
  have diff : DifferentiableOn ℝ f (B ∩ s) := f_diff.mono (inter_subset_right _ _)
  have bound : ∀ z ∈ B ∩ s, ‖fderivWithin ℝ f (B ∩ s) z - f'‖ ≤ ε :=
    by
    intro z z_in
    have h := hδ z
    have : fderivWithin ℝ f (B ∩ s) z = fderiv ℝ f z :=
      by
      have op : IsOpen (B ∩ s) := isOpen_ball.inter s_open
      rw [DifferentiableAt.fderivWithin _ (op.uniqueDiffOn z z_in)]
      exact (diff z z_in).differentiableAt (IsOpen.mem_nhds op z_in)
    rw [← this] at h
    exact (le_of_lt (h z_in.2 z_in.1))
  simpa using conv.norm_image_sub_le_of_norm_fderivWithin_le' diff bound u_in v_in
rintro ⟨u, v⟩ uv_in
refine' ContinuousWithinAt.closure_le uv_in _ _ key
have f_cont' : ∀ y ∈ closure s, ContinuousWithinAt (f - ⇑f') s y :=
  by
  intro y y_in
  exact Tendsto.sub (f_cont y y_in) f'.cont.continuousWithinAt
all_goals
  -- common start for both continuity proofs
  have : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s := by mono <;> exact inter_subset_right _ _
  obtain ⟨u_in, v_in⟩ : u ∈ closure s ∧ v ∈ closure s := by simpa [closure_prod_eq] using closure_mono this uv_in
  apply ContinuousWithinAt.mono _ this
  simp only [ContinuousWithinAt]
rw [nhdsWithin_prod_eq]
· have : ∀ u v, f v - f u - (f' v - f' u) = f v - f' v - (f u - f' u) := by intros; abel
  simp only [this]
  exact
    Tendsto.comp continuous_norm.continuousAt
      ((Tendsto.comp (f_cont' v v_in) tendsto_snd).sub <| Tendsto.comp (f_cont' u u_in) tendsto_fst)
· apply tendsto_nhdsWithin_of_tendsto_nhds
  rw [nhds_prod_eq]
  exact tendsto_const_nhds.mul (Tendsto.comp continuous_norm.continuousAt <| tendsto_snd.sub tendsto_fst)
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
⊢ HasFDerivWithinAt f f' (closure s) x
[PROOFSTEP]
by_cases hx : x ∉ closure s
[GOAL]
case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : ¬x ∈ closure s
⊢ HasFDerivWithinAt f f' (closure s) x
[PROOFSTEP]
rw [← closure_closure] at hx
[GOAL]
case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : ¬x ∈ closure (closure s)
⊢ HasFDerivWithinAt f f' (closure s) x
[PROOFSTEP]
exact hasFDerivWithinAt_of_not_mem_closure hx
[GOAL]
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : ¬¬x ∈ closure s
⊢ HasFDerivWithinAt f f' (closure s) x
[PROOFSTEP]
push_neg at hx
[GOAL]
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
⊢ HasFDerivWithinAt f f' (closure s) x
[PROOFSTEP]
rw [HasFDerivWithinAt, HasFDerivAtFilter, Asymptotics.isLittleO_iff]
  /- One needs to show that `‖f y - f x - f' (y - x)‖ ≤ ε ‖y - x‖` for `y` close to `x` in
        `closure s`, where `ε` is an arbitrary positive constant. By continuity of the functions, it
        suffices to prove this for nearby points inside `s`. In a neighborhood of `x`, the derivative
        of `f` is arbitrarily close to `f'` by assumption. The mean value inequality completes the
        proof. -/
[GOAL]
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[closure s] x, ‖f x_1 - f x - ↑f' (x_1 - x)‖ ≤ c * ‖x_1 - x‖
[PROOFSTEP]
intro ε ε_pos
[GOAL]
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
⊢ ∀ᶠ (x_1 : E) in 𝓝[closure s] x, ‖f x_1 - f x - ↑f' (x_1 - x)‖ ≤ ε * ‖x_1 - x‖
[PROOFSTEP]
obtain ⟨δ, δ_pos, hδ⟩ : ∃ δ > 0, ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε := by
  simpa [dist_zero_right] using tendsto_nhdsWithin_nhds.1 h ε ε_pos
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ δ, δ > 0 ∧ ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
[PROOFSTEP]
simpa [dist_zero_right] using tendsto_nhdsWithin_nhds.1 h ε ε_pos
[GOAL]
case neg.intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
⊢ ∀ᶠ (x_1 : E) in 𝓝[closure s] x, ‖f x_1 - f x - ↑f' (x_1 - x)‖ ≤ ε * ‖x_1 - x‖
[PROOFSTEP]
set B := ball x δ
[GOAL]
case neg.intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
⊢ ∀ᶠ (x_1 : E) in 𝓝[closure s] x, ‖f x_1 - f x - ↑f' (x_1 - x)‖ ≤ ε * ‖x_1 - x‖
[PROOFSTEP]
suffices : ∀ y ∈ B ∩ closure s, ‖f y - f x - (f' y - f' x)‖ ≤ ε * ‖y - x‖
[GOAL]
case neg.intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
this : ∀ (y : E), y ∈ B ∩ closure s → ‖f y - f x - (↑f' y - ↑f' x)‖ ≤ ε * ‖y - x‖
⊢ ∀ᶠ (x_1 : E) in 𝓝[closure s] x, ‖f x_1 - f x - ↑f' (x_1 - x)‖ ≤ ε * ‖x_1 - x‖
case this
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
⊢ ∀ (y : E), y ∈ B ∩ closure s → ‖f y - f x - (↑f' y - ↑f' x)‖ ≤ ε * ‖y - x‖
[PROOFSTEP]
exact mem_nhdsWithin_iff.2 ⟨δ, δ_pos, fun y hy => by simpa using this y hy⟩
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
this : ∀ (y : E), y ∈ B ∩ closure s → ‖f y - f x - (↑f' y - ↑f' x)‖ ≤ ε * ‖y - x‖
y : E
hy : y ∈ ball x δ ∩ closure s
⊢ y ∈ {x_1 | (fun x_2 => ‖f x_2 - f x - ↑f' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}
[PROOFSTEP]
simpa using this y hy
[GOAL]
case this
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
⊢ ∀ (y : E), y ∈ B ∩ closure s → ‖f y - f x - (↑f' y - ↑f' x)‖ ≤ ε * ‖y - x‖
[PROOFSTEP]
suffices ∀ p : E × E, p ∈ closure ((B ∩ s) ×ˢ (B ∩ s)) → ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
  by
  rw [closure_prod_eq] at this
  intro y y_in
  apply this ⟨x, y⟩
  have : B ∩ closure s ⊆ closure (B ∩ s) := isOpen_ball.inter_closure
  exact ⟨this ⟨mem_ball_self δ_pos, hx⟩, this y_in⟩
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
this :
  ∀ (p : E × E), p ∈ closure ((B ∩ s) ×ˢ (B ∩ s)) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
⊢ ∀ (y : E), y ∈ B ∩ closure s → ‖f y - f x - (↑f' y - ↑f' x)‖ ≤ ε * ‖y - x‖
[PROOFSTEP]
rw [closure_prod_eq] at this
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
this :
  ∀ (p : E × E),
    p ∈ closure (B ∩ s) ×ˢ closure (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
⊢ ∀ (y : E), y ∈ B ∩ closure s → ‖f y - f x - (↑f' y - ↑f' x)‖ ≤ ε * ‖y - x‖
[PROOFSTEP]
intro y y_in
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
this :
  ∀ (p : E × E),
    p ∈ closure (B ∩ s) ×ˢ closure (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
y : E
y_in : y ∈ B ∩ closure s
⊢ ‖f y - f x - (↑f' y - ↑f' x)‖ ≤ ε * ‖y - x‖
[PROOFSTEP]
apply this ⟨x, y⟩
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
this :
  ∀ (p : E × E),
    p ∈ closure (B ∩ s) ×ˢ closure (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
y : E
y_in : y ∈ B ∩ closure s
⊢ (x, y) ∈ closure (B ∩ s) ×ˢ closure (B ∩ s)
[PROOFSTEP]
have : B ∩ closure s ⊆ closure (B ∩ s) := isOpen_ball.inter_closure
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
this✝ :
  ∀ (p : E × E),
    p ∈ closure (B ∩ s) ×ˢ closure (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
y : E
y_in : y ∈ B ∩ closure s
this : B ∩ closure s ⊆ closure (B ∩ s)
⊢ (x, y) ∈ closure (B ∩ s) ×ˢ closure (B ∩ s)
[PROOFSTEP]
exact ⟨this ⟨mem_ball_self δ_pos, hx⟩, this y_in⟩
[GOAL]
case this
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
⊢ ∀ (p : E × E), p ∈ closure ((B ∩ s) ×ˢ (B ∩ s)) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
[PROOFSTEP]
have key : ∀ p : E × E, p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖ :=
  by
  rintro ⟨u, v⟩ ⟨u_in, v_in⟩
  have conv : Convex ℝ (B ∩ s) := (convex_ball _ _).inter s_conv
  have diff : DifferentiableOn ℝ f (B ∩ s) := f_diff.mono (inter_subset_right _ _)
  have bound : ∀ z ∈ B ∩ s, ‖fderivWithin ℝ f (B ∩ s) z - f'‖ ≤ ε :=
    by
    intro z z_in
    have h := hδ z
    have : fderivWithin ℝ f (B ∩ s) z = fderiv ℝ f z :=
      by
      have op : IsOpen (B ∩ s) := isOpen_ball.inter s_open
      rw [DifferentiableAt.fderivWithin _ (op.uniqueDiffOn z z_in)]
      exact (diff z z_in).differentiableAt (IsOpen.mem_nhds op z_in)
    rw [← this] at h
    exact (le_of_lt (h z_in.2 z_in.1))
  simpa using conv.norm_image_sub_le_of_norm_fderivWithin_le' diff bound u_in v_in
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
⊢ ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
[PROOFSTEP]
rintro ⟨u, v⟩ ⟨u_in, v_in⟩
[GOAL]
case mk.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
u v : E
u_in : (u, v).fst ∈ B ∩ s
v_in : (u, v).snd ∈ B ∩ s
⊢ ‖f (u, v).snd - f (u, v).fst - (↑f' (u, v).snd - ↑f' (u, v).fst)‖ ≤ ε * ‖(u, v).snd - (u, v).fst‖
[PROOFSTEP]
have conv : Convex ℝ (B ∩ s) := (convex_ball _ _).inter s_conv
[GOAL]
case mk.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
u v : E
u_in : (u, v).fst ∈ B ∩ s
v_in : (u, v).snd ∈ B ∩ s
conv : Convex ℝ (B ∩ s)
⊢ ‖f (u, v).snd - f (u, v).fst - (↑f' (u, v).snd - ↑f' (u, v).fst)‖ ≤ ε * ‖(u, v).snd - (u, v).fst‖
[PROOFSTEP]
have diff : DifferentiableOn ℝ f (B ∩ s) := f_diff.mono (inter_subset_right _ _)
[GOAL]
case mk.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
u v : E
u_in : (u, v).fst ∈ B ∩ s
v_in : (u, v).snd ∈ B ∩ s
conv : Convex ℝ (B ∩ s)
diff : DifferentiableOn ℝ f (B ∩ s)
⊢ ‖f (u, v).snd - f (u, v).fst - (↑f' (u, v).snd - ↑f' (u, v).fst)‖ ≤ ε * ‖(u, v).snd - (u, v).fst‖
[PROOFSTEP]
have bound : ∀ z ∈ B ∩ s, ‖fderivWithin ℝ f (B ∩ s) z - f'‖ ≤ ε :=
  by
  intro z z_in
  have h := hδ z
  have : fderivWithin ℝ f (B ∩ s) z = fderiv ℝ f z :=
    by
    have op : IsOpen (B ∩ s) := isOpen_ball.inter s_open
    rw [DifferentiableAt.fderivWithin _ (op.uniqueDiffOn z z_in)]
    exact (diff z z_in).differentiableAt (IsOpen.mem_nhds op z_in)
  rw [← this] at h
  exact (le_of_lt (h z_in.2 z_in.1))
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
u v : E
u_in : (u, v).fst ∈ B ∩ s
v_in : (u, v).snd ∈ B ∩ s
conv : Convex ℝ (B ∩ s)
diff : DifferentiableOn ℝ f (B ∩ s)
⊢ ∀ (z : E), z ∈ B ∩ s → ‖fderivWithin ℝ f (B ∩ s) z - f'‖ ≤ ε
[PROOFSTEP]
intro z z_in
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
u v : E
u_in : (u, v).fst ∈ B ∩ s
v_in : (u, v).snd ∈ B ∩ s
conv : Convex ℝ (B ∩ s)
diff : DifferentiableOn ℝ f (B ∩ s)
z : E
z_in : z ∈ B ∩ s
⊢ ‖fderivWithin ℝ f (B ∩ s) z - f'‖ ≤ ε
[PROOFSTEP]
have h := hδ z
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h✝ : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
u v : E
u_in : (u, v).fst ∈ B ∩ s
v_in : (u, v).snd ∈ B ∩ s
conv : Convex ℝ (B ∩ s)
diff : DifferentiableOn ℝ f (B ∩ s)
z : E
z_in : z ∈ B ∩ s
h : z ∈ s → dist z x < δ → ‖fderiv ℝ f z - f'‖ < ε
⊢ ‖fderivWithin ℝ f (B ∩ s) z - f'‖ ≤ ε
[PROOFSTEP]
have : fderivWithin ℝ f (B ∩ s) z = fderiv ℝ f z :=
  by
  have op : IsOpen (B ∩ s) := isOpen_ball.inter s_open
  rw [DifferentiableAt.fderivWithin _ (op.uniqueDiffOn z z_in)]
  exact (diff z z_in).differentiableAt (IsOpen.mem_nhds op z_in)
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h✝ : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
u v : E
u_in : (u, v).fst ∈ B ∩ s
v_in : (u, v).snd ∈ B ∩ s
conv : Convex ℝ (B ∩ s)
diff : DifferentiableOn ℝ f (B ∩ s)
z : E
z_in : z ∈ B ∩ s
h : z ∈ s → dist z x < δ → ‖fderiv ℝ f z - f'‖ < ε
⊢ fderivWithin ℝ f (B ∩ s) z = fderiv ℝ f z
[PROOFSTEP]
have op : IsOpen (B ∩ s) := isOpen_ball.inter s_open
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h✝ : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
u v : E
u_in : (u, v).fst ∈ B ∩ s
v_in : (u, v).snd ∈ B ∩ s
conv : Convex ℝ (B ∩ s)
diff : DifferentiableOn ℝ f (B ∩ s)
z : E
z_in : z ∈ B ∩ s
h : z ∈ s → dist z x < δ → ‖fderiv ℝ f z - f'‖ < ε
op : IsOpen (B ∩ s)
⊢ fderivWithin ℝ f (B ∩ s) z = fderiv ℝ f z
[PROOFSTEP]
rw [DifferentiableAt.fderivWithin _ (op.uniqueDiffOn z z_in)]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h✝ : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
u v : E
u_in : (u, v).fst ∈ B ∩ s
v_in : (u, v).snd ∈ B ∩ s
conv : Convex ℝ (B ∩ s)
diff : DifferentiableOn ℝ f (B ∩ s)
z : E
z_in : z ∈ B ∩ s
h : z ∈ s → dist z x < δ → ‖fderiv ℝ f z - f'‖ < ε
op : IsOpen (B ∩ s)
⊢ DifferentiableAt ℝ f z
[PROOFSTEP]
exact (diff z z_in).differentiableAt (IsOpen.mem_nhds op z_in)
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h✝ : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
u v : E
u_in : (u, v).fst ∈ B ∩ s
v_in : (u, v).snd ∈ B ∩ s
conv : Convex ℝ (B ∩ s)
diff : DifferentiableOn ℝ f (B ∩ s)
z : E
z_in : z ∈ B ∩ s
h : z ∈ s → dist z x < δ → ‖fderiv ℝ f z - f'‖ < ε
this : fderivWithin ℝ f (B ∩ s) z = fderiv ℝ f z
⊢ ‖fderivWithin ℝ f (B ∩ s) z - f'‖ ≤ ε
[PROOFSTEP]
rw [← this] at h
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h✝ : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
u v : E
u_in : (u, v).fst ∈ B ∩ s
v_in : (u, v).snd ∈ B ∩ s
conv : Convex ℝ (B ∩ s)
diff : DifferentiableOn ℝ f (B ∩ s)
z : E
z_in : z ∈ B ∩ s
h : z ∈ s → dist z x < δ → ‖fderivWithin ℝ f (B ∩ s) z - f'‖ < ε
this : fderivWithin ℝ f (B ∩ s) z = fderiv ℝ f z
⊢ ‖fderivWithin ℝ f (B ∩ s) z - f'‖ ≤ ε
[PROOFSTEP]
exact (le_of_lt (h z_in.2 z_in.1))
[GOAL]
case mk.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
u v : E
u_in : (u, v).fst ∈ B ∩ s
v_in : (u, v).snd ∈ B ∩ s
conv : Convex ℝ (B ∩ s)
diff : DifferentiableOn ℝ f (B ∩ s)
bound : ∀ (z : E), z ∈ B ∩ s → ‖fderivWithin ℝ f (B ∩ s) z - f'‖ ≤ ε
⊢ ‖f (u, v).snd - f (u, v).fst - (↑f' (u, v).snd - ↑f' (u, v).fst)‖ ≤ ε * ‖(u, v).snd - (u, v).fst‖
[PROOFSTEP]
simpa using conv.norm_image_sub_le_of_norm_fderivWithin_le' diff bound u_in v_in
[GOAL]
case this
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
⊢ ∀ (p : E × E), p ∈ closure ((B ∩ s) ×ˢ (B ∩ s)) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
[PROOFSTEP]
rintro ⟨u, v⟩ uv_in
[GOAL]
case this.mk
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
⊢ ‖f (u, v).snd - f (u, v).fst - (↑f' (u, v).snd - ↑f' (u, v).fst)‖ ≤ ε * ‖(u, v).snd - (u, v).fst‖
[PROOFSTEP]
refine' ContinuousWithinAt.closure_le uv_in _ _ key
[GOAL]
case this.mk.refine'_1
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
⊢ ContinuousWithinAt (fun y => ‖f y.snd - f y.fst - (↑f' y.snd - ↑f' y.fst)‖) ((B ∩ s) ×ˢ (B ∩ s)) (u, v)
case this.mk.refine'_2
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
⊢ ContinuousWithinAt (fun y => ε * ‖y.snd - y.fst‖) ((B ∩ s) ×ˢ (B ∩ s)) (u, v)
[PROOFSTEP]
have f_cont' : ∀ y ∈ closure s, ContinuousWithinAt (f - ⇑f') s y :=
  by
  intro y y_in
  exact Tendsto.sub (f_cont y y_in) f'.cont.continuousWithinAt
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
⊢ ∀ (y : E), y ∈ closure s → ContinuousWithinAt (f - ↑f') s y
[PROOFSTEP]
intro y y_in
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
y : E
y_in : y ∈ closure s
⊢ ContinuousWithinAt (f - ↑f') s y
[PROOFSTEP]
exact Tendsto.sub (f_cont y y_in) f'.cont.continuousWithinAt
[GOAL]
case this.mk.refine'_1
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ (y : E), y ∈ closure s → ContinuousWithinAt (f - ↑f') s y
⊢ ContinuousWithinAt (fun y => ‖f y.snd - f y.fst - (↑f' y.snd - ↑f' y.fst)‖) ((B ∩ s) ×ˢ (B ∩ s)) (u, v)
case this.mk.refine'_2
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
⊢ ContinuousWithinAt (fun y => ε * ‖y.snd - y.fst‖) ((B ∩ s) ×ˢ (B ∩ s)) (u, v)
[PROOFSTEP]
all_goals
  -- common start for both continuity proofs
  have : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s := by mono <;> exact inter_subset_right _ _
  obtain ⟨u_in, v_in⟩ : u ∈ closure s ∧ v ∈ closure s := by simpa [closure_prod_eq] using closure_mono this uv_in
  apply ContinuousWithinAt.mono _ this
  simp only [ContinuousWithinAt]
[GOAL]
case this.mk.refine'_1
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ (y : E), y ∈ closure s → ContinuousWithinAt (f - ↑f') s y
⊢ ContinuousWithinAt (fun y => ‖f y.snd - f y.fst - (↑f' y.snd - ↑f' y.fst)‖) ((B ∩ s) ×ˢ (B ∩ s)) (u, v)
[PROOFSTEP]
have : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s := by mono <;> exact inter_subset_right _ _
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ (y : E), y ∈ closure s → ContinuousWithinAt (f - ↑f') s y
⊢ (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
[PROOFSTEP]
mono
[GOAL]
case hs
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ (y : E), y ∈ closure s → ContinuousWithinAt (f - ↑f') s y
⊢ B ∩ s ⊆ s
[PROOFSTEP]
exact inter_subset_right _ _
[GOAL]
case ht
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ (y : E), y ∈ closure s → ContinuousWithinAt (f - ↑f') s y
⊢ B ∩ s ⊆ s
[PROOFSTEP]
exact inter_subset_right _ _
[GOAL]
case this.mk.refine'_1
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ (y : E), y ∈ closure s → ContinuousWithinAt (f - ↑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
⊢ ContinuousWithinAt (fun y => ‖f y.snd - f y.fst - (↑f' y.snd - ↑f' y.fst)‖) ((B ∩ s) ×ˢ (B ∩ s)) (u, v)
[PROOFSTEP]
obtain ⟨u_in, v_in⟩ : u ∈ closure s ∧ v ∈ closure s := by simpa [closure_prod_eq] using closure_mono this uv_in
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ (y : E), y ∈ closure s → ContinuousWithinAt (f - ↑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
⊢ u ∈ closure s ∧ v ∈ closure s
[PROOFSTEP]
simpa [closure_prod_eq] using closure_mono this uv_in
[GOAL]
case this.mk.refine'_1.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ (y : E), y ∈ closure s → ContinuousWithinAt (f - ↑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure s
v_in : v ∈ closure s
⊢ ContinuousWithinAt (fun y => ‖f y.snd - f y.fst - (↑f' y.snd - ↑f' y.fst)‖) ((B ∩ s) ×ˢ (B ∩ s)) (u, v)
[PROOFSTEP]
apply ContinuousWithinAt.mono _ this
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ (y : E), y ∈ closure s → ContinuousWithinAt (f - ↑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure s
v_in : v ∈ closure s
⊢ ContinuousWithinAt (fun y => ‖f y.snd - f y.fst - (↑f' y.snd - ↑f' y.fst)‖) (s ×ˢ s) (u, v)
[PROOFSTEP]
simp only [ContinuousWithinAt]
[GOAL]
case this.mk.refine'_2
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
⊢ ContinuousWithinAt (fun y => ε * ‖y.snd - y.fst‖) ((B ∩ s) ×ˢ (B ∩ s)) (u, v)
[PROOFSTEP]
have : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s := by mono <;> exact inter_subset_right _ _
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
⊢ (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
[PROOFSTEP]
mono
[GOAL]
case hs
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
⊢ B ∩ s ⊆ s
[PROOFSTEP]
exact inter_subset_right _ _
[GOAL]
case ht
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
⊢ B ∩ s ⊆ s
[PROOFSTEP]
exact inter_subset_right _ _
[GOAL]
case this.mk.refine'_2
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
⊢ ContinuousWithinAt (fun y => ε * ‖y.snd - y.fst‖) ((B ∩ s) ×ˢ (B ∩ s)) (u, v)
[PROOFSTEP]
obtain ⟨u_in, v_in⟩ : u ∈ closure s ∧ v ∈ closure s := by simpa [closure_prod_eq] using closure_mono this uv_in
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
⊢ u ∈ closure s ∧ v ∈ closure s
[PROOFSTEP]
simpa [closure_prod_eq] using closure_mono this uv_in
[GOAL]
case this.mk.refine'_2.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure s
v_in : v ∈ closure s
⊢ ContinuousWithinAt (fun y => ε * ‖y.snd - y.fst‖) ((B ∩ s) ×ˢ (B ∩ s)) (u, v)
[PROOFSTEP]
apply ContinuousWithinAt.mono _ this
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure s
v_in : v ∈ closure s
⊢ ContinuousWithinAt (fun y => ε * ‖y.snd - y.fst‖) (s ×ˢ s) (u, v)
[PROOFSTEP]
simp only [ContinuousWithinAt]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ (y : E), y ∈ closure s → ContinuousWithinAt (f - ↑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure s
v_in : v ∈ closure s
⊢ Tendsto (fun y => ‖f y.snd - f y.fst - (↑f' y.snd - ↑f' y.fst)‖) (𝓝[s ×ˢ s] (u, v)) (𝓝 ‖f v - f u - (↑f' v - ↑f' u)‖)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure s
v_in : v ∈ closure s
⊢ Tendsto (fun y => ε * ‖y.snd - y.fst‖) (𝓝[s ×ˢ s] (u, v)) (𝓝 (ε * ‖v - u‖))
[PROOFSTEP]
rw [nhdsWithin_prod_eq]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ (y : E), y ∈ closure s → ContinuousWithinAt (f - ↑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure s
v_in : v ∈ closure s
⊢ Tendsto (fun y => ‖f y.snd - f y.fst - (↑f' y.snd - ↑f' y.fst)‖) (𝓝[s] u ×ˢ 𝓝[s] v) (𝓝 ‖f v - f u - (↑f' v - ↑f' u)‖)
[PROOFSTEP]
have : ∀ u v, f v - f u - (f' v - f' u) = f v - f' v - (f u - f' u) := by intros; abel
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ (y : E), y ∈ closure s → ContinuousWithinAt (f - ↑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure s
v_in : v ∈ closure s
⊢ ∀ (u v : E), f v - f u - (↑f' v - ↑f' u) = f v - ↑f' v - (f u - ↑f' u)
[PROOFSTEP]
intros
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ (y : E), y ∈ closure s → ContinuousWithinAt (f - ↑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure s
v_in : v ∈ closure s
u✝ v✝ : E
⊢ f v✝ - f u✝ - (↑f' v✝ - ↑f' u✝) = f v✝ - ↑f' v✝ - (f u✝ - ↑f' u✝)
[PROOFSTEP]
abel
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ (y : E), y ∈ closure s → ContinuousWithinAt (f - ↑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure s
v_in : v ∈ closure s
u✝ v✝ : E
⊢ f v✝ - f u✝ - (↑f' v✝ - ↑f' u✝) = f v✝ - ↑f' v✝ - (f u✝ - ↑f' u✝)
[PROOFSTEP]
abel
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ (y : E), y ∈ closure s → ContinuousWithinAt (f - ↑f') s y
this✝ : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure s
v_in : v ∈ closure s
this : ∀ (u v : E), f v - f u - (↑f' v - ↑f' u) = f v - ↑f' v - (f u - ↑f' u)
⊢ Tendsto (fun y => ‖f y.snd - f y.fst - (↑f' y.snd - ↑f' y.fst)‖) (𝓝[s] u ×ˢ 𝓝[s] v) (𝓝 ‖f v - f u - (↑f' v - ↑f' u)‖)
[PROOFSTEP]
simp only [this]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ (y : E), y ∈ closure s → ContinuousWithinAt (f - ↑f') s y
this✝ : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure s
v_in : v ∈ closure s
this : ∀ (u v : E), f v - f u - (↑f' v - ↑f' u) = f v - ↑f' v - (f u - ↑f' u)
⊢ Tendsto (fun y => ‖f y.snd - ↑f' y.snd - (f y.fst - ↑f' y.fst)‖) (𝓝[s] u ×ˢ 𝓝[s] v) (𝓝 ‖f v - ↑f' v - (f u - ↑f' u)‖)
[PROOFSTEP]
exact
  Tendsto.comp continuous_norm.continuousAt
    ((Tendsto.comp (f_cont' v v_in) tendsto_snd).sub <| Tendsto.comp (f_cont' u u_in) tendsto_fst)
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure s
v_in : v ∈ closure s
⊢ Tendsto (fun y => ε * ‖y.snd - y.fst‖) (𝓝[s ×ˢ s] (u, v)) (𝓝 (ε * ‖v - u‖))
[PROOFSTEP]
apply tendsto_nhdsWithin_of_tendsto_nhds
[GOAL]
case h
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure s
v_in : v ∈ closure s
⊢ Tendsto (fun y => ε * ‖y.snd - y.fst‖) (𝓝 (u, v)) (𝓝 (ε * ‖v - u‖))
[PROOFSTEP]
rw [nhds_prod_eq]
[GOAL]
case h
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen s
f_cont : ∀ (y : E), y ∈ closure s → ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ (y : E), y ∈ s → dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ (p : E × E), p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.snd - f p.fst - (↑f' p.snd - ↑f' p.fst)‖ ≤ ε * ‖p.snd - p.fst‖
u v : E
uv_in : (u, v) ∈ closure ((B ∩ s) ×ˢ (B ∩ s))
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure s
v_in : v ∈ closure s
⊢ Tendsto (fun y => ε * ‖y.snd - y.fst‖) (𝓝 u ×ˢ 𝓝 v) (𝓝 (ε * ‖v - u‖))
[PROOFSTEP]
exact tendsto_const_nhds.mul (Tendsto.comp continuous_norm.continuousAt <| tendsto_snd.sub tendsto_fst)
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Ioi a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Ioi a] a) (𝓝 e)
⊢ HasDerivWithinAt f e (Ici a) a
[PROOFSTEP]
obtain ⟨b, ab : a < b, sab : Ioc a b ⊆ s⟩ := mem_nhdsWithin_Ioi_iff_exists_Ioc_subset.1 hs
[GOAL]
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Ioi a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Ioi a] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
⊢ HasDerivWithinAt f e (Ici a) a
[PROOFSTEP]
let t := Ioo a b
[GOAL]
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Ioi a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Ioi a] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
⊢ HasDerivWithinAt f e (Ici a) a
[PROOFSTEP]
have ts : t ⊆ s := Subset.trans Ioo_subset_Ioc_self sab
[GOAL]
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Ioi a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Ioi a] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
⊢ HasDerivWithinAt f e (Ici a) a
[PROOFSTEP]
have t_diff : DifferentiableOn ℝ f t := f_diff.mono ts
[GOAL]
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Ioi a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Ioi a] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
⊢ HasDerivWithinAt f e (Ici a) a
[PROOFSTEP]
have t_conv : Convex ℝ t := convex_Ioo a b
[GOAL]
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Ioi a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Ioi a] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
⊢ HasDerivWithinAt f e (Ici a) a
[PROOFSTEP]
have t_open : IsOpen t := isOpen_Ioo
[GOAL]
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Ioi a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Ioi a] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
⊢ HasDerivWithinAt f e (Ici a) a
[PROOFSTEP]
have t_closure : closure t = Icc a b := closure_Ioo ab.ne
[GOAL]
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Ioi a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Ioi a] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
⊢ HasDerivWithinAt f e (Ici a) a
[PROOFSTEP]
have t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y :=
  by
  rw [t_closure]
  intro y hy
  by_cases h : y = a
  · rw [h]; exact f_lim.mono ts
  · have : y ∈ s := sab ⟨lt_of_le_of_ne hy.1 (Ne.symm h), hy.2⟩
    exact (f_diff.continuousOn y this).mono ts
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Ioi a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Ioi a] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
⊢ ∀ (y : ℝ), y ∈ closure t → ContinuousWithinAt f t y
[PROOFSTEP]
rw [t_closure]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Ioi a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Ioi a] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
⊢ ∀ (y : ℝ), y ∈ Icc a b → ContinuousWithinAt f t y
[PROOFSTEP]
intro y hy
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Ioi a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Ioi a] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
y : ℝ
hy : y ∈ Icc a b
⊢ ContinuousWithinAt f t y
[PROOFSTEP]
by_cases h : y = a
[GOAL]
case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Ioi a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Ioi a] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
y : ℝ
hy : y ∈ Icc a b
h : y = a
⊢ ContinuousWithinAt f t y
[PROOFSTEP]
rw [h]
[GOAL]
case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Ioi a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Ioi a] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
y : ℝ
hy : y ∈ Icc a b
h : y = a
⊢ ContinuousWithinAt f t a
[PROOFSTEP]
exact f_lim.mono ts
[GOAL]
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Ioi a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Ioi a] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
y : ℝ
hy : y ∈ Icc a b
h : ¬y = a
⊢ ContinuousWithinAt f t y
[PROOFSTEP]
have : y ∈ s := sab ⟨lt_of_le_of_ne hy.1 (Ne.symm h), hy.2⟩
[GOAL]
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Ioi a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Ioi a] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
y : ℝ
hy : y ∈ Icc a b
h : ¬y = a
this : y ∈ s
⊢ ContinuousWithinAt f t y
[PROOFSTEP]
exact (f_diff.continuousOn y this).mono ts
[GOAL]
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Ioi a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Ioi a] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
t_cont : ∀ (y : ℝ), y ∈ closure t → ContinuousWithinAt f t y
⊢ HasDerivWithinAt f e (Ici a) a
[PROOFSTEP]
have t_diff' : Tendsto (fun x => fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight 1 e)) :=
  by
  simp only [deriv_fderiv.symm]
  exact
    Tendsto.comp (isBoundedBilinearMap_smulRight : IsBoundedBilinearMap ℝ _).continuous_right.continuousAt
      (tendsto_nhdsWithin_mono_left Ioo_subset_Ioi_self f_lim')
        -- now we can apply `has_fderiv_at_boundary_of_differentiable`
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Ioi a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Ioi a] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
t_cont : ∀ (y : ℝ), y ∈ closure t → ContinuousWithinAt f t y
⊢ Tendsto (fun x => fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight 1 e))
[PROOFSTEP]
simp only [deriv_fderiv.symm]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Ioi a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Ioi a] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
t_cont : ∀ (y : ℝ), y ∈ closure t → ContinuousWithinAt f t y
⊢ Tendsto (fun x => smulRight 1 (deriv f x)) (𝓝[Ioo a b] a) (𝓝 (smulRight 1 e))
[PROOFSTEP]
exact
  Tendsto.comp (isBoundedBilinearMap_smulRight : IsBoundedBilinearMap ℝ _).continuous_right.continuousAt
    (tendsto_nhdsWithin_mono_left Ioo_subset_Ioi_self f_lim')
      -- now we can apply `has_fderiv_at_boundary_of_differentiable`
[GOAL]
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Ioi a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Ioi a] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
t_cont : ∀ (y : ℝ), y ∈ closure t → ContinuousWithinAt f t y
t_diff' : Tendsto (fun x => fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight 1 e))
⊢ HasDerivWithinAt f e (Ici a) a
[PROOFSTEP]
have : HasDerivWithinAt f e (Icc a b) a :=
  by
  rw [hasDerivWithinAt_iff_hasFDerivWithinAt, ← t_closure]
  exact has_fderiv_at_boundary_of_tendsto_fderiv t_diff t_conv t_open t_cont t_diff'
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Ioi a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Ioi a] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
t_cont : ∀ (y : ℝ), y ∈ closure t → ContinuousWithinAt f t y
t_diff' : Tendsto (fun x => fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight 1 e))
⊢ HasDerivWithinAt f e (Icc a b) a
[PROOFSTEP]
rw [hasDerivWithinAt_iff_hasFDerivWithinAt, ← t_closure]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Ioi a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Ioi a] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
t_cont : ∀ (y : ℝ), y ∈ closure t → ContinuousWithinAt f t y
t_diff' : Tendsto (fun x => fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight 1 e))
⊢ HasFDerivWithinAt f (smulRight 1 e) (closure t) a
[PROOFSTEP]
exact has_fderiv_at_boundary_of_tendsto_fderiv t_diff t_conv t_open t_cont t_diff'
[GOAL]
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Ioi a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Ioi a] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
t_cont : ∀ (y : ℝ), y ∈ closure t → ContinuousWithinAt f t y
t_diff' : Tendsto (fun x => fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight 1 e))
this : HasDerivWithinAt f e (Icc a b) a
⊢ HasDerivWithinAt f e (Ici a) a
[PROOFSTEP]
exact this.nhdsWithin (Icc_mem_nhdsWithin_Ici <| left_mem_Ico.2 ab)
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Iio a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Iio a] a) (𝓝 e)
⊢ HasDerivWithinAt f e (Iic a) a
[PROOFSTEP]
obtain ⟨b, ba, sab⟩ : ∃ b ∈ Iio a, Ico b a ⊆ s := mem_nhdsWithin_Iio_iff_exists_Ico_subset.1 hs
[GOAL]
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Iio a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Iio a] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
⊢ HasDerivWithinAt f e (Iic a) a
[PROOFSTEP]
let t := Ioo b a
[GOAL]
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Iio a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Iio a] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
⊢ HasDerivWithinAt f e (Iic a) a
[PROOFSTEP]
have ts : t ⊆ s := Subset.trans Ioo_subset_Ico_self sab
[GOAL]
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Iio a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Iio a] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
⊢ HasDerivWithinAt f e (Iic a) a
[PROOFSTEP]
have t_diff : DifferentiableOn ℝ f t := f_diff.mono ts
[GOAL]
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Iio a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Iio a] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
⊢ HasDerivWithinAt f e (Iic a) a
[PROOFSTEP]
have t_conv : Convex ℝ t := convex_Ioo b a
[GOAL]
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Iio a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Iio a] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
⊢ HasDerivWithinAt f e (Iic a) a
[PROOFSTEP]
have t_open : IsOpen t := isOpen_Ioo
[GOAL]
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Iio a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Iio a] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
⊢ HasDerivWithinAt f e (Iic a) a
[PROOFSTEP]
have t_closure : closure t = Icc b a := closure_Ioo (ne_of_lt ba)
[GOAL]
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Iio a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Iio a] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
⊢ HasDerivWithinAt f e (Iic a) a
[PROOFSTEP]
have t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y :=
  by
  rw [t_closure]
  intro y hy
  by_cases h : y = a
  · rw [h]; exact f_lim.mono ts
  · have : y ∈ s := sab ⟨hy.1, lt_of_le_of_ne hy.2 h⟩
    exact (f_diff.continuousOn y this).mono ts
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Iio a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Iio a] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
⊢ ∀ (y : ℝ), y ∈ closure t → ContinuousWithinAt f t y
[PROOFSTEP]
rw [t_closure]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Iio a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Iio a] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
⊢ ∀ (y : ℝ), y ∈ Icc b a → ContinuousWithinAt f t y
[PROOFSTEP]
intro y hy
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Iio a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Iio a] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
y : ℝ
hy : y ∈ Icc b a
⊢ ContinuousWithinAt f t y
[PROOFSTEP]
by_cases h : y = a
[GOAL]
case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Iio a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Iio a] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
y : ℝ
hy : y ∈ Icc b a
h : y = a
⊢ ContinuousWithinAt f t y
[PROOFSTEP]
rw [h]
[GOAL]
case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Iio a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Iio a] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
y : ℝ
hy : y ∈ Icc b a
h : y = a
⊢ ContinuousWithinAt f t a
[PROOFSTEP]
exact f_lim.mono ts
[GOAL]
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Iio a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Iio a] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
y : ℝ
hy : y ∈ Icc b a
h : ¬y = a
⊢ ContinuousWithinAt f t y
[PROOFSTEP]
have : y ∈ s := sab ⟨hy.1, lt_of_le_of_ne hy.2 h⟩
[GOAL]
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Iio a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Iio a] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
y : ℝ
hy : y ∈ Icc b a
h : ¬y = a
this : y ∈ s
⊢ ContinuousWithinAt f t y
[PROOFSTEP]
exact (f_diff.continuousOn y this).mono ts
[GOAL]
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Iio a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Iio a] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
t_cont : ∀ (y : ℝ), y ∈ closure t → ContinuousWithinAt f t y
⊢ HasDerivWithinAt f e (Iic a) a
[PROOFSTEP]
have t_diff' : Tendsto (fun x => fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight 1 e)) :=
  by
  simp only [deriv_fderiv.symm]
  exact
    Tendsto.comp (isBoundedBilinearMap_smulRight : IsBoundedBilinearMap ℝ _).continuous_right.continuousAt
      (tendsto_nhdsWithin_mono_left Ioo_subset_Iio_self f_lim')
        -- now we can apply `has_fderiv_at_boundary_of_differentiable`
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Iio a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Iio a] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
t_cont : ∀ (y : ℝ), y ∈ closure t → ContinuousWithinAt f t y
⊢ Tendsto (fun x => fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight 1 e))
[PROOFSTEP]
simp only [deriv_fderiv.symm]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Iio a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Iio a] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
t_cont : ∀ (y : ℝ), y ∈ closure t → ContinuousWithinAt f t y
⊢ Tendsto (fun x => smulRight 1 (deriv f x)) (𝓝[Ioo b a] a) (𝓝 (smulRight 1 e))
[PROOFSTEP]
exact
  Tendsto.comp (isBoundedBilinearMap_smulRight : IsBoundedBilinearMap ℝ _).continuous_right.continuousAt
    (tendsto_nhdsWithin_mono_left Ioo_subset_Iio_self f_lim')
      -- now we can apply `has_fderiv_at_boundary_of_differentiable`
[GOAL]
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Iio a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Iio a] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
t_cont : ∀ (y : ℝ), y ∈ closure t → ContinuousWithinAt f t y
t_diff' : Tendsto (fun x => fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight 1 e))
⊢ HasDerivWithinAt f e (Iic a) a
[PROOFSTEP]
have : HasDerivWithinAt f e (Icc b a) a :=
  by
  rw [hasDerivWithinAt_iff_hasFDerivWithinAt, ← t_closure]
  exact has_fderiv_at_boundary_of_tendsto_fderiv t_diff t_conv t_open t_cont t_diff'
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Iio a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Iio a] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
t_cont : ∀ (y : ℝ), y ∈ closure t → ContinuousWithinAt f t y
t_diff' : Tendsto (fun x => fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight 1 e))
⊢ HasDerivWithinAt f e (Icc b a) a
[PROOFSTEP]
rw [hasDerivWithinAt_iff_hasFDerivWithinAt, ← t_closure]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Iio a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Iio a] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
t_cont : ∀ (y : ℝ), y ∈ closure t → ContinuousWithinAt f t y
t_diff' : Tendsto (fun x => fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight 1 e))
⊢ HasFDerivWithinAt f (smulRight 1 e) (closure t) a
[PROOFSTEP]
exact has_fderiv_at_boundary_of_tendsto_fderiv t_diff t_conv t_open t_cont t_diff'
[GOAL]
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[Iio a] a
f_lim' : Tendsto (fun x => deriv f x) (𝓝[Iio a] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
t_cont : ∀ (y : ℝ), y ∈ closure t → ContinuousWithinAt f t y
t_diff' : Tendsto (fun x => fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight 1 e))
this : HasDerivWithinAt f e (Icc b a) a
⊢ HasDerivWithinAt f e (Iic a) a
[PROOFSTEP]
exact this.nhdsWithin (Icc_mem_nhdsWithin_Iic <| right_mem_Ioc.2 ba)
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ HasDerivAt f (g x) x
[PROOFSTEP]
have A : HasDerivWithinAt f (g x) (Ici x) x :=
  by
  have diff : DifferentiableOn ℝ f (Ioi x) := fun y hy =>
    (f_diff y (ne_of_gt hy)).differentiableAt.differentiableWithinAt
  apply has_deriv_at_interval_left_endpoint_of_tendsto_deriv diff hf.continuousWithinAt self_mem_nhdsWithin
  have : Tendsto g (𝓝[>] x) (𝓝 (g x)) := tendsto_inf_left hg
  apply this.congr' _
  apply mem_of_superset self_mem_nhdsWithin fun y hy => _
  intros y hy
  exact (f_diff y (ne_of_gt hy)).deriv.symm
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ HasDerivWithinAt f (g x) (Ici x) x
[PROOFSTEP]
have diff : DifferentiableOn ℝ f (Ioi x) := fun y hy => (f_diff y (ne_of_gt hy)).differentiableAt.differentiableWithinAt
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
⊢ HasDerivWithinAt f (g x) (Ici x) x
[PROOFSTEP]
apply has_deriv_at_interval_left_endpoint_of_tendsto_deriv diff hf.continuousWithinAt self_mem_nhdsWithin
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
⊢ Tendsto (fun x => deriv f x) (𝓝[Ioi x] x) (𝓝 (g x))
[PROOFSTEP]
have : Tendsto g (𝓝[>] x) (𝓝 (g x)) := tendsto_inf_left hg
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
this : Tendsto g (𝓝[Ioi x] x) (𝓝 (g x))
⊢ Tendsto (fun x => deriv f x) (𝓝[Ioi x] x) (𝓝 (g x))
[PROOFSTEP]
apply this.congr' _
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
this : Tendsto g (𝓝[Ioi x] x) (𝓝 (g x))
⊢ g =ᶠ[𝓝[Ioi x] x] fun x => deriv f x
[PROOFSTEP]
apply mem_of_superset self_mem_nhdsWithin fun y hy => _
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
this : Tendsto g (𝓝[Ioi x] x) (𝓝 (g x))
⊢ ∀ (y : ℝ), y ∈ Ioi x → y ∈ {x | (fun x => g x = (fun x => deriv f x) x) x}
[PROOFSTEP]
intros y hy
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
this : Tendsto g (𝓝[Ioi x] x) (𝓝 (g x))
y : ℝ
hy : y ∈ Ioi x
⊢ y ∈ {x | (fun x => g x = (fun x => deriv f x) x) x}
[PROOFSTEP]
exact (f_diff y (ne_of_gt hy)).deriv.symm
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
⊢ HasDerivAt f (g x) x
[PROOFSTEP]
have B : HasDerivWithinAt f (g x) (Iic x) x :=
  by
  have diff : DifferentiableOn ℝ f (Iio x) := fun y hy =>
    (f_diff y (ne_of_lt hy)).differentiableAt.differentiableWithinAt
  apply has_deriv_at_interval_right_endpoint_of_tendsto_deriv diff hf.continuousWithinAt self_mem_nhdsWithin
  have : Tendsto g (𝓝[<] x) (𝓝 (g x)) := tendsto_inf_left hg
  apply this.congr' _
  apply mem_of_superset self_mem_nhdsWithin fun y hy => _
  intros y hy
  exact (f_diff y (ne_of_lt hy)).deriv.symm
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
⊢ HasDerivWithinAt f (g x) (Iic x) x
[PROOFSTEP]
have diff : DifferentiableOn ℝ f (Iio x) := fun y hy => (f_diff y (ne_of_lt hy)).differentiableAt.differentiableWithinAt
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
⊢ HasDerivWithinAt f (g x) (Iic x) x
[PROOFSTEP]
apply has_deriv_at_interval_right_endpoint_of_tendsto_deriv diff hf.continuousWithinAt self_mem_nhdsWithin
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
⊢ Tendsto (fun x => deriv f x) (𝓝[Iio x] x) (𝓝 (g x))
[PROOFSTEP]
have : Tendsto g (𝓝[<] x) (𝓝 (g x)) := tendsto_inf_left hg
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
this : Tendsto g (𝓝[Iio x] x) (𝓝 (g x))
⊢ Tendsto (fun x => deriv f x) (𝓝[Iio x] x) (𝓝 (g x))
[PROOFSTEP]
apply this.congr' _
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
this : Tendsto g (𝓝[Iio x] x) (𝓝 (g x))
⊢ g =ᶠ[𝓝[Iio x] x] fun x => deriv f x
[PROOFSTEP]
apply mem_of_superset self_mem_nhdsWithin fun y hy => _
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
this : Tendsto g (𝓝[Iio x] x) (𝓝 (g x))
⊢ ∀ (y : ℝ), y ∈ Iio x → y ∈ {x | (fun x => g x = (fun x => deriv f x) x) x}
[PROOFSTEP]
intros y hy
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
this : Tendsto g (𝓝[Iio x] x) (𝓝 (g x))
y : ℝ
hy : y ∈ Iio x
⊢ y ∈ {x | (fun x => g x = (fun x => deriv f x) x) x}
[PROOFSTEP]
exact (f_diff y (ne_of_lt hy)).deriv.symm
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
B : HasDerivWithinAt f (g x) (Iic x) x
⊢ HasDerivAt f (g x) x
[PROOFSTEP]
simpa using B.union A
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
y : ℝ
⊢ HasDerivAt f (g y) y
[PROOFSTEP]
rcases eq_or_ne y x with (rfl | hne)
[GOAL]
case inl
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : ℝ → E
y : ℝ
f_diff : ∀ (y_1 : ℝ), y_1 ≠ y → HasDerivAt f (g y_1) y_1
hf : ContinuousAt f y
hg : ContinuousAt g y
⊢ HasDerivAt f (g y) y
[PROOFSTEP]
exact hasDerivAt_of_hasDerivAt_of_ne f_diff hf hg
[GOAL]
case inr
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
y : ℝ
hne : y ≠ x
⊢ HasDerivAt f (g y) y
[PROOFSTEP]
exact f_diff y hne


[GOAL]
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
⊢ Tendsto (fun n => (↑n)⁻¹) atTop (nhds 0)
[PROOFSTEP]
convert tendsto_algebraMap_inverse_atTop_nhds_0_nat 𝕜
[GOAL]
case h.e'_3.h
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
x✝ : ℕ
⊢ (↑x✝)⁻¹ = (↑(algebraMap ℝ 𝕜) ∘ fun n => (↑n)⁻¹) x✝
[PROOFSTEP]
simp