Verification of the UpDown Scheme

Title:	Verification of the UpDown Scheme
Author:	Johannes Hölzl
Submission date:	2015-01-28
Abstract:	The UpDown scheme is a recursive scheme used to compute the stiffness matrix on a special form of sparse grids. Usually, when discretizing a Euclidean space of dimension d we need O(n^d) points, for n points along each dimension. Sparse grids are a hierarchical representation where the number of points is reduced to O(n * log(n)^d). One disadvantage of such sparse grids is that the algorithm now operate recursively in the dimensions and levels of the sparse grid. The UpDown scheme allows us to compute the stiffness matrix on such a sparse grid. The stiffness matrix represents the influence of each representation function on the L^2 scalar product. For a detailed description see Dirk Pflüger's PhD thesis. This formalization was developed as an interdisciplinary project (IDP) at the Technische Universität München.
BibTeX:	@article{UpDown_Scheme-AFP, author = {Johannes Hölzl}, title = {Verification of the UpDown Scheme}, journal = {Archive of Formal Proofs}, month = jan, year = 2015, note = {\url{http://isa-afp.org/entries/UpDown_Scheme.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Automatic_Refinement, Separation_Logic_Imperative_HOL
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.