Coarse-graining support: Support.Book.Ch02.DoubledResponse

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

structure HCPolySupport.Book.Ch02.DoubledField (d : ℕ) : Type

Public doubled field, represented by potential and flux components.

• potential : Vec d → Vec d

  The vector field forming the potential component of the doubled field.

• flux : Vec d → Vec d

  The vector field forming the flux component of the doubled field.

def HCPolySupport.Book.Ch02.DoubledField.eval {d : ℕ} (X : DoubledField d) (x : Vec d) : BlockVec d

Evaluate a doubled field as a block vector.

Equations

• X.eval x = (X.potential x, X.flux x)

def HCPolySupport.Book.Ch02.DoubledField.SameAE {d : ℕ} {U : Domain d} (X Y : DoubledField d) : Prop

A.e. equality of public doubled fields on a Chapter 2 domain.

Equations

• X.SameAE Y = (X.potential =ᵐ[HCPolySupport.volumeMeasureOn U.carrier] Y.potential ∧ X.flux =ᵐ[HCPolySupport.volumeMeasureOn U.carrier] Y.flux)

@[instance_reducible]

instance HCPolySupport.Book.Ch02.DoubledField.instZero {d : ℕ} : Zero (DoubledField d)

Equations

• HCPolySupport.Book.Ch02.DoubledField.instZero = { zero := { potential := 0, flux := 0 } }

@[instance_reducible]

instance HCPolySupport.Book.Ch02.DoubledField.instAdd {d : ℕ} : Add (DoubledField d)

Equations

• HCPolySupport.Book.Ch02.DoubledField.instAdd = { add := fun (X Y : HCPolySupport.Book.Ch02.DoubledField d) => { potential := X.potential + Y.potential, flux := X.flux + Y.flux } }

@[instance_reducible]

instance HCPolySupport.Book.Ch02.DoubledField.instNeg {d : ℕ} : Neg (DoubledField d)

Equations

• HCPolySupport.Book.Ch02.DoubledField.instNeg = { neg := fun (X : HCPolySupport.Book.Ch02.DoubledField d) => { potential := -X.potential, flux := -X.flux } }

@[instance_reducible]

instance HCPolySupport.Book.Ch02.DoubledField.instSub {d : ℕ} : Sub (DoubledField d)

Equations

• HCPolySupport.Book.Ch02.DoubledField.instSub = { sub := fun (X Y : HCPolySupport.Book.Ch02.DoubledField d) => { potential := X.potential - Y.potential, flux := X.flux - Y.flux } }

@[instance_reducible]

instance HCPolySupport.Book.Ch02.DoubledField.instSMulReal {d : ℕ} : SMul ℝ (DoubledField d)

Equations

• HCPolySupport.Book.Ch02.DoubledField.instSMulReal = { smul := fun (c : ℝ) (X : HCPolySupport.Book.Ch02.DoubledField d) => { potential := c • X.potential, flux := c • X.flux } }

@[simp]

theorem HCPolySupport.Book.Ch02.DoubledField.eval_zero {d : ℕ} (x : Vec d) : eval 0 x = 0

@[simp]

theorem HCPolySupport.Book.Ch02.DoubledField.eval_add {d : ℕ} (X Y : DoubledField d) (x : Vec d) : (X + Y).eval x = X.eval x + Y.eval x

@[simp]

theorem HCPolySupport.Book.Ch02.DoubledField.eval_neg {d : ℕ} (X : DoubledField d) (x : Vec d) : (-X).eval x = -X.eval x

@[simp]

theorem HCPolySupport.Book.Ch02.DoubledField.eval_sub {d : ℕ} (X Y : DoubledField d) (x : Vec d) : (X - Y).eval x = X.eval x - Y.eval x

@[simp]

theorem HCPolySupport.Book.Ch02.DoubledField.eval_smul {d : ℕ} (c : ℝ) (X : DoubledField d) (x : Vec d) : (c • X).eval x = c • X.eval x

def HCPolySupport.Book.Ch02.IsDoubledAmbientField {d : ℕ} (U : Domain d) (X : DoubledField d) : Prop

Public field in \Lpot(U) × \Lsol(U).

Equations

• HCPolySupport.Book.Ch02.IsDoubledAmbientField U X = (HCPolySupport.Book.Ch01.PotentialFieldOn U.carrier X.potential ∧ HCPolySupport.Book.Ch01.SolenoidalFieldOn U.carrier X.flux)

def HCPolySupport.Book.Ch02.IsDoubledTestField {d : ℕ} (U : Domain d) (X : DoubledField d) : Prop

Public test field in \Lpoto(U) × \Lsolo(U).

Equations

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

noncomputable def HCPolySupport.Book.Ch02.doubledBlockPairingIntegrand {d : ℕ} (U : Domain d) (a : CoeffOn U) (Y X : DoubledField d) : Vec d → ℝ

Block pairing integrand Y · A X for doubled fields.

Equations

