RelativeNormalization

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

Same-cutoff relative normalization

The canonical normalization used elsewhere is indexed by a natural dilation depth. Section 3.5 instead compares arbitrary integer cutoff and observation scales. This file keeps the cutoff index fixed and rescales space by the integer-dependent factor 3^(m+c), where the dimension-only shift c leaves strict room for CoarseGraining's unit-range bridge.

No covariance between different cutoff indices is asserted. The normalized law is exactly a spatial pushforward of coefficientCutoffLaw M m at the same m.

noncomputable def Algsuperdiff.Section3.Cutoff.scaledCoefficientCutoffLaw {d : ℕ} (M : ABKModel d) (m : ℤ) (r : ℝ) (hr : r ≠ 0) : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d

The law of the genuine cutoff after the spatial change a(x) ↦ a(r x).

Equations

• Algsuperdiff.Section3.Cutoff.scaledCoefficientCutoffLaw M m r hr = MeasureTheory.Measure.map (HCPolySupport.smulReg r hr) (Algsuperdiff.Section3.Cutoff.coefficientCutoffLaw M m)

instance Algsuperdiff.Section3.Cutoff.scaledCoefficientCutoffLaw_isProbabilityMeasure {d : ℕ} (M : ABKModel d) (m : ℤ) (r : ℝ) (hr : r ≠ 0) : MeasureTheory.IsProbabilityMeasure (scaledCoefficientCutoffLaw M m r hr)

theorem Algsuperdiff.Section3.Cutoff.scaledCoefficientCutoffLaw_stationary_real {d : ℕ} (M : ABKModel d) (m : ℤ) {r : ℝ} (hr : r ≠ 0) (z : HCPolySupport.Vec d) : MeasureTheory.Measure.map (HCPolySupport.translateReg z) (scaledCoefficientCutoffLaw M m r hr) = scaledCoefficientCutoffLaw M m r hr

Real-translation stationarity survives every nonzero spatial scaling.

theorem Algsuperdiff.Section3.Cutoff.scaledCoefficientCutoffLaw_stationary {d : ℕ} (M : ABKModel d) (m : ℤ) {r : ℝ} (hr : r ≠ 0) : HCPolySupport.Book.Ch04.RestrictionStationaryLaw (scaledCoefficientCutoffLaw M m r hr)

CoarseGraining's integer-translation stationarity for a spatially scaled cutoff law.

theorem Algsuperdiff.Section3.Cutoff.scaledCoefficientCutoffLaw_isotropic {d : ℕ} (M : ABKModel d) (m : ℤ) {r : ℝ} (hr : r ≠ 0) : HCPolySupport.Book.Ch04.RestrictionIsotropicLaw (scaledCoefficientCutoffLaw M m r hr)

Signed-permutation isotropy survives every nonzero spatial scaling.

theorem Algsuperdiff.Section3.Cutoff.scaledCoefficientCutoffLaw_adjoint_invariant {d : ℕ} (M : ABKModel d) (m : ℤ) {r : ℝ} (hr : r ≠ 0) : HCPolySupport.Book.Ch04.RestrictionAdjointInvariantLaw (scaledCoefficientCutoffLaw M m r hr)

Adjoint invariance survives every nonzero spatial scaling.

theorem Algsuperdiff.Section3.Cutoff.scaledCoefficientCutoffLaw_unitRangeDependent {d : ℕ} (M : ABKModel d) (m : ℤ) {r : ℝ} (hr : r ≠ 0) (hrpos : 0 < r) (hslack : cutoffNaturalRange d m < r * (1 - 2 * cutoffBridgeEpsilon)) : HCPolySupport.Book.Ch04.RestrictionUnitRangeDependentLaw (scaledCoefficientCutoffLaw M m r hr)

Any positive scaling that leaves the fixed thickening slack turns the literal cutoff range into CoarseGraining's exact unit-range dependence predicate.

noncomputable def Algsuperdiff.Section3.Cutoff.cutoffRelativeNormalizationShift (d : ℕ) : ℕ

Dimension-only buffer used by the same-cutoff relative normalization.

Equations

• Algsuperdiff.Section3.Cutoff.cutoffRelativeNormalizationShift d = Algsuperdiff.Section3.Cutoff.cutoffNormalizationDepth d 0

noncomputable def Algsuperdiff.Section3.Cutoff.cutoffRelativeNormalizationScale (d : ℕ) (m : ℤ) : ℝ

The relative normalization factor 3^(m+c).

Equations

• Algsuperdiff.Section3.Cutoff.cutoffRelativeNormalizationScale d m = 3 ^ (m + ↑(Algsuperdiff.Section3.Cutoff.cutoffRelativeNormalizationShift d))

theorem Algsuperdiff.Section3.Cutoff.cutoffRelativeNormalizationScale_pos (d : ℕ) (m : ℤ) : 0 < cutoffRelativeNormalizationScale d m

theorem Algsuperdiff.Section3.Cutoff.cutoffRelativeNormalizationScale_ne_zero (d : ℕ) (m : ℤ) : cutoffRelativeNormalizationScale d m ≠ 0

