Coarse-graining support: Support.CoarseGraining.Definitions

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

noncomputable def HCPolySupport.volumeAverage {d : ℕ} (U : Set (Vec d)) (f : Vec d → ℝ) : ℝ

The Lebesgue integral over U multiplied by the inverse real value of its volume.

Equations

• HCPolySupport.volumeAverage U f = (MeasureTheory.volume U).toReal⁻¹ * ∫ (x : HCPolySupport.Vec d) in U, f x

noncomputable def HCPolySupport.volumeAverageVec {d : ℕ} (U : Set (Vec d)) (f : Vec d → Vec d) : Vec d

The coordinatewise volume average of a vector field on U.

Equations

• HCPolySupport.volumeAverageVec U f i = HCPolySupport.volumeAverage U fun (x : HCPolySupport.Vec d) => f x i

noncomputable def HCPolySupport.volumeAverageMat {d : ℕ} (U : Set (Vec d)) (f : Vec d → Mat d) : Mat d

The entrywise volume average of a matrix field on U.

Equations

• HCPolySupport.volumeAverageMat U f i j = HCPolySupport.volumeAverage U fun (x : HCPolySupport.Vec d) => f x i j

theorem HCPolySupport.volumeAverage_eq_zero_of_integral_eq_zero {d : ℕ} {U : Set (Vec d)} {f : Vec d → ℝ} (h : ∫ (x : Vec d) in U, f x = 0) : volumeAverage U f = 0

noncomputable def HCPolySupport.muValueSet {d : ℕ} (U : Set (Vec d)) (P : BlockVec d) (a : CoeffField d) : Set ℝ

The averaged block energies of states admissible for the prescribed constant pair P.

Equations

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

noncomputable def HCPolySupport.Mu {d : ℕ} (U : Set (Vec d)) (P : BlockVec d) (a : CoeffField d) : ℝ

The real infimum of averaged block energies of states admissible for P.

Equations

• HCPolySupport.Mu U P a = sInf (HCPolySupport.muValueSet U P a)

