Mercurial > hg > Members > kono > Proof > HyperReal

comparison src/HyperReal.agda @ 20:a839f149825f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 08 Jul 2021 17:14:30 +0900
parents f0763f51631e
children 5e4b38745a39
comparison
equal deleted inserted replaced
19:f0763f51631e 20:a839f149825f
90 ... | tri≈ ¬a b ¬c = {!!} 90 ... | tri≈ ¬a b ¬c = {!!}
91 ... | tri> ¬a ¬b c = {!!} 91 ... | tri> ¬a ¬b c = {!!}
92 trans1 : {i j k : HyperNat} → i n≤ j → j n≤ k → i n≤ k 92 trans1 : {i j k : HyperNat} → i n≤ j → j n≤ k → i n≤ k
93 trans1 = {!!} 93 trans1 = {!!}
94 94
95 record n-finite (i : HyperNat ) : Set where
96 field
97 val : ℕ
98 is-val : i n= h val
99
100 n-infinite : (i : HyperNat ) → Set
101 n-infinite i = (j : ℕ ) → h j n≤ i
102
103 n-linear : HyperNat
104 n-linear i = i
105
106 n-linear-is-infnite : n-infinite n-linear
107 n-linear-is-infnite i = record { ≤-map = bid ℕ ; ≤-m = i ; is-n≤ = λ k lt → <to≤ lt }
108
109 ¬-infinite-n-finite : (i : HyperNat ) → n-finite i → ¬ n-infinite i
110 ¬-infinite-n-finite = {!!}
95 111
96 data HyperZ : Set where 112 data HyperZ : Set where
97 hz : HyperNat → HyperNat → HyperZ 113 hz : HyperNat → HyperNat → HyperZ
98 114
99 hZ : ℕ → ℕ → HyperZ 115 hZ : ℕ → ℕ → HyperZ
117 _z<_ : (i j : HyperZ ) → Set 133 _z<_ : (i j : HyperZ ) → Set
118 _z<_ (hz x0 y0) (hz x1 y1) = (x0 n+ y1) n< (x1 n+ y0) 134 _z<_ (hz x0 y0) (hz x1 y1) = (x0 n+ y1) n< (x1 n+ y0)
119 135
120 <-cmpz : Trichotomous {Level.zero} _z=_ _z<_ 136 <-cmpz : Trichotomous {Level.zero} _z=_ _z<_
121 <-cmpz (hz x0 y0) (hz x1 y1) = <-cmpn (x0 n+ y1) (x1 n+ y0) 137 <-cmpz (hz x0 y0) (hz x1 y1) = <-cmpn (x0 n+ y1) (x1 n+ y0)
138
139 -z : (i : HyperZ ) → HyperZ
140 -z (hz x y) = hz y x
141
142 z-z=0 : (i : HyperZ ) → (i z+ (-z i)) z= hZ 0 0
143 z-z=0 = {!!}
144
145 z+infinite : (i : HyperZ ) → Set
146 z+infinite i = (j : ℕ ) → hZ j 0 z≤ i
147
148 z-infinite : (i : HyperZ ) → Set
149 z-infinite i = (j : ℕ ) → i z≤ hZ 0 j
122 150
123 import Axiom.Extensionality.Propositional 151 import Axiom.Extensionality.Propositional
124 postulate f-extensionality : { n m : Level} → Axiom.Extensionality.Propositional.Extensionality n m 152 postulate f-extensionality : { n m : Level} → Axiom.Extensionality.Propositional.Extensionality n m
125 153
126 --- x*y ...... 0 0 0 0 ... 154 --- x*y ...... 0 0 0 0 ...
147 175
148 HZzero? : ( i : HyperZ ) → Dec (HZzero i) 176 HZzero? : ( i : HyperZ ) → Dec (HZzero i)
149 HZzero? = {!!} 177 HZzero? = {!!}
150 178
151 data HyperR : Set where 179 data HyperR : Set where
152 hr : HyperZ → (k : HyperNat ) → ¬ (k n= h 0) → HyperR 180 hr : HyperZ → (k : HyperNat ) → ((i : ℕ) → 0 < k i) → HyperR
153 181
154 HZnzero* : {x y : HyperZ } → ¬ ( HZzero x ) → ¬ ( HZzero y ) → ¬ ( HZzero (x z* y) ) 182 HZnzero* : {x y : HyperZ } → ¬ ( HZzero x ) → ¬ ( HZzero y ) → ¬ ( HZzero (x z* y) )
155 HZnzero* {x} {y} nzx nzy nzx*y = {!!} 183 HZnzero* {x} {y} nzx nzy nzx*y = {!!}
156 184
157 HRzero : HyperR → Set 185 HRzero : HyperR → Set
158 HRzero (hr i j nz ) = HZzero i 186 HRzero (hr i j nz ) = HZzero i
159 187
160 hR : ℕ → ℕ → (k : HyperNat ) → ¬ (k n= h 0) → HyperR 188 R0 : HyperR
189 R0 = hr (hZ 0 0) (h 1) {!!}
190
191 record Rational : Set where
192 field
193 rp rm k : ℕ
194 0<k : 0 < k
195
196 hR : ℕ → ℕ → (k : HyperNat ) → ((i : ℕ) → 0 < k i) → HyperR
161 hR x y k ne = hr (hZ x y) k ne 197 hR x y k ne = hr (hZ x y) k ne
198
199 rH : (r : Rational ) → HyperR
200 rH r = hr (hZ (Rational.rp r) (Rational.rm r)) (h (Rational.k r)) {!!}
162 201
163 -- 202 --
164 -- z0 / y0 = z1 / y1 ← z0 * y1 = z1 * y0 203 -- z0 / y0 = z1 / y1 ← z0 * y1 = z1 * y0
165 -- 204 --
166 _h=_ : (i j : HyperR ) → Set 205 _h=_ : (i j : HyperR ) → Set
174 213
175 <-cmph : Trichotomous {Level.zero} _h=_ _h<_ 214 <-cmph : Trichotomous {Level.zero} _h=_ _h<_
176 <-cmph (hr z0 k0 ne0 ) ( hr z1 k1 ne1 ) = <-cmpz (z0 z* (hz k1 (h 0))) (z1 z* (hz k0 (h 0))) 215 <-cmph (hr z0 k0 ne0 ) ( hr z1 k1 ne1 ) = <-cmpz (z0 z* (hz k1 (h 0))) (z1 z* (hz k0 (h 0)))
177 216
178 _h*_ : (i j : HyperR) → HyperR 217 _h*_ : (i j : HyperR) → HyperR
179 hr x k nz h* hr y k₁ nz₁ = hr ( x z* y ) ( k n* k₁ ) (HNnzero* nz nz₁) 218 hr x k nz h* hr y k₁ nz₁ = hr ( x z* y ) ( k n* k₁ ) {!!}
180 219
181 _h+_ : (i j : HyperR) → HyperR 220 _h+_ : (i j : HyperR) → HyperR
182 hr x k nz h+ hr y k₁ nz₁ = hr ( (x z* (hz k hzero)) z+ (y z* (hz k₁ hzero)) ) (k n* k₁) (HNnzero* nz nz₁) 221 hr x k nz h+ hr y k₁ nz₁ = hr ( (x z* (hz k hzero)) z+ (y z* (hz k₁ hzero)) ) (k n* k₁) {!!}
222
223 -h : (i : HyperR) → HyperR
224 -h (hr x k nz) = hr (-z x) k nz
225
226 inifinitesimal-R : (inf : HyperR) → Set
227 inifinitesimal-R inf = ( r : Rational ) → R0 h< rH r → ( -h (rH r) h< inf ) ∧ ( inf h< rH r)
228
229 1/x : HyperR
230 1/x = hr (hZ 1 0) n-linear {!!}
231
232 1/x-is-inifinitesimal : inifinitesimal-R 1/x
233 1/x-is-inifinitesimal r 0<r = ⟪ {!!} , {!!} ⟫
183 234
184 HyperReal : Set 235 HyperReal : Set
185 HyperReal = ℕ → HyperR 236 HyperReal = ℕ → HyperR
186 237
187 HR→HRl : HyperR → HyperReal 238 HR→HRl : HyperR → HyperReal
191 HRl→HR r = hr (hz (λ k → {!!}) (λ k → {!!}) ) factor {!!} where 242 HRl→HR r = hr (hz (λ k → {!!}) (λ k → {!!}) ) factor {!!} where
192 factor : HyperNat 243 factor : HyperNat
193 factor n = {!!} 244 factor n = {!!}
194 fne : (n : ℕ) → ¬ (factor n= h 0) 245 fne : (n : ℕ) → ¬ (factor n= h 0)
195 fne = {!!} 246 fne = {!!}
247
248 _≈_ : (x y : HyperR ) → Set
249 x ≈ y = inifinitesimal-R (x h+ ( -h y ))
250
251 record Real : Set
252 field
253 st : HyperR → HyperR
254 is-st : (x : HyperR ) → x ≈ st x
255 st-unique : (x y : HyperR ) → st x ≡ st y
256
257
258