Coarse-graining support: Support.Probability.RandomFieldMeasurability

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

Foundational measurability lemmas for coefficient fields viewed as the sample space of the probability layer.

This file stays deliberately law-centric: the primitive random object remains a measure on CoeffField d. The role of the present API is to expose the basic measurable coefficient-field transforms and the LocalSigma measurability of the generator observables used to define locality in law.

theorem HCPolySupport.measurable_coeffField_entry {d : ℕ} (x : Vec d) (i j : Fin d) : Measurable fun (a : CoeffField d) => a x i j

theorem HCPolySupport.measurable_restrictCoeffField {d : ℕ} (U : Set (Vec d)) : Measurable (restrictCoeffField U)

theorem HCPolySupport.restrictionSigma_le_coeffField {d : ℕ} (U : Set (Vec d)) : RestrictionSigma U ≤ instMeasurableSpaceCoeffField d

theorem HCPolySupport.measurable_restrictCoeffField_restrictionSigma {d : ℕ} (U : Set (Vec d)) : Measurable (restrictCoeffField U)

theorem HCPolySupport.restrictCoeffField_comp_restrictCoeffField_of_subset {d : ℕ} {U V : Set (Vec d)} (hUV : U ⊆ V) : restrictCoeffField U ∘ restrictCoeffField V = restrictCoeffField U

theorem HCPolySupport.measurable_restrictCoeffField_restrictionSigma_of_subset {d : ℕ} {U V : Set (Vec d)} (hUV : U ⊆ V) : Measurable (restrictCoeffField U)

theorem HCPolySupport.RestrictionSigma_mono {d : ℕ} {U V : Set (Vec d)} (hUV : U ⊆ V) : RestrictionSigma U ≤ RestrictionSigma V

theorem HCPolySupport.localTestObservable_translateCoeffField {d : ℕ} (z e e' : Vec d) (φ : Vec d → ℝ) (a : CoeffField d) : localTestObservable e e' φ (translateCoeffField z a) = localTestObservable e e' (fun (y : Vec d) => φ (y - z)) a

theorem HCPolySupport.localFiniteTestObservable_translateCoeffField {d : ℕ} {ι : Type} (z : Vec d) (I : Finset ι) (e e' : ι → Vec d) (φ : ι → Vec d → ℝ) (a : CoeffField d) : localFiniteTestObservable I e e' φ (translateCoeffField z a) = localFiniteTestObservable I e e' (fun (k : ι) (y : Vec d) => φ k (y - z)) a

theorem HCPolySupport.measurable_translateCoeffField {d : ℕ} (z : Vec d) : Measurable (translateCoeffField z)

theorem HCPolySupport.measurable_translateByInt {d : ℕ} (z : Fin d → ℤ) : Measurable (translateByInt z)

theorem HCPolySupport.vecDot_matVecMul_symmPart_cross {d : ℕ} (A : Mat d) (e e' : Vec d) : vecDot e' (matVecMul (symmPart A) e) = 1 / 2 * (vecDot e' (matVecMul A e) + vecDot e (matVecMul A e'))

theorem HCPolySupport.vecDot_matVecMul_skewPart_cross {d : ℕ} (A : Mat d) (e e' : Vec d) : vecDot e' (matVecMul (skewPart A) e) = 1 / 2 * (vecDot e' (matVecMul A e) - vecDot e (matVecMul A e'))

theorem HCPolySupport.localFiniteTestObservable_symmCoeffField {d : ℕ} {ι : Type} (I : Finset ι) (e e' : ι → Vec d) (φ : ι → Vec d → ℝ) (a : CoeffField d) : localFiniteTestObservable I e e' φ (symmCoeffField a) = localFiniteTestObservable (I.product Finset.univ) (fun (kb : ι × Bool) => if kb.2 = true then e' kb.1 else e kb.1) (fun (kb : ι × Bool) => if kb.2 = true then e kb.1 else e' kb.1) (fun (kb : ι × Bool) (x : Vec d) => 1 / 2 * φ kb.1 x) a

theorem HCPolySupport.localFiniteTestObservable_skewCoeffField {d : ℕ} {ι : Type} (I : Finset ι) (e e' : ι → Vec d) (φ : ι → Vec d → ℝ) (a : CoeffField d) : localFiniteTestObservable I e e' φ (skewCoeffField a) = localFiniteTestObservable (I.product Finset.univ) (fun (kb : ι × Bool) => if kb.2 = true then e' kb.1 else e kb.1) (fun (kb : ι × Bool) => if kb.2 = true then e kb.1 else e' kb.1) (fun (kb : ι × Bool) (x : Vec d) => if kb.2 = true then -(1 / 2) * φ kb.1 x else 1 / 2 * φ kb.1 x) a

theorem HCPolySupport.measurable_symmCoeffField {d : ℕ} : Measurable symmCoeffField

theorem HCPolySupport.measurable_skewCoeffField {d : ℕ} : Measurable skewCoeffField

theorem HCPolySupport.IsStationary.map_translateByInt {d : ℕ} {P : MeasureTheory.Measure (CoeffField d)} (hP : IsStationary P) (z : Fin d → ℤ) : MeasureTheory.Measure.map (translateByInt z) P = P

theorem HCPolySupport.integral_comp_translateByInt_eq_of_isStationary {d : ℕ} {P : MeasureTheory.Measure (CoeffField d)} (hP : IsStationary P) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (z : Fin d → ℤ) (f : CoeffField d → E) (hf : MeasureTheory.AEStronglyMeasurable f P) : ∫ (a : CoeffField d), f (translateByInt z a) ∂P = ∫ (a : CoeffField d), f a ∂P

theorem HCPolySupport.localTestObservable_eq_of_ae_eq {d : ℕ} {a b : CoeffField d} (h : a =ᵐ[MeasureTheory.volume] b) (e e' : Vec d) (φ : Vec d → ℝ) : localTestObservable e e' φ a = localTestObservable e e' φ b

theorem HCPolySupport.localFiniteTestObservable_eq_of_ae_eq {d : ℕ} {ι : Type} {a b : CoeffField d} (h : a =ᵐ[MeasureTheory.volume] b) (I : Finset ι) (e e' : ι → Vec d) (φ : ι → Vec d → ℝ) : localFiniteTestObservable I e e' φ a = localFiniteTestObservable I e e' φ b

theorem HCPolySupport.mem_iff_of_measurableSet_pointwiseLocalSigma_of_pointwiseAgreementOn {d : ℕ} {U : Set (Vec d)} {s : Set (CoeffField d)} (hs : MeasurableSet s) {a b : CoeffField d} (hab : PointwiseAgreementOn U a b) : a ∈ s ↔ b ∈ s

theorem HCPolySupport.mem_iff_of_measurableSet_localSigma_of_localAgreementOn {d : ℕ} {U : Set (Vec d)} {s : Set (CoeffField d)} (hs : MeasurableSet s) {a b : CoeffField d} (hab : LocalAgreementOn U a b) : a ∈ s ↔ b ∈ s

theorem HCPolySupport.mem_iff_of_measurableSet_pointwiseLocalSigma_of_eqOn {d : ℕ} {U : Set (Vec d)} {s : Set (CoeffField d)} (hs : MeasurableSet s) {a b : CoeffField d} (h : ∀ x ∈ U, a x = b x) : a ∈ s ↔ b ∈ s

theorem HCPolySupport.mem_iff_of_measurableSet_localSigma_of_eqOn {d : ℕ} {U : Set (Vec d)} {s : Set (CoeffField d)} (hs : MeasurableSet s) {a b : CoeffField d} (h : ∀ x ∈ U, a x = b x) : a ∈ s ↔ b ∈ s

def HCPolySupport.IsPointwiseLocalSigmaMeasurableOn {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : Ω → CoeffField d) (U : Set (Vec d)) : Prop

A sample-space-valued coefficient field is pointwise-locally measurable on U if it is measurable with codomain PointwiseLocalSigma U.

Equations

• HCPolySupport.IsPointwiseLocalSigmaMeasurableOn A U = Measurable A

@[reducible, inline]

abbrev HCPolySupport.IsLocalSigmaMeasurableOn {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : Ω → CoeffField d) (U : Set (Vec d)) : Prop

Compatibility name for IsPointwiseLocalSigmaMeasurableOn.

Equations

• HCPolySupport.IsLocalSigmaMeasurableOn A U = HCPolySupport.IsPointwiseLocalSigmaMeasurableOn A U

def HCPolySupport.IsRestrictionSigmaMeasurableOn {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (A : Ω → CoeffField d) (U : Set (Vec d)) : Prop

A sample-space-valued coefficient field is restriction-measurable on U if it is measurable with codomain RestrictionSigma U.

Equations

• HCPolySupport.IsRestrictionSigmaMeasurableOn A U = Measurable A

theorem HCPolySupport.AreUnitSeparated.symm {d : ℕ} {U V : Set (Vec d)} (hUV : AreUnitSeparated U V) : AreUnitSeparated V U

theorem HCPolySupport.areUnitSeparated_cubeSet_of_ne_of_mem_descendantsAtScaleColorClass {d : ℕ} {Q R S : TriadicCube d} {k : ℤ} {c : CubeColor d} (hk : 0 ≤ k) (hR : R ∈ descendantsAtScaleColorClass Q k c) (hS : S ∈ descendantsAtScaleColorClass Q k c) (hneq : R ≠ S) : AreUnitSeparated (cubeSet R) (cubeSet S)

theorem HCPolySupport.pairwise_areUnitSeparated_cubeSet_descendantsAtScaleColorClass {d : ℕ} (Q : TriadicCube d) {k : ℤ} (hk : 0 ≤ k) (c : CubeColor d) : (↑(descendantsAtScaleColorClass Q k c)).Pairwise fun (R S : TriadicCube d) => AreUnitSeparated (cubeSet R) (cubeSet S)

theorem HCPolySupport.pairwise_areUnitSeparated_cubeSet_subtype_descendantsAtScaleColorClass {d : ℕ} (Q : TriadicCube d) {k : ℤ} (hk : 0 ≤ k) (c : CubeColor d) : Pairwise fun (R S : ↥(descendantsAtScaleColorClass Q k c)) => AreUnitSeparated (cubeSet ↑R) (cubeSet ↑S)

theorem HCPolySupport.areUnitSeparated_cubeSet_of_ne_of_mem_descendantsAtScaleScaleColorClass {d : ℕ} {Q R S : TriadicCube d} {k : ℤ} {c : ScaleColor d k} (hR : R ∈ descendantsAtScaleScaleColorClass Q k c) (hS : S ∈ descendantsAtScaleScaleColorClass Q k c) (hneq : R ≠ S) : AreUnitSeparated (cubeSet R) (cubeSet S)

theorem HCPolySupport.pairwise_areUnitSeparated_cubeSet_descendantsAtScaleScaleColorClass {d : ℕ} (Q : TriadicCube d) {k : ℤ} (c : ScaleColor d k) : (↑(descendantsAtScaleScaleColorClass Q k c)).Pairwise fun (R S : TriadicCube d) => AreUnitSeparated (cubeSet R) (cubeSet S)

theorem HCPolySupport.pairwise_areUnitSeparated_cubeSet_subtype_descendantsAtScaleScaleColorClass {d : ℕ} (Q : TriadicCube d) {k : ℤ} (c : ScaleColor d k) : Pairwise fun (R S : ↥(descendantsAtScaleScaleColorClass Q k c)) => AreUnitSeparated (cubeSet ↑R) (cubeSet ↑S)

theorem HCPolySupport.areUnitSeparated_biUnion_right {d : ℕ} {ι : Type u_1} {U : Set (Vec d)} {V : ι → Set (Vec d)} {s : Finset ι} (h : ∀ i ∈ s, AreUnitSeparated U (V i)) : AreUnitSeparated U (⋃ i ∈ s, V i)

theorem HCPolySupport.measurableSet_biInter_restrictionSigma_biUnion {d : ℕ} {ι : Type u_1} {U : ι → Set (Vec d)} {f : ι → Set (CoeffField d)} {s : Finset ι} (hf : ∀ i ∈ s, MeasurableSet (f i)) : MeasurableSet (⋂ i ∈ s, f i)

theorem HCPolySupport.iIndep_restrictionSigma_of_isRestrictionUnitRangeDependent {d : ℕ} {ι : Type u_1} {P : MeasureTheory.Measure (CoeffField d)} [MeasureTheory.IsProbabilityMeasure P] {U : ι → Set (Vec d)} (hP : IsRestrictionUnitRangeDependent P) (hsep : Pairwise fun (i j : ι) => AreUnitSeparated (U i) (U j)) : ProbabilityTheory.iIndep (fun (i : ι) => RestrictionSigma (U i)) P

theorem HCPolySupport.iIndep_restrictionSigma_descendantsAtScaleColorClass_of_isRestrictionUnitRangeDependent {d : ℕ} {Q : TriadicCube d} {k : ℤ} (hk : 0 ≤ k) {c : CubeColor d} {P : MeasureTheory.Measure (CoeffField d)} [MeasureTheory.IsProbabilityMeasure P] (hP : IsRestrictionUnitRangeDependent P) : ProbabilityTheory.iIndep (fun (R : ↥(descendantsAtScaleColorClass Q k c)) => RestrictionSigma (cubeSet ↑R)) P

theorem HCPolySupport.iIndep_restrictionSigma_descendantsAtScaleScaleColorClass_of_isRestrictionUnitRangeDependent {d : ℕ} {Q : TriadicCube d} {k : ℤ} {c : ScaleColor d k} {P : MeasureTheory.Measure (CoeffField d)} [MeasureTheory.IsProbabilityMeasure P] (hP : IsRestrictionUnitRangeDependent P) : ProbabilityTheory.iIndep (fun (R : ↥(descendantsAtScaleScaleColorClass Q k c)) => RestrictionSigma (cubeSet ↑R)) P

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

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

Compatibility spelling for the pointwise-local measurability theorem.