中国科学技术大学研究生教育创新计划高水平学术前沿讲座
题目：基于有限元方法的计算机数学证明 -- 从有限挑战无限
报告人：刘雪峰 博士
时间：9月9日，10日，11日，12日，13日 上午9:45―12:15
地点：管理科研楼1518室
报告人简介：
刘雪峰 早稻田大学理工学术院 次席研究员 (Junior researcher)
1998年～2003年 中国科大数学系
2004年～2009年 东京大学数理科学研究科，学习有限元方法等
2009年～至今 早稻田大学，从事微分算子的特征值精确估计等研究
课程概要：
本课程将阐述利用浮点小数来进行精确计算的方法以及其用于数学证明的框架和实现方法。特别的，我们将详细讨论如何利用有限元方法来估计拉普拉斯算子的特征值，以及验证非线性微分方程解的存在性和唯一性等。本讲义从浮点小数的数值计算标准讲起，介绍利用区间计算的无误差计算方法。其中将探讨如何精确地求解线性代数的基本问题，比如一次线性方程和矩阵特征值问题等。进一步，本讲义将讲述有限元方法的基本知识，及其在求解Poisson方程和拉普拉斯算子的特征值问题中的定性及定量的误差估计理论。特别的，我们将介绍最新的对含有奇异性的解的处理方法。课程中最后将介绍如何结合有限元方法和无误差计算来验证非线性微分方程问题的解的存在性，局部唯一性等。
课程目标：
选修此课程的同学需要使用Matlab来编写基本的程序。课程结束时，将能够设计完整的程序来计算拉普拉斯算子的精确的特征值估计。
课程内容及进度安排：
第一讲：
无误差计算及数学证明的基本概念(30Min)
科学浮点小数的计算标准IEE0754 （30Min）
区间计算及Matlab的区间计算程序库IntLab (30Min)
精确求解线性方程组的方法（30Min）
精确求矩阵解特征值问题的方法（30Min）
第二讲：
Poisson方程及有限元方法 (30Min)
有限元数值解的存在性，误差估计。(Lax-Milgram定理, Aubin-Nitsue方法）
(60Min)
误差常数的估计（45Min）
有限元的程序设计（30Min）
第三讲：
拉普拉斯算子的特征值问题（30Min）
Min-max定理及上下界 (60Min)
特征值估计的程序设计（60Min）
第四讲：
多项式基函数及边界连续条件(Berstein function) （30Min）
特征值优化估计 （Lehmann-Gorisch定理）(60Min)
特征函数的奇异性（30Min）
程序设计（30min）
第五讲：
椭圆型非线性微分方程问题 （30Min）
Newton-Kantorovich定理及应用 （60Min）
程序设计及数值求解方法（30Min）
结语（Open problem ）（30Min）
主办单位：中国科技大学数学学院 中国科技大学研究生院
欢迎感兴趣的师生参加！
题目：基于有限元方法的计算机数学证明 -- 从有限挑战无限
报告人：刘雪峰 博士
时间：9月9日，10日，11日，12日，13日 上午9:45―12:15
地点：管理科研楼1518室
报告人简介：
刘雪峰 早稻田大学理工学术院 次席研究员 (Junior researcher)
1998年～2003年 中国科大数学系
2004年～2009年 东京大学数理科学研究科，学习有限元方法等
2009年～至今 早稻田大学，从事微分算子的特征值精确估计等研究
课程概要：
本课程将阐述利用浮点小数来进行精确计算的方法以及其用于数学证明的框架和实现方法。特别的，我们将详细讨论如何利用有限元方法来估计拉普拉斯算子的特征值，以及验证非线性微分方程解的存在性和唯一性等。本讲义从浮点小数的数值计算标准讲起，介绍利用区间计算的无误差计算方法。其中将探讨如何精确地求解线性代数的基本问题，比如一次线性方程和矩阵特征值问题等。进一步，本讲义将讲述有限元方法的基本知识，及其在求解Poisson方程和拉普拉斯算子的特征值问题中的定性及定量的误差估计理论。特别的，我们将介绍最新的对含有奇异性的解的处理方法。课程中最后将介绍如何结合有限元方法和无误差计算来验证非线性微分方程问题的解的存在性，局部唯一性等。
课程目标：
选修此课程的同学需要使用Matlab来编写基本的程序。课程结束时，将能够设计完整的程序来计算拉普拉斯算子的精确的特征值估计。
课程内容及进度安排：
第一讲：
无误差计算及数学证明的基本概念(30Min)
科学浮点小数的计算标准IEE0754 （30Min）
区间计算及Matlab的区间计算程序库IntLab (30Min)
精确求解线性方程组的方法（30Min）
精确求矩阵解特征值问题的方法（30Min）
第二讲：
Poisson方程及有限元方法 (30Min)
有限元数值解的存在性，误差估计。(Lax-Milgram定理, Aubin-Nitsue方法）
(60Min)
误差常数的估计（45Min）
有限元的程序设计（30Min）
第三讲：
拉普拉斯算子的特征值问题（30Min）
Min-max定理及上下界 (60Min)
特征值估计的程序设计（60Min）
第四讲：
多项式基函数及边界连续条件(Berstein function) （30Min）
特征值优化估计 （Lehmann-Gorisch定理）(60Min)
特征函数的奇异性（30Min）
程序设计（30min）
第五讲：
椭圆型非线性微分方程问题 （30Min）
Newton-Kantorovich定理及应用 （60Min）
程序设计及数值求解方法（30Min）
结语（Open problem ）（30Min）
主办单位：中国科技大学数学学院 中国科技大学研究生院
欢迎感兴趣的师生参加！
