Coarse-graining support: Support.CoarseGraining.BlockResponse.Perturbation.ResponseJMuAdjoint #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
BlockResponse perturbation -- responseJ and mu-adjoint-sum family #
blockEnergyAverage = responseJ identities under pairingAverage and firstVariation hypotheses, the half-responseJ-sum reduction for isResponseMaximizer / scalarCanonicalMaximizer data, the upper bound on mu_zero_right against the half responseJ adjoint sum, and the corresponding blockJValueSet / blockJ membership / bound theorems.
theorem
HCPolySupport.blockEnergyAverage_blockResponseHalfState_eq_responseJ
{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)
(v : AHarmonicFunction (adjointCoeffField a) U)
(hpair :
(volumeAverage U fun (x : Vec d) =>
vecDot ((blockResponsePairHalfState a u v).potential x) ((blockResponsePairHalfState a u v).flux x)) = 0)
(hfirst : ∀ (w : AHarmonicFunction a U), volumeAverage U (scalarFirstVariationIntegrand U a p q u w) = 0)
:
Coupling lemma with arbitrary scalar response data.
theorem
HCPolySupport.blockEnergyAverage_blockResponseHalfState_eq_responseJ_sub_pairing
{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)
(v : AHarmonicFunction (adjointCoeffField a) U)
(pairing : ℝ)
(hpair :
(volumeAverage U fun (x : Vec d) =>
vecDot ((blockResponsePairHalfState a u v).potential x) ((blockResponsePairHalfState a u v).flux x)) = pairing)
(hfirst : ∀ (w : AHarmonicFunction a U), volumeAverage U (scalarFirstVariationIntegrand U a p q u w) = 0)
:
Coupling lemma with arbitrary scalar response data and nonzero average state-pairing. The pairing is exactly the correction term between the block half-pair energy and the scalar response value.
theorem
HCPolySupport.blockEnergyAverage_blockResponseHalfState_eq_responseJ_left_zero
{d : ℕ}
{U : Set (Vec d)}
(a : CoeffField d)
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hEll : IsEllipticFieldOn lam Lam U a)
(p : Vec d)
(u : AHarmonicFunction a U)
(v : AHarmonicFunction (adjointCoeffField a) U)
(hpair :
(volumeAverage U fun (x : Vec d) =>
vecDot ((blockResponsePairHalfState a u v).potential x) ((blockResponsePairHalfState a u v).flux x)) = 0)
(hfirst : ∀ (w : AHarmonicFunction a U), volumeAverage U (scalarFirstVariationIntegrand U a (-p) 0 u w) = 0)
:
Pure-gradient coupling: the recovered first variation appears at (-p,0),
and the final statement uses the quadratic evenness of ResponseJ in the
pure-gradient slice.
theorem
HCPolySupport.blockEnergyAverage_blockResponseHalfState_eq_responseJ_zero
{d : ℕ}
{U : Set (Vec d)}
(a : CoeffField d)
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hU : MeasurableSet U)
(hEll : IsEllipticFieldOn lam Lam U a)
(q : Vec d)
(u : AHarmonicFunction a U)
(v : AHarmonicFunction (adjointCoeffField a) U)
(hpair :
(volumeAverage U fun (x : Vec d) =>
vecDot ((blockResponsePairHalfState a u v).potential x) ((blockResponsePairHalfState a u v).flux x)) = 0)
(hfirst : ∀ (w : AHarmonicFunction a U), volumeAverage U (scalarFirstVariationIntegrand U a 0 q u w) = 0)
:
Coupling lemma for the pure-flux slice: if the half-pair has zero average
state-pairing and its primal scalar component satisfies the Euler-Lagrange
identity for ResponseJ U 0 q a, then the block half-pair energy is exactly
that scalar response value.
theorem
HCPolySupport.blockEnergyAverage_blockResponseHalfState_eq_half_responseJ_sum
{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 p' q' : Vec d)
(u : AHarmonicFunction a U)
(v : AHarmonicFunction (adjointCoeffField a) U)
(hmax : IsResponseMaximizer U p q a u)
(hmaxAdj : IsResponseMaximizer U p' q' (adjointCoeffField a) v)
:
blockEnergyAverage U a (blockResponsePairHalfState a u v) = 1 / 2 * ResponseJ U p q a + 1 / 2 * ResponseJ U p' q' (adjointCoeffField a)
If the two scalar inputs are response maximizers, the half-pair witness has block energy equal to one half of the sum of the corresponding response values.
theorem
HCPolySupport.blockEnergyAverage_blockResponseHalfState_eq_half_responseJ_sum_of_ellipticField
{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 p' q' : Vec d)
(u : ScalarCanonicalMaximizer U p q a)
(v : ScalarCanonicalMaximizer U p' q' (adjointCoeffField a))
:
blockEnergyAverage U a
(blockResponsePairHalfState a u.toAHarmonicFunctionMeanZero.toAHarmonicFunction
v.toAHarmonicFunctionMeanZero.toAHarmonicFunction) = 1 / 2 * ResponseJ U p q a + 1 / 2 * ResponseJ U p' q' (adjointCoeffField a)
Scalar canonical maximizers feed the previous half-pair energy identity without extra bookkeeping.
theorem
HCPolySupport.blockResponse_half_scalarResponse_sum_mem_blockJ
{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_scalarResponse_sum_le_blockJ_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)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(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) ≤ BlockJ U (p, q) (qStar, pStar) a
theorem
HCPolySupport.blockResponse_half_responseJ_adjoint_sum_note_form_mem_blockJValueSet
{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)
:
theorem
HCPolySupport.blockResponse_half_responseJ_adjoint_sum_le_blockJ_of_isResponseMaximizer_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)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(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_le_blockJ
{d : ℕ}
{U : Set (Vec d)}
(a : CoeffField d)
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hU : MeasurableSet U)
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(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)
:
theorem
HCPolySupport.blockResponse_half_responseJ_adjoint_sum_mem_blockJValueSet
{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 : ScalarCanonicalMaximizer U (p - pStar) (qStar - q) a)
(v : ScalarCanonicalMaximizer U (pStar + p) (qStar + q) (adjointCoeffField a))
:
theorem
HCPolySupport.blockResponse_half_responseJ_adjoint_sum_note_form_mem_of_ellipticField
{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 : ScalarCanonicalMaximizer U p (q - h) a)
(v : ScalarCanonicalMaximizer U p (q + h) (adjointCoeffField a))
:
theorem
HCPolySupport.blockResponse_half_adjointResponseJ_sum_le_blockJ_of_maximizers
{d : ℕ}
{U : Set (Vec d)}
(a : CoeffField d)
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hU : MeasurableSet U)
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(p pStar q qStar : Vec d)
(u : ScalarCanonicalMaximizer U (p - pStar) (qStar - q) a)
(v : ScalarCanonicalMaximizer U (pStar + p) (qStar + q) (adjointCoeffField a))
:
theorem
HCPolySupport.blockResponse_half_responseJ_adjoint_sum_note_form_le_blockJ_of_ellipticField
{d : ℕ}
{U : Set (Vec d)}
(a : CoeffField d)
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hU : MeasurableSet U)
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(p q h : Vec d)
(u : ScalarCanonicalMaximizer U p (q - h) a)
(v : ScalarCanonicalMaximizer U p (q + h) (adjointCoeffField a))
: