BoundaryWindowNormalized

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The window norms in the anchor's volume-normalized carrier

The boundary window estimates are stated against CoarseGraining's own domain measure volume.restrict W', while the frozen statement prices every window norm against the volume-normalized measure Support.normalizedVolumeMeasureOn W'. This file records the identity that relates the two carriers: an L² norm against the normalized measure is the restricted one times the scalar (vol W')^{-1/2}, which does not depend on the function. Since the boundary estimates are homogeneous — the same window on both sides — that scalar cancels exactly and no constant changes.

References

• ABK26, l.harmonic.approximation.good.scales, Step 2.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.eLpNorm_normalizedVolumeMeasureOn_eq {d : ℕ} (A : Set (HCPolySupport.Vec d)) (f : HCPolySupport.Vec d → ℝ) : MeasureTheory.eLpNorm f 2 (Support.normalizedVolumeMeasureOn A) = (MeasureTheory.volume A)⁻¹ ^ (1 / 2) * MeasureTheory.eLpNorm f 2 (MeasureTheory.volume.restrict A)

The volume-normalized L² norm is the restricted one times a scalar that does not depend on the function.