収束とベクトルの理論

Isabelle/HOLに収束理論はありますか？私は∥x(t)∥ ⟶ 0 as t ⟶ ∞を定義する必要があります。収束とベクトルの理論

また、私はベクトル理論を探していますが、私は行列理論を見つけましたが、ベクトル1を見つけることができませんでした。Isabelle/HOLにこのような理論がありますか？

乾杯。

2017-03-27 O.J

コンバージェンスなどは、フィルターで表されます。

filterlim (λt. norm (x t)) (nhds 0) at_top

または、tendsto略語を使用して、⤏はイザベルのシンボル\<longlongrightarrow>である、ことができます

((λt. norm (x t)) ⤏ 0) at_top

のようなものであろうと、あなたのケースでは

（対応documentationを参照してください）略語--->を使用して入力します。

あなたが最初の場所でそのように書いている理由を注意点として、私はそれが

filterlim x (nhds 0) at_top

または、tendsto構文と同等ですと見て、疑問に思って：

(x ⤏ 0) at_top

これらのフィルタの推論は最初は難しいかもしれませんが、限界や他の位相的な概念の統一されたフレームワークを提供するという利点があります。

ベクターについては、~~/src/HOL/Analysis/Analysisをインポートするだけです。それはあなたが必要とするすべてを持っているはずです。理想的には、isabelle jedit -l HOL-AnalysisでIsabelle/jEditを起動して、HOL-Analysisセッションイメージを構築します。その後、システムを起動するたびにIsabelleの分析ライブラリのすべてを処理する必要はありません。

「ベクトル」とは、Φⁿのような具体的な有限次元の実ベクトル空間を意味します。これは、HOL分析の一部である~~/src/HOL/Analysis/Finite_Cartesian_Product.thyによって提供されます。これは、コンポーネントタイプ（おそらくreal）とベクトル空間の次元を指定するインデックスタイプの2つのパラメータを取るvecタイプを提供します。

また、すべての正の整数nにあらかじめ定義されたタイプnがあります。ベクトル空間ℝ³については(real, 3) vecです。型構文もあり、('a, 'n) vecには'a^'nと書くことができます。

出典

2017-03-27 18:25:04

あなたの詳細な説明については、ありがとうございます。「∥x（t）∥⟶0をt⟶∞とすると、xは実ベクトルであり、t（時間）が無限に収束するにつれて、このベクトルの各要素は0に収束すべきである。私はまだIsabelleには困難があります。例えば、x $ iは（ 'a、' b）vecと同じですか？ベクトルと行列の関係（マルチ、追加など）はできますか？ –

はい、 '∥x（t）∥⟶0'と' x（t）⟶0'は完全に等価です。そして、 'x $ i'はベクトル 'x'の$ i $番目の成分であり、'（' a、 'b）vec'は成分の型が '' a'のベクトルの* type *です。寸法は「b」である。私。 '（real、3）vec'は³3に対応します。ベクトル/行列の加算は '+'で、ベクトルの内積は '∙'（\ ）、行列の乗算は '' ** ''、ベクトル/行列の乗算は '' v * '' * v'。 'Cartesian_Euclidean_Space'の理論を参照してください。 –

もう一度マヌエル、本当に便利です。正直なところ、私はエンジニアリングの問題に取り組んでいます。私はどの定理証明がより便利であるかを調べています。心の中の2つ、Isabelle/HOLとPVS。私はイサベルとの最初の試みをしたいと思っています。すでに広範な理論が立証されており、コミュニティの数はユーザー数の点で優れていると思います。不等式、普遍的な定量化不等式、高次関数、規範、収束、微分方程式、ODE、三角関数など、実フィールドに関連する定理または補題があります。どう思いますか？ –

答えて

関連する問題