ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>n : ℕ<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>c : Composition n<VAR>f : ContinuousMultilinearMap 𝕜 (fun _i => F) G<VAR>v : Fin n → E<GOAL>(ContinuousMultilinearMap.compAlongComposition p c f) v = f (p.applyComposition c v)
<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>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>c : Composition n<VAR>v : Fin n → E<GOAL>(q.compAlongComposition p c) v = (q c.length) (p.applyComposition c v)
<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>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>v : Fin 0 → E<VAR>v' : Fin 0 → F<GOAL>(q.comp p 0) v = (q 0) v'
<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>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>v : Fin 0 → E<GOAL>(q.comp p 0) v = (q 0) fun _i => 0
<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>q : FormalMultilinearSeries 𝕜 E F<VAR>p : FormalMultilinearSeries 𝕜 E E<GOAL>q.comp p 0 = q 0
<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>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>v : Fin 1 → E<GOAL>(q.comp p 1) v = (q 1) fun _i => (p 1) v
<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>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>q.removeZero.comp p n = q.comp p n
<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>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<GOAL>q.comp p.removeZero = q.comp p
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>c : Composition n<VAR>f : ContinuousMultilinearMap 𝕜 (fun _i => F) G<VAR>v : Fin n → E<GOAL>‖(ContinuousMultilinearMap.compAlongComposition p c f) v‖ ≤ (‖f‖ * ∏ i : Fin c.length, ‖p (c.blocksFun i)‖) * ∏ i : Fin n, ‖v i‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>c : Composition n<GOAL>‖q.compAlongComposition p c‖ ≤ ‖q c.length‖ * ∏ i : Fin c.length, ‖p (c.blocksFun i)‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>c : Composition n<GOAL>‖q.compAlongComposition p c‖₊ ≤ ‖q c.length‖₊ * ∏ i : Fin c.length, ‖p (c.blocksFun i)‖₊
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>v : Fin 1 → E<GOAL>(FormalMultilinearSeries.id 𝕜 E 1) v = v 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>n : ℕ<VAR>h : n = 1<VAR>v : Fin n → E<GOAL>(FormalMultilinearSeries.id 𝕜 E n) v = v ⟨0, ⋯⟩
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>n : ℕ<VAR>h : n ≠ 1<GOAL>FormalMultilinearSeries.id 𝕜 E n = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<GOAL>p.comp (FormalMultilinearSeries.id 𝕜 E) = p
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>h : p 0 = 0<GOAL>(FormalMultilinearSeries.id 𝕜 F).comp p = p
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hq : 0 < q.radius<VAR>hp : 0 < p.radius<GOAL>∃ r > 0, Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>hr : Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst<GOAL>↑r ≤ (q.comp p).radius
<VAR>m M N : ℕ<VAR>i : (n : ℕ) × (Fin n → ℕ)<GOAL>i ∈ FormalMultilinearSeries.compPartialSumSource m M N ↔ (m ≤ i.fst ∧ i.fst < M) ∧ ∀ (a : Fin i.fst), 1 ≤ i.snd a ∧ i.snd a < N
<VAR>m M N : ℕ<VAR>i : (n : ℕ) × (Fin n → ℕ)<VAR>hi : i ∈ FormalMultilinearSeries.compPartialSumSource m M N<GOAL>(FormalMultilinearSeries.compChangeOfVariables m M N i hi).snd.length = i.fst
<VAR>m M N : ℕ<VAR>i : (n : ℕ) × (Fin n → ℕ)<VAR>hi : i ∈ FormalMultilinearSeries.compPartialSumSource m M N<VAR>j : Fin i.fst<GOAL>(FormalMultilinearSeries.compChangeOfVariables m M N i hi).snd.blocksFun ⟨↑j, ⋯⟩ = i.snd j
<VAR>m M N : ℕ<VAR>i : (n : ℕ) × Composition n<VAR>hi : i ∈ FormalMultilinearSeries.compPartialSumTargetSet m M N<GOAL>∃ j, ∃ (hj : j ∈ FormalMultilinearSeries.compPartialSumSource m M N), FormalMultilinearSeries.compChangeOfVariables m M N j hj = i
<VAR>m M N : ℕ<VAR>a : (n : ℕ) × Composition n<GOAL>a ∈ FormalMultilinearSeries.compPartialSumTarget m M N ↔ m ≤ a.snd.length ∧ a.snd.length < M ∧ ∀ (j : Fin a.snd.length), a.snd.blocksFun j < N
<VAR>α : Type u_6<VAR>AddCommMonoid α<VAR>m M N : ℕ<VAR>f : (n : ℕ) × (Fin n → ℕ) → α<VAR>g : (n : ℕ) × Composition n → α<VAR>h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ FormalMultilinearSeries.compPartialSumSource m M N), f e = g (FormalMultilinearSeries.compChangeOfVariables m M N e he)<GOAL>∑ e ∈ FormalMultilinearSeries.compPartialSumSource m M N, f e = ∑ e ∈ FormalMultilinearSeries.compPartialSumTarget m M N, g e
<GOAL>Filter.Tendsto (fun N => FormalMultilinearSeries.compPartialSumTarget 0 N N) Filter.atTop Filter.atTop
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>N : ℕ<VAR>z : E<GOAL>q.partialSum N (∑ i ∈ Finset.Ico 1 N, (p i) fun _j => z) = ∑ i ∈ FormalMultilinearSeries.compPartialSumTarget 0 N N, (q.compAlongComposition p i.snd) fun _j => z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>g : F → G<VAR>f : E → F<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>hg : HasFPowerSeriesAt g q (f x)<VAR>hf : HasFPowerSeriesAt f p x<GOAL>HasFPowerSeriesAt (g ∘ f) (q.comp p) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>g : F → G<VAR>f : E → F<VAR>x : E<VAR>hg : AnalyticAt 𝕜 g (f x)<VAR>hf : AnalyticAt 𝕜 f x<GOAL>AnalyticAt 𝕜 (g ∘ f) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>g : F → G<VAR>f : E → F<VAR>y : F<VAR>x : E<VAR>hg : AnalyticAt 𝕜 g y<VAR>hf : AnalyticAt 𝕜 f x<VAR>hy : f x = y<GOAL>AnalyticAt 𝕜 (g ∘ f) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>g : F → G<VAR>f : E → F<VAR>hg : AnalyticOn 𝕜 g (f '' s)<VAR>hf : AnalyticOn 𝕜 f s<GOAL>AnalyticOn 𝕜 (g ∘ f) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>t : Set F<VAR>g : F → G<VAR>f : E → F<VAR>hg : AnalyticOn 𝕜 g t<VAR>hf : AnalyticOn 𝕜 f s<VAR>st : Set.MapsTo f s t<GOAL>AnalyticOn 𝕜 (g ∘ f) s
<VAR>n : ℕ<VAR>i j : (a : Composition n) × Composition a.length<GOAL>i = j ↔ i.fst.blocks = j.fst.blocks ∧ i.snd.blocks = j.snd.blocks
<VAR>n : ℕ<VAR>u v : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))<GOAL>u = v ↔ (List.ofFn fun i => (u.snd i).blocks) = List.ofFn fun i => (v.snd i).blocks
<VAR>n : ℕ<VAR>a : Composition n<VAR>b : Composition a.length<GOAL>(a.gather b).length = b.length
<VAR>n : ℕ<VAR>a : Composition n<VAR>b : Composition a.length<VAR>i : Fin b.length<GOAL>(a.sigmaCompositionAux b ⟨↑i, ⋯⟩).length = b.blocksFun i
<VAR>n : ℕ<VAR>a : Composition n<VAR>b : Composition a.length<VAR>i : Fin b.length<VAR>j : Fin (b.blocksFun i)<GOAL>(a.sigmaCompositionAux b ⟨↑i, ⋯⟩).blocksFun ⟨↑j, ⋯⟩ = a.blocksFun ((b.embedding i) j)
<VAR>n : ℕ<VAR>a : Composition n<VAR>b : Composition a.length<VAR>i j : ℕ<VAR>hi : i < b.length<VAR>hj : j < b.blocksFun ⟨i, hi⟩<GOAL>a.sizeUpTo (b.sizeUpTo i + j) = (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>r : FormalMultilinearSeries 𝕜 G H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<GOAL>(r.comp q).comp p = r.comp (q.comp p)
<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>A : E →L[𝕜] F<VAR>x : F<GOAL>(ContinuousLinearMap.adjointAux A) x = (InnerProductSpace.toDual 𝕜 E).symm ((ContinuousLinearMap.toSesqForm A) x)
<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>A : E →L[𝕜] F<VAR>x : E<VAR>y : F<GOAL>⟪(ContinuousLinearMap.adjointAux A) y, x⟫_𝕜 = ⟪y, A x⟫_𝕜
<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>A : E →L[𝕜] F<VAR>x : E<VAR>y : F<GOAL>⟪x, (ContinuousLinearMap.adjointAux A) y⟫_𝕜 = ⟪A x, y⟫_𝕜
<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>A : E →L[𝕜] F<GOAL>ContinuousLinearMap.adjointAux (ContinuousLinearMap.adjointAux A) = A
<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>A : E →L[𝕜] F<GOAL>‖ContinuousLinearMap.adjointAux A‖ = ‖A‖
<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>A : E →L[𝕜] F<VAR>x : E<VAR>y : F<GOAL>⟪(ContinuousLinearMap.adjoint A) y, x⟫_𝕜 = ⟪y, A x⟫_𝕜
<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>A : E →L[𝕜] F<VAR>x : E<VAR>y : F<GOAL>⟪x, (ContinuousLinearMap.adjoint A) y⟫_𝕜 = ⟪A x, y⟫_𝕜
<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>A : E →L[𝕜] F<GOAL>ContinuousLinearMap.adjoint (ContinuousLinearMap.adjoint A) = A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup G<VAR>InnerProductSpace 𝕜 E<VAR>InnerProductSpace 𝕜 F<VAR>InnerProductSpace 𝕜 G<VAR>CompleteSpace E<VAR>CompleteSpace G<VAR>CompleteSpace F<VAR>A : F →L[𝕜] G<VAR>B : E →L[𝕜] F<GOAL>ContinuousLinearMap.adjoint (A.comp B) = (ContinuousLinearMap.adjoint B).comp (ContinuousLinearMap.adjoint A)
<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>A : E →L[𝕜] F<VAR>x : E<GOAL>‖A x‖ ^ 2 = RCLike.re ⟪((ContinuousLinearMap.adjoint A).comp A) x, x⟫_𝕜
<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>A : E →L[𝕜] F<VAR>x : E<GOAL>‖A x‖ = √(RCLike.re ⟪((ContinuousLinearMap.adjoint A).comp A) x, x⟫_𝕜)
<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>A : E →L[𝕜] F<VAR>x : E<GOAL>‖A x‖ ^ 2 = RCLike.re ⟪x, ((ContinuousLinearMap.adjoint A).comp A) x⟫_𝕜
<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>A : E →L[𝕜] F<VAR>x : E<GOAL>‖A x‖ = √(RCLike.re ⟪x, ((ContinuousLinearMap.adjoint A).comp A) x⟫_𝕜)
<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>A : E →L[𝕜] F<VAR>B : F →L[𝕜] E<GOAL>A = ContinuousLinearMap.adjoint B ↔ ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<GOAL>ContinuousLinearMap.adjoint (ContinuousLinearMap.id 𝕜 E) = ContinuousLinearMap.id 𝕜 E
<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>CompleteSpace ↥U<GOAL>ContinuousLinearMap.adjoint U.subtypeL = orthogonalProjection U
<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>CompleteSpace ↥U<GOAL>ContinuousLinearMap.adjoint (orthogonalProjection U) = U.subtypeL
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>A : E →L[𝕜] E<GOAL>star A = ContinuousLinearMap.adjoint A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>A : E →L[𝕜] E<GOAL>IsSelfAdjoint A ↔ ContinuousLinearMap.adjoint A = A
<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>A : E →L[𝕜] F<GOAL>‖(ContinuousLinearMap.adjoint A).comp A‖ = ‖A‖ * ‖A‖
<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>A : E →L[𝕜] F<GOAL>sesqFormOfInner.IsAdjointPair sesqFormOfInner ↑A ↑(ContinuousLinearMap.adjoint A)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>A : E →L[𝕜] E<VAR>hA : IsSelfAdjoint A<GOAL>ContinuousLinearMap.adjoint A = A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>A : E →L[𝕜] E<VAR>hA : IsSelfAdjoint A<GOAL>(↑A).IsSymmetric
<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 : IsSelfAdjoint T<VAR>S : E →L[𝕜] F<GOAL>IsSelfAdjoint (S.comp (T.comp (ContinuousLinearMap.adjoint S)))
<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 : IsSelfAdjoint T<VAR>S : F →L[𝕜] E<GOAL>IsSelfAdjoint ((ContinuousLinearMap.adjoint S).comp (T.comp S))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>A : E →L[𝕜] E<GOAL>IsSelfAdjoint A ↔ (↑A).IsSymmetric
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>A : E →L[𝕜] E<VAR>hA : (↑A).IsSymmetric<GOAL>IsSelfAdjoint A
<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>CompleteSpace ↥U<GOAL>IsSelfAdjoint (U.subtypeL.comp (orthogonalProjection U))
<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 : IsSelfAdjoint T<VAR>U : Submodule 𝕜 E<VAR>CompleteSpace ↥U<GOAL>IsSelfAdjoint (U.subtypeL.comp ((orthogonalProjection U).comp (T.comp (U.subtypeL.comp (orthogonalProjection U)))))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<GOAL>↑↑hT.toSelfAdjoint = T
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>x : E<GOAL>↑hT.toSelfAdjoint x = T x
<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>FiniteDimensional 𝕜 E<VAR>FiniteDimensional 𝕜 F<VAR>A : E →ₗ[𝕜] F<GOAL>LinearMap.toContinuousLinearMap (LinearMap.adjoint A) = ContinuousLinearMap.adjoint (LinearMap.toContinuousLinearMap A)
<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>FiniteDimensional 𝕜 E<VAR>FiniteDimensional 𝕜 F<VAR>A : E →ₗ[𝕜] F<GOAL>LinearMap.adjoint A = ↑(ContinuousLinearMap.adjoint (LinearMap.toContinuousLinearMap A))
<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>FiniteDimensional 𝕜 E<VAR>FiniteDimensional 𝕜 F<VAR>A : E →ₗ[𝕜] F<VAR>x : E<VAR>y : F<GOAL>⟪(LinearMap.adjoint A) y, x⟫_𝕜 = ⟪y, A x⟫_𝕜
<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>FiniteDimensional 𝕜 E<VAR>FiniteDimensional 𝕜 F<VAR>A : E →ₗ[𝕜] F<VAR>x : E<VAR>y : F<GOAL>⟪x, (LinearMap.adjoint A) y⟫_𝕜 = ⟪A x, y⟫_𝕜
<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>FiniteDimensional 𝕜 E<VAR>FiniteDimensional 𝕜 F<VAR>A : E →ₗ[𝕜] F<GOAL>LinearMap.adjoint (LinearMap.adjoint A) = A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup G<VAR>InnerProductSpace 𝕜 E<VAR>InnerProductSpace 𝕜 F<VAR>InnerProductSpace 𝕜 G<VAR>FiniteDimensional 𝕜 E<VAR>FiniteDimensional 𝕜 F<VAR>FiniteDimensional 𝕜 G<VAR>A : F →ₗ[𝕜] G<VAR>B : E →ₗ[𝕜] F<GOAL>LinearMap.adjoint (A ∘ₗ B) = LinearMap.adjoint B ∘ₗ LinearMap.adjoint A
<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>FiniteDimensional 𝕜 E<VAR>FiniteDimensional 𝕜 F<VAR>A : E →ₗ[𝕜] F<VAR>B : F →ₗ[𝕜] E<GOAL>A = LinearMap.adjoint B ↔ ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜
<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>FiniteDimensional 𝕜 E<VAR>FiniteDimensional 𝕜 F<VAR>ι₁ : Type u_5<VAR>ι₂ : Type u_6<VAR>b₁ : Basis ι₁ 𝕜 E<VAR>b₂ : Basis ι₂ 𝕜 F<VAR>A : E →ₗ[𝕜] F<VAR>B : F →ₗ[𝕜] E<GOAL>A = LinearMap.adjoint B ↔ ∀ (i₁ : ι₁) (i₂ : ι₂), ⟪A (b₁ i₁), b₂ i₂⟫_𝕜 = ⟪b₁ i₁, B (b₂ i₂)⟫_𝕜