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

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

Local observables (carrier re-type, Packet P3)

IsRestrictionLocalRandomVariable U hU X is the permanent Ch4 predicate for restriction-local random observables. Following the carrier redesign, observables are functions of the honest-fields carrier RegCoeffField d, and locality is measurability for the carrier restriction σ-algebra RestrictionSigmaR U hU (which needs the observation set to be measurable — the D7-approved MeasurableSet side-condition making RestrictionSigmaR well defined). Everything downstream should enter measurability through this predicate and the promotion lemmas in Ch04.Measurability.

Reference: the paper (Armstrong–Kuusi–Loher, to appear).

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

A random observable depending only on the restriction-local carrier σ-algebra on the measurable set U.

Equations

• HCPolySupport.Book.Ch04.IsRestrictionLocalRandomVariable U hU X = Measurable X

theorem HCPolySupport.Book.Ch04.IsRestrictionLocalRandomVariable.restrictionSigma_mono {d : ℕ} {U V : Set (Vec d)} (hU : MeasurableSet U) (hV : MeasurableSet V) (hUV : U ⊆ V) : RestrictionSigmaR U hU ≤ RestrictionSigmaR V hV

Monotonicity of the restriction-local carrier σ-algebra.

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

A local observable on a smaller observation set is local on any larger one.

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

Constant local observables.

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

Compose a local observable with a measurable map.

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

Locality of a vector-valued observable follows componentwise.

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

Components of a vector-valued local observable are local.

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

Locality of a matrix-valued observable follows entrywise.

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

Entries of a matrix-valued local observable are local.

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

Sum of real-valued local observables.

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

Negation of a real-valued local observable.

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

Difference of real-valued local observables.

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

Product of real-valued local observables.

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

Inverse of a real-valued local observable.

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

Absolute value of a real-valued local observable.

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

Finite sums of real-valued local observables.

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

Bundled restriction-local Chapter 4 observable. This is the canonical engineering object for whole-restriction locality. The observation set's measurability is kept as a field (rather than a type parameter) so the type signature remains stable.

• measurableSet : MeasurableSet U
• toFun : RegCoeffField d → β

  The observable on regular coefficient fields whose measurability is local to restriction on U.

• isLocal : IsRestrictionLocalRandomVariable U ⋯ self.toFun

@[instance_reducible]

instance HCPolySupport.Book.Ch04.RestrictionObservable.instCoeFunForallRegCoeffField {d : ℕ} {U : Set (Vec d)} {β : Type u_1} [MeasurableSpace β] : CoeFun (RestrictionObservable d U β) fun (x : RestrictionObservable d U β) => RegCoeffField d → β

Equations

• HCPolySupport.Book.Ch04.RestrictionObservable.instCoeFunForallRegCoeffField = { coe := HCPolySupport.Book.Ch04.RestrictionObservable.toFun }

theorem HCPolySupport.Book.Ch04.RestrictionObservable.isRestrictionLocal {d : ℕ} {U : Set (Vec d)} {β : Type u_1} [MeasurableSpace β] (X : RestrictionObservable d U β) : IsRestrictionLocalRandomVariable U ⋯ X.toFun

Explicit accessor for the permanent restriction-locality predicate.

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

Enlarge the observation set of a bundled observable.

Equations

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

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

Constant bundled observables.

Equations

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

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

Measurable postcomposition of a bundled observable.

Equations

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

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

Build a vector-valued bundled observable from bundled components.

Equations

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

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

Extract one component of a vector-valued bundled observable.

Equations

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

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

Build a matrix-valued bundled observable from bundled entries.

Equations

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

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

Extract one entry of a matrix-valued bundled observable.

Equations

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

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

Sum of real-valued bundled observables.

Equations

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

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

Negation of a real-valued bundled observable.

Equations

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

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

Difference of real-valued bundled observables.

Equations

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

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

Product of real-valued bundled observables.

Equations

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

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

Inverse of a real-valued bundled observable.

Equations

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

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

Absolute value of a real-valued bundled observable.

Equations

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

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

Finite sum of real-valued bundled observables over a finite type.

Equations

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