1. notice
  3. English
  5. logic-topic
  6. 1. logic
  7. 2. set-theory
  8. 3. map
  9. 4. order
  10. 5. combinatorics
  12. calculus
  13. 6. real-numbers
  14. 7. limit-sequence
  15. 8. ℝ^n
  16. 9. Euclidean-space
  17. 10. Minkowski-space
  18. 11. polynomial
  19. 12. analytic-Euclidean
  20. 13. analytic-Minkowski
  21. 14. analytic-struct-operation
  22. 15. ordinary-differential-equation
  23. 16. volume
  24. 17. integral
  25. 18. divergence
  26. 19. limit-net
  27. 20. topology
  28. 21. compact
  29. 22. connected
  30. 23. topology-struct-operation
  31. 24. exponential
  32. 25. angle
  34. geometry
  35. 26. manifold
  36. 27. metric
  37. 28. metric-connection
  38. 29. geodesic-derivative
  39. 30. curvature-of-metric
  40. 31. Einstein-metric
  41. 32. constant-sectional-curvature
  42. 33. simple-symmetric-space
  43. 34. principal-bundle
  44. 35. group-action
  45. 36. stereographic-projection
  46. 37. Hopf-bundle
  48. field-theory
  49. 38. point-particle-non-relativity
  50. 39. point-particle-relativity
  51. 40. scalar-field
  52. 41. scalar-field-current
  53. 42. scalar-field-non-relativity
  54. 43. projective-lightcone
  55. 44. spacetime-momentum-spinor-representation
  56. 45. Lorentz-group
  57. 46. spinor-field
  58. 47. spinor-field-current
  59. 48. electromagnetic-field
  60. 49. Laplacian-of-tensor-field
  61. 50. Einstein-metric
  62. 51. interaction
  63. 52. harmonic-oscillator-quantization
  64. 53. spinor-field-misc
  65. 54. reference
  67. 中文
  68. 55. notice
  70. 逻辑
  71. 56. 逻辑
  72. 57. 集合论
  73. 58. 映射
  74. 59. 序
  75. 60. 组合
  77. 微积分
  78. 61. 实数
  79. 62. 数列极限
  80. 63. ℝ^n
  81. 64. Euclidean 空间
  82. 65. Minkowski 空间
  83. 66. 多项式
  84. 67. 解析 (Euclidean)
  85. 68. 解析 (Minkowski)
  86. 69. 解析 struct 的操作
  87. 70. 常微分方程
  88. 71. 体积
  89. 72. 积分
  90. 73. 散度
  91. 74. 网极限
  92. 75. 拓扑
  93. 76. 紧致
  94. 77. 连通
  95. 78. 拓扑 struct 的操作
  96. 79. 指数函数
  97. 80. 角度
  99. 几何
  100. 81. 流形
  101. 82. 度规
  102. 83. 度规的联络
  103. 84. Levi-Civita 导数
  104. 85. 度规的曲率
  105. 86. Einstein 度规
  106. 87. 常截面曲率
  107. 88. simple-symmetric-space
  108. 89. 主丛
  109. 90. 群作用
  110. 91. 球极投影
  111. 92. Hopf 丛
  113. 场论
  114. 93. 非相对论点粒子
  115. 94. 相对论点粒子
  116. 95. 纯量场
  117. 96. 纯量场的守恒流
  118. 97. 非相对论纯量场
  119. 98. 光锥射影
  120. 99. 时空动量的自旋表示
  121. 100. Lorentz 群
  122. 101. 旋量场
  123. 102. 旋量场的守恒流
  124. 103. 电磁场
  125. 104. 张量场的 Laplacian
  126. 105. Einstein 度规
  127. 106. 相互作用
  128. 107. 谐振子量子化
  129. 108. 旋量场杂项
  130. 109. 参考

note-math

自然数 的加法

是数 次 , 是先数 次, 再数 次

  • 结合律:
  • 交换律:

Proof 在现实世界的直观是, 对于数数 , 无论怎样把数数任务手动分成几个子任务, 都不会影响结果, 而且总的分解方式有限. 加法结合律和交换律只是其中的特殊情况. 就像我们通过数数来认识自然数一样, 我们总是可以通过数数认识交换律和结合律. 所有东西都 reduce to 完全加法分解的情况, 只有大量 的交换律和结合律

有两种加法的定义, 或者 . 在一种加法定义中通过 (在中途) 交换输入, 可以得到另一种加法定义. 证明加法交换性就是证明这两种定义对相同的输入给出相同的输出结果. 直觉上当然是结果相同的, 只是把要数数的量放到了不同的 "插槽位置", 从而有 "交换性"

或者, 对两个位置的数数 的函数, 一个位置 先数数后作为 "基础位置", 另一位置 再数数作为 "增值位置", 得到的结果是 "总的数数" . 交换律就是, 交换两个位置进行操作, 结果还是相同, 应该都是 "总的数数"

自然数 的乘法

