Coarse-graining support: Support.Book.Ch04.AnnealedDefinitions

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

Annealed coarse definitions

This file owns the Chapter 4 definitions of annealed coarse matrices and response observables. Scalarization witnesses and route data live in HCPolySupport.Book.Ch04.Internal.ScalarizationWitnesses.

noncomputable def HCPolySupport.Book.Ch04.annealedBlockMatrix {d : ℕ} (P : RestrictionCoeffLaw d) (U : Set (Vec d)) : BlockMat d

The annealed doubled coarse-grained matrix \overline{\mathbf A}(U), obtained by averaging each deterministic coarse matrix entry.

Equations

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

noncomputable def HCPolySupport.Book.Ch04.annealedStarredBlockMatrixInv {d : ℕ} (P : RestrictionCoeffLaw d) (U : Set (Vec d)) : BlockMat d

The annealed starred block matrix \overline{\mathbf A}_{*,n}^{-1}.

Equations

• HCPolySupport.Book.Ch04.annealedStarredBlockMatrixInv P U = HCPolySupport.blockReflect (HCPolySupport.Book.Ch04.annealedBlockMatrix P U)

noncomputable def HCPolySupport.Book.Ch04.annealedSigmaStarInv {d : ℕ} (P : RestrictionCoeffLaw d) (U : Set (Vec d)) : Mat d

The annealed inverse-star matrix \overline\sigma_*^{-1}(U).

Equations

• HCPolySupport.Book.Ch04.annealedSigmaStarInv P U = (HCPolySupport.Book.Ch04.annealedBlockMatrix P U).lowerRight

noncomputable def HCPolySupport.Book.Ch04.annealedSigmaStar {d : ℕ} (P : RestrictionCoeffLaw d) (U : Set (Vec d)) : Mat d

The annealed starred matrix \overline\sigma_*(U).

Equations

• HCPolySupport.Book.Ch04.annealedSigmaStar P U = (HCPolySupport.Book.Ch04.annealedSigmaStarInv P U)⁻¹

noncomputable def HCPolySupport.Book.Ch04.annealedSigmaStarInvKappaMean {d : ℕ} (P : RestrictionCoeffLaw d) (U : Set (Vec d)) : Mat d

The annealed mixed block E[\sigma_*^{-1}(U; a)\kappa(U; a)].

Equations

• HCPolySupport.Book.Ch04.annealedSigmaStarInvKappaMean P U = -(HCPolySupport.Book.Ch04.annealedBlockMatrix P U).lowerLeft

noncomputable def HCPolySupport.Book.Ch04.annealedKappa {d : ℕ} (P : RestrictionCoeffLaw d) (U : Set (Vec d)) : Mat d

The annealed coupling matrix \overline\kappa(U).

Equations

• HCPolySupport.Book.Ch04.annealedKappa P U = HCPolySupport.Book.Ch04.annealedSigmaStar P U * HCPolySupport.Book.Ch04.annealedSigmaStarInvKappaMean P U

noncomputable def HCPolySupport.Book.Ch04.annealedB {d : ℕ} (P : RestrictionCoeffLaw d) (U : Set (Vec d)) : Mat d

The annealed upper-left block \overline b(U).

Equations

• HCPolySupport.Book.Ch04.annealedB P U = (HCPolySupport.Book.Ch04.annealedBlockMatrix P U).upperLeft

noncomputable def HCPolySupport.Book.Ch04.annealedSigma {d : ℕ} (P : RestrictionCoeffLaw d) (U : Set (Vec d)) : Mat d

The annealed conductivity matrix \overline\sigma = \overline b - \overline\kappa^t \overline\sigma_*^{-1}\overline\kappa.

Equations

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

@[simp]

theorem HCPolySupport.Book.Ch04.annealedBlockMatrix_upperLeft_apply {d : ℕ} (P : RestrictionCoeffLaw d) (U : Set (Vec d)) (i j : Fin d) : (annealedBlockMatrix P U).upperLeft i j = ∫ (a : RegCoeffField d), (coarseBlockMatrix U a.toFun).upperLeft i j ∂P

@[simp]

theorem HCPolySupport.Book.Ch04.annealedBlockMatrix_upperRight_apply {d : ℕ} (P : RestrictionCoeffLaw d) (U : Set (Vec d)) (i j : Fin d) : (annealedBlockMatrix P U).upperRight i j = ∫ (a : RegCoeffField d), (coarseBlockMatrix U a.toFun).upperRight i j ∂P

@[simp]

theorem HCPolySupport.Book.Ch04.annealedBlockMatrix_lowerLeft_apply {d : ℕ} (P : RestrictionCoeffLaw d) (U : Set (Vec d)) (i j : Fin d) : (annealedBlockMatrix P U).lowerLeft i j = ∫ (a : RegCoeffField d), (coarseBlockMatrix U a.toFun).lowerLeft i j ∂P

@[simp]

theorem HCPolySupport.Book.Ch04.annealedBlockMatrix_lowerRight_apply {d : ℕ} (P : RestrictionCoeffLaw d) (U : Set (Vec d)) (i j : Fin d) : (annealedBlockMatrix P U).lowerRight i j = ∫ (a : RegCoeffField d), (coarseBlockMatrix U a.toFun).lowerRight i j ∂P

@[simp]

theorem HCPolySupport.Book.Ch04.annealedSigmaStarInv_apply {d : ℕ} (P : RestrictionCoeffLaw d) (U : Set (Vec d)) (i j : Fin d) : annealedSigmaStarInv P U i j = ∫ (a : RegCoeffField d), (coarseBlockMatrix U a.toFun).lowerRight i j ∂P

@[simp]

theorem HCPolySupport.Book.Ch04.annealedSigmaStarInvKappaMean_apply {d : ℕ} (P : RestrictionCoeffLaw d) (U : Set (Vec d)) (i j : Fin d) : annealedSigmaStarInvKappaMean P U i j = -∫ (a : RegCoeffField d), (coarseBlockMatrix U a.toFun).lowerLeft i j ∂P

@[simp]

theorem HCPolySupport.Book.Ch04.annealedB_apply {d : ℕ} (P : RestrictionCoeffLaw d) (U : Set (Vec d)) (i j : Fin d) : annealedB P U i j = ∫ (a : RegCoeffField d), (coarseBlockMatrix U a.toFun).upperLeft i j ∂P

noncomputable def HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale {d : ℕ} (P : RestrictionCoeffLaw d) (n : ℤ) : BlockMat d

Annealed block matrix on the origin cube at scale n.

Equations

• HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale P n = HCPolySupport.Book.Ch04.annealedBlockMatrix P (HCPolySupport.cubeSet (HCPolySupport.originCube d n))

noncomputable def HCPolySupport.Book.Ch04.annealedStarredBlockMatrixInvAtScale {d : ℕ} (P : RestrictionCoeffLaw d) (n : ℤ) : BlockMat d

Annealed starred block matrix on the origin cube at scale n.

Equations

• HCPolySupport.Book.Ch04.annealedStarredBlockMatrixInvAtScale P n = HCPolySupport.Book.Ch04.annealedStarredBlockMatrixInv P (HCPolySupport.cubeSet (HCPolySupport.originCube d n))

noncomputable def HCPolySupport.Book.Ch04.annealedSigmaStarInvAtScale {d : ℕ} (P : RestrictionCoeffLaw d) (n : ℤ) : Mat d

Annealed inverse-star matrix on the origin cube at scale n.

Equations

• HCPolySupport.Book.Ch04.annealedSigmaStarInvAtScale P n = HCPolySupport.Book.Ch04.annealedSigmaStarInv P (HCPolySupport.cubeSet (HCPolySupport.originCube d n))

noncomputable def HCPolySupport.Book.Ch04.annealedSigmaStarAtScale {d : ℕ} (P : RestrictionCoeffLaw d) (n : ℤ) : Mat d

