Coarse-graining support: Support.CoarseGraining.Symmetric.AverageFormulas #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Average formulas for symmetric coefficient fields #
For symmetric coefficient fields, the canonical average-gradient and
average-flux formulas split into pure Dirichlet and Neumann response pieces.
The scalar maximizer for (p, 0) corresponds to the negative of the affine
Dirichlet solution, which accounts for the signs in the pure-gradient formulas.
theorem
HCPolySupport.ScalarCanonicalMaximizer.averageGradientFormulaCanonical_p_zero_of_isSymmetricCoeffField
{d : ℕ}
{U : Set (Vec d)}
{p : Vec d}
{a : CoeffField d}
{sigmaStar kappa : Mat d}
(v : ScalarCanonicalMaximizer U p 0 a)
(ha : IsSymmetricCoeffField a)
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hdet : IsUnit (Matrix.det sigmaStar))
(hInt : ResponseLinearIntegrabilityData U a)
(vGrad : (i : Fin d) → ScalarCanonicalMaximizer U 0 (Pi.single i 1) a)
:
(fun (i : Fin d) =>
volumeAverage U fun (x : Vec d) => v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x i) = -p
theorem
HCPolySupport.ScalarCanonicalMaximizer.averageFluxFormulaCanonical_p_zero_of_isSymmetricCoeffField
{d : ℕ}
{U : Set (Vec d)}
{p : Vec d}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(v : ScalarCanonicalMaximizer U p 0 a)
(ha : IsSymmetricCoeffField a)
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hdet : IsUnit (Matrix.det sigmaStar))
(hInt : ResponseLinearIntegrabilityData U a)
(vFlux : (i : Fin d) → ScalarCanonicalMaximizer U (Pi.single i 1) 0 a)
:
(fun (i : Fin d) =>
volumeAverage U fun (x : Vec d) =>
matVecMul (a x) (v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x) i) = -matVecMul (sigmaCoarse U a) p
theorem
HCPolySupport.ScalarCanonicalMaximizer.averageGradientFormulaCanonical_zero_q_of_isSymmetricCoeffField
{d : ℕ}
{U : Set (Vec d)}
{q : Vec d}
{a : CoeffField d}
{sigmaStar kappa : Mat d}
(v : ScalarCanonicalMaximizer U 0 q a)
(ha : IsSymmetricCoeffField a)
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hdet : IsUnit (Matrix.det sigmaStar))
(hInt : ResponseLinearIntegrabilityData U a)
(vGrad : (i : Fin d) → ScalarCanonicalMaximizer U 0 (Pi.single i 1) a)
:
(fun (i : Fin d) =>
volumeAverage U fun (x : Vec d) => v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x i) = matVecMul (sigmaStarInvCoarse U a) q
theorem
HCPolySupport.ScalarCanonicalMaximizer.averageFluxFormulaCanonical_zero_q_of_isSymmetricCoeffField
{d : ℕ}
{U : Set (Vec d)}
{q : Vec d}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(v : ScalarCanonicalMaximizer U 0 q a)
(ha : IsSymmetricCoeffField a)
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hdet : IsUnit (Matrix.det sigmaStar))
(hInt : ResponseLinearIntegrabilityData U a)
(vFlux : (i : Fin d) → ScalarCanonicalMaximizer U (Pi.single i 1) 0 a)
:
(fun (i : Fin d) =>
volumeAverage U fun (x : Vec d) =>
matVecMul (a x) (v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x) i) = q