Numerical Verification Methods and Computer-Assisted Proofs for Partial Differential Equations (eBook)

Mitsuhiro T. Nakao, Michael Plum, Yoshitaka Watanabe (Autoren)

eBook Download: PDF

2019 | 1. Auflage
XIII, 469 Seiten
Springer Singapore (Verlag)
978-981-13-7669-6 (ISBN)

Infos

Recently, various mathematical problems have been solved by computer-assisted proofs, among them the Kepler conjecture, the existence of chaos, the existence of the Lorenz attractor, the famous four-color problem, and more. In many cases, computer-assisted proofs have the remarkable advantage (compared with a 'theoretical' proof) of providing accurate quantitative information.

The authors have been working more than a quarter century to establish the verified computations of solutions for partial differential equations, mainly to the nonlinear elliptic problems of the form -?u=f(x,u,?u) with Dirichlet boundary conditions. Here, by 'verified computation' is meant a computer-assisted numerical approach to proving the existence of a solution in a close and explicit neighborhood of an approximate solution. Therefore, the quantitative information by the technique shown here should also be significant from the viewpoint of the a posteriori error estimates for approximate solution of concerned partial differential equations with mathematically rigorous sense.

In this monograph, the authors describe a survey on the verified computations or computer-assisted proofs for partial differential equations that they developed. In Part I, the methods mainly studied by authors Nakao and Watanabe are presented. These methods are based on the finite dimensional projection and the constructive a priori error estimates for the finite element approximation of the Poisson equation. In Part II, the computer-assisted approaches via eigenvalue bounds developed by the second author, Plum, are explained in detail. The main task of this method consists of eigenvalue bounds for the corresponding nonlinear problems of the linearized operators. Some brief remarks are also given on other approaches in Part III. Each method in Parts I and II is followed by appropriate numerical examples that confirm the actual usefulness of the authors' methods. Also in some examples the practical computer algorithms are supplied so that readers can easily implement the verification program by themselves.

---

In the last decades, various mathematical problems have been solved by computer-assisted proofs, among them the Kepler conjecture, the existence of chaos, the existence of the Lorenz attractor, the famous four-color problem, and more. In many cases, computer-assisted proofs have the remarkable advantage (compared with a "e;theoretical"e; proof) of additionally providing accurate quantitative information.The authors have been working more than a quarter century to establish methods for the verified computation of solutions for partial differential equations, mainly for nonlinear elliptic problems of the form -?u=f(x,u,?u) with Dirichlet boundary conditions. Here, by "e;verified computation"e; is meant a computer-assisted numerical approach for proving the existence of a solution in a close and explicit neighborhood of an approximate solution. The quantitative information provided by these techniques is also significant from the viewpoint of a posteriori error estimates for approximate solutions of the concerned partial differential equations in a mathematically rigorous sense.In this monograph, the authors give a detailed description of the verified computations and computer-assisted proofs for partial differential equations that they developed. In Part I, the methods mainly studied by the authors Nakao and Watanabe are presented. These methods are based on a finite dimensional projection and constructive a priori error estimates for finite element approximations of the Poisson equation. In Part II, the computer-assisted approaches via eigenvalue bounds developed by the author Plum are explained in detail. The main task of this method consists of establishing eigenvalue bounds for the linearization of the corresponding nonlinear problem at the computed approximate solution. Some brief remarks on other approaches are also given in Part III. Each method in Parts I and II is accompanied by appropriate numerical examples that confirm the actual usefulness of theauthors' methods. Also in some examples practical computer algorithms are supplied so that readers can easily implement the verification programs by themselves.

Inhalt

