Coarse-graining support: Support.Probability.Source.Coarse.Laws #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Every point of U is at Euclidean distance at least one from every point of V.
Equations
- HCPolySupport.Source.Coarse.EuclideanUnitSeparated U V = ∀ ⦃x y : HCPolySupport.Vec d⦄, x ∈ U → y ∈ V → 1 ≤ HCPolySupport.euclideanDist x y
Instances For
The coefficient law is invariant under every integer coordinate translation.
Equations
- HCPolySupport.Source.Coarse.IsStationary P = ∀ (z : Fin d → ℤ), MeasureTheory.Measure.map (HCPolySupport.Source.Coarse.Carrier.translate z) P = P
Instances For
def
HCPolySupport.Source.Coarse.IsUnitRangeDependent
{d : ℕ}
(P : MeasureTheory.Measure (Carrier d))
:
The local sigma algebras of measurable sets separated by Euclidean distance at least one are independent under the coefficient law.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
HCPolySupport.Source.Coarse.IsIsotropicAndAdjointInvariant
{d : ℕ}
(P : MeasureTheory.Measure (Carrier d))
:
The coefficient law is invariant under signed coordinate permutations and under taking the adjoint.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HCPolySupport.Source.Coarse.iIndep_localSigma_of_pairwise_euclideanUnitSeparated
{d : ℕ}
{ι : Type u_1}
(P : MeasureTheory.Measure (Carrier d))
[MeasureTheory.IsProbabilityMeasure P]
(hP2 : IsUnitRangeDependent P)
{U : ι → Set (Vec d)}
(hU : ∀ (i : ι), MeasurableSet (U i))
(hsep : Pairwise fun (i j : ι) => EuclideanUnitSeparated (U i) (U j))
:
ProbabilityTheory.iIndep (fun (i : ι) => localSigma (U i) ⋯) P
theorem
HCPolySupport.Source.Coarse.iIndepFun_of_localObservable_of_pairwise_euclideanUnitSeparated
{d : ℕ}
{ι : Type u_1}
(P : MeasureTheory.Measure (Carrier d))
[MeasureTheory.IsProbabilityMeasure P]
(hP2 : IsUnitRangeDependent P)
{U : ι → Set (Vec d)}
(hU : ∀ (i : ι), MeasurableSet (U i))
{β : ι → Type u_2}
[(i : ι) → MeasurableSpace (β i)]
{X : (i : ι) → Carrier d → β i}
(hX : ∀ (i : ι), IsLocalObservable (U i) ⋯ (X i))
(hsep : Pairwise fun (i j : ι) => EuclideanUnitSeparated (U i) (U j))
: