雑感・音楽等

音楽・数学・プログラミングに関する,思い付き・雑感を記す.

haskellでテトレーションを計算

 x\uparrow \uparrow yを求める関数.

tetration x y= foldr1 (^) $ take y $ repeat x

シフト演算子の微分

ステップ関数:  H_\lambda(t) = 
\begin{cases}
0 & ( 0 \leq t< \lambda ) \\
1 & ( 0 \leq \lambda < t )
\end{cases}
シフト演算子:  h^\lambda = s \{ H_\lambda(t) \}
 h^\lambda = s \{ H_\lambda(t) \}=s^2 \{ h_1 (\lambda , t) \}=s^3 \{ h_2 (\lambda , t) \}

 h_1 (\lambda, t )  = - \frac{\partial}{\partial \lambda} h_2 ( \lambda , t) =
\begin{cases}
0 & ( 0 \leq t< \lambda ) \\
t-\lambda & ( 0 \leq \lambda \leq t )
\end{cases}
 h_2 (\lambda, t )  =
\begin{cases}
0 & ( 0 \leq t \leq \lambda ) \\
\frac{1}{2} (t-\lambda)^2 & ( 0 \leq \lambda < t )
\end{cases}

シフト演算子微分:  (h^\lambda)' = s^3 \left\{\frac{\partial}{\partial \lambda} h_2 (\lambda, t)\right\} \\
 = s^3 \{ -h_1 (\lambda, t) \} = -s \cdot s^2 \{ h_1 (\lambda, t) \} \\ = -s h^\lambda

文献

  • ヤン・ミクシンスキー. 演算子法: 上巻. 松村英之, 松浦重武訳. 新版, 裳華房, 299p.


関数に対する微分演算子sの作用

積分演算子: l=\left\{ 1 \right\}
微分演算子: s=\frac{1}{l}=\frac{1}{\left\{ 1 \right\}}
関数:  f(t), \, g(t)
定数:  k

以下が成立する.
\left\{ f(t) \right\}+\left\{ g(t) \right\} = \left\{ f(t)+g(t) \right\}.
\left\{ f(t) \right\}\left\{ g(t) \right\} = \left\{ \int^t_0 f(x)g(t-x)dx \right\}.
 k \left\{ 1 \right\}=lk=\left\{ k \right\}.
l\left\{ f(t) \right\}=\left\{ 1 \right\}\left\{ f(t) \right\}= \left\{ \int^t_0 1 \cdot f(x)dx \right\}.
ls=sl=\frac{\left\{ 1 \right\}}{\left\{ 1 \right\}}=1.

微分演算子微分作用

 \left\{ f(t) \right\} =\left\{ f(t)-f(0)+f(0) \right\}  =  \left\{ \left[ f(x) \right]^{x=t}_{x=0}+ f(0) \right\} \\ = \left\{ \int^{t}_{0} f'(x) dx+ a(0) \right\} = \left\{ \int^{t}_{0} 1 \cdot f'(x) dx\right\}+\left\{ f(0) \right\} \\ 
 = l \left\{ f'(t) \right\}+l\,f(0).
辺々に微分演算子sを掛ける.
 s\left\{ f(t) \right\} = sl \left\{ f'(t) \right\}+sl\,f(0) =  \left\{ f'(t) \right\}+f(0)  .

文献

  • ヤン・ミクシンスキー. 演算子法: 上巻. 松村英之, 松浦重武訳. 新版, 裳華房, 299p.

発散・回転・勾配の連鎖(ベクトル解析)

\phi,\, \psi: スカラ
\boldsymbol{A}\, \boldsymbol{B}:ベクタ
div\, \boldsymbol{A}=\nabla \cdot \boldsymbol{A}: ベクタ→スカラ
grad\, \phi=\nabla \phi: スカラ→ベクタ
rot\, \boldsymbol{A}=\nabla \times \boldsymbol{A}: ベクタ→ベクタ
\Delta \boldsymbol{A}=(\nabla \cdot \nabla) \boldsymbol{A} \neq \nabla(\nabla \cdot \boldsymbol{A})

ベクタ grad \,(div \, \boldsymbol{A})=\boldsymbol{B} NG div \,(div \, \boldsymbol{A}) NG rot \,(div \, \boldsymbol{A})
NG grad \,(grad \,\phi) スカラ div \,(grad \,\phi)=\Delta \phi ベクタ rot \,(grad \,\phi)=\boldsymbol{0}
NG grad \,(rot \, \boldsymbol{A}) スカラ div \,(rot \, \boldsymbol{A})=0 ベクタ rot \,(rot \, \boldsymbol{A})\\=grad \,(div \, \boldsymbol{A})-\Delta \boldsymbol{A}
ベクタ \nabla(\nabla \cdot \boldsymbol{A})=\boldsymbol{B} NG \nabla\cdot(\nabla \cdot \boldsymbol{A}) NG \nabla\times(\nabla \cdot \boldsymbol{A})
NG \nabla(\nabla\phi) スカラ \nabla\cdot(\nabla\phi)=\Delta \phi ベクタ \nabla\times(\nabla\phi)=\boldsymbol{0}
NG \nabla(\nabla \times \boldsymbol{A}) スカラ \nabla\cdot(\nabla \times \boldsymbol{A})=0 ベクタ \nabla\times(\nabla \times \boldsymbol{A})\\=\nabla(\nabla \cdot \boldsymbol{A})-\Delta \boldsymbol{A}

命題論理のメモ "Theorem syl5"の証明

syl5 - Metamath Proof Explorer
syl5 - Intuitionistic Logic Explorer


Hypothesis

Ref Expression
syl5.1 ⊢(𝜑→𝜓)
syl5.2 ⊢(𝜒→(𝜓→𝜃))

Assertion

Ref Expression
syl5 ⊢(𝜒→(𝜑→𝜃))


Proof of Theorem com12

Step Hyp Ref Expression
1 syl5.1 ⊢(𝜑→𝜓)
2 1 a1i ⊢(𝜒→(𝜑→𝜓))
3 syl5.2 ⊢(𝜒→(𝜓→𝜃))
4 3 a1i ⊢(𝜒→(𝜑→(𝜓→𝜃)))
5 4 a2d ⊢(𝜒→((𝜑→𝜓)→(𝜑→𝜃)))
6 5 a2i ⊢( (𝜒→(𝜑→𝜓)) → (𝜒→(𝜑→𝜃)) )
7 2, 6 ax-mp ⊢(𝜒→(𝜑→𝜃))

積と微分でつながる4つの物理量の構造

教わったことの受け売り.

構造の共通が興味深く,美しいと思った.


電磁気学の図で電荷・磁束を結ぶメモリスタという素子は,
抵抗・キャパシタ・インダクタと比べて,最近実現された素子らしい.

力学の図で,電荷・磁束に対応するのは運動量・位置だが,
不確定性原理によると,これらの物理量は1対1対応には出来ないようだ.

電磁気学

f:id:kazmus:20170502000542j:plain
電圧:v
電流:i
電荷:q
磁束:φ

抵抗:R
静電容量:C
インダクタンス:L
メモリスタンス:M

力学

f:id:kazmus:20170502002251j:plain
速度:v
力:F
運動量:p
位置:x

ダンパの減衰定数:c
質量:m
バネ定数:k

命題論理のメモ "Theorem com12"の証明

com12 - Metamath Proof Explorer
com12 - Intuitionistic Logic Explorer

Hypothesis

Ref Expression
com12.1 ⊢(𝜑→(𝜓→𝜒))

Assertion

Ref Expression
com12 ⊢(𝜓→(𝜑→𝜒))


Proof of Theorem com12

Step Hyp Ref Expression
1 com12.1 ⊢(𝜑→(𝜓→𝜒))
2 ax-2 ⊢((𝜑→(𝜓→𝜒))→((𝜑→𝜓)→(𝜑→𝜒)))
3 1, 2 ax-mp ⊢((𝜑→𝜓)→(𝜑→𝜒))
4 ax-1 ⊢( ((𝜑→𝜓)→(𝜑→𝜒)) →( 𝜓 → ((𝜑→𝜓)→(𝜑→𝜒)) ))
5 3, 4 ax-mp ⊢(𝜓→((𝜑→𝜓)→(𝜑→𝜒)))
6 ax-2 ⊢( (𝜓→((𝜑→𝜓)→(𝜑→𝜒))) → ((𝜓→(𝜑→𝜓))→(𝜓→(𝜑→𝜒))) )
7 5, 6 ax-mp ⊢( (𝜓→(𝜑→𝜓)) → (𝜓→(𝜑→𝜒)) )
8 ax-1 ⊢(𝜓→(𝜑→𝜓))
9 7, 8 ax-mp ⊢(𝜓→(𝜑→𝜒))