𝕜 : Type u_2
E : Type u_1
E' : Type ?u.49605
F : Type ?u.49608
G : Type ?u.49611
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
⊢ y = ↑T x
𝕜 : Type u_2
E : Type u_1
E' : Type ?u.49605
F : Type ?u.49608
G : Type ?u.49611
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
⊢ Continuous ↑T
refine' T.continuous_of_seq_closed_graph fun u x y hu hTu => _
𝕜 : Type u_2
E : Type u_1
E' : Type ?u.49605
F : Type ?u.49608
G : Type ?u.49611
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
⊢ inner (y - ↑T x) (y - ↑T x) = 0
𝕜 : Type u_2
E : Type u_1
E' : Type ?u.49605
F : Type ?u.49608
G : Type ?u.49611
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
⊢ y = ↑T x
rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜]
𝕜 : Type u_2
E : Type u_1
E' : Type ?u.49605
F : Type ?u.49608
G : Type ?u.49611
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ inner (y - ↑T x) (y - ↑T x) = 0
𝕜 : Type u_2
E : Type u_1
E' : Type ?u.49605
F : Type ?u.49608
G : Type ?u.49611
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
⊢ inner (y - ↑T x) (y - ↑T x) = 0
have hlhs : ∀ k : ℕ, ⟪T (u k) - T x, y - T x⟫ = ⟪u k - x, T (y - T x)⟫ := by
  intro k
  rw [← T.map_sub, hT]
𝕜 : Type u_2
E : Type u_1
E' : Type ?u.49605
F : Type ?u.49608
G : Type ?u.49611
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ Filter.Tendsto (fun t => inner ((↑T ∘ u) t - ↑T x) (y - ↑T x)) Filter.atTop (nhds 0)
𝕜 : Type u_2
E : Type u_1
E' : Type ?u.49605
F : Type ?u.49608
G : Type ?u.49611
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ inner (y - ↑T x) (y - ↑T x) = 0
refine' tendsto_nhds_unique ((hTu.sub_const _).inner tendsto_const_nhds) _
𝕜 : Type u_2
E : Type u_1
E' : Type ?u.49605
F : Type ?u.49608
G : Type ?u.49611
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ Filter.Tendsto (fun t => inner (u t - x) (↑T (y - ↑T x))) Filter.atTop (nhds 0)
𝕜 : Type u_2
E : Type u_1
E' : Type ?u.49605
F : Type ?u.49608
G : Type ?u.49611
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ Filter.Tendsto (fun t => inner ((↑T ∘ u) t - ↑T x) (y - ↑T x)) Filter.atTop (nhds 0)
simp_rw [Function.comp_apply, hlhs]
𝕜 : Type u_2
E : Type u_1
E' : Type ?u.49605
F : Type ?u.49608
G : Type ?u.49611
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ Filter.Tendsto (fun t => inner (u t - x) (↑T (y - ↑T x))) Filter.atTop (nhds (inner 0 (↑T (y - ↑T x))))
𝕜 : Type u_2
E : Type u_1
E' : Type ?u.49605
F : Type ?u.49608
G : Type ?u.49611
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ Filter.Tendsto (fun t => inner (u t - x) (↑T (y - ↑T x))) Filter.atTop (nhds 0)
rw [← inner_zero_left (T (y - T x))]
𝕜 : Type u_2
E : Type u_1
E' : Type ?u.49605
F : Type ?u.49608
G : Type ?u.49611
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ Filter.Tendsto (fun t => u t - x) Filter.atTop (nhds 0)
𝕜 : Type u_2
E : Type u_1
E' : Type ?u.49605
F : Type ?u.49608
G : Type ?u.49611
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ Filter.Tendsto (fun t => inner (u t - x) (↑T (y - ↑T x))) Filter.atTop (nhds (inner 0 (↑T (y - ↑T x))))
refine' Filter.Tendsto.inner _ tendsto_const_nhds
𝕜 : Type u_2
E : Type u_1
E' : Type ?u.49605
F : Type ?u.49608
G : Type ?u.49611
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ Filter.Tendsto (fun t => u t - x) Filter.atTop (nhds (x - x))
𝕜 : Type u_2
E : Type u_1
E' : Type ?u.49605
F : Type ?u.49608
G : Type ?u.49611
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ Filter.Tendsto (fun t => u t - x) Filter.atTop (nhds 0)
rw [← sub_self x]
no goals
𝕜 : Type u_2
E : Type u_1
E' : Type ?u.49605
F : Type ?u.49608
G : Type ?u.49611
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ Filter.Tendsto (fun t => u t - x) Filter.atTop (nhds (x - x))
exact hu.sub_const _
𝕜 : Type u_2
E : Type u_1
E' : Type ?u.49605
F : Type ?u.49608
G : Type ?u.49611
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
k : ℕ
⊢ inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
𝕜 : Type u_2
E : Type u_1
E' : Type ?u.49605
F : Type ?u.49608
G : Type ?u.49611
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
⊢ ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
intro k
no goals
𝕜 : Type u_2
E : Type u_1
E' : Type ?u.49605
F : Type ?u.49608
G : Type ?u.49611
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
k : ℕ
⊢ inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
rw [← T.map_sub, hT]