Coarse-graining support: Support.Internal.Ch02.DoubledResponse.Common

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

Common Doubled-Response Helpers

This file is split mechanically out of Internal.Ch02.DoubledResponse.

def HCPolySupport.Internal.Ch02.BookCh02.blockStateOfDoubled {d : ℕ} (X : Book.Ch02.DoubledField d) : BlockState d

The block state with the same potential and flux fields as a doubled field.

Equations

• HCPolySupport.Internal.Ch02.BookCh02.blockStateOfDoubled X = { potential := X.potential, flux := X.flux }

def HCPolySupport.Internal.Ch02.BookCh02.doubledFieldOfBlockState {d : ℕ} (X : BlockState d) : Book.Ch02.DoubledField d

The doubled field with the same potential and flux fields as a block state.

Equations

• HCPolySupport.Internal.Ch02.BookCh02.doubledFieldOfBlockState X = { potential := X.potential, flux := X.flux }

theorem HCPolySupport.Internal.Ch02.BookCh02.doubledField_ext {d : ℕ} {X Y : Book.Ch02.DoubledField d} (hpot : X.potential = Y.potential) (hflux : X.flux = Y.flux) : X = Y

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

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

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

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

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

theorem HCPolySupport.Internal.Ch02.BookCh02.doubledFieldOfSolutions_sameAE_ofAEEq {d : ℕ} {U : Book.Ch02.Domain d} {a b : Book.Ch02.CoeffOn U} (h : a.AEEq b) (v : Book.Ch02.Solution U a) (vStar : Book.Ch02.Solution U a.transpose) : (Book.Ch02.doubledFieldOfSolutions a v vStar).SameAE (Book.Ch02.doubledFieldOfSolutions b (Book.Ch02.Solution.ofAEEq h v) (Book.Ch02.Solution.ofAEEq ⋯ vStar))

theorem HCPolySupport.Internal.Ch02.BookCh02.doubledFieldOfScalarMaximizers_sameAE_ofAEEq {d : ℕ} {U : Book.Ch02.Domain d} {a b : Book.Ch02.CoeffOn U} (h : a.AEEq b) (v : Book.Ch02.Solution U a) (vStar : Book.Ch02.Solution U a.transpose) : (Book.Ch02.doubledFieldOfScalarMaximizers a v vStar).SameAE (Book.Ch02.doubledFieldOfScalarMaximizers b (Book.Ch02.Solution.ofAEEq h v) (Book.Ch02.Solution.ofAEEq ⋯ vStar))

noncomputable def HCPolySupport.Internal.Ch02.BookCh02.solutionSMul {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (c : ℝ) (u : Book.Ch02.Solution U a) : Book.Ch02.Solution U a

Scalar multiplication of a harmonic solution, with its value and gradient multiplied by c.

Equations

• HCPolySupport.Internal.Ch02.BookCh02.solutionSMul U a c u = { toH1 := c • u.toH1, isHarmonic := ⋯ }

noncomputable def HCPolySupport.Internal.Ch02.BookCh02.doubledResponseFirstVariationLeft {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (P Q : BlockVec d) (T : Book.Ch02.DoubledField d) : Vec d → ℝ

The load-dependent first variation density Q · T - P · BT, where B is the block coefficient field.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Internal.Ch02.BookCh02.doubledResponseFirstVariationRight {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (S T : Book.Ch02.DoubledField d) : Vec d → ℝ

The bilinear first variation density T · BS, where B is the block coefficient field.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Internal.Ch02.BookCh02.average_eq_of_average_sub_eq_zero {d : ℕ} (U : Book.Ch02.Domain d) {f g : Vec d → ℝ} (hf : MeasureTheory.IntegrableOn f U.carrier MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn g U.carrier MeasureTheory.volume) (hzero : (Book.Ch02.average U fun (x : Vec d) => f x - g x) = 0) : Book.Ch02.average U f = Book.Ch02.average U g

theorem HCPolySupport.Internal.Ch02.BookCh02.doubledResponseFirstVariationLeft_average_eq_of_sameAE {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (P Q : BlockVec d) {T T' : Book.Ch02.DoubledField d} (hTT' : T.SameAE T') : Book.Ch02.average U (doubledResponseFirstVariationLeft U a P Q T) = Book.Ch02.average U (doubledResponseFirstVariationLeft U a P Q T')

theorem HCPolySupport.Internal.Ch02.BookCh02.doubledResponseFirstVariationRight_average_eq_of_sameAE {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) {S S' T T' : Book.Ch02.DoubledField d} (hSS' : S.SameAE S') (hTT' : T.SameAE T') : Book.Ch02.average U (doubledResponseFirstVariationRight U a S T) = Book.Ch02.average U (doubledResponseFirstVariationRight U a S' T')

theorem HCPolySupport.Internal.Ch02.BookCh02.doubledResponseFirstVariationLeft_average_eq_ofAEEq {d : ℕ} {U : Book.Ch02.Domain d} {a b : Book.Ch02.CoeffOn U} (h : a.AEEq b) (P Q : BlockVec d) (T : Book.Ch02.DoubledField d) : Book.Ch02.average U (doubledResponseFirstVariationLeft U a P Q T) = Book.Ch02.average U (doubledResponseFirstVariationLeft U b P Q T)

theorem HCPolySupport.Internal.Ch02.BookCh02.doubledResponseFirstVariationRight_average_eq_ofAEEq {d : ℕ} {U : Book.Ch02.Domain d} {a b : Book.Ch02.CoeffOn U} (h : a.AEEq b) (S T : Book.Ch02.DoubledField d) : Book.Ch02.average U (doubledResponseFirstVariationRight U a S T) = Book.Ch02.average U (doubledResponseFirstVariationRight U b S T)

theorem HCPolySupport.Internal.Ch02.BookCh02.doubledFieldOfSolutions_solutionSMul_half_eq_pairHalf {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (u : Book.Ch02.Solution U a) (vStar : Book.Ch02.Solution U a.transpose) : Book.Ch02.doubledFieldOfSolutions a (solutionSMul U a (1 / 2) u) (solutionSMul U a.transpose (1 / 2) vStar) = doubledFieldOfBlockState (blockResponsePairHalfState a.toCoeffField u vStar)

theorem HCPolySupport.Internal.Ch02.BookCh02.blockStateOfDoubled_scalarMaximizers_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) : blockStateOfDoubled (Book.Ch02.doubledFieldOfScalarMaximizers a v vStar) = blockResponsePairHalfState a.toCoeffField v vStar

theorem HCPolySupport.Internal.Ch02.BookCh02.blockStateOfDoubled_solutions_eq_pairHalf_two {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (w : Book.Ch02.Solution U a) (z : Book.Ch02.Solution U a.transpose) : blockStateOfDoubled (Book.Ch02.doubledFieldOfSolutions a w z) = blockResponsePairHalfState a.toCoeffField (solutionSMul U a 2 w) (solutionSMul U a.transpose 2 z)