The cut-off heat-representation identity #
HB2_cutoff_decomposition assembles the forward heat representation, the Leibniz rule for the
heat operator on a product, the compactly supported cutoff extension, and the three slice
integrations by parts of the cutoff-commutator kernel into a single identity: given w = div U
and (∂ₜ − Δ) w = div Y on an open set containing the backward parabolic window at (x, s),
w (x, s) is recovered from the cut-off heat weight paired against Y and the cutoff-commutator
kernel paired against U. This is the pointwise heat bound of the interior estimates in the
proof of lem:aniso:annulus, one step short of the final norm bound.
The hypothesis ρ ≤ 1 is required
because the two slice integrations by parts this file cites, integral_serrinHeatWeight_mul_ spatialPartial and integral_divergence_mul_serrinCutoffKernel (both in HeatSliceIBP.lean),
already carry it. The downstream heat bound that uses this lemma already assumes ρ ≤ 1, so
the extra hypothesis costs nothing.