Coarse-graining support: Support.Book.Ch02.CoeffRestriction

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

noncomputable def HCPolySupport.Book.Ch02.CoeffOn.restrictToSubcube {d : ℕ} {Q R : TriadicCube d} (a : CoeffOn (cubeDomain Q)) (hRQ : openCubeSet R ⊆ openCubeSet Q) : CoeffOn (cubeDomain R)

The literal restriction of one coefficient representative to a subcube.

Unlike a coefficient-family compatibility witness, this keeps the same raw representative and transports only its a.e. data to the smaller cube.

Equations

• a.restrictToSubcube hRQ = { toCoeffField := a.toCoeffField, lam := a.lam, Lam := a.Lam, lam_pos := ⋯, lam_le_Lam := ⋯, aeStronglyMeasurable := ⋯, aeElliptic := ⋯ }

@[simp]

theorem HCPolySupport.Book.Ch02.CoeffOn.restrictToSubcube_toCoeffField {d : ℕ} {Q R : TriadicCube d} (a : CoeffOn (cubeDomain Q)) (hRQ : openCubeSet R ⊆ openCubeSet Q) : (a.restrictToSubcube hRQ).toCoeffField = a.toCoeffField

theorem HCPolySupport.Book.Ch02.CoeffOn.restrictToSubcube_restrictsTo {d : ℕ} {Q R : TriadicCube d} (a : CoeffOn (cubeDomain Q)) (hRQ : openCubeSet R ⊆ openCubeSet Q) : a.RestrictsTo (a.restrictToSubcube hRQ)

theorem HCPolySupport.Book.Ch02.CoeffOn.restrictToSubcube_trans_aeeq {d : ℕ} {Q R S : TriadicCube d} (a : CoeffOn (cubeDomain Q)) (hRQ : openCubeSet R ⊆ openCubeSet Q) (hSR : openCubeSet S ⊆ openCubeSet R) : ((a.restrictToSubcube hRQ).restrictToSubcube hSR).AEEq (a.restrictToSubcube ⋯)