Coarse-graining support: Support.Probability.RandomCoeffField

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

Actual random coefficient fields over a sample space.

The probability layer in the rest of the project is law-centric: the main objects are measures on CoeffField d. This file adds the lightweight bundled object RandomCoeffField Ω d so we can also speak cleanly about measurable sample-space-valued coefficient fields and the local sigma-algebras they induce on Ω.

structure HCPolySupport.RandomCoeffField (Ω : Type u_1) [MeasurableSpace Ω] (d : ℕ) : Type u_1

A coefficient field valued random object on a sample space Ω.

• toFun : Ω → CoeffField d

  The sample-space realization of the coefficient field.

• measurable_toFun : Measurable self.toFun

  Measurability into the ambient product sigma-algebra on CoeffField d.

@[instance_reducible]

instance HCPolySupport.RandomCoeffField.instCoeFunForallCoeffField {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} : CoeFun (RandomCoeffField Ω d) fun (x : RandomCoeffField Ω d) => Ω → CoeffField d

Equations

• HCPolySupport.RandomCoeffField.instCoeFunForallCoeffField = { coe := HCPolySupport.RandomCoeffField.toFun }

theorem HCPolySupport.RandomCoeffField.measurable {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) : Measurable A.toFun

theorem HCPolySupport.RandomCoeffField.ext {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} {A B : RandomCoeffField Ω d} (h : ∀ (ω : Ω), A.toFun ω = B.toFun ω) : A = B

theorem HCPolySupport.RandomCoeffField.ext_iff {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} {A B : RandomCoeffField Ω d} : A = B ↔ ∀ (ω : Ω), A.toFun ω = B.toFun ω

noncomputable def HCPolySupport.RandomCoeffField.law {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) (μ : MeasureTheory.Measure Ω) : MeasureTheory.Measure (CoeffField d)

The law of a random coefficient field under a base measure μ.

Equations

• A.law μ = MeasureTheory.Measure.map A.toFun μ

theorem HCPolySupport.RandomCoeffField.map_law_eq {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} {A : RandomCoeffField Ω d} (μ : MeasureTheory.Measure Ω) {β : Type u_2} [MeasurableSpace β] (f : CoeffField d → β) (hf : Measurable f) : MeasureTheory.Measure.map f (A.law μ) = MeasureTheory.Measure.map (fun (ω : Ω) => f (A.toFun ω)) μ

def HCPolySupport.RandomCoeffField.map {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) (f : CoeffField d → CoeffField d) (hf : Measurable f) : RandomCoeffField Ω d

Apply a measurable coefficient-field transform pointwise to a random coefficient field.

Equations

• A.map f hf = { toFun := fun (ω : Ω) => f (A.toFun ω), measurable_toFun := ⋯ }

def HCPolySupport.RandomCoeffField.translateByInt {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) (z : Fin d → ℤ) : RandomCoeffField Ω d

Integer-translate a random coefficient field.

Equations

• A.translateByInt z = A.map (HCPolySupport.translateByInt z) ⋯

def HCPolySupport.RandomCoeffField.rotate {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) (R : Mat d) (hR : IsSignedPermutationMatrix R) : RandomCoeffField Ω d

Rotate a random coefficient field by a signed permutation matrix.

Equations

• A.rotate R hR = A.map (HCPolySupport.rotateCoeffField R) ⋯

def HCPolySupport.RandomCoeffField.adjoint {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) : RandomCoeffField Ω d

Take the adjoint random coefficient field.

Equations

• A.adjoint = A.map HCPolySupport.adjointCoeffField ⋯

noncomputable def HCPolySupport.RandomCoeffField.restrictSet {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) (U : Set (Vec d)) : RandomCoeffField Ω d

Restrict a random coefficient field to a deterministic domain.

Equations

• A.restrictSet U = A.map (HCPolySupport.restrictCoeffField U) ⋯

noncomputable def HCPolySupport.RandomCoeffField.symmPart {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) : RandomCoeffField Ω d

Take the symmetric part of a random coefficient field.

Equations

• A.symmPart = A.map HCPolySupport.symmCoeffField ⋯

noncomputable def HCPolySupport.RandomCoeffField.skewPart {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) : RandomCoeffField Ω d

Take the skew part of a random coefficient field.

Equations

• A.skewPart = A.map HCPolySupport.skewCoeffField ⋯

