Coarse-graining support: Support.Book.Ch04.Theorems.DilationLaw

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

Dilation of Chapter 4 laws

This file starts the law-facing dilation API used in Section 5.5. The normalized law is the push-forward of the original coefficient law by the triadic pullback which sends scale k in the original coordinates to scale zero in normalized coordinates.

noncomputable def HCPolySupport.Book.Ch04.restrictionScaleNormalizedLaw {d : ℕ} (k : ℕ) (P : RestrictionCoeffLaw d) : RestrictionCoeffLaw d

Scale-normalize a carrier coefficient law by pulling honest fields back under the triadic dilation x ↦ 3^k x (the carrier endomorphism dilateReg).

Equations

• HCPolySupport.Book.Ch04.restrictionScaleNormalizedLaw k P = MeasureTheory.Measure.map (HCPolySupport.dilateReg (-↑k)) P

theorem HCPolySupport.Book.Ch04.rescaleCoeffField_eq_dilateCoeffField_neg_nat {d : ℕ} (k : ℕ) : rescaleCoeffField k = Ch02.dilateCoeffField (-↑k)

The existing probability-layer rescaling is the same map as the Ch2 dilation by the negative natural scale (raw coefficient fields; kept as the public raw-layer bridge still consumed by the coarse-graining and high-contrast tracks).

theorem HCPolySupport.Book.Ch04.rescaleReg_toFun {d : ℕ} (k : ℕ) (a : RegCoeffField d) : (rescaleReg k a).toFun = rescaleCoeffField k a.toFun

The honest sample of a triadically rescaled carrier field is the raw triadic rescaling of its honest sample (rfl).

theorem HCPolySupport.Book.Ch04.dilateReg_toFun {d : ℕ} (k : ℤ) (a : RegCoeffField d) : (dilateReg k a).toFun = Ch02.dilateCoeffField k a.toFun

The honest sample of a triadically dilated carrier field is the raw triadic dilation of its honest sample (rfl).

theorem HCPolySupport.Book.Ch04.rescaleReg_eq_dilateReg_neg_nat {d : ℕ} (k : ℕ) : rescaleReg k = dilateReg (-↑k)

The carrier triadic rescaling by 3^k is the carrier dilation by the negative natural scale (carrier analog of rescaleCoeffField_eq_dilateCoeffField_neg_nat).

theorem HCPolySupport.Book.Ch04.restrictionScaleNormalizedLaw_eq_map_rescaleReg {d : ℕ} (k : ℕ) (P : RestrictionCoeffLaw d) : restrictionScaleNormalizedLaw k P = MeasureTheory.Measure.map (rescaleReg k) P

restrictionScaleNormalizedLaw is the pushforward under the carrier triadic rescaling.

theorem HCPolySupport.Book.Ch04.isProbabilityMeasure_restrictionScaleNormalizedLaw {d : ℕ} (k : ℕ) (P : RestrictionCoeffLaw d) [MeasureTheory.IsProbabilityMeasure P] : MeasureTheory.IsProbabilityMeasure (restrictionScaleNormalizedLaw k P)

A scale-normalized probability law is again a probability law.

