Coarse-graining support: Support.Probability.LocalObservable

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

Generic measurable local observables on coefficient space.

This file packages the common probability-theoretic pattern:

• a coefficient-space observable is measurable;
• it depends only on the coefficient field inside a deterministic region U;
• therefore its law and its Bochner integrals depend only on the restricted law Measure.map (restrictCoeffField U) P.

Concrete coarse observables such as Mu U P, the coarse matrix entries, and their matrix-valued packages should be bundled as instances of MeasurableLocalObservable in downstream files.

theorem HCPolySupport.restrictCoeffField_eq_of_forall_mem_eq {d : ℕ} {U : Set (Vec d)} {a₁ a₂ : CoeffField d} (h : ∀ x ∈ U, a₁ x = a₂ x) : restrictCoeffField U a₁ = restrictCoeffField U a₂

theorem HCPolySupport.comp_restrictCoeffField_eq_of_isRestrictionLocalObservable {β : Type u_1} {d : ℕ} {U : Set (Vec d)} {X : CoeffField d → β} (hX : IsRestrictionLocalObservable U X) : X ∘ restrictCoeffField U = X

theorem HCPolySupport.comp_restrictCoeffField_eq_of_isLocalObservable {β : Type u_1} {d : ℕ} {U : Set (Vec d)} {X : CoeffField d → β} (hX : IsLocalObservable U X) : X ∘ restrictCoeffField U = X

Compatibility spelling for the restriction-local restriction identity.

theorem HCPolySupport.map_eq_map_restrictCoeffField_of_isRestrictionLocalObservable {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U : Set (Vec d)} {P : MeasureTheory.Measure (CoeffField d)} {X : CoeffField d → β} (hX_meas : Measurable X) (hX_local : IsRestrictionLocalObservable U X) : MeasureTheory.Measure.map X (MeasureTheory.Measure.map (restrictCoeffField U) P) = MeasureTheory.Measure.map X P

theorem HCPolySupport.map_eq_map_restrictCoeffField_of_isLocalObservable {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U : Set (Vec d)} {P : MeasureTheory.Measure (CoeffField d)} {X : CoeffField d → β} (hX_meas : Measurable X) (hX_local : IsRestrictionLocalObservable U X) : MeasureTheory.Measure.map X (MeasureTheory.Measure.map (restrictCoeffField U) P) = MeasureTheory.Measure.map X P

Compatibility spelling for the restriction-local map identity.

theorem HCPolySupport.map_eq_of_map_restrictCoeffField_eq_of_isRestrictionLocalObservable {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U : Set (Vec d)} {P Q : MeasureTheory.Measure (CoeffField d)} {X : CoeffField d → β} (hX_meas : Measurable X) (hX_local : IsRestrictionLocalObservable U X) (hPQ : MeasureTheory.Measure.map (restrictCoeffField U) P = MeasureTheory.Measure.map (restrictCoeffField U) Q) : MeasureTheory.Measure.map X P = MeasureTheory.Measure.map X Q

theorem HCPolySupport.map_eq_of_map_restrictCoeffField_eq_of_isLocalObservable {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U : Set (Vec d)} {P Q : MeasureTheory.Measure (CoeffField d)} {X : CoeffField d → β} (hX_meas : Measurable X) (hX_local : IsLocalObservable U X) (hPQ : MeasureTheory.Measure.map (restrictCoeffField U) P = MeasureTheory.Measure.map (restrictCoeffField U) Q) : MeasureTheory.Measure.map X P = MeasureTheory.Measure.map X Q

Compatibility spelling for the restriction-local map comparison.

theorem HCPolySupport.integral_map_restrictCoeffField_eq_of_isRestrictionLocalObservable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {d : ℕ} {U : Set (Vec d)} {P : MeasureTheory.Measure (CoeffField d)} {X : CoeffField d → E} (hX_meas : Measurable X) (hX_local : IsRestrictionLocalObservable U X) : ∫ (a : CoeffField d), X a ∂MeasureTheory.Measure.map (restrictCoeffField U) P = ∫ (a : CoeffField d), X a ∂P

theorem HCPolySupport.integral_map_restrictCoeffField_eq_of_isLocalObservable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {d : ℕ} {U : Set (Vec d)} {P : MeasureTheory.Measure (CoeffField d)} {X : CoeffField d → E} (hX_meas : Measurable X) (hX_local : IsLocalObservable U X) : ∫ (a : CoeffField d), X a ∂MeasureTheory.Measure.map (restrictCoeffField U) P = ∫ (a : CoeffField d), X a ∂P

Compatibility spelling for the restriction-local integral identity.

theorem HCPolySupport.integral_eq_of_map_restrictCoeffField_eq_of_isRestrictionLocalObservable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {d : ℕ} {U : Set (Vec d)} {P Q : MeasureTheory.Measure (CoeffField d)} {X : CoeffField d → E} (hX_meas : Measurable X) (hX_local : IsRestrictionLocalObservable U X) (hPQ : MeasureTheory.Measure.map (restrictCoeffField U) P = MeasureTheory.Measure.map (restrictCoeffField U) Q) : ∫ (a : CoeffField d), X a ∂P = ∫ (a : CoeffField d), X a ∂Q

