Coarse-graining support: Support.Book.Ch02.Theorems.DoubledResponseDefinitions

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

theorem HCPolySupport.Book.Ch02.DoubledField.SameAE.refl {d : ℕ} {U : Domain d} (X : DoubledField d) : X.SameAE X

theorem HCPolySupport.Book.Ch02.DoubledField.SameAE.symm {d : ℕ} {U : Domain d} {X Y : DoubledField d} (hXY : X.SameAE Y) : Y.SameAE X

theorem HCPolySupport.Book.Ch02.DoubledField.SameAE.trans {d : ℕ} {U : Domain d} {X Y Z : DoubledField d} (hXY : X.SameAE Y) (hYZ : Y.SameAE Z) : X.SameAE Z

theorem HCPolySupport.Book.Ch02.DoubledField.SameAE.add {d : ℕ} {U : Domain d} {X1 X2 Y1 Y2 : DoubledField d} (hX : X1.SameAE X2) (hY : Y1.SameAE Y2) : (X1 + Y1).SameAE (X2 + Y2)

theorem HCPolySupport.Book.Ch02.DoubledField.SameAE.smul {d : ℕ} {U : Domain d} (c : ℝ) {X Y : DoubledField d} (hXY : X.SameAE Y) : (c • X).SameAE (c • Y)

theorem HCPolySupport.Book.Ch02.doubledResponseIntegrand_ae_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (P Q : BlockVec d) (X : DoubledField d) : doubledResponseIntegrand U a P Q X =ᵐ[volumeMeasureOn U.carrier] doubledResponseIntegrand U b P Q X

theorem HCPolySupport.Book.Ch02.doubledResponseValue_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (P Q : BlockVec d) (X : DoubledField d) : doubledResponseValue U a P Q X = doubledResponseValue U b P Q X

theorem HCPolySupport.Book.Ch02.IsDoubledResponseField.ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) {X : DoubledField d} (hX : IsDoubledResponseField U a X) : IsDoubledResponseField U b X

theorem HCPolySupport.Book.Ch02.doubledResponseValueSet_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (P Q : BlockVec d) : doubledResponseValueSet U a P Q = doubledResponseValueSet U b P Q

theorem HCPolySupport.Book.Ch02.doubledResponseJ_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (P Q : BlockVec d) : doubledResponseJ U a P Q = doubledResponseJ U b P Q

theorem HCPolySupport.Book.Ch02.IsDoubledResponseMaximizer.ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) {P Q : BlockVec d} {X : DoubledField d} (hX : IsDoubledResponseMaximizer U a P Q X) : IsDoubledResponseMaximizer U b P Q X

structure HCPolySupport.Book.Ch02.DoubledResponseTheory {d : ℕ} (U : Domain d) (a : CoeffOn U) : Prop

Public theorem package for l.block.response.functional.basic.definitions.

The canonical public theorem proving this package is doubledResponseTheory in DoubledResponse.lean.

• response_space_by_solutions (X : DoubledField d) : IsDoubledResponseField U a X ↔ ∃ (v : Solution U a) (vStar : Solution U a.transpose), X.SameAE (doubledFieldOfSolutions a v vStar)
• doubled_response_by_scalar (p pStar q qStar : Vec d) : doubledResponseJ U a (p, q) (qStar, pStar) = 1 / 2 * responseJ U a (p - pStar) (qStar - q) + 1 / 2 * responseJ U a.transpose (pStar + p) (qStar + q)
• scalar_maximizers_give_doubled_maximizer (p pStar q qStar : Vec d) (v : Solution U a) (vStar : Solution U a.transpose) : IsResponseMaximizer U a (p - pStar) (qStar - q) v → IsResponseMaximizer U a.transpose (pStar + p) (qStar + q) vStar → IsDoubledResponseMaximizer U a (p, q) (qStar, pStar) (doubledFieldOfScalarMaximizers a v vStar)
• maximizer_exists (P Q : BlockVec d) : DoubledResponseMaximizerExists U a P Q
• maximizer_unique_ae (P Q : BlockVec d) (X Y : DoubledField d) : IsDoubledResponseMaximizer U a P Q X → IsDoubledResponseMaximizer U a P Q Y → X.SameAE Y
• maximizer_add_sameAE (P1 Q1 P2 Q2 : BlockVec d) (X12 X1 X2 : DoubledField d) : IsDoubledResponseMaximizer U a (P1 + P2) (Q1 + Q2) X12 → IsDoubledResponseMaximizer U a P1 Q1 X1 → IsDoubledResponseMaximizer U a P2 Q2 X2 → X12.SameAE (X1 + X2)
• maximizer_smul_sameAE (c : ℝ) (P Q : BlockVec d) (Xc X : DoubledField d) : IsDoubledResponseMaximizer U a (c • P) (c • Q) Xc → IsDoubledResponseMaximizer U a P Q X → Xc.SameAE (c • X)
• first_variation (P Q : BlockVec d) (S T : DoubledField d) : IsDoubledResponseMaximizer U a P Q S → IsDoubledResponseField U a T → (average U fun (x : Vec d) => blockVecDot Q (T.eval x) - blockVecDot P (blockMatVecMul (blockMatrixField a x) (T.eval x))) = average U fun (x : Vec d) => blockVecDot (T.eval x) (blockMatVecMul (blockMatrixField a x) (S.eval x))

theorem HCPolySupport.Book.Ch02.DoubledResponseTheory.doubledResponseJ_eq_scalar {d : ℕ} {U : Domain d} {a : CoeffOn U} (h : DoubledResponseTheory U a) (p pStar q qStar : Vec d) : doubledResponseJ U a (p, q) (qStar, pStar) = 1 / 2 * responseJ U a (p - pStar) (qStar - q) + 1 / 2 * responseJ U a.transpose (pStar + p) (qStar + q)

Accessor for the scalar splitting of doubled response e.block.J.by.J.Jstar.basic.definitions.