Public one-cube and multiscale dilation theory

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

The public theory structures package the solution, response, and multiscale transport lemmas proved in Dilation.Proofs.

structure HCPolySupport.Book.Ch02.CubeDilationTheory (d : ℕ) : Prop

One-cube public dilation statements. These are the Chapter 3-facing facts: solutions dilate to solutions, scalar and doubled response values are unchanged, and all canonical one-cube coarse matrices are unchanged.

• solution_dilation_exists {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) : Nonempty (Solution.CubeDilation hCoeff u)
• responseValue_dilate {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} : 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
• variationEnergyValue_dilate {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} : Solution.IsCubeDilation hCoeff u v → variationEnergyValue (cubeDomain (dilateCube k Q)) b v = variationEnergyValue (cubeDomain Q) a u
• averageGradient_dilate {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} : Solution.IsCubeDilation hCoeff u v → averageGradient (cubeDomain (dilateCube k Q)) b v = averageGradient (cubeDomain Q) a u
• averageFlux_dilate {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} : Solution.IsCubeDilation hCoeff u v → averageFlux (cubeDomain (dilateCube k Q)) b v = averageFlux (cubeDomain Q) a u
• responseJ_dilate {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} : CoeffOn.IsCubeDilation k a b → ∀ (p q : Vec d), responseJ (cubeDomain (dilateCube k Q)) b p q = responseJ (cubeDomain Q) a p q
• doubledMu_dilate {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} : CoeffOn.IsCubeDilation k a b → ∀ (P : BlockVec d), doubledMu (cubeDomain (dilateCube k Q)) b P = doubledMu (cubeDomain Q) a P
• doubledResponseJ_dilate {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} : CoeffOn.IsCubeDilation k a b → ∀ (P R : BlockVec d), doubledResponseJ (cubeDomain (dilateCube k Q)) b P R = doubledResponseJ (cubeDomain Q) a P R
• sigmaCoarse_dilate {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} : CoeffOn.IsCubeDilation k a b → sigmaCoarse (cubeDomain (dilateCube k Q)) b = sigmaCoarse (cubeDomain Q) a
• sigmaStarInvCoarse_dilate {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} : CoeffOn.IsCubeDilation k a b → sigmaStarInvCoarse (cubeDomain (dilateCube k Q)) b = sigmaStarInvCoarse (cubeDomain Q) a
• sigmaStarCoarse_dilate {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} : CoeffOn.IsCubeDilation k a b → sigmaStarCoarse (cubeDomain (dilateCube k Q)) b = sigmaStarCoarse (cubeDomain Q) a
• kappaCoarse_dilate {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} : CoeffOn.IsCubeDilation k a b → kappaCoarse (cubeDomain (dilateCube k Q)) b = kappaCoarse (cubeDomain Q) a
• coarseMatrices_dilate {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} : CoeffOn.IsCubeDilation k a b → coarseMatrices (cubeDomain (dilateCube k Q)) b = coarseMatrices (cubeDomain Q) a
• bCoarse_dilate {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} : CoeffOn.IsCubeDilation k a b → bCoarse (cubeDomain (dilateCube k Q)) b = bCoarse (cubeDomain Q) a
• aCoarse_dilate {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} : CoeffOn.IsCubeDilation k a b → aCoarse (cubeDomain (dilateCube k Q)) b = aCoarse (cubeDomain Q) a
• aStarCoarse_dilate {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} : CoeffOn.IsCubeDilation k a b → aStarCoarse (cubeDomain (dilateCube k Q)) b = aStarCoarse (cubeDomain Q) a

structure HCPolySupport.Book.Ch02.MultiscaleDilationTheory (d : ℕ) [NeZero d] : Prop

Chapter 2.5 multiscale dilation statements. A dilation shifts every scale index by k; the normalized multiscale quantities themselves do not change.

