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

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

Public multiscale homogenization error

This file records the Chapter 2 note-facing quantity \mathcal E_{s,p,q} using the public TriadicCoeffFamily interface. In particular the heterogeneous coefficient is a.e.-elliptic on every open cube, not pointwise elliptic.

def HCPolySupport.Book.Ch02.fullBlockVecNormSq {d : ℕ} (x : FullBlockVec d) : ℝ

Euclidean squared norm on doubled vectors in the full 2d indexing.

Equations

• HCPolySupport.Book.Ch02.fullBlockVecNormSq x = ∑ i : HCPolySupport.BlockCoord d, x i ^ 2

noncomputable def HCPolySupport.Book.Ch02.finsetAverageReal {α : Type u_1} (s : Finset α) (f : α → ℝ) : ℝ

Average of a real-valued function over a finite set.

Equations

• HCPolySupport.Book.Ch02.finsetAverageReal s f = (↑s.card)⁻¹ * s.sum f

noncomputable def HCPolySupport.Book.Ch02.constantBlockMatrix {d : ℕ} (a0 : Mat d) : BlockMat d

Constant block matrix associated with a constant coefficient matrix a0.

Equations

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

noncomputable def HCPolySupport.Book.Ch02.constantFullBlockMatrix {d : ℕ} (a0 : Mat d) : FullBlockMat d

Constant block matrix in full 2d × 2d matrix coordinates.

Equations

• HCPolySupport.Book.Ch02.constantFullBlockMatrix a0 = HCPolySupport.toFullBlockMat (HCPolySupport.Book.Ch02.constantBlockMatrix a0)

noncomputable def HCPolySupport.Book.Ch02.constantFullBlockMatrixSqrt {d : ℕ} (a0 : Mat d) : FullBlockMat d

Positive square root used in the normalization of \mathcal E.

Equations

• HCPolySupport.Book.Ch02.constantFullBlockMatrixSqrt a0 = CFC.sqrt (HCPolySupport.Book.Ch02.constantFullBlockMatrix a0)

noncomputable def HCPolySupport.Book.Ch02.constantFullBlockMatrixInvSqrt {d : ℕ} (a0 : Mat d) : FullBlockMat d

Inverse positive square root used in the normalization of \mathcal E.

Equations

• HCPolySupport.Book.Ch02.constantFullBlockMatrixInvSqrt a0 = (HCPolySupport.Book.Ch02.constantFullBlockMatrixSqrt a0)⁻¹

noncomputable def HCPolySupport.Book.Ch02.normalizedBlockResponseValueSet {d : ℕ} (Q : TriadicCube d) (a : TriadicCoeffFamily d) (a0 : Mat d) : Set ℝ

The normalized block-response value set max_{|e|=1} J(Q, A0^{-1/2} e, A0^{1/2} e; a).

Equations

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

noncomputable def HCPolySupport.Book.Ch02.normalizedBlockResponseMax {d : ℕ} (Q : TriadicCube d) (a : TriadicCoeffFamily d) (a0 : Mat d) : ℝ

The one-cube normalized block-response maximum.

Equations

• HCPolySupport.Book.Ch02.normalizedBlockResponseMax Q a a0 = sSup (HCPolySupport.Book.Ch02.normalizedBlockResponseValueSet Q a a0)

noncomputable def HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale {d : ℕ} (Q : TriadicCube d) (k : ℤ) (a : TriadicCoeffFamily d) (a0 : Mat d) : ℝ

Maximum normalized block response over descendants of Q at scale k.

Equations

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

noncomputable def HCPolySupport.Book.Ch02.scaleResponseAtScale {d : ℕ} (Q : TriadicCube d) (k : ℤ) (p : MultiscaleExponent) (a : TriadicCoeffFamily d) (a0 : Mat d) : ℝ

The p-aggregation over descendants at one scale in the definition of \mathcal E_{s,p,q}.

Equations

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

noncomputable def HCPolySupport.Book.Ch02.HomogenizationErrorFinite {d : ℕ} (Q : TriadicCube d) (n : ℤ) (s : ℝ) (p : MultiscaleExponent) (q : ℝ) (a : TriadicCoeffFamily d) (a0 : Mat d) : ℝ

Finite-q multiscale homogenization error.

Equations

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

noncomputable def HCPolySupport.Book.Ch02.HomogenizationErrorInfinity {d : ℕ} (Q : TriadicCube d) (n : ℤ) (s : ℝ) (p : MultiscaleExponent) (a : TriadicCoeffFamily d) (a0 : Mat d) : ℝ

Endpoint-q multiscale homogenization error.

Equations

• HCPolySupport.Book.Ch02.HomogenizationErrorInfinity Q n s p a a0 = sSup {m : ℝ | ∃ (l : ℕ), m = Real.rpow 3 (-s * ↑l) * HCPolySupport.Book.Ch02.scaleResponseAtScale Q (n - ↑l) p a a0}

noncomputable def HCPolySupport.Book.Ch02.HomogenizationError {d : ℕ} (Q : TriadicCube d) (n : ℤ) (s : ℝ) (p q : MultiscaleExponent) (a : TriadicCoeffFamily d) (a0 : Mat d) : ℝ

Multiscale homogenization error for finite q and q = infinity.

Equations

• HCPolySupport.Book.Ch02.HomogenizationError Q n s p (HCPolySupport.Book.Ch02.MultiscaleExponent.finite p_2) a a0 = HCPolySupport.Book.Ch02.HomogenizationErrorFinite Q n s p p_2 a a0
• HCPolySupport.Book.Ch02.HomogenizationError Q n s p HCPolySupport.Book.Ch02.MultiscaleExponent.infinity a a0 = HCPolySupport.Book.Ch02.HomogenizationErrorInfinity Q n s p a a0

noncomputable def HCPolySupport.Book.Ch02.HomogenizationErrorOnCube {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : MultiscaleExponent) (a : TriadicCoeffFamily d) (a0 : Mat d) : ℝ

The untruncated cube quantity \mathcal E_{s,p,q}(Q; a, a0), where the truncation scale is the scale of Q.

Equations

• HCPolySupport.Book.Ch02.HomogenizationErrorOnCube Q s p q a a0 = HCPolySupport.Book.Ch02.HomogenizationError Q Q.scale s p q a a0