ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>f : E ≃ₗ[𝕜] E'<VAR>v : Basis ι 𝕜 E<VAR>hv : Orthonormal 𝕜 ⇑v<VAR>hf : Orthonormal 𝕜 (⇑f ∘ ⇑v)<GOAL>⇑(f.isometryOfOrthonormal hv hf) = ⇑f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>f : E ≃ₗ[𝕜] E'<VAR>v : Basis ι 𝕜 E<VAR>hv : Orthonormal 𝕜 ⇑v<VAR>hf : Orthonormal 𝕜 (⇑f ∘ ⇑v)<GOAL>(f.isometryOfOrthonormal hv hf).toLinearEquiv = f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>v : Basis ι 𝕜 E<VAR>hv : Orthonormal 𝕜 ⇑v<VAR>v' : Basis ι' 𝕜 E'<VAR>hv' : Orthonormal 𝕜 ⇑v'<VAR>e : ι ≃ ι'<GOAL>(hv.equiv hv' e).toLinearEquiv = v.equiv v' e
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>ι' : Type u_9<VAR>v : Basis ι 𝕜 E<VAR>hv : Orthonormal 𝕜 ⇑v<VAR>v' : Basis ι' 𝕜 E'<VAR>hv' : Orthonormal 𝕜 ⇑v'<VAR>e : ι ≃ ι'<VAR>i : ι<GOAL>(hv.equiv hv' e) (v i) = v' (e i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>v : Basis ι 𝕜 E<VAR>hv : Orthonormal 𝕜 ⇑v<GOAL>hv.equiv hv (Equiv.refl ι) = LinearIsometryEquiv.refl 𝕜 E
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>v : Basis ι 𝕜 E<VAR>hv : Orthonormal 𝕜 ⇑v<VAR>v' : Basis ι' 𝕜 E'<VAR>hv' : Orthonormal 𝕜 ⇑v'<VAR>e : ι ≃ ι'<GOAL>(hv.equiv hv' e).symm = hv'.equiv hv e.symm
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>ι'' : Type u_6<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>E'' : Type u_8<VAR>NormedAddCommGroup E''<VAR>InnerProductSpace 𝕜 E''<VAR>v : Basis ι 𝕜 E<VAR>hv : Orthonormal 𝕜 ⇑v<VAR>v' : Basis ι' 𝕜 E'<VAR>hv' : Orthonormal 𝕜 ⇑v'<VAR>e : ι ≃ ι'<VAR>v'' : Basis ι'' 𝕜 E''<VAR>hv'' : Orthonormal 𝕜 ⇑v''<VAR>e' : ι' ≃ ι''<GOAL>(hv.equiv hv' e).trans (hv'.equiv hv'' e') = hv.equiv hv'' (e.trans e')
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>v : Basis ι 𝕜 E<VAR>hv : Orthonormal 𝕜 ⇑v<VAR>v' : Basis ι' 𝕜 E'<VAR>hv' : Orthonormal 𝕜 ⇑v'<VAR>e : ι ≃ ι'<GOAL>v.map (hv.equiv hv' e).toLinearEquiv = v'.reindex e.symm
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>⟪x, y⟫_ℝ = (‖x + y‖ * ‖x + y‖ - ‖x‖ * ‖x‖ - ‖y‖ * ‖y‖) / 2
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>⟪x, y⟫_ℝ = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ = 0
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>‖x + y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ ⟪x, y⟫_ℝ = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<VAR>h : ⟪x, y⟫_𝕜 = 0<GOAL>‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ = 0
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>‖x - y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ ⟪x, y⟫_ℝ = 0
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>⟪x + y, x - y⟫_ℝ = 0 ↔ ‖x‖ = ‖y‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>v w : E<VAR>h : ⟪v, w⟫_𝕜 = 0<GOAL>‖w - v‖ = ‖w + v‖
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>|⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)| ≤ 1
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x : F<VAR>r : ℝ<GOAL>⟪r • x, x⟫_ℝ = r * (‖x‖ * ‖x‖)
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x : F<VAR>r : ℝ<GOAL>⟪x, r • x⟫_ℝ = r * (‖x‖ * ‖x‖)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x : E<VAR>r : 𝕜<VAR>hx : x ≠ 0<VAR>hr : r ≠ 0<GOAL>‖⟪x, r • x⟫_𝕜‖ / (‖x‖ * ‖r • x‖) = 1
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x : F<VAR>r : ℝ<VAR>hx : x ≠ 0<VAR>hr : r ≠ 0<GOAL>|⟪x, r • x⟫_ℝ| / (‖x‖ * ‖r • x‖) = 1
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x : F<VAR>r : ℝ<VAR>hx : x ≠ 0<VAR>hr : 0 < r<GOAL>⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = 1
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x : F<VAR>r : ℝ<VAR>hx : x ≠ 0<VAR>hr : r < 0<GOAL>⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = -1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>[‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x, x = 0 ∨ ∃ r, y = r • x, x = 0 ∨ y ∈ Submodule.span 𝕜 {x}].TFAE
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<VAR>hx₀ : x ≠ 0<VAR>hy₀ : y ≠ 0<GOAL>‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖ ↔ ∃ r, r ≠ 0 ∧ y = r • x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>‖⟪x, y⟫_𝕜 / (↑‖x‖ * ↑‖y‖)‖ = 1 ↔ x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>|⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)| = 1 ↔ x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<VAR>h₀ : x ≠ 0<GOAL>⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖ ↔ (↑‖y‖ / ↑‖x‖) • x = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖ ↔ ↑‖y‖ • x = ↑‖x‖ • y
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>⟪x, y⟫_ℝ = ‖x‖ * ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1 ↔ x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = -1 ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<VAR>hx : ‖x‖ = 1<VAR>hy : ‖y‖ = 1<GOAL>⟪x, y⟫_𝕜 = 1 ↔ x = y
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>⟪x, y⟫_ℝ < ‖x‖ * ‖y‖ ↔ ‖y‖ • x ≠ ‖x‖ • y
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<VAR>hx : ‖x‖ = 1<VAR>hy : ‖y‖ = 1<GOAL>⟪x, y⟫_ℝ < 1 ↔ x ≠ y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<VAR>hle : ‖x‖ ≤ ‖y‖<VAR>h : RCLike.re ⟪x, y⟫_𝕜 = ‖y‖ ^ 2<GOAL>x = y
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>ι₁ : Type u_4<VAR>s₁ : Finset ι₁<VAR>w₁ : ι₁ → ℝ<VAR>v₁ : ι₁ → F<VAR>h₁ : ∑ i ∈ s₁, w₁ i = 0<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w₂ : ι₂ → ℝ<VAR>v₂ : ι₂ → F<VAR>h₂ : ∑ i ∈ s₂, w₂ i = 0<GOAL>⟪∑ i₁ ∈ s₁, w₁ i₁ • v₁ i₁, ∑ i₂ ∈ s₂, w₂ i₂ • v₂ i₂⟫_ℝ = (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>v : E<GOAL>⇑((innerₛₗ 𝕜) v) = fun w => ⟪v, w⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>v w : E<GOAL>((innerₛₗ 𝕜) v) w = ⟪v, w⟫_𝕜
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<GOAL>(innerₗ F).flip = innerₗ F
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>v w : F<GOAL>((innerₗ F) v) w = ⟪v, w⟫_ℝ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>v : E<GOAL>⇑((innerSL 𝕜) v) = fun w => ⟪v, w⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>v w : E<GOAL>((innerSL 𝕜) v) w = ⟪v, w⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x : E<GOAL>‖(innerSL 𝕜) x‖ = ‖x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<GOAL>‖innerSL 𝕜‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>((innerSLFlip 𝕜) x) y = ⟪y, x⟫_𝕜
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<GOAL>(innerSL ℝ).flip = innerSL ℝ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>E' : Type u_4<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>f : E →L[𝕜] E'<VAR>x : E'<GOAL>(ContinuousLinearMap.toSesqForm f) x = ((innerSL 𝕜) x).comp f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>E' : Type u_4<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>f : E →L[𝕜] E'<VAR>v : E'<GOAL>‖(ContinuousLinearMap.toSesqForm f) v‖ ≤ ‖f‖ * ‖v‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<GOAL>IsBoundedBilinearMap ℝ fun p => ⟪p.1, p.2⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>x : E<VAR>v : ι → E<VAR>s : Finset ι<VAR>hv : Orthonormal 𝕜 v<GOAL>∑ i ∈ s, ‖⟪v i, x⟫_𝕜‖ ^ 2 ≤ ‖x‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>x : E<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<GOAL>∑' (i : ι), ‖⟪v i, x⟫_𝕜‖ ^ 2 ≤ ‖x‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>x : E<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<GOAL>Summable fun i => ‖⟪v i, x⟫_𝕜‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>x y : 𝕜<GOAL>⟪x, y⟫_𝕜 = (starRingEnd 𝕜) x * y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>W : Submodule 𝕜 E<VAR>x y : ↥W<GOAL>⟪x, y⟫_𝕜 = ⟪↑x, ↑y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>s : Submodule 𝕜 E<VAR>hvs : ∀ (i : ι), v i ∈ s<GOAL>Orthonormal 𝕜 (Set.codRestrict v (↑s) hvs)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<GOAL>Orthonormal 𝕜 fun i => ⟨v i, ⋯⟩
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<GOAL>OrthogonalFamily 𝕜 (fun _i => 𝕜) fun i => LinearIsometry.toSpanSingleton 𝕜 E ⋯
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>G : ι → Type u_5<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>DecidableEq ι<VAR>i j : ι<VAR>v : G i<VAR>w : G j<GOAL>⟪(V i) v, (V j) w⟫_𝕜 = if i = j then ⟪(V i) v, (V j) w⟫_𝕜 else 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>G : ι → Type u_5<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)<VAR>DecidableEq ι<VAR>l : DirectSum ι fun i => G i<VAR>i : ι<VAR>v : G i<GOAL>⟪(V i) v, DFinsupp.sum l fun j => ⇑(V j)⟫_𝕜 = ⟪v, l i⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>G : ι → Type u_5<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>Fintype ι<VAR>l : (i : ι) → G i<VAR>i : ι<VAR>v : G i<GOAL>⟪(V i) v, ∑ j : ι, (V j) (l j)⟫_𝕜 = ⟪v, l i⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>G : ι → Type u_5<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>l₁ l₂ : (i : ι) → G i<VAR>s : Finset ι<GOAL>⟪∑ i ∈ s, (V i) (l₁ i), ∑ j ∈ s, (V j) (l₂ j)⟫_𝕜 = ∑ i ∈ s, ⟪l₁ i, l₂ i⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>G : ι → Type u_5<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>l : (i : ι) → G i<VAR>s : Finset ι<GOAL>‖∑ i ∈ s, (V i) (l i)‖ ^ 2 = ∑ i ∈ s, ‖l i‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>G : ι → Type u_5<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>γ : Type u_6<VAR>f : γ → ι<VAR>hf : Function.Injective f<GOAL>OrthogonalFamily 𝕜 (fun g => G (f g)) fun g => V (f g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>G : ι → Type u_5<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>α : ι → Type u_6<VAR>v_family : (i : ι) → α i → G i<VAR>hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)<GOAL>Orthonormal 𝕜 fun a => (V a.fst) (v_family a.fst a.snd)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>G : ι → Type u_5<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>DecidableEq ι<VAR>f : (i : ι) → G i<VAR>s₁ s₂ : Finset ι<GOAL>‖∑ i ∈ s₁, (V i) (f i) - ∑ i ∈ s₂, (V i) (f i)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖f i‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>G : ι → Type u_5<VAR>(i : ι) → NormedAddCommGroup (G i)<VAR>(i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>CompleteSpace E<VAR>f : (i : ι) → G i<GOAL>(Summable fun i => (V i) (f i)) ↔ Summable fun i => ‖f i‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>V : ι → Submodule 𝕜 E<VAR>hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ<GOAL>CompleteLattice.Independent V
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>V : ι → Submodule 𝕜 E<VAR>hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ<VAR>hV_sum : DirectSum.IsInternal fun i => V i<VAR>α : ι → Type u_6<VAR>v_family : (i : ι) → Basis (α i) 𝕜 ↥(V i)<VAR>hv_family : ∀ (i : ι), Orthonormal 𝕜 ⇑(v_family i)<GOAL>Orthonormal 𝕜 ⇑(hV_sum.collectedBasis v_family)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>⟪x, y⟫_ℝ = RCLike.re ⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x : E<GOAL>⟪x, RCLike.I • x⟫_ℝ = 0
<VAR>w z : ℂ<GOAL>⟪w, z⟫_ℝ = ((starRingEnd ℂ) w * z).re
<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>InnerProductSpace ℝ G<VAR>f : G ≃ₗᵢ[ℝ] ℂ<VAR>x y : G<GOAL>⟪x, y⟫_ℝ = ((starRingEnd ℂ) (f x) * f y).re
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<GOAL>Continuous fun p => ⟪p.1, p.2⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>α : Type u_4<VAR>f g : α → E<VAR>l : Filter α<VAR>x y : E<VAR>hf : Filter.Tendsto f l (𝓝 x)<VAR>hg : Filter.Tendsto g l (𝓝 y)<GOAL>Filter.Tendsto (fun t => ⟪f t, g t⟫_𝕜) l (𝓝 ⟪x, y⟫_𝕜)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>f g : α → E<VAR>x : α<VAR>s : Set α<VAR>hf : ContinuousWithinAt f s x<VAR>hg : ContinuousWithinAt g s x<GOAL>ContinuousWithinAt (fun t => ⟪f t, g t⟫_𝕜) s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>f g : α → E<VAR>x : α<VAR>hf : ContinuousAt f x<VAR>hg : ContinuousAt g x<GOAL>ContinuousAt (fun t => ⟪f t, g t⟫_𝕜) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>f g : α → E<VAR>s : Set α<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<GOAL>ContinuousOn (fun t => ⟪f t, g t⟫_𝕜) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>f g : α → E<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun t => ⟪f t, g t⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →L[𝕜] E<VAR>x : E<GOAL>T.reApplyInnerSelf x = RCLike.re ⟪T x, x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →L[𝕜] E<GOAL>Continuous T.reApplyInnerSelf
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →L[𝕜] E<VAR>x : E<VAR>c : 𝕜<GOAL>T.reApplyInnerSelf (c • x) = ‖c‖ ^ 2 * T.reApplyInnerSelf x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>a b : E<GOAL>⟪↑E a, ↑E b⟫_𝕜 = ⟪a, b⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<GOAL>Continuous (Function.uncurry inner)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>f g : α → UniformSpace.Completion E<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun x => ⟪f x, g x⟫_𝕜
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>K : Set F<VAR>ne : K.Nonempty<VAR>h₁ : IsComplete K<VAR>h₂ : Convex ℝ K<VAR>u : F<GOAL>∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>K : Set F<VAR>h : Convex ℝ K<VAR>u v : F<VAR>hv : v ∈ K<GOAL>‖u - v‖ = ⨅ w, ‖u - ↑w‖ ↔ ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>h : IsComplete ↑K<VAR>u : E<GOAL>∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>K : Submodule ℝ F<VAR>u v : F<VAR>hv : v ∈ K<GOAL>‖u - v‖ = ⨅ w, ‖u - ↑w‖ ↔ ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>u v : E<VAR>hv : v ∈ K<GOAL>‖u - v‖ = ⨅ w, ‖u - ↑w‖ ↔ ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>self : HasOrthogonalProjection K<VAR>v : E<GOAL>∃ w ∈ K, v - w ∈ Kᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>v : E<GOAL>orthogonalProjectionFn K v ∈ K
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>v w : E<GOAL>w ∈ K → ⟪v - orthogonalProjectionFn K v, w⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>u v : E<VAR>hvm : v ∈ K<VAR>hvo : ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0<GOAL>orthogonalProjectionFn K u = v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>v : E<GOAL>‖v‖ * ‖v‖ = ‖v - orthogonalProjectionFn K v‖ * ‖v - orthogonalProjectionFn K v‖ + ‖orthogonalProjectionFn K v‖ * ‖orthogonalProjectionFn K v‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>v : E<GOAL>orthogonalProjectionFn K v = ↑((orthogonalProjection K) v)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>v w : E<GOAL>w ∈ K → ⟪v - ↑((orthogonalProjection K) v), w⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>v : E<GOAL>v - ↑((orthogonalProjection K) v) ∈ Kᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>u v : E<VAR>hvm : v ∈ K<VAR>hvo : ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0<GOAL>↑((orthogonalProjection K) u) = v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>u v : E<VAR>hv : v ∈ K<VAR>hvo : u - v ∈ Kᗮ<GOAL>↑((orthogonalProjection K) u) = v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>u v z : E<VAR>hv : v ∈ K<VAR>hz : z ∈ Kᗮ<VAR>hu : u = v + z<GOAL>↑((orthogonalProjection K) u) = v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>u : E<GOAL>↑((orthogonalProjection Kᗮ) u) = u - ↑((orthogonalProjection K) u)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>u : E<GOAL>(orthogonalProjection Kᗮ) u = ⟨u - ↑((orthogonalProjection K) u), ⋯⟩
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U : Submodule 𝕜 E<VAR>HasOrthogonalProjection U<VAR>y : E<GOAL>‖y - ↑((orthogonalProjection U) y)‖ = ⨅ x, ‖y - ↑x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>K' : Submodule 𝕜 E<VAR>HasOrthogonalProjection K'<VAR>h : K = K'<VAR>u : E<GOAL>↑((orthogonalProjection K) u) = ↑((orthogonalProjection K') u)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>v : ↥K<GOAL>(orthogonalProjection K) ↑v = v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>v : E<GOAL>↑((orthogonalProjection K) v) = v ↔ v ∈ K
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>v : E<GOAL>(orthogonalProjection K) v = 0 ↔ v ∈ Kᗮ