theorem HCPolySupport.RandomCoeffField.law_map {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) (μ : MeasureTheory.Measure Ω) (f : CoeffField d → CoeffField d) (hf : Measurable f) : (A.map f hf).law μ = MeasureTheory.Measure.map f (A.law μ)

theorem HCPolySupport.RandomCoeffField.law_restrictSet {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) (μ : MeasureTheory.Measure Ω) (U : Set (Vec d)) : (A.restrictSet U).law μ = MeasureTheory.Measure.map (restrictCoeffField U) (A.law μ)

theorem HCPolySupport.RandomCoeffField.law_translateByInt {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) (μ : MeasureTheory.Measure Ω) (z : Fin d → ℤ) : (A.translateByInt z).law μ = MeasureTheory.Measure.map (HCPolySupport.translateByInt z) (A.law μ)

theorem HCPolySupport.RandomCoeffField.law_rotate {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) (μ : MeasureTheory.Measure Ω) (R : Mat d) (hR : IsSignedPermutationMatrix R) : (A.rotate R hR).law μ = MeasureTheory.Measure.map (rotateCoeffField R) (A.law μ)

theorem HCPolySupport.RandomCoeffField.law_adjoint {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) (μ : MeasureTheory.Measure Ω) : A.adjoint.law μ = MeasureTheory.Measure.map adjointCoeffField (A.law μ)

theorem HCPolySupport.RandomCoeffField.law_symmPart {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) (μ : MeasureTheory.Measure Ω) : A.symmPart.law μ = MeasureTheory.Measure.map symmCoeffField (A.law μ)

theorem HCPolySupport.RandomCoeffField.law_skewPart {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) (μ : MeasureTheory.Measure Ω) : A.skewPart.law μ = MeasureTheory.Measure.map skewCoeffField (A.law μ)

@[reducible, inline]

abbrev HCPolySupport.RandomCoeffField.pointwiseLocalSigma {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) (U : Set (Vec d)) : MeasurableSpace Ω

The pointwise-local sigma-algebra on the sample space induced by a random coefficient field and the deterministic region U. This belongs to the retained restriction engineering lane.

Equations

• A.pointwiseLocalSigma U = MeasurableSpace.comap A.toFun (HCPolySupport.PointwiseLocalSigma U)

@[reducible, inline]

abbrev HCPolySupport.RandomCoeffField.localSigma {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) (U : Set (Vec d)) : MeasurableSpace Ω

Compatibility name for pointwiseLocalSigma.

Equations

• A.localSigma U = A.pointwiseLocalSigma U

@[reducible, inline]

noncomputable abbrev HCPolySupport.RandomCoeffField.restrictionSigma {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) (U : Set (Vec d)) : MeasurableSpace Ω

The restriction sigma-algebra on the sample space induced by a random coefficient field and the deterministic region U. This is the pullback of RestrictionSigma U, hence the sigma-algebra naturally matched to pointwise local observables.

Equations

• A.restrictionSigma U = MeasurableSpace.comap A.toFun (HCPolySupport.RestrictionSigma U)

theorem HCPolySupport.RandomCoeffField.measurable_pointwiseLocalSigma {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) (U : Set (Vec d)) : Measurable A.toFun

theorem HCPolySupport.RandomCoeffField.measurable_localSigma {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) (U : Set (Vec d)) : Measurable A.toFun

Compatibility spelling for measurable_pointwiseLocalSigma.

theorem HCPolySupport.RandomCoeffField.measurable_restrictionSigma {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) (U : Set (Vec d)) : Measurable A.toFun

theorem HCPolySupport.RandomCoeffField.measurable_localTestObservable_pointwiseLocalSigma {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) (U : Set (Vec d)) (e e' : Vec d) {φ : Vec d → ℝ} (hφ_cont : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_support : tsupport φ ⊆ U) : Measurable fun (ω : Ω) => localTestObservable e e' φ (A.toFun ω)

theorem HCPolySupport.RandomCoeffField.measurable_localTestObservable {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) (U : Set (Vec d)) (e e' : Vec d) {φ : Vec d → ℝ} (hφ_cont : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_support : tsupport φ ⊆ U) : Measurable fun (ω : Ω) => localTestObservable e e' φ (A.toFun ω)

Compatibility spelling for the pointwise-local test-observable theorem.