DivergenceKernel #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: an explicit divergence kernel for a difference of tensor densities #
Several smoothing arguments in Section 3 need to compare the same field averaged at two different scales, i.e. they need to control a difference of two product densities
χ_a(x) − χ_b(x) = ∏ᵢ a(xᵢ) − ∏ᵢ b(xᵢ),
where a and b are one-dimensional smooth compactly supported probability
densities (in practice a = φ_ε and b = φ_R, the one-dimensional factors of
Algsuperdiff/Section3/Provider/Corrector/MollifierScaling.lean's
productDensity). What makes such a difference small when tested against a
solenoidal or mean-zero field is that it is a divergence of a smooth
compactly supported vector field.
This file writes that vector field down explicitly. With
G(t) = ∫_{-T}^{t} (a(s) − b(s)) ds (kernelPrimitive),
g_k(x) = G(x_k) · ∏_{i < k} b(x_i) · ∏_{i > k} a(x_i) (divKernel),
the fundamental theorem of calculus gives ∂_k g_k(x) = (a(x_k) − b(x_k)) · ∏_{i<k} b(x_i) · ∏_{i>k} a(x_i), because neither product involves the
coordinate x_k. In terms of the interpolating densities
χ_m(x) = ∏_{i.val < m} b(x_i) · ∏_{m ≤ i.val} a(x_i) (mixedDensity),
this reads ∂_k g_k = χ_{k.val} − χ_{k.val + 1}, so the sum over k
telescopes:
Σ_k ∂_k g_k = χ_0 − χ_d = χ_a − χ_b (coordDeriv_sum_divKernel).
Nothing deeper is used: no Newtonian potential, no Newton theorem, no elliptic
solve and no Fourier analysis. The construction is elementary and completely
explicit, and the divergence is phrased with
Algsuperdiff/Section3/Provider/Corrector/SolenoidalStream.lean's coordDeriv,
so it composes with the stream-tensor layer used there.
Support and smoothness are recorded as well: each component g_k is C^∞
(contDiff_divKernel_apply) and vanishes off the closed sup-norm ball of radius
T (hasCompactSupport_divKernel_apply, tsupport_divKernel_apply_subset),
provided a and b are unit-mass densities vanishing for T ≤ |s|. The
concrete two-scale instance a = scaledBump hε, b = scaledBump hR,
T = ε + R is recorded at the end of the file.
Disclosure. Nothing in this file realizes any source node. It is an elementary explicit construction offered as a local helper, and it claims no node status.
Coordinate derivatives along a single coordinate line #
Moving the kth coordinate of x to t is the same as translating x
along the kth basis vector.
Coordinate derivatives are one-dimensional derivatives. If restricting a
field differentiable at x to the kth coordinate line through x produces the
one-dimensional function h, then the kth coordinate derivative of the field
at x is the derivative of h at x k.
The index blocks of the telescoping #
The coordinates strictly below the level m.
Equations
- Algsuperdiff.Section3.Provider.Corrector.idxBelow d m = {i : Fin d | ↑i < m}
Instances For
The coordinates at or above the level m.
Equations
- Algsuperdiff.Section3.Provider.Corrector.idxAbove d m = {i : Fin d | m ≤ ↑i}
Instances For
Every coordinate lies at or above level 0.
Every coordinate lies below level d.
The one-dimensional primitive of the difference #
The primitive G(t) = ∫_{-T}^{t}(a − b) of the difference of the two
one-dimensional densities.
Equations
Instances For
Fundamental theorem of calculus for the primitive: G' = a − b.
The primitive vanishes outside (-T, T). To the left of -T the
integrand vanishes identically; to the right of T the integral over [-T, T]
is the full integral of a − b, which is 1 − 1 = 0.
The tensor densities and the divergence kernel #
The tensor-product density χ_a(x) = ∏ᵢ a(xᵢ).
Equations
- Algsuperdiff.Section3.Provider.Corrector.tensorDensity a x = ∏ i : Fin d, a (x i)
Instances For
The interpolating density at level m: the first m coordinates carry the
density b, the remaining coordinates carry the density a.
Equations
- One or more equations did not get rendered due to their size.
Instances For
At level 0 the interpolating density is χ_a.
At level d the interpolating density is χ_b.
The divergence kernel. Its kth component carries the primitive G in
the kth coordinate, the density b in the coordinates below k and the
density a in the coordinates above k.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The divergence kernel vanishes outside the closed sup-norm ball of radius
T: some coordinate of x then has modulus at least T, and whichever of the
three factors sits at that coordinate vanishes.
Every component of the divergence kernel is compactly supported.
The telescoping divergence identity #
The kth coordinate derivative of the kth component. Only the factor
G(x_k) depends on the coordinate x_k, and G' = a − b.
The kth coordinate derivative is one telescoping step.
The divergence identity. The divergence of the explicit smooth
compactly supported vector field divKernel a b T is the difference of the two
tensor-product densities:
Σ_k ∂_k g_k(x) = ∏ᵢ a(xᵢ) − ∏ᵢ b(xᵢ).
Only smoothness of the two one-dimensional densities is used; support and unit mass enter nowhere.
The two-scale instance #
Every component of the two-scale divergence kernel is smooth.
Every component of the two-scale divergence kernel is compactly supported in
the closed sup-norm ball of radius ε + R.
The two-scale divergence identity. The difference of the product
densities at the scales ε and R is the divergence of the explicit smooth
vector field divKernel (scaledBump hε) (scaledBump hR) (ε + R), whose
components are supported in the closed sup-norm ball of radius ε + R.