@@ -3,83 +3,82 @@ import SciLean.Analysis.AdjointSpace.CanonicalBasis
33
44namespace SciLean
55
6- #exit
7- class TensorProductCurry (𝕜 X Y Z : Type *)
8- [RCLike 𝕜]
9- [NormedAddCommGroup X] [AdjointSpace 𝕜 X]
10- [NormedAddCommGroup Y] [AdjointSpace 𝕜 Y]
11- [NormedAddCommGroup Z] [AdjointSpace 𝕜 Z]
12- {XY : Type *} [NormedAddCommGroup XY] [AdjointSpace 𝕜 XY]
13- [TensorProductType 𝕜 X Y XY]
14- where
15- tcurry : (X ⊗[𝕜] Y →L[𝕜] Z) ≃L[𝕜] (X →L[𝕜] Y →L[𝕜] Z)
16-
17- export TensorProductCurry (tcurry)
18-
19- class TensorBasis (𝕜 X Y XY : Type *)
20- [RCLike 𝕜] [NormedAddCommGroup X] [AdjointSpace 𝕜 X]
21- [NormedAddCommGroup Y] [AdjointSpace 𝕜 Y]
22- {XY : Type *} [NormedAddCommGroup XY] [AdjointSpace 𝕜 XY] [TensorProductType 𝕜 X Y XY]
23- {I} [Fintype I] [CanonicalBasis I 𝕜 X]
24- {J} [Fintype J] [CanonicalBasis J 𝕜 Y]
25- [CanonicalBasis (I×J) 𝕜 XY] : Prop where
26- basis_eq_tmul_basis : ∀ i j, ⅇ[𝕜,XY,(i,j)] = ⅇ[𝕜,X,i] ⊗[𝕜] ⅇ[𝕜,Y,j]
27-
28-
29- variable
30- {𝕜 X Y Z W : Type *}
31- [RCLike 𝕜]
32- [NormedAddCommGroup X] [AdjointSpace 𝕜 X]
33- [NormedAddCommGroup Y] [AdjointSpace 𝕜 Y]
34- [NormedAddCommGroup Z] [AdjointSpace 𝕜 Z]
35- [NormedAddCommGroup W] [AdjointSpace 𝕜 W]
36- {XY : Type *} [NormedAddCommGroup XY] [AdjointSpace 𝕜 XY] [TensorProductType 𝕜 X Y XY]
37- {YX : Type *} [NormedAddCommGroup YX] [AdjointSpace 𝕜 YX] [TensorProductType 𝕜 Y X YX]
38- {ZW : Type *} [NormedAddCommGroup ZW] [AdjointSpace 𝕜 ZW] [TensorProductType 𝕜 Z W ZW]
39- {I} [Fintype I] [CanonicalBasis I 𝕜 X]
40- {J} [Fintype J] [CanonicalBasis J 𝕜 Y]
41- [CanonicalBasis (I×J) 𝕜 XY] [TensorBasis 𝕜 X Y XY]
42-
43-
44- @[fun_prop]
45- theorem tmul.arg_xy.Continuous_rule : Continuous (fun xy : X×Y => xy.1 ⊗[𝕜]xy.2 ) := sorry_proof
46- @[fun_prop]
47- theorem tmul.arg_x.IsContinuousLinearMap_rule (y : Y) : IsContinuousLinearMap 𝕜 (fun x : X => x⊗[𝕜]y) := sorry_proof
48- @[fun_prop]
49- theorem tmul.arg_y.IsContinuousLinearMap_rule (x : X) : IsContinuousLinearMap 𝕜 (fun y : Y => x⊗[𝕜]y) := sorry_proof
50-
51-
52- set_default_scalar 𝕜
53-
6+ -- class TensorProductCurry (𝕜 X Y Z : Type*)
7+ -- [RCLike 𝕜]
8+ -- [NormedAddCommGroup X] [AdjointSpace 𝕜 X]
9+ -- [NormedAddCommGroup Y] [AdjointSpace 𝕜 Y]
10+ -- [NormedAddCommGroup Z] [AdjointSpace 𝕜 Z]
11+ -- {XY : Type*} [NormedAddCommGroup XY] [AdjointSpace 𝕜 XY]
12+ -- [TensorProductType 𝕜 X Y XY]
13+ -- where
14+ -- tcurry : (X ⊗[ 𝕜 ] Y →L[ 𝕜 ] Z) ≃L[ 𝕜 ] (X →L[ 𝕜 ] Y →L[ 𝕜 ] Z)
15+
16+ -- export TensorProductCurry (tcurry)
17+
18+ -- class TensorBasis (𝕜 X Y XY : Type*)
19+ -- [RCLike 𝕜] [NormedAddCommGroup X] [AdjointSpace 𝕜 X]
20+ -- [NormedAddCommGroup Y] [AdjointSpace 𝕜 Y]
21+ -- {XY : Type*} [NormedAddCommGroup XY] [AdjointSpace 𝕜 XY] [TensorProductType 𝕜 X Y XY]
22+ -- {I} [Fintype I] [CanonicalBasis I 𝕜 X]
23+ -- {J} [Fintype J] [CanonicalBasis J 𝕜 Y]
24+ -- [CanonicalBasis (I×J) 𝕜 XY] : Prop where
25+ -- basis_eq_tmul_basis : ∀ i j, ⅇ[ 𝕜,XY,(i,j) ] = ⅇ[ 𝕜,X,i ] ⊗[ 𝕜 ] ⅇ[ 𝕜,Y,j ]
26+
27+
28+ -- variable
29+ -- {𝕜 X Y Z W : Type*}
30+ -- [RCLike 𝕜]
31+ -- [NormedAddCommGroup X] [AdjointSpace 𝕜 X]
32+ -- [NormedAddCommGroup Y] [AdjointSpace 𝕜 Y]
33+ -- [NormedAddCommGroup Z] [AdjointSpace 𝕜 Z]
34+ -- [NormedAddCommGroup W] [AdjointSpace 𝕜 W]
35+ -- {XY : Type*} [NormedAddCommGroup XY] [AdjointSpace 𝕜 XY] [TensorProductType 𝕜 X Y XY]
36+ -- {YX : Type*} [NormedAddCommGroup YX] [AdjointSpace 𝕜 YX] [TensorProductType 𝕜 Y X YX]
37+ -- {ZW : Type*} [NormedAddCommGroup ZW] [AdjointSpace 𝕜 ZW] [TensorProductType 𝕜 Z W ZW]
38+ -- {I} [Fintype I] [CanonicalBasis I 𝕜 X]
39+ -- {J} [Fintype J] [CanonicalBasis J 𝕜 Y]
40+ -- [CanonicalBasis (I×J) 𝕜 XY] [TensorBasis 𝕜 X Y XY]
41+
42+
43+ -- @[ fun_prop ]
44+ -- theorem tmul.arg_xy.Continuous_rule : Continuous (fun xy : X×Y => xy.1⊗[ 𝕜 ] xy.2) := sorry_proof
45+ -- @[ fun_prop ]
46+ -- theorem tmul.arg_x.IsContinuousLinearMap_rule (y : Y) : IsContinuousLinearMap 𝕜 (fun x : X => x⊗[ 𝕜 ] y) := sorry_proof
47+ -- @[ fun_prop ]
48+ -- theorem tmul.arg_y.IsContinuousLinearMap_rule (x : X) : IsContinuousLinearMap 𝕜 (fun y : Y => x⊗[ 𝕜 ] y) := sorry_proof
49+
50+
51+ -- set_default_scalar 𝕜
52+
53+ -- -- noncomputable
54+ -- -- def tcurry : (X ⊗[ 𝕜 ] Y →L[ 𝕜 ] Z) ≃L[ 𝕜 ] (X →L[ 𝕜 ] Y →L[ 𝕜 ] Z) where
55+ -- -- toFun := fun f => fun x =>L[ 𝕜 ] fun y =>L[ 𝕜 ] f (x⊗y)
56+ -- -- invFun := fun f => fun xy =>L[ 𝕜 ] ∑ (i : I) (j : J), ⟪ⅇ'[ X,i ] ⊗ⅇ'[ Y,j ] , xy⟫ • f ⅇ[ X,i ] ⅇ[ Y,j ]
57+ -- -- map_add' := sorry_proof
58+ -- -- map_smul' := sorry_proof
59+ -- -- left_inv := sorry_proof
60+ -- -- right_inv := sorry_proof
61+ -- -- continuous_toFun := by sorry_proof
62+ -- -- continuous_invFun := by sorry_proof
63+
64+
65+
66+ -- def tcurry (f : X ⊗[ 𝕜 ] Y → Z) (x : X) (y : Y) : Z := f (x⊗y)
67+
68+
69+ -- /--
70+ -- Uncurry bilinear map `f : X → Y → Z` to a linear map over tensor product `X ⊗ Y`
71+
72+ -- It is marker as noncomputable as it is too slow to compute.
73+ -- -/
5474-- noncomputable
55- -- def tcurry : (X ⊗[ 𝕜 ] Y →L[ 𝕜 ] Z) ≃L[ 𝕜 ] (X →L[ 𝕜 ] Y →L[ 𝕜 ] Z) where
56- -- toFun := fun f => fun x =>L[ 𝕜 ] fun y =>L[ 𝕜 ] f (x⊗y)
57- -- invFun := fun f => fun xy =>L[ 𝕜 ] ∑ (i : I) (j : J), ⟪ⅇ'[ X,i ] ⊗ⅇ'[ Y,j ] , xy⟫ • f ⅇ[ X,i ] ⅇ[ Y,j ]
58- -- map_add' := sorry_proof
59- -- map_smul' := sorry_proof
60- -- left_inv := sorry_proof
61- -- right_inv := sorry_proof
62- -- continuous_toFun := by sorry_proof
63- -- continuous_invFun := by sorry_proof
64-
65-
66-
67- def tcurry (f : X ⊗[𝕜] Y → Z) (x : X) (y : Y) : Z := f (x⊗y)
75+ -- def tuncurry (f : X → Y → Z) (xy : X⊗Y) : Z := ∑ (i : I) (j : J), ⟪ⅇ[ X,i ] ⊗ⅇ[ Y,j ] , xy⟫ • f ⅇ[ X,i ] ⅇ[ Y,j ]
6876
77+ -- /--
78+ -- Combine two linear maps to a single linear map over the tensor product of its domains and codomains.
6979
70- /--
71- Uncurry bilinear map `f : X → Y → Z` to a linear map over tensor product `X ⊗ Y`
72-
73- It is marker as noncomputable as it is too slow to compute.
74- -/
75- noncomputable
76- def tuncurry (f : X → Y → Z) (xy : X⊗Y) : Z := ∑ (i : I) (j : J), ⟪ⅇ[X,i]⊗ⅇ[Y,j], xy⟫ • f ⅇ[X,i] ⅇ[Y,j]
77-
78- /--
79- Combine two linear maps to a single linear map over the tensor product of its domains and codomains.
80-
81- It is marker as noncomputable as it is too slow to compute.
82- -/
83- noncomputable
84- def tmap (f : X → Z) (g : Y → W) (xy : X⊗Y) : Z⊗W :=
85- ∑ (i : I) (j : J), ⟪ⅇ'[X,i]⊗ⅇ'[Y,j], xy⟫ • (f ⅇ[X,i] ⊗ g ⅇ[Y,j])
80+ -- It is marker as noncomputable as it is too slow to compute.
81+ -- -/
82+ -- noncomputable
83+ -- def tmap (f : X → Z) (g : Y → W) (xy : X⊗Y) : Z⊗W :=
84+ -- ∑ (i : I) (j : J), ⟪ⅇ'[ X,i ] ⊗ⅇ'[ Y,j ] , xy⟫ • (f ⅇ[ X,i ] ⊗ g ⅇ[ Y,j ] )
0 commit comments