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

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

noncomputable def HCPolySupport.Book.Ch02.average {d : ℕ} (U : Domain d) (f : Vec d → ℝ) : ℝ

Public normalized average over a Chapter 2 domain.

Equations

• HCPolySupport.Book.Ch02.average U f = (MeasureTheory.volume U.carrier).toReal⁻¹ * ∫ (x : HCPolySupport.Vec d) in U.carrier, f x

noncomputable def HCPolySupport.Book.Ch02.averageVec {d : ℕ} (U : Domain d) (F : Vec d → Vec d) : Vec d

Public normalized vector average over a Chapter 2 domain.

Equations

• HCPolySupport.Book.Ch02.averageVec U F i = HCPolySupport.Book.Ch02.average U fun (x : HCPolySupport.Vec d) => F x i

noncomputable def HCPolySupport.Book.Ch02.responseIntegrand {d : ℕ} (U : Domain d) (a : CoeffOn U) (p q : Vec d) (v : Solution U a) : Vec d → ℝ

The response integrand from the notes, used under the normalized volume average.

Equations

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

noncomputable def HCPolySupport.Book.Ch02.responseValue {d : ℕ} (U : Domain d) (a : CoeffOn U) (p q : Vec d) (v : Solution U a) : ℝ

The response value of one admissible solution.

Equations

• HCPolySupport.Book.Ch02.responseValue U a p q v = HCPolySupport.Book.Ch02.average U (HCPolySupport.Book.Ch02.responseIntegrand U a p q v)

theorem HCPolySupport.Book.Ch02.responseIntegrand_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (p q : Vec d) (v : Solution U a) : responseIntegrand U b p q (Solution.ofAEEq h v) =ᵐ[volumeMeasureOn U.carrier] responseIntegrand U a p q v

theorem HCPolySupport.Book.Ch02.responseValue_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (p q : Vec d) (v : Solution U a) : responseValue U b p q (Solution.ofAEEq h v) = responseValue U a p q v

noncomputable def HCPolySupport.Book.Ch02.firstVariationIntegrand {d : ℕ} (U : Domain d) (a : CoeffOn U) (p q : Vec d) (v w : Solution U a) : Vec d → ℝ

The first-variation integrand appearing in the Euler-Lagrange equation for the response maximizer.

Equations

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

noncomputable def HCPolySupport.Book.Ch02.firstVariationValue {d : ℕ} (U : Domain d) (a : CoeffOn U) (p q : Vec d) (v w : Solution U a) : ℝ

The averaged first variation. A maximizer makes this vanish for every admissible direction.

Equations

• HCPolySupport.Book.Ch02.firstVariationValue U a p q v w = HCPolySupport.Book.Ch02.average U (HCPolySupport.Book.Ch02.firstVariationIntegrand U a p q v w)

noncomputable def HCPolySupport.Book.Ch02.variationEnergyIntegrand {d : ℕ} (U : Domain d) (a : CoeffOn U) (w : Solution U a) : Vec d → ℝ

The positive quadratic energy in the second-variation formula.

Equations

• HCPolySupport.Book.Ch02.variationEnergyIntegrand U a w x = HCPolySupport.vecDot (w.toH1.grad x) (HCPolySupport.matVecMul (HCPolySupport.symmPart (a.toCoeffField x)) (w.toH1.grad x))

noncomputable def HCPolySupport.Book.Ch02.variationEnergyValue {d : ℕ} (U : Domain d) (a : CoeffOn U) (w : Solution U a) : ℝ

The averaged quadratic energy of an admissible variation.

Equations

• HCPolySupport.Book.Ch02.variationEnergyValue U a w = HCPolySupport.Book.Ch02.average U (HCPolySupport.Book.Ch02.variationEnergyIntegrand U a w)

noncomputable def HCPolySupport.Book.Ch02.secondVariationEnergyValue {d : ℕ} (U : Domain d) (a : CoeffOn U) (v w : Solution U a) : ℝ

The right-hand side in the second-variation identity for two admissible solutions.

Equations

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

noncomputable def HCPolySupport.Book.Ch02.averageGradient {d : ℕ} (U : Domain d) (a : CoeffOn U) (v : Solution U a) : Vec d

The averaged gradient of a Chapter 2 solution.

Equations

• HCPolySupport.Book.Ch02.averageGradient U a v = HCPolySupport.Book.Ch02.averageVec U v.toH1.grad

noncomputable def HCPolySupport.Book.Ch02.averageFlux {d : ℕ} (U : Domain d) (a : CoeffOn U) (v : Solution U a) : Vec d

The averaged flux of a Chapter 2 solution.

Equations

• HCPolySupport.Book.Ch02.averageFlux U a v = HCPolySupport.Book.Ch02.averageVec U fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (a.toCoeffField x) (v.toH1.grad x)

theorem HCPolySupport.Book.Ch02.averageGradient_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (v : Solution U a) : averageGradient U b (Solution.ofAEEq h v) = averageGradient U a v

The averaged gradient is unchanged by a null-set change of coefficient representative.

theorem HCPolySupport.Book.Ch02.averageFlux_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (v : Solution U a) : averageFlux U b (Solution.ofAEEq h v) = averageFlux U a v

The averaged flux is unchanged by a null-set change of coefficient representative.

theorem HCPolySupport.Book.Ch02.firstVariationIntegrand_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (p q : Vec d) (v w : Solution U a) : firstVariationIntegrand U b p q (Solution.ofAEEq h v) (Solution.ofAEEq h w) =ᵐ[volumeMeasureOn U.carrier] firstVariationIntegrand U a p q v w