theorem HCPolySupport.integral_eq_of_map_restrictCoeffField_eq_of_isLocalObservable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {d : ℕ} {U : Set (Vec d)} {P Q : MeasureTheory.Measure (CoeffField d)} {X : CoeffField d → E} (hX_meas : Measurable X) (hX_local : IsLocalObservable U X) (hPQ : MeasureTheory.Measure.map (restrictCoeffField U) P = MeasureTheory.Measure.map (restrictCoeffField U) Q) : ∫ (a : CoeffField d), X a ∂P = ∫ (a : CoeffField d), X a ∂Q

Compatibility spelling for the restriction-local integral comparison.

theorem HCPolySupport.measurable_of_isRestrictionLocalObservable_restrictionSigma {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U : Set (Vec d)} {X : CoeffField d → β} (hX_meas : Measurable X) (hX_local : IsRestrictionLocalObservable U X) : Measurable X

theorem HCPolySupport.IsRestrictionLocalObservable.mono {β : Type u_1} {d : ℕ} {U V : Set (Vec d)} {X : CoeffField d → β} (hX : IsRestrictionLocalObservable U X) (hUV : U ⊆ V) : IsRestrictionLocalObservable V X

theorem HCPolySupport.IsLocalObservable.mono {β : Type u_1} {d : ℕ} {U V : Set (Vec d)} {X : CoeffField d → β} (hX : IsLocalObservable U X) (hUV : U ⊆ V) : IsLocalObservable V X

Compatibility spelling for IsRestrictionLocalObservable.mono.

theorem HCPolySupport.measurable_of_isLocalObservable_restrictionSigma {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U : Set (Vec d)} {X : CoeffField d → β} (hX_meas : Measurable X) (hX_local : IsLocalObservable U X) : Measurable X

Compatibility spelling for the restriction-local measurability theorem.

theorem HCPolySupport.measurable_of_isRestrictionLocalObservable_restrictionSigma_mono {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U V : Set (Vec d)} {X : CoeffField d → β} (hX_meas : Measurable X) (hX_local : IsRestrictionLocalObservable U X) (hUV : U ⊆ V) : Measurable X

theorem HCPolySupport.measurable_of_isLocalObservable_restrictionSigma_mono {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U V : Set (Vec d)} {X : CoeffField d → β} (hX_meas : Measurable X) (hX_local : IsLocalObservable U X) (hUV : U ⊆ V) : Measurable X

Compatibility spelling for the monotone restriction-local measurability theorem.

theorem HCPolySupport.comp_translateByInt_eq_of_isTranslationCovariant {β : Type u_1} {d : ℕ} {X : Set (Vec d) → CoeffField d → β} (hX : IsTranslationCovariant X) (U : Set (Vec d)) (z : Fin d → ℤ) : X (translateSet (intVecToRealVec z) U) = X U ∘ translateByInt z

theorem HCPolySupport.map_eq_map_translateByInt_of_isTranslationCovariant {β : Type u_1} [MeasurableSpace β] {d : ℕ} {P : MeasureTheory.Measure (CoeffField d)} {X : Set (Vec d) → CoeffField d → β} (hP : IsStationary P) {U : Set (Vec d)} (hX_meas : Measurable (X U)) (hX_cov : IsTranslationCovariant X) (z : Fin d → ℤ) : MeasureTheory.Measure.map (X (translateSet (intVecToRealVec z) U)) P = MeasureTheory.Measure.map (X U) P

theorem HCPolySupport.map_eq_map_translateByInt_of_isTranslationCovariant_aemeasurable {β : Type u_1} [MeasurableSpace β] {d : ℕ} {P : MeasureTheory.Measure (CoeffField d)} {X : Set (Vec d) → CoeffField d → β} (hP : IsStationary P) {U : Set (Vec d)} (hX_aemeas : AEMeasurable (X U) P) (hX_cov : IsTranslationCovariant X) (z : Fin d → ℤ) : MeasureTheory.Measure.map (X (translateSet (intVecToRealVec z) U)) P = MeasureTheory.Measure.map (X U) P

A.e.-measurable version of map_eq_map_translateByInt_of_isTranslationCovariant.

