Coarse-graining support: Support.Probability.Source.Coarse

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

def HCPolySupport.Source.Coarse.euclideanBall {d : ℕ} (R : ℝ) : Set (Vec d)

The open Euclidean ball centered at zero with radius R.

Equations

• HCPolySupport.Source.Coarse.euclideanBall R = {x : HCPolySupport.Vec d | HCPolySupport.euclideanNorm x < R}

structure HCPolySupport.Source.Coarse.SmoothCompactProbe {d : ℕ} (φ : Vec d → ℝ) : Prop

Smoothness of all orders together with compact support of a scalar probe.

• smooth : ContDiff ℝ (↑⊤) φ
• compact : HasCompactSupport φ

def HCPolySupport.Source.Coarse.Carrier (d : ℕ) : Type

Measurable coefficient fields with pointwise uniform ellipticity on every Euclidean ball of radius at least one, with bounds allowed to depend on the ball.

Equations

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

@[instance_reducible]

instance HCPolySupport.Source.Coarse.instCoeFunCarrier (d : ℕ) : CoeFun (Carrier d) fun (x : Carrier d) => CoeffField d

Equations

• HCPolySupport.Source.Coarse.instCoeFunCarrier d = { coe := fun (a : HCPolySupport.Source.Coarse.Carrier d) => ↑a }

noncomputable def HCPolySupport.Source.Coarse.bilinearTest {d : ℕ} (e e' : Vec d) (φ : Vec d → ℝ) (a : Carrier d) : ℝ

The Lebesgue integral of the coefficient pairing e'·a e against a scalar probe.

Equations

• HCPolySupport.Source.Coarse.bilinearTest e e' φ a = ∫ (x : HCPolySupport.Vec d), HCPolySupport.vecDot e' (HCPolySupport.matVecMul (↑a x) e) * φ x

@[reducible, inline]

abbrev HCPolySupport.Source.Coarse.localSigma {d : ℕ} (U : Set (Vec d)) (_hU : MeasurableSet U) : MeasurableSpace (Carrier d)

The sigma-algebra generated by coefficient-pairing integrals against smooth compact probes whose topological support is contained in U.

Equations

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

@[reducible, inline]

abbrev HCPolySupport.Source.Coarse.globalSigma (d : ℕ) : MeasurableSpace (Carrier d)

The integral-generated sigma-algebra using probes supported in the whole space.

Equations

• HCPolySupport.Source.Coarse.globalSigma d = HCPolySupport.Source.Coarse.localSigma Set.univ ⋯

@[instance_reducible]

instance HCPolySupport.Source.Coarse.instMeasurableSpaceCarrier (d : ℕ) : MeasurableSpace (Carrier d)

Equations

• HCPolySupport.Source.Coarse.instMeasurableSpaceCarrier d = HCPolySupport.Source.Coarse.globalSigma d

def HCPolySupport.Source.Coarse.IsLocalObservable {d : ℕ} (U : Set (Vec d)) (hU : MeasurableSet U) {β : Type u_1} [MeasurableSpace β] (X : Carrier d → β) : Prop

Measurability of an observable for the probe-generated local sigma-algebra on U.

Equations

• HCPolySupport.Source.Coarse.IsLocalObservable U hU X = Measurable X

theorem HCPolySupport.Source.Coarse.euclideanNorm_add_le {d : ℕ} (x y : Vec d) : euclideanNorm (x + y) ≤ euclideanNorm x + euclideanNorm y

theorem HCPolySupport.Source.Coarse.euclideanNorm_matVecMul_signedPermutation {d : ℕ} {R : Mat d} (hR : IsSignedPermutationMatrix R) (x : Vec d) : euclideanNorm (matVecMul R x) = euclideanNorm x

theorem HCPolySupport.Source.Coarse.isEllipticMatrix_rotate {d : ℕ} {lam Lam : ℝ} {R A : Mat d} (hR : IsSignedPermutationMatrix R) (hA : IsEllipticMatrix lam Lam A) : IsEllipticMatrix lam Lam (matTranspose R * A * R)

def HCPolySupport.Source.Coarse.Carrier.translate {d : ℕ} (z : Fin d → ℤ) (a : Carrier d) : Carrier d

Translate a locally elliptic measurable coefficient field by an integer lattice vector.

Equations

• HCPolySupport.Source.Coarse.Carrier.translate z a = ⟨fun (x : HCPolySupport.Vec d) => ↑a (x + HCPolySupport.intVecToRealVec z), ⋯⟩

@[simp]

theorem HCPolySupport.Source.Coarse.Carrier.translate_apply {d : ℕ} (z : Fin d → ℤ) (a : Carrier d) (x : Vec d) : ↑(translate z a) x = ↑a (x + intVecToRealVec z)

def HCPolySupport.Source.Coarse.Carrier.adjoint {d : ℕ} (a : Carrier d) : Carrier d

Transpose every matrix of a locally elliptic measurable coefficient field.

Equations

• a.adjoint = ⟨fun (x : HCPolySupport.Vec d) => HCPolySupport.matTranspose (↑a x), ⋯⟩

@[simp]

theorem HCPolySupport.Source.Coarse.Carrier.adjoint_apply {d : ℕ} (a : Carrier d) (x : Vec d) : ↑a.adjoint x = matTranspose (↑a x)

def HCPolySupport.Source.Coarse.Carrier.rotate {d : ℕ} (R : Mat d) (hR : IsSignedPermutationMatrix R) (a : Carrier d) : Carrier d

Transform the field by x ↦ Rᵀ * a (R x) * R for a signed permutation matrix.

Equations

• HCPolySupport.Source.Coarse.Carrier.rotate R hR a = ⟨fun (x : HCPolySupport.Vec d) => HCPolySupport.matTranspose R * ↑a (HCPolySupport.matVecMul R x) * R, ⋯⟩

@[simp]

theorem HCPolySupport.Source.Coarse.Carrier.rotate_apply {d : ℕ} (R : Mat d) (hR : IsSignedPermutationMatrix R) (a : Carrier d) (x : Vec d) : ↑(rotate R hR a) x = matTranspose R * ↑a (matVecMul R x) * R

theorem HCPolySupport.Source.Coarse.localSigma_mono {d : ℕ} {U V : Set (Vec d)} (hU : MeasurableSet U) (hV : MeasurableSet V) (hUV : U ⊆ V) : localSigma U hU ≤ localSigma V hV

theorem HCPolySupport.Source.Coarse.measurable_translate_localSigma {d : ℕ} (z : Fin d → ℤ) {U : Set (Vec d)} (hU : MeasurableSet U) : Measurable (Carrier.translate z)

Translating coefficients by z pulls observables local to U back to observables local to U + z.

theorem HCPolySupport.Source.Coarse.IsLocalObservable.comp_translate {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) {β : Type u_1} [MeasurableSpace β] {X : Carrier d → β} (hX : IsLocalObservable U hU X) (z : Fin d → ℤ) : IsLocalObservable (translateSet (intVecToRealVec z) U) ⋯ (X ∘ Carrier.translate z)

A local observable remains local after precomposing with a coefficient translation, with its region translated by the same vector.

theorem HCPolySupport.Source.Coarse.measurable_translate_globalSigma {d : ℕ} (z : Fin d → ℤ) : Measurable (Carrier.translate z)

theorem HCPolySupport.Source.Coarse.measurable_adjoint_globalSigma {d : ℕ} : Measurable Carrier.adjoint

theorem HCPolySupport.Source.Coarse.measurable_rotate_globalSigma {d : ℕ} (R : Mat d) (hR : IsSignedPermutationMatrix R) : Measurable (Carrier.rotate R hR)