Coarse-graining support: Support.Book.Ch04.SourceObservable

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

Exact coarse-source local observables

Locality in this file is measurability for the coarse source's integral-only sigma algebra. It is intentionally separate from restriction locality.

@[instance_reducible]

instance HCPolySupport.Book.Ch04.instMeasurableSpaceMat (d : ℕ) : MeasurableSpace (Mat d)

Equations

• HCPolySupport.Book.Ch04.instMeasurableSpaceMat d = HCPolySupport.Book.Ch04.instMeasurableSpaceMat._aux_1 d

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

A random variable local for the exact coarse source sigma algebra.

Equations

• HCPolySupport.Book.Ch04.IsSourceLocalRandomVariable U hU X = HCPolySupport.Source.Coarse.IsLocalObservable U hU X

theorem HCPolySupport.Book.Ch04.IsSourceLocalRandomVariable.mono {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U V : Set (Vec d)} {X : Source.Coarse.Carrier d → β} (hU : MeasurableSet U) (hV : MeasurableSet V) (hUV : U ⊆ V) (hX : IsSourceLocalRandomVariable U hU X) : IsSourceLocalRandomVariable V hV X

Enlarge the observation set of a source-local random variable.

theorem HCPolySupport.Book.Ch04.IsSourceLocalRandomVariable.const {β : Type u_1} [MeasurableSpace β] {d : ℕ} (U : Set (Vec d)) (hU : MeasurableSet U) (b : β) : IsSourceLocalRandomVariable U hU fun (_a : Source.Coarse.Carrier d) => b

Constant source-local random variables.

theorem HCPolySupport.Book.Ch04.IsSourceLocalRandomVariable.comp_measurable {β : Type u_1} {γ : Type u_2} [MeasurableSpace β] [MeasurableSpace γ] {d : ℕ} {U : Set (Vec d)} {hU : MeasurableSet U} {X : Source.Coarse.Carrier d → β} (hX : IsSourceLocalRandomVariable U hU X) {g : β → γ} (hg : Measurable g) : IsSourceLocalRandomVariable U hU fun (a : Source.Coarse.Carrier d) => g (X a)

Measurable postcomposition preserves source locality.

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

Precomposing a source-local random variable with coefficient translation translates its observation region by the same integer vector.

theorem HCPolySupport.Book.Ch04.IsSourceLocalRandomVariable.vec_of_components {d m : ℕ} {U : Set (Vec d)} {hU : MeasurableSet U} {X : Source.Coarse.Carrier d → Vec m} (hX : ∀ (i : Fin m), IsSourceLocalRandomVariable U hU fun (a : Source.Coarse.Carrier d) => X a i) : IsSourceLocalRandomVariable U hU X

Source locality of a vector-valued random variable follows componentwise.

theorem HCPolySupport.Book.Ch04.IsSourceLocalRandomVariable.vec_component {d m : ℕ} {U : Set (Vec d)} {hU : MeasurableSet U} {X : Source.Coarse.Carrier d → Vec m} (hX : IsSourceLocalRandomVariable U hU X) (i : Fin m) : IsSourceLocalRandomVariable U hU fun (a : Source.Coarse.Carrier d) => X a i

Components of a source-local vector-valued random variable are source-local.

theorem HCPolySupport.Book.Ch04.IsSourceLocalRandomVariable.mat_of_entries {d m : ℕ} {U : Set (Vec d)} {hU : MeasurableSet U} {X : Source.Coarse.Carrier d → Mat m} (hX : ∀ (i j : Fin m), IsSourceLocalRandomVariable U hU fun (a : Source.Coarse.Carrier d) => X a i j) : IsSourceLocalRandomVariable U hU X

Source locality of a matrix-valued random variable follows entrywise.

theorem HCPolySupport.Book.Ch04.IsSourceLocalRandomVariable.mat_entry {d m : ℕ} {U : Set (Vec d)} {hU : MeasurableSet U} {X : Source.Coarse.Carrier d → Mat m} (hX : IsSourceLocalRandomVariable U hU X) (i j : Fin m) : IsSourceLocalRandomVariable U hU fun (a : Source.Coarse.Carrier d) => X a i j

