Mercurial > hg > Members > kono > Proof > HyperReal

comparison src/HyperReal.agda @ 22:942f4e528a79 default tip

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 Fri, 09 Jul 2021 11:11:10 +0900
parents 5e4b38745a39
children
comparison
equal deleted inserted replaced
21:5e4b38745a39 22:942f4e528a79
186 HRzero (hr i j nz ) = HZzero i 186 HRzero (hr i j nz ) = HZzero i
187 187
188 R0 : HyperR 188 R0 : HyperR
189 R0 = hr (hZ 0 0) (h 1) {!!} 189 R0 = hr (hZ 0 0) (h 1) {!!}
190 190
191 R1 : HyperR
192 R1 = hr (hZ 1 0) (h 1) {!!}
193
191 record Rational : Set where 194 record Rational : Set where
192 field 195 field
193 rp rm k : ℕ 196 rp rm k : ℕ
194 0<k : 0 < k 197 0<k : 0 < k
195 198
196 hR : ℕ → ℕ → (k : HyperNat ) → ((i : ℕ) → 0 < k i) → HyperR 199 hR : ℕ → ℕ → (k : HyperNat ) → ((i : ℕ) → 0 < k i) → HyperR
197 hR x y k ne = hr (hZ x y) k ne 200 hR x y k ne = hr (hZ x y) k ne
198 201
199 rH : (r : Rational ) → HyperR 202 rH : (r : Rational ) → HyperR
200 rH r = hr (hZ (Rational.rp r) (Rational.rm r)) (h (Rational.k r)) {!!} 203 rH r = hr (hZ (Rational.rp r) (Rational.rm r)) (h (Rational.k r)) {!!}
204
205 nH : (r : ℕ ) → HyperR
206 nH r = hr (hZ r 0) (h 1) {!!}
201 207
202 -- 208 --
203 -- z0 / y0 = z1 / y1 ← z0 * y1 = z1 * y0 209 -- z0 / y0 = z1 / y1 ← z0 * y1 = z1 * y0
204 -- 210 --
205 _h=_ : (i j : HyperR ) → Set 211 _h=_ : (i j : HyperR ) → Set
254 record Standard : Set where 260 record Standard : Set where
255 field 261 field
256 standard : HyperR → HyperR 262 standard : HyperR → HyperR
257 is-standard : {x : HyperR } → x ≈ standard x 263 is-standard : {x : HyperR } → x ≈ standard x
258 standard-unique : {x y : HyperR } → x ≈ y → standard x ≡ standard y 264 standard-unique : {x y : HyperR } → x ≈ y → standard x ≡ standard y
259 st-inifinitesimal : {x : HyperR } → inifinitesimal-R x → st x ≡ R0 265 st-inifinitesimal : {x : HyperR } → inifinitesimal-R x → standard x ≡ R0
266 st-ℕ : {x : HyperR } → { i : ℕ } → x ≈ nH i → standard x ≡ nH i
260 267
261 postulate 268 postulate
262 ST : Standard 269 ST : Standard
263 270
264 open Standard 271 open Standard
265 272
266 st : HyperR → HyperR 273 st : HyperR → HyperR
267 st x = standard ST x 274 st x = standard ST x
268 275
269 276 open import Algebra.Structures
270 277 open import Algebra.Bundles
278
279 HRing : CommutativeRing Level.zero Level.zero
280 HRing = record {
281 Carrier = HyperR
282 ; _≈_ = _h=_
283 ; _+_ = _h+_
284 ; _*_ = _h*_
285 ; -_ = -h
286 ; 0# = R0
287 ; 1# = R1
288 ; isCommutativeRing = {!!}
289 }
290
291
292 transfer : ( p : Rational ∨ HyperR → Set )
293 → ((x : Rational ) → p (case1 x) )
294 → ((x : HyperR ) → p (case2 x))
295 transfer = {!!}