theorem HCPolySupport.Book.Ch04.integral_restrictionScaleNormalizedLaw {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {P : RestrictionCoeffLaw d} (k : ℕ) (X : RegCoeffField d → E) (hX : MeasureTheory.AEStronglyMeasurable X (restrictionScaleNormalizedLaw k P)) : ∫ (a : RegCoeffField d), X a ∂restrictionScaleNormalizedLaw k P = ∫ (a : RegCoeffField d), X (dilateReg (-↑k) a) ∂P

Bochner integral under a scale-normalized law.

theorem HCPolySupport.Book.Ch04.integrable_restrictionScaleNormalizedLaw_iff {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {P : RestrictionCoeffLaw d} (k : ℕ) {X : RegCoeffField d → E} (hX : MeasureTheory.AEStronglyMeasurable X (restrictionScaleNormalizedLaw k P)) : MeasureTheory.Integrable X (restrictionScaleNormalizedLaw k P) ↔ MeasureTheory.Integrable (fun (a : RegCoeffField d) => X (dilateReg (-↑k) a)) P

Integrability under a scale-normalized law is integrability after composing with the defining dilation.

theorem HCPolySupport.Book.Ch04.measurableSet_triadicDilateSet {d : ℕ} (k : ℕ) {U : Set (Vec d)} (hU : MeasurableSet U) : MeasurableSet (triadicDilateSet k U)

Triadic dilation preserves Borel measurability of ambient regions: the image of a measurable set under scaling by 3^k is the preimage of that set under scaling by (3^k)⁻¹, hence measurable.

theorem HCPolySupport.Book.Ch04.restrictReg_comp_rescaleReg_eq {d : ℕ} (k : ℕ) (U : Set (Vec d)) (hU : MeasurableSet U) : restrictReg U hU ∘ rescaleReg k = rescaleReg k ∘ restrictReg (triadicDilateSet k U) ⋯

Restriction/dilation commutation on the carrier. Restricting a triadically rescaled field to U equals rescaling the field restricted to the dilated set triadicDilateSet k U — the escape route recorded in the LOCALSIGMA plan.

theorem HCPolySupport.Book.Ch04.measurable_rescaleReg_restrictionSigmaR {d : ℕ} (k : ℕ) (U : Set (Vec d)) (hU : MeasurableSet U) : Measurable (rescaleReg k)

Pullback by carrier triadic rescaling sends restriction-local information on U to restriction-local information on the dilated set.

noncomputable def HCPolySupport.Book.Ch04.rescaleRegMeasurableEquiv {d : ℕ} (k : ℕ) : RegCoeffField d ≃ᵐ RegCoeffField d

The carrier triadic rescaling is a measurable equivalence, with inverse the carrier dilation by the positive scale.

Equations

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

theorem HCPolySupport.Book.Ch04.RestrictionUnitRangeDependentLaw.scaleNormalized {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionUnitRangeDependentLaw P) (k : ℕ) : RestrictionUnitRangeDependentLaw (restrictionScaleNormalizedLaw k P)

Restriction-unit-range dependence is preserved by triadic scale-normalization.

theorem HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField.of_rescaleCoeffField {d : ℕ} {a : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) (k : ℕ) : AELocallyUniformlyEllipticField (rescaleReg k a)

Locally a.e.-uniform ellipticity is preserved by triadic rescaling of the carrier coefficient field.

theorem HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticLaw.scaleNormalized {d : ℕ} {P : RestrictionCoeffLaw d} (hP : AELocallyUniformlyEllipticLaw P) (k : ℕ) : AELocallyUniformlyEllipticLaw (restrictionScaleNormalizedLaw k P)

A locally a.e.-uniformly elliptic law remains so after triadic scale-normalization.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.scaleNormalized {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (k : ℕ) : RestrictionLawCarrier (restrictionScaleNormalizedLaw k P)

The Chapter 4 law carrier is preserved by triadic scale-normalization.

theorem HCPolySupport.Book.Ch04.triadicCoeffFamily_rescaleCoeffField_aeeq_dilate {d : ℕ} {a : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) (k : ℕ) : (triadicCoeffFamilyOfAELocallyUniformlyEllipticField (rescaleReg k a) ⋯).AEEq (Ch02.TriadicCoeffFamily.dilate (-↑k) (triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha))

theorem HCPolySupport.Book.Ch04.LambdaSqCoeffField_rescaleCoeffField_of_aelocallyUniformlyElliptic {d : ℕ} {a : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) (k : ℕ) (Q : TriadicCube d) (s : ℝ) (q : Ch02.MultiscaleExponent) : LambdaSqCoeffField Q s q (rescaleReg k a) = LambdaSqCoeffField (Ch02.dilateCube (↑k) Q) s q a

theorem HCPolySupport.Book.Ch04.lambdaSqCoeffField_rescaleCoeffField_of_aelocallyUniformlyElliptic {d : ℕ} {a : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) (k : ℕ) (Q : TriadicCube d) (s : ℝ) (q : Ch02.MultiscaleExponent) : lambdaSqCoeffField Q s q (rescaleReg k a) = lambdaSqCoeffField (Ch02.dilateCube (↑k) Q) s q a

@[simp]

theorem HCPolySupport.Book.Ch04.dilateCube_originCube_nat {d : ℕ} (k m : ℕ) : Ch02.dilateCube (↑k) (originCube d ↑m) = originCube d ↑(k + m)

theorem HCPolySupport.Book.Ch04.LambdaSqCoeffField_originCube_rescaleCoeffField_of_aelocallyUniformlyElliptic {d : ℕ} {a : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) (k m : ℕ) (s : ℝ) (q : Ch02.MultiscaleExponent) : LambdaSqCoeffField (originCube d ↑m) s q (rescaleReg k a) = LambdaSqCoeffField (originCube d ↑(k + m)) s q a

theorem HCPolySupport.Book.Ch04.lambdaSqCoeffField_originCube_rescaleCoeffField_of_aelocallyUniformlyElliptic {d : ℕ} {a : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) (k m : ℕ) (s : ℝ) (q : Ch02.MultiscaleExponent) : lambdaSqCoeffField (originCube d ↑m) s q (rescaleReg k a) = lambdaSqCoeffField (originCube d ↑(k + m)) s q a

theorem HCPolySupport.Book.Ch04.coarseBlockMatrix_originCube_rescaleCoeffField_of_aelocallyUniformlyElliptic {d : ℕ} [NeZero d] {a : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) (k m : ℕ) : coarseBlockMatrix (cubeSet (originCube d ↑m)) (rescaleReg k a).toFun = coarseBlockMatrix (cubeSet (originCube d ↑(k + m))) a.toFun

The ambient coarse block matrix rescales by shifting the origin-cube scale.

theorem HCPolySupport.Book.Ch04.restrictionResponseJObservableCubeSet_originCube_rescaleCoeffField_of_aelocallyUniformlyElliptic {d : ℕ} [NeZero d] {a : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) (k m : ℕ) (p q : Vec d) : restrictionResponseJObservableCubeSet (originCube d ↑m) p q (rescaleReg k a) = restrictionResponseJObservableCubeSet (originCube d ↑(k + m)) p q a

Scalar response observables rescale by shifting the origin-cube scale.

theorem HCPolySupport.Book.Ch04.responseJObservableSet_cube_dilateCoeffField_neg_nat {d : ℕ} [NeZero d] {a : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) (k m : ℕ) (p q : Vec d) : restrictionResponseJObservableCubeSet (originCube d ↑m) p q (dilateReg (-↑k) a) = restrictionResponseJObservableCubeSet (originCube d ↑(k + m)) p q a

Scalar response observables under the dilation defining restrictionScaleNormalizedLaw.

theorem HCPolySupport.Book.Ch04.LambdaMomentAtScale_restrictionScaleNormalizedLaw {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (k m : ℕ) {s : ℝ} (hs : 0 < s) (ξ : ℕ) : LambdaMomentAtScale (restrictionScaleNormalizedLaw k P) (↑m) s ξ = LambdaMomentAtScale P (↑(k + m)) s ξ

Upper multiscale ellipticity moments shift under scale-normalization of the law.

theorem HCPolySupport.Book.Ch04.lambdaInvMomentAtScale_restrictionScaleNormalizedLaw {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (k m : ℕ) {s : ℝ} (hs : 0 < s) (ξ : ℕ) : lambdaInvMomentAtScale (restrictionScaleNormalizedLaw k P) (↑m) s ξ = lambdaInvMomentAtScale P (↑(k + m)) s ξ

Lower inverse multiscale ellipticity moments shift under scale-normalization of the law.

theorem HCPolySupport.Book.Ch04.widetildeThetaAtScale_restrictionScaleNormalizedLaw {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (k m : ℕ) {sUpper sLower : ℝ} (hsUpper : 0 < sUpper) (hsLower : 0 < sLower) (ξ : ℕ) : widetildeThetaAtScale (restrictionScaleNormalizedLaw k P) (↑m) sUpper sLower ξ = widetildeThetaAtScale P (↑(k + m)) sUpper sLower ξ

The enhanced ellipticity moment contrast shifts under scale-normalization of the law.

theorem HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale_restrictionScaleNormalizedLaw {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (k m : ℕ) : annealedBlockMatrixAtScale (restrictionScaleNormalizedLaw k P) ↑m = annealedBlockMatrixAtScale P ↑(k + m)

The annealed full coarse block matrix shifts under scale-normalization of the law.

theorem HCPolySupport.Book.Ch04.annealedBAtScale_restrictionScaleNormalizedLaw {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (k m : ℕ) : annealedBAtScale (restrictionScaleNormalizedLaw k P) ↑m = annealedBAtScale P ↑(k + m)

The annealed upper-left scalar block shifts under scale-normalization of the law.

theorem HCPolySupport.Book.Ch04.annealedSigmaStarInvAtScale_restrictionScaleNormalizedLaw {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (k m : ℕ) : annealedSigmaStarInvAtScale (restrictionScaleNormalizedLaw k P) ↑m = annealedSigmaStarInvAtScale P ↑(k + m)

The annealed inverse-star scalar block shifts under scale-normalization of the law.

theorem HCPolySupport.Book.Ch04.RestrictionStationaryLaw.scaleNormalized {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionStationaryLaw P) (k : ℕ) : RestrictionStationaryLaw (restrictionScaleNormalizedLaw k P)

Stationarity is preserved by triadic scale-normalization.

theorem HCPolySupport.Book.Ch04.RestrictionIsotropicLaw.scaleNormalized {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionIsotropicLaw P) (k : ℕ) : RestrictionIsotropicLaw (restrictionScaleNormalizedLaw k P)

Isotropy under signed permutations is preserved by triadic scale-normalization.

theorem HCPolySupport.Book.Ch04.RestrictionAdjointInvariantLaw.scaleNormalized {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionAdjointInvariantLaw P) (k : ℕ) : RestrictionAdjointInvariantLaw (restrictionScaleNormalizedLaw k P)

Adjoint invariance is preserved by triadic scale-normalization.

theorem HCPolySupport.Book.Ch04.RestrictionStructuralLaw.scaleNormalized {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionStructuralLaw P) (k : ℕ) : RestrictionStructuralLaw (restrictionScaleNormalizedLaw k P)

The full structural law package is preserved by triadic scale-normalization.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.barBAtScale_restrictionScaleNormalizedLaw {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (k m : ℕ) : ⋯.barBAtScale ⋯ ↑m = hP.barBAtScale hStruct ↑(k + m)

The primitive upper-left structural scalar shifts under scale-normalization.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.barSigmaStarInvAtScale_restrictionScaleNormalizedLaw {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (k m : ℕ) : ⋯.barSigmaStarInvAtScale ⋯ ↑m = hP.barSigmaStarInvAtScale hStruct ↑(k + m)

The primitive inverse-star structural scalar shifts under scale-normalization.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.barSigmaAtScale_restrictionScaleNormalizedLaw {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (k m : ℕ) : ⋯.barSigmaAtScale ⋯ ↑m = hP.barSigmaAtScale hStruct ↑(k + m)

The structural-law scalar \bar\sigma shifts under scale-normalization.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.barSigmaStarAtScale_restrictionScaleNormalizedLaw {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (k m : ℕ) : ⋯.barSigmaStarAtScale ⋯ ↑m = hP.barSigmaStarAtScale hStruct ↑(k + m)

The structural-law scalar \bar\sigma_* shifts under scale-normalization.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.thetaAtScale_restrictionScaleNormalizedLaw {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (k m : ℕ) : ⋯.thetaAtScale ⋯ ↑m = hP.thetaAtScale hStruct ↑(k + m)

The structural-law contrast \Theta shifts under scale-normalization.