Preface 6
Contents 8
Part I Verification by Finite-Dimensional Projection 15
1 Basic Principle of the Verification 16
1.1 Fixed-Point Formulation of the Problem 16
1.2 Finite-Dimensional Projection and Constructive Error Estimates 18
1.2.1 Aubin–Nitsche Trick 20
1.3 FS-Int: A Simple Enclosure Method of Solutions 20
1.3.1 Criterion for Infinite-Dimensional Part 21
1.3.2 Criterion for Finite-Dimensional Part 22
1.3.3 Notes on FS-Int Programming 25
1.4 An Application to the Second-Order Elliptic Boundary Value Problems 25
1.4.1 Dirichlet Boundary Value Problems 25
1.4.2 Constructive Error Estimations 27
1.4.2.1 One-Dimensional Case 27
1.4.2.2 Two-Dimensional Case 30
1.4.2.3 Linear Triangular Element 31
1.4.2.4 Fourier Basis 31
1.4.2.5 Legendre Basis 32
1.5 A Simple Example of FS-Int 33
1.6 Other Examples of FS-Int 38
1.7 Case of Non-convex Domain 39
1.7.1 An Example for H10-Error Estimations on Non-convex Polygon 39
1.7.1.1 Finite-Element Approximation 39
1.7.1.2 Computation of the Constant c2(h) 42
1.7.1.3 Computation of the Constants c3 and c4 44
1.7.1.4 Computation of the Constant K1 47
1.7.1.5 Computation of the Constant K2 49
1.7.1.6 Computation of the Constant K3 50
1.7.1.7 An Example 52
1.8 Embedding Constants 53
2 Newton-Type Approaches in Finite Dimension 56
2.1 FN-Int: An Enclosure Method with Newton-Type Operator 56
2.1.1 Deriving Newton-Type Operator Nh 58
2.1.2 Fixed-Point Formulation by Newton-Type Operator 59
2.1.3 Notes on FN-Int Programming 61
2.2 A Simple Example of FN-Int 62
2.3 Other Examples of FN-Int 64
2.3.1 Simplifying Grad–Shafranov Equation 64
2.3.2 Verification for Bifurcated Solutions 65
2.4 Some Refinements 66
2.4.1 Residual Formulation 66
2.4.1.1 Direct Residual Formulation 66
2.4.1.2 An Example of Direct Residual Formulation 67
2.4.1.3 X*-Type Residual Formulation 68
2.4.1.4 X*-Type a Posteriori Residual Formulation 69
2.4.1.5 Examples 70
2.4.2 Norm Estimation for the Finite-Dimensional Part 70
2.4.2.1 Some Difficulties in FN-Int 70
2.4.2.2 Alternative Computation for Finite-Dimensional Part 71
2.4.2.3 Notes on FN-Norm Programming 73
2.4.2.4 Examples 73
2.5 Verification of the Local Uniqueness by FN-Int 76
2.5.1 Residual Vector 76
2.5.2 Candidate Set and Verification Condition 76
2.5.3 Notes on FN-IntU Programming 80
2.5.3.1 Example 80
2.6 Verification of the Local Uniqueness for FN-Norm 81
2.6.1 Candidate Set and Verification Condition 81
2.6.2 Notes on FN-NormU Programming 84
2.6.3 Examples 84
3 Infinite-Dimensional Newton-Type Method 85
3.1 A Verification Algorithm Based on Sequential Iterations 85
3.1.1 Fixed-Point Form 85
3.1.2 Verification Condition 86
3.1.3 Local Uniqueness of the Solution 87
3.1.4 Verification Algorithm IS-Res 88
3.1.5 Notes on IS-Res Programming 88
3.1.6 Extension of the Region for Local Uniqueness 89
3.1.7 Examples 90
3.1.7.1 Two-Point Boundary Value Problem 90
3.1.7.2 Second-Order Elliptic Boundary Value Problem 91
3.1.7.3 Fourth-Order Elliptic Problem 91
3.2 A Verification Algorithm Based on Newton-Like Iterations 93
3.2.1 Fixed-Point Formulation 93
3.2.2 Verification Condition 94
3.2.3 Local Uniqueness of the Solution 95
3.2.4 Verification Algorithm 96
3.2.5 Extension of the Region for Local Uniqueness 97
3.3 The Invertibility of L and Computation of M 97
3.3.1 A Method Based on Fixed-Point Formulation 98
3.3.2 A Method of Direct Computation of M 104
3.3.3 In the Case of Second-Order Elliptic Boundary Value Problems 107
3.4 Examples 109
3.4.1 Second-Order Elliptic Boundary Value Problems 109
3.4.1.1 A Reaction Diffusion System 109
3.4.1.2 Two-Dimensional Problem 111
3.4.2 Fourth-Order Elliptic Problem 112
4 Applications to the Computer-Assisted Proofs in Analysis 114
4.1 Nonlinear Elliptic Boundary Value Problems 114
4.1.1 Emden Equation 114
4.1.2 Elliptic Equations with Neumann Boundary Conditions and Systems 115
4.1.3 Stationary Navier–Stokes Problem 116
4.1.4 Kolmogorov Problem 116
4.2 Driven Cavity Problem 118
4.2.1 Fixed-Point Formulation Based on IN-Linz 120
4.2.2 Invertibility Condition of L and Computation of M 121
4.2.3 Examples 126
4.3 Heat Convection Problems 126
4.3.1 Verification of Two-Dimensional Non TrivialSolutions 127
4.3.2 Existence Proof of a Bifurcation Point 130
4.3.3 Three-Dimensional Problems 134
4.4 Enclosing/Excluding Eigenvalue Problems 140
4.4.1 Second-Order Elliptic Eigenvalue Problem 140
4.4.2 Orr–Sommerfeld Problem 140
4.4.3 Eigenvalue Exclosure 141
4.5 Other Applications 142
5 Evolutional Equations 143
5.1 Full Discretization of the Heat Equation 144
5.1.1 Notations and Finite-Dimensional Projections 144
5.1.2 Full-Discretization Scheme 145
5.2 Error Estimates for Full-Discretization 150
5.2.1 Preliminary Results for Semidiscretization 150
5.2.2 Constructive Estimates for Full-Discretization 154
5.3 Norm Estimates for the Inverse of Linear Parabolic Operator 158
5.3.1 Discretized Linear Problem 159
5.3.2 A Posteriori Estimates for Lt-1 164
5.4 Numerical Examples 169
5.4.1 A Posteriori Estimates of the Inverse ParabolicOperator 170
5.4.2 Verification Results for Solutions of Nonlinear Parabolic Equations 173
5.5 A Related Fully Discrete Galerkin Scheme 176
5.5.1 A Full Discretization Scheme for Heat Equation 176
5.5.2 Application to the Verified Computation of Nonlinear Problems 180
5.5.3 Numerical Examples 181
Example 1: Fujita-Type Equation 181
Example 2: Allen-Cahn Equation 182
5.5.4 Some Remarks on Other Approaches 185
Part II Computer-Assisted Proofs for Nonlinear Elliptic Boundary Value Problems via Eigenvalue Bounds 187
6 Semilinear Elliptic Boundary Value Problems: Abstract Approach and Strong Solutions 188
6.1 Abstract Formulation 190
6.2 Strong Solutions 198
6.2.1 Computation of ? in H2(?) H01 (?) 199
6.2.2 L2-defect Bound ? 200
6.2.3 Bound K for L-1:L2(?)?H2(?) H01 (?) 201
6.2.4 Local Lipschitz Bound g for F': H2(?) H01 (?) ? B ( H2(?) H01 (?),L2(?)) 204
6.2.5 A Computer-Assisted Multiplicity proof 205
6.2.6 Explicit Constants for the EmbeddingH2 (?) -3mu?C (?) 208
6.2.7 L2-Bounds for the Hessian Matrix 213
7 Weak Solutions 223
7.1 Computation of ? in H10(?) 228
7.2 H-1-defect Bound ? 228
7.3 Bound K for L-1:H-1(?)?H10(?) 230
7.4 Local Lipschitz Bound g for F': H10(?)?B (H01 (?),H-1(?)) 234
7.5 Examples 236
7.5.1 Emden's Equation on an Unbounded L-ShapedDomain 236
7.5.2 A Nonlinear Schrödinger Equation on R2 240
7.5.3 Gelfand's Equation on a Non-convex PolygonalDomain 243
7.6 Embedding Constants 246
7.7 Proof of Lemma 7.1 254
8 Fourth-Order Problems 259
8.1 Computation of ? in H20(?) 266
8.2 H-2-defect Bound ? 267
8.3 Bound K for L-1:H-2(?)?H20(?) 268
8.4 Local Lipschitz Bound g for F': H20(?)?B (H02 (?),H-2(?)) 271
8.5 Travelling Waves in a Nonlinearly Supported Beam 271
9 Other Problem Types 278
9.1 Solution Branches 278
9.1.1 A Computer-Assisted Uniqueness Proof 284
9.2 Turning and Bifurcation Points 286
9.2.1 Turning Points 288
9.2.1.1 Gelfand's Equation on a Square 293
9.2.2 Symmetry-Breaking Bifurcations 297
9.2.2.1 Symmetric Solution Branch 298
9.2.2.2 Symmetry-Breaking Solution Branch 301
9.2.2.3 An Alternative Approach 308
9.2.2.4 A Duffing-Type Equation 309
9.3 Non-self-Adjoint Eigenvalue Problems 311
9.3.1 Eigenpair Enclosures 311
9.3.2 Eigenvalue Exclosures 322
9.3.3 The Orr–Sommerfeld Equation with Blasius Profile 324
9.3.3.1 Computation of (?0,?), ?, and K 326
9.3.3.2 Goerisch Setting and Homotopy for Problem (9.131) 327
9.3.3.3 Numerical Results and Instability Proof 334
9.4 Systems and Non-symmetric Problems of Second Order 336
9.4.1 Bound K for L-1, Bijectivity of L 338
9.4.1.1 Strong Formulation 339
9.4.1.2 Weak Formulation 341
9.4.2 Local Lipschitz Bound for F' 348
10 Eigenvalue Bounds for Self-Adjoint Eigenvalue Problems 355
10.1 Eigenvalue Bounds for Self-Adjoint Operators 358
10.1.1 Basic Properties 358
10.1.2 Bounds for Eigenvalues in General Location 361
10.1.3 Bounds to Eigenvalues Below ?ess(A) 369
10.1.4 Poincaré's Min-Max Principle, Comparison Problems 372
10.2 Eigenvalue Problems with Bilinear Forms 378
10.2.1 The Associated Self-Adjoint Operator 379
10.2.2 Eigenvalue Bounds for the Bilinear Form Problem 380
10.2.3 Goerisch's Extension 384
10.2.4 Comparison Problems, Homotopy Method 395
10.2.5 Examples of Homotopies 400
10.2.5.1 Coefficient Homotopy 400
10.2.5.2 Domain Deformation Homotopy 403
10.2.5.3 Domain Decomposition Homotopy 405
10.2.5.4 Fourth-Order Problems, BoundaryHomotopy 412
Part III Related Work and Tools 418
11 Computer-Assisted Proofs for Dynamical Systems 419
11.1 Topological Methods 420
11.2 Fixed-Point Approaches 422
11.2.1 Stationary Solutions of Problem (11.1) 422
11.2.2 Time-Periodic Orbits 423
11.2.3 Stable and Unstable Manifold 423
11.2.4 Connecting Orbits 425
12 Basic Tools 426
12.1 Fixed-Point Formulation 426
12.2 Some Pitfalls in Numerical Computation 428
12.2.1 ``Spurious'' Solution in a Discretized Problem 429
12.2.2 Rounding Errors in MATLAB Linear Solver 430
12.2.3 Rump's Example 431
12.3 Interval Arithmetic 433
12.3.1 Interval Representation 433
12.3.2 The Four Operations of Interval Arithmetic 433
12.3.3 Some Properties of Interval Arithmetic 434
12.3.4 Introduction to INTLAB 435
12.4 Verifications for Finite-Dimensional Problems 436
12.4.1 Nonlinear Systems in Rn 436
12.4.2 Linear Systems 438
12.4.3 Matrix Eigenvalue Problems 439
12.4.4 Validation of Positive Definiteness of Matrices 439
12.4.5 Spectral Norms 441
12.4.5.1 For General Matrices 441
12.4.5.2 For Hermitian Matrices 442
12.4.6 An Upper Bound of "026B30D DH2G-1D12"026B30D 2 443
12.4.6.1 For General Matrix G 443
12.4.6.2 For Hermitian Matrix G 443
12.4.7 An Upper Bound of "026B30D DH2G-1L12"026B30D 2 445
12.4.7.1 For General Matrix G 446
12.4.7.2 For Hermitian Matrix G 446
12.4.8 An Upper Bound of Absolute Maximum Eigenvalues for Generalized Matrix EigenvalueProblem 447
References 449
Index 465

Produkt-Details

• Erscheint lt. Verlag: 11.11.2019
• Reihe/Serie: Springer Series in Computational Mathematics
• Zusatzinfo: XIII, 467 p. 59 illus., 17 illus. in color.
• Sprache: englisch
• Themenwelt: Mathematik / Informatik ► Informatik ► Theorie / Studium
• Themenwelt: Mathematik / Informatik ► Mathematik ► Analysis
• Schlagworte: Computer-assisted proofs in analysis • Mathematically rigorous a posteriori error estimates • Nonlinear Partial Differential Equations • Numerical enclosure of solutions for PDEs • Numerical verification methods for nonlinear problems • Partial differential equations
• ISBN-10: 981-13-7669-7 / 9811376697
• ISBN-13: 978-981-13-7669-6 / 9789811376696