Coarse-graining support: Support.Internal.Ch02.DoubledResponse.ScalarMaximizers #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Scalar Maximizers and Doubled Maximizers #
This file is split mechanically out of Internal.Ch02.DoubledResponse.
theorem
HCPolySupport.Internal.Ch02.BookCh02.doubled_response_by_scalar_of_isEllipticFieldOn
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField)
(p pStar q qStar : Vec d)
:
theorem
HCPolySupport.Internal.Ch02.BookCh02.doubledFieldOfScalarMaximizers_eq_pairHalf
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(v : Book.Ch02.Solution U a)
(vStar : Book.Ch02.Solution U a.transpose)
:
Book.Ch02.doubledFieldOfScalarMaximizers a v vStar = doubledFieldOfBlockState (blockResponsePairHalfState a.toCoeffField v vStar)
theorem
HCPolySupport.Internal.Ch02.BookCh02.old_isResponseMaximizer_of_public
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(p q : Vec d)
(v : Book.Ch02.Solution U a)
(hv : Book.Ch02.IsResponseMaximizer U a p q v)
:
IsResponseMaximizer U.carrier p q a.toCoeffField v
theorem
HCPolySupport.Internal.Ch02.BookCh02.doubledResponseValue_scalarMaximizers_eq_scalar_responseJ_of_isEllipticFieldOn
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField)
(p pStar q qStar : Vec d)
(v : Book.Ch02.Solution U a)
(vStar : Book.Ch02.Solution U a.transpose)
(hv : Book.Ch02.IsResponseMaximizer U a (p - pStar) (qStar - q) v)
(hvStar : Book.Ch02.IsResponseMaximizer U a.transpose (pStar + p) (qStar + q) vStar)
:
Book.Ch02.doubledResponseValue U a (p, q) (qStar, pStar) (Book.Ch02.doubledFieldOfScalarMaximizers a v vStar) = 1 / 2 * Book.Ch02.responseJ U a (p - pStar) (qStar - q) + 1 / 2 * Book.Ch02.responseJ U a.transpose (pStar + p) (qStar + q)
theorem
HCPolySupport.Internal.Ch02.BookCh02.doubledResponseValue_eq_of_sameAE
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(P Q : BlockVec d)
{X Y : Book.Ch02.DoubledField d}
(hXY : X.SameAE Y)
:
theorem
HCPolySupport.Internal.Ch02.BookCh02.isDoubledResponseMaximizer_of_sameAE
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(P Q : BlockVec d)
{X Y : Book.Ch02.DoubledField d}
(hXY : X.SameAE Y)
(hY : Book.Ch02.IsDoubledResponseMaximizer U a P Q Y)
:
Book.Ch02.IsDoubledResponseMaximizer U a P Q X
theorem
HCPolySupport.Internal.Ch02.BookCh02.doubledResponseJ_eq_value_of_maximizer
{d : ℕ}
{U : Book.Ch02.Domain d}
{a : Book.Ch02.CoeffOn U}
{P Q : BlockVec d}
{X : Book.Ch02.DoubledField d}
(hX : Book.Ch02.IsDoubledResponseMaximizer U a P Q X)
:
theorem
HCPolySupport.Internal.Ch02.BookCh02.doubledResponseValue_scalarPair_eq_scalar_values_of_isEllipticFieldOn
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField)
(p pStar q qStar : Vec d)
(v : Book.Ch02.Solution U a)
(vStar : Book.Ch02.Solution U a.transpose)
:
Book.Ch02.doubledResponseValue U a (p, q) (qStar, pStar) (Book.Ch02.doubledFieldOfScalarMaximizers a v vStar) = 1 / 2 * volumeAverage U.carrier (scalarResponseIntegrand U.carrier a.toCoeffField (p - pStar) (qStar - q) v) + 1 / 2 * volumeAverage U.carrier
(scalarResponseIntegrand U.carrier (adjointCoeffField a.toCoeffField) (pStar + p) (qStar + q) vStar)
theorem
HCPolySupport.Internal.Ch02.BookCh02.old_isResponseMaximizer_of_value_eq_responseJ
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(p q : Vec d)
(v : AHarmonicFunction a U)
(hval : volumeAverage U (scalarResponseIntegrand U a p q v) = ResponseJ U p q a)
:
IsResponseMaximizer U p q a v
theorem
HCPolySupport.Internal.Ch02.BookCh02.public_isResponseMaximizer_of_old
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(p q : Vec d)
(v : Book.Ch02.Solution U a)
(hv : IsResponseMaximizer U.carrier p q a.toCoeffField v)
:
Book.Ch02.IsResponseMaximizer U a p q v
theorem
HCPolySupport.Internal.Ch02.BookCh02.doubledFieldOfScalarMaximizers_mem_responseField_of_isEllipticFieldOn
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField)
(v : Book.Ch02.Solution U a)
(vStar : Book.Ch02.Solution U a.transpose)
:
theorem
HCPolySupport.Internal.Ch02.BookCh02.scalar_maximizers_give_doubled_maximizer_of_isEllipticFieldOn
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField)
(p pStar q qStar : Vec d)
(v : Book.Ch02.Solution U a)
(vStar : Book.Ch02.Solution U a.transpose)
:
Book.Ch02.IsResponseMaximizer U a (p - pStar) (qStar - q) v →
Book.Ch02.IsResponseMaximizer U a.transpose (pStar + p) (qStar + q) vStar →
Book.Ch02.IsDoubledResponseMaximizer U a (p, q) (qStar, pStar) (Book.Ch02.doubledFieldOfScalarMaximizers a v vStar)
theorem
HCPolySupport.Internal.Ch02.BookCh02.maximizer_exists_of_isEllipticFieldOn
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField)
(P Q : BlockVec d)
:
theorem
HCPolySupport.Internal.Ch02.BookCh02.doubled_maximizer_sameAE_scalar_maximizers_of_isEllipticFieldOn
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField)
(p pStar q qStar : Vec d)
(X : Book.Ch02.DoubledField d)
:
Book.Ch02.IsDoubledResponseMaximizer U a (p, q) (qStar, pStar) X →
∃ (v : Book.Ch02.Solution U a) (vStar : Book.Ch02.Solution U a.transpose),
Book.Ch02.IsResponseMaximizer U a (p - pStar) (qStar - q) v ∧ Book.Ch02.IsResponseMaximizer U a.transpose (pStar + p) (qStar + q) vStar ∧ X.SameAE (Book.Ch02.doubledFieldOfScalarMaximizers a v vStar)