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

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

Carrier endomorphisms

This file equips the regular-fields carrier RegCoeffField d with the structural self-maps used by the law layer of the homogenization development: spatial translation, signed-permutation rotation (isotropy), triadic rescaling and dilation, restriction to a measurable set, and elliptic truncation. Each map is shown to preserve the carrier (entrywise Borel measurability and local integrability are stable) and, where possible, to be genuinely measurable for the canonical carrier σ-algebra pointwiseSigmaR ⊔ entryTestSigmaR.

The measurability proofs go through the P1 probe-transport criterion measurable_of_entryTestR_transport: each entry generator on the transformed field equals a scalar multiple of a relabelled entry generator on the input, the scalar being the Jacobian factor of the underlying change of variables.

translateReg, rotateReg, rescaleReg, dilateReg and restrictReg are genuinely measurable at the join. ellipticTruncateReg is a genuine carrier element and is measurable for the pointwise lane; its entry-test lane is a nonlinear integral functional that is not a transported generator (see the note at that declaration).

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

Local-integrability transport under a homeomorphism

theorem HCPolySupport.locallyIntegrable_comp_homeomorph_of_map_smul {d : ℕ} {f : Vec d → ℝ} (hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume) (e : Vec d ≃ₜ Vec d) {c : ENNReal} (hc0 : c ≠ 0) (hctop : c ≠ ⊤) (hmap : MeasureTheory.Measure.map (⇑e) MeasureTheory.volume = c • MeasureTheory.volume) : MeasureTheory.LocallyIntegrable (fun (x : Vec d) => f (e x)) MeasureTheory.volume

Local integrability is stable under precomposition with a homeomorphism whose pushforward of Lebesgue measure is a finite nonzero rescaling of Lebesgue measure. This covers translation and rotation (c = 1) and triadic rescaling/dilation (c the Jacobian factor).

theorem HCPolySupport.locallyIntegrable_comp_homeomorph_of_measurePreserving {d : ℕ} {f : Vec d → ℝ} (hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume) (e : Vec d ≃ₜ Vec d) (hmp : MeasureTheory.MeasurePreserving (⇑e) MeasureTheory.volume MeasureTheory.volume) : MeasureTheory.LocallyIntegrable (fun (x : Vec d) => f (e x)) MeasureTheory.volume

Local-integrability transport under a measure-preserving homeomorphism.

Matrix-action infrastructure (re-derived, public)

theorem HCPolySupport.continuous_matVecMul {d : ℕ} (R : Mat d) : Continuous fun (x : Vec d) => matVecMul R x

Continuity of the linear action x ↦ R x (local copy of the raw-layer private lemma).

theorem HCPolySupport.matVecMul_one' {d : ℕ} (x : Vec d) : matVecMul 1 x = x

def HCPolySupport.matVecMulHomeomorph {d : ℕ} (R : Mat d) (hR : IsSignedPermutationMatrix R) : Vec d ≃ₜ Vec d

A signed permutation acts as a homeomorphism of the base space.

Equations

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

@[simp]

theorem HCPolySupport.matVecMulHomeomorph_apply {d : ℕ} (R : Mat d) (hR : IsSignedPermutationMatrix R) (x : Vec d) : (matVecMulHomeomorph R hR) x = matVecMul R x

theorem HCPolySupport.measurePreserving_matVecMul {d : ℕ} (R : Mat d) (hR : IsSignedPermutationMatrix R) : MeasureTheory.MeasurePreserving (fun (x : Vec d) => matVecMul R x) MeasureTheory.volume MeasureTheory.volume

The signed-permutation action preserves Lebesgue measure (|det R| = 1).

Translation

def HCPolySupport.translateReg {d : ℕ} (z : Vec d) (a : RegCoeffField d) : RegCoeffField d

Precomposition with the spatial translation x ↦ x + z is a carrier endomorphism (mirrors translateCoeffField on the raw carrier).

Equations

• HCPolySupport.translateReg z a = { toFun := fun (x : HCPolySupport.Vec d) => a.toFun (x + z), entry_measurable := ⋯, entry_locInt := ⋯ }

@[simp]

theorem HCPolySupport.translateReg_apply {d : ℕ} (z : Vec d) (a : RegCoeffField d) (x : Vec d) : (translateReg z a).toFun x = a.toFun (x + z)

theorem HCPolySupport.entryTestR_translateReg {d : ℕ} (i j : Fin d) (φ : Vec d → ℝ) (z : Vec d) (a : RegCoeffField d) : entryTestR i j φ (translateReg z a) = entryTestR i j (fun (y : Vec d) => φ (y - z)) a

Generator transport for translation: the entry test of a translated field is the entry test against the back-translated probe (Jacobian factor 1).

theorem HCPolySupport.measurable_translateReg {d : ℕ} (z : Vec d) : Measurable (translateReg z)

Translation is genuinely measurable at the join.

Signed-permutation rotation (isotropy)

theorem HCPolySupport.matTranspose_mul_mul_apply {d : ℕ} {R : Mat d} {σ : Equiv.Perm (Fin d)} {s : Fin d → ℝ} (hRdef : ∀ (i j : Fin d), R i j = if i = σ j then s j else 0) (M : Mat d) (i j : Fin d) : (matTranspose R * M * R) i j = s i * s j * M (σ i) (σ j)

The conjugation-by-R collapse for a signed permutation R with underlying permutation σ and signs s: (Rᵀ M R)_{ij} = s_i s_j M_{σ i, σ j}. This is the algebraic heart of the isotropy endomorphism.

def HCPolySupport.rotateReg {d : ℕ} (R : Mat d) (hR : IsSignedPermutationMatrix R) (a : RegCoeffField d) : RegCoeffField d

Precomposition-and-conjugation with a signed permutation R is a carrier endomorphism (mirrors rotateCoeffField). The signed-permutation hypothesis is what makes local integrability stable: matVecMul R is a measure-preserving homeomorphism.

Equations

• HCPolySupport.rotateReg R hR a = { toFun := fun (x : HCPolySupport.Vec d) => HCPolySupport.matTranspose R * a.toFun (HCPolySupport.matVecMul R x) * R, entry_measurable := ⋯, entry_locInt := ⋯ }

@[simp]

theorem HCPolySupport.rotateReg_apply {d : ℕ} (R : Mat d) (hR : IsSignedPermutationMatrix R) (a : RegCoeffField d) (x : Vec d) : (rotateReg R hR a).toFun x = matTranspose R * a.toFun (matVecMul R x) * R

theorem HCPolySupport.measurable_rotateReg {d : ℕ} (R : Mat d) (hR : IsSignedPermutationMatrix R) : Measurable (rotateReg R hR)

Signed-permutation rotation is genuinely measurable at the join.

Spatial scaling (rescale / dilate)

def HCPolySupport.smulReg {d : ℕ} (r : ℝ) (hr : r ≠ 0) (a : RegCoeffField d) : RegCoeffField d

Precomposition with a nonzero spatial scaling x ↦ r • x is a carrier endomorphism. Local integrability is stable because the scaling is a homeomorphism whose Jacobian is the finite nonzero factor |r|^{-d}; the entry generators transport with exactly this scalar.

Equations

• HCPolySupport.smulReg r hr a = { toFun := fun (x : HCPolySupport.Vec d) => a.toFun (r • x), entry_measurable := ⋯, entry_locInt := ⋯ }

@[simp]

theorem HCPolySupport.smulReg_apply {d : ℕ} (r : ℝ) (hr : r ≠ 0) (a : RegCoeffField d) (x : Vec d) : (smulReg r hr a).toFun x = a.toFun (r • x)

theorem HCPolySupport.entryTestR_smulReg {d : ℕ} (i j : Fin d) (φ : Vec d → ℝ) (r : ℝ) (hr : r ≠ 0) (a : RegCoeffField d) : entryTestR i j φ (smulReg r hr a) = |(r ^ Module.finrank ℝ (Vec d))⁻¹| * entryTestR i j (fun (y : Vec d) => φ (r⁻¹ • y)) a

Generator transport for a spatial scaling: the entry test of a scaled field is the Jacobian factor |r|^{-d} times the entry test against the inverse-scaled probe.

theorem HCPolySupport.measurable_smulReg {d : ℕ} (r : ℝ) (hr : r ≠ 0) : Measurable (smulReg r hr)

Spatial scaling is genuinely measurable at the join.

def HCPolySupport.rescaleReg {d : ℕ} (n : ℕ) : RegCoeffField d → RegCoeffField d

Triadic rescaling by 3^n (mirrors rescaleCoeffField): the rescaled field is x ↦ a(3^n • x).

Equations

• HCPolySupport.rescaleReg n = HCPolySupport.smulReg (3 ^ n) ⋯

@[simp]

theorem HCPolySupport.rescaleReg_apply {d : ℕ} (n : ℕ) (a : RegCoeffField d) (x : Vec d) : (rescaleReg n a).toFun x = a.toFun (3 ^ n • x)

theorem HCPolySupport.measurable_rescaleReg {d : ℕ} (n : ℕ) : Measurable (rescaleReg n)

noncomputable def HCPolySupport.dilateReg {d : ℕ} (k : ℤ) : RegCoeffField d → RegCoeffField d

Triadic dilation by 3^k (mirrors dilateCoeffField): the dilated field is x ↦ a(3^{-k} • x).

