Shape Perturbation of the Galerkin Boundary Element Dirichlet-to-Neumann Matrix on Moving Polygons
Tokuhiro Eto
math.NA
Nov 10, 2026 · v1
TL;DR
Formal counterparts of the main shape-perturbation theorems (3.3–3.7) are kernel-checked in Lean 4 with Mathlib; the formalization is archived on Zenodo.
Abstract
For nonlocal interface evolution problems such as the Mullins-Sekerka flow, certain parametric schemes discretize only the interface and approximate the Dirichlet-to-Neumann map by boundary elements. Their error analysis requires bounds on how this discrete operator changes as the polygon moves. In that analysis, the polygons are only Lipschitz and close to a smooth curve only in a Lipschitz norm, the perturbations are controlled only in the energy norm, and the kernels are singular on the diagonal. We study the symmetric Galerkin boundary element matrix on the polygons in a Lipschitz neighborhood of a smooth reference curve. Its first variation, tested against discrete Neumann solutions, is bounded by the energy norm of the perturbation alone. The second-order remainder of the associated mass form is bounded by the product of the energy norm and the Lipschitz norm of the perturbation, so that only one of the two factors needs a uniform bound. On the interpolating polygon, the matrix is consistent with the continuous operator without the logarithmic loss that a pointwise comparison of the kernels would suggest, and its shape derivative is consistent with that of the continuous operator. All bounds are uniform in the mesh size and depend only on the constants of the reference curve.
Problem
Parametric schemes for nonlocal interface flows such as Mullins–Sekerka approximate the Dirichlet-to-Neumann map with a symmetric Galerkin boundary element matrix on a moving polygon. Their error analysis needs bounds on how this matrix changes as the polygon moves. The polygons are only Lipschitz, perturbations are controlled only in the energy norm, and the kernels are singular on the diagonal.
Approach
The SGBEM Steklov–Poincaré matrix is rewritten on a fixed parameter circle, so that all shape dependence enters through parameter integrals of the chord logarithm. Polygons are restricted to a Lipschitz neighborhood of the interpolant of a smooth reference curve, taken from a family with uniform chord, derivative and coercivity constants. First variations and second-order remainders are then estimated. Formal counterparts of the main theorems are verified in Lean 4 using Mathlib.
Results
The first variation, tested against discrete Neumann solutions, is bounded by the H^1 norm of the perturbation alone. The second-order remainder of the mass form is bounded by the product of the energy and Lipschitz norms. On the interpolating polygon, the matrix and its shape derivative are consistent with the continuous operator without logarithmic loss. All bounds are uniform in the mesh size, and the Lean proofs use only Lean's standard axioms.
