E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun h => h ^ 2
⊢ ↑(↑f'' w) v = ↑(↑f'' v) w
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
⊢ ↑(↑f'' w) v = ↑(↑f'' v) w
have A : (fun h : ℝ => h ^ 2 • (f'' w v - f'' v w)) =o[𝓝[>] 0] fun h => h ^ 2 := by
  convert (s_conv.isLittleO_alternate_sum_square hf xs hx h4v h4w).sub
    (s_conv.isLittleO_alternate_sum_square hf xs hx h4w h4v) using 1
  ext h
  simp only [add_comm, smul_add, smul_sub]
  abel
no goals
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun h => h ^ 2
B : (fun x => ↑(↑f'' w) v - ↑(↑f'' v) w) =o[𝓝[Ioi 0] 0] fun x => 1
⊢ ↑(↑f'' w) v = ↑(↑f'' v) w
simpa only [sub_eq_zero] using isLittleO_const_const_iff.1 B
case h.e'_7
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
⊢ (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) = fun x_1 =>
    f (x + x_1 • (2 • v + 2 • w)) + f (x + x_1 • (v + w)) - f (x + x_1 • (2 • v + w)) - f (x + x_1 • (v + 2 • w)) -
        x_1 ^ 2 • ↑(↑f'' v) w -
      (f (x + x_1 • (2 • w + 2 • v)) + f (x + x_1 • (w + v)) - f (x + x_1 • (2 • w + v)) - f (x + x_1 • (w + 2 • v)) -
        x_1 ^ 2 • ↑(↑f'' w) v)
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
⊢ (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun h => h ^ 2
convert (s_conv.isLittleO_alternate_sum_square hf xs hx h4v h4w).sub
  (s_conv.isLittleO_alternate_sum_square hf xs hx h4w h4v) using 1
case h.e'_7.h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
h : ℝ
⊢ h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w) =
    f (x + h • (2 • v + 2 • w)) + f (x + h • (v + w)) - f (x + h • (2 • v + w)) - f (x + h • (v + 2 • w)) -
        h ^ 2 • ↑(↑f'' v) w -
      (f (x + h • (2 • w + 2 • v)) + f (x + h • (w + v)) - f (x + h • (2 • w + v)) - f (x + h • (w + 2 • v)) -
        h ^ 2 • ↑(↑f'' w) v)
case h.e'_7
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
⊢ (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) = fun x_1 =>
    f (x + x_1 • (2 • v + 2 • w)) + f (x + x_1 • (v + w)) - f (x + x_1 • (2 • v + w)) - f (x + x_1 • (v + 2 • w)) -
        x_1 ^ 2 • ↑(↑f'' v) w -
      (f (x + x_1 • (2 • w + 2 • v)) + f (x + x_1 • (w + v)) - f (x + x_1 • (2 • w + v)) - f (x + x_1 • (w + 2 • v)) -
        x_1 ^ 2 • ↑(↑f'' w) v)
ext h
case h.e'_7.h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
h : ℝ
⊢ h ^ 2 • ↑(↑f'' w) v - h ^ 2 • ↑(↑f'' v) w =
    f (x + (h • v + h • w)) + f (x + (h • 2 • v + h • 2 • w)) - f (x + (h • w + h • 2 • v)) -
          f (x + (h • v + h • 2 • w)) -
        h ^ 2 • ↑(↑f'' v) w -
      (f (x + (h • v + h • w)) + f (x + (h • 2 • v + h • 2 • w)) - f (x + (h • v + h • 2 • w)) -
          f (x + (h • w + h • 2 • v)) -
        h ^ 2 • ↑(↑f'' w) v)
case h.e'_7.h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
h : ℝ
⊢ h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w) =
    f (x + h • (2 • v + 2 • w)) + f (x + h • (v + w)) - f (x + h • (2 • v + w)) - f (x + h • (v + 2 • w)) -
        h ^ 2 • ↑(↑f'' v) w -
      (f (x + h • (2 • w + 2 • v)) + f (x + h • (w + v)) - f (x + h • (2 • w + v)) - f (x + h • (w + 2 • v)) -
        h ^ 2 • ↑(↑f'' w) v)