theorem HCPolySupport.muValueSet_mem {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {a : CoeffField d} {X : BlockState d} (hX : IsBlockMuAdmissible U P X) : volumeAverage U (blockEnergyDensity a X) ∈ muValueSet U P a

theorem HCPolySupport.muValueSet_nonempty {d : ℕ} (U : Set (Vec d)) (P : BlockVec d) (a : CoeffField d) : (muValueSet U P a).Nonempty

theorem HCPolySupport.le_Mu_of_forall_mem_muValueSet {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {a : CoeffField d} {c : ℝ} (hc : ∀ m ∈ muValueSet U P a, c ≤ m) : c ≤ Mu U P a

theorem HCPolySupport.le_Mu_of_forall_isBlockMuAdmissible {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {a : CoeffField d} {c : ℝ} (hc : ∀ (X : BlockState d), IsBlockMuAdmissible U P X → c ≤ volumeAverage U (blockEnergyDensity a X)) : c ≤ Mu U P a

noncomputable def HCPolySupport.blockResponseIntegrand {d : ℕ} (a : CoeffField d) (P Q : BlockVec d) (X : BlockState d) : Vec d → ℝ

The block response density -X·A X / 2 - P·A X + Q·X, with A the block coefficient.

Equations

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

structure HCPolySupport.BlockResponseIntegrabilityData {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (X : BlockState d) : Prop

Square-integrability of the flux and integrability of the block energy on U.

• flux_memL2 : MemVectorL2 U X.flux
• energyIntegrable : MeasureTheory.IntegrableOn (blockEnergyDensity a X) U MeasureTheory.volume

noncomputable def HCPolySupport.blockJValueSet {d : ℕ} (U : Set (Vec d)) (P Q : BlockVec d) (a : CoeffField d) : Set ℝ

Averaged block response densities of response-space states with integrable energy and L² flux.

Equations

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

noncomputable def HCPolySupport.BlockJ {d : ℕ} (U : Set (Vec d)) (P Q : BlockVec d) (a : CoeffField d) : ℝ

The real supremum of the admissible averaged block response values.

Equations

• HCPolySupport.BlockJ U P Q a = sSup (HCPolySupport.blockJValueSet U P Q a)

noncomputable def HCPolySupport.scalarResponseIntegrand {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (p q : Vec d) (u : AHarmonicFunction a U) : Vec d → ℝ

The scalar response density -∇u·symm(a)∇u / 2 - p·a∇u + q·∇u.

Equations

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

noncomputable def HCPolySupport.responseJValueSet {d : ℕ} (U : Set (Vec d)) (p q : Vec d) (a : CoeffField d) : Set ℝ

The averaged scalar response densities of all a-harmonic H¹ functions on U.

Equations

• HCPolySupport.responseJValueSet U p q a = {m : ℝ | ∃ (u : HCPolySupport.AHarmonicFunction a U), m = HCPolySupport.volumeAverage U (HCPolySupport.scalarResponseIntegrand U a p q u)}

noncomputable def HCPolySupport.ResponseJ {d : ℕ} (U : Set (Vec d)) (p q : Vec d) (a : CoeffField d) : ℝ

The real supremum of averaged scalar responses over a-harmonic H¹ functions.

Equations

• HCPolySupport.ResponseJ U p q a = sSup (HCPolySupport.responseJValueSet U p q a)

def HCPolySupport.IsCoarseBlockMatrix {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (Abar : BlockMat d) : Prop

A symmetric block matrix representing Mu U P a as one half of its quadratic form.

Equations

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

def HCPolySupport.HasQuadraticMu {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : Prop

Mu is quadratic in the note-faithful sense: after passing to the full 2d-dimensional coordinate space, it is one half of a quadratic form.

Equations

• HCPolySupport.HasQuadraticMu U a = ∃ (Q : QuadraticForm ℝ (HCPolySupport.FullBlockVec d)), ∀ (P : HCPolySupport.BlockVec d), HCPolySupport.Mu U P a = 1 / 2 * Q (HCPolySupport.toFullBlockVec P)

noncomputable def HCPolySupport.coarseBlockEntry {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (α β : BlockCoord d) : ℝ

A polarized entry of Mu: twice the basis energy on the diagonal, and the energy of the basis sum minus the two basis energies off the diagonal.

Equations

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

noncomputable def HCPolySupport.coarseBlockMatrix {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : BlockMat d

The block matrix assembled from polarized basis values of Mu.

Equations

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

theorem HCPolySupport.blockEnergyDensity_restrictCoeffField_eq_of_mem {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) (X : BlockState d) {x : Vec d} (hx : x ∈ U) : blockEnergyDensity (restrictCoeffField U a) X x = blockEnergyDensity a X x

theorem HCPolySupport.volumeAverage_blockEnergyDensity_restrictCoeffField_eq {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (a : CoeffField d) (X : BlockState d) : volumeAverage U (blockEnergyDensity (restrictCoeffField U a) X) = volumeAverage U (blockEnergyDensity a X)

theorem HCPolySupport.muValueSet_restrictCoeffField_eq {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (P : BlockVec d) (a : CoeffField d) : muValueSet U P (restrictCoeffField U a) = muValueSet U P a

theorem HCPolySupport.Mu_restrictCoeffField_eq {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (P : BlockVec d) (a : CoeffField d) : Mu U P (restrictCoeffField U a) = Mu U P a

theorem HCPolySupport.coarseBlockMatrix_eq_of_mu_eq {d : ℕ} {U V : Set (Vec d)} {a b : CoeffField d} (hmu : ∀ (P : BlockVec d), Mu U P a = Mu V P b) : coarseBlockMatrix U a = coarseBlockMatrix V b

theorem HCPolySupport.coarseBlockMatrix_restrictCoeffField_eq {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (a : CoeffField d) : coarseBlockMatrix U (restrictCoeffField U a) = coarseBlockMatrix U a

theorem HCPolySupport.eq_coarseBlockMatrix_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {Abar : BlockMat d} (hA : IsCoarseBlockMatrix U a Abar) : Abar = coarseBlockMatrix U a

theorem HCPolySupport.isCoarseBlockMatrix_coarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar) : IsCoarseBlockMatrix U a (coarseBlockMatrix U a)

theorem HCPolySupport.Mu_eq_half_blockVecDot_coarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar) (P : BlockVec d) : Mu U P a = 1 / 2 * blockVecDot P (blockMatVecMul (coarseBlockMatrix U a) P)

theorem HCPolySupport.existsUnique_coarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar) : ∃! Abar : BlockMat d, IsCoarseBlockMatrix U a Abar

theorem HCPolySupport.isCoarseBlockMatrix_of_mu_eq_half_quadraticForm {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {Q : QuadraticForm ℝ (FullBlockVec d)} (hmu : ∀ (P : BlockVec d), Mu U P a = 1 / 2 * Q (toFullBlockVec P)) : IsCoarseBlockMatrix U a (ofFullBlockMat Q.toMatrix')

theorem HCPolySupport.eq_coarseBlockMatrix_of_mu_eq_half_quadraticForm {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {Q : QuadraticForm ℝ (FullBlockVec d)} (hmu : ∀ (P : BlockVec d), Mu U P a = 1 / 2 * Q (toFullBlockVec P)) : ofFullBlockMat Q.toMatrix' = coarseBlockMatrix U a

theorem HCPolySupport.exists_coarseBlockMatrix_of_hasQuadraticMu {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hquad : HasQuadraticMu U a) : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar

theorem HCPolySupport.existsUnique_coarseBlockMatrix_of_hasQuadraticMu {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hquad : HasQuadraticMu U a) : ∃! Abar : BlockMat d, IsCoarseBlockMatrix U a Abar

theorem HCPolySupport.Mu_eq_half_blockVecDot_coarseBlockMatrix_of_hasQuadraticMu {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hquad : HasQuadraticMu U a) (P : BlockVec d) : Mu U P a = 1 / 2 * blockVecDot P (blockMatVecMul (coarseBlockMatrix U a) P)

noncomputable def HCPolySupport.coarseStarredBlockMatrixInv {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : BlockMat d

The note-faithful \mathbf A_*^{-1}(U; a) obtained from \mathbf A(U; a) by reflection.

Equations

• HCPolySupport.coarseStarredBlockMatrixInv U a = HCPolySupport.blockReflect (HCPolySupport.coarseBlockMatrix U a)

def HCPolySupport.IsSigmaStarCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (sigmaStar : Mat d) : Prop

A symmetric matrix whose inverse quadratic form represents twice ResponseJ U 0 q a.

Equations

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

def HCPolySupport.IsKappaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (sigmaStar kappa : Mat d) : Prop

Representation of the corrected mixed response by the bilinear form q·sigmaStar⁻¹ kappa p.

Equations

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

def HCPolySupport.IsSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (sigma sigmaStar kappa : Mat d) : Prop

A symmetric matrix representing the p-response after subtracting the kappa quadratic correction.

Equations

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

def HCPolySupport.IsSigmaStarInvCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (sigmaStarInv : Mat d) : Prop

A symmetric matrix representing twice the pure q-response as a quadratic form.

Equations

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

noncomputable def HCPolySupport.sigmaStarInvEntry {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (i j : Fin d) : ℝ

A polarized entry of the pure q-response, with twice the basis response on the diagonal.

Equations

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

noncomputable def HCPolySupport.sigmaStarInvCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : Mat d

The matrix assembled from polarized values of the pure q-response.

Equations

• HCPolySupport.sigmaStarInvCoarse U a i j = HCPolySupport.sigmaStarInvEntry U a i j

@[simp]

theorem HCPolySupport.sigmaStarInvCoarse_apply_same {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (i : Fin d) : sigmaStarInvCoarse U a i i = 2 * ResponseJ U 0 (Pi.single i 1) a

@[simp]

theorem HCPolySupport.sigmaStarInvCoarse_apply_of_ne {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {i j : Fin d} (hij : i ≠ j) : sigmaStarInvCoarse U a i j = ResponseJ U 0 (Pi.single i 1 + Pi.single j 1) a - ResponseJ U 0 (Pi.single i 1) a - ResponseJ U 0 (Pi.single j 1) a

theorem HCPolySupport.eq_sigmaStarInvCoarse_of_isSigmaStarInvCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigmaStarInv : Mat d} (hS : IsSigmaStarInvCoarse U a sigmaStarInv) : sigmaStarInv = sigmaStarInvCoarse U a

theorem HCPolySupport.isSigmaStarInvCoarse_sigmaStarInvCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (sigmaStarInv : Mat d), IsSigmaStarInvCoarse U a sigmaStarInv) : IsSigmaStarInvCoarse U a (sigmaStarInvCoarse U a)

theorem HCPolySupport.existsUnique_sigmaStarInvCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (sigmaStarInv : Mat d), IsSigmaStarInvCoarse U a sigmaStarInv) : ∃! sigmaStarInv : Mat d, IsSigmaStarInvCoarse U a sigmaStarInv

theorem HCPolySupport.isSigmaStarInvCoarse_of_isSigmaStarCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigmaStar : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) : IsSigmaStarInvCoarse U a sigmaStar⁻¹

theorem HCPolySupport.sigmaStarInvCoarse_eq_inv_of_isSigmaStarCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigmaStar : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) : sigmaStarInvCoarse U a = sigmaStar⁻¹

noncomputable def HCPolySupport.sigmaStarCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : Mat d

The matrix inverse of the polarized pure q-response matrix.

Equations

• HCPolySupport.sigmaStarCoarse U a = (HCPolySupport.sigmaStarInvCoarse U a)⁻¹

theorem HCPolySupport.eq_sigmaStarCoarse_of_isSigmaStarCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigmaStar : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hdet : IsUnit (Matrix.det sigmaStar)) : sigmaStarCoarse U a = sigmaStar

theorem HCPolySupport.sigmaStarCoarse_isSymm_of_isSigmaStarCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigmaStar : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hdet : IsUnit (Matrix.det sigmaStar)) : Matrix.IsSymm (sigmaStarCoarse U a)

def HCPolySupport.IsSigmaStarInvKappaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (M : Mat d) : Prop

Representation of the corrected mixed response by the bilinear form q·M p.

Equations

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

noncomputable def HCPolySupport.sigmaStarInvKappaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : Mat d

The matrix of mixed basis responses corrected by subtracting pure responses and adding p·q.

Equations

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

theorem HCPolySupport.eq_sigmaStarInvKappaCoarse_of_isSigmaStarInvKappaCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {M : Mat d} (hM : IsSigmaStarInvKappaCoarse U a M) : M = sigmaStarInvKappaCoarse U a

theorem HCPolySupport.isSigmaStarInvKappaCoarse_sigmaStarInvKappaCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (M : Mat d), IsSigmaStarInvKappaCoarse U a M) : IsSigmaStarInvKappaCoarse U a (sigmaStarInvKappaCoarse U a)

theorem HCPolySupport.existsUnique_sigmaStarInvKappaCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (M : Mat d), IsSigmaStarInvKappaCoarse U a M) : ∃! M : Mat d, IsSigmaStarInvKappaCoarse U a M

theorem HCPolySupport.isSigmaStarInvKappaCoarse_of_isKappaCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigmaStar kappa : Mat d} (hK : IsKappaCoarse U a sigmaStar kappa) : IsSigmaStarInvKappaCoarse U a (sigmaStar⁻¹ * kappa)

theorem HCPolySupport.sigmaStarInvKappaCoarse_eq_mul_of_isKappaCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigmaStar kappa : Mat d} (hK : IsKappaCoarse U a sigmaStar kappa) : sigmaStarInvKappaCoarse U a = sigmaStar⁻¹ * kappa

noncomputable def HCPolySupport.kappaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : Mat d

The product of the coarse sigmaStar matrix and the corrected mixed-response matrix.

Equations

• HCPolySupport.kappaCoarse U a = HCPolySupport.sigmaStarCoarse U a * HCPolySupport.sigmaStarInvKappaCoarse U a

theorem HCPolySupport.eq_kappaCoarse_of_isKappaCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) : kappaCoarse U a = kappa

noncomputable def HCPolySupport.sigmaCorrectedResponse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (p : Vec d) : ℝ

The pure p-response minus one half of the canonical kappaᵀ sigmaStarInv kappa quadratic form.

Equations

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

def HCPolySupport.IsSigmaCanonicalCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (sigma : Mat d) : Prop

A symmetric matrix representing twice the canonically corrected p-response.

Equations

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

noncomputable def HCPolySupport.sigmaEntry {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (i j : Fin d) : ℝ

A polarized entry of the canonically corrected p-response.

Equations

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

noncomputable def HCPolySupport.sigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : Mat d

The matrix assembled from polarized values of the canonically corrected p-response.

Equations

• HCPolySupport.sigmaCoarse U a i j = HCPolySupport.sigmaEntry U a i j

@[simp]

theorem HCPolySupport.sigmaCoarse_apply_same {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (i : Fin d) : sigmaCoarse U a i i = 2 * sigmaCorrectedResponse U a (Pi.single i 1)

@[simp]

theorem HCPolySupport.sigmaCoarse_apply_of_ne {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {i j : Fin d} (hij : i ≠ j) : sigmaCoarse U a i j = sigmaCorrectedResponse U a (Pi.single i 1 + Pi.single j 1) - sigmaCorrectedResponse U a (Pi.single i 1) - sigmaCorrectedResponse U a (Pi.single j 1)

theorem HCPolySupport.eq_sigmaCoarse_of_isSigmaCanonicalCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma : Mat d} (hSigma : IsSigmaCanonicalCoarse U a sigma) : sigma = sigmaCoarse U a

theorem HCPolySupport.isSigmaCanonicalCoarse_sigmaCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (sigma : Mat d), IsSigmaCanonicalCoarse U a sigma) : IsSigmaCanonicalCoarse U a (sigmaCoarse U a)

theorem HCPolySupport.existsUnique_sigmaCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (sigma : Mat d), IsSigmaCanonicalCoarse U a sigma) : ∃! sigma : Mat d, IsSigmaCanonicalCoarse U a sigma

theorem HCPolySupport.isSigmaCanonicalCoarse_of_isSigmaCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) : IsSigmaCanonicalCoarse U a sigma

theorem HCPolySupport.sigmaCoarse_eq_of_isSigmaCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) : sigmaCoarse U a = sigma

theorem HCPolySupport.sigmaCoarse_isSymm_of_isSigmaCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) : Matrix.IsSymm (sigmaCoarse U a)

noncomputable def HCPolySupport.bCoarse {d : ℕ} (sigma sigmaStar kappa : Mat d) : Mat d

The matrix sigma + kappaᵀ sigmaStar⁻¹ kappa.

Equations

• HCPolySupport.bCoarse sigma sigmaStar kappa = sigma + HCPolySupport.matTranspose kappa * sigmaStar⁻¹ * kappa

theorem HCPolySupport.bCoarse_smul {d : ℕ} {sigma sigmaStar kappa : Mat d} (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) : bCoarse (lam • sigma) (lam • sigmaStar) (lam • kappa) = lam • bCoarse sigma sigmaStar kappa

theorem HCPolySupport.bCoarse_isSymm_of_isSigmaCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) : Matrix.IsSymm (bCoarse sigma sigmaStar kappa)

noncomputable def HCPolySupport.aCoarse {d : ℕ} (sigma kappa : Mat d) : Mat d

The matrix sigma - kappaᵀ.

Equations

• HCPolySupport.aCoarse sigma kappa = sigma - HCPolySupport.matTranspose kappa

noncomputable def HCPolySupport.aStarCoarse {d : ℕ} (sigmaStar kappa : Mat d) : Mat d

The matrix sigmaStar - kappaᵀ.

Equations

• HCPolySupport.aStarCoarse sigmaStar kappa = sigmaStar - HCPolySupport.matTranspose kappa