Documentation

LeanPool.HighContrastHomogenization.Provider.Response.SubdivisionDefect

High-contrast homogenization: Provider.Response.SubdivisionDefect #

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The subdivision defect of the response functional #

A maximizer of the response functional on a domain restricts to an admissible competitor on every subdomain, and its response integrand is a fixed function of the coefficient representative and the gradient. Averaging that integrand over a subdivision of the parent into cells that are pairwise disjoint and cover the parent up to a null set therefore returns the parent response exactly.

Subtracting this from the second-variation identity on each cell gives the subdivision defect identity: the weighted average of the cells' response values exceeds the parent's response value by precisely the weighted average of the symmetric energies of the gradient differences between the cell maximizers and the restricted parent maximizer. In the equal-volume case the weights are all the reciprocal cell count, which is the form the localization argument uses.

Since the symmetric part of an elliptic coefficient is positive semidefinite, every cell contribution is nonnegative, and so is the defect.

Everything is stated over an arbitrary Chapter 2 domain and an arbitrary finite family of subdomains, so it reads on triadic cubes and on adapted cells alike.

The canonical maximizer as a solution #

source
noncomputable def HCPolySupport.HighContrast.Response.canonicalResponseSolution {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (p r : Vec d) :
Book.Ch02.Solution U a

The canonical response maximizer of a Chapter 2 domain, read as a solution.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.Response.canonicalResponseSolution_isMaximizer {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (p r : Vec d) :
    Book.Ch02.IsResponseMaximizer U a p r (canonicalResponseSolution U a p r)

    The canonical response solution maximizes the response functional.

    The response integrand depends only on the representative and the #

    gradient

    source
    theorem HCPolySupport.HighContrast.Response.responseIntegrand_congr {d : ℕ} {U V : Book.Ch02.Domain d} {a : Book.Ch02.CoeffOn U} {b : Book.Ch02.CoeffOn V} (hrep : b.toCoeffField = a.toCoeffField) {v : Book.Ch02.Solution U a} {z : Book.Ch02.Solution V b} (hz : z.toH1.grad = v.toH1.grad) (p r : Vec d) :
    Book.Ch02.responseIntegrand V b p r z = Book.Ch02.responseIntegrand U a p r v

    Two solutions with the same gradient, on domains carrying the same coefficient representative, have the same response integrand.

    The parent response is the weighted average of the restricted values #

    source
    theorem HCPolySupport.HighContrast.Response.sum_weight_responseValue_eq_responseJ {d : ℕ} {ι : Type u_1} {Z : Finset ι} {U : Book.Ch02.Domain d} {V : ι → Book.Ch02.Domain d} {a : Book.Ch02.CoeffOn U} {b : (i : ι) → Book.Ch02.CoeffOn (V i)} (hrep : ∀ i ∈ Z, (b i).toCoeffField = a.toCoeffField) (hsub : ∀ i ∈ Z, (V i).carrier ⊆ U.carrier) (hdisj : (↑Z).PairwiseDisjoint fun (i : ι) => (V i).carrier) (hnull : MeasureTheory.volume (U.carrier \ ⋃ i ∈ ↑Z, (V i).carrier) = 0) {p r : Vec d} {v : Book.Ch02.Solution U a} (hv : Book.Ch02.IsResponseMaximizer U a p r v) {z : (i : ι) → Book.Ch02.Solution (V i) (b i)} (hz : ∀ i ∈ Z, (z i).toH1.grad = v.toH1.grad) :
    ∑ i ∈ Z, (MeasureTheory.volume (V i).carrier).toReal / (MeasureTheory.volume U.carrier).toReal * Book.Ch02.responseValue (V i) (b i) p r (z i) = Book.Ch02.responseJ U a p r

    The weighted average over a subdivision of the response values of the restricted parent maximizer is the parent response.

    The subdivision defect identity #

    source
    theorem HCPolySupport.HighContrast.Response.sum_weight_responseJ_sub_responseJ_eq_sum_weight_secondVariation {d : ℕ} {ι : Type u_1} {Z : Finset ι} {U : Book.Ch02.Domain d} {V : ι → Book.Ch02.Domain d} {a : Book.Ch02.CoeffOn U} {b : (i : ι) → Book.Ch02.CoeffOn (V i)} (hrep : ∀ i ∈ Z, (b i).toCoeffField = a.toCoeffField) (hsub : ∀ i ∈ Z, (V i).carrier ⊆ U.carrier) (hdisj : (↑Z).PairwiseDisjoint fun (i : ι) => (V i).carrier) (hnull : MeasureTheory.volume (U.carrier \ ⋃ i ∈ ↑Z, (V i).carrier) = 0) {p r : Vec d} {v : Book.Ch02.Solution U a} (hv : Book.Ch02.IsResponseMaximizer U a p r v) {z : (i : ι) → Book.Ch02.Solution (V i) (b i)} (hz : ∀ i ∈ Z, (z i).toH1.grad = v.toH1.grad) :
    ∑ i ∈ Z, (MeasureTheory.volume (V i).carrier).toReal / (MeasureTheory.volume U.carrier).toReal * Book.Ch02.responseJ (V i) (b i) p r - Book.Ch02.responseJ U a p r = ∑ i ∈ Z, (MeasureTheory.volume (V i).carrier).toReal / (MeasureTheory.volume U.carrier).toReal * Book.Ch02.secondVariationEnergyValue (V i) (b i) (canonicalResponseSolution (V i) (b i) p r) (z i)

    The subdivision defect identity. The weighted average of the cells' responses exceeds the parent response by the weighted average of the symmetric energies of the gradient differences between the cell maximizers and the restricted parent maximizer.

    Nonnegativity #