TranslationTransportNorms

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

The A4 transport of the normalized norms

TranslationTransport.lean moves the equation from the frozen theorem's frame (the window z + □_{n+2} at the sample ω) to the harmonic slot's frame (the origin cube □_{n+2} at translateCutoffSample z ω). This module moves the norms that appear on the right-hand side of e.good.scale.homog, and records the one geometric simplification the interior regime provides.

Everything here is an exact identity: Lebesgue measure is translation invariant, so a normalized average over z + A of f is the normalized average over A of f(· + z), with no constant.

The interior regime collapses the intersected windows

The frozen statement carries its right-hand-side norms on the intersected window (z + □_{n+2}) ∩ □_m. On the frontier-empty gate — which is exactly the hypothesis of the anchor's sharpened interior clause — the gate's own inclusion makes that intersection the bare translate z + □_{n+2}. So in the interior regime the intersection is pure bookkeeping and disappears (inter_eq_of_frontier_inter_empty).

Main results

• inter_eq_of_frontier_inter_empty — the intersected window is the translate.
• normalizedL2SqOnSet_translateSet, normalizedSetAverage_translateSet, normalizedSetAverage_vecNormSq_translateSet — the three norm transports.
• normalizedL2SqOnSet_sub_volumeAverage_translateSet — the mean-subtracted L² square of the anchor's solution on the parent window equals that of the transported solution on □_{n+2}; both the norm and the subtracted mean move together.

References

• ABK26, e.good.scale.homog.
• CoarseGraining, Homogenization/Book/Ch01/Theorems/NormScaling.lean (Ch01.volumeAverage_translateSet_eq_comp_addRight).

1. The interior regime collapses the intersected window

theorem Algsuperdiff.Section4.Provider.ExcessDecay.inter_eq_of_frontier_inter_empty {d : ℕ} {k m : ℤ} {z : HCPolySupport.Vec d} (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hfr : (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k) ∩ frontier (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) = ∅) : (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) = (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k)

In the interior regime the anchor's intersected window is the bare translate. The frontier-empty gate gives z + □_k ⊆ □_m, so the intersection with □_m is inert.

2. The norm transports

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedSetAverage_translateSet {d : ℕ} (z : HCPolySupport.Vec d) (U : Set (HCPolySupport.Vec d)) (f : HCPolySupport.Vec d → ℝ) : HCPolySupport.Book.Ch03.normalizedSetAverage (HCPolySupport.translateSet z U) f = HCPolySupport.Book.Ch03.normalizedSetAverage U fun (x : HCPolySupport.Vec d) => f (x + z)

The normalized average transports exactly.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2SqOnSet_translateSet {d : ℕ} (z : HCPolySupport.Vec d) (U : Set (HCPolySupport.Vec d)) (f : HCPolySupport.Vec d → ℝ) : HCPolySupport.Book.Ch03.normalizedL2SqOnSet (HCPolySupport.translateSet z U) f = HCPolySupport.Book.Ch03.normalizedL2SqOnSet U fun (x : HCPolySupport.Vec d) => f (x + z)

The normalized L² square transports exactly.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedSetAverage_vecNormSq_translateSet {d : ℕ} (z : HCPolySupport.Vec d) (U : Set (HCPolySupport.Vec d)) (G : HCPolySupport.Vec d → HCPolySupport.Vec d) : (HCPolySupport.Book.Ch03.normalizedSetAverage (HCPolySupport.translateSet z U) fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (G x)) = HCPolySupport.Book.Ch03.normalizedSetAverage U fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (G (x + z))

The normalized gradient energy transports exactly.

3. The mean-subtracted L² square of the anchor's solution