High-contrast homogenization: Entry.Response.Core.ScalarMaximizerExistence

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

Existence of the canonical scalar maximizer

This file proves existence of the canonical scalar maximizer on an adapted cell for each of the recentred coefficient a_- = a - g and its adjoint a_+ = aᵀ + g. It shows the set defining the weak response energy respWeakEnergy as a supremum is bounded above — both in general and for each of the two recentred coefficients and their associated respWMinus/respWPlus families — and that this energy equals the supremum over that set. Along the way it records that the Chapter-2 coefficient functional on an elliptic field is well defined and that the cell average respects almost-everywhere equality of the underlying field. This is the scalar-maximizer input to the response transfer p.response.transfer.

Maximizer existence on adapted cells

This file proves existence of canonical scalar maximizers on adapted cells for the recentred coefficient a_- = a - g and its adjoint a_+ = a^t + g, and the boundedness of the defining set of respWeakEnergy.

theorem HCPolySupport.HighContrast.Multiscale.adaptedCellTranslate_zero {d : ℕ} (q : Mat d) (j : ℤ) : adaptedCellTranslate q j 0 = adaptedCell q j

theorem HCPolySupport.HighContrast.Multiscale.volumeAverage_scalarResponseIntegrand_congr {d : ℕ} {U : Set (Vec d)} {a b : CoeffField d} (h : a =ᵐ[volumeMeasureOn U] b) (p q : Vec d) (u : AHarmonicFunction a U) (v : AHarmonicFunction b U) (hgrad : ∀ (x : Vec d), u.toH1.grad x = v.toH1.grad x) : volumeAverage U (scalarResponseIntegrand U a p q u) = volumeAverage U (scalarResponseIntegrand U b p q v)

theorem HCPolySupport.HighContrast.Multiscale.nonempty_scalarCanonicalMaximizer_of_aeEq {d : ℕ} {U : Set (Vec d)} {a b : CoeffField d} (h : a =ᵐ[volumeMeasureOn U] b) (p q : Vec d) (hv : Nonempty (ScalarCanonicalMaximizer U p q a)) : Nonempty (ScalarCanonicalMaximizer U p q b)

theorem HCPolySupport.HighContrast.Multiscale.nonempty_scalarCanonicalMaximizer_respCoeffMinus {d : ℕ} (q : Mat d) (hq : IsUnit q) (t : ℤ) (F : BlockMat d) (a : CoeffSpace d) (p r : Vec d) : Nonempty (ScalarCanonicalMaximizer (adaptedCell q t) p r (respCoeffMinus F a))

Existence of a canonical maximizer for a_- = a - g on U_t (p.response.transfer, e.response.energy.and.defect).

theorem HCPolySupport.HighContrast.Multiscale.nonempty_scalarCanonicalMaximizer_respCoeffPlus {d : ℕ} (q : Mat d) (hq : IsUnit q) (t : ℤ) (F : BlockMat d) (a : CoeffSpace d) (p r : Vec d) : Nonempty (ScalarCanonicalMaximizer (adaptedCell q t) p r (respCoeffPlus F a))

The adjoint twin for a_+ = a^t + g.

BddAbove for the sSup defining respWeakEnergy

The lemmas standardCell_subset_centeredCube_of_mem_triadicIndexBox and adaptedCellAtCenter_subset_adaptedCell below are also declared, under the same names, in ScaleAverageSeminorm.lean, which imports this file. The declarations here provide the copies needed in this file to prove bddAbove_respWeakEnergySet.

theorem HCPolySupport.HighContrast.Multiscale.standardCell_subset_centeredCube_of_mem_triadicIndexBox {d : ℕ} (t : ℤ) (n : ℕ) {w : Fin d → ℤ} (hw : w ∈ triadicIndexBox d n) : standardCell d (t - ↑n) w ⊆ centeredCube d t

theorem HCPolySupport.HighContrast.Multiscale.adaptedCellAtCenter_subset_adaptedCell {d : ℕ} (q : Mat d) (t : ℤ) (n : ℕ) {w : Fin d → ℤ} (hw : w ∈ triadicIndexBox d n) : adaptedCellAtCenter q (t - ↑n) w ⊆ adaptedCell q t