theorem HCPolySupport.Book.Ch02.firstVariationValue_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (p q : Vec d) (v w : Solution U a) : firstVariationValue U b p q (Solution.ofAEEq h v) (Solution.ofAEEq h w) = firstVariationValue U a p q v w

theorem HCPolySupport.Book.Ch02.variationEnergyIntegrand_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (w : Solution U a) : variationEnergyIntegrand U b (Solution.ofAEEq h w) =ᵐ[volumeMeasureOn U.carrier] variationEnergyIntegrand U a w

theorem HCPolySupport.Book.Ch02.variationEnergyValue_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (w : Solution U a) : variationEnergyValue U b (Solution.ofAEEq h w) = variationEnergyValue U a w

theorem HCPolySupport.Book.Ch02.secondVariationEnergyValue_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (v w : Solution U a) : secondVariationEnergyValue U b (Solution.ofAEEq h v) (Solution.ofAEEq h w) = secondVariationEnergyValue U a v w

noncomputable def HCPolySupport.Book.Ch02.responseValueSet {d : ℕ} (U : Domain d) (a : CoeffOn U) (p q : Vec d) : Set ℝ

The set of values whose supremum is J(U,p,q;a).

Equations

• HCPolySupport.Book.Ch02.responseValueSet U a p q = {m : ℝ | ∃ (v : HCPolySupport.Book.Ch02.Solution U a), m = HCPolySupport.Book.Ch02.responseValue U a p q v}

theorem HCPolySupport.Book.Ch02.responseValueSet_nonempty {d : ℕ} (U : Domain d) (a : CoeffOn U) (p q : Vec d) : (responseValueSet U a p q).Nonempty

noncomputable def HCPolySupport.Book.Ch02.responseJ {d : ℕ} (U : Domain d) (a : CoeffOn U) (p q : Vec d) : ℝ

Public Chapter 2 response functional J(U,p,q;a).

Equations

• HCPolySupport.Book.Ch02.responseJ U a p q = sSup (HCPolySupport.Book.Ch02.responseValueSet U a p q)

theorem HCPolySupport.Book.Ch02.responseValueSet_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (p q : Vec d) : responseValueSet U a p q = responseValueSet U b p q

theorem HCPolySupport.Book.Ch02.responseJ_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (p q : Vec d) : responseJ U a p q = responseJ U b p q

def HCPolySupport.Book.Ch02.IsResponseMaximizer {d : ℕ} (U : Domain d) (a : CoeffOn U) (p q : Vec d) (v : Solution U a) : Prop

A solution is a response maximizer if it realizes the variational supremum.

Equations

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

theorem HCPolySupport.Book.Ch02.IsResponseMaximizer.ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) {p q : Vec d} {v : Solution U a} (hv : IsResponseMaximizer U a p q v) : IsResponseMaximizer U b p q (Solution.ofAEEq h v)

theorem HCPolySupport.Book.Ch02.responseValueSet_isGreatest_of_isResponseMaximizer {d : ℕ} {U : Domain d} {a : CoeffOn U} {p q : Vec d} {v : Solution U a} (hv : IsResponseMaximizer U a p q v) : IsGreatest (responseValueSet U a p q) (responseValue U a p q v)

theorem HCPolySupport.Book.Ch02.responseJ_eq_responseValue_of_isResponseMaximizer {d : ℕ} {U : Domain d} {a : CoeffOn U} {p q : Vec d} {v : Solution U a} (hv : IsResponseMaximizer U a p q v) : responseJ U a p q = responseValue U a p q v

structure HCPolySupport.Book.Ch02.CanonicalMaximizer {d : ℕ} (U : Domain d) (a : CoeffOn U) (p q : Vec d) : Type

The mean-zero response maximizer as a packaged object.

• toSolution : Solution U a

  The harmonic solution underlying the mean-zero response maximizer.

• meanZero : MeanZeroOn U.carrier self.toSolution.toH1.toFun
• isMaximizer : IsResponseMaximizer U a p q self.toSolution

@[instance_reducible]

instance HCPolySupport.Book.Ch02.CanonicalMaximizer.instCoeOutSolution {d : ℕ} {U : Domain d} {a : CoeffOn U} {p q : Vec d} : CoeOut (CanonicalMaximizer U a p q) (Solution U a)

Equations

• HCPolySupport.Book.Ch02.CanonicalMaximizer.instCoeOutSolution = { coe := fun (v : HCPolySupport.Book.Ch02.CanonicalMaximizer U a p q) => v.toSolution }

def HCPolySupport.Book.Ch02.CanonicalMaximizer.ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) {p q : Vec d} (v : CanonicalMaximizer U a p q) : CanonicalMaximizer U b p q

Transport the canonical maximizer package across a null-set change of coefficient representative.

Equations

• HCPolySupport.Book.Ch02.CanonicalMaximizer.ofAEEq h v = { toSolution := HCPolySupport.Book.Ch02.Solution.ofAEEq h v.toSolution, meanZero := ⋯, isMaximizer := ⋯ }

theorem HCPolySupport.Book.Ch02.CanonicalMaximizer.responseJ_eq {d : ℕ} {U : Domain d} {a : CoeffOn U} {p q : Vec d} (v : CanonicalMaximizer U a p q) : responseJ U a p q = responseValue U a p q v.toSolution