Equations

• HCPolySupport.dilateReg k = HCPolySupport.smulReg (3 ^ k)⁻¹ ⋯

@[simp]

theorem HCPolySupport.dilateReg_apply {d : ℕ} (k : ℤ) (a : RegCoeffField d) (x : Vec d) : (dilateReg k a).toFun x = a.toFun ((3 ^ k)⁻¹ • x)

theorem HCPolySupport.measurable_dilateReg {d : ℕ} (k : ℤ) : Measurable (dilateReg k)

Restriction to a measurable set

noncomputable def HCPolySupport.restrictReg {d : ℕ} (U : Set (Vec d)) (hU : MeasurableSet U) (a : RegCoeffField d) : RegCoeffField d

Restriction of a carrier field to a measurable set U (zero outside U; mirrors restrictCoeffField). Both regularity conjuncts are stable: the restricted entries are indicator products.

Equations

• HCPolySupport.restrictReg U hU a = { toFun := U.indicator a.toFun, entry_measurable := ⋯, entry_locInt := ⋯ }

@[simp]

theorem HCPolySupport.restrictReg_apply {d : ℕ} (U : Set (Vec d)) (hU : MeasurableSet U) (a : RegCoeffField d) (x : Vec d) : (restrictReg U hU a).toFun x = U.indicator a.toFun x

theorem HCPolySupport.restrictReg_apply_entry {d : ℕ} (U : Set (Vec d)) (hU : MeasurableSet U) (a : RegCoeffField d) (x : Vec d) (i j : Fin d) : (restrictReg U hU a).toFun x i j = U.indicator (fun (x : Vec d) => a.toFun x i j) x

theorem HCPolySupport.entryTestR_restrictReg {d : ℕ} (i j : Fin d) (φ : Vec d → ℝ) (U : Set (Vec d)) (hU : MeasurableSet U) (a : RegCoeffField d) : entryTestR i j φ (restrictReg U hU a) = entryTestR i j (U.indicator φ) a

Generator transport for restriction: the entry test of a restricted field is the entry test against the indicator-masked probe (Jacobian factor 1).

theorem HCPolySupport.measurable_restrictReg {d : ℕ} (U : Set (Vec d)) (hU : MeasurableSet U) : Measurable (restrictReg U hU)

Restriction is genuinely measurable at the join.

Elliptic truncation

ellipticTruncateReg Θ a keeps a x where it is (1, Θ)-elliptic and replaces it by the identity elsewhere (mirrors the coarse-graining a.e.-bridge truncation). It is a genuine carrier element: on the elliptic branch the entries are bounded by Θ (abs_apply_le_of_isEllipticMatrix), off it they are entries of the identity matrix, so each entry is bounded and measurable, hence locally integrable.

Measurability (research item). The pointwise lane is genuinely measurable (measurable_pointwiseSigmaR_ellipticTruncateReg): the elliptic locus is Borel (measurableSet_isEllipticMatrix), so each coordinate a ↦ (trunc a) y_{ij} is a piecewise-measurable function of the evaluations of a. The entry-test lane, however, is not a transported generator: entryTestR i j φ (trunc a) is the integral of a genuinely nonlinear (piecewise) function of the matrix values a x, not a scalar multiple of a linear entry generator of a. On the carrier the joint map (a, x) ↦ a x is not measurable for the pointwise product σ-algebra (uncountably many coordinates), and no monotone-class approximation is available for merely locally-integrable a (Riemann sums need not converge), so the entry-test lane cannot be discharged from the P1 generators. We therefore land ellipticTruncateReg with pointwise-lane measurability only and flag the join measurability as a design signal for the consumer packets (P5/P7).

noncomputable def HCPolySupport.ellipticTruncateReg {d : ℕ} (Θ : ℝ) (a : RegCoeffField d) : RegCoeffField d

The regular coefficient field retaining a x where it has ellipticity parameters 1 and Θ, and replacing it by the identity elsewhere.

Equations

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

@[simp]

theorem HCPolySupport.ellipticTruncateReg_apply {d : ℕ} (Θ : ℝ) (a : RegCoeffField d) (x : Vec d) : (ellipticTruncateReg Θ a).toFun x = if IsEllipticMatrix 1 Θ (a.toFun x) then a.toFun x else 1

theorem HCPolySupport.measurable_pointwiseSigmaR_ellipticTruncateReg {d : ℕ} (Θ : ℝ) : Measurable (ellipticTruncateReg Θ)

The elliptic truncation is measurable for the pointwise lane. See the declaration docstring: the entry-test lane is a design signal (nonlinear integral functional, no monotone-class route on the carrier), so join measurability is deliberately not claimed here.