Coarse-graining support: Support.CoarseGraining.BlockResponse.Perturbation.PairHalfScalar #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
BlockResponse perturbation -- pair-half scalar decomposition #
Pointwise decomposition of blockResponse_integrand on pair-half states into the scalarResponse sum, and the resulting blockJValueSet membership lemmas including the responseJ-adjoint-sum and note-form witness theorems.
theorem
HCPolySupport.blockResponse_integrand_pair_half_eq_pointwise_split_of_pointwise_det
{d : ℕ}
(a : CoeffField d)
(p pStar q qStar : Vec d)
(ξ η : Vec d → Vec d)
(hdet : ∀ (x : Vec d), IsUnit (Matrix.det (symmPart (a x))))
:
blockResponseIntegrand a (p, q) (qStar, pStar)
((1 / 2) • { potential := fun (x : Vec d) => ξ x + η x,
flux := fun (x : Vec d) => matVecMul (a x) (ξ x) - matVecMul (matTranspose (a x)) (η x) }) = fun (x : Vec d) =>
1 / 2 * (-(1 / 2 * vecDot (ξ x) (matVecMul (symmPart (a x)) (ξ x))) - vecDot (p - pStar) (matVecMul (a x) (ξ x)) + vecDot (qStar - q) (ξ x)) + 1 / 2 * (-(1 / 2 * vecDot (η x) (matVecMul (symmPart (matTranspose (a x))) (η x))) - vecDot (pStar + p) (matVecMul (matTranspose (a x)) (η x)) + vecDot (qStar + q) (η x))
theorem
HCPolySupport.blockResponse_integrand_pair_half_eq_scalarResponse_sum_on_of_isEllipticFieldOn
{d : ℕ}
{U : Set (Vec d)}
(a : CoeffField d)
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U a)
(p pStar q qStar : Vec d)
(u : AHarmonicFunction a U)
(v : AHarmonicFunction (adjointCoeffField a) U)
(x : Vec d)
:
x ∈ U →
blockResponseIntegrand a (p, q) (qStar, pStar)
((1 / 2) • { potential := fun (y : Vec d) => u.toH1.grad y + v.toH1.grad y,
flux := fun (y : Vec d) => matVecMul (a y) (u.toH1.grad y) - matVecMul (matTranspose (a y)) (v.toH1.grad y) })
x = 1 / 2 * scalarResponseIntegrand U a (p - pStar) (qStar - q) u x + 1 / 2 * scalarResponseIntegrand U (adjointCoeffField a) (pStar + p) (qStar + q) v x
theorem
HCPolySupport.volumeAverage_halfBlockPair_eq_scalarResponseSum_of_ellipticity
{d : ℕ}
{U : Set (Vec d)}
(a : CoeffField d)
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hU : MeasurableSet U)
(hEll : IsEllipticFieldOn lam Lam U a)
(p pStar q qStar : Vec d)
(u : AHarmonicFunction a U)
(v : AHarmonicFunction (adjointCoeffField a) U)
:
volumeAverage U
(blockResponseIntegrand a (p, q) (qStar, pStar)
((1 / 2) • { potential := fun (x : Vec d) => u.toH1.grad x + v.toH1.grad x,
flux := fun (x : Vec d) =>
matVecMul (a x) (u.toH1.grad x) - matVecMul (matTranspose (a x)) (v.toH1.grad x) })) = 1 / 2 * volumeAverage U (scalarResponseIntegrand U a (p - pStar) (qStar - q) u) + 1 / 2 * volumeAverage U (scalarResponseIntegrand U (adjointCoeffField a) (pStar + p) (qStar + q) v)
theorem
HCPolySupport.blockResponse_half_scalarResponse_sum_mem_blockJValueSet_of_responseSpace_of_isEllipticFieldOn
{d : ℕ}
{U : Set (Vec d)}
(a : CoeffField d)
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hU : MeasurableSet U)
(hEll : IsEllipticFieldOn lam Lam U a)
(p pStar q qStar : Vec d)
(u : AHarmonicFunction a U)
(v : AHarmonicFunction (adjointCoeffField a) U)
(hX :
BlockResponseSpace a U
((1 / 2) • { potential := fun (x : Vec d) => u.toH1.grad x + v.toH1.grad x,
flux := fun (x : Vec d) => matVecMul (a x) (u.toH1.grad x) - matVecMul (matTranspose (a x)) (v.toH1.grad x) }))
:
1 / 2 * volumeAverage U (scalarResponseIntegrand U a (p - pStar) (qStar - q) u) + 1 / 2 * volumeAverage U (scalarResponseIntegrand U (adjointCoeffField a) (pStar + p) (qStar + q) v) ∈ blockJValueSet U (p, q) (qStar, pStar) a
theorem
HCPolySupport.blockResponse_half_scalarResponse_sum_mem_blockJValueSet_of_isEllipticFieldOn
{d : ℕ}
{U : Set (Vec d)}
(a : CoeffField d)
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hU : MeasurableSet U)
(hEll : IsEllipticFieldOn lam Lam U a)
(p pStar q qStar : Vec d)
(u : AHarmonicFunction a U)
(v : AHarmonicFunction (adjointCoeffField a) U)
:
1 / 2 * volumeAverage U (scalarResponseIntegrand U a (p - pStar) (qStar - q) u) + 1 / 2 * volumeAverage U (scalarResponseIntegrand U (adjointCoeffField a) (pStar + p) (qStar + q) v) ∈ blockJValueSet U (p, q) (qStar, pStar) a
theorem
HCPolySupport.blockResponse_half_responseJ_adjoint_sum_mem_blockJValueSet_of_isResponseMaximizer
{d : ℕ}
{U : Set (Vec d)}
(a : CoeffField d)
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hU : MeasurableSet U)
(hEll : IsEllipticFieldOn lam Lam U a)
(p pStar q qStar : Vec d)
(u : AHarmonicFunction a U)
(v : AHarmonicFunction (adjointCoeffField a) U)
(hmax : IsResponseMaximizer U (p - pStar) (qStar - q) a u)
(hmaxAdj : IsResponseMaximizer U (pStar + p) (qStar + q) (adjointCoeffField a) v)
:
theorem
HCPolySupport.blockResponse_half_responseJ_adjoint_sum_note_form_mem_blockJValueSet_of_isResponseMaximizer
{d : ℕ}
{U : Set (Vec d)}
(a : CoeffField d)
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hU : MeasurableSet U)
(hEll : IsEllipticFieldOn lam Lam U a)
(p q h : Vec d)
(u : AHarmonicFunction a U)
(v : AHarmonicFunction (adjointCoeffField a) U)
(hmax : IsResponseMaximizer U p (q - h) a u)
(hmaxAdj : IsResponseMaximizer U p (q + h) (adjointCoeffField a) v)
: