ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>v : E<VAR>hv : v ∈ (⨆ μ, Module.End.eigenspace T μ)ᗮ<GOAL>T v ∈ (⨆ μ, Module.End.eigenspace T μ)ᗮ
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>μ : 𝕜<GOAL>Module.End.eigenspace (T.restrict ⋯) μ = ⊥
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>FiniteDimensional 𝕜 E<GOAL>(⨆ μ, Module.End.eigenspace T μ)ᗮ = ⊥
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>FiniteDimensional 𝕜 E<GOAL>(⨆ μ, Module.End.eigenspace T (↑T μ))ᗮ = ⊥
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>FiniteDimensional 𝕜 E<VAR>_hT : Fact T.IsSymmetric<VAR>x : E<VAR>μ : Module.End.Eigenvalues T<GOAL>((DirectSum.decompose fun μ => Module.End.eigenspace T (↑T μ)) x) μ = (orthogonalProjection (Module.End.eigenspace T (↑T μ))) x
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>FiniteDimensional 𝕜 E<GOAL>DirectSum.IsInternal fun μ => Module.End.eigenspace T (↑T μ)
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>FiniteDimensional 𝕜 E<VAR>w : PiLp 2 fun μ => ↥(Module.End.eigenspace T (↑T μ))<GOAL>hT.diagonalization.symm w = ∑ μ : Module.End.Eigenvalues T, ↑(w μ)
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>FiniteDimensional 𝕜 E<VAR>v : E<VAR>μ : Module.End.Eigenvalues T<GOAL>hT.diagonalization (T v) μ = ↑T μ • hT.diagonalization v μ
<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank 𝕜 E = n<GOAL>hT.eigenvectorBasis hn = DirectSum.IsInternal.subordinateOrthonormalBasis hn ⋯ ⋯
<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank 𝕜 E = n<VAR>i : Fin n<GOAL>hT.eigenvalues hn i = RCLike.re (↑T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯))
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank 𝕜 E = n<VAR>i : Fin n<GOAL>Module.End.HasEigenvector T (↑(hT.eigenvalues hn i)) ((hT.eigenvectorBasis hn) i)
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank 𝕜 E = n<VAR>i : Fin n<GOAL>Module.End.HasEigenvalue T ↑(hT.eigenvalues hn i)
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank 𝕜 E = n<VAR>i : Fin n<GOAL>T ((hT.eigenvectorBasis hn) i) = ↑(hT.eigenvalues hn i) • (hT.eigenvectorBasis hn) i
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank 𝕜 E = n<VAR>v : E<VAR>i : Fin n<GOAL>(hT.eigenvectorBasis hn).repr (T v) i = ↑(hT.eigenvalues hn i) * (hT.eigenvectorBasis hn).repr v i
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>μ : 𝕜<VAR>v : E<VAR>T : E →ₗ[𝕜] E<VAR>h : v ∈ Module.End.eigenspace T μ<GOAL>⟪v, T v⟫_𝕜 = μ * ↑‖v‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>μ : ℝ<VAR>T : E →ₗ[𝕜] E<VAR>hμ : Module.End.HasEigenvalue T ↑μ<VAR>hnn : ∀ (x : E), 0 ≤ RCLike.re ⟪x, T x⟫_𝕜<GOAL>0 ≤ μ
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>μ : ℝ<VAR>T : E →ₗ[𝕜] E<VAR>hμ : Module.End.HasEigenvalue T ↑μ<VAR>hnn : ∀ (x : E), 0 < RCLike.re ⟪x, T x⟫_𝕜<GOAL>0 < μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>ι : Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>e f : OrthonormalBasis ι ℝ E<VAR>h : e.toBasis.orientation = f.toBasis.orientation<GOAL>e.toBasis.det ⇑f = 1
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>ι : Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>e f : OrthonormalBasis ι ℝ E<VAR>h : e.toBasis.orientation ≠ f.toBasis.orientation<GOAL>e.toBasis.det ⇑f = -1
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>ι : Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>e f : OrthonormalBasis ι ℝ E<GOAL>e.toBasis.det = f.toBasis.det ↔ e.toBasis.orientation = f.toBasis.orientation
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>ι : Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>e f : OrthonormalBasis ι ℝ E<VAR>h : e.toBasis.orientation ≠ f.toBasis.orientation<GOAL>e.toBasis.det = -f.toBasis.det
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>ι : Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>ne : Nonempty ι<VAR>e : OrthonormalBasis ι ℝ E<VAR>x : Orientation ℝ E ι<GOAL>Orthonormal ℝ ⇑(e.toBasis.adjustToOrientation x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>ι : Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>ne : Nonempty ι<VAR>e : OrthonormalBasis ι ℝ E<VAR>x : Orientation ℝ E ι<GOAL>(e.adjustToOrientation x).toBasis = e.toBasis.adjustToOrientation x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>ι : Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>ne : Nonempty ι<VAR>e : OrthonormalBasis ι ℝ E<VAR>x : Orientation ℝ E ι<GOAL>(e.adjustToOrientation x).toBasis.orientation = x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>ι : Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>ne : Nonempty ι<VAR>e : OrthonormalBasis ι ℝ E<VAR>x : Orientation ℝ E ι<VAR>i : ι<GOAL>(e.adjustToOrientation x) i = e i ∨ (e.adjustToOrientation x) i = -e i
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>ι : Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>ne : Nonempty ι<VAR>e : OrthonormalBasis ι ℝ E<VAR>x : Orientation ℝ E ι<GOAL>(e.adjustToOrientation x).toBasis.det = e.toBasis.det ∨ (e.adjustToOrientation x).toBasis.det = -e.toBasis.det
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>ι : Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>ne : Nonempty ι<VAR>e : OrthonormalBasis ι ℝ E<VAR>x : Orientation ℝ E ι<VAR>v : ι → E<GOAL>|(e.adjustToOrientation x).toBasis.det v| = |e.toBasis.det v|
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : FiniteDimensional.finrank ℝ E = n<VAR>x : Orientation ℝ E (Fin n)<GOAL>(Orientation.finOrthonormalBasis hn h x).toBasis.orientation = x
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (FiniteDimensional.finrank ℝ E = n)<VAR>o : Orientation ℝ E (Fin n)<GOAL>o.volumeForm = Nat.casesAuxOn (motive := fun a => n = a → E [⋀^Fin n]→ₗ[ℝ] ℝ) n (fun h => Eq.ndrec (motive := fun {n} => [_i : Fact (FiniteDimensional.finrank ℝ E = n)] → Orientation ℝ E (Fin n) → E [⋀^Fin n]→ₗ[ℝ] ℝ) (fun [Fact (FiniteDimensional.finrank ℝ E = 0)] o => let opos := AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1; ⋯.by_cases (fun x => opos) fun x => -opos) ⋯ o) (fun n_1 h => Eq.ndrec (motive := fun {n} => [_i : Fact (FiniteDimensional.finrank ℝ E = n)] → Orientation ℝ E (Fin n) → E [⋀^Fin n]→ₗ[ℝ] ℝ) (fun [Fact (FiniteDimensional.finrank ℝ E = n_1 + 1)] o => (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det) ⋯ o) ⋯
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>_i : Fact (FiniteDimensional.finrank ℝ E = 0)<GOAL>positiveOrientation.volumeForm = AlternatingMap.constLinearEquivOfIsEmpty 1
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>_i : Fact (FiniteDimensional.finrank ℝ E = 0)<GOAL>(-positiveOrientation).volumeForm = -AlternatingMap.constLinearEquivOfIsEmpty 1
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (FiniteDimensional.finrank ℝ E = n)<VAR>o : Orientation ℝ E (Fin n)<VAR>b : OrthonormalBasis (Fin n) ℝ E<VAR>hb : b.toBasis.orientation = o<GOAL>o.volumeForm = b.toBasis.det
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (FiniteDimensional.finrank ℝ E = n)<VAR>o : Orientation ℝ E (Fin n)<VAR>b : OrthonormalBasis (Fin n) ℝ E<VAR>hb : b.toBasis.orientation ≠ o<GOAL>o.volumeForm = -b.toBasis.det
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (FiniteDimensional.finrank ℝ E = n)<VAR>o : Orientation ℝ E (Fin n)<GOAL>(-o).volumeForm = -o.volumeForm
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (FiniteDimensional.finrank ℝ E = n)<VAR>o : Orientation ℝ E (Fin n)<VAR>b : OrthonormalBasis (Fin n) ℝ E<VAR>v : Fin n → E<GOAL>|o.volumeForm v| = |b.toBasis.det v|
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (FiniteDimensional.finrank ℝ E = n)<VAR>o : Orientation ℝ E (Fin n)<VAR>v : Fin n → E<GOAL>|o.volumeForm v| ≤ ∏ i : Fin n, ‖v i‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (FiniteDimensional.finrank ℝ E = n)<VAR>o : Orientation ℝ E (Fin n)<VAR>v : Fin n → E<GOAL>o.volumeForm v ≤ ∏ i : Fin n, ‖v i‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (FiniteDimensional.finrank ℝ E = n)<VAR>o : Orientation ℝ E (Fin n)<VAR>v : Fin n → E<VAR>hv : Pairwise fun i j => ⟪v i, v j⟫_ℝ = 0<GOAL>|o.volumeForm v| = ∏ i : Fin n, ‖v i‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (FiniteDimensional.finrank ℝ E = n)<VAR>o : Orientation ℝ E (Fin n)<VAR>v : OrthonormalBasis (Fin n) ℝ E<GOAL>|o.volumeForm ⇑v| = 1
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (FiniteDimensional.finrank ℝ E = n)<VAR>o : Orientation ℝ E (Fin n)<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>Fact (FiniteDimensional.finrank ℝ F = n)<VAR>φ : E ≃ₗᵢ[ℝ] F<VAR>x : Fin n → F<GOAL>((Orientation.map (Fin n) φ.toLinearEquiv) o).volumeForm x = o.volumeForm (⇑φ.symm ∘ x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (FiniteDimensional.finrank ℝ E = n)<VAR>o : Orientation ℝ E (Fin n)<VAR>φ : E ≃ₗᵢ[ℝ] E<VAR>hφ : 0 < LinearMap.det ↑φ.toLinearEquiv<VAR>x : Fin n → E<GOAL>o.volumeForm (⇑φ ∘ x) = o.volumeForm x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>((InnerProductSpace.toDualMap 𝕜 E) x) y = ⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Nontrivial E<GOAL>‖innerSL 𝕜‖ = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>x y : E<VAR>b : Basis ι 𝕜 E<VAR>h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜<GOAL>x = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>x y : E<VAR>b : Basis ι 𝕜 E<VAR>h : ∀ (i : ι), ⟪x, b i⟫_𝕜 = ⟪y, b i⟫_𝕜<GOAL>x = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>x y : E<GOAL>((InnerProductSpace.toDual 𝕜 E) x) y = ⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>x : E<VAR>y : NormedSpace.Dual 𝕜 E<GOAL>⟪(InnerProductSpace.toDual 𝕜 E).symm y, x⟫_𝕜 = y x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>B : E →L⋆[𝕜] E →L[𝕜] 𝕜<VAR>v w : E<GOAL>⟪(InnerProductSpace.continuousLinearMapOfBilin B) v, w⟫_𝕜 = (B v) w
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>B : E →L⋆[𝕜] E →L[𝕜] 𝕜<VAR>v f : E<VAR>is_lax_milgram : ∀ (w : E), ⟪f, w⟫_𝕜 = (B v) w<GOAL>f = (InnerProductSpace.continuousLinearMapOfBilin B) v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>T : E →L[𝕜] E<VAR>hT : T.IsPositive<GOAL>IsSelfAdjoint T
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>T : E →L[𝕜] E<VAR>hT : T.IsPositive<VAR>x : E<GOAL>0 ≤ RCLike.re ⟪T x, x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>T : E →L[𝕜] E<VAR>hT : T.IsPositive<VAR>x : E<GOAL>0 ≤ RCLike.re ⟪x, T x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<GOAL>ContinuousLinearMap.IsPositive 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<GOAL>ContinuousLinearMap.IsPositive 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>T S : E →L[𝕜] E<VAR>hT : T.IsPositive<VAR>hS : S.IsPositive<GOAL>(T + S).IsPositive
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 E<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace E<VAR>CompleteSpace F<VAR>T : E →L[𝕜] E<VAR>hT : T.IsPositive<VAR>S : E →L[𝕜] F<GOAL>(S.comp (T.comp (ContinuousLinearMap.adjoint S))).IsPositive
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 E<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace E<VAR>CompleteSpace F<VAR>T : E →L[𝕜] E<VAR>hT : T.IsPositive<VAR>S : F →L[𝕜] E<GOAL>((ContinuousLinearMap.adjoint S).comp (T.comp S)).IsPositive
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>U : Submodule 𝕜 E<VAR>T : E →L[𝕜] E<VAR>hT : T.IsPositive<VAR>CompleteSpace ↥U<GOAL>(U.subtypeL.comp ((orthogonalProjection U).comp (T.comp (U.subtypeL.comp (orthogonalProjection U))))).IsPositive
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>T : E →L[𝕜] E<VAR>hT : T.IsPositive<VAR>U : Submodule 𝕜 E<VAR>CompleteSpace ↥U<GOAL>((orthogonalProjection U).comp (T.comp U.subtypeL)).IsPositive
<VAR>E' : Type u_4<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace ℂ E'<VAR>CompleteSpace E'<VAR>T : E' →L[ℂ] E'<GOAL>T.IsPositive ↔ ∀ (x : E'), ↑(RCLike.re ⟪T x, x⟫_ℂ) = ⟪T x, x⟫_ℂ ∧ 0 ≤ RCLike.re ⟪T x, x⟫_ℂ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>f g : E →L[𝕜] E<GOAL>f ≤ g ↔ (g - f).IsPositive
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>f : E →L[𝕜] E<GOAL>0 ≤ f ↔ f.IsPositive
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<GOAL>Filter.Tendsto (fun n => (↑n)⁻¹) Filter.atTop (𝓝 0)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>x : E<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>HasFDerivAt (fun x => ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>Differentiable ℝ fun x => ‖x‖ ^ p
<VAR>x : ℝ<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>HasDerivAt (fun x => ‖x‖ ^ p) (p * ‖x‖ ^ (p - 2) * x) x
<VAR>x : ℝ<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>HasDerivAt (fun x => |x| ^ p) (p * |x| ^ (p - 2) * x) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>x : E<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>fderiv ℝ (fun x => ‖x‖ ^ p) x = (p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : F → E<VAR>hf : Differentiable ℝ f<VAR>x : F<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>fderiv ℝ (fun x => ‖f x‖ ^ p) x = (p * ‖f x‖ ^ (p - 2)) • ((innerSL ℝ) (f x)).comp (fderiv ℝ f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : F → E<VAR>hf : Differentiable ℝ f<VAR>x : F<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>‖fderiv ℝ (fun x => ‖f x‖ ^ p) x‖ ≤ p * ‖f x‖ ^ (p - 1) * ‖fderiv ℝ f x‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>x : E<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>‖fderiv ℝ (fun x => ‖x‖ ^ p) x‖ = p * ‖x‖ ^ (p - 1)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : F → E<VAR>hf : Differentiable ℝ f<VAR>x : F<VAR>p : NNReal<VAR>hp : 1 < p<GOAL>‖fderiv ℝ (fun x => ‖f x‖ ^ ↑p) x‖₊ ≤ p * ‖f x‖₊ ^ (↑p - 1) * ‖fderiv ℝ f x‖₊
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>ContDiff ℝ 1 fun x => ‖x‖ ^ p
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : F → E<VAR>hf : ContDiff ℝ 1 f<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>ContDiff ℝ 1 fun x => ‖f x‖ ^ p
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : F → E<VAR>hf : Differentiable ℝ f<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>Differentiable ℝ fun x => ‖f x‖ ^ p
<VAR>M : Type u_1<VAR>OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu : Monotone u<VAR>n : ℕ<GOAL>∑ k ∈ Finset.Ico (u 0) (u n), f k ≤ ∑ k ∈ Finset.range n, (u (k + 1) - u k) • f (u k)
<VAR>M : Type u_1<VAR>OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>n : ℕ<GOAL>∑ k ∈ Finset.Ico 1 (2 ^ n), f k ≤ ∑ k ∈ Finset.range n, 2 ^ k • f (2 ^ k)
<VAR>M : Type u_1<VAR>OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu : Monotone u<VAR>n : ℕ<GOAL>∑ k ∈ Finset.range (u n), f k ≤ ∑ k ∈ Finset.range (u 0), f k + ∑ k ∈ Finset.range n, (u (k + 1) - u k) • f (u k)
<VAR>M : Type u_1<VAR>OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>n : ℕ<GOAL>∑ k ∈ Finset.range (2 ^ n), f k ≤ f 0 + ∑ k ∈ Finset.range n, 2 ^ k • f (2 ^ k)
<VAR>M : Type u_1<VAR>OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu : Monotone u<VAR>n : ℕ<GOAL>∑ k ∈ Finset.range n, (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Finset.Ico (u 0 + 1) (u n + 1), f k
<VAR>M : Type u_1<VAR>OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<VAR>n : ℕ<GOAL>∑ k ∈ Finset.range n, 2 ^ k • f (2 ^ (k + 1)) ≤ ∑ k ∈ Finset.Ico 2 (2 ^ n + 1), f k
<VAR>M : Type u_1<VAR>OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>C : ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>h_nonneg : ∀ (n : ℕ), 0 ≤ f n<VAR>hu : Monotone u<VAR>h_succ_diff : SuccDiffBounded C u<VAR>n : ℕ<GOAL>∑ k ∈ Finset.range (n + 1), (u (k + 1) - u k) • f (u k) ≤ (u 1 - u 0) • f (u 0) + C • ∑ k ∈ Finset.Ico (u 0 + 1) (u n + 1), f k
<VAR>M : Type u_1<VAR>OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<VAR>n : ℕ<GOAL>∑ k ∈ Finset.range (n + 1), 2 ^ k • f (2 ^ k) ≤ f 1 + 2 • ∑ k ∈ Finset.Ico 2 (2 ^ n + 1), f k
<VAR>u : ℕ → ℕ<VAR>f : ℕ → ENNReal<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu : StrictMono u<GOAL>∑' (k : ℕ), f k ≤ ∑ k ∈ Finset.range (u 0), f k + ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k)
<VAR>f : ℕ → ENNReal<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<GOAL>∑' (k : ℕ), f k ≤ f 0 + ∑' (k : ℕ), 2 ^ k * f (2 ^ k)
<VAR>u : ℕ → ℕ<VAR>f : ℕ → ENNReal<VAR>C : ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>h_nonneg : ∀ (n : ℕ), 0 ≤ f n<VAR>hu : Monotone u<VAR>h_succ_diff : SuccDiffBounded C u<GOAL>∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k) ≤ (↑(u 1) - ↑(u 0)) * f (u 0) + ↑C * ∑' (k : ℕ), f k
<VAR>f : ℕ → ENNReal<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<GOAL>∑' (k : ℕ), 2 ^ k * f (2 ^ k) ≤ f 1 + 2 * ∑' (k : ℕ), f k
<VAR>C : ℕ<VAR>u : ℕ → ℕ<VAR>f : ℕ → NNReal<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu_strict : StrictMono u<VAR>hC_nonzero : C ≠ 0<VAR>h_succ_diff : SuccDiffBounded C u<GOAL>(Summable fun k => (↑(u (k + 1)) - ↑(u k)) * f (u k)) ↔ Summable f
<VAR>f : ℕ → NNReal<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<GOAL>(Summable fun k => 2 ^ k * f (2 ^ k)) ↔ Summable f
<VAR>C : ℕ<VAR>u : ℕ → ℕ<VAR>f : ℕ → ℝ<VAR>h_nonneg : ∀ (n : ℕ), 0 ≤ f n<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu_strict : StrictMono u<VAR>hC_nonzero : C ≠ 0<VAR>h_succ_diff : SuccDiffBounded C u<GOAL>(Summable fun k => (↑(u (k + 1)) - ↑(u k)) * f (u k)) ↔ Summable f
<VAR>f : ℕ → ℝ<VAR>h_nonneg : ∀ (n : ℕ), 0 ≤ f n<VAR>h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<GOAL>(Summable fun k => 2 ^ k * f (2 ^ k)) ↔ Summable f
<VAR>p : ℝ<GOAL>(Summable fun n => 1 / ↑n ^ p) ↔ 1 < p
<GOAL>Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, 1 / (↑i + 1)) Filter.atTop Filter.atTop
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>k n : ℕ<VAR>hk : k ≠ 0<VAR>h : k ≤ n<GOAL>∑ i ∈ Finset.Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>k n : ℕ<GOAL>∑ i ∈ Finset.Ioo k n, (↑i ^ 2)⁻¹ ≤ 2 / (↑k + 1)
<VAR>m : ℕ<VAR>hm : m ≠ 0<VAR>k : ZMod m<GOAL>¬Summable ({n | ↑n = k}.indicator fun n => 1 / ↑n)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>v : E<GOAL>v ∈ Kᗮ ↔ ∀ u ∈ K, ⟪u, v⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>v : E<GOAL>v ∈ Kᗮ ↔ ∀ u ∈ K, ⟪v, u⟫_𝕜 = 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>hu : u ∈ K<VAR>hv : v ∈ Kᗮ<GOAL>⟪u, v⟫_𝕜 = 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>hu : u ∈ K<VAR>hv : v ∈ Kᗮ<GOAL>⟪v, u⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>u v : E<GOAL>v ∈ (Submodule.span 𝕜 {u})ᗮ ↔ ⟪u, v⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>u v : E<GOAL>v ∈ (Submodule.span 𝕜 {u})ᗮ ↔ ⟪v, u⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>x y : E<VAR>h : ∀ (v : ↥K), ⟪x, ↑v⟫_𝕜 = ⟪y, ↑v⟫_𝕜<GOAL>x - y ∈ Kᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>x y : E<VAR>h : ∀ (v : ↥K), ⟪↑v, x⟫_𝕜 = ⟪↑v, y⟫_𝕜<GOAL>x - y ∈ Kᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<GOAL>K ⊓ Kᗮ = ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<GOAL>Disjoint K Kᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<GOAL>Kᗮ = ⨅ v, LinearMap.ker ((innerSL 𝕜) ↑v)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<GOAL>IsClosed ↑Kᗮ