theorem HCPolySupport.integral_eq_of_isTranslationCovariant_of_isStationary {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {d : ℕ} {P : MeasureTheory.Measure (CoeffField d)} {X : Set (Vec d) → CoeffField d → E} (hP : IsStationary P) {U : Set (Vec d)} (hX_meas : Measurable (X U)) (hX_cov : IsTranslationCovariant X) (z : Fin d → ℤ) : ∫ (a : CoeffField d), X (translateSet (intVecToRealVec z) U) a ∂P = ∫ (a : CoeffField d), X U a ∂P

theorem HCPolySupport.integral_eq_of_isTranslationCovariant_of_isStationary_aestronglyMeasurable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {d : ℕ} {P : MeasureTheory.Measure (CoeffField d)} {X : Set (Vec d) → CoeffField d → E} (hP : IsStationary P) {U : Set (Vec d)} (hX_aemeas : MeasureTheory.AEStronglyMeasurable (X U) P) (hX_cov : IsTranslationCovariant X) (z : Fin d → ℤ) : ∫ (a : CoeffField d), X (translateSet (intVecToRealVec z) U) a ∂P = ∫ (a : CoeffField d), X U a ∂P

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

A coefficient-space observable that is both measurable and pointwise restriction-local on U.

• toFun : CoeffField d → β

  The measurable coefficient-field observable determined by the field's values on U.

• measurable_toFun : Measurable self.toFun
• isLocal_toFun : IsRestrictionLocalObservable U self.toFun

@[instance_reducible]

instance HCPolySupport.MeasurableLocalObservable.instCoeFunForallCoeffField {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U : Set (Vec d)} : CoeFun (MeasurableLocalObservable d U β) fun (x : MeasurableLocalObservable d U β) => CoeffField d → β

Equations

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

theorem HCPolySupport.MeasurableLocalObservable.measurable {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U : Set (Vec d)} (X : MeasurableLocalObservable d U β) : Measurable X.toFun

theorem HCPolySupport.MeasurableLocalObservable.isLocal {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U : Set (Vec d)} (X : MeasurableLocalObservable d U β) : IsLocalObservable U X.toFun

theorem HCPolySupport.MeasurableLocalObservable.isRestrictionLocal {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U : Set (Vec d)} (X : MeasurableLocalObservable d U β) : IsRestrictionLocalObservable U X.toFun

The explicit restriction-local spelling of the bundled locality field.

theorem HCPolySupport.MeasurableLocalObservable.measurable_restrictionSigma {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U : Set (Vec d)} (X : MeasurableLocalObservable d U β) : Measurable X.toFun

theorem HCPolySupport.MeasurableLocalObservable.measurable_restrictionSigma_mono {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U V : Set (Vec d)} (X : MeasurableLocalObservable d U β) (hUV : U ⊆ V) : Measurable X.toFun

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

Regard an observable local to U as local to a containing region V.

Equations

• X.mono hUV = { toFun := X.toFun, measurable_toFun := ⋯, isLocal_toFun := ⋯ }

@[simp]

theorem HCPolySupport.MeasurableLocalObservable.mono_apply {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U V : Set (Vec d)} (X : MeasurableLocalObservable d U β) (hUV : U ⊆ V) (a : CoeffField d) : (X.mono hUV).toFun a = X.toFun a

def HCPolySupport.MeasurableLocalObservable.const {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U : Set (Vec d)} (c : β) : MeasurableLocalObservable d U β

The constant observable with value c, local to any region.

Equations

• HCPolySupport.MeasurableLocalObservable.const c = { toFun := fun (x : HCPolySupport.CoeffField d) => c, measurable_toFun := ⋯, isLocal_toFun := ⋯ }

def HCPolySupport.MeasurableLocalObservable.comp {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U : Set (Vec d)} {γ : Type u_2} [MeasurableSpace γ] (X : MeasurableLocalObservable d U β) (f : β → γ) (hf : Measurable f) : MeasurableLocalObservable d U γ

Compose a local observable with a measurable function of its value.

Equations

• X.comp f hf = { toFun := f ∘ X.toFun, measurable_toFun := ⋯, isLocal_toFun := ⋯ }

def HCPolySupport.MeasurableLocalObservable.prod {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U : Set (Vec d)} {γ : Type u_2} [MeasurableSpace γ] (X : MeasurableLocalObservable d U β) (Y : MeasurableLocalObservable d U γ) : MeasurableLocalObservable d U (β × γ)

The pair of two measurable observables local to the same region.

Equations

• X.prod Y = { toFun := fun (a : HCPolySupport.CoeffField d) => (X.toFun a, Y.toFun a), measurable_toFun := ⋯, isLocal_toFun := ⋯ }

def HCPolySupport.MeasurableLocalObservable.pi {d : ℕ} {U : Set (Vec d)} {ι : Type u_2} {γ : ι → Type u_3} [(i : ι) → MeasurableSpace (γ i)] (X : (i : ι) → MeasurableLocalObservable d U (γ i)) : MeasurableLocalObservable d U ((i : ι) → γ i)

The coordinate family formed from measurable observables local to the same region.

Equations

• HCPolySupport.MeasurableLocalObservable.pi X = { toFun := fun (a : HCPolySupport.CoeffField d) (i : ι) => (X i).toFun a, measurable_toFun := ⋯, isLocal_toFun := ⋯ }

def HCPolySupport.MeasurableLocalObservable.neg {d : ℕ} {U : Set (Vec d)} {β : Type u_2} [MeasurableSpace β] [Neg β] [MeasurableNeg β] (X : MeasurableLocalObservable d U β) : MeasurableLocalObservable d U β

The pointwise negation of a measurable local observable.

Equations

• X.neg = X.comp (fun (x : β) => -x) ⋯

def HCPolySupport.MeasurableLocalObservable.add {d : ℕ} {U : Set (Vec d)} {β : Type u_2} [MeasurableSpace β] [Add β] [MeasurableAdd₂ β] (X Y : MeasurableLocalObservable d U β) : MeasurableLocalObservable d U β

The pointwise sum of two measurable local observables.

Equations

• X.add Y = { toFun := fun (a : HCPolySupport.CoeffField d) => X.toFun a + Y.toFun a, measurable_toFun := ⋯, isLocal_toFun := ⋯ }

def HCPolySupport.MeasurableLocalObservable.sub {d : ℕ} {U : Set (Vec d)} {β : Type u_2} [MeasurableSpace β] [Sub β] [MeasurableSub₂ β] (X Y : MeasurableLocalObservable d U β) : MeasurableLocalObservable d U β

The pointwise difference of two measurable local observables.

Equations

• X.sub Y = { toFun := fun (a : HCPolySupport.CoeffField d) => X.toFun a - Y.toFun a, measurable_toFun := ⋯, isLocal_toFun := ⋯ }

def HCPolySupport.MeasurableLocalObservable.constantScalarMultiply {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U : Set (Vec d)} {M : Type u_2} [SMul M β] [MeasurableConstSMul M β] (c : M) (X : MeasurableLocalObservable d U β) : MeasurableLocalObservable d U β

Multiply a measurable local observable by a fixed scalar.

Equations

• HCPolySupport.MeasurableLocalObservable.constantScalarMultiply c X = { toFun := fun (a : HCPolySupport.CoeffField d) => c • X.toFun a, measurable_toFun := ⋯, isLocal_toFun := ⋯ }

def HCPolySupport.MeasurableLocalObservable.finsetPi {d : ℕ} {ι : Type u_2} {γ : ι → Type u_3} [(i : ι) → MeasurableSpace (γ i)] (s : Finset ι) {V : ι → Set (Vec d)} (X : (i : ι) → MeasurableLocalObservable d (V i) (γ i)) : MeasurableLocalObservable d (⋃ i ∈ s, V i) ((i : ↥s) → γ ↑i)

The finite coordinate family of observables, local to the union of their regions.

Equations

• HCPolySupport.MeasurableLocalObservable.finsetPi s X = { toFun := fun (a : HCPolySupport.CoeffField d) (i : ↥s) => (X ↑i).toFun a, measurable_toFun := ⋯, isLocal_toFun := ⋯ }

theorem HCPolySupport.MeasurableLocalObservable.measurable_subtypeFinsetSum {ι : Type u_2} (s : Finset ι) {γ : Type u_3} [MeasurableSpace γ] [AddCommMonoid γ] [MeasurableAdd₂ γ] : Measurable fun (y : ↥s → γ) => ∑ i : ↥s, y i

noncomputable def HCPolySupport.MeasurableLocalObservable.finsetSum {d : ℕ} {ι : Type u_2} {γ : Type u_3} [MeasurableSpace γ] [AddCommMonoid γ] [MeasurableAdd₂ γ] (s : Finset ι) {V : ι → Set (Vec d)} (X : (i : ι) → MeasurableLocalObservable d (V i) γ) : MeasurableLocalObservable d (⋃ i ∈ s, V i) γ

The finite sum of observables, local to the union of their regions.

Equations

• HCPolySupport.MeasurableLocalObservable.finsetSum s X = (HCPolySupport.MeasurableLocalObservable.finsetPi s X).comp (fun (y : ↥s → γ) => ∑ i : ↥s, y i) ⋯

noncomputable def HCPolySupport.MeasurableLocalObservable.finsetAverage {d : ℕ} {ι : Type u_2} {γ : Type u_3} [MeasurableSpace γ] [AddCommMonoid γ] [MeasurableAdd₂ γ] [SMul ℝ γ] [MeasurableConstSMul ℝ γ] (s : Finset ι) {V : ι → Set (Vec d)} (X : (i : ι) → MeasurableLocalObservable d (V i) γ) : MeasurableLocalObservable d (⋃ i ∈ s, V i) γ

The finite sum multiplied by inverse cardinality, local to the union of the regions.

Equations

• HCPolySupport.MeasurableLocalObservable.finsetAverage s X = HCPolySupport.MeasurableLocalObservable.constantScalarMultiply (↑s.card)⁻¹ (HCPolySupport.MeasurableLocalObservable.finsetSum s X)

theorem HCPolySupport.MeasurableLocalObservable.comp_restrictCoeffField_eq {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U : Set (Vec d)} (X : MeasurableLocalObservable d U β) : X.toFun ∘ restrictCoeffField U = X.toFun

theorem HCPolySupport.MeasurableLocalObservable.map_eq_map_restrictCoeffField {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U : Set (Vec d)} (X : MeasurableLocalObservable d U β) {P : MeasureTheory.Measure (CoeffField d)} : MeasureTheory.Measure.map X.toFun (MeasureTheory.Measure.map (restrictCoeffField U) P) = MeasureTheory.Measure.map X.toFun P

theorem HCPolySupport.MeasurableLocalObservable.map_eq_of_map_restrictCoeffField_eq {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U : Set (Vec d)} (X : MeasurableLocalObservable d U β) {P Q : MeasureTheory.Measure (CoeffField d)} (hPQ : MeasureTheory.Measure.map (restrictCoeffField U) P = MeasureTheory.Measure.map (restrictCoeffField U) Q) : MeasureTheory.Measure.map X.toFun P = MeasureTheory.Measure.map X.toFun Q

theorem HCPolySupport.MeasurableLocalObservable.measurable_comp_randomCoeffField {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U : Set (Vec d)} {Ω : Type u_2} [MeasurableSpace Ω] (X : MeasurableLocalObservable d U β) (A : RandomCoeffField Ω d) : Measurable fun (ω : Ω) => X.toFun (A.toFun ω)

theorem HCPolySupport.MeasurableLocalObservable.measurable_comp_randomCoeffField_restrictionSigma {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U : Set (Vec d)} {Ω : Type u_2} [MeasurableSpace Ω] (X : MeasurableLocalObservable d U β) (A : RandomCoeffField Ω d) : Measurable fun (ω : Ω) => X.toFun (A.toFun ω)

theorem HCPolySupport.MeasurableLocalObservable.indepFun_of_indep_restrictionSigma {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U : Set (Vec d)} {γ : Type u_2} [MeasurableSpace γ] {V : Set (Vec d)} {P : MeasureTheory.Measure (CoeffField d)} (hP : ProbabilityTheory.Indep (RestrictionSigma U) (RestrictionSigma V) P) (X : MeasurableLocalObservable d U β) (Y : MeasurableLocalObservable d V γ) : ProbabilityTheory.IndepFun X.toFun Y.toFun P

theorem HCPolySupport.MeasurableLocalObservable.integral_map_restrictCoeffField_eq {d : ℕ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {U : Set (Vec d)} (X : MeasurableLocalObservable d U E) {P : MeasureTheory.Measure (CoeffField d)} : ∫ (a : CoeffField d), X.toFun a ∂MeasureTheory.Measure.map (restrictCoeffField U) P = ∫ (a : CoeffField d), X.toFun a ∂P

theorem HCPolySupport.MeasurableLocalObservable.integral_eq_of_map_restrictCoeffField_eq {d : ℕ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {U : Set (Vec d)} (X : MeasurableLocalObservable d U E) {P Q : MeasureTheory.Measure (CoeffField d)} (hPQ : MeasureTheory.Measure.map (restrictCoeffField U) P = MeasureTheory.Measure.map (restrictCoeffField U) Q) : ∫ (a : CoeffField d), X.toFun a ∂P = ∫ (a : CoeffField d), X.toFun a ∂Q

theorem HCPolySupport.MeasurableLocalObservable.iIndepFun_of_isRestrictionUnitRangeDependent {d : ℕ} {ι : Type u_2} {γ : ι → Type u_3} [(i : ι) → MeasurableSpace (γ i)] {P : MeasureTheory.Measure (CoeffField d)} [MeasureTheory.IsProbabilityMeasure P] {V : ι → Set (Vec d)} (hP : IsRestrictionUnitRangeDependent P) (hsep : Pairwise fun (i j : ι) => AreUnitSeparated (V i) (V j)) (X : (i : ι) → MeasurableLocalObservable d (V i) (γ i)) : ProbabilityTheory.iIndepFun (fun (i : ι) => (X i).toFun) P

theorem HCPolySupport.MeasurableLocalObservable.indepFun_finset_of_isRestrictionUnitRangeDependent {d : ℕ} {ι : Type u_2} {γ : ι → Type u_3} [(i : ι) → MeasurableSpace (γ i)] {P : MeasureTheory.Measure (CoeffField d)} [MeasureTheory.IsProbabilityMeasure P] {V : ι → Set (Vec d)} (hP : IsRestrictionUnitRangeDependent P) (hsep : Pairwise fun (i j : ι) => AreUnitSeparated (V i) (V j)) (X : (i : ι) → MeasurableLocalObservable d (V i) (γ i)) (S T : Finset ι) (hST : Disjoint S T) : ProbabilityTheory.IndepFun (fun (a : CoeffField d) (i : ↥S) => (X ↑i).toFun a) (fun (a : CoeffField d) (i : ↥T) => (X ↑i).toFun a) P

theorem HCPolySupport.MeasurableLocalObservable.indepFun_finsetSum_of_isRestrictionUnitRangeDependent {d : ℕ} {ι : Type u_2} {γ : Type u_3} [MeasurableSpace γ] [AddCommMonoid γ] [MeasurableAdd₂ γ] {P : MeasureTheory.Measure (CoeffField d)} [MeasureTheory.IsProbabilityMeasure P] {V : ι → Set (Vec d)} (hP : IsRestrictionUnitRangeDependent P) (hsep : Pairwise fun (i j : ι) => AreUnitSeparated (V i) (V j)) (X : (i : ι) → MeasurableLocalObservable d (V i) γ) (S T : Finset ι) (hST : Disjoint S T) : ProbabilityTheory.IndepFun (finsetSum S X).toFun (finsetSum T X).toFun P

theorem HCPolySupport.MeasurableLocalObservable.indepFun_finsetAverage_of_isRestrictionUnitRangeDependent {d : ℕ} {ι : Type u_2} {γ : Type u_3} [MeasurableSpace γ] [AddCommMonoid γ] [MeasurableAdd₂ γ] [SMul ℝ γ] [MeasurableConstSMul ℝ γ] {P : MeasureTheory.Measure (CoeffField d)} [MeasureTheory.IsProbabilityMeasure P] {V : ι → Set (Vec d)} (hP : IsRestrictionUnitRangeDependent P) (hsep : Pairwise fun (i j : ι) => AreUnitSeparated (V i) (V j)) (X : (i : ι) → MeasurableLocalObservable d (V i) γ) (S T : Finset ι) (hST : Disjoint S T) : ProbabilityTheory.IndepFun (finsetAverage S X).toFun (finsetAverage T X).toFun P

theorem HCPolySupport.MeasurableLocalObservable.iIndepFun_descendantsAtScaleColorClass_of_isRestrictionUnitRangeDependent {d : ℕ} {Q : TriadicCube d} {k : ℤ} (hk : 0 ≤ k) {c : CubeColor d} {P : MeasureTheory.Measure (CoeffField d)} [MeasureTheory.IsProbabilityMeasure P] {γ : ↥(descendantsAtScaleColorClass Q k c) → Type u_2} [(R : ↥(descendantsAtScaleColorClass Q k c)) → MeasurableSpace (γ R)] (hP : IsRestrictionUnitRangeDependent P) (X : (R : ↥(descendantsAtScaleColorClass Q k c)) → MeasurableLocalObservable d (cubeSet ↑R) (γ R)) : ProbabilityTheory.iIndepFun (fun (R : ↥(descendantsAtScaleColorClass Q k c)) => (X R).toFun) P

theorem HCPolySupport.MeasurableLocalObservable.indepFun_finset_descendantsAtScaleColorClass_of_isRestrictionUnitRangeDependent {d : ℕ} {Q : TriadicCube d} {k : ℤ} (hk : 0 ≤ k) {c : CubeColor d} {γ : Type u_2} [MeasurableSpace γ] {P : MeasureTheory.Measure (CoeffField d)} [MeasureTheory.IsProbabilityMeasure P] (hP : IsRestrictionUnitRangeDependent P) (X : (R : ↥(descendantsAtScaleColorClass Q k c)) → MeasurableLocalObservable d (cubeSet ↑R) γ) (S T : Finset ↥(descendantsAtScaleColorClass Q k c)) (hST : Disjoint S T) : ProbabilityTheory.IndepFun (fun (a : CoeffField d) (R : ↥S) => (X ↑R).toFun a) (fun (a : CoeffField d) (R : ↥T) => (X ↑R).toFun a) P

theorem HCPolySupport.MeasurableLocalObservable.indepFun_finsetSum_descendantsAtScaleColorClass_of_isRestrictionUnitRangeDependent {d : ℕ} {Q : TriadicCube d} {k : ℤ} (hk : 0 ≤ k) {c : CubeColor d} {γ : Type u_2} [MeasurableSpace γ] [AddCommMonoid γ] [MeasurableAdd₂ γ] {P : MeasureTheory.Measure (CoeffField d)} [MeasureTheory.IsProbabilityMeasure P] (hP : IsRestrictionUnitRangeDependent P) (X : (R : ↥(descendantsAtScaleColorClass Q k c)) → MeasurableLocalObservable d (cubeSet ↑R) γ) (S T : Finset ↥(descendantsAtScaleColorClass Q k c)) (hST : Disjoint S T) : ProbabilityTheory.IndepFun (finsetSum S X).toFun (finsetSum T X).toFun P

theorem HCPolySupport.MeasurableLocalObservable.indepFun_finsetAverage_descendantsAtScaleColorClass_of_isRestrictionUnitRangeDependent {d : ℕ} {Q : TriadicCube d} {k : ℤ} (hk : 0 ≤ k) {c : CubeColor d} {γ : Type u_2} [MeasurableSpace γ] [AddCommMonoid γ] [MeasurableAdd₂ γ] [SMul ℝ γ] [MeasurableConstSMul ℝ γ] {P : MeasureTheory.Measure (CoeffField d)} [MeasureTheory.IsProbabilityMeasure P] (hP : IsRestrictionUnitRangeDependent P) (X : (R : ↥(descendantsAtScaleColorClass Q k c)) → MeasurableLocalObservable d (cubeSet ↑R) γ) (S T : Finset ↥(descendantsAtScaleColorClass Q k c)) (hST : Disjoint S T) : ProbabilityTheory.IndepFun (finsetAverage S X).toFun (finsetAverage T X).toFun P

theorem HCPolySupport.MeasurableLocalObservable.iIndepFun_descendantsAtScaleScaleColorClass_of_isRestrictionUnitRangeDependent {d : ℕ} {Q : TriadicCube d} {k : ℤ} {c : ScaleColor d k} {P : MeasureTheory.Measure (CoeffField d)} [MeasureTheory.IsProbabilityMeasure P] {γ : ↥(descendantsAtScaleScaleColorClass Q k c) → Type u_2} [(R : ↥(descendantsAtScaleScaleColorClass Q k c)) → MeasurableSpace (γ R)] (hP : IsRestrictionUnitRangeDependent P) (X : (R : ↥(descendantsAtScaleScaleColorClass Q k c)) → MeasurableLocalObservable d (cubeSet ↑R) (γ R)) : ProbabilityTheory.iIndepFun (fun (R : ↥(descendantsAtScaleScaleColorClass Q k c)) => (X R).toFun) P

theorem HCPolySupport.MeasurableLocalObservable.indepFun_finset_descendantsAtScaleScaleColorClass_of_isRestrictionUnitRangeDependent {d : ℕ} {Q : TriadicCube d} {k : ℤ} {c : ScaleColor d k} {γ : Type u_2} [MeasurableSpace γ] {P : MeasureTheory.Measure (CoeffField d)} [MeasureTheory.IsProbabilityMeasure P] (hP : IsRestrictionUnitRangeDependent P) (X : (R : ↥(descendantsAtScaleScaleColorClass Q k c)) → MeasurableLocalObservable d (cubeSet ↑R) γ) (S T : Finset ↥(descendantsAtScaleScaleColorClass Q k c)) (hST : Disjoint S T) : ProbabilityTheory.IndepFun (fun (a : CoeffField d) (R : ↥S) => (X ↑R).toFun a) (fun (a : CoeffField d) (R : ↥T) => (X ↑R).toFun a) P

theorem HCPolySupport.MeasurableLocalObservable.indepFun_finsetSum_descendantsAtScaleScaleColorClass_of_isRestrictionUnitRangeDependent {d : ℕ} {Q : TriadicCube d} {k : ℤ} {c : ScaleColor d k} {γ : Type u_2} [MeasurableSpace γ] [AddCommMonoid γ] [MeasurableAdd₂ γ] {P : MeasureTheory.Measure (CoeffField d)} [MeasureTheory.IsProbabilityMeasure P] (hP : IsRestrictionUnitRangeDependent P) (X : (R : ↥(descendantsAtScaleScaleColorClass Q k c)) → MeasurableLocalObservable d (cubeSet ↑R) γ) (S T : Finset ↥(descendantsAtScaleScaleColorClass Q k c)) (hST : Disjoint S T) : ProbabilityTheory.IndepFun (finsetSum S X).toFun (finsetSum T X).toFun P

theorem HCPolySupport.MeasurableLocalObservable.indepFun_finsetAverage_descendantsAtScaleScaleColorClass_of_isRestrictionUnitRangeDependent {d : ℕ} {Q : TriadicCube d} {k : ℤ} {c : ScaleColor d k} {γ : Type u_2} [MeasurableSpace γ] [AddCommMonoid γ] [MeasurableAdd₂ γ] [SMul ℝ γ] [MeasurableConstSMul ℝ γ] {P : MeasureTheory.Measure (CoeffField d)} [MeasureTheory.IsProbabilityMeasure P] (hP : IsRestrictionUnitRangeDependent P) (X : (R : ↥(descendantsAtScaleScaleColorClass Q k c)) → MeasurableLocalObservable d (cubeSet ↑R) γ) (S T : Finset ↥(descendantsAtScaleScaleColorClass Q k c)) (hST : Disjoint S T) : ProbabilityTheory.IndepFun (finsetAverage S X).toFun (finsetAverage T X).toFun P

@[reducible, inline]

abbrev HCPolySupport.MeasurableRestrictionLocalObservable (d : ℕ) (U : Set (Vec d)) (β : Type u_1) [MeasurableSpace β] : Type u_1

Explicit restriction-local spelling for the unchanged raw coefficient-field observable bundle.

Equations

• HCPolySupport.MeasurableRestrictionLocalObservable d U β = HCPolySupport.MeasurableLocalObservable d U β

theorem HCPolySupport.MeasurableRestrictionLocalObservable.isRestrictionLocal {β : Type u_1} [MeasurableSpace β] {d : ℕ} {U : Set (Vec d)} (X : MeasurableRestrictionLocalObservable d U β) : IsRestrictionLocalObservable U X.toFun

The explicit restriction-local spelling of the bundled locality field.

@[simp]

theorem HCPolySupport.RandomCoeffField.restrictSet_apply {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) (U : Set (Vec d)) (ω : Ω) : (A.restrictSet U).toFun ω = restrictCoeffField U (A.toFun ω)

theorem HCPolySupport.RandomCoeffField.law_eq_law_restrictSet_of_isLocalObservable {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.Measure Ω) {U : Set (Vec d)} {X : CoeffField d → β} (hX_meas : Measurable X) (hX_local : IsRestrictionLocalObservable U X) : MeasureTheory.Measure.map X ((A.restrictSet U).law μ) = MeasureTheory.Measure.map X (A.law μ)

theorem HCPolySupport.RandomCoeffField.integral_comp_restrictSet_eq_of_isLocalObservable {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (μ : MeasureTheory.Measure Ω) {U : Set (Vec d)} {X : CoeffField d → E} (hX_local : IsRestrictionLocalObservable U X) : ∫ (ω : Ω), X ((A.restrictSet U).toFun ω) ∂μ = ∫ (ω : Ω), X (A.toFun ω) ∂μ

theorem HCPolySupport.RandomCoeffField.integral_law_restrictSet_eq_of_isLocalObservable {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (μ : MeasureTheory.Measure Ω) {U : Set (Vec d)} {X : CoeffField d → E} (hX_meas : Measurable X) (hX_local : IsRestrictionLocalObservable U X) : ∫ (a : CoeffField d), X a ∂(A.restrictSet U).law μ = ∫ (a : CoeffField d), X a ∂A.law μ

theorem HCPolySupport.RandomCoeffField.law_eq_law_restrictSet {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.Measure Ω) {U : Set (Vec d)} (X : MeasurableLocalObservable d U β) : MeasureTheory.Measure.map X.toFun ((A.restrictSet U).law μ) = MeasureTheory.Measure.map X.toFun (A.law μ)

theorem HCPolySupport.RandomCoeffField.integral_comp_restrictSet_eq {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] (μ : MeasureTheory.Measure Ω) {U : Set (Vec d)} (X : MeasurableLocalObservable d U E) : ∫ (ω : Ω), X.toFun ((A.restrictSet U).toFun ω) ∂μ = ∫ (ω : Ω), X.toFun (A.toFun ω) ∂μ

theorem HCPolySupport.RandomCoeffField.integral_law_restrictSet_eq {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (μ : MeasureTheory.Measure Ω) {U : Set (Vec d)} (X : MeasurableLocalObservable d U E) : ∫ (a : CoeffField d), X.toFun a ∂(A.restrictSet U).law μ = ∫ (a : CoeffField d), X.toFun a ∂A.law μ

theorem HCPolySupport.RandomCoeffField.indepFun_comp_of_indep_restrictionSigma {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) {β : Type u_2} {γ : Type u_3} [MeasurableSpace β] [MeasurableSpace γ] {μ : MeasureTheory.Measure Ω} {U V : Set (Vec d)} (hμ : ProbabilityTheory.Indep (A.restrictionSigma U) (A.restrictionSigma V) μ) (X : MeasurableLocalObservable d U β) (Y : MeasurableLocalObservable d V γ) : ProbabilityTheory.IndepFun (fun (ω : Ω) => X.toFun (A.toFun ω)) (fun (ω : Ω) => Y.toFun (A.toFun ω)) μ

theorem HCPolySupport.RandomCoeffField.iIndepFun_comp_of_iIndep_restrictionSigma {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] {μ : MeasureTheory.Measure Ω} {U : ι → Set (Vec d)} (hμ : ProbabilityTheory.iIndep (fun (i : ι) => A.restrictionSigma (U i)) μ) (X : (i : ι) → MeasurableLocalObservable d (U i) (β i)) : ProbabilityTheory.iIndepFun (fun (i : ι) (ω : Ω) => (X i).toFun (A.toFun ω)) μ

theorem HCPolySupport.RandomCoeffField.indepFun_comp_finset_of_iIndep_restrictionSigma {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] {μ : MeasureTheory.Measure Ω} {U : ι → Set (Vec d)} (hμ : ProbabilityTheory.iIndep (fun (i : ι) => A.restrictionSigma (U i)) μ) (X : (i : ι) → MeasurableLocalObservable d (U i) (β i)) (S T : Finset ι) (hST : Disjoint S T) : ProbabilityTheory.IndepFun (fun (ω : Ω) (i : ↥S) => (X ↑i).toFun (A.toFun ω)) (fun (ω : Ω) (i : ↥T) => (X ↑i).toFun (A.toFun ω)) μ

theorem HCPolySupport.RandomCoeffField.indepFun_comp_finsetSum_of_iIndep_restrictionSigma {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) {ι : Type u_2} {β : Type u_3} [MeasurableSpace β] [AddCommMonoid β] [MeasurableAdd₂ β] {μ : MeasureTheory.Measure Ω} {U : ι → Set (Vec d)} (hμ : ProbabilityTheory.iIndep (fun (i : ι) => A.restrictionSigma (U i)) μ) (X : (i : ι) → MeasurableLocalObservable d (U i) β) (S T : Finset ι) (hST : Disjoint S T) : ProbabilityTheory.IndepFun (fun (ω : Ω) => (MeasurableLocalObservable.finsetSum S X).toFun (A.toFun ω)) (fun (ω : Ω) => (MeasurableLocalObservable.finsetSum T X).toFun (A.toFun ω)) μ

theorem HCPolySupport.RandomCoeffField.indepFun_comp_finsetAverage_of_iIndep_restrictionSigma {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : RandomCoeffField Ω d) {ι : Type u_2} {β : Type u_3} [MeasurableSpace β] [AddCommMonoid β] [MeasurableAdd₂ β] [SMul ℝ β] [MeasurableConstSMul ℝ β] {μ : MeasureTheory.Measure Ω} {U : ι → Set (Vec d)} (hμ : ProbabilityTheory.iIndep (fun (i : ι) => A.restrictionSigma (U i)) μ) (X : (i : ι) → MeasurableLocalObservable d (U i) β) (S T : Finset ι) (hST : Disjoint S T) : ProbabilityTheory.IndepFun (fun (ω : Ω) => (MeasurableLocalObservable.finsetAverage S X).toFun (A.toFun ω)) (fun (ω : Ω) => (MeasurableLocalObservable.finsetAverage T X).toFun (A.toFun ω)) μ