Coarse-graining support: Support.Probability.RegCoeffField.Laws

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Structural laws on the carrier

This file restates the law-level structural predicates of HCPolySupport.Probability.RandomField on the honest-fields carrier RegCoeffLaw d = Measure (RegCoeffField d), using the carrier endomorphisms of Endomorphisms.lean in place of the raw-CoeffField ones. The semantic shapes are preserved:

• IsStationaryR — invariance under integer translations;
• IsRestrictionUnitRangeDependentR — independence of the restriction σ-algebras of unit-separated measurable sets (the MeasurableSet side-conditions are the D7-approved refinement making RestrictionSigmaR well defined);
• IsIsotropicInLawR — invariance under signed-permutation rotations;
• IsAdjointInvariantInLawR — invariance under the entrywise adjoint.

Each Measure.map is well formed: the underlying endomorphism is measurable (measurable_translateReg, measurable_rotateReg, measurable_adjointReg), and we record the corresponding integral/integrable transfer lemmas.

Reference: the paper (Armstrong–Kuusi–Loher, to appear).

Stationarity

def HCPolySupport.IsStationaryR {d : ℕ} (P : RegCoeffLaw d) : Prop

A carrier law is stationary if it is invariant under every integer translation (mirrors IsStationary).

Equations

• HCPolySupport.IsStationaryR P = ∀ (z : Fin d → ℤ), MeasureTheory.Measure.map (HCPolySupport.translateReg (HCPolySupport.intVecToRealVec z)) P = P

theorem HCPolySupport.IsStationaryR.integral_comp_translateReg {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {P : RegCoeffLaw d} (hP : IsStationaryR P) (z : Fin d → ℤ) (f : RegCoeffField d → E) (hf : MeasureTheory.AEStronglyMeasurable f P) : ∫ (a : RegCoeffField d), f (translateReg (intVecToRealVec z) a) ∂P = ∫ (a : RegCoeffField d), f a ∂P

Integral transfer under integer translation for a stationary carrier law.

Unit-range dependence

def HCPolySupport.IsRestrictionUnitRangeDependentR {d : ℕ} (P : RegCoeffLaw d) : Prop

A carrier law is restriction-unit-range dependent if the restriction σ-algebras of any two sup-unit-separated measurable sets are independent. This is the pointwise-restriction lane, with the MeasurableSet refinement, and is distinct from the exact source-integral/Euclidean locality assumption; the differing separation predicates preclude a generic P2 implication.

Equations

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

Isotropy

def HCPolySupport.IsIsotropicInLawR {d : ℕ} (P : RegCoeffLaw d) : Prop

A carrier law is isotropic if it is invariant under every signed-permutation rotation (mirrors IsIsotropicInLaw).

Equations

• HCPolySupport.IsIsotropicInLawR P = ∀ (R : HCPolySupport.Mat d) (hR : HCPolySupport.IsSignedPermutationMatrix R), MeasureTheory.Measure.map (HCPolySupport.rotateReg R hR) P = P

theorem HCPolySupport.IsIsotropicInLawR.integral_comp_rotateReg {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {P : RegCoeffLaw d} (hP : IsIsotropicInLawR P) {R : Mat d} (hR : IsSignedPermutationMatrix R) (f : RegCoeffField d → E) (hf : MeasureTheory.AEStronglyMeasurable f P) : ∫ (a : RegCoeffField d), f (rotateReg R hR a) ∂P = ∫ (a : RegCoeffField d), f a ∂P

Integral transfer under a signed-permutation rotation for an isotropic law.

Adjoint invariance

def HCPolySupport.IsAdjointInvariantInLawR {d : ℕ} (P : RegCoeffLaw d) : Prop

A carrier law is adjoint invariant if it is invariant under the entrywise adjoint (mirrors IsAdjointInvariantInLaw).

Equations

• HCPolySupport.IsAdjointInvariantInLawR P = (MeasureTheory.Measure.map HCPolySupport.adjointReg P = P)

theorem HCPolySupport.IsAdjointInvariantInLawR.integral_comp_adjointReg {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {P : RegCoeffLaw d} (hP : IsAdjointInvariantInLawR P) (f : RegCoeffField d → E) (hf : MeasureTheory.AEStronglyMeasurable f P) : ∫ (a : RegCoeffField d), f (adjointReg a) ∂P = ∫ (a : RegCoeffField d), f a ∂P

Integral transfer under the adjoint for an adjoint-invariant law.