收斂和向量理論

Isabelle/HOL中是否存在收斂理論？我需要定義∥x(t)∥ ⟶ 0 as t ⟶ ∞。收斂和向量理論

此外，我正在尋找向量理論，我找到了矩陣理論，但我找不到向量之一，Isabelle/HOL中是否存在這樣的理論？

乾杯。

2017-03-27 O.J

收斂等用過濾器表示在伊莎貝爾。（請參見相應的documentation）

在你的情況，那將是什麼樣

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

，或者使用tendsto縮寫，

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

其中⤏是伊莎貝爾符號\<longlongrightarrow>，它可以使用縮寫--->輸入。

作爲一個方面說明，我想知道你爲什麼寫它擺在首位的是這樣，看到它相當於

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-Analysis的一部分~~/src/HOL/Analysis/Finite_Cartesian_Product.thy提供。這提供了vec類型，它有兩個參數：組件類型（可能是real）和索引類型，它指定向量空間的維度。

對於每個正整數n還有一個預定義類型n，以便您可以編寫例如向量空間012³爲(real, 3) vec。還有類型語法，以便您可以爲('a, 'n) vec編寫'a^'n。

來源

2017-03-27 18:25:04

非常感謝Manuel的廣泛解釋。對於‖x（t）‖‖0，當t∞∞時，「x」是一個實數矢量，當t（時間）收斂於無窮大時，這個矢量中的每個元素應該收斂到零。我對伊莎貝爾仍然有困難，例如，x $ i是否與（'a，'b）vec？一樣？我可以在向量和矩陣之間進行一些關係（mult，add等）嗎？ –

是的，但是‖x（t）‖‖0'和'x（t）‖0'完全等價。並且，不，'x $ i'是向量'x'的$ i $ -th分量，而'（'a，'b）vec'是其元素具有類型'a'的向量的*類型*其維度是「b」。即'（real，3）vec'對應於ℝ³。向量/矩陣的加法是用'+'完成的，向量的點積是'*'（\ ），矩陣乘法是'**'，向量/矩陣乘法是'v *'，矩陣/向量乘法是' * v'。參見'Cartesian_Euclidean_Space'理論。 –

再次感謝Manuel，這真的很有用。老實說，我正在研究工程問題，並且正在研究哪一個定理證明者更方便。頭腦中有兩個人，Isabelle/HOL和PVS。我想先嚐試一下Isabelle，因爲我認爲它已經證明了更廣泛的理論，並且社區在用戶數量方面更好。所需的定理或引理與真實領域有關，如不等式，普遍量化的不等式，高階函數，規範，收斂，微分方程，ODE，三角函數等。你認爲如何？ –

收斂和向量理論

回答

相關問題