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

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

Public dilation package after the Chapter 2.5 definitions

This file freezes the note-facing dilation vocabulary used by later Chapter 3 arguments. The statements are deliberately phrased with the public CoeffOn and TriadicCoeffFamily interfaces: coefficient representatives are compared only almost everywhere on the dilated cube.

The geometric convention is that dilation by 3^k sends a triadic cube Q = 3^m (z + [-1/2,1/2]^d) to the cube with the same integer index and scale m + k.

noncomputable def HCPolySupport.Book.Ch02.triadicDilationFactor (k : ℤ) : ℝ

The positive dilation factor 3^k.

Equations

• HCPolySupport.Book.Ch02.triadicDilationFactor k = 3 ^ k

theorem HCPolySupport.Book.Ch02.triadicDilationFactor_pos (k : ℤ) : 0 < triadicDilationFactor k

theorem HCPolySupport.Book.Ch02.triadicDilationFactor_ne_zero (k : ℤ) : triadicDilationFactor k ≠ 0

noncomputable def HCPolySupport.Book.Ch02.dilateVec {d : ℕ} (k : ℤ) (x : Vec d) : Vec d

Dilation of a vector by 3^k.

Equations

• HCPolySupport.Book.Ch02.dilateVec k x = HCPolySupport.Book.Ch02.triadicDilationFactor k • x

noncomputable def HCPolySupport.Book.Ch02.undilateVec {d : ℕ} (k : ℤ) (x : Vec d) : Vec d

Pullback map associated with dilation by 3^k.

Equations

• HCPolySupport.Book.Ch02.undilateVec k x = (HCPolySupport.Book.Ch02.triadicDilationFactor k)⁻¹ • x

noncomputable def HCPolySupport.Book.Ch02.dilateCoeffField {d : ℕ} (k : ℤ) (a : CoeffField d) : CoeffField d

Representative-level pullback of a coefficient field under dilation by 3^k. Public coefficient objects use CoeffOn.IsCubeDilation below, which records this relation only a.e. on the target cube.

Equations

• HCPolySupport.Book.Ch02.dilateCoeffField k a x = a (HCPolySupport.Book.Ch02.undilateVec k x)

@[simp]

theorem HCPolySupport.Book.Ch02.dilateCoeffField_apply {d : ℕ} (k : ℤ) (a : CoeffField d) (x : Vec d) : dilateCoeffField k a x = a (undilateVec k x)

def HCPolySupport.Book.Ch02.dilateCube {d : ℕ} (k : ℤ) (Q : TriadicCube d) : TriadicCube d

Dilation of a triadic cube by 3^k: the scale is shifted by k, while the integer index is unchanged.

Equations

• HCPolySupport.Book.Ch02.dilateCube k Q = { scale := Q.scale + k, index := Q.index }

@[simp]

theorem HCPolySupport.Book.Ch02.dilateCube_scale {d : ℕ} (k : ℤ) (Q : TriadicCube d) : (dilateCube k Q).scale = Q.scale + k

@[simp]

theorem HCPolySupport.Book.Ch02.dilateCube_index {d : ℕ} (k : ℤ) (Q : TriadicCube d) : (dilateCube k Q).index = Q.index

theorem HCPolySupport.Book.Ch02.cubeScaleFactor_dilateCube {d : ℕ} (k : ℤ) (Q : TriadicCube d) : cubeScaleFactor (dilateCube k Q) = triadicDilationFactor k * cubeScaleFactor Q

theorem HCPolySupport.Book.Ch02.openCubeSet_dilateCube {d : ℕ} (k : ℤ) (Q : TriadicCube d) : openCubeSet (dilateCube k Q) = triadicDilationFactor k • openCubeSet Q

theorem HCPolySupport.Book.Ch02.IsSolenoidalOn.dilateSet {d : ℕ} {U V : Set (Vec d)} {r : ℝ} (hr : 0 < r) (hV : V = r • U) {g : Vec d → Vec d} (hg : IsSolenoidalOn U g) : IsSolenoidalOn V fun (x : Vec d) => g (r⁻¹ • x)

theorem HCPolySupport.Book.Ch02.IsSolenoidalOn.congr_ae {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hfg : f =ᵐ[volumeMeasureOn U] g) (hf : IsSolenoidalOn U f) : IsSolenoidalOn U g

theorem HCPolySupport.Book.Ch02.IsSolenoidalOn.undilateSet {d : ℕ} {U V : Set (Vec d)} {r : ℝ} (hr : 0 < r) (hV : V = r • U) {g : Vec d → Vec d} (hg : IsSolenoidalOn V g) : IsSolenoidalOn U fun (x : Vec d) => g (r • x)