• coarseBMatrixNorm_dilate {k : ℤ} {a b : TriadicCoeffFamily d} : TriadicCoeffFamily.IsDilation k a b → ∀ (Q : TriadicCube d), coarseBMatrixNorm (dilateCube k Q) b = coarseBMatrixNorm Q a
• coarseSigmaStarInvMatrixNorm_dilate {k : ℤ} {a b : TriadicCoeffFamily d} : TriadicCoeffFamily.IsDilation k a b → ∀ (Q : TriadicCube d), coarseSigmaStarInvMatrixNorm (dilateCube k Q) b = coarseSigmaStarInvMatrixNorm Q a
• maxDescendantBMatrixNormAtScale_dilate {k : ℤ} {a b : TriadicCoeffFamily d} : TriadicCoeffFamily.IsDilation k a b → ∀ (Q : TriadicCube d) (n : ℤ), maxDescendantBMatrixNormAtScale (dilateCube k Q) (n + k) b = maxDescendantBMatrixNormAtScale Q n a
• maxDescendantSigmaStarInvMatrixNormAtScale_dilate {k : ℤ} {a b : TriadicCoeffFamily d} : TriadicCoeffFamily.IsDilation k a b → ∀ (Q : TriadicCube d) (n : ℤ), maxDescendantSigmaStarInvMatrixNormAtScale (dilateCube k Q) (n + k) b = maxDescendantSigmaStarInvMatrixNormAtScale Q n a
• LambdaSq_dilate {k : ℤ} {a b : TriadicCoeffFamily d} : TriadicCoeffFamily.IsDilation k a b → ∀ (Q : TriadicCube d) (s : ℝ) (q : MultiscaleExponent), LambdaSq (dilateCube k Q) s q b = LambdaSq Q s q a
• lambdaSq_dilate {k : ℤ} {a b : TriadicCoeffFamily d} : TriadicCoeffFamily.IsDilation k a b → ∀ (Q : TriadicCube d) (s : ℝ) (q : MultiscaleExponent), lambdaSq (dilateCube k Q) s q b = lambdaSq Q s q a
• LambdaS_dilate {k : ℤ} {a b : TriadicCoeffFamily d} : TriadicCoeffFamily.IsDilation k a b → ∀ (Q : TriadicCube d) (s : ℝ), LambdaS (dilateCube k Q) s b = LambdaS Q s a
• lambdaS_dilate {k : ℤ} {a b : TriadicCoeffFamily d} : TriadicCoeffFamily.IsDilation k a b → ∀ (Q : TriadicCube d) (s : ℝ), lambdaS (dilateCube k Q) s b = lambdaS Q s a
• ThetaRatio_dilate {k : ℤ} {a b : TriadicCoeffFamily d} : TriadicCoeffFamily.IsDilation k a b → ∀ (Q : TriadicCube d) (s t : ℝ), ThetaRatio (dilateCube k Q) s t b = ThetaRatio Q s t a
• maxDescendantUpperEllipticityAtScale_dilate {k : ℤ} {a b : TriadicCoeffFamily d} : TriadicCoeffFamily.IsDilation k a b → ∀ (Q : TriadicCube d) (n : ℤ) (s : ℝ) (q : MultiscaleExponent), maxDescendantUpperEllipticityAtScale (dilateCube k Q) (n + k) s q b = maxDescendantUpperEllipticityAtScale Q n s q a
• maxDescendantLowerEllipticityInvAtScale_dilate {k : ℤ} {a b : TriadicCoeffFamily d} : TriadicCoeffFamily.IsDilation k a b → ∀ (Q : TriadicCube d) (n : ℤ) (s : ℝ) (q : MultiscaleExponent), maxDescendantLowerEllipticityInvAtScale (dilateCube k Q) (n + k) s q b = maxDescendantLowerEllipticityInvAtScale Q n s q a
• normalizedBlockResponseMax_dilate {k : ℤ} {a b : TriadicCoeffFamily d} : TriadicCoeffFamily.IsDilation k a b → ∀ (Q : TriadicCube d) (a0 : Mat d), normalizedBlockResponseMax (dilateCube k Q) b a0 = normalizedBlockResponseMax Q a a0
• maxDescendantNormalizedBlockResponseAtScale_dilate {k : ℤ} {a b : TriadicCoeffFamily d} : TriadicCoeffFamily.IsDilation k a b → ∀ (Q : TriadicCube d) (n : ℤ) (a0 : Mat d), maxDescendantNormalizedBlockResponseAtScale (dilateCube k Q) (n + k) b a0 = maxDescendantNormalizedBlockResponseAtScale Q n a a0
• scaleResponseAtScale_dilate {k : ℤ} {a b : TriadicCoeffFamily d} : TriadicCoeffFamily.IsDilation k a b → ∀ (Q : TriadicCube d) (n : ℤ) (p : MultiscaleExponent) (a0 : Mat d), scaleResponseAtScale (dilateCube k Q) (n + k) p b a0 = scaleResponseAtScale Q n p a a0
• HomogenizationError_dilate {k : ℤ} {a b : TriadicCoeffFamily d} : TriadicCoeffFamily.IsDilation k a b → ∀ (Q : TriadicCube d) (n : ℤ) (s : ℝ) (p q : MultiscaleExponent) (a0 : Mat d), HomogenizationError (dilateCube k Q) (n + k) s p q b a0 = HomogenizationError Q n s p q a a0
• HomogenizationErrorOnCube_dilate {k : ℤ} {a b : TriadicCoeffFamily d} : TriadicCoeffFamily.IsDilation k a b → ∀ (Q : TriadicCube d) (s : ℝ) (p q : MultiscaleExponent) (a0 : Mat d), HomogenizationErrorOnCube (dilateCube k Q) s p q b a0 = HomogenizationErrorOnCube Q s p q a a0

structure HCPolySupport.Book.Ch02.DilationTheory (d : ℕ) [NeZero d] : Prop

Aggregate public dilation theorem package for Chapter 2 / 2.5, intended to be imported by Chapter 3 scale-normalization arguments.

• cube : CubeDilationTheory d
• multiscale : MultiscaleDilationTheory d