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

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

noncomputable def HCPolySupport.Book.Ch02.h1AverageGradient {d : ℕ} (U : Domain d) (u : H1Function U.carrier) : Vec d

Public averaged gradient of an arbitrary H¹ function on a Chapter 2 domain.

Equations

• HCPolySupport.Book.Ch02.h1AverageGradient U u = HCPolySupport.Book.Ch02.averageVec U u.grad

noncomputable def HCPolySupport.Book.Ch02.h1AverageFlux {d : ℕ} (U : Domain d) (a : CoeffOn U) (u : H1Function U.carrier) : Vec d

Public averaged flux of an arbitrary H¹ function on a Chapter 2 domain.

Equations

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

def HCPolySupport.Book.Ch02.IsSymmetricDirichletAdmissible {d : ℕ} (U : Domain d) (p : Vec d) (u : H1Function U.carrier) : Prop

Public Dirichlet admissibility for the symmetric subsection: u ∈ p · x + H¹₀(U), stated by saying that ∇u - p is a zero-trace potential field.

Equations

• HCPolySupport.Book.Ch02.IsSymmetricDirichletAdmissible U p u = HCPolySupport.Book.Ch01.PotentialZeroTraceFieldOn U.carrier fun (x : HCPolySupport.Vec d) => u.grad x - p

noncomputable def HCPolySupport.Book.Ch02.symmetricDirichletEnergyValue {d : ℕ} (U : Domain d) (a : CoeffOn U) (u : H1Function U.carrier) : ℝ

Public Dirichlet energy value from e.def.nuD.nuN.symmetric.basic.definitions.

Equations

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

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

Public value set whose infimum is ν_D(U,p;a).

Equations

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

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

Public Dirichlet value ν_D(U,p;a).

Equations

• HCPolySupport.Book.Ch02.symmetricDirichletNu U a p = sInf (HCPolySupport.Book.Ch02.symmetricDirichletValueSet U a p)

def HCPolySupport.Book.Ch02.IsSymmetricDirichletMinimizer {d : ℕ} (U : Domain d) (a : CoeffOn U) (p : Vec d) (u : H1Function U.carrier) : Prop

A public minimizer for ν_D(U,p;a).

Equations

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

noncomputable def HCPolySupport.Book.Ch02.symmetricNeumannEnergyValue {d : ℕ} (U : Domain d) (a : CoeffOn U) (q : Vec d) (u : H1Function U.carrier) : ℝ

Public Neumann value of a candidate from e.def.nuD.nuN.symmetric.basic.definitions.

Equations

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

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

Public value set whose supremum is ν_N(U,q;a).

Equations

• HCPolySupport.Book.Ch02.symmetricNeumannValueSet U a q = {E : ℝ | ∃ (u : HCPolySupport.H1Function U.carrier), E = HCPolySupport.Book.Ch02.symmetricNeumannEnergyValue U a q u}

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

Public Neumann value ν_N(U,q;a).

Equations

• HCPolySupport.Book.Ch02.symmetricNeumannNu U a q = sSup (HCPolySupport.Book.Ch02.symmetricNeumannValueSet U a q)

def HCPolySupport.Book.Ch02.IsSymmetricNeumannMaximizer {d : ℕ} (U : Domain d) (a : CoeffOn U) (q : Vec d) (u : H1Function U.carrier) : Prop

A public maximizer for ν_N(U,q;a). The note chooses the mean-zero representative separately, so mean-zero is a theorem-field condition rather than part of this maximizer predicate.

Equations

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

theorem HCPolySupport.Book.Ch02.symmetricDirichletEnergyValue_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (u : H1Function U.carrier) : symmetricDirichletEnergyValue U a u = symmetricDirichletEnergyValue U b u

The public Dirichlet energy depends only on the coefficient field up to a.e. equality on the domain.

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

The public Dirichlet value set is invariant under a.e. coefficient changes.

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

The public Dirichlet value is invariant under a.e. coefficient changes.

theorem HCPolySupport.Book.Ch02.IsSymmetricDirichletMinimizer.ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) {p : Vec d} {u : H1Function U.carrier} (hu : IsSymmetricDirichletMinimizer U a p u) : IsSymmetricDirichletMinimizer U b p u

Transport a public symmetric Dirichlet minimizer across an a.e. coefficient change.

theorem HCPolySupport.Book.Ch02.symmetricNeumannEnergyValue_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (q : Vec d) (u : H1Function U.carrier) : symmetricNeumannEnergyValue U a q u = symmetricNeumannEnergyValue U b q u

The public Neumann candidate value depends only on the coefficient field up to a.e. equality on the domain.

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

The public Neumann value set is invariant under a.e. coefficient changes.

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

The public Neumann value is invariant under a.e. coefficient changes.

theorem HCPolySupport.Book.Ch02.IsSymmetricNeumannMaximizer.ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) {q : Vec d} {u : H1Function U.carrier} (hu : IsSymmetricNeumannMaximizer U a q u) : IsSymmetricNeumannMaximizer U b q u

Transport a public symmetric Neumann maximizer across an a.e. coefficient change.

theorem HCPolySupport.Book.Ch02.h1AverageFlux_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (u : H1Function U.carrier) : h1AverageFlux U a u = h1AverageFlux U b u

The public averaged flux of an arbitrary H¹ function is invariant under a.e. coefficient changes.

theorem HCPolySupport.Book.Ch02.averageMat_toCoeffField_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) : averageMat U a.toCoeffField = averageMat U b.toCoeffField

The raw public coefficient average is invariant under a.e. coefficient changes.