Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP Entry: Verification of the UpDown Sche...


view this post on Zulip Email Gateway (Aug 19 2022 at 17:02):

From: Tobias Nipkow <nipkow@in.tum.de>
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.

http://afp.sourceforge.net/entries/UpDown_Scheme.shtml

We thank Johannes for this first entry in 2015!
smime.p7s


Last updated: Apr 25 2024 at 08:20 UTC