Coarse-graining support: Support.CoarseGraining.BlockResponse.Equalities.LowerImageNamespace #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
BlockResponse Equalities -- BlockResponseLowerImageMemVectorL2Data namespace #
blockJ le / eq half responseJ adjoint sum in the BlockResponseLowerImageMemVectorL2Data namespace (with and without hodgeConverseCriterion / IsOpenBoundedConvexDomain), the blockJ eq half scalarResponse sum for scalarCanonicalMaximizers, plus the trailing blockResponse integrand_add / blockJValueSet membership and blockJ_nonneg lemmas.
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.blockJ_le_half_responseJ_adjoint_sum_of_isEllipticFieldOn
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
[HasHodgeConverse U]
(hU : MeasurableSet U)
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(p pStar q qStar : Vec d)
:
Lower-level Hodge-packaged upper bound for the doubled response functional.
For note-facing Chapter 2 statements on bounded open convex domains, prefer
blockJ_le_half_responseJ_adjoint_sum_of_isEllipticFieldOn_of_isOpenBoundedConvexDomain.
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.blockJ_le_half_responseJ_adjoint_sum_of_isEllipticFieldOn_of_hodgeConverseCriterion
{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)
(hHodge : HodgeConverseCriterion U)
(p pStar q qStar : Vec d)
:
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.blockJ_le_half_adjointResponseSum
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hConv : IsOpenBoundedConvexDomain U)
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(p pStar q qStar : Vec d)
:
Preferred note-facing lower-image-packaged upper bound for the doubled response functional on bounded open convex domains.
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.blockJ_note_form_le_half_responseJ_adjoint_sum_of_isEllipticFieldOn
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
[HasHodgeConverse U]
(hU : MeasurableSet U)
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(p q h : Vec d)
:
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.blockJ_note_le_half_adjointResponseSum_of_HodgeConverse
{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)
(hHodge : HodgeConverseCriterion U)
(p q h : Vec d)
:
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.blockJ_note_le_half_adjointResponseSum_of_ConvexDomain
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hConv : IsOpenBoundedConvexDomain U)
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(p q h : Vec d)
:
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.half_responseJ_adjoint_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)
:
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.half_responseJ_adjoint_sum_note_form_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 q h : Vec d)
:
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.blockJ_eq_half_responseJ_adjoint_sum_of_isEllipticFieldOn
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
[HasHodgeConverse U]
(hU : MeasurableSet U)
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(p pStar q qStar : Vec d)
:
Lower-level Hodge-packaged equality
BlockJ = (1/2)(ResponseJ + ResponseJ^*). For note-facing Chapter 2
statements on bounded open convex domains, prefer
blockJ_eq_half_responseJ_adjoint_sum_of_isEllipticFieldOn_of_isOpenBoundedConvexDomain.
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.blockJ_eq_half_responseJ_adjoint_sum_of_isEllipticFieldOn_of_hodgeConverseCriterion
{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)
(hHodge : HodgeConverseCriterion U)
(p pStar q qStar : Vec d)
:
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.blockJ_eq_half_adjointResponseSum_of_ConvexDomain
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hConv : IsOpenBoundedConvexDomain U)
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(p pStar q qStar : Vec d)
:
Preferred note-facing lower-image-packaged equality
BlockJ = (1/2)(ResponseJ + ResponseJ^*) on bounded open convex domains.
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.blockJ_note_form_eq_half_responseJ_adjoint_sum_of_isEllipticFieldOn
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
[HasHodgeConverse U]
(hU : MeasurableSet U)
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(p q h : Vec d)
:
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.blockJ_note_eq_half_adjointResponseSum_of_HodgeConverse
{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)
(hHodge : HodgeConverseCriterion U)
(p q h : Vec d)
:
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.blockJ_note_eq_half_adjointResponseSum_of_ConvexDomain
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hConv : IsOpenBoundedConvexDomain U)
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(p q h : Vec d)
:
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.blockJ_eq_half_scalarResponse_sum_of_scalarCanonicalMaximizers_of_isEllipticFieldOn
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
[HasHodgeConverse 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))
:
BlockJ U (p, q) (qStar, pStar) a = 1 / 2 * volumeAverage U
(scalarResponseIntegrand U a (p - pStar) (qStar - q) u.toAHarmonicFunctionMeanZero.toAHarmonicFunction) + 1 / 2 * volumeAverage U
(scalarResponseIntegrand U (adjointCoeffField a) (pStar + p) (qStar + q)
v.toAHarmonicFunctionMeanZero.toAHarmonicFunction)
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.blockJ_eq_half_scalarResponse_sum_of_scalarCanonicalMaximizers
{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)
(hHodge : HodgeConverseCriterion U)
(p pStar q qStar : Vec d)
(u : ScalarCanonicalMaximizer U (p - pStar) (qStar - q) a)
(v : ScalarCanonicalMaximizer U (pStar + p) (qStar + q) (adjointCoeffField a))
:
BlockJ U (p, q) (qStar, pStar) a = 1 / 2 * volumeAverage U
(scalarResponseIntegrand U a (p - pStar) (qStar - q) u.toAHarmonicFunctionMeanZero.toAHarmonicFunction) + 1 / 2 * volumeAverage U
(scalarResponseIntegrand U (adjointCoeffField a) (pStar + p) (qStar + q)
v.toAHarmonicFunctionMeanZero.toAHarmonicFunction)
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.blockJ_eq_half_scalarResponse_sum_of_scalarCanonicalMaximizers_of_ellipticField
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hConv : IsOpenBoundedConvexDomain 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))
:
BlockJ U (p, q) (qStar, pStar) a = 1 / 2 * volumeAverage U
(scalarResponseIntegrand U a (p - pStar) (qStar - q) u.toAHarmonicFunctionMeanZero.toAHarmonicFunction) + 1 / 2 * volumeAverage U
(scalarResponseIntegrand U (adjointCoeffField a) (pStar + p) (qStar + q)
v.toAHarmonicFunctionMeanZero.toAHarmonicFunction)
Preferred note-facing scalar-canonical lower-image-packaged equality on bounded open convex domains.
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.blockJ_eq_half_scalarResponse_sum_of_isEllipticFieldOn_of_isOpenBoundedConvexDomain
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hConv : IsOpenBoundedConvexDomain 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)),
BlockJ U (p, q) (qStar, pStar) a = 1 / 2 * volumeAverage U
(scalarResponseIntegrand U a (p - pStar) (qStar - q) u.toAHarmonicFunctionMeanZero.toAHarmonicFunction) + 1 / 2 * volumeAverage U
(scalarResponseIntegrand U (adjointCoeffField a) (pStar + p) (qStar + q)
v.toAHarmonicFunctionMeanZero.toAHarmonicFunction)
Witness-free convex-domain scalar-response equality: the maximizing scalar states are chosen internally from the direct-method existence theorem. This is the preferred Chapter-2-facing surface when one wants the scalar-response decomposition without threading explicit maximizer data through the statement.
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.exists_scalarCanonicalMaximizers_blockJ_eq_half_scalarResponse_sum
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hConv : IsOpenBoundedConvexDomain 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)),
BlockJ U (p, q) (qStar, pStar) a = 1 / 2 * volumeAverage U
(scalarResponseIntegrand U a (p - pStar) (qStar - q) u.toAHarmonicFunctionMeanZero.toAHarmonicFunction) + 1 / 2 * volumeAverage U
(scalarResponseIntegrand U (adjointCoeffField a) (pStar + p) (qStar + q)
v.toAHarmonicFunctionMeanZero.toAHarmonicFunction)
Explicitly named existential version of the previous theorem.
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.blockJ_note_form_eq_half_scalarResponse_sum_of_scalarCanonicalMaximizers_of_isEllipticFieldOn
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
[HasHodgeConverse 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))
:
BlockJ U (p, h) (q, 0) a = 1 / 2 * volumeAverage U (scalarResponseIntegrand U a p (q - h) u.toAHarmonicFunctionMeanZero.toAHarmonicFunction) + 1 / 2 * volumeAverage U
(scalarResponseIntegrand U (adjointCoeffField a) p (q + h) v.toAHarmonicFunctionMeanZero.toAHarmonicFunction)
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.blockJ_note_form_eq_half_scalarResponse_sum_of_scalarCanonicalMaximizers
{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)
(hHodge : HodgeConverseCriterion U)
(p q h : Vec d)
(u : ScalarCanonicalMaximizer U p (q - h) a)
(v : ScalarCanonicalMaximizer U p (q + h) (adjointCoeffField a))
:
BlockJ U (p, h) (q, 0) a = 1 / 2 * volumeAverage U (scalarResponseIntegrand U a p (q - h) u.toAHarmonicFunctionMeanZero.toAHarmonicFunction) + 1 / 2 * volumeAverage U
(scalarResponseIntegrand U (adjointCoeffField a) p (q + h) v.toAHarmonicFunctionMeanZero.toAHarmonicFunction)
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.blockJ_note_form_eq_half_scalarResponse_sum_of_of_scalarCanonicalMaximizers
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hConv : IsOpenBoundedConvexDomain 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))
:
BlockJ U (p, h) (q, 0) a = 1 / 2 * volumeAverage U (scalarResponseIntegrand U a p (q - h) u.toAHarmonicFunctionMeanZero.toAHarmonicFunction) + 1 / 2 * volumeAverage U
(scalarResponseIntegrand U (adjointCoeffField a) p (q + h) v.toAHarmonicFunctionMeanZero.toAHarmonicFunction)
Preferred note-facing scalar-canonical lower-image-packaged equality in the note form on bounded open convex domains.
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.blockJ_note_form_eq_half_scalarResponse_sum_of_isEllipticFieldOn_of_isOpenBoundedConvexDomain
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hConv : IsOpenBoundedConvexDomain 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)),
BlockJ U (p, h) (q, 0) a = 1 / 2 * volumeAverage U (scalarResponseIntegrand U a p (q - h) u.toAHarmonicFunctionMeanZero.toAHarmonicFunction) + 1 / 2 * volumeAverage U
(scalarResponseIntegrand U (adjointCoeffField a) p (q + h) v.toAHarmonicFunctionMeanZero.toAHarmonicFunction)
Witness-free convex-domain note-form scalar-response equality. The scalar canonical maximizers are obtained internally, so downstream arguments can consume the decomposition without packaging explicit maximizer witnesses.
theorem
HCPolySupport.BlockResponseLowerImageMemVectorL2Data.exists_scalarCanonicalMaximizers_blockJ_note_form_eq_half_scalarResponse_sum
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hConv : IsOpenBoundedConvexDomain 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)),
BlockJ U (p, h) (q, 0) a = 1 / 2 * volumeAverage U (scalarResponseIntegrand U a p (q - h) u.toAHarmonicFunctionMeanZero.toAHarmonicFunction) + 1 / 2 * volumeAverage U
(scalarResponseIntegrand U (adjointCoeffField a) p (q + h) v.toAHarmonicFunctionMeanZero.toAHarmonicFunction)
Explicitly named existential version of the previous theorem.
theorem
HCPolySupport.blockResponse_integrand_add
{d : ℕ}
(a : CoeffField d)
(P Q : BlockVec d)
(X Y : BlockState d)
:
blockResponseIntegrand a P Q (X + Y) = fun (x : Vec d) =>
blockResponseIntegrand a P Q X x + blockResponseIntegrand a P Q Y x - blockVecDot (Y.eval x) (blockMatVecMul (blockCoeffField a x) (X.eval x))
theorem
HCPolySupport.blockResponse_integrand_add_smul
{d : ℕ}
(a : CoeffField d)
(P Q : BlockVec d)
(X Y : BlockState d)
(c : ℝ)
:
blockResponseIntegrand a P Q (X + c • Y) = fun (x : Vec d) =>
blockResponseIntegrand a P Q X x - c ^ 2 * blockEnergyDensity a Y x - c * blockVecDot P (blockMatVecMul (blockCoeffField a x) (Y.eval x)) + c * blockVecDot Q (Y.eval x) - c * blockVecDot (Y.eval x) (blockMatVecMul (blockCoeffField a x) (X.eval x))
theorem
HCPolySupport.blockResponse_mem_blockJValueSet
{d : ℕ}
{U : Set (Vec d)}
{P Q : BlockVec d}
{a : CoeffField d}
{X : BlockState d}
(hX : BlockResponseSpace a U X)
(hInt : BlockResponseIntegrabilityData U a X)
:
theorem
HCPolySupport.blockResponse_blockJValueSet_smul_mem
{d : ℕ}
{U : Set (Vec d)}
{P Q : BlockVec d}
{a : CoeffField d}
{m : ℝ}
(hm : m ∈ blockJValueSet U P Q a)
(c : ℝ)
:
theorem
HCPolySupport.blockResponse_zero_mem_blockJValueSet
{d : ℕ}
(U : Set (Vec d))
(P Q : BlockVec d)
(a : CoeffField d)
:
theorem
HCPolySupport.blockResponse_blockJValueSet_nonempty
{d : ℕ}
(U : Set (Vec d))
(P Q : BlockVec d)
(a : CoeffField d)
:
(blockJValueSet U P Q a).Nonempty
theorem
HCPolySupport.blockJ_nonneg
{d : ℕ}
(U : Set (Vec d))
(P Q : BlockVec d)
(a : CoeffField d)
: