Coarse-graining support: Support.Probability.RandomField

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

@[instance_reducible]

instance HCPolySupport.instMeasurableSpaceVec (d : ℕ) : MeasurableSpace (Vec d)

Equations

• HCPolySupport.instMeasurableSpaceVec d = id inferInstance

@[instance_reducible]

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

Equations

• HCPolySupport.instMeasurableSpaceMat d = id inferInstance

def HCPolySupport.IsLocallyUniformlyElliptic {d : ℕ} (a : CoeffField d) : Prop

Uniform ellipticity on every closed ball of radius at least one, with positive bounds ε and ε⁻¹ allowed to depend on the ball.

Equations

• HCPolySupport.IsLocallyUniformlyElliptic a = ∀ (R : ℝ), 1 ≤ R → ∃ (ε : ℝ), 0 < ε ∧ ε ≤ 1 ∧ HCPolySupport.IsEllipticFieldOn ε ε⁻¹ (Metric.closedBall 0 R) a

noncomputable def HCPolySupport.localTestObservable {d : ℕ} (e e' : Vec d) (φ : Vec d → ℝ) (a : CoeffField d) : ℝ

The Lebesgue integral of the coefficient pairing e'·a e against φ.

Equations

• HCPolySupport.localTestObservable e e' φ a = ∫ (x : HCPolySupport.Vec d), HCPolySupport.vecDot e' (HCPolySupport.matVecMul (a x) e) * φ x

noncomputable def HCPolySupport.localFiniteTestObservable {d : ℕ} {ι : Type} (s : Finset ι) (e e' : ι → Vec d) (φ : ι → Vec d → ℝ) (a : CoeffField d) : ℝ

A finite local test observable, with the finite sum kept inside the integral. This avoids using additivity of the Bochner integral for arbitrary coefficient fields.

Equations

• HCPolySupport.localFiniteTestObservable s e e' φ a = ∫ (x : HCPolySupport.Vec d), ∑ k ∈ s, HCPolySupport.vecDot (e' k) (HCPolySupport.matVecMul (a x) (e k)) * φ k x

def HCPolySupport.PointwiseAgreementOn {d : ℕ} (U : Set (Vec d)) (a b : CoeffField d) : Prop

Two coefficient fields agree on all points of an observation set. This is the pointwise locality relation retained by the restriction engineering lane.

Equations

• HCPolySupport.PointwiseAgreementOn U a b = ∀ x ∈ U, a x = b x

@[reducible, inline]

abbrev HCPolySupport.LocalAgreementOn {d : ℕ} (U : Set (Vec d)) (a b : CoeffField d) : Prop

Compatibility name for PointwiseAgreementOn.

Equations

• HCPolySupport.LocalAgreementOn U a b = HCPolySupport.PointwiseAgreementOn U a b

def HCPolySupport.IsPointwiseLocalEvent {d : ℕ} (U : Set (Vec d)) (s : Set (CoeffField d)) : Prop

A coefficient-field event determined by the values of the field on U. This is pointwise-local information in the retained restriction lane.

Equations

• HCPolySupport.IsPointwiseLocalEvent U s = ∀ ⦃a b : HCPolySupport.CoeffField d⦄, HCPolySupport.PointwiseAgreementOn U a b → (a ∈ s ↔ b ∈ s)

@[reducible, inline]

abbrev HCPolySupport.IsLocalEvent {d : ℕ} (U : Set (Vec d)) (s : Set (CoeffField d)) : Prop

Compatibility name for IsPointwiseLocalEvent.

Equations

• HCPolySupport.IsLocalEvent U s = HCPolySupport.IsPointwiseLocalEvent U s

@[reducible, inline]

abbrev HCPolySupport.PointwiseLocalSigma {d : ℕ} (U : Set (Vec d)) : MeasurableSpace (CoeffField d)

The sigma-algebra generated by pointwise-local events on U. It belongs to the retained restriction engineering lane and remains distinct from the restriction-comap sigma-algebra RestrictionSigma U.

Equations

• HCPolySupport.PointwiseLocalSigma U = MeasurableSpace.generateFrom {s : Set (HCPolySupport.CoeffField d) | HCPolySupport.IsPointwiseLocalEvent U s}

@[reducible, inline]

abbrev HCPolySupport.LocalSigma {d : ℕ} (U : Set (Vec d)) : MeasurableSpace (CoeffField d)

Compatibility name for PointwiseLocalSigma.

Equations

• HCPolySupport.LocalSigma U = HCPolySupport.PointwiseLocalSigma U

@[reducible, inline]

abbrev HCPolySupport.pointwiseCoeffFieldMeasurableSpace (d : ℕ) : MeasurableSpace (CoeffField d)

The pointwise (product) σ-algebra on coefficient fields: the smallest σ-algebra making every coordinate evaluation a ↦ a x measurable.

Equations

• HCPolySupport.pointwiseCoeffFieldMeasurableSpace d = MeasurableSpace.pi

@[reducible, inline]

abbrev HCPolySupport.boundedLocalCoeffFieldMeasurableSpace (d : ℕ) : MeasurableSpace (CoeffField d)

The bounded-local σ-algebra on coefficient fields: local events over bounded observation sets. This deliberately excludes unbounded regions such as Set.univ; including LocalSigma Set.univ would make the ambient coefficient space discrete and would rule out genuine infinite-product random fields.

Equations

• HCPolySupport.boundedLocalCoeffFieldMeasurableSpace d = ⨆ (U : { U : Set (HCPolySupport.Vec d) // Bornology.IsBounded U }), HCPolySupport.LocalSigma ↑U

@[instance_reducible]

instance HCPolySupport.instMeasurableSpaceCoeffField (d : ℕ) : MeasurableSpace (CoeffField d)

The ambient σ-algebra on coefficient fields: the pointwise σ-algebra joined with bounded local coefficient-field information. This keeps every coordinate evaluation measurable while making the bounded local events used by compact tests and triadic cubes measurable.

Equations

• HCPolySupport.instMeasurableSpaceCoeffField d = HCPolySupport.pointwiseCoeffFieldMeasurableSpace d ⊔ HCPolySupport.boundedLocalCoeffFieldMeasurableSpace d

@[reducible, inline]

noncomputable abbrev HCPolySupport.RestrictionSigma {d : ℕ} (U : Set (Vec d)) : MeasurableSpace (CoeffField d)

The sigma-algebra on coefficient space induced by restricting the field to the deterministic set U. This is the measurable local sigma algebra used for unit-range dependence of genuine random fields.

Equations

• HCPolySupport.RestrictionSigma U = MeasurableSpace.comap (HCPolySupport.restrictCoeffField U) inferInstance

theorem HCPolySupport.pointwise_le_coeffField (d : ℕ) : pointwiseCoeffFieldMeasurableSpace d ≤ instMeasurableSpaceCoeffField d

theorem HCPolySupport.localSigma_le_coeffField_of_isBounded {d : ℕ} {U : Set (Vec d)} (hU : Bornology.IsBounded U) : LocalSigma U ≤ instMeasurableSpaceCoeffField d

The ambient→bounded-local bridge: every local event over a bounded observation set is ambient-measurable.

theorem HCPolySupport.measurable_coeffField_eval {d : ℕ} (y : Vec d) : Measurable fun (a : CoeffField d) => a y

Coordinate evaluation is ambient-measurable (it factors through the pointwise σ-algebra).

theorem HCPolySupport.measurable_coeffField_to_ambient {d : ℕ} {f : CoeffField d → CoeffField d} (hpt : Measurable f) (hloc : ∀ (U : Set (Vec d)), Bornology.IsBounded U → Measurable f) : Measurable f

A self-map of coefficient fields is ambient-measurable if it is measurable into the pointwise σ-algebra and into every local sigma algebra.

theorem HCPolySupport.measurable_to_coeffField_ambient {α : Type u_1} [mα : MeasurableSpace α] {d : ℕ} {f : α → CoeffField d} (hpt : Measurable f) (hloc : ∀ (U : Set (Vec d)), Bornology.IsBounded U → Measurable f) : Measurable f

A map from an arbitrary measurable space into coefficient fields is ambient-measurable if it is pointwise-measurable and measurable into every bounded local sigma algebra.

theorem HCPolySupport.localTestObservable_eq_localFiniteTestObservable {d : ℕ} (e e' : Vec d) (φ : Vec d → ℝ) : localTestObservable e e' φ = localFiniteTestObservable {()} (fun (x : Unit) => e) (fun (x : Unit) => e') fun (x : Unit) => φ

theorem HCPolySupport.measurable_localFiniteTestObservable_localSigma {d : ℕ} {U : Set (Vec d)} {ι : Type} {I : Finset ι} {e e' : ι → Vec d} {φ : ι → Vec d → ℝ} (hφ_support : ∀ k ∈ I, Function.support (φ k) ⊆ U) : Measurable (localFiniteTestObservable I e e' φ)

A finite test observable is measurable for the local sigma algebra on any set containing the supports of all scalar probes in the finite sum.

theorem HCPolySupport.PointwiseAgreementOn.mono {d : ℕ} {U V : Set (Vec d)} {a b : CoeffField d} (hUV : U ⊆ V) (h : PointwiseAgreementOn V a b) : PointwiseAgreementOn U a b

theorem HCPolySupport.LocalAgreementOn.mono {d : ℕ} {U V : Set (Vec d)} {a b : CoeffField d} (hUV : U ⊆ V) (h : LocalAgreementOn V a b) : LocalAgreementOn U a b

Compatibility spelling for PointwiseAgreementOn.mono.

theorem HCPolySupport.isBounded_image_of_continuous_vec {d : ℕ} {f : Vec d → Vec d} (hf : Continuous f) {U : Set (Vec d)} (hU : Bornology.IsBounded U) : Bornology.IsBounded (f '' U)

theorem HCPolySupport.measurable_localSigma_of_local {d : ℕ} {T : CoeffField d → CoeffField d} (h : ∀ (U : Set (Vec d)), Bornology.IsBounded U → ∃ (V : Set (Vec d)), Bornology.IsBounded V ∧ ∀ ⦃a b : CoeffField d⦄, LocalAgreementOn V a b → LocalAgreementOn U (T a) (T b)) (U : Set (Vec d)) (hU : Bornology.IsBounded U) : Measurable T

A self-map T of coefficient fields is measurable into LocalSigma U when its values on U are determined by the input field on some source region.

theorem HCPolySupport.measurable_localTestObservable_localSigma {d : ℕ} {U : Set (Vec d)} (e e' : Vec d) {φ : Vec d → ℝ} (_hφ_cont : ContDiff ℝ (↑⊤) φ) (_hφ_compact : HasCompactSupport φ) (hφ_support : tsupport φ ⊆ U) : Measurable (localTestObservable e e' φ)

localTestObservable e e' φ is LocalSigma U-measurable when tsupport φ ⊆ U.

theorem HCPolySupport.preimage_localTestObservable_mem_localSigma {d : ℕ} {U : Set (Vec d)} (e e' : Vec d) {φ : Vec d → ℝ} (hφ_cont : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_support : tsupport φ ⊆ U) {t : Set ℝ} (ht : MeasurableSet t) : MeasurableSet (localTestObservable e e' φ ⁻¹' t)

The generator set localTestObservable e e' φ ⁻¹' t is LocalSigma U-measurable.

theorem HCPolySupport.measurable_localTestObservable {d : ℕ} (e e' : Vec d) {φ : Vec d → ℝ} (hφ_cont : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) : Measurable (localTestObservable e e' φ)

localTestObservable e e' φ is ambient-measurable.

def HCPolySupport.translateByInt {d : ℕ} (z : Fin d → ℤ) : CoeffField d → CoeffField d

Translation of coefficient fields by the real vector associated with an integer lattice vector.

Equations

• HCPolySupport.translateByInt z = HCPolySupport.translateCoeffField (HCPolySupport.intVecToRealVec z)

def HCPolySupport.IsStationary {d : ℕ} (P : MeasureTheory.Measure (CoeffField d)) : Prop

Invariance of the coefficient-field measure under every integer translation.

Equations

• HCPolySupport.IsStationary P = ∀ (z : Fin d → ℤ), MeasureTheory.Measure.map (HCPolySupport.translateByInt z) P = P

def HCPolySupport.AreUnitSeparated {d : ℕ} (U V : Set (Vec d)) : Prop

Every point of U is at distance at least one from every point of V.

Equations

• HCPolySupport.AreUnitSeparated U V = ∀ ⦃x y : HCPolySupport.Vec d⦄, x ∈ U → y ∈ V → 1 ≤ dist x y

def HCPolySupport.IsRestrictionUnitRangeDependent {d : ℕ} (P : MeasureTheory.Measure (CoeffField d)) : Prop

Independence of restriction sigma-algebras for every pair of unit-separated regions.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev HCPolySupport.IsUnitRangeDependent {d : ℕ} (P : MeasureTheory.Measure (CoeffField d)) : Prop

Compatibility name for IsRestrictionUnitRangeDependent.

Equations

• HCPolySupport.IsUnitRangeDependent P = HCPolySupport.IsRestrictionUnitRangeDependent P

def HCPolySupport.rotateCoeffField {d : ℕ} (R : Mat d) (a : CoeffField d) : CoeffField d

The transformed field x ↦ Rᵀ * a (R x) * R.

Equations

• HCPolySupport.rotateCoeffField R a x = HCPolySupport.matTranspose R * a (HCPolySupport.matVecMul R x) * R

def HCPolySupport.adjointCoeffField {d : ℕ} (a : CoeffField d) : CoeffField d

The coefficient field obtained by transposing each matrix.

Equations

• HCPolySupport.adjointCoeffField a x = HCPolySupport.matTranspose (a x)

theorem HCPolySupport.measurable_rotateCoeffField {d : ℕ} (R : Mat d) (hR : IsSignedPermutationMatrix R) : Measurable (rotateCoeffField R)

theorem HCPolySupport.localTestObservable_adjoint {d : ℕ} (e e' : Vec d) (φ : Vec d → ℝ) (a : CoeffField d) : localTestObservable e e' φ (adjointCoeffField a) = localTestObservable e' e φ a

The adjoint pulls a local test back to the test with e, e' swapped (same test function, same region).

theorem HCPolySupport.localFiniteTestObservable_adjoint {d : ℕ} {ι : Type} (I : Finset ι) (e e' : ι → Vec d) (φ : ι → Vec d → ℝ) (a : CoeffField d) : localFiniteTestObservable I e e' φ (adjointCoeffField a) = localFiniteTestObservable I e' e φ a

theorem HCPolySupport.measurable_adjointCoeffField {d : ℕ} : Measurable adjointCoeffField

def HCPolySupport.IsIsotropicInLaw {d : ℕ} (P : MeasureTheory.Measure (CoeffField d)) : Prop

Invariance of the coefficient-field measure under signed permutation transformations.

Equations

• HCPolySupport.IsIsotropicInLaw P = ∀ (R : HCPolySupport.Mat d), HCPolySupport.IsSignedPermutationMatrix R → MeasureTheory.Measure.map (HCPolySupport.rotateCoeffField R) P = P

def HCPolySupport.IsAdjointInvariantInLaw {d : ℕ} (P : MeasureTheory.Measure (CoeffField d)) : Prop

Invariance of the coefficient-field measure under matrix transposition.

Equations

• HCPolySupport.IsAdjointInvariantInLaw P = (MeasureTheory.Measure.map HCPolySupport.adjointCoeffField P = P)

theorem HCPolySupport.integral_comp_eq_of_map_eq {α : Type u_1} [MeasurableSpace α] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {P : MeasureTheory.Measure α} {f : α → α} (hf : Measurable f) (hmap : MeasureTheory.Measure.map f P = P) (g : α → E) (hg : MeasureTheory.AEStronglyMeasurable g P) : ∫ (a : α), g (f a) ∂P = ∫ (a : α), g a ∂P

theorem HCPolySupport.isSignedPermutationMatrix_signFlipMatrix {d : ℕ} (i : Fin d) : IsSignedPermutationMatrix (signFlipMatrix i)

theorem HCPolySupport.isSignedPermutationMatrix_swap {d : ℕ} (i j : Fin d) : IsSignedPermutationMatrix (Matrix.swap ℝ i j)

theorem HCPolySupport.IsIsotropicInLaw.map_rotateCoeffField_signFlipMatrix {d : ℕ} {P : MeasureTheory.Measure (CoeffField d)} (hP : IsIsotropicInLaw P) (i : Fin d) : MeasureTheory.Measure.map (rotateCoeffField (signFlipMatrix i)) P = P

theorem HCPolySupport.IsIsotropicInLaw.map_rotateCoeffField_swap {d : ℕ} {P : MeasureTheory.Measure (CoeffField d)} (hP : IsIsotropicInLaw P) (i j : Fin d) : MeasureTheory.Measure.map (rotateCoeffField (Matrix.swap ℝ i j)) P = P

theorem HCPolySupport.integral_comp_rotateCoeffField_eq_of_isIsotropicInLaw {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {P : MeasureTheory.Measure (CoeffField d)} (hP : IsIsotropicInLaw P) {R : Mat d} (hR : IsSignedPermutationMatrix R) (f : CoeffField d → E) (hf : MeasureTheory.AEStronglyMeasurable f P) : ∫ (a : CoeffField d), f (rotateCoeffField R a) ∂P = ∫ (a : CoeffField d), f a ∂P

theorem HCPolySupport.integrable_comp_rotateCoeffField_of_isIsotropicInLaw {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {P : MeasureTheory.Measure (CoeffField d)} (hP : IsIsotropicInLaw P) {R : Mat d} (hR : IsSignedPermutationMatrix R) (f : CoeffField d → E) (hf : MeasureTheory.Integrable f P) : MeasureTheory.Integrable (fun (a : CoeffField d) => f (rotateCoeffField R a)) P

theorem HCPolySupport.integral_comp_adjointCoeffField_eq_of_isAdjointInvariantInLaw {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {P : MeasureTheory.Measure (CoeffField d)} (hP : IsAdjointInvariantInLaw P) (f : CoeffField d → E) (hf : MeasureTheory.AEStronglyMeasurable f P) : ∫ (a : CoeffField d), f (adjointCoeffField a) ∂P = ∫ (a : CoeffField d), f a ∂P

theorem HCPolySupport.integrable_comp_adjointCoeffField_of_isAdjointInvariantInLaw {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {P : MeasureTheory.Measure (CoeffField d)} (hP : IsAdjointInvariantInLaw P) (f : CoeffField d → E) (hf : MeasureTheory.Integrable f P) : MeasureTheory.Integrable (fun (a : CoeffField d) => f (adjointCoeffField a)) P

def HCPolySupport.IsRestrictionLocalObservable {β : Type u_1} {d : ℕ} (U : Set (Vec d)) (X : CoeffField d → β) : Prop

The observable takes equal values on coefficient fields agreeing pointwise on U.

Equations

• HCPolySupport.IsRestrictionLocalObservable U X = ∀ ⦃a₁ a₂ : HCPolySupport.CoeffField d⦄, (∀ x ∈ U, a₁ x = a₂ x) → X a₁ = X a₂

@[reducible, inline]

abbrev HCPolySupport.IsLocalObservable {β : Type u_1} {d : ℕ} (U : Set (Vec d)) (X : CoeffField d → β) : Prop

Compatibility name for IsRestrictionLocalObservable.

Equations

• HCPolySupport.IsLocalObservable U X = HCPolySupport.IsRestrictionLocalObservable U X

def HCPolySupport.IsTranslationCovariant {β : Type u_1} {d : ℕ} (X : Set (Vec d) → CoeffField d → β) : Prop

Translating the region gives the same observable value as translating the coefficient field.

Equations

• One or more equations did not get rendered due to their size.