Entries of a source-local matrix-valued random variable are source-local.

theorem HCPolySupport.Book.Ch04.IsSourceLocalRandomVariable.add {d : ℕ} {U : Set (Vec d)} {hU : MeasurableSet U} {X Y : Source.Coarse.Carrier d → ℝ} (hX : IsSourceLocalRandomVariable U hU X) (hY : IsSourceLocalRandomVariable U hU Y) : IsSourceLocalRandomVariable U hU fun (a : Source.Coarse.Carrier d) => X a + Y a

Sum of source-local real random variables.

theorem HCPolySupport.Book.Ch04.IsSourceLocalRandomVariable.neg {d : ℕ} {U : Set (Vec d)} {hU : MeasurableSet U} {X : Source.Coarse.Carrier d → ℝ} (hX : IsSourceLocalRandomVariable U hU X) : IsSourceLocalRandomVariable U hU fun (a : Source.Coarse.Carrier d) => -X a

Negation of a source-local real random variable.

theorem HCPolySupport.Book.Ch04.IsSourceLocalRandomVariable.sub {d : ℕ} {U : Set (Vec d)} {hU : MeasurableSet U} {X Y : Source.Coarse.Carrier d → ℝ} (hX : IsSourceLocalRandomVariable U hU X) (hY : IsSourceLocalRandomVariable U hU Y) : IsSourceLocalRandomVariable U hU fun (a : Source.Coarse.Carrier d) => X a - Y a

Difference of source-local real random variables.

theorem HCPolySupport.Book.Ch04.IsSourceLocalRandomVariable.mul {d : ℕ} {U : Set (Vec d)} {hU : MeasurableSet U} {X Y : Source.Coarse.Carrier d → ℝ} (hX : IsSourceLocalRandomVariable U hU X) (hY : IsSourceLocalRandomVariable U hU Y) : IsSourceLocalRandomVariable U hU fun (a : Source.Coarse.Carrier d) => X a * Y a

Product of source-local real random variables.

theorem HCPolySupport.Book.Ch04.IsSourceLocalRandomVariable.inv {d : ℕ} {U : Set (Vec d)} {hU : MeasurableSet U} {X : Source.Coarse.Carrier d → ℝ} (hX : IsSourceLocalRandomVariable U hU X) : IsSourceLocalRandomVariable U hU fun (a : Source.Coarse.Carrier d) => (X a)⁻¹

Inverse of a source-local real random variable.

theorem HCPolySupport.Book.Ch04.IsSourceLocalRandomVariable.abs {d : ℕ} {U : Set (Vec d)} {hU : MeasurableSet U} {X : Source.Coarse.Carrier d → ℝ} (hX : IsSourceLocalRandomVariable U hU X) : IsSourceLocalRandomVariable U hU fun (a : Source.Coarse.Carrier d) => |X a|

Absolute value of a source-local real random variable.

theorem HCPolySupport.Book.Ch04.IsSourceLocalRandomVariable.finset_sum {d : ℕ} {ι : Type u_1} [Fintype ι] {U : Set (Vec d)} {hU : MeasurableSet U} {X : ι → Source.Coarse.Carrier d → ℝ} (hX : ∀ (i : ι), IsSourceLocalRandomVariable U hU (X i)) : IsSourceLocalRandomVariable U hU fun (a : Source.Coarse.Carrier d) => ∑ i : ι, X i a

Finite sums of source-local real random variables are source-local.

structure HCPolySupport.Book.Ch04.SourceObservable (d : ℕ) (U : Set (Vec d)) (β : Type u_1) [MeasurableSpace β] : Type u_1

A bundled observable local for the exact coarse source sigma algebra.

• measurableSet : MeasurableSet U
• toFun : Source.Coarse.Carrier d → β

  The observable on the coarse source carrier whose measurability is local to U.

• isLocal : IsSourceLocalRandomVariable U ⋯ self.toFun

@[instance_reducible]

instance HCPolySupport.Book.Ch04.SourceObservable.instCoeFunForallCarrier {d : ℕ} {U : Set (Vec d)} {β : Type u_1} [MeasurableSpace β] : CoeFun (SourceObservable d U β) fun (x : SourceObservable d U β) => Source.Coarse.Carrier d → β

Equations

• HCPolySupport.Book.Ch04.SourceObservable.instCoeFunForallCarrier = { coe := HCPolySupport.Book.Ch04.SourceObservable.toFun }

def HCPolySupport.Book.Ch04.SourceObservable.mono {d : ℕ} {U V : Set (Vec d)} {β : Type u_1} [MeasurableSpace β] (X : SourceObservable d U β) (hV : MeasurableSet V) (hUV : U ⊆ V) : SourceObservable d V β

Enlarge the observation set of a bundled source observable.

Equations

• X.mono hV hUV = { measurableSet := hV, toFun := X.toFun, isLocal := ⋯ }

def HCPolySupport.Book.Ch04.SourceObservable.const {d : ℕ} {β : Type u_1} [MeasurableSpace β] (U : Set (Vec d)) (hU : MeasurableSet U) (b : β) : SourceObservable d U β

Constant bundled source observables.

Equations

• HCPolySupport.Book.Ch04.SourceObservable.const U hU b = { measurableSet := hU, toFun := fun (_a : HCPolySupport.Source.Coarse.Carrier d) => b, isLocal := ⋯ }

def HCPolySupport.Book.Ch04.SourceObservable.comp {d : ℕ} {U : Set (Vec d)} {β : Type u_1} {γ : Type u_2} [MeasurableSpace β] [MeasurableSpace γ] (X : SourceObservable d U β) (g : β → γ) (hg : Measurable g) : SourceObservable d U γ

Measurable postcomposition of a bundled source observable.

Equations

• X.comp g hg = { measurableSet := ⋯, toFun := fun (a : HCPolySupport.Source.Coarse.Carrier d) => g (X.toFun a), isLocal := ⋯ }

def HCPolySupport.Book.Ch04.SourceObservable.translate {d : ℕ} {U : Set (Vec d)} {β : Type u_1} [MeasurableSpace β] (X : SourceObservable d U β) (z : Fin d → ℤ) : SourceObservable d (translateSet (intVecToRealVec z) U) β

Translate a bundled source observable together with its observation region.

Equations

• X.translate z = { measurableSet := ⋯, toFun := X.toFun ∘ HCPolySupport.Source.Coarse.Carrier.translate z, isLocal := ⋯ }

@[simp]

theorem HCPolySupport.Book.Ch04.SourceObservable.translate_apply {d : ℕ} {U : Set (Vec d)} {β : Type u_1} [MeasurableSpace β] (X : SourceObservable d U β) (z : Fin d → ℤ) (a : Source.Coarse.Carrier d) : (X.translate z).toFun a = X.toFun (Source.Coarse.Carrier.translate z a)

def HCPolySupport.Book.Ch04.SourceObservable.vecOfComponents {d m : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (X : Fin m → SourceObservable d U ℝ) : SourceObservable d U (Vec m)

Build a vector-valued bundled source observable from bundled components.

Equations

• HCPolySupport.Book.Ch04.SourceObservable.vecOfComponents hU X = { measurableSet := hU, toFun := fun (a : HCPolySupport.Source.Coarse.Carrier d) (i : Fin m) => (X i).toFun a, isLocal := ⋯ }

def HCPolySupport.Book.Ch04.SourceObservable.vecComponent {d m : ℕ} {U : Set (Vec d)} (X : SourceObservable d U (Vec m)) (i : Fin m) : SourceObservable d U ℝ

Extract one component of a vector-valued bundled source observable.

Equations

• X.vecComponent i = { measurableSet := ⋯, toFun := fun (a : HCPolySupport.Source.Coarse.Carrier d) => X.toFun a i, isLocal := ⋯ }

def HCPolySupport.Book.Ch04.SourceObservable.matOfEntries {d m : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (X : Fin m → Fin m → SourceObservable d U ℝ) : SourceObservable d U (Mat m)

Build a matrix-valued bundled source observable from bundled entries.

Equations

• HCPolySupport.Book.Ch04.SourceObservable.matOfEntries hU X = { measurableSet := hU, toFun := fun (a : HCPolySupport.Source.Coarse.Carrier d) (i j : Fin m) => (X i j).toFun a, isLocal := ⋯ }

def HCPolySupport.Book.Ch04.SourceObservable.matEntry {d m : ℕ} {U : Set (Vec d)} (X : SourceObservable d U (Mat m)) (i j : Fin m) : SourceObservable d U ℝ

Extract one entry of a matrix-valued bundled source observable.

Equations

• X.matEntry i j = { measurableSet := ⋯, toFun := fun (a : HCPolySupport.Source.Coarse.Carrier d) => X.toFun a i j, isLocal := ⋯ }

def HCPolySupport.Book.Ch04.SourceObservable.add {d : ℕ} {U : Set (Vec d)} (X Y : SourceObservable d U ℝ) : SourceObservable d U ℝ

Sum of bundled source observables.

Equations

• X.add Y = { measurableSet := ⋯, toFun := fun (a : HCPolySupport.Source.Coarse.Carrier d) => X.toFun a + Y.toFun a, isLocal := ⋯ }

def HCPolySupport.Book.Ch04.SourceObservable.neg {d : ℕ} {U : Set (Vec d)} (X : SourceObservable d U ℝ) : SourceObservable d U ℝ

Negation of a bundled source observable.

Equations

• X.neg = { measurableSet := ⋯, toFun := fun (a : HCPolySupport.Source.Coarse.Carrier d) => -X.toFun a, isLocal := ⋯ }

def HCPolySupport.Book.Ch04.SourceObservable.sub {d : ℕ} {U : Set (Vec d)} (X Y : SourceObservable d U ℝ) : SourceObservable d U ℝ

Difference of bundled source observables.

Equations

• X.sub Y = { measurableSet := ⋯, toFun := fun (a : HCPolySupport.Source.Coarse.Carrier d) => X.toFun a - Y.toFun a, isLocal := ⋯ }

def HCPolySupport.Book.Ch04.SourceObservable.mul {d : ℕ} {U : Set (Vec d)} (X Y : SourceObservable d U ℝ) : SourceObservable d U ℝ

Product of bundled source observables.

Equations

• X.mul Y = { measurableSet := ⋯, toFun := fun (a : HCPolySupport.Source.Coarse.Carrier d) => X.toFun a * Y.toFun a, isLocal := ⋯ }

noncomputable def HCPolySupport.Book.Ch04.SourceObservable.inv {d : ℕ} {U : Set (Vec d)} (X : SourceObservable d U ℝ) : SourceObservable d U ℝ

Inverse of a bundled source observable.

Equations

• X.inv = { measurableSet := ⋯, toFun := fun (a : HCPolySupport.Source.Coarse.Carrier d) => (X.toFun a)⁻¹, isLocal := ⋯ }

def HCPolySupport.Book.Ch04.SourceObservable.abs {d : ℕ} {U : Set (Vec d)} (X : SourceObservable d U ℝ) : SourceObservable d U ℝ

Absolute value of a bundled source observable.

Equations

• X.abs = { measurableSet := ⋯, toFun := fun (a : HCPolySupport.Source.Coarse.Carrier d) => |X.toFun a|, isLocal := ⋯ }

def HCPolySupport.Book.Ch04.SourceObservable.finsetSum {d : ℕ} {U : Set (Vec d)} {ι : Type u_1} [Fintype ι] (hU : MeasurableSet U) (X : ι → SourceObservable d U ℝ) : SourceObservable d U ℝ

Finite sum of bundled source observables.

Equations

• HCPolySupport.Book.Ch04.SourceObservable.finsetSum hU X = { measurableSet := hU, toFun := fun (a : HCPolySupport.Source.Coarse.Carrier d) => ∑ i : ι, (X i).toFun a, isLocal := ⋯ }