Coarse-graining support: Support.CoarseGraining.ResponseIdentities.AverageFormulas.CoarseFormulas

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

Average formulas (part 2) -- sigma-coarse formulas

energy-average / responseJ-zero formulas under IsSigmaStarCoarse and IsSigmaCoarse, their deterministicCoarseBlockMatrix / coarseBlockMatrix variants, and the corresponding average-gradient / average-flux formula theorems for IsResponseMaximizer data.

theorem HCPolySupport.basic_cg_identities_energy_average_gradient_canonical_of_isSigmaStarCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) {sigmaStar : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hdet : IsUnit (Matrix.det sigmaStar)) (hInt : ResponseLinearIntegrabilityData U a) (w u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U 0 (matVecMul (sigmaStarCoarse U a) fun (i : Fin d) => volumeAverage U fun (x : Vec d) => w.toH1.grad x i) a u) : 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.basic_cg_identities_energy_average_gradient_canonical_of_isSigmaStarCoarse_of_isEllipticFieldOn {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) {sigmaStar : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hdet : IsUnit (Matrix.det sigmaStar)) (w u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U 0 (matVecMul (sigmaStarCoarse U a) fun (i : Fin d) => volumeAverage U fun (x : Vec d) => w.toH1.grad x i) a u) : 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.responseJ_zero_eq_half_bCoarse_of_isSigmaCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (p : Vec d) : ResponseJ U p 0 a = 1 / 2 * vecDot p (matVecMul (bCoarse sigma sigmaStar kappa) p)

theorem HCPolySupport.basic_cg_identities_responseJ_zero_formula_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (p : Vec d) : ResponseJ U p 0 a = 1 / 2 * vecDot p (matVecMul (bCoarse sigma sigmaStar kappa) p)

theorem HCPolySupport.basic_cg_identities_responseJ_zero_formula_canonical_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)) (p : Vec d) : ResponseJ U p 0 a = 1 / 2 * vecDot p (matVecMul (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a)) p)

theorem HCPolySupport.basic_cg_identities_energy_average_flux_canonical_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) {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)) (hInt : ResponseLinearIntegrabilityData U a) (w u : AHarmonicFunction a U) (hmax : IsResponseMaximizer 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 u) : 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.basic_cg_identities_energy_average_flux_canonical_of_isSigmaCoarse_of_isEllipticFieldOn {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) {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)) (w u : AHarmonicFunction a U) (hmax : IsResponseMaximizer 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 u) : 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.basic_cg_identities_responseJ_zero_formula_deterministicCoarseBlockMatrix_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)) (p : Vec d) : ResponseJ U p 0 a = 1 / 2 * vecDot p (matVecMul (deterministicCoarseBlockMatrix U a).upperLeft p)

theorem HCPolySupport.basic_cg_identities_responseJ_zero_formula_coarseBlockMatrix_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (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)) (p : Vec d) : ResponseJ U p 0 a = 1 / 2 * vecDot p (matVecMul (coarseBlockMatrix U a).upperLeft p)

theorem HCPolySupport.basic_cg_identities_responseJ_formula_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) (p q : Vec d) : ResponseJ U p q a = 1 / 2 * vecDot q (matVecMul sigmaStar⁻¹ q) - vecDot p q + vecDot q (matVecMul sigmaStar⁻¹ (matVecMul kappa p)) + 1 / 2 * vecDot p (matVecMul (bCoarse sigma sigmaStar kappa) p)

theorem HCPolySupport.basic_cg_identities_responseJ_formula_canonical_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)) (p q : Vec d) : ResponseJ U p q a = 1 / 2 * vecDot q (matVecMul (sigmaStarInvCoarse U a) q) - vecDot p q + vecDot q (matVecMul (sigmaStarInvCoarse U a) (matVecMul (kappaCoarse U a) p)) + 1 / 2 * vecDot p (matVecMul (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a)) p)

theorem HCPolySupport.basic_cg_identities_responseJ_formula_deterministicCoarseBlockMatrix_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)) (p q : Vec d) : ResponseJ U p q a = 1 / 2 * vecDot q (matVecMul (deterministicCoarseBlockMatrix U a).lowerRight q) - vecDot p q - vecDot q (matVecMul (deterministicCoarseBlockMatrix U a).lowerLeft p) + 1 / 2 * vecDot p (matVecMul (deterministicCoarseBlockMatrix U a).upperLeft p)

theorem HCPolySupport.basic_cg_identities_responseJ_formula_coarseBlockMatrix_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (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)) (p q : Vec d) : ResponseJ U p q a = 1 / 2 * vecDot q (matVecMul (coarseBlockMatrix U a).lowerRight q) - vecDot p q - vecDot q (matVecMul (coarseBlockMatrix U a).lowerLeft p) + 1 / 2 * vecDot p (matVecMul (coarseBlockMatrix U a).upperLeft p)

theorem HCPolySupport.basic_cg_identities_average_gradient_formula_of_isResponseMaximizer {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (p q : Vec d) (hInt : ResponseLinearIntegrabilityData U a) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (uGrad : Fin d → AHarmonicFunction a U) (hmaxGrad : ∀ (i : Fin d), IsResponseMaximizer U 0 (Pi.single i 1) a (uGrad i)) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => u.toH1.grad x i) = -p + matVecMul sigmaStar⁻¹ (q + matVecMul kappa p)

theorem HCPolySupport.basic_cg_identities_average_flux_formula_of_isResponseMaximizer {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) (p q : Vec d) (hInt : ResponseLinearIntegrabilityData U a) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (uFlux : Fin d → AHarmonicFunction a U) (hmaxFlux : ∀ (i : Fin d), IsResponseMaximizer U (Pi.single i 1) 0 a (uFlux i)) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (u.toH1.grad x) i) = q - matVecMul (matTranspose kappa) (matVecMul sigmaStar⁻¹ q) - matVecMul (bCoarse sigma sigmaStar kappa) p

theorem HCPolySupport.basic_cg_identities_average_gradient_formula_canonical_of_isResponseMaximizer {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)) (p q : Vec d) (hInt : ResponseLinearIntegrabilityData U a) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (uGrad : Fin d → AHarmonicFunction a U) (hmaxGrad : ∀ (i : Fin d), IsResponseMaximizer U 0 (Pi.single i 1) a (uGrad i)) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => u.toH1.grad x i) = -p + matVecMul (sigmaStarInvCoarse U a) (q + matVecMul (kappaCoarse U a) p)

theorem HCPolySupport.basic_cg_identities_average_flux_formula_canonical_of_isResponseMaximizer {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)) (p q : Vec d) (hInt : ResponseLinearIntegrabilityData U a) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (uFlux : Fin d → AHarmonicFunction a U) (hmaxFlux : ∀ (i : Fin d), IsResponseMaximizer U (Pi.single i 1) 0 a (uFlux i)) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (u.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.averageGradient_eq_deterministicFormula_of_responseMaximizer {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)) (p q : Vec d) (hInt : ResponseLinearIntegrabilityData U a) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (uGrad : Fin d → AHarmonicFunction a U) (hmaxGrad : ∀ (i : Fin d), IsResponseMaximizer U 0 (Pi.single i 1) a (uGrad i)) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => u.toH1.grad x i) = -p + matVecMul (deterministicCoarseBlockMatrix U a).lowerRight q - matVecMul (deterministicCoarseBlockMatrix U a).lowerLeft p

theorem HCPolySupport.basic_cg_identities_average_flux_formula_deterministicCoarseBlockMatrix_of_isResponseMaximizer {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)) (p q : Vec d) (hInt : ResponseLinearIntegrabilityData U a) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (uFlux : Fin d → AHarmonicFunction a U) (hmaxFlux : ∀ (i : Fin d), IsResponseMaximizer U (Pi.single i 1) 0 a (uFlux i)) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (u.toH1.grad x) i) = q + matVecMul (deterministicCoarseBlockMatrix U a).upperRight q - matVecMul (deterministicCoarseBlockMatrix U a).upperLeft p

theorem HCPolySupport.basic_cg_identities_average_gradient_formula_coarseBlockMatrix_of_isResponseMaximizer {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (p q : Vec d) (hInt : ResponseLinearIntegrabilityData U a) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (uGrad : Fin d → AHarmonicFunction a U) (hmaxGrad : ∀ (i : Fin d), IsResponseMaximizer U 0 (Pi.single i 1) a (uGrad i)) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => u.toH1.grad x i) = -p + matVecMul (coarseBlockMatrix U a).lowerRight q - matVecMul (coarseBlockMatrix U a).lowerLeft p

theorem HCPolySupport.basic_cg_identities_average_flux_formula_coarseBlockMatrix_of_isResponseMaximizer {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (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)) (p q : Vec d) (hInt : ResponseLinearIntegrabilityData U a) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (uFlux : Fin d → AHarmonicFunction a U) (hmaxFlux : ∀ (i : Fin d), IsResponseMaximizer U (Pi.single i 1) 0 a (uFlux i)) : (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (u.toH1.grad x) i) = q + matVecMul (coarseBlockMatrix U a).upperRight q - matVecMul (coarseBlockMatrix U a).upperLeft p