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

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

The AKL a.e.-quotient coefficient-field kernel

The high-moment manuscript uses uniformly elliptic, measurable coefficient fields modulo equality almost everywhere. This module gives its fixed-Θ carrier and its integral-only local sigma-algebras.

@[reducible, inline]

abbrev HCPolySupport.Source.AKL.Field (d : ℕ) : Type

Almost-everywhere classes of almost-everywhere measurable matrix fields for Lebesgue measure.

Equations

• HCPolySupport.Source.AKL.Field d = (HCPolySupport.Vec d →ₘ[MeasureTheory.volume] HCPolySupport.Mat d)

def HCPolySupport.Source.AKL.Carrier (d : ℕ) (Θ : ℝ) : Type

Matrix field classes satisfying ellipticity bounds one and Θ almost everywhere.

Equations

• HCPolySupport.Source.AKL.Carrier d Θ = { a : HCPolySupport.Source.AKL.Field d // ∀ᵐ (x : HCPolySupport.Vec d), HCPolySupport.IsEllipticMatrix 1 Θ (↑a x) }

@[reducible, inline]

abbrev HCPolySupport.Source.AKL.BorelRegion (d : ℕ) : Type

Measurable subsets of the ambient coordinate space.

Equations

• HCPolySupport.Source.AKL.BorelRegion d = { U : Set (HCPolySupport.Vec d) // MeasurableSet U }

def HCPolySupport.Source.AKL.IsEllipticEntry {d : ℕ} (Θ : ℝ) (A : Mat d) : Prop

The bounds |ξ|² ≤ ξ·Aξ and |Aη|² ≤ Θ * η·Aη for every pair of vectors.

Equations

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

@[instance_reducible]

instance HCPolySupport.Source.AKL.instMeasurableSpaceMat {d : ℕ} : MeasurableSpace (Mat d)

Equations

• HCPolySupport.Source.AKL.instMeasurableSpaceMat = HCPolySupport.Source.AKL.instMeasurableSpaceMat._aux_1

instance HCPolySupport.Source.AKL.instBorelSpaceMat {d : ℕ} : BorelSpace (Mat d)

instance HCPolySupport.Source.AKL.instPseudoMetrizableSpaceMat {d : ℕ} : TopologicalSpace.PseudoMetrizableSpace (Mat d)

theorem HCPolySupport.Source.AKL.field_ae_elliptic_iff_exists_pointwise_representative {d : ℕ} {Θ : ℝ} (hΘ : 1 ≤ Θ) (a : Field d) : (∀ᵐ (x : Vec d), IsEllipticMatrix 1 Θ (↑a x)) ↔ ∃ (f : Vec d → Mat d), Measurable f ∧ (∀ (x : Vec d), IsEllipticMatrix 1 Θ (f x)) ∧ ↑a =ᵐ[MeasureTheory.volume] f

theorem HCPolySupport.Source.AKL.carrier_exists_pointwise_elliptic_measurable_representative {d : ℕ} {Θ : ℝ} (hΘ : 1 ≤ Θ) (a : Carrier d Θ) : ∃ (f : Vec d → Mat d), Measurable f ∧ (∀ (x : Vec d), IsEllipticMatrix 1 Θ (f x)) ∧ ↑↑a =ᵐ[MeasureTheory.volume] f

noncomputable def HCPolySupport.Source.AKL.rawGenerator {d : ℕ} (U : BorelRegion d) (e e' : Vec d) (φ : Vec d → ℝ) (a : Vec d → Mat d) : ℝ

The integral over U of the matrix pairing e'·a e against the scalar probe φ.

Equations

• HCPolySupport.Source.AKL.rawGenerator U e e' φ a = ∫ (x : HCPolySupport.Vec d) in ↑U, HCPolySupport.vecDot e' (HCPolySupport.matVecMul (a x) e) * φ x

noncomputable def HCPolySupport.Source.AKL.generator {d : ℕ} {Θ : ℝ} (U : BorelRegion d) (e e' : Vec d) (φ : Vec d → ℝ) (a : Carrier d Θ) : ℝ

The integral coefficient pairing on U evaluated on an elliptic field class.

Equations

• HCPolySupport.Source.AKL.generator U e e' φ a = HCPolySupport.Source.AKL.rawGenerator U e e' φ ↑↑a

theorem HCPolySupport.Source.AKL.generator_mk_eq_raw {d : ℕ} {Θ : ℝ} (U : BorelRegion d) (e e' : Vec d) (φ : Vec d → ℝ) (f : Vec d → Mat d) (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (hEll : ∀ᵐ (x : Vec d), IsEllipticMatrix 1 Θ (↑(MeasureTheory.AEEqFun.mk f hf) x)) : generator U e e' φ ⟨MeasureTheory.AEEqFun.mk f hf, hEll⟩ = rawGenerator U e e' φ f

@[reducible, inline]

abbrev HCPolySupport.Source.AKL.localSigma {d : ℕ} {Θ : ℝ} (U : BorelRegion d) : MeasurableSpace (Carrier d Θ)

The sigma-algebra generated by coefficient-pairing integrals over U against all smooth compactly supported scalar probes.

Equations

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

@[reducible, inline]

abbrev HCPolySupport.Source.AKL.globalSigma (d : ℕ) (Θ : ℝ) : MeasurableSpace (Carrier d Θ)

The integral-generated sigma-algebra with the region equal to the whole space.

Equations

• HCPolySupport.Source.AKL.globalSigma d Θ = HCPolySupport.Source.AKL.localSigma ⟨Set.univ, ⋯⟩

@[reducible, inline]

abbrev HCPolySupport.Source.AKL.Law (d : ℕ) (Θ : ℝ) : Type

Measures on the elliptic field carrier with its global integral-generated sigma-algebra.

Equations

• HCPolySupport.Source.AKL.Law d Θ = MeasureTheory.Measure (HCPolySupport.Source.AKL.Carrier d Θ)

def HCPolySupport.Source.AKL.IsSourceLocal {d : ℕ} {Θ : ℝ} {E : Type u_1} [MeasurableSpace E] (U : BorelRegion d) (X : Carrier d Θ → E) : Prop

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

Equations

• HCPolySupport.Source.AKL.IsSourceLocal U X = Measurable X

noncomputable def HCPolySupport.Source.AKL.density {Θ : ℝ} {d : ℕ} (e e' : Vec d) (a : Carrier d Θ) : Vec d → ℝ

The pointwise scalar coefficient pairing e'·a e of a field representative.

Equations

• HCPolySupport.Source.AKL.density e e' a x = HCPolySupport.vecDot e' (HCPolySupport.matVecMul (↑↑a x) e)

def HCPolySupport.Source.AKL.densityBound {d : ℕ} (Θ : ℝ) (e e' : Vec d) : ℝ

The sum ∑ i j, |e' i| * max Θ 0 * |e j|, used to bound the coefficient pairing.

Equations

• HCPolySupport.Source.AKL.densityBound Θ e e' = ∑ i : Fin d, ∑ j : Fin d, |e' i| * max Θ 0 * |e j|

theorem HCPolySupport.Source.AKL.localSigma_mono {d : ℕ} {Θ : ℝ} {U V : BorelRegion d} (hUV : ↑U ⊆ ↑V) : localSigma U ≤ localSigma V

def HCPolySupport.Source.AKL.intTranslation {d : ℕ} (z : Fin d → ℤ) : Vec d

The real coordinate vector obtained from an integer lattice vector.

Equations

• HCPolySupport.Source.AKL.intTranslation z i = ↑(z i)

noncomputable def HCPolySupport.Source.AKL.translateField {d : ℕ} (z : Fin d → ℤ) (a : Field d) : Field d

Translation of an almost-everywhere matrix field class by an integer lattice vector.

Equations

• HCPolySupport.Source.AKL.translateField z a = MeasureTheory.AEEqFun.compMeasurePreserving a (fun (x : HCPolySupport.Vec d) => x + HCPolySupport.Source.AKL.intTranslation z) ⋯

theorem HCPolySupport.Source.AKL.translateField_ae {d : ℕ} (z : Fin d → ℤ) (a : Field d) : ↑(translateField z a) =ᵐ[MeasureTheory.volume] fun (x : Vec d) => ↑a (x + intTranslation z)

noncomputable def HCPolySupport.Source.AKL.translate {d : ℕ} {Θ : ℝ} (z : Fin d → ℤ) : Carrier d Θ → Carrier d Θ

Translation of an elliptic field class by an integer lattice vector.

Equations

• HCPolySupport.Source.AKL.translate z a = ⟨HCPolySupport.Source.AKL.translateField z ↑a, ⋯⟩

theorem HCPolySupport.Source.AKL.measurable_translate_global {d : ℕ} {Θ : ℝ} (z : Fin d → ℤ) : Measurable (translate z)

def HCPolySupport.Source.AKL.supDist {d : ℕ} (x y : Vec d) : ℝ

The supremum-norm distance ‖x - y‖ between coordinate vectors.

Equations

• HCPolySupport.Source.AKL.supDist x y = ‖x - y‖