def HCPolySupport.Book.Ch02.CoeffOn.IsCubeDilation {d : ℕ} (k : ℤ) {Q : TriadicCube d} (a : CoeffOn (cubeDomain Q)) (b : CoeffOn (cubeDomain (dilateCube k Q))) : Prop

Public a.e. relation saying that b is the dilation by 3^k of a coefficient field a from Q to 3^k Q.

The lower/upper ellipticity constants are required to be the same named constants, and the representatives agree a.e. with the pullback a(3^{-k} ·) on the target cube.

Equations

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

theorem HCPolySupport.Book.Ch02.CoeffOn.IsCubeDilation.lam_eq {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (h : IsCubeDilation k a b) : b.lam = a.lam

theorem HCPolySupport.Book.Ch02.CoeffOn.IsCubeDilation.Lam_eq {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (h : IsCubeDilation k a b) : b.Lam = a.Lam

theorem HCPolySupport.Book.Ch02.CoeffOn.IsCubeDilation.coeff_ae_eq {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (h : IsCubeDilation k a b) : b.toCoeffField =ᵐ[volumeMeasureOn (openCubeSet (dilateCube k Q))] dilateCoeffField k a.toCoeffField

theorem HCPolySupport.Book.Ch02.CoeffOn.IsCubeDilation.transpose {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (h : IsCubeDilation k a b) : IsCubeDilation k a.transpose b.transpose

def HCPolySupport.Book.Ch02.TriadicCoeffFamily.IsDilation {d : ℕ} (k : ℤ) (a b : TriadicCoeffFamily d) : Prop

A triadic coefficient family b is the dilation by 3^k of a if, on every original cube Q, the coefficient object on the dilated cube 3^k Q is the public a.e. dilation of the coefficient object on Q.

Equations

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

structure HCPolySupport.Book.Ch02.Solution.IsCubeDilation {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) (u : Solution (cubeDomain Q) a) (v : Solution (cubeDomain (dilateCube k Q)) b) : Prop

Data expressing that v is the dilation of a Chapter 2 solution u from Q to 3^k Q.

The function is scaled by 3^k, so its gradient and flux pull back without an extra scalar. This is the normalization under which response quantities and coarse matrices are scale invariant.

• value_ae_eq : v.toH1.toFun =ᵐ[volumeMeasureOn (openCubeSet (dilateCube k Q))] fun (x : Vec d) => triadicDilationFactor k * u.toH1.toFun (undilateVec k x)
• grad_ae_eq : v.toH1.grad =ᵐ[volumeMeasureOn (openCubeSet (dilateCube k Q))] fun (x : Vec d) => u.toH1.grad (undilateVec k x)
• flux_ae_eq : (fun (x : Vec d) => matVecMul (b.toCoeffField x) (v.toH1.grad x)) =ᵐ[volumeMeasureOn (openCubeSet (dilateCube k Q))] fun (x : Vec d) => matVecMul (a.toCoeffField (undilateVec k x)) (u.toH1.grad (undilateVec k x))

structure HCPolySupport.Book.Ch02.Solution.CubeDilation {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) (u : Solution (cubeDomain Q) a) : Type

A packaged dilated solution. The toSolution field is the public lemma's conclusion: it is an actual solution of the dilated equation.

• toSolution : Solution (cubeDomain (dilateCube k Q)) b

  The solution on the dilated cube associated with the coefficient dilation.

• isDilation : IsCubeDilation hCoeff u self.toSolution

noncomputable def HCPolySupport.Book.Ch02.Solution.dilate {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) (u : Solution (cubeDomain Q) a) : CubeDilation hCoeff u

Dilation of a public Chapter 2 solution. The function is normalized as v(x) = 3^k u(3^{-k}x), so its weak gradient and flux are plain pullbacks.

Equations

• HCPolySupport.Book.Ch02.Solution.dilate hCoeff u = { toSolution := { toH1 := HCPolySupport.H1Function.dilateSet ⋯ ⋯ u.toH1, isHarmonic := ⋯ }, isDilation := ⋯ }

noncomputable def HCPolySupport.Book.Ch02.Solution.undilate {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) (v : Solution (cubeDomain (dilateCube k Q)) b) : Solution (cubeDomain Q) a

Inverse transport for a dilated public solution. This is used to show that dilation identifies the whole response value set, not just one chosen solution.

Equations

• HCPolySupport.Book.Ch02.Solution.undilate hCoeff v = { toH1 := HCPolySupport.H1Function.undilateSet ⋯ ⋯ v.toH1, isHarmonic := ⋯ }

theorem HCPolySupport.Book.Ch02.Solution.undilate_isDilation {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) (v : Solution (cubeDomain (dilateCube k Q)) b) : IsCubeDilation hCoeff (undilate hCoeff v) v

theorem HCPolySupport.Book.Ch02.Solution.CubeDilation.is_solution {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} {hCoeff : CoeffOn.IsCubeDilation k a b} {u : Solution (cubeDomain Q) a} (v : CubeDilation hCoeff u) : IsAHarmonicGradient b.toCoeffField (openCubeSet (dilateCube k Q)) v.toSolution.toH1.grad

theorem HCPolySupport.Book.Ch02.Solution.CubeDilation.grad_ae_eq {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} {hCoeff : CoeffOn.IsCubeDilation k a b} {u : Solution (cubeDomain Q) a} (v : CubeDilation hCoeff u) : v.toSolution.toH1.grad =ᵐ[volumeMeasureOn (openCubeSet (dilateCube k Q))] fun (x : Vec d) => u.toH1.grad (undilateVec k x)

theorem HCPolySupport.Book.Ch02.Solution.CubeDilation.flux_ae_eq {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} {hCoeff : CoeffOn.IsCubeDilation k a b} {u : Solution (cubeDomain Q) a} (v : CubeDilation hCoeff u) : (fun (x : Vec d) => matVecMul (b.toCoeffField x) (v.toSolution.toH1.grad x)) =ᵐ[volumeMeasureOn (openCubeSet (dilateCube k Q))] fun (x : Vec d) => matVecMul (a.toCoeffField (undilateVec k x)) (u.toH1.grad (undilateVec k x))

theorem HCPolySupport.Book.Ch02.average_eq_of_ae_eq {d : ℕ} {U : Domain d} {f g : Vec d → ℝ} (hfg : f =ᵐ[volumeMeasureOn U.carrier] g) : average U f = average U g

theorem HCPolySupport.Book.Ch02.averageVec_eq_of_ae_eq {d : ℕ} {U : Domain d} {f g : Vec d → Vec d} (hfg : f =ᵐ[volumeMeasureOn U.carrier] g) : averageVec U f = averageVec U g

theorem HCPolySupport.Book.Ch02.average_dilate_comp_undilate {d : ℕ} (k : ℤ) (Q : TriadicCube d) (f : Vec d → ℝ) : (average (cubeDomain (dilateCube k Q)) fun (x : Vec d) => f (undilateVec k x)) = average (cubeDomain Q) f

theorem HCPolySupport.Book.Ch02.averageVec_dilate_comp_undilate {d : ℕ} (k : ℤ) (Q : TriadicCube d) (F : Vec d → Vec d) : (averageVec (cubeDomain (dilateCube k Q)) fun (x : Vec d) => F (undilateVec k x)) = averageVec (cubeDomain Q) F

theorem HCPolySupport.Book.Ch02.responseIntegrand_dilate_ae {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} {hCoeff : CoeffOn.IsCubeDilation k a b} {u : Solution (cubeDomain Q) a} {v : Solution (cubeDomain (dilateCube k Q)) b} (hDilation : Solution.IsCubeDilation hCoeff u v) (p q : Vec d) : responseIntegrand (cubeDomain (dilateCube k Q)) b p q v =ᵐ[volumeMeasureOn (openCubeSet (dilateCube k Q))] fun (x : Vec d) => responseIntegrand (cubeDomain Q) a p q u (undilateVec k x)

theorem HCPolySupport.Book.Ch02.variationEnergyIntegrand_dilate_ae {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} {hCoeff : CoeffOn.IsCubeDilation k a b} {u : Solution (cubeDomain Q) a} {v : Solution (cubeDomain (dilateCube k Q)) b} (hDilation : Solution.IsCubeDilation hCoeff u v) : variationEnergyIntegrand (cubeDomain (dilateCube k Q)) b v =ᵐ[volumeMeasureOn (openCubeSet (dilateCube k Q))] fun (x : Vec d) => variationEnergyIntegrand (cubeDomain Q) a u (undilateVec k x)

theorem HCPolySupport.Book.Ch02.responseValue_dilate_of_isCubeDilation {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) {u : Solution (cubeDomain Q) a} {v : Solution (cubeDomain (dilateCube k Q)) b} (hDilation : Solution.IsCubeDilation hCoeff u v) (p q : Vec d) : responseValue (cubeDomain (dilateCube k Q)) b p q v = responseValue (cubeDomain Q) a p q u

theorem HCPolySupport.Book.Ch02.variationEnergyValue_dilate_of_isCubeDilation {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) {u : Solution (cubeDomain Q) a} {v : Solution (cubeDomain (dilateCube k Q)) b} (hDilation : Solution.IsCubeDilation hCoeff u v) : variationEnergyValue (cubeDomain (dilateCube k Q)) b v = variationEnergyValue (cubeDomain Q) a u

theorem HCPolySupport.Book.Ch02.averageGradient_dilate_of_isCubeDilation {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) {u : Solution (cubeDomain Q) a} {v : Solution (cubeDomain (dilateCube k Q)) b} (hDilation : Solution.IsCubeDilation hCoeff u v) : averageGradient (cubeDomain (dilateCube k Q)) b v = averageGradient (cubeDomain Q) a u

theorem HCPolySupport.Book.Ch02.averageFlux_dilate_of_isCubeDilation {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) {u : Solution (cubeDomain Q) a} {v : Solution (cubeDomain (dilateCube k Q)) b} (hDilation : Solution.IsCubeDilation hCoeff u v) : averageFlux (cubeDomain (dilateCube k Q)) b v = averageFlux (cubeDomain Q) a u

theorem HCPolySupport.Book.Ch02.responseValueSet_dilate {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) (p q : Vec d) : responseValueSet (cubeDomain (dilateCube k Q)) b p q = responseValueSet (cubeDomain Q) a p q

theorem HCPolySupport.Book.Ch02.responseJ_dilate {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) (p q : Vec d) : responseJ (cubeDomain (dilateCube k Q)) b p q = responseJ (cubeDomain Q) a p q

theorem HCPolySupport.Book.Ch02.sigmaStarInvEntry_dilate {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) (i j : Fin d) : sigmaStarInvEntry (cubeDomain (dilateCube k Q)) b i j = sigmaStarInvEntry (cubeDomain Q) a i j

theorem HCPolySupport.Book.Ch02.sigmaStarInvCoarse_dilate {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) : sigmaStarInvCoarse (cubeDomain (dilateCube k Q)) b = sigmaStarInvCoarse (cubeDomain Q) a

theorem HCPolySupport.Book.Ch02.sigmaStarCoarse_dilate {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) : sigmaStarCoarse (cubeDomain (dilateCube k Q)) b = sigmaStarCoarse (cubeDomain Q) a

theorem HCPolySupport.Book.Ch02.mixedResponse_dilate {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) (p q : Vec d) : mixedResponse (cubeDomain (dilateCube k Q)) b p q = mixedResponse (cubeDomain Q) a p q

theorem HCPolySupport.Book.Ch02.sigmaStarInvKappaCoarse_dilate {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) : sigmaStarInvKappaCoarse (cubeDomain (dilateCube k Q)) b = sigmaStarInvKappaCoarse (cubeDomain Q) a

theorem HCPolySupport.Book.Ch02.kappaCoarse_dilate {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) : kappaCoarse (cubeDomain (dilateCube k Q)) b = kappaCoarse (cubeDomain Q) a

theorem HCPolySupport.Book.Ch02.canonicalSigmaCorrectedResponse_dilate {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) (p : Vec d) : canonicalSigmaCorrectedResponse (cubeDomain (dilateCube k Q)) b p = canonicalSigmaCorrectedResponse (cubeDomain Q) a p

theorem HCPolySupport.Book.Ch02.sigmaEntry_dilate {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) (i j : Fin d) : sigmaEntry (cubeDomain (dilateCube k Q)) b i j = sigmaEntry (cubeDomain Q) a i j

theorem HCPolySupport.Book.Ch02.sigmaCoarse_dilate {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) : sigmaCoarse (cubeDomain (dilateCube k Q)) b = sigmaCoarse (cubeDomain Q) a

theorem HCPolySupport.Book.Ch02.coarseMatrices_dilate {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) : coarseMatrices (cubeDomain (dilateCube k Q)) b = coarseMatrices (cubeDomain Q) a

theorem HCPolySupport.Book.Ch02.bCoarse_dilate {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) : bCoarse (cubeDomain (dilateCube k Q)) b = bCoarse (cubeDomain Q) a

theorem HCPolySupport.Book.Ch02.aCoarse_dilate {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) : aCoarse (cubeDomain (dilateCube k Q)) b = aCoarse (cubeDomain Q) a

theorem HCPolySupport.Book.Ch02.aStarCoarse_dilate {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) : aStarCoarse (cubeDomain (dilateCube k Q)) b = aStarCoarse (cubeDomain Q) a