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

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

Average formulas (part 1) -- basic variation and pairing identities

basic_cg_identities_linear_response (sq and linear form), average-pairing and polarization identities, and the average-gradient / average-flux coordinate / vector identities for IsResponseMaximizer data.

theorem HCPolySupport.basic_cg_identities_linear_response_sq_of_isResponseMaximizer {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (p q : Vec d) (hInt : ResponseLinearIntegrabilityData U a) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (w : AHarmonicFunction a U) : ((volumeAverage U fun (x : Vec d) => vecDot q (w.toH1.grad x)) - volumeAverage U fun (x : Vec d) => vecDot p (matVecMul (a x) (w.toH1.grad x))) ^ 2 ≤ volumeAverage U (scalarVariationEnergyIntegrand a w) * (2 * ResponseJ U p q a)

theorem HCPolySupport.basic_cg_identities_linear_response_sq_of_isResponseMaximizer_of_isEllipticFieldOn {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) (p q : Vec d) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (w : AHarmonicFunction a U) : ((volumeAverage U fun (x : Vec d) => vecDot q (w.toH1.grad x)) - volumeAverage U fun (x : Vec d) => vecDot p (matVecMul (a x) (w.toH1.grad x))) ^ 2 ≤ volumeAverage U (scalarVariationEnergyIntegrand a w) * (2 * ResponseJ U p q a)

theorem HCPolySupport.basic_cg_identities_linear_response_of_isResponseMaximizer {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (p q : Vec d) (hInt : ResponseLinearIntegrabilityData U a) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (w : AHarmonicFunction a U) : |(volumeAverage U fun (x : Vec d) => vecDot q (w.toH1.grad x)) - volumeAverage U fun (x : Vec d) => vecDot p (matVecMul (a x) (w.toH1.grad x))| ≤ √(volumeAverage U (scalarVariationEnergyIntegrand a w)) * √(2 * ResponseJ U p q a)

theorem HCPolySupport.basic_cg_identities_linear_response_of_isResponseMaximizer_of_isEllipticFieldOn {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) (p q : Vec d) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (w : AHarmonicFunction a U) : |(volumeAverage U fun (x : Vec d) => vecDot q (w.toH1.grad x)) - volumeAverage U fun (x : Vec d) => vecDot p (matVecMul (a x) (w.toH1.grad x))| ≤ √(volumeAverage U (scalarVariationEnergyIntegrand a w)) * √(2 * ResponseJ U p q a)

theorem HCPolySupport.basic_cg_identities_average_pairing_eq_vecDot_average_gradient_sub_average_flux {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (p q : Vec d) (hInt : ResponseLinearIntegrabilityData U a) (w : AHarmonicFunction a U) : ((volumeAverage U fun (x : Vec d) => vecDot q (w.toH1.grad x)) - volumeAverage U fun (x : Vec d) => vecDot p (matVecMul (a x) (w.toH1.grad x))) = (vecDot q fun (i : Fin d) => volumeAverage U fun (x : Vec d) => w.toH1.grad x i) - vecDot p fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x) i

theorem HCPolySupport.averagePairing_eq_averageGradient_minusFlux_of_ellipticity {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) (p q : Vec d) (w : AHarmonicFunction a U) : ((volumeAverage U fun (x : Vec d) => vecDot q (w.toH1.grad x)) - volumeAverage U fun (x : Vec d) => vecDot p (matVecMul (a x) (w.toH1.grad x))) = (vecDot q fun (i : Fin d) => volumeAverage U fun (x : Vec d) => w.toH1.grad x i) - vecDot p fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x) i

theorem HCPolySupport.basic_cg_identities_polarization_of_isResponseMaximizer {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (p q p' q' : Vec d) (hInt : ResponseLinearIntegrabilityData U a) (u u' : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (hmax' : IsResponseMaximizer U p' q' a u') : (volumeAverage U fun (x : Vec d) => vecDot (u'.toH1.grad x) (matVecMul (symmPart (a x)) (u.toH1.grad x))) = ResponseJ U p q a + ResponseJ U p' q' a - ResponseJ U (p - p') (q - q') a

theorem HCPolySupport.basic_cg_identities_polarization_of_isResponseMaximizer_of_isEllipticFieldOn {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) (p q p' q' : Vec d) (u u' : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (hmax' : IsResponseMaximizer U p' q' a u') : (volumeAverage U fun (x : Vec d) => vecDot (u'.toH1.grad x) (matVecMul (symmPart (a x)) (u.toH1.grad x))) = ResponseJ U p q a + ResponseJ U p' q' a - ResponseJ U (p - p') (q - q') a

theorem HCPolySupport.basic_cg_identities_average_pairing_of_isResponseMaximizer {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (p q p' q' : Vec d) (hInt : ResponseLinearIntegrabilityData U a) (u u' : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (hmax' : IsResponseMaximizer U p' q' a u') : ((volumeAverage U fun (x : Vec d) => vecDot q' (u.toH1.grad x)) - volumeAverage U fun (x : Vec d) => vecDot p' (matVecMul (a x) (u.toH1.grad x))) = ResponseJ U p q a + ResponseJ U p' q' a - ResponseJ U (p - p') (q - q') a

theorem HCPolySupport.basic_cg_identities_average_pairing_of_isResponseMaximizer_of_isEllipticFieldOn {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) (p q p' q' : Vec d) (u u' : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (hmax' : IsResponseMaximizer U p' q' a u') : ((volumeAverage U fun (x : Vec d) => vecDot q' (u.toH1.grad x)) - volumeAverage U fun (x : Vec d) => vecDot p' (matVecMul (a x) (u.toH1.grad x))) = ResponseJ U p q a + ResponseJ U p' q' a - ResponseJ U (p - p') (q - q') a

theorem HCPolySupport.basic_cg_identities_average_gradient_coordinate_of_isResponseMaximizer {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (p q : Vec d) (hInt : ResponseLinearIntegrabilityData U a) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (i : Fin d) (u' : AHarmonicFunction a U) (hmax' : IsResponseMaximizer U 0 (Pi.single i 1) a u') : (volumeAverage U fun (x : Vec d) => u.toH1.grad x i) = ResponseJ U p q a + ResponseJ U 0 (Pi.single i 1) a - ResponseJ U p (q - Pi.single i 1) a

theorem HCPolySupport.basic_cg_identities_average_gradient_coordinate_of_isResponseMaximizer_of_isEllipticFieldOn {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) (p q : Vec d) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (i : Fin d) (u' : AHarmonicFunction a U) (hmax' : IsResponseMaximizer U 0 (Pi.single i 1) a u') : (volumeAverage U fun (x : Vec d) => u.toH1.grad x i) = ResponseJ U p q a + ResponseJ U 0 (Pi.single i 1) a - ResponseJ U p (q - Pi.single i 1) a

theorem HCPolySupport.basic_cg_identities_average_flux_coordinate_of_isResponseMaximizer {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (p q : Vec d) (hInt : ResponseLinearIntegrabilityData U a) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (i : Fin d) (u' : AHarmonicFunction a U) (hmax' : IsResponseMaximizer U (Pi.single i 1) 0 a u') : (volumeAverage U fun (x : Vec d) => matVecMul (a x) (u.toH1.grad x) i) = ResponseJ U (p - Pi.single i 1) q a - ResponseJ U p q a - ResponseJ U (Pi.single i 1) 0 a

theorem HCPolySupport.basic_cg_identities_average_flux_coordinate_of_isResponseMaximizer_of_isEllipticFieldOn {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) (p q : Vec d) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (i : Fin d) (u' : AHarmonicFunction a U) (hmax' : IsResponseMaximizer U (Pi.single i 1) 0 a u') : (volumeAverage U fun (x : Vec d) => matVecMul (a x) (u.toH1.grad x) i) = ResponseJ U (p - Pi.single i 1) q a - ResponseJ U p q a - ResponseJ U (Pi.single i 1) 0 a

theorem HCPolySupport.basic_cg_identities_average_gradient_of_isResponseMaximizer {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (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) = 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.basic_cg_identities_average_gradient_of_isResponseMaximizer_of_isEllipticFieldOn {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) (p q : Vec d) (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) = 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.basic_cg_identities_average_flux_of_isResponseMaximizer {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (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) = 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.basic_cg_identities_average_flux_of_isResponseMaximizer_of_isEllipticFieldOn {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) (p q : Vec d) (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) = 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