Coarse-graining support: Support.Probability.RescaledLaw

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

Triadically rescaled coefficient laws and random scale parameters.

The Chapter 4 probability layer is mostly law-centric: coefficient fields are sampled from a measure on CoeffField d. This module adds the basic transport API for passing from a law to its triadically rescaled law and records the lightweight random-scale package used by later quenched-scale arguments.

noncomputable def HCPolySupport.triadicDilateVec {d : ℕ} (n : ℕ) (x : Vec d) : Vec d

Dilate a vector by the triadic factor 3^n.

Equations

• HCPolySupport.triadicDilateVec n x i = 3 ^ n * x i

noncomputable def HCPolySupport.triadicDilateSet {d : ℕ} (n : ℕ) (U : Set (Vec d)) : Set (Vec d)

The image of a set under triadic dilation by 3^n.

Equations

• HCPolySupport.triadicDilateSet n U = {x : HCPolySupport.Vec d | ∃ y ∈ U, x = HCPolySupport.triadicDilateVec n y}

def HCPolySupport.triadicScaleIntShift {d : ℕ} (n : ℕ) (z : Fin d → ℤ) : Fin d → ℤ

The integer shift in the original variables corresponding to an integer shift after triadic rescaling.

Equations

• HCPolySupport.triadicScaleIntShift n z i = ↑(3 ^ n) * z i

noncomputable def HCPolySupport.rescaleCoeffField {d : ℕ} (n : ℕ) (a : CoeffField d) : CoeffField d

Rescale a coefficient field by the triadic factor 3^n.

The rescaled field is x ↦ a(3^n x). Thus integer translations of the rescaled field correspond to translations of the original field by integer vectors multiplied by 3^n.

Equations

• HCPolySupport.rescaleCoeffField n a x = a (HCPolySupport.triadicDilateVec n x)

@[simp]

theorem HCPolySupport.triadicDilateVec_zero {d : ℕ} (x : Vec d) : triadicDilateVec 0 x = x

@[simp]

theorem HCPolySupport.triadicDilateVec_mem_triadicDilateSet {d : ℕ} (n : ℕ) {U : Set (Vec d)} {x : Vec d} (hx : x ∈ U) : triadicDilateVec n x ∈ triadicDilateSet n U

theorem HCPolySupport.isBounded_triadicDilateSet {d : ℕ} (n : ℕ) {U : Set (Vec d)} (hU : Bornology.IsBounded U) : Bornology.IsBounded (triadicDilateSet n U)

Triadic dilation sends bounded subsets of the ambient space to bounded subsets.

@[simp]

theorem HCPolySupport.rescaleCoeffField_zero {d : ℕ} (a : CoeffField d) : rescaleCoeffField 0 a = a

theorem HCPolySupport.rescaleCoeffField_add {d : ℕ} (m n : ℕ) (a : CoeffField d) : rescaleCoeffField (m + n) a = rescaleCoeffField n (rescaleCoeffField m a)

theorem HCPolySupport.localTestObservable_rescaleCoeffField_eq_const_mul {d : ℕ} (k : ℕ) (e e' : Vec d) (φ : Vec d → ℝ) (a : CoeffField d) : localTestObservable e e' φ (rescaleCoeffField k a) = ((3 ^ k) ^ d)⁻¹ * localTestObservable e e' (fun (y : Vec d) => φ ((3 ^ k)⁻¹ • y)) a

theorem HCPolySupport.localFiniteTestObservable_rescaleCoeffField_eq {d : ℕ} {ι : Type} (n : ℕ) (I : Finset ι) (e e' : ι → Vec d) (φ : ι → Vec d → ℝ) (a : CoeffField d) : localFiniteTestObservable I e e' φ (rescaleCoeffField n a) = localFiniteTestObservable I e e' (fun (k : ι) (y : Vec d) => ((3 ^ n) ^ d)⁻¹ * φ k ((3 ^ n)⁻¹ • y)) a

theorem HCPolySupport.measurable_rescaleCoeffField {d : ℕ} (n : ℕ) : Measurable (rescaleCoeffField n)

theorem HCPolySupport.translateByInt_rescaleCoeffField_eq_rescaleCoeffField_translateByInt {d : ℕ} (n : ℕ) (z : Fin d → ℤ) (a : CoeffField d) : translateByInt z (rescaleCoeffField n a) = rescaleCoeffField n (translateByInt (triadicScaleIntShift n z) a)