• HCPolySupport.Book.Ch02.doubledBlockPairingIntegrand U a Y X x = HCPolySupport.blockVecDot (Y.eval x) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.blockMatrixField a x) (X.eval x))

def HCPolySupport.Book.Ch02.IsDoubledResponseField {d : ℕ} (U : Domain d) (a : CoeffOn U) (X : DoubledField d) : Prop

Public doubled response space S(U; a).

Equations

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

def HCPolySupport.Book.Ch02.IsDoubledMuAdmissible {d : ℕ} (U : Domain d) (P : BlockVec d) (X : DoubledField d) : Prop

Public admissibility for the doubled mu problem: X ∈ P + Lpoto(U) × Lsolo(U).

Equations

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

noncomputable def HCPolySupport.Book.Ch02.doubledMuValue {d : ℕ} (U : Domain d) (a : CoeffOn U) (X : DoubledField d) : ℝ

Public doubled mu energy value of an admissible field.

Equations

• HCPolySupport.Book.Ch02.doubledMuValue U a X = HCPolySupport.Book.Ch02.average U fun (x : HCPolySupport.Vec d) => HCPolySupport.Book.Ch02.blockEnergyDensityAt a (X.eval x) x

noncomputable def HCPolySupport.Book.Ch02.doubledMuValueSet {d : ℕ} (U : Domain d) (a : CoeffOn U) (P : BlockVec d) : Set ℝ

Public value set whose infimum is mu(U,P;a).

Equations

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

noncomputable def HCPolySupport.Book.Ch02.doubledMu {d : ℕ} (U : Domain d) (a : CoeffOn U) (P : BlockVec d) : ℝ

Public doubled variational quantity mu(U,P;a).

Equations

• HCPolySupport.Book.Ch02.doubledMu U a P = sInf (HCPolySupport.Book.Ch02.doubledMuValueSet U a P)

def HCPolySupport.Book.Ch02.IsDoubledMuMinimizer {d : ℕ} (U : Domain d) (a : CoeffOn U) (P : BlockVec d) (X : DoubledField d) : Prop

A public minimizer for mu(U,P;a).

Equations

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

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

Public doubled response integrand from e.def.block.J.basic.definitions.

Equations

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

noncomputable def HCPolySupport.Book.Ch02.doubledResponseValue {d : ℕ} (U : Domain d) (a : CoeffOn U) (P Q : BlockVec d) (X : DoubledField d) : ℝ

Public doubled response value of one field.

Equations

• HCPolySupport.Book.Ch02.doubledResponseValue U a P Q X = HCPolySupport.Book.Ch02.average U (HCPolySupport.Book.Ch02.doubledResponseIntegrand U a P Q X)

noncomputable def HCPolySupport.Book.Ch02.doubledResponseValueSet {d : ℕ} (U : Domain d) (a : CoeffOn U) (P Q : BlockVec d) : Set ℝ

Public value set whose supremum is Jbold(U,P,Q;a).

Equations

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

noncomputable def HCPolySupport.Book.Ch02.doubledResponseJ {d : ℕ} (U : Domain d) (a : CoeffOn U) (P Q : BlockVec d) : ℝ

Public doubled response functional Jbold(U,P,Q;a).

Equations

• HCPolySupport.Book.Ch02.doubledResponseJ U a P Q = sSup (HCPolySupport.Book.Ch02.doubledResponseValueSet U a P Q)

def HCPolySupport.Book.Ch02.IsDoubledResponseMaximizer {d : ℕ} (U : Domain d) (a : CoeffOn U) (P Q : BlockVec d) (X : DoubledField d) : Prop

A public maximizer for the doubled response functional.

Equations

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

def HCPolySupport.Book.Ch02.DoubledResponseMaximizerExists {d : ℕ} (U : Domain d) (a : CoeffOn U) (P Q : BlockVec d) : Prop

Public existence statement for doubled response maximizers.

Equations

• HCPolySupport.Book.Ch02.DoubledResponseMaximizerExists U a P Q = ∃ (X : HCPolySupport.Book.Ch02.DoubledField d), HCPolySupport.Book.Ch02.IsDoubledResponseMaximizer U a P Q X

noncomputable def HCPolySupport.Book.Ch02.doubledFieldOfSolutions {d : ℕ} {U : Domain d} (a : CoeffOn U) (v : Solution U a) (vStar : Solution U a.transpose) : DoubledField d

Public doubled field generated by a primal and adjoint solution.

Equations

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

noncomputable def HCPolySupport.Book.Ch02.doubledFieldOfScalarMaximizers {d : ℕ} {U : Domain d} (a : CoeffOn U) (v : Solution U a) (vStar : Solution U a.transpose) : DoubledField d

Public doubled maximizer candidate generated by the scalar maximizers in e.block.maximizer.by.v.vstar.basic.definitions.

Equations

• HCPolySupport.Book.Ch02.doubledFieldOfScalarMaximizers a v vStar = (1 / 2) • HCPolySupport.Book.Ch02.doubledFieldOfSolutions a v vStar