Coarse-graining support:

Support.CoarseGraining.ResponseIdentities.AverageFormulas.CanonicalFormulas

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

Average formulas (part 4) -- ScalarCanonicalMaximizer average formulas

averageGradient / averageFlux (plain and canonical) and their formula variants (generic, canonical, deterministicCoarseBlockMatrix, coarseBlockMatrix) inside the ScalarCanonicalMaximizer namespace.

theorem HCPolySupport.ScalarCanonicalMaximizer.averageGradient {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} (v : ScalarCanonicalMaximizer U p q a) (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) = fun (i : Fin d) => ResponseJ U p q a + ResponseJ U 0 (Pi.single i 1) a - ResponseJ U p (q - Pi.single i 1) a

theorem HCPolySupport.ScalarCanonicalMaximizer.averageGradientOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam 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) = fun (i : Fin d) => ResponseJ U p q a + ResponseJ U 0 (Pi.single i 1) a - ResponseJ U p (q - Pi.single i 1) a

theorem HCPolySupport.ScalarCanonicalMaximizer.averageGradientOfBasisData {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} (v : ScalarCanonicalMaximizer U p q a) (hInt : ResponseLinearIntegrabilityData U a) (basis : GradientBasisData U a) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x i) = fun (i : Fin d) => ResponseJ U p q a + ResponseJ U 0 (Pi.single i 1) a - ResponseJ U p (q - Pi.single i 1) a

theorem HCPolySupport.ScalarCanonicalMaximizer.averageGradientOfBasisDataOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam U a) (basis : GradientBasisData U a) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x i) = fun (i : Fin d) => ResponseJ U p q a + ResponseJ U 0 (Pi.single i 1) a - ResponseJ U p (q - Pi.single i 1) a

theorem HCPolySupport.ScalarCanonicalMaximizer.averageFlux {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} (v : ScalarCanonicalMaximizer U p q a) (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) = fun (i : Fin d) => ResponseJ U (p - Pi.single i 1) q a - ResponseJ U p q a - ResponseJ U (Pi.single i 1) 0 a

theorem HCPolySupport.ScalarCanonicalMaximizer.averageFluxOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam 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) = fun (i : Fin d) => ResponseJ U (p - Pi.single i 1) q a - ResponseJ U p q a - ResponseJ U (Pi.single i 1) 0 a

theorem HCPolySupport.ScalarCanonicalMaximizer.averageFluxOfBasisData {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} (v : ScalarCanonicalMaximizer U p q a) (hInt : ResponseLinearIntegrabilityData U a) (basis : FluxBasisData U a) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x) i) = fun (i : Fin d) => ResponseJ U (p - Pi.single i 1) q a - ResponseJ U p q a - ResponseJ U (Pi.single i 1) 0 a

theorem HCPolySupport.ScalarCanonicalMaximizer.averageFluxOfBasisDataOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam U a) (basis : FluxBasisData U a) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x) i) = fun (i : Fin d) => ResponseJ U (p - Pi.single i 1) q a - ResponseJ U p q a - ResponseJ U (Pi.single i 1) 0 a

theorem HCPolySupport.ScalarCanonicalMaximizer.averageGradientFormula {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q a) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (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 + matVecMul sigmaStar⁻¹ (q + matVecMul kappa p)

theorem HCPolySupport.ScalarCanonicalMaximizer.averageGradientFormulaOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam U a) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (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 + matVecMul sigmaStar⁻¹ (q + matVecMul kappa p)

theorem HCPolySupport.ScalarCanonicalMaximizer.averageGradientFormulaOfBasisData {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q a) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hInt : ResponseLinearIntegrabilityData U a) (basis : GradientBasisData U a) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x i) = -p + matVecMul sigmaStar⁻¹ (q + matVecMul kappa p)

theorem HCPolySupport.ScalarCanonicalMaximizer.averageGradientFormulaOfBasisDataOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam U a) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (basis : GradientBasisData U a) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x i) = -p + matVecMul sigmaStar⁻¹ (q + matVecMul kappa p)

theorem HCPolySupport.ScalarCanonicalMaximizer.averageFluxFormula {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q a) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (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 - matVecMul (matTranspose kappa) (matVecMul sigmaStar⁻¹ q) - matVecMul (bCoarse sigma sigmaStar kappa) p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageFluxFormulaOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {sigma sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam U a) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (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 - matVecMul (matTranspose kappa) (matVecMul sigmaStar⁻¹ q) - matVecMul (bCoarse sigma sigmaStar kappa) p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageFluxFormulaOfBasisData {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q a) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hInt : ResponseLinearIntegrabilityData U a) (basis : FluxBasisData U a) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x) i) = q - matVecMul (matTranspose kappa) (matVecMul sigmaStar⁻¹ q) - matVecMul (bCoarse sigma sigmaStar kappa) p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageFluxFormulaOfBasisDataOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {sigma sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam U a) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (basis : FluxBasisData U a) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x) i) = q - matVecMul (matTranspose kappa) (matVecMul sigmaStar⁻¹ q) - matVecMul (bCoarse sigma sigmaStar kappa) p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageGradientFormulaCanonical {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q 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 + matVecMul (sigmaStarInvCoarse U a) (q + matVecMul (kappaCoarse U a) p)

theorem HCPolySupport.ScalarCanonicalMaximizer.averageGradientFormulaCanonicalOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam U a) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (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 + matVecMul (sigmaStarInvCoarse U a) (q + matVecMul (kappaCoarse U a) p)

theorem HCPolySupport.ScalarCanonicalMaximizer.averageGradientFormulaCanonicalOfBasisData {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q a) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (hInt : ResponseLinearIntegrabilityData U a) (basis : GradientBasisData U a) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x i) = -p + matVecMul (sigmaStarInvCoarse U a) (q + matVecMul (kappaCoarse U a) p)

theorem HCPolySupport.ScalarCanonicalMaximizer.averageGradientFormulaCanonicalOfBasisDataOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam U a) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (basis : GradientBasisData U a) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x i) = -p + matVecMul (sigmaStarInvCoarse U a) (q + matVecMul (kappaCoarse U a) p)

theorem HCPolySupport.ScalarCanonicalMaximizer.averageFluxFormulaCanonical {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q 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 - matVecMul (matTranspose (kappaCoarse U a)) (matVecMul (sigmaStarInvCoarse U a) q) - matVecMul (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a)) p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageFluxFormulaCanonicalOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {sigma sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam 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)) (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 - matVecMul (matTranspose (kappaCoarse U a)) (matVecMul (sigmaStarInvCoarse U a) q) - matVecMul (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a)) p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageFluxFormulaCanonicalOfBasisData {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q 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) (basis : FluxBasisData U a) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x) i) = q - matVecMul (matTranspose (kappaCoarse U a)) (matVecMul (sigmaStarInvCoarse U a) q) - matVecMul (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a)) p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageFluxFormulaCanonicalOfBasisDataOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {sigma sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam 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)) (basis : FluxBasisData U a) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x) i) = q - matVecMul (matTranspose (kappaCoarse U a)) (matVecMul (sigmaStarInvCoarse U a) q) - matVecMul (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a)) p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageGradientFormulaDeterministicCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q 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 + matVecMul (deterministicCoarseBlockMatrix U a).lowerRight q - matVecMul (deterministicCoarseBlockMatrix U a).lowerLeft p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageGradientFormulaDeterministicCoarseBlockMatrixOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam U a) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (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 + matVecMul (deterministicCoarseBlockMatrix U a).lowerRight q - matVecMul (deterministicCoarseBlockMatrix U a).lowerLeft p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageGradientFormulaDeterministicCoarseBlockMatrixOfBasisData {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q a) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (hInt : ResponseLinearIntegrabilityData U a) (basis : GradientBasisData U a) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x i) = -p + matVecMul (deterministicCoarseBlockMatrix U a).lowerRight q - matVecMul (deterministicCoarseBlockMatrix U a).lowerLeft p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageGradientFormulaDeterministicCoarseBlockMatrixOfBasisDataOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam U a) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (basis : GradientBasisData U a) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x i) = -p + matVecMul (deterministicCoarseBlockMatrix U a).lowerRight q - matVecMul (deterministicCoarseBlockMatrix U a).lowerLeft p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageFluxFormulaDeterministicCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q 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 + matVecMul (deterministicCoarseBlockMatrix U a).upperRight q - matVecMul (deterministicCoarseBlockMatrix U a).upperLeft p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageFluxFormulaDeterministicCoarseBlockMatrixOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {sigma sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam 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)) (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 + matVecMul (deterministicCoarseBlockMatrix U a).upperRight q - matVecMul (deterministicCoarseBlockMatrix U a).upperLeft p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageFluxFormulaDeterministicCoarseBlockMatrixOfBasisData {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q 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) (basis : FluxBasisData U a) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x) i) = q + matVecMul (deterministicCoarseBlockMatrix U a).upperRight q - matVecMul (deterministicCoarseBlockMatrix U a).upperLeft p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageFluxFormulaDeterministicCoarseBlockMatrixOfBasisDataOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {sigma sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam 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)) (basis : FluxBasisData U a) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x) i) = q + matVecMul (deterministicCoarseBlockMatrix U a).upperRight q - matVecMul (deterministicCoarseBlockMatrix U a).upperLeft p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageGradientFormulaCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q 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 + matVecMul (coarseBlockMatrix U a).lowerRight q - matVecMul (coarseBlockMatrix U a).lowerLeft p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageGradientFormulaCoarseBlockMatrixOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam U a) (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (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 + matVecMul (coarseBlockMatrix U a).lowerRight q - matVecMul (coarseBlockMatrix U a).lowerLeft p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageGradientFormulaCoarseBlockMatrixOfBasisData {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q 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) (basis : GradientBasisData U a) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x i) = -p + matVecMul (coarseBlockMatrix U a).lowerRight q - matVecMul (coarseBlockMatrix U a).lowerLeft p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageGradientFormulaCoarseBlockMatrixOfBasisDataOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam U a) (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (basis : GradientBasisData U a) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x i) = -p + matVecMul (coarseBlockMatrix U a).lowerRight q - matVecMul (coarseBlockMatrix U a).lowerLeft p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageFluxFormulaCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q 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 + matVecMul (coarseBlockMatrix U a).upperRight q - matVecMul (coarseBlockMatrix U a).upperLeft p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageFluxFormulaCoarseBlockMatrixOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {sigma sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam U 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)) (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 + matVecMul (coarseBlockMatrix U a).upperRight q - matVecMul (coarseBlockMatrix U a).upperLeft p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageFluxFormulaCoarseBlockMatrixOfBasisData {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q 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) (basis : FluxBasisData U a) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x) i) = q + matVecMul (coarseBlockMatrix U a).upperRight q - matVecMul (coarseBlockMatrix U a).upperLeft p

