OneStepCornerTransportNorms

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

Transport of the excess calculus along a coordinate negation

This module transports the excess/seminorm calculus of Algsuperdiff/Section4/Support/AffineExcess.lean along the coordinate negation

σ_i := coordFaceReflection (0 : ℝ) i ,     σ_i y l = if l = i then -(y l) else y l ,

the linear isometric involution of Vec d that negates the i-th coordinate (CoarseGraining's Homogenization.coordFaceReflection at the face coordinate a = 0).

It is the measure-side half of the lower/mixed-face transport of the §4.3 boundary branch. The domain cube □_m is origin-symmetric, so negating one coordinate carries a window that meets the lower i-face of □_m to a window that meets the upper i-face; the boundary branch therefore only ever has to be proved for upper faces, and the lower and mixed (corner) faces are obtained by composing the upper-face statement with the negations σ_i. The present module supplies the half of that reduction which is pure measure theory: every norm, average, affine distance, excess and minimizer predicate appearing in the branch is exactly invariant under σ_i, with no constant.

The two facts that drive everything are:

• σ_i is measure preserving and a measurable embedding, so volume, set integrals, volumeAverage and normalizedL2On transport with equality (volume_preimage_coordFaceReflection … normalizedL2On_comp_coordFaceReflection);
• at a = 0 the map is linear and self-adjoint for vecDot (vecDot_coordFaceReflection_zero), so the affine competitor family is carried onto itself by (c, g) ↦ (c, σ_i g) (affineEval_comp_coordFaceReflection_zero, affineDistSet_comp_coordFaceReflection_zero).

Consequently the whole excess tower is invariant: affineDistOn, affineDistSet, affineExcessRaw, affineExcess, and the minimizer predicate IsAffineMinimizer (as an iff). The MemLp side condition transports too (memLp_comp_coordFaceReflection), so the hypotheses of the NormalizedL2 calculus survive the move.

Only the reflected face coordinate a = 0 gives a linear map, so the affine half of the module is stated at a = 0; the purely measure-theoretic half is stated at a general face coordinate a, where it is equally true.

References

• ABK26, §4.3 boundary branch.
• CoarseGraining, Homogenization/Sobolev/Foundations/CubeReflection/Reflections.lean (coordFaceReflection, measurePreserving_coordFaceReflection).
• Algsuperdiff/Section4/Support/AffineExcess.lean (the transported calculus).

1. The coordinate negation

theorem Algsuperdiff.Section4.Provider.ExcessDecay.coordFaceReflection_zero_apply {d : ℕ} (i : Fin d) (y : HCPolySupport.Vec d) (l : Fin d) : HCPolySupport.coordFaceReflection 0 i y l = if l = i then -y l else y l

The reflection at the face coordinate 0 is the coordinate negation. σ_i negates the i-th coordinate and fixes every other one.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.measurableEmbedding_coordFaceReflection {d : ℕ} (a : ℝ) (i : Fin d) : MeasurableEmbedding (HCPolySupport.coordFaceReflection a i)

The coordinate reflection is a measurable embedding: it is measurable (being measure preserving), injective (being an involution), and it maps measurable sets to measurable sets (its image is its own preimage).

2. The measure-side transport

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_preimage_coordFaceReflection {d : ℕ} {a : ℝ} (i : Fin d) {W : Set (HCPolySupport.Vec d)} (hW : MeasurableSet W) : MeasureTheory.volume (HCPolySupport.coordFaceReflection a i ⁻¹' W) = MeasureTheory.volume W

The reflection preserves Lebesgue measure, so a window and its preimage have the same volume.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.setIntegral_comp_coordFaceReflection {d : ℕ} {a : ℝ} (i : Fin d) {W : Set (HCPolySupport.Vec d)} (hW : MeasurableSet W) (f : HCPolySupport.Vec d → ℝ) : ∫ (y : HCPolySupport.Vec d) in HCPolySupport.coordFaceReflection a i ⁻¹' W, f (HCPolySupport.coordFaceReflection a i y) = ∫ (y : HCPolySupport.Vec d) in W, f y

The change of variables. Integrating f ∘ σ_i over the reflected window is integrating f over the window, with no Jacobian.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volumeAverage_comp_coordFaceReflection {d : ℕ} {a : ℝ} (i : Fin d) {W : Set (HCPolySupport.Vec d)} (hW : MeasurableSet W) (f : HCPolySupport.Vec d → ℝ) : (HCPolySupport.volumeAverage (HCPolySupport.coordFaceReflection a i ⁻¹' W) fun (y : HCPolySupport.Vec d) => f (HCPolySupport.coordFaceReflection a i y)) = HCPolySupport.volumeAverage W f

The volume average is invariant: both the normalizer and the integral transport.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_comp_coordFaceReflection {d : ℕ} {a : ℝ} (i : Fin d) {W : Set (HCPolySupport.Vec d)} (hW : MeasurableSet W) (f : HCPolySupport.Vec d → ℝ) : (Support.normalizedL2On (HCPolySupport.coordFaceReflection a i ⁻¹' W) fun (y : HCPolySupport.Vec d) => f (HCPolySupport.coordFaceReflection a i y)) = Support.normalizedL2On W f

The volume-normalized L² seminorm is invariant under the reflection.

3. The affine transport at the face coordinate 0

theorem Algsuperdiff.Section4.Provider.ExcessDecay.vecDot_coordFaceReflection_zero {d : ℕ} (i : Fin d) (g y : HCPolySupport.Vec d) : HCPolySupport.vecDot g (HCPolySupport.coordFaceReflection 0 i y) = HCPolySupport.vecDot (HCPolySupport.coordFaceReflection 0 i g) y

Self-adjointness of the coordinate negation. At a = 0 the reflection is linear and orthogonal, so it moves across the euclidean pairing.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.affineEval_comp_coordFaceReflection_zero {d : ℕ} (i : Fin d) (c : ℝ) (g y : HCPolySupport.Vec d) : Support.affineEval c g (HCPolySupport.coordFaceReflection 0 i y) = Support.affineEval c (HCPolySupport.coordFaceReflection 0 i g) y

The affine family is carried onto itself. Precomposing the affine function (c, g) with the coordinate negation is the affine function (c, σ_i g): the intercept is untouched and the slope is reflected.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.affineDistOn_comp_coordFaceReflection_zero {d : ℕ} (i : Fin d) {W : Set (HCPolySupport.Vec d)} (hW : MeasurableSet W) (f : HCPolySupport.Vec d → ℝ) (c : ℝ) (g : HCPolySupport.Vec d) : Support.affineDistOn (HCPolySupport.coordFaceReflection 0 i ⁻¹' W) (fun (y : HCPolySupport.Vec d) => f (HCPolySupport.coordFaceReflection 0 i y)) c (HCPolySupport.coordFaceReflection 0 i g) = Support.affineDistOn W f c g

The affine distance is invariant, with the slope reflected along.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.affineDistSet_comp_coordFaceReflection_zero {d : ℕ} (i : Fin d) {W : Set (HCPolySupport.Vec d)} (hW : MeasurableSet W) (f : HCPolySupport.Vec d → ℝ) : (Support.affineDistSet (HCPolySupport.coordFaceReflection 0 i ⁻¹' W) fun (y : HCPolySupport.Vec d) => f (HCPolySupport.coordFaceReflection 0 i y)) = Support.affineDistSet W f

The competitor set is invariant. The bijection (c, g) ↦ (c, σ_i g) of the affine parameter space ℝ × Vec d --- its own inverse, by involutivity --- matches the two competitor families.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.affineExcessRaw_comp_coordFaceReflection_zero {d : ℕ} (i : Fin d) {W : Set (HCPolySupport.Vec d)} (hW : MeasurableSet W) (f : HCPolySupport.Vec d → ℝ) : (Support.affineExcessRaw (HCPolySupport.coordFaceReflection 0 i ⁻¹' W) fun (y : HCPolySupport.Vec d) => f (HCPolySupport.coordFaceReflection 0 i y)) = Support.affineExcessRaw W f

The unnormalized excess is invariant: it is the infimum of an invariant set.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isAffineMinimizer_comp_coordFaceReflection_zero {d : ℕ} (i : Fin d) {W : Set (HCPolySupport.Vec d)} (hW : MeasurableSet W) (f : HCPolySupport.Vec d → ℝ) (c : ℝ) (g : HCPolySupport.Vec d) : Support.IsAffineMinimizer (HCPolySupport.coordFaceReflection 0 i ⁻¹' W) (fun (y : HCPolySupport.Vec d) => f (HCPolySupport.coordFaceReflection 0 i y)) c (HCPolySupport.coordFaceReflection 0 i g) ↔ Support.IsAffineMinimizer W f c g

The best-affine predicate transports both ways: (c, g) is a minimizer for f on W exactly when (c, σ_i g) is one for f ∘ σ_i on σ_i ⁻¹' W.

4. The L² side condition

theorem Algsuperdiff.Section4.Provider.ExcessDecay.memLp_comp_coordFaceReflection {d : ℕ} {a : ℝ} (i : Fin d) {W : Set (HCPolySupport.Vec d)} (hW : MeasurableSet W) {f : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict W)) : MeasureTheory.MemLp (fun (y : HCPolySupport.Vec d) => f (HCPolySupport.coordFaceReflection a i y)) 2 (MeasureTheory.volume.restrict (HCPolySupport.coordFaceReflection a i ⁻¹' W))

The MemLp hypothesis of the NormalizedL2 calculus transports along the reflection, so no side condition is lost when the boundary branch is moved.