OneStepBoundaryGeometry #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The boundary ball family: the Schauder geometry on the doubled window #
OneStepSchauderWindow.metricBall_subset_truncatedWindow_of_interior supplies the
ball family the Schauder atom consumes on the interior branch: every point of
the Hölder window U_3 = (x + □_{n-3}) ∩ □_m carries a sup-ball of radius
3^{n-3}/2 inside the replacement window U_2 = (x + □_{n-2}) ∩ □_m. That
inclusion needs the interior hypothesis x + □_{n-2} ⊆ □_m, because a point of
U_3 may sit at zero distance from a met face of ∂□_m.
On the boundary branch the harmonicity domain is not U_2 but its partial
reflection reflectedWindow x m (n-2) (OddReflectionWindow), across every met
face of ∂□_m at once. This module records that the same radius works there,
with no interior hypothesis and with no restriction on the number of met faces:
p ∈ (x + □_{n-3}) ∩ □_m ⟹ ball p (3^{n-3}/2) ⊆ reflectedWindow x m (n-2) .
Why the unmet coordinates are free (the machine-checked point) #
The apparent difficulty — "along an unmet coordinate the window is still cut by
∂□_m" — does not exist: being cut in coordinate i is the definition of
meeting the i-face. MeetsUpperFace x m k i is literally
½·3^m ≤ xᵢ + ½·3^k, i.e. windowHi x m k i = ½·3^m; if the face is not met
then windowHi x m k i = xᵢ + ½·3^k and the window has its full triadic edge in
that coordinate. So on an unmet coordinate the margin is the interior margin
3^{n-2}/2 − 3^{n-3}/2 = 3^{n-3} of one full triadic scale, and on a met
coordinate the reflection supplies the same margin on the far side. Both cases
are already discharged, coordinate by coordinate, by
OddReflectionWindow.image_add_openCubeSet_subset_reflectedWindow, which is
proved by a three-way by_cases on MeetsUpperFace / MeetsLowerFace /
neither; the present module only converts its cube conclusion p + □_{n-3} into
the ball shape the atom consumes and adds the volume bookkeeping.
Consequence for the multi-met-face question. The geometry of the boundary
branch is uniform in the met set S ⊆ Fin d: nothing here assumes #S ≤ 1. The
one-met-face restriction of OddReflectionAssembly is a restriction on the
analytic transfer (the harmonicity of the odd extension), not on the ball
family.
The volume ratio #
|reflectedWindow x m (n-2)| ≤ 2^d · |U_2| ≤ (2·3^{n-2})^d
(OddReflectionVolume.volume_reflectedWindow_le, then the window sandwich), and
|euclideanBall p ρ| ≥ (ρ/(d+1))^d at ρ = 3^{n-3}/4, so the ratio is bounded
by the scale-free constant (24(d+1))^d — exactly twice the interior base
12(d+1), the reflection's 2^d spread over the d factors.
References #
- ABK26,
l.excess.decay.good.scales, the Schauder gradient-Hölder estimate.
1. Sup-balls are triadic cubes #
The sup-ball of radius 3^k/2 centred at p is the translated open cube
p + □_k; only the inclusion ⊆ is needed downstream.
2. The boundary ball family #
The boundary ball family. Every point of the Hölder window
(x + □_{n-3}) ∩ □_m carries a sup-ball of radius 3^{n-3}/2 inside the
partially reflected window reflectedWindow x m (n-2) — the same radius as the
interior family of metricBall_subset_truncatedWindow_of_interior, with the
interior hypothesis x + □_{n-2} ⊆ □_m removed and with no restriction on
which, or on how many, faces of ∂□_m are met.
The Euclidean-ball form of the boundary family, at any admissible radius.
The toEuc-image form of the boundary family, as the Schauder atom consumes
it.
3. The volume of the reflected window #
The reflected window's volume, from above. The partial reflection costs
a factor 2^d (exactly 2^{#S}), and the window itself is inside a cube of side
3^k.
4. The scale-free volume ratio of the boundary family #
The ratio constant of the boundary gap: √((24(d+1))^d) — the interior
constant √((12(d+1))^d) with the reflection's factor 2^d folded in.
Equations
Instances For
The boundary volume ratio is scale free. The ratio of the reflected
window's volume to the volume of any of the atom's half-balls is at most
(24(d+1))^d, independently of n, m and x.