simp only [add_comm, smul_add, smul_sub]
no goals
case h.e'_7.h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
h : ℝ
⊢ h ^ 2 • ↑(↑f'' w) v - h ^ 2 • ↑(↑f'' v) w =
    f (x + (h • v + h • w)) + f (x + (h • 2 • v + h • 2 • w)) - f (x + (h • w + h • 2 • v)) -
          f (x + (h • v + h • 2 • w)) -
        h ^ 2 • ↑(↑f'' v) w -
      (f (x + (h • v + h • w)) + f (x + (h • 2 • v + h • 2 • w)) - f (x + (h • v + h • 2 • w)) -
          f (x + (h • w + h • 2 • v)) -
        h ^ 2 • ↑(↑f'' w) v)
abel
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun h => h ^ 2
this : (fun h => 1 / h ^ 2) =O[𝓝[Ioi 0] 0] fun h => 1 / h ^ 2
⊢ (fun x => ↑(↑f'' w) v - ↑(↑f'' v) w) =o[𝓝[Ioi 0] 0] fun x => 1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun h => h ^ 2
⊢ (fun x => ↑(↑f'' w) v - ↑(↑f'' v) w) =o[𝓝[Ioi 0] 0] fun x => 1
have : (fun h : ℝ => 1 / h ^ 2) =O[𝓝[>] 0] fun h => 1 / h ^ 2 := isBigO_refl _ _
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun h => h ^ 2
this : (fun h => 1 / h ^ 2) =O[𝓝[Ioi 0] 0] fun h => 1 / h ^ 2
C : (fun x => (1 / x ^ 2) • x ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun x => (1 / x ^ 2) • x ^ 2
⊢ (fun x => ↑(↑f'' w) v - ↑(↑f'' v) w) =o[𝓝[Ioi 0] 0] fun x => 1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun h => h ^ 2
this : (fun h => 1 / h ^ 2) =O[𝓝[Ioi 0] 0] fun h => 1 / h ^ 2
⊢ (fun x => ↑(↑f'' w) v - ↑(↑f'' v) w) =o[𝓝[Ioi 0] 0] fun x => 1
have C := this.smul_isLittleO A
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun h => h ^ 2
this : (fun h => 1 / h ^ 2) =O[𝓝[Ioi 0] 0] fun h => 1 / h ^ 2
C : (fun x => (1 / x ^ 2) • x ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun x => (1 / x ^ 2) • x ^ 2
⊢ (fun x => (1 / x ^ 2) • x ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =ᶠ[𝓝[Ioi 0] 0] fun x => ↑(↑f'' w) v - ↑(↑f'' v) w

E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun h => h ^ 2
this : (fun h => 1 / h ^ 2) =O[𝓝[Ioi 0] 0] fun h => 1 / h ^ 2
C : (fun x => (1 / x ^ 2) • x ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun x => (1 / x ^ 2) • x ^ 2
⊢ (fun x => (1 / x ^ 2) • x ^ 2) =ᶠ[𝓝[Ioi 0] 0] fun x => 1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun h => h ^ 2
this : (fun h => 1 / h ^ 2) =O[𝓝[Ioi 0] 0] fun h => 1 / h ^ 2
C : (fun x => (1 / x ^ 2) • x ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun x => (1 / x ^ 2) • x ^ 2
⊢ (fun x => ↑(↑f'' w) v - ↑(↑f'' v) w) =o[𝓝[Ioi 0] 0] fun x => 1
apply C.congr' _ _
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun h => h ^ 2
this : (fun h => 1 / h ^ 2) =O[𝓝[Ioi 0] 0] fun h => 1 / h ^ 2
C : (fun x => (1 / x ^ 2) • x ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun x => (1 / x ^ 2) • x ^ 2
⊢ ∀ (a : ℝ), a ∈ Ioi 0 → (1 / a ^ 2) • a ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w) = ↑(↑f'' w) v - ↑(↑f'' v) w
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun h => h ^ 2
this : (fun h => 1 / h ^ 2) =O[𝓝[Ioi 0] 0] fun h => 1 / h ^ 2
C : (fun x => (1 / x ^ 2) • x ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun x => (1 / x ^ 2) • x ^ 2
⊢ (fun x => (1 / x ^ 2) • x ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =ᶠ[𝓝[Ioi 0] 0] fun x => ↑(↑f'' w) v - ↑(↑f'' v) w
filter_upwards [self_mem_nhdsWithin]
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun h => h ^ 2
this : (fun h => 1 / h ^ 2) =O[𝓝[Ioi 0] 0] fun h => 1 / h ^ 2
C : (fun x => (1 / x ^ 2) • x ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun x => (1 / x ^ 2) • x ^ 2
h : ℝ
hpos : 0 < h
⊢ (1 / h ^ 2) • h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w) = ↑(↑f'' w) v - ↑(↑f'' v) w
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun h => h ^ 2
this : (fun h => 1 / h ^ 2) =O[𝓝[Ioi 0] 0] fun h => 1 / h ^ 2
C : (fun x => (1 / x ^ 2) • x ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun x => (1 / x ^ 2) • x ^ 2
⊢ ∀ (a : ℝ), a ∈ Ioi 0 → (1 / a ^ 2) • a ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w) = ↑(↑f'' w) v - ↑(↑f'' v) w
intro h (hpos : 0 < h)
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun h => h ^ 2
this : (fun h => 1 / h ^ 2) =O[𝓝[Ioi 0] 0] fun h => 1 / h ^ 2
C : (fun x => (1 / x ^ 2) • x ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun x => (1 / x ^ 2) • x ^ 2
h : ℝ
hpos : 0 < h
⊢ (1 / h ^ 2 * h ^ 2 * 1) • (↑(↑f'' w) v - ↑(↑f'' v) w) = 1 • (↑(↑f'' w) v - ↑(↑f'' v) w)
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun h => h ^ 2
this : (fun h => 1 / h ^ 2) =O[𝓝[Ioi 0] 0] fun h => 1 / h ^ 2
C : (fun x => (1 / x ^ 2) • x ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun x => (1 / x ^ 2) • x ^ 2
h : ℝ
hpos : 0 < h
⊢ (1 / h ^ 2) • h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w) = ↑(↑f'' w) v - ↑(↑f'' v) w
rw [← one_smul ℝ (f'' w v - f'' v w), smul_smul, smul_smul]
case h.e_a
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun h => h ^ 2
this : (fun h => 1 / h ^ 2) =O[𝓝[Ioi 0] 0] fun h => 1 / h ^ 2
C : (fun x => (1 / x ^ 2) • x ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun x => (1 / x ^ 2) • x ^ 2
h : ℝ
hpos : 0 < h
⊢ 1 / h ^ 2 * h ^ 2 * 1 = 1
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun h => h ^ 2
this : (fun h => 1 / h ^ 2) =O[𝓝[Ioi 0] 0] fun h => 1 / h ^ 2
C : (fun x => (1 / x ^ 2) • x ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun x => (1 / x ^ 2) • x ^ 2
h : ℝ
hpos : 0 < h
⊢ (1 / h ^ 2 * h ^ 2 * 1) • (↑(↑f'' w) v - ↑(↑f'' v) w) = 1 • (↑(↑f'' w) v - ↑(↑f'' v) w)
congr 1
no goals
case h.e_a
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun h => h ^ 2
this : (fun h => 1 / h ^ 2) =O[𝓝[Ioi 0] 0] fun h => 1 / h ^ 2
C : (fun x => (1 / x ^ 2) • x ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun x => (1 / x ^ 2) • x ^ 2
h : ℝ
hpos : 0 < h
⊢ 1 / h ^ 2 * h ^ 2 * 1 = 1
field_simp [LT.lt.ne' hpos]
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun h => h ^ 2
this : (fun h => 1 / h ^ 2) =O[𝓝[Ioi 0] 0] fun h => 1 / h ^ 2
C : (fun x => (1 / x ^ 2) • x ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun x => (1 / x ^ 2) • x ^ 2
h : ℝ
hpos : 0 < h
⊢ (1 / h ^ 2) • h ^ 2 = 1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun h => h ^ 2
this : (fun h => 1 / h ^ 2) =O[𝓝[Ioi 0] 0] fun h => 1 / h ^ 2
C : (fun x => (1 / x ^ 2) • x ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun x => (1 / x ^ 2) • x ^ 2
⊢ (fun x => (1 / x ^ 2) • x ^ 2) =ᶠ[𝓝[Ioi 0] 0] fun x => 1
filter_upwards [self_mem_nhdsWithin] with h (hpos : 0 < h)
no goals
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ (x : E), x ∈ interior s → HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h => h ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun h => h ^ 2
this : (fun h => 1 / h ^ 2) =O[𝓝[Ioi 0] 0] fun h => 1 / h ^ 2
C : (fun x => (1 / x ^ 2) • x ^ 2 • (↑(↑f'' w) v - ↑(↑f'' v) w)) =o[𝓝[Ioi 0] 0] fun x => (1 / x ^ 2) • x ^ 2
h : ℝ
hpos : 0 < h
⊢ (1 / h ^ 2) • h ^ 2 = 1
field_simp [LT.lt.ne' hpos, SMul.smul]