theorem Algsuperdiff.Section3.Cutoff.cutoffRelativeNormalizationScale_strict_slack (d : ℕ) (m : ℤ) : cutoffNaturalRange d m < cutoffRelativeNormalizationScale d m * (1 - 2 * cutoffBridgeEpsilon)

noncomputable def Algsuperdiff.Section3.Cutoff.relativeNormalizedCutoffLaw {d : ℕ} (M : ABKModel d) (m : ℤ) : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d

The same-cutoff relative law. Its spatial scaling depends on m, but its cutoff-law index remains exactly m.

Equations

• Algsuperdiff.Section3.Cutoff.relativeNormalizedCutoffLaw M m = Algsuperdiff.Section3.Cutoff.scaledCoefficientCutoffLaw M m (Algsuperdiff.Section3.Cutoff.cutoffRelativeNormalizationScale d m) ⋯

instance Algsuperdiff.Section3.Cutoff.relativeNormalizedCutoffLaw_isProbabilityMeasure {d : ℕ} (M : ABKModel d) (m : ℤ) : MeasureTheory.IsProbabilityMeasure (relativeNormalizedCutoffLaw M m)

theorem Algsuperdiff.Section3.Cutoff.relativeNormalizedCutoffLaw_stationary_real {d : ℕ} (M : ABKModel d) (m : ℤ) (z : HCPolySupport.Vec d) : MeasureTheory.Measure.map (HCPolySupport.translateReg z) (relativeNormalizedCutoffLaw M m) = relativeNormalizedCutoffLaw M m

theorem Algsuperdiff.Section3.Cutoff.relativeNormalizedCutoffLaw_stationary {d : ℕ} (M : ABKModel d) (m : ℤ) : HCPolySupport.Book.Ch04.RestrictionStationaryLaw (relativeNormalizedCutoffLaw M m)

theorem Algsuperdiff.Section3.Cutoff.relativeNormalizedCutoffLaw_unitRangeDependent {d : ℕ} (M : ABKModel d) (m : ℤ) : HCPolySupport.Book.Ch04.RestrictionUnitRangeDependentLaw (relativeNormalizedCutoffLaw M m)

theorem Algsuperdiff.Section3.Cutoff.relativeNormalizedCutoffLaw_eq_map_dilateReg {d : ℕ} (M : ABKModel d) (m : ℤ) : relativeNormalizedCutoffLaw M m = MeasureTheory.Measure.map (HCPolySupport.dilateReg (-(m + ↑(cutoffRelativeNormalizationShift d)))) (coefficientCutoffLaw M m)

The relative law is exactly the integer dilation proposed by the source-relative scale arithmetic.

theorem Algsuperdiff.Section3.Cutoff.aelocallyUniformlyEllipticField_dilateReg {d : ℕ} {a : HCPolySupport.RegCoeffField d} (ha : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField a) (k : ℤ) : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField (HCPolySupport.dilateReg k a)

Local a.e. uniform ellipticity is preserved by every integer triadic dilation, with no sign restriction on the dilation exponent.

theorem Algsuperdiff.Section3.Cutoff.triadicCoeffFamily_dilateReg_aeeq_dilate {d : ℕ} {a : HCPolySupport.RegCoeffField d} (ha : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField a) (k : ℤ) : (HCPolySupport.Book.Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField (HCPolySupport.dilateReg k a) ⋯).AEEq (HCPolySupport.Book.Ch02.TriadicCoeffFamily.dilate k (HCPolySupport.Book.Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha))

The canonical Chapter 4 family of an integer-dilated field agrees a.e. with the literal Chapter 2 dilation of the original canonical family.

noncomputable def Algsuperdiff.Section3.Cutoff.dilateRegMeasurableEquiv {d : ℕ} (k : ℤ) : HCPolySupport.RegCoeffField d ≃ᵐ HCPolySupport.RegCoeffField d

Triadic dilation of regular coefficient fields as a measurable equivalence.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Cutoff.relativeNormalizedCutoffLaw_aeLocallyUniformlyElliptic {d : ℕ} (M : ABKModel d) (m : ℤ) : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticLaw (relativeNormalizedCutoffLaw M m)

The relative law is supported on the exact Chapter 4 local ellipticity carrier.

theorem Algsuperdiff.Section3.Cutoff.relativeNormalizedCutoffLaw_lawCarrier {d : ℕ} (M : ABKModel d) (m : ℤ) : HCPolySupport.Book.Ch04.RestrictionLawCarrier (relativeNormalizedCutoffLaw M m)

The relative law is a Chapter 4 restriction-law carrier.

theorem Algsuperdiff.Section3.Cutoff.relativeNormalizedCutoffLaw_structuralLaw {d : ℕ} (M : ABKModel d) (m : ℤ) : HCPolySupport.Book.Ch04.RestrictionStructuralLaw (relativeNormalizedCutoffLaw M m)

Full structural package for the same-cutoff relative normalization.