Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch04.SourceMu

Coarse-graining support: Support.Book.Ch04.SourceMu #

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

Source-local coarse-grained energy #

The exact coarse-source carrier has deterministic AEE-slice coverage on each triadic cube. On every slice, the coarse-to-regular integral realization lets the carrier Mu engine consume the source's smooth integral observables. A countable liftCover then gives an exactly source-local, pointwise equal version of Mu.

source
theorem HCPolySupport.Book.Ch04.isSourceLocalRandomVariable_Mu_cubeSet {d : ℕ} (Q : TriadicCube d) (P0 : BlockVec d) :
IsSourceLocalRandomVariable (cubeSet Q) ⋯ fun (a : Source.Coarse.Carrier d) => Mu (cubeSet Q) P0 ↑a

The exact coarse-source energy on a triadic cube is source-local. Its proof uses only deterministic source-carrier slice coverage.

source
noncomputable def HCPolySupport.Book.Ch04.SourceObservable.mu {d : ℕ} (Q : TriadicCube d) (P0 : BlockVec d) :
SourceObservable d (cubeSet Q) ℝ

The coarse-grained energy on a triadic cube, bundled as an exact source-local observable.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem HCPolySupport.Book.Ch04.SourceObservable.mu_apply {d : ℕ} (Q : TriadicCube d) (P0 : BlockVec d) (a : Source.Coarse.Carrier d) :
    (mu Q P0).toFun a = Mu (cubeSet Q) P0 ↑a