ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x : E<VAR>hx : x ≠ 0<GOAL>⇑(o.basisRightAngleRotation x hx) = ![x, o.rightAngleRotation x]
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>a x : E<GOAL>⟪a, x⟫_ℝ • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a = ‖a‖ ^ 2 • (innerₛₗ ℝ) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>a x y : E<GOAL>⟪a, x⟫_ℝ * ⟪a, y⟫_ℝ + (o.areaForm a) x * (o.areaForm a) y = ‖a‖ ^ 2 * ⟪x, y⟫_ℝ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>a b : E<GOAL>⟪a, b⟫_ℝ ^ 2 + (o.areaForm a) b ^ 2 = ‖a‖ ^ 2 * ‖b‖ ^ 2
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>a x : E<GOAL>⟪a, x⟫_ℝ • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a = ‖a‖ ^ 2 • o.areaForm x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>a x y : E<GOAL>⟪a, x⟫_ℝ * (o.areaForm a) y - (o.areaForm a) x * ⟪a, y⟫_ℝ = ‖a‖ ^ 2 * (o.areaForm x) y
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>0 ≤ ⟪x, y⟫_ℝ ∧ (o.areaForm x) y = 0 ↔ SameRay ℝ x y
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.kahler x) y = ↑⟪x, y⟫_ℝ + (o.areaForm x) y • Complex.I
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.kahler x) y = (starRingEnd ℂ) ((o.kahler y) x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x : E<GOAL>(o.kahler x) x = ↑‖x‖ ^ 2
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.kahler (o.rightAngleRotation x)) y = -Complex.I * (o.kahler x) y
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.kahler x) (o.rightAngleRotation y) = Complex.I * (o.kahler x) y
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.kahler (o.rightAngleRotation x)) (o.rightAngleRotation y) = (o.kahler x) y
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>-(Complex.I * (Complex.I * (o.kahler x) y)) = (o.kahler x) y
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>((-o).kahler x) y = (starRingEnd ℂ) ((o.kahler x) y)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>a x y : E<GOAL>(o.kahler x) a * (o.kahler a) y = ↑‖a‖ ^ 2 * (o.kahler x) y
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>Complex.normSq ((o.kahler x) y) = ‖x‖ ^ 2 * ‖y‖ ^ 2
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>Complex.abs ((o.kahler x) y) = ‖x‖ * ‖y‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>‖(o.kahler x) y‖ = ‖x‖ * ‖y‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<VAR>hx : (o.kahler x) y = 0<GOAL>x = 0 ∨ y = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.kahler x) y = 0 ↔ x = 0 ∨ y = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(o.kahler x) y ≠ 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.kahler x) y ≠ 0 ↔ x ≠ 0 ∧ y ≠ 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>hF : Fact (FiniteDimensional.finrank ℝ F = 2)<VAR>φ : E ≃ₗᵢ[ℝ] F<VAR>x y : F<GOAL>(((Orientation.map (Fin 2) φ.toLinearEquiv) o).kahler x) y = (o.kahler (φ.symm x)) (φ.symm y)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>φ : E ≃ₗᵢ[ℝ] E<VAR>hφ : 0 < LinearMap.det ↑φ.toLinearEquiv<VAR>x y : E<GOAL>(o.kahler (φ x)) (φ y) = (o.kahler x) y
<VAR>w z : ℂ<GOAL>(Complex.orientation.areaForm w) z = ((starRingEnd ℂ) w * z).im
<VAR>z : ℂ<GOAL>Complex.orientation.rightAngleRotation z = Complex.I * z
<VAR>w z : ℂ<GOAL>(Complex.orientation.kahler w) z = (starRingEnd ℂ) w * z
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>f : E ≃ₗᵢ[ℝ] ℂ<VAR>hf : (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation<VAR>x y : E<GOAL>(o.areaForm x) y = ((starRingEnd ℂ) (f x) * f y).im
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>f : E ≃ₗᵢ[ℝ] ℂ<VAR>hf : (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation<VAR>x : E<GOAL>f (o.rightAngleRotation x) = Complex.I * f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>Fact (FiniteDimensional.finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>f : E ≃ₗᵢ[ℝ] ℂ<VAR>hf : (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation<VAR>x y : E<GOAL>(o.kahler x) y = (starRingEnd ℂ) (f x) * f y
<VAR>𝕜 : Type u_1<VAR>NormedField 𝕜<VAR>E : Type u_2<VAR>NormedRing E<VAR>StarRing E<VAR>CstarRing E<VAR>NormedAlgebra 𝕜 E<VAR>CompleteSpace E<VAR>u : ↥(unitary E)<GOAL>spectrum 𝕜 ↑u ⊆ Metric.sphere 0 1
<VAR>𝕜 : Type u_1<VAR>NormedField 𝕜<VAR>E : Type u_2<VAR>NormedRing E<VAR>StarRing E<VAR>CstarRing E<VAR>NormedAlgebra 𝕜 E<VAR>CompleteSpace E<VAR>u : E<VAR>h : u ∈ unitary E<GOAL>spectrum 𝕜 u ⊆ Metric.sphere 0 1
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>StarRing A<VAR>CstarRing A<VAR>a : A<VAR>ha : IsSelfAdjoint a<GOAL>spectralRadius ℂ a = ↑‖a‖₊
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>StarRing A<VAR>CstarRing A<VAR>a : A<VAR>ha : IsSelfAdjoint a<GOAL>(spectralRadius ℂ a).toReal = ‖a‖
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>StarRing A<VAR>CstarRing A<VAR>a : A<VAR>IsStarNormal a<GOAL>spectralRadius ℂ a = ↑‖a‖₊
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>StarRing A<VAR>CstarRing A<VAR>StarModule ℂ A<VAR>a : A<VAR>ha : IsSelfAdjoint a<VAR>z : ℂ<VAR>hz : z ∈ spectrum ℂ a<GOAL>z = ↑z.re
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>StarRing A<VAR>CstarRing A<VAR>StarModule ℂ A<VAR>a : ↥(selfAdjoint A)<VAR>z : ℂ<VAR>hz : z ∈ spectrum ℂ ↑a<GOAL>z = ↑z.re
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>StarRing A<VAR>CstarRing A<VAR>StarModule ℂ A<VAR>a : A<VAR>ha : IsSelfAdjoint a<GOAL>spectrum ℂ a = Complex.ofReal' ∘ Complex.re '' spectrum ℂ a
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>StarRing A<VAR>CstarRing A<VAR>StarModule ℂ A<VAR>a : ↥(selfAdjoint A)<GOAL>spectrum ℂ ↑a = Complex.ofReal' ∘ Complex.re '' spectrum ℂ ↑a
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>StarRing A<VAR>CstarRing A<VAR>NormedRing B<VAR>NormedAlgebra ℂ B<VAR>CompleteSpace B<VAR>StarRing B<VAR>CstarRing B<VAR>FunLike F A B<VAR>AlgHomClass F ℂ A B<VAR>StarAlgHomClass F ℂ A B<VAR>φ : F<VAR>a : A<GOAL>‖φ a‖₊ ≤ ‖a‖₊
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>StarRing A<VAR>CstarRing A<VAR>NormedRing B<VAR>NormedAlgebra ℂ B<VAR>CompleteSpace B<VAR>StarRing B<VAR>CstarRing B<VAR>FunLike F A B<VAR>AlgHomClass F ℂ A B<VAR>StarAlgHomClass F ℂ A B<VAR>φ : F<VAR>a : A<GOAL>‖φ a‖ ≤ ‖a‖
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>StarRing A<VAR>CstarRing A<VAR>NormedRing B<VAR>NormedAlgebra ℂ B<VAR>CompleteSpace B<VAR>StarRing B<VAR>CstarRing B<VAR>EquivLike F A B<VAR>NonUnitalAlgEquivClass F ℂ A B<VAR>StarAlgEquivClass F ℂ A B<VAR>φ : F<VAR>a : A<GOAL>‖φ a‖₊ = ‖a‖₊
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>StarRing A<VAR>CstarRing A<VAR>NormedRing B<VAR>NormedAlgebra ℂ B<VAR>CompleteSpace B<VAR>StarRing B<VAR>CstarRing B<VAR>EquivLike F A B<VAR>NonUnitalAlgEquivClass F ℂ A B<VAR>StarAlgEquivClass F ℂ A B<VAR>φ : F<VAR>a : A<GOAL>‖φ a‖ = ‖a‖
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>StarRing A<VAR>CstarRing A<VAR>NormedRing B<VAR>NormedAlgebra ℂ B<VAR>CompleteSpace B<VAR>StarRing B<VAR>CstarRing B<VAR>EquivLike F A B<VAR>NonUnitalAlgEquivClass F ℂ A B<VAR>StarAlgEquivClass F ℂ A B<VAR>φ : F<GOAL>Isometry ⇑φ
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>StarRing A<VAR>CstarRing A<VAR>StarModule ℂ A<VAR>FunLike F A ℂ<VAR>hF : AlgHomClass F ℂ A ℂ<GOAL>StarAlgHomClass F ℂ A ℂ
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>A : Matrix m n α<GOAL>‖A‖ = ‖fun i j => A i j‖
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>A : Matrix m n α<GOAL>‖A‖ = ↑(Finset.univ.sup fun i => Finset.univ.sup fun j => ‖A i j‖₊)
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>A : Matrix m n α<GOAL>‖A‖₊ = ‖fun i j => A i j‖₊
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>A : Matrix m n α<GOAL>‖A‖ ≤ r ↔ ∀ (i : m) (j : n), ‖A i j‖ ≤ r
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>r : ℝ≥0<VAR>A : Matrix m n α<GOAL>‖A‖₊ ≤ r ↔ ∀ (i : m) (j : n), ‖A i j‖₊ ≤ r
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>r : ℝ<VAR>hr : 0 < r<VAR>A : Matrix m n α<GOAL>‖A‖ < r ↔ ∀ (i : m) (j : n), ‖A i j‖ < r
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>r : ℝ≥0<VAR>hr : 0 < r<VAR>A : Matrix m n α<GOAL>‖A‖₊ < r ↔ ∀ (i : m) (j : n), ‖A i j‖₊ < r
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>A : Matrix m n α<VAR>i : m<VAR>j : n<GOAL>‖A i j‖ ≤ ‖A‖
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>A : Matrix m n α<VAR>i : m<VAR>j : n<GOAL>‖A i j‖₊ ≤ ‖A‖₊
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>Fintype m<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>A : Matrix m n α<VAR>f : α → β<VAR>hf : ∀ (a : α), ‖f a‖₊ = ‖a‖₊<GOAL>‖A.map f‖₊ = ‖A‖₊
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>Fintype m<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>A : Matrix m n α<VAR>f : α → β<VAR>hf : ∀ (a : α), ‖f a‖ = ‖a‖<GOAL>‖A.map f‖ = ‖A‖
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>A : Matrix m n α<GOAL>‖Aᵀ‖₊ = ‖A‖₊
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>A : Matrix m n α<GOAL>‖Aᵀ‖ = ‖A‖
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>StarAddMonoid α<VAR>NormedStarGroup α<VAR>A : Matrix m n α<GOAL>‖Aᴴ‖₊ = ‖A‖₊
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>StarAddMonoid α<VAR>NormedStarGroup α<VAR>A : Matrix m n α<GOAL>‖Aᴴ‖ = ‖A‖
<VAR>m : Type u_3<VAR>α : Type u_5<VAR>ι : Type u_7<VAR>Fintype m<VAR>Unique ι<VAR>SeminormedAddCommGroup α<VAR>v : m → α<GOAL>‖Matrix.col ι v‖₊ = ‖v‖₊
<VAR>m : Type u_3<VAR>α : Type u_5<VAR>ι : Type u_7<VAR>Fintype m<VAR>Unique ι<VAR>SeminormedAddCommGroup α<VAR>v : m → α<GOAL>‖Matrix.col ι v‖ = ‖v‖
<VAR>n : Type u_4<VAR>α : Type u_5<VAR>ι : Type u_7<VAR>Fintype n<VAR>Unique ι<VAR>SeminormedAddCommGroup α<VAR>v : n → α<GOAL>‖Matrix.row ι v‖₊ = ‖v‖₊
<VAR>n : Type u_4<VAR>α : Type u_5<VAR>ι : Type u_7<VAR>Fintype n<VAR>Unique ι<VAR>SeminormedAddCommGroup α<VAR>v : n → α<GOAL>‖Matrix.row ι v‖ = ‖v‖
<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>DecidableEq n<VAR>v : n → α<GOAL>‖Matrix.diagonal v‖₊ = ‖v‖₊
<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>DecidableEq n<VAR>v : n → α<GOAL>‖Matrix.diagonal v‖ = ‖v‖
<VAR>R : Type u_1<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>SeminormedRing R<VAR>SeminormedAddCommGroup α<VAR>Module R α<VAR>BoundedSMul R α<GOAL>BoundedSMul R (Matrix m n α)
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>A : Matrix m n α<GOAL>‖A‖ = ↑(Finset.univ.sup fun i => ∑ j : n, ‖A i j‖₊)
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>A : Matrix m n α<GOAL>‖A‖₊ = Finset.univ.sup fun i => ∑ j : n, ‖A i j‖₊
<VAR>n : Type u_4<VAR>α : Type u_5<VAR>ι : Type u_7<VAR>Fintype n<VAR>Unique ι<VAR>SeminormedAddCommGroup α<VAR>v : n → α<GOAL>‖Matrix.row ι v‖₊ = ∑ i : n, ‖v i‖₊
<VAR>n : Type u_4<VAR>α : Type u_5<VAR>ι : Type u_7<VAR>Fintype n<VAR>Unique ι<VAR>SeminormedAddCommGroup α<VAR>v : n → α<GOAL>‖Matrix.row ι v‖ = ∑ i : n, ‖v i‖
<VAR>m : Type u_3<VAR>α : Type u_5<VAR>Fintype m<VAR>SeminormedAddCommGroup α<VAR>DecidableEq m<VAR>v : m → α<GOAL>‖Matrix.diagonal v‖₊ = ‖v‖₊
<VAR>m : Type u_3<VAR>α : Type u_5<VAR>Fintype m<VAR>SeminormedAddCommGroup α<VAR>DecidableEq m<VAR>v : m → α<GOAL>‖Matrix.diagonal v‖ = ‖v‖
<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype l<VAR>Fintype m<VAR>Fintype n<VAR>NonUnitalSeminormedRing α<VAR>A : Matrix l m α<VAR>B : Matrix m n α<GOAL>‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊
<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype l<VAR>Fintype m<VAR>Fintype n<VAR>NonUnitalSeminormedRing α<VAR>A : Matrix l m α<VAR>B : Matrix m n α<GOAL>‖A * B‖ ≤ ‖A‖ * ‖B‖
<VAR>l : Type u_2<VAR>m : Type u_3<VAR>α : Type u_5<VAR>Fintype l<VAR>Fintype m<VAR>NonUnitalSeminormedRing α<VAR>A : Matrix l m α<VAR>v : m → α<GOAL>‖A *ᵥ v‖₊ ≤ ‖A‖₊ * ‖v‖₊
<VAR>l : Type u_2<VAR>m : Type u_3<VAR>α : Type u_5<VAR>Fintype l<VAR>Fintype m<VAR>NonUnitalSeminormedRing α<VAR>A : Matrix l m α<VAR>v : m → α<GOAL>‖A *ᵥ v‖ ≤ ‖A‖ * ‖v‖
<VAR>α : Type u_5<VAR>NormedDivisionRing α<VAR>NormedAlgebra ℝ α<VAR>a : α<GOAL>‖Matrix.unitOf a‖₊ = 1
<VAR>α : Type u_5<VAR>NormedDivisionRing α<VAR>NormedAlgebra ℝ α<VAR>a : α<GOAL>a * Matrix.unitOf a = (algebraMap ℝ α) ↑‖a‖₊
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>NontriviallyNormedField α<VAR>NormedAlgebra ℝ α<VAR>A : Matrix m n α<GOAL>‖A‖₊ = ‖{ toLinearMap := A.mulVecLin, cont := ⋯ }‖₊
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>NontriviallyNormedField α<VAR>NormedAlgebra ℝ α<VAR>A : Matrix m n α<GOAL>‖A‖ = ‖{ toLinearMap := A.mulVecLin, cont := ⋯ }‖
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>NontriviallyNormedField α<VAR>NormedAlgebra ℝ α<VAR>DecidableEq n<VAR>f : (n → α) →L[α] m → α<GOAL>‖LinearMap.toMatrix' ↑f‖₊ = ‖f‖₊
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>NontriviallyNormedField α<VAR>NormedAlgebra ℝ α<VAR>DecidableEq n<VAR>f : (n → α) →L[α] m → α<GOAL>‖LinearMap.toMatrix' ↑f‖ = ‖f‖
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>A : Matrix m n α<GOAL>‖A‖₊ = (∑ i : m, ∑ j : n, ‖A i j‖₊ ^ 2) ^ (1 / 2)
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>A : Matrix m n α<GOAL>‖A‖ = (∑ i : m, ∑ j : n, ‖A i j‖ ^ 2) ^ (1 / 2)
<VAR>m : Type u_3<VAR>α : Type u_5<VAR>ι : Type u_7<VAR>Fintype m<VAR>Unique ι<VAR>SeminormedAddCommGroup α<VAR>v : m → α<GOAL>‖Matrix.row ι v‖ = ‖(WithLp.equiv 2 (m → α)).symm v‖
<VAR>m : Type u_3<VAR>α : Type u_5<VAR>ι : Type u_7<VAR>Fintype m<VAR>Unique ι<VAR>SeminormedAddCommGroup α<VAR>v : m → α<GOAL>‖Matrix.row ι v‖₊ = ‖(WithLp.equiv 2 (m → α)).symm v‖₊
<VAR>n : Type u_4<VAR>α : Type u_5<VAR>ι : Type u_7<VAR>Fintype n<VAR>Unique ι<VAR>SeminormedAddCommGroup α<VAR>v : n → α<GOAL>‖Matrix.col ι v‖ = ‖(WithLp.equiv 2 (n → α)).symm v‖
<VAR>n : Type u_4<VAR>α : Type u_5<VAR>ι : Type u_7<VAR>Fintype n<VAR>Unique ι<VAR>SeminormedAddCommGroup α<VAR>v : n → α<GOAL>‖Matrix.col ι v‖₊ = ‖(WithLp.equiv 2 (n → α)).symm v‖₊
<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>DecidableEq n<VAR>v : n → α<GOAL>‖Matrix.diagonal v‖₊ = ‖(WithLp.equiv 2 (n → α)).symm v‖₊
<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype n<VAR>SeminormedAddCommGroup α<VAR>DecidableEq n<VAR>v : n → α<GOAL>‖Matrix.diagonal v‖ = ‖(WithLp.equiv 2 (n → α)).symm v‖
<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype n<VAR>DecidableEq n<VAR>SeminormedAddCommGroup α<VAR>One α<GOAL>‖1‖₊ = NNReal.sqrt ↑(Fintype.card n) * ‖1‖₊
<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype l<VAR>Fintype m<VAR>Fintype n<VAR>RCLike α<VAR>A : Matrix l m α<VAR>B : Matrix m n α<GOAL>‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊
<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>Fintype l<VAR>Fintype m<VAR>Fintype n<VAR>RCLike α<VAR>A : Matrix l m α<VAR>B : Matrix m n α<GOAL>‖A * B‖ ≤ ‖A‖ * ‖B‖
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>n : ℕ<VAR>CompleteSpace E<VAR>I : BoxIntegral.Box (Fin (n + 1))<VAR>i : Fin (n + 1)<VAR>f : (Fin (n + 1) → ℝ) → E<VAR>f' : (Fin (n + 1) → ℝ) →L[ℝ] E<VAR>hfc : ContinuousOn f (BoxIntegral.Box.Icc I)<VAR>x : Fin (n + 1) → ℝ<VAR>hxI : x ∈ BoxIntegral.Box.Icc I<VAR>a : E<VAR>ε : ℝ<VAR>h0 : 0 < ε<VAR>hε : ∀ y ∈ BoxIntegral.Box.Icc I, ‖f y - a - f' (y - x)‖ ≤ ε * ‖y - x‖<VAR>c : ℝ≥0<VAR>hc : I.distortion ≤ c<GOAL>‖(∏ j : Fin (n + 1), (I.upper j - I.lower j)) • f' (Pi.single i 1) - (BoxIntegral.integral (I.face i) ⊥ (f ∘ i.insertNth (I.upper i)) BoxIntegral.BoxAdditiveMap.volume - BoxIntegral.integral (I.face i) ⊥ (f ∘ i.insertNth (I.lower i)) BoxIntegral.BoxAdditiveMap.volume)‖ ≤ 2 * ε * ↑c * ∏ j : Fin (n + 1), (I.upper j - I.lower j)
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>n : ℕ<VAR>CompleteSpace E<VAR>I : BoxIntegral.Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hs : ∀ x ∈ s, ContinuousWithinAt f (BoxIntegral.Box.Icc I) x<VAR>Hd : ∀ x ∈ BoxIntegral.Box.Icc I \ s, HasFDerivWithinAt f (f' x) (BoxIntegral.Box.Icc I) x<VAR>i : Fin (n + 1)<GOAL>BoxIntegral.HasIntegral I BoxIntegral.IntegrationParams.GP (fun x => (f' x) (Pi.single i 1)) BoxIntegral.BoxAdditiveMap.volume (BoxIntegral.integral (I.face i) BoxIntegral.IntegrationParams.GP (fun x => f (i.insertNth (I.upper i) x)) BoxIntegral.BoxAdditiveMap.volume - BoxIntegral.integral (I.face i) BoxIntegral.IntegrationParams.GP (fun x => f (i.insertNth (I.lower i) x)) BoxIntegral.BoxAdditiveMap.volume)
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>n : ℕ<VAR>CompleteSpace E<VAR>I : BoxIntegral.Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hs : ∀ x ∈ s, ContinuousWithinAt f (BoxIntegral.Box.Icc I) x<VAR>Hd : ∀ x ∈ BoxIntegral.Box.Icc I \ s, HasFDerivWithinAt f (f' x) (BoxIntegral.Box.Icc I) x<GOAL>BoxIntegral.HasIntegral I BoxIntegral.IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), (f' x) (Pi.single i 1) i) BoxIntegral.BoxAdditiveMap.volume (∑ i : Fin (n + 1), (BoxIntegral.integral (I.face i) BoxIntegral.IntegrationParams.GP (fun x => f (i.insertNth (I.upper i) x) i) BoxIntegral.BoxAdditiveMap.volume - BoxIntegral.integral (I.face i) BoxIntegral.IntegrationParams.GP (fun x => f (i.insertNth (I.lower i) x) i) BoxIntegral.BoxAdditiveMap.volume))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>CommRing 𝕜<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<GOAL>p.applyComposition (Composition.ones n) = fun v i => (p 1) fun x => v (Fin.castLE ⋯ i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>CommRing 𝕜<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : 0 < n<VAR>v : Fin n → E<GOAL>p.applyComposition (Composition.single n hn) v = fun _j => (p n) v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>CommRing 𝕜<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>c : Composition n<GOAL>p.removeZero.applyComposition c = p.applyComposition c
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>CommRing 𝕜<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>c : Composition n<VAR>j : Fin n<VAR>v : Fin n → E<VAR>z : E<GOAL>p.applyComposition c (Function.update v j z) = Function.update (p.applyComposition c v) (c.index j) ((p (c.blocksFun (c.index j))) (Function.update (v ∘ ⇑(c.embedding (c.index j))) (c.invEmbedding j) z))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>CommRing 𝕜<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>AddCommGroup G<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>Module 𝕜 G<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>TopologicalSpace G<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>TopologicalAddGroup G<VAR>ContinuousConstSMul 𝕜 G<VAR>n : ℕ<VAR>p : FormalMultilinearSeries 𝕜 F G<VAR>f : E →L[𝕜] F<VAR>c : Composition n<VAR>v : Fin n → E<GOAL>(p.compContinuousLinearMap f).applyComposition c v = p.applyComposition c (⇑f ∘ v)