是数 次的数 次

也满足交换律和结合律. 在现实世界的直观是 "二维和三维矩形", 对于数数 , 无论分解成怎么样的 product 分解的子任务, 都不影响结果. 所以乘法交换律和结合律只是完全乘法分解 i.e. 素数分解的特殊情况, 而且总分解次数有限

自然数运算分配律

直观是用二维矩形的边长的 sum 分解

整数

数轴有两个方向

有理数

等分操作, 乘法的逆

不要混淆于 的除, 余, 那是一个数 另一个数 的逐次减法, 而不是等分

实数

实数的一种直观是长度. 或者包含有理数 + 线序 + 序完备

鉴于实数的直观性, 可以认为它存在, 用很多公理去定义实数 i.e. 假设 true proposition. 但也可以从有理数 "恢复" 实数

无理数的例子

代数整数

代数整数里的 "整数" 是因为

Proof (p.43 of ref-8)

取 互素. 代入方程, 乘

右边被 整除. 但 互素, 所以 或 .

从而 . 从而

特殊情况 . 但是 且

所以 即 不是有理数

代数数

注意不要求 , 不限制 , 包含所有有理数 , 部分无理数 e.g.

代数数 是可数集, 实数 是不可数集

超越数 . 是超越数

十进制, 二进制 vs 区间套 vs 分割

十进制 (区间套) 似乎很直观

然而十进制并不能原生地处理

很多不同 区间套有相同极限, e.g. vs , 需要 limit-distance-vanish 系 quotient

let . let and , 定义 的 limit-distance-vanish 等价关系 (alias Cauchy 收敛) :=

可以把 有理数区间套改为一般的长度 极限 趋于零的有理数区间 线序链 或者更一般的长度趋于零的有理数区间 (极大的) 网

有理数区间是子集 with property 序不中断

从操作简单性来说, 应该用 Dedekind-cut. "操作简单" 是指

  • let , 一一对应
  • 所以 和 一一对应

[Dedekind-cut] 无理数

一一对应到

. 将 重新记为

实数

逻辑上等价地可以只使用一半, 例如, 有理数 的任何左半无限区间, 然后自动通过做 中的补集得到右半无限区间. 但这里用更对称的表示

  • [order-real] 序

let

  • [add-real] 加法. let

由于 的存在, 乘法不保持序. 但是 的乘法保持序. 先处理 的情况, 再用反射 得到 的情况

  • [multiply-real] 乘法. let

的 都有结合律, 交换律, 分配律

实际上, 对于乘法及其定理来说, 相对于用 Dedekind 分割和线序处理乘法, 可能更方便的做法是有理区间网的极限来处理 (网介于偏序和线序之间)

[completeness-real] 完备性

[exact-bound] 确界原理

let 有上界

上确界

[monotone-convergence] 单调有界 收敛 Proof use 确界原理

[nested-closed-interval-theorem] 闭区间套定理

无论是 区间套还是 线序链区间套, 线序意味着区间端点单调性, 对小端点集用上确界 , 对大端点集用下确界 , 得到 with 得到闭区间套交集是闭区间 . 可以理解为 线序链区间套的最小元

[closed-interval-intersection-theorem]

实际上, 只需要闭区间族的小端点都 大端点, 即可得到交集非空

Proof 同理, 对小端点用上确界 , 对大端点集用下确界 , 得到 with 得到闭区间族交集是闭区间

[closed-interval-net-theorem] 闭区间 网 交集非空

Proof

闭区间网 ==> 闭区间族的小端点都 大端点

反方向 "闭区间族的小端点都 大端点 ==> 区间网" 不成立, 考虑只有两个区间 且交集非空 且 的闭区间族, 没有第三个区间属于它们的交集. 虽然只要补充交集, 就能满足

let

def 序列 单调递减, 单调递增

[limsup] 上极限

[liminf] 下极限

Example

对于 序列定义

对于一般 net 定义

[limit-distance-vanish-sequence] := . i.e. tail distance vanish

[limit-distance-vanish-net] :=

[Cauchy-completeness-real] limit-distance-vanish 序列 or net 收敛

Proof

limit-distance-vanish ==>

let , then

==> limit-distance-vanish 序列有界

==> 单调增减有界序列 有极限

limit-distance-vanish 性质 ==>

从而 收敛到

对网, 使用网的集合的上下确界, 使用 limit-distance-vanish-net 得到 net 收敛

反过来, 收敛序列是 limit-distance-vanish 的. by 三角不等式

序列 or net 收敛到 <==> limit-distance-vanish

[uncountable-real] 实数不可数

已经证明了 . cf. cardinal-increase

recall

Proof

根据区间套定理, 实数的二进制小数点表示: 第 位取 或

==> . 其中, 把二进制中可能的两种等价的选择 quotient

by 线性映射 or 仿射映射

by

Proof

它代表二进制中, 出现的第一个位置是 , 第二个位置是 …

对比 , vs

距离