Coarse-graining support: Support.CoarseGraining.ResponseIdentities.Foundations.Algebra

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

Scalar response-integrand algebra

Volume-average linearity, symmetric-matrix polarization lemmas, AHarmonicFunction rescale/unscale/sub helpers, and basic algebraic identities for scalarResponseIntegrand and scalarVariationEnergyIntegrand.

@[simp]

theorem HCPolySupport.volumeAverage_zero {d : ℕ} (U : Set (Vec d)) : volumeAverage U 0 = 0

theorem HCPolySupport.volumeAverage_smul {d : ℕ} (U : Set (Vec d)) (c : ℝ) (f : Vec d → ℝ) : volumeAverage U (c • f) = c * volumeAverage U f

theorem HCPolySupport.volumeAverage_add {d : ℕ} {U : Set (Vec d)} {f g : Vec d → ℝ} (hf : MeasureTheory.IntegrableOn f U MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn g U MeasureTheory.volume) : volumeAverage U (f + g) = volumeAverage U f + volumeAverage U g

theorem HCPolySupport.volumeAverage_sub {d : ℕ} {U : Set (Vec d)} {f g : Vec d → ℝ} (hf : MeasureTheory.IntegrableOn f U MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn g U MeasureTheory.volume) : volumeAverage U (f - g) = volumeAverage U f - volumeAverage U g

theorem HCPolySupport.volumeAverage_sum {d : ℕ} {α : Type u_1} {U : Set (Vec d)} (s : Finset α) (f : α → Vec d → ℝ) (hf : ∀ a ∈ s, MeasureTheory.IntegrableOn (f a) U MeasureTheory.volume) : (volumeAverage U fun (x : Vec d) => ∑ a ∈ s, f a x) = ∑ a ∈ s, volumeAverage U (f a)

theorem HCPolySupport.volumeAverage_const {d : ℕ} {U : Set (Vec d)} {c : ℝ} (hvol : (MeasureTheory.volume U).toReal ≠ 0) : (volumeAverage U fun (x : Vec d) => c) = c

theorem HCPolySupport.volumeAverage_vecDot_left {d : ℕ} {U : Set (Vec d)} (v : Vec d) (f : Vec d → Vec d) (hf : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => f x i) U MeasureTheory.volume) : (volumeAverage U fun (x : Vec d) => vecDot v (f x)) = vecDot v fun (i : Fin d) => volumeAverage U fun (x : Vec d) => f x i

theorem HCPolySupport.volumeAverage_vecDot_right {d : ℕ} {U : Set (Vec d)} (f : Vec d → Vec d) (v : Vec d) (hf : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => f x i) U MeasureTheory.volume) : (volumeAverage U fun (x : Vec d) => vecDot (f x) v) = vecDot (fun (i : Fin d) => volumeAverage U fun (x : Vec d) => f x i) v

theorem HCPolySupport.integrableOn_matVecMul_of_integrableOn_entries {d : ℕ} {U : Set (Vec d)} {f : Vec d → Mat d} (hf : ∀ (i j : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => f x i j) U MeasureTheory.volume) (y : Vec d) (i : Fin d) : MeasureTheory.IntegrableOn (fun (x : Vec d) => matVecMul (f x) y i) U MeasureTheory.volume

theorem HCPolySupport.integrableOn_vecDot_matVecMul_of_integrableOn_entries {d : ℕ} {U : Set (Vec d)} {f : Vec d → Mat d} (hf : ∀ (i j : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => f x i j) U MeasureTheory.volume) (x y : Vec d) : MeasureTheory.IntegrableOn (fun (z : Vec d) => vecDot x (matVecMul (f z) y)) U MeasureTheory.volume

theorem HCPolySupport.matVecMul_volumeAverageMat {d : ℕ} {U : Set (Vec d)} {f : Vec d → Mat d} (hf : ∀ (i j : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => f x i j) U MeasureTheory.volume) (y : Vec d) : matVecMul (volumeAverageMat U f) y = fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (f x) y i

theorem HCPolySupport.vecDot_matVecMul_volumeAverageMat {d : ℕ} {U : Set (Vec d)} {f : Vec d → Mat d} (hf : ∀ (i j : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => f x i j) U MeasureTheory.volume) (x y : Vec d) : vecDot x (matVecMul (volumeAverageMat U f) y) = volumeAverage U fun (z : Vec d) => vecDot x (matVecMul (f z) y)

theorem HCPolySupport.volumeAverage_nonneg_of_nonneg_on {d : ℕ} {U : Set (Vec d)} {f : Vec d → ℝ} (hU : MeasurableSet U) (h_nonneg : ∀ x ∈ U, 0 ≤ f x) : 0 ≤ volumeAverage U f