def HCPolySupport.HighContrast.Multiscale.respWeakEnergySet {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (qq : Mat d) (t : ℤ) (M0 : BlockMat d) (p q' : Vec d) (b : CoeffSpace d → CoeffField d) (Y : BlockVec d) : Set ℝ

The defining set of respWeakEnergy (ResponseBlockObjects.lean), named so that its boundedness can be stated.

Equations

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

theorem HCPolySupport.HighContrast.Multiscale.respWeakEnergy_eq_sSup_respWeakEnergySet {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (qq : Mat d) (t : ℤ) (M0 : BlockMat d) (p q' : Vec d) (b : CoeffSpace d → CoeffField d) (Y : BlockVec d) : respWeakEnergy P qq t M0 p q' b Y = sSup (respWeakEnergySet P qq t M0 p q' b Y)

def HCPolySupport.HighContrast.Multiscale.coeffOnOfIsEllipticFieldOn {d : ℕ} {U : Book.Ch02.Domain d} {lam Lam : ℝ} {f : CoeffField d} (hlam : 0 < lam) (hle : lam ≤ Lam) (hEll : IsEllipticFieldOn lam Lam U.carrier f) : Book.Ch02.CoeffOn U

A Chapter-2 coefficient object from a pointwise elliptic field on the domain.

Equations

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

theorem HCPolySupport.HighContrast.Multiscale.book_isResponseMaximizer_iff {d : ℕ} {U : Book.Ch02.Domain d} {a : Book.Ch02.CoeffOn U} {p q : Vec d} {v : Book.Ch02.Solution U a} : Book.Ch02.IsResponseMaximizer U a p q v ↔ IsResponseMaximizer U.carrier p q a.toCoeffField v

theorem HCPolySupport.HighContrast.Multiscale.besovSeminorm_congr {d : ℕ} {t : ℤ} {avg1 avg2 : ℕ → (Fin d → ℤ) → BlockVec d} (h : ∀ (n : ℕ), ∀ w ∈ triadicIndexBox d n, avg1 n w = avg2 n w) : besovSeminorm t avg1 = besovSeminorm t avg2

theorem HCPolySupport.HighContrast.Multiscale.cellAverage_congr_ae {d : ℕ} {V U : Set (Vec d)} (hVU : V ⊆ U) {X Z : Vec d → BlockVec d} (h : X =ᵐ[volumeMeasureOn U] Z) : cellAverage V X = cellAverage V Z

theorem HCPolySupport.HighContrast.Multiscale.bddAbove_respWeakEnergySet {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (qq : Mat d) (hq : IsUnit qq) (t : ℤ) (M0 : BlockMat d) (p q' : Vec d) (b : CoeffSpace d → CoeffField d) (Y : BlockVec d) (hb : ∀ (a : CoeffSpace d), ∃ (lam : ℝ) (Lam : ℝ) (f : CoeffField d), 0 < lam ∧ lam ≤ Lam ∧ IsEllipticFieldOn lam Lam (adaptedCell qq t) f ∧ b a =ᵐ[volumeMeasureOn (adaptedCell qq t)] f) : BddAbove (respWeakEnergySet P qq t M0 p q' b Y)

The defining set of respWeakEnergy is bounded above: by Chapter-2 a.e. gradient uniqueness any two admissible maximizer families give the same value.

theorem HCPolySupport.HighContrast.Multiscale.bddAbove_respWeakEnergySet_respCoeffMinus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (qq : Mat d) (hq : IsUnit qq) (t : ℤ) (M0 : BlockMat d) (p q' : Vec d) (F : BlockMat d) (Y : BlockVec d) : BddAbove (respWeakEnergySet P qq t M0 p q' (respCoeffMinus F) Y)

The defining set of respWeakEnergy for a_- = a - g is bounded above.

theorem HCPolySupport.HighContrast.Multiscale.bddAbove_respWeakEnergySet_respCoeffPlus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (qq : Mat d) (hq : IsUnit qq) (t : ℤ) (M0 : BlockMat d) (p q' : Vec d) (F : BlockMat d) (Y : BlockVec d) : BddAbove (respWeakEnergySet P qq t M0 p q' (respCoeffPlus F) Y)

The defining set of respWeakEnergy for a_+ = a^t + g is bounded above.

theorem HCPolySupport.HighContrast.Multiscale.bddAbove_respWeakEnergySet_respWMinus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (e : Vec d) (hgrid : IsUnit (respGrid jStar F)) : BddAbove (respWeakEnergySet P (respGrid jStar F) t (respM0 F) (respP (respMean P jStar F t) e) (respqMinus P jStar F t e) (respCoeffMinus F) (respYMinus P jStar F t e))

The sSup in respWMinus is over a set bounded above.

theorem HCPolySupport.HighContrast.Multiscale.bddAbove_respWeakEnergySet_respWPlus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (e : Vec d) (hgrid : IsUnit (respGrid jStar F)) : BddAbove (respWeakEnergySet P (respGrid jStar F) t (respM0 F) (respP (respMean P jStar F t) e) (respqPlus P jStar F t e) (respCoeffPlus F) (respYPlus P jStar F t e))

The sSup in respWPlus is over a set bounded above.

AK.HC (2.32), the optimizer-mean identity blockAverage_eq, stated on

Book.Ch02.Domain; Internal.Ch02.BookCh02.responseBasicVariationalIdentitiesTheory. Paper e.response.energy.and.defect (Y = (I + R A) x), the optimizer-mean identity.