Coq/SSReflect/MathCompで解析入門の1章の命題を全て証明
はじめにCoqで解析入門の1章にある命題を全て証明してみたので記事を書いてみます。 Coqでの証明大学で記号論理学の授業を受けたことはありますか？記号論理学では数学の命題を証明木を用いて形式的証明をしていましたがCoqでも形式的証明をします。流れは以下です。 数学の命題を論理記号で書きますゴールが表示されるので適切にCoqのTacticを使いますするとゴールが変わるので未証明のゴールがなくなるまで繰り返しTacticを使います Coqでの証明の魅力は 証明が正しいことをCoqが保証してくれること(Coqにバグがあるかもしれませんが多分)証明した定理が他の定理の証明に使えて楽しいところ などです。 やろうと思った背景大学1年生の頃、解析入門を前から読んで途中で理解できなくなって読み直すというのを繰り返していました。 いつか理解したいなと思っていたときに記号論理学の授業を受けて解析入門の証明も
書評『統計のための行列代数』 | Hippocampus's Garden
書評『統計のための行列代数』July 19, 2020 | 21 min read | 3,454 views jabookmathはじめに 『統計のための行列代数』（D. A. Harville 著，伊理正夫 監訳，丸善出版，2012年）を読んだので，まとめと感想を書きます． （そこまでの精読はできていませんが，それでも誤植と思われる箇所が散見されたので，気づいた範囲ですが末尾にまとめておきました．） まとめ+α 原題は『Matrix Algebra from a Statistician’s Perspective』で，統計学者が身につけるべき線形代数の知識や考え方を全2巻でまとめた著名な教科書です．線形代数は重要かつ範囲がとても広く，抑えるべきポイントがわかりづらいと大学時代から感じていたので，こういう応用を見据えた教科書はありがたいです． 一般的な線形代数の教科書ではあまり
測度論の「お気持ち」を最短で理解する - Qiita
# python f = lambda x: ### n = ### S = 0 for k in range(n): S += f(k/n) / n print(S) 簡単ですね． 長方形近似の極限としてのリーマン積分 リーマン積分は，こうした長方形近似の極限として求められます(厳密な定義ではありません4)． $$\int_0^1 f(x) \, dx \; = \; \lim_{n \to \infty} \frac{1}{n} \sum_{k=1}^{n} f\left(a_k\right) \;\;\left(\frac{k-1}{n}\le a_k \le \frac{k}{n}\right) .$$ この式はすぐ後に使います． リーマン積分できない関数 さて，リーマン積分を考えましたが，この考え方を用いて，区間 $[0,1]$ 上で定義される以下の関数 $1_\mathbb{Q
Feature Column from the AMS: Pagerank
Imagine a library containing 25 billion documents but with no centralized organization and no librarians. In addition, anyone may add a document at any time without telling anyone. You may feel sure that one of the documents contained in the collection has a piece of information that is vitally important to you, and, being impatient like most of us, you'd like to find it in a matter of seconds. Ho
ラグランジュ関数の背後にある理論 (Boyd本5章概要) - うどん記
ラグランジュ関数は以下のような形をした制約付き最適化問題を解くために導入される有名な手法です． $\min_{x \in D} f_0(x),$ $\mbox{subject to}$ $f_i(x) \le 0$ $(i=1,2,...,m)$ $h_i(x) = 0$ $(i=1,2,...,p)$ ここで，$D \subseteq \mathbb{R}^n$ は目的関数の定義域で， $f_0,f_1,\cdots,f_m, h_1, \cdots, h_p: D \rightarrow \mathbb{R}$ は任意の関数． この記事では "Convex Optimization" (by Boyd and Vandenberghe) の5章 "Duality" の項を元に，ラグランジュ関数とその背後にある理論について記します．主に記したことは以下のとおりです． ラグランジュ関数の定
Nelder-Mead methodをRで実装した - yasuhisa's blog
最適化理論の課題提出期限が過ぎたと思うので、うpします。この辺の軌跡を書くためのコードです。 www.yasuhisay.info Nelder-Mead methodがどんな手法の説明はこの辺に書いている。一行で要約すると、ヘッセ行列、勾配ベクトルすら使わずに関数値のみで動いていく最適化手法で変数が非常に多いときなどに威力を発揮するような手法です。 課題では(図示するために)2変数の最適化問題となっていますが、コード自体はさらなる多変数でも動くように作ってます。まあ、結局optim関数で実装されているので実際に使うことはないと思うけど、自分でいじりたくなったときのためということで。あと、パラメータを変えたときにTeXをちまちま編集するのが面倒だったので、RでTeXを吐いてincludeするようにしているなど。収束判定は結構微妙なところがあり、論文にもいろいろ書いてあったが面倒だってので定
Introduction to Applied Linear Algebra – Vectors, Matrices, and Least Squares
Introduction to Applied Linear Algebra – Vectors, Matrices, and Least Squares Introduction to Applied Linear Algebra – Vectors, Matrices, and Least Squares Stephen Boyd and Lieven Vandenberghe Cambridge University Press This book is used as the textbook for our own courses ENGR108 (Stanford) and EE133A (UCLA), where you will find additional related material. If you find an error not listed in our
逆行列補題とBFGSへの応用 - Qiita
逆行列補題について まずブロック行列とその逆行列から話を始めよう。 $I_{n},I_{m},P,Q,R,S$をそれぞれ以下の条件を満たす行列とする。 $・I_{n}:n×n単位行列$ , $I_{m}:m×m単位行列$ $・P:n×n行列$ , $Q:n×m行列$ , $R:m×m行列$ , $S:m×n行列$ $・P,Rはそれぞれ逆行列を持つ$ $・P+QRS$ $及び$ $R^{-1}+SP^{-1}Q$ はそれぞれ逆行列を持つ その上で以下のブロック行列を考えよう。 \begin{align} \begin{pmatrix} P & -Q \\ S & R^{-1} \end{pmatrix} &=\begin{pmatrix} I_{n} & -QR \\ 0 & I_{m} \end{pmatrix} \begin{pmatrix} P+QRS & 0 \\ 0 &R^{-1}
a/(b+c)+b/(c+a)+c/(a+b)=4の自然数解(a,b,c)を求める - Qiita
はじめに ちょっと前に、こんな問題が話題になった。 ネタ元はどこか知らないが、僕は以下のサイトで知った。 適当に和訳してみた。 元の出題は果物とか使ってて「数学パズルです〜」みたいな顔をしているが、これは典型的ディオファントス方程式で、途中で楕円曲線が出てくるガチな問題になっている。解説は先のサイトに書いてあるが、いくつか天下りな箇所があるので、そこをちょっと丁寧に解説しつつ、Rubyで解を探してみる。 方針 問題は以下の通り。 上記を満たす「自然数」の組(a,b,c)を求める。すぐに分かる通り、もしひとつの解の組(a,b,c)が求まったら、それぞれ定数倍した(ta, tb, tc)も解となる。従って、大事なのは(a,b,c)の比であり、例えば$c=1$に固定して、(a,b)の有理数解を求める、という問題と等価である。従って、この問題の自由度(実質的な変数の数)は2となる。 さっきの式の分
任意精度演算 - Wikipedia
任意精度演算（にんいせいどえんざん）[1]とは、数値の精度を必要ならいくらでも伸ばしたりできるような演算システム（実際上は利用可能なメモリ容量に制限されるが）による演算である。 概要[編集] 多倍長整数（たばいちょうせいすう）などを内部処理に利用し、必要な桁数の浮動小数点計算を行う。固定長の整数や一般的な固定精度の浮動小数点方式は、ハードウェアで高速に処理できるのに対し、任意精度演算はソフトウェアで実装され、重い処理を必要とする。十進の0.1を2進で表現しようとする場合のように、有限の桁数では表現し切れない場合もあることから、2進でなく十進で処理するものや、有理数演算を併用したりもする。 多倍長演算（たばいちょうえんざん）[2]とも言うが、プログラミング言語によっては、多倍長整数 (特に区別する場合は bigint などと言う) の名前が bignum であることもある。 最近のプログラミ
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
自動微分を実装して理解する（前編） - Qiita