theorem HCPolySupport.volumeAverage_le_of_le_on {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {f : Vec d → ℝ} {c : ℝ} (hU : MeasurableSet U) (hf : MeasureTheory.IntegrableOn f U MeasureTheory.volume) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (h_le : ∀ x ∈ U, f x ≤ c) : volumeAverage U f ≤ c

theorem HCPolySupport.symmPart_smul {d : ℕ} (c : ℝ) (A : Mat d) : symmPart (c • A) = c • symmPart A

theorem HCPolySupport.vecDot_matVecMul_symmPart_comm {d : ℕ} (A : Mat d) (ξ η : Vec d) : vecDot ξ (matVecMul (symmPart A) η) = vecDot η (matVecMul (symmPart A) ξ)

theorem HCPolySupport.half_vecDot_sub_polarization_of_isSymm {d : ℕ} {A : Mat d} (hA : Matrix.IsSymm A) (ξ η : Vec d) : 1 / 2 * vecDot ξ (matVecMul A ξ) + 1 / 2 * vecDot η (matVecMul A η) - 1 / 2 * vecDot (ξ - η) (matVecMul A (ξ - η)) = vecDot η (matVecMul A ξ)

theorem HCPolySupport.half_vecDot_sub_sub_of_isSymm {d : ℕ} {A : Mat d} (hA : Matrix.IsSymm A) (ξ η : Vec d) : 1 / 2 * vecDot (ξ - η) (matVecMul A (ξ - η)) - 1 / 2 * vecDot ξ (matVecMul A ξ) - 1 / 2 * vecDot η (matVecMul A η) = -vecDot η (matVecMul A ξ)

@[instance_reducible]

instance HCPolySupport.AHarmonicFunction.instZero {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} : Zero (AHarmonicFunction a U)

Equations

• HCPolySupport.AHarmonicFunction.instZero = { zero := { toH1 := 0, isHarmonic := ⋯ } }

@[instance_reducible]

instance HCPolySupport.AHarmonicFunction.instSMulReal {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} : SMul ℝ (AHarmonicFunction a U)

Equations

• HCPolySupport.AHarmonicFunction.instSMulReal = { smul := fun (c : ℝ) (u : HCPolySupport.AHarmonicFunction a U) => { toH1 := c • u.toH1, isHarmonic := ⋯ } }

@[simp]

theorem HCPolySupport.AHarmonicFunction.toH1_zero {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} : toH1 0 = 0

@[simp]

theorem HCPolySupport.AHarmonicFunction.toH1_smul {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (c : ℝ) (u : AHarmonicFunction a U) : (c • u).toH1 = c • u.toH1

@[simp]

theorem HCPolySupport.AHarmonicFunction.grad_zero {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} : (toH1 0).grad = 0

theorem HCPolySupport.AHarmonicFunction.grad_smul {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (c : ℝ) (u : AHarmonicFunction a U) : (c • u).toH1.grad = c • u.toH1.grad

def HCPolySupport.AHarmonicFunction.rescaleCoeff {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (u : AHarmonicFunction a U) (c : ℝ) : AHarmonicFunction (c • a) U

The same H¹ function viewed as harmonic for the scalar-multiplied coefficient field c • a.

Equations

• u.rescaleCoeff c = { toH1 := u.toH1, isHarmonic := ⋯ }

@[simp]

theorem HCPolySupport.AHarmonicFunction.toH1_rescaleCoeff {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (u : AHarmonicFunction a U) (c : ℝ) : (u.rescaleCoeff c).toH1 = u.toH1

@[simp]

theorem HCPolySupport.AHarmonicFunction.grad_rescaleCoeff {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (u : AHarmonicFunction a U) (c : ℝ) : (u.rescaleCoeff c).toH1.grad = u.toH1.grad

def HCPolySupport.AHarmonicFunction.unscaleCoeff {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (c : ℝ) (hc : c ≠ 0) (u : AHarmonicFunction (c • a) U) : AHarmonicFunction a U

The same H¹ function viewed as harmonic for a after removing a nonzero scalar factor from the coefficient field.

Equations

• HCPolySupport.AHarmonicFunction.unscaleCoeff c hc u = { toH1 := u.toH1, isHarmonic := ⋯ }

@[simp]

theorem HCPolySupport.AHarmonicFunction.toH1_unscaleCoeff {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (c : ℝ) (hc : c ≠ 0) (u : AHarmonicFunction (c • a) U) : (unscaleCoeff c hc u).toH1 = u.toH1

@[simp]

theorem HCPolySupport.AHarmonicFunction.grad_unscaleCoeff {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (c : ℝ) (hc : c ≠ 0) (u : AHarmonicFunction (c • a) U) : (unscaleCoeff c hc u).toH1.grad = u.toH1.grad

def HCPolySupport.AHarmonicFunction.subOfIntegrable {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (u v : AHarmonicFunction a U) (hu_int : weakFluxIntegrable U a u) (hv_int : weakFluxIntegrable U a v) : AHarmonicFunction a U

The difference of two harmonic H¹ functions, with harmonicity supplied by integrability of their weak flux pairings.

Equations

• u.subOfIntegrable v hu_int hv_int = u.addSMulOfIntegrable v hu_int hv_int (-1)

@[simp]

theorem HCPolySupport.AHarmonicFunction.toH1_subOfIntegrable {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (u v : AHarmonicFunction a U) (hu_int : weakFluxIntegrable U a u) (hv_int : weakFluxIntegrable U a v) : (u.subOfIntegrable v hu_int hv_int).toH1 = u.toH1 - v.toH1

theorem HCPolySupport.AHarmonicFunction.grad_subOfIntegrable {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (u v : AHarmonicFunction a U) (hu_int : weakFluxIntegrable U a u) (hv_int : weakFluxIntegrable U a v) : (u.subOfIntegrable v hu_int hv_int).toH1.grad = u.toH1.grad - v.toH1.grad

theorem HCPolySupport.scalarResponseIntegrand_eq_of_grad_eq {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {p q : Vec d} {u v : AHarmonicFunction a U} (hgrad : u.toH1.grad = v.toH1.grad) : scalarResponseIntegrand U a p q u = scalarResponseIntegrand U a p q v

@[simp]

theorem HCPolySupport.scalarResponseIntegrand_addConst {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (p q : Vec d) (u : AHarmonicFunction a U) (c : ℝ) : scalarResponseIntegrand U a p q (u.addConst c) = scalarResponseIntegrand U a p q u

@[simp]

theorem HCPolySupport.scalarResponseIntegrand_normalizeMeanZero {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (p q : Vec d) (u : AHarmonicFunction a U) : scalarResponseIntegrand U a p q u.normalizeMeanZero = scalarResponseIntegrand U a p q u

@[simp]

theorem HCPolySupport.scalarResponseIntegrand_zero {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (p q : Vec d) : scalarResponseIntegrand U a p q 0 = 0

theorem HCPolySupport.scalarResponseIntegrand_smul {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (c : ℝ) (p q : Vec d) (u : AHarmonicFunction a U) : scalarResponseIntegrand U a (c • p) (c • q) (c • u) = fun (x : Vec d) => c ^ 2 * scalarResponseIntegrand U a p q u x

theorem HCPolySupport.volumeAverage_scalarResponseIntegrand_smul {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (c : ℝ) (p q : Vec d) (u : AHarmonicFunction a U) : volumeAverage U (scalarResponseIntegrand U a (c • p) (c • q) (c • u)) = c ^ 2 * volumeAverage U (scalarResponseIntegrand U a p q u)

noncomputable def HCPolySupport.scalarFirstVariationIntegrand {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (p q : Vec d) (u w : AHarmonicFunction a U) : Vec d → ℝ

The first variation density of the scalar response at u in direction w, namely q · ∇w - p · a∇w - ∇w · symmPart(a)∇u.

Equations

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

noncomputable def HCPolySupport.scalarVariationEnergyIntegrand {d : ℕ} (a : CoeffField d) {U : Set (Vec d)} (w : AHarmonicFunction a U) : Vec d → ℝ

The symmetric quadratic gradient energy density ∇w · symmPart(a)∇w of a harmonic variation.

Equations

• HCPolySupport.scalarVariationEnergyIntegrand a w x = HCPolySupport.vecDot (w.toH1.grad x) (HCPolySupport.matVecMul (HCPolySupport.symmPart (a x)) (w.toH1.grad x))

theorem HCPolySupport.scalarVariationEnergyIntegrand_smul {d : ℕ} (a : CoeffField d) {U : Set (Vec d)} (c : ℝ) (w : AHarmonicFunction a U) : scalarVariationEnergyIntegrand a (c • w) = fun (x : Vec d) => c ^ 2 * scalarVariationEnergyIntegrand a w x

theorem HCPolySupport.volumeAverage_scalarVariationEnergyIntegrand_smul {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (c : ℝ) (w : AHarmonicFunction a U) : volumeAverage U (scalarVariationEnergyIntegrand a (c • w)) = c ^ 2 * volumeAverage U (scalarVariationEnergyIntegrand a w)