掃一掃
關(guān)注中圖網(wǎng)
官方微博
包郵 矩陣結(jié)構(gòu)與矩陣函數(shù)的形式化
開本：
B5
頁(yè)數(shù)：
112
本類五星書更多>
-
>
全國(guó)計(jì)算機(jī)等級(jí)考試最新真考題庫(kù)模擬考場(chǎng)及詳解·二級(jí)MSOffice高級(jí)應(yīng)用
-
>
決戰(zhàn)行測(cè)5000題(言語(yǔ)理解與表達(dá))
-
>
軟件性能測(cè)試.分析與調(diào)優(yōu)實(shí)踐之路
-
>
第一行代碼Android
-
>
JAVA持續(xù)交付
-
>
EXCEL最強(qiáng)教科書(完全版)(全彩印刷)
-
>
深度學(xué)習(xí)
中圖價(jià):¥55.6
加入購(gòu)物車
矩陣結(jié)構(gòu)與矩陣函數(shù)的形式化 版權(quán)信息
- ISBN：9787030763303
- 條形碼：9787030763303 ; 978-7-03-076330-3
- 裝幀：平裝膠訂
- 冊(cè)數(shù)：暫無
- 重量：暫無
- 所屬分類：>
矩陣結(jié)構(gòu)與矩陣函數(shù)的形式化 內(nèi)容簡(jiǎn)介
在使用ITP技術(shù)來驗(yàn)證日趨復(fù)雜的現(xiàn)代工程應(yīng)用問題時(shí)，特別是涉及有關(guān)微積分等理論的復(fù)雜數(shù)學(xué)分析問題的形式化證明時(shí)，因缺乏矩陣分析理論基礎(chǔ)定理庫(kù)的支持，其證明還異常困難或無法實(shí)現(xiàn)。為了解決ITP技術(shù)在驗(yàn)證這些復(fù)雜問題時(shí)所面臨的技術(shù)障礙，提高系統(tǒng)的安全等級(jí)，本書以矩陣分析理論的形式化作為基本任務(wù)，旨在構(gòu)建一個(gè)用戶友好的形式化數(shù)學(xué)體系，并將該體系運(yùn)用于實(shí)際物理問題的證明。
矩陣結(jié)構(gòu)與矩陣函數(shù)的形式化 目錄
目錄
符號(hào)說明
序
前言
第1章緒論1
1.1背景及意義1
1.2研究現(xiàn)狀3
1.2.1矩陣分析3
1.2.2數(shù)學(xué)形式化的發(fā)展現(xiàn)狀5
1.3定理證明系統(tǒng)HOL Light9
1.3.1HOL Light簡(jiǎn)介9
1.3.2系統(tǒng)相關(guān)符號(hào)的約定10
1.4主要內(nèi)容11
1.5本書結(jié)構(gòu)13
參考文獻(xiàn).14
第2章矩陣結(jié)構(gòu)的形式化18
2.1抽象空間18
2.1.1線性空間19
2.1.2拓?fù)淇臻g19
2.1.3距離空間與賦范空間19
2.1.4內(nèi)積空間與希爾伯特空間20
2.2矩陣結(jié)構(gòu)20
2.3矩陣結(jié)構(gòu)的基本數(shù)據(jù)類型21
2.4矩陣結(jié)構(gòu)基本性質(zhì)的形式化23
2.4.1線性性質(zhì)23
2.4.2拓?fù)湫再|(zhì)27
2.4.3范數(shù)性質(zhì)32
2.4.4內(nèi)積性質(zhì)36
2.5矩陣結(jié)構(gòu)的完備性.38
2.5.1空間完備性的形式化38
2.5.2巴拿赫空間與希爾伯特空間39
2.6本章小結(jié)39
參考文獻(xiàn)40
第3章矩陣序列與矩陣級(jí)數(shù)理論的形式化41
3.1矩陣序列與矩陣級(jí)數(shù)的形式化41
3.1.1矩陣序列41
3.1.2矩陣級(jí)數(shù)42
3.1.3矩陣冪級(jí)數(shù)44
3.2柯西審斂準(zhǔn)則在矩陣序列的推廣47
3.2.1柯西審斂準(zhǔn)則47
3.2.2比較審斂法和比值審斂法48
3.3矩陣函數(shù)的形式化50
3.3.1一般矩陣函數(shù)的形式化定義50
3.3.2常用的由矩陣冪級(jí)數(shù)表示的矩陣函數(shù)51
3.4矩陣結(jié)構(gòu)緊致性的形式化分析53
3.4.1緊致性相關(guān)概念的形式化53
3.4.2緊致性的等價(jià)性證明54
3.5本章小結(jié)54
參考文獻(xiàn)55
第4章矩陣函數(shù)微分的形式化56
4.1矩陣函數(shù)連續(xù)性56
4.1.1矩陣函數(shù)連續(xù)性的形式化定義56
4.1.2矩陣函數(shù)連續(xù)性的形式化60
4.2矩陣函數(shù)的Fréchet微分62
4.2.1Fréchet微分定義的形式化62
4.2.2矩陣函數(shù)微分基本性質(zhì)的形式化63
4.3矩陣函數(shù)微分與有界線性算子66
4.4本章小結(jié)68
參考文獻(xiàn)69
第5章矩陣?yán)碚摰淖詣?dòng)定理證明70
5.1引言70
5.2判定程序基本理論及矩陣結(jié)構(gòu)理論判定性研究73
5.2.1判定程序基本理論73
5.2.2矩陣結(jié)構(gòu)理論判定性的初步研究74
5.3自動(dòng)證明算法的設(shè)計(jì)與實(shí)現(xiàn)76
5.3.1算法的基本流程76
5.3.2算法的程序?qū)崿F(xiàn)78
5.3.3判定程序的有效性測(cè)試80
5.4本章小結(jié)81
參考文獻(xiàn)82
第6章應(yīng)用示例83
6.1一種面向Massive MIMO的矩陣求逆算法形式化分析83
6.1.1引言83
6.1.2系統(tǒng)模型的形式化85
6.1.3算法模型的形式化86
6.1.4級(jí)數(shù)收斂性的形式化分析89
6.2機(jī)器人機(jī)構(gòu)運(yùn)動(dòng)學(xué)中的李群李代數(shù)模型的形式化驗(yàn)證91
6.2.1引言91
6.2.2機(jī)構(gòu)運(yùn)動(dòng)學(xué)中常用李群李代數(shù)的形式化92
6.2.3機(jī)構(gòu)運(yùn)動(dòng)學(xué)中常用李群李代數(shù)及其指數(shù)映射的形式化驗(yàn)證96
6.3本章小結(jié)98
參考文獻(xiàn)99
展開全部
書友推薦
- >
我與地壇
- >
羅曼·羅蘭讀書隨筆-精裝
- >
史學(xué)評(píng)論
- >
企鵝口袋書系列·偉大的思想20:論自然選擇(英漢雙語(yǔ))
- >
自卑與超越
- >
中國(guó)人在烏蘇里邊疆區(qū):歷史與人類學(xué)概述
- >
龍榆生：詞曲概論/大家小書
- >
大紅狗在馬戲團(tuán)-大紅狗克里弗-助人
本類暢銷