Annealed starred matrix on the origin cube at scale n.

Equations

• HCPolySupport.Book.Ch04.annealedSigmaStarAtScale P n = HCPolySupport.Book.Ch04.annealedSigmaStar P (HCPolySupport.cubeSet (HCPolySupport.originCube d n))

noncomputable def HCPolySupport.Book.Ch04.annealedSigmaStarInvKappaMeanAtScale {d : ℕ} (P : RestrictionCoeffLaw d) (n : ℤ) : Mat d

Annealed mixed block on the origin cube at scale n.

Equations

• HCPolySupport.Book.Ch04.annealedSigmaStarInvKappaMeanAtScale P n = HCPolySupport.Book.Ch04.annealedSigmaStarInvKappaMean P (HCPolySupport.cubeSet (HCPolySupport.originCube d n))

noncomputable def HCPolySupport.Book.Ch04.annealedKappaAtScale {d : ℕ} (P : RestrictionCoeffLaw d) (n : ℤ) : Mat d

Annealed coupling matrix on the origin cube at scale n.

Equations

• HCPolySupport.Book.Ch04.annealedKappaAtScale P n = HCPolySupport.Book.Ch04.annealedKappa P (HCPolySupport.cubeSet (HCPolySupport.originCube d n))

noncomputable def HCPolySupport.Book.Ch04.annealedBAtScale {d : ℕ} (P : RestrictionCoeffLaw d) (n : ℤ) : Mat d

Annealed upper-left block on the origin cube at scale n.

Equations

• HCPolySupport.Book.Ch04.annealedBAtScale P n = HCPolySupport.Book.Ch04.annealedB P (HCPolySupport.cubeSet (HCPolySupport.originCube d n))

noncomputable def HCPolySupport.Book.Ch04.annealedSigmaAtScale {d : ℕ} (P : RestrictionCoeffLaw d) (n : ℤ) : Mat d

Annealed conductivity matrix on the origin cube at scale n.

Equations

• HCPolySupport.Book.Ch04.annealedSigmaAtScale P n = HCPolySupport.Book.Ch04.annealedSigma P (HCPolySupport.cubeSet (HCPolySupport.originCube d n))

noncomputable def HCPolySupport.Book.Ch04.responseJAtScale {d : ℕ} (n : ℤ) (p q : Vec d) (a : CoeffField d) : ℝ

Response functional on the origin cube at scale n.

Equations

• HCPolySupport.Book.Ch04.responseJAtScale n p q a = HCPolySupport.ResponseJ (HCPolySupport.cubeSet (HCPolySupport.originCube d n)) p q a

noncomputable def HCPolySupport.Book.Ch04.responseJOnCube {d : ℕ} (Q : TriadicCube d) (p q : Vec d) (a : CoeffField d) : ℝ

Response functional on an arbitrary triadic cube.

Equations

• HCPolySupport.Book.Ch04.responseJOnCube Q p q a = HCPolySupport.ResponseJ (HCPolySupport.cubeSet Q) p q a

noncomputable def HCPolySupport.Book.Ch04.annealedResponseJAtScale {d : ℕ} (P : RestrictionCoeffLaw d) (n : ℤ) (p q : Vec d) : ℝ

Annealed response functional on the origin cube at scale n.

Equations

• HCPolySupport.Book.Ch04.annealedResponseJAtScale P n p q = ∫ (a : HCPolySupport.RegCoeffField d), HCPolySupport.Book.Ch04.responseJAtScale n p q a.toFun ∂P

noncomputable def HCPolySupport.Book.Ch04.coarseFullBlockMatrixAtCube {d : ℕ} (Q : TriadicCube d) : RegCoeffField d → FullBlockMat d

Full unfolded coarse block observable on a deterministic triadic cube.

Equations

• HCPolySupport.Book.Ch04.coarseFullBlockMatrixAtCube Q a = HCPolySupport.coarseFullBlockMatrixObservable (HCPolySupport.cubeSet Q) a.toFun