theorem HCPolySupport.ScalarCanonicalMaximizer.averageFluxFormulaCoarseBlockMatrixOfBasisDataOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {sigma sigmaStar kappa : Mat d} (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam U 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)) (basis : FluxBasisData U a) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x) i) = q + matVecMul (coarseBlockMatrix U a).upperRight q - matVecMul (coarseBlockMatrix U a).upperLeft p

theorem HCPolySupport.ScalarCanonicalMaximizer.energyAverageGradientCanonicalOfIsSigmaStarCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {sigmaStar : Mat d} (hEll : IsEllipticFieldOn lam Lam U a) (hS : IsSigmaStarCoarse U a sigmaStar) (hdet : IsUnit (Matrix.det sigmaStar)) (hInt : ResponseLinearIntegrabilityData U a) (w : AHarmonicFunction a U) (v : ScalarCanonicalMaximizer U 0 (matVecMul (sigmaStarCoarse U a) fun (i : Fin d) => volumeAverage U fun (x : Vec d) => w.toH1.grad x i) a) : 1 / 2 * vecDot (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => w.toH1.grad x i) (matVecMul (sigmaStarCoarse U a) fun (i : Fin d) => volumeAverage U fun (x : Vec d) => w.toH1.grad x i) ≤ 1 / 2 * volumeAverage U (scalarVariationEnergyIntegrand a w)

theorem HCPolySupport.ScalarCanonicalMaximizer.energyAverageGradientCanonicalOfIsSigmaStarCoarseOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {sigmaStar : Mat d} (hEll : IsEllipticFieldOn lam Lam U a) (hS : IsSigmaStarCoarse U a sigmaStar) (hdet : IsUnit (Matrix.det sigmaStar)) (w : AHarmonicFunction a U) (v : ScalarCanonicalMaximizer U 0 (matVecMul (sigmaStarCoarse U a) fun (i : Fin d) => volumeAverage U fun (x : Vec d) => w.toH1.grad x i) a) : 1 / 2 * vecDot (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => w.toH1.grad x i) (matVecMul (sigmaStarCoarse U a) fun (i : Fin d) => volumeAverage U fun (x : Vec d) => w.toH1.grad x i) ≤ 1 / 2 * volumeAverage U (scalarVariationEnergyIntegrand a w)

theorem HCPolySupport.ScalarCanonicalMaximizer.energyAverageFluxCanonicalOfIsSigmaCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {sigma sigmaStar kappa : Mat d} (hEll : IsEllipticFieldOn lam Lam 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) (w : AHarmonicFunction a U) (v : ScalarCanonicalMaximizer U (-matVecMul (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a))⁻¹ fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x) i) 0 a) : 1 / 2 * vecDot (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x) i) (matVecMul (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a))⁻¹ fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x) i) ≤ 1 / 2 * volumeAverage U (scalarVariationEnergyIntegrand a w)

theorem HCPolySupport.ScalarCanonicalMaximizer.energyAverageFluxCanonicalOfIsSigmaCoarseOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {sigma sigmaStar kappa : Mat d} (hEll : IsEllipticFieldOn lam Lam 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)) (w : AHarmonicFunction a U) (v : ScalarCanonicalMaximizer U (-matVecMul (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a))⁻¹ fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x) i) 0 a) : 1 / 2 * vecDot (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x) i) (matVecMul (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a))⁻¹ fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x) i) ≤ 1 / 2 * volumeAverage U (scalarVariationEnergyIntegrand a w)