High-contrast homogenization: Provider.Response.DiagonalWeakNormState

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

Optimizer states for the diagonal weak estimate

The diagonal weak estimate is stated for the canonical response optimizer of a coefficient sample on an adapted parent cell. This file turns that description into a source-facing object: a sample is restricted to the parent domain, the public canonical maximizer is selected, and its gradient and flux form the doubled state. Its energy is the square root of the normalized variational energy.

The adjoint sample is also constructed on the a.e.-quotient coefficient space. Its domain-local coefficient is a.e. equal to the transpose of the original domain-local coefficient, so the Chapter 2 transpose congruence applies without choosing an additional representative.

The adjoint coefficient sample

noncomputable def HCPolySupport.HighContrast.CoeffSpace.transpose {d : ℕ} (a : CoeffSpace d) : CoeffSpace d

The adjoint sample aᵗ, obtained by transposing the coefficient matrix at almost every point.

Equations

• a.transpose = ⟨MeasureTheory.AEEqFun.comp HCPolySupport.matTranspose ⋯ ↑a, ⋯⟩

theorem HCPolySupport.HighContrast.CoeffSpace.transpose_ae {d : ℕ} (a : CoeffSpace d) : ↑↑a.transpose =ᵐ[MeasureTheory.volume] fun (x : Vec d) => matTranspose (↑↑a x)

The adjoint sample is represented almost everywhere by the pointwise transpose of the original sample.

@[simp]

theorem HCPolySupport.HighContrast.CoeffSpace.transpose_transpose {d : ℕ} (a : CoeffSpace d) : a.transpose.transpose = a

Taking the adjoint twice returns the original coefficient sample.

theorem HCPolySupport.HighContrast.CoeffSpace.coeffOn_transpose_aeeq {d : ℕ} (a : CoeffSpace d) (U : Book.Ch02.Domain d) : (a.transpose.coeffOn U).AEEq (a.coeffOn U).transpose

On a Chapter 2 domain, restricting the adjoint sample agrees almost everywhere with transposing the restricted original sample.

theorem HCPolySupport.HighContrast.CoeffSpace.exists_pointwise_coeffOn_family_aeeq {d : ℕ} (a : CoeffSpace d) : ∃ (f : CoeffField d), ↑↑a =ᵐ[MeasureTheory.volume] f ∧ ∀ (U : Book.Ch02.Domain d), ∃ (b : Book.Ch02.CoeffOn U) (lam : ℝ) (Lam : ℝ), b.toCoeffField = f ∧ b.lam = lam ∧ b.Lam = Lam ∧ IsEllipticFieldOn lam Lam U.carrier f ∧ (a.coeffOn U).AEEq b

A sample admits one representative shared by every domain, elliptic at every point of each of them with that domain's own constants, together with the a.e. equality needed to transport its canonical optimizer.

theorem HCPolySupport.HighContrast.Response.coarseBlock_transpose {d : ℕ} (a : CoeffSpace d) (U : Book.Ch02.Domain d) : coarseBlock U.carrier a.transpose = Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul (coarseBlock U.carrier a) (Book.Ch02.blockDiag 1 (-1)))

Coarse response of an adjoint sample is the signed block congruence of the original response.

theorem HCPolySupport.HighContrast.Response.adaptedResponse_transpose {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) (w : Fin d → ℤ) (a : CoeffSpace d) : adaptedResponse q k w a.transpose = Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul (adaptedResponse q k w a) (Book.Ch02.blockDiag 1 (-1)))

The adjoint congruence on one adapted response block.

The canonical parent optimizer and its state

noncomputable def HCPolySupport.HighContrast.Response.diagonalWeakOptimizer {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (p r : Vec d) : Book.Ch02.Solution (adaptedDomain hq t) (a.coeffOn (adaptedDomain hq t))

The canonical variational maximizer v_t on the adapted parent cell U_t = q◇_t.

Equations

• HCPolySupport.HighContrast.Response.diagonalWeakOptimizer hq t a p r = (HCPolySupport.Book.Ch02.canonicalMaximizer ⋯ p r).toSolution

theorem HCPolySupport.HighContrast.Response.diagonalWeakOptimizer_isMaximizer {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (p r : Vec d) : Book.Ch02.IsResponseMaximizer (adaptedDomain hq t) (a.coeffOn (adaptedDomain hq t)) p r (diagonalWeakOptimizer hq t a p r)

The chosen optimizer is a response maximizer at the printed load.

noncomputable def HCPolySupport.HighContrast.Response.diagonalWeakState {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (p r : Vec d) : Vec d → BlockVec d

The doubled optimizer state X_t = (∇v_t,a∇v_t).

Equations

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

theorem HCPolySupport.HighContrast.Response.diagonalWeakState_eq {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (p r x : Vec d) : diagonalWeakState hq t a p r x = ((diagonalWeakOptimizer hq t a p r).toH1.grad x, matVecMul ((a.coeffOn (adaptedDomain hq t)).toCoeffField x) ((diagonalWeakOptimizer hq t a p r).toH1.grad x))

The defining equation of the doubled optimizer state.

noncomputable def HCPolySupport.HighContrast.Response.diagonalWeakEnergy {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (p r : Vec d) : ℝ

The normalized optimizer energy ℰ_t = ‖symm(a)¹⁄² ∇v_t‖_{L_underlined²(U_t)}.

Equations

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

theorem HCPolySupport.HighContrast.Response.diagonalWeakEnergy_eq {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (p r : Vec d) : diagonalWeakEnergy hq t a p r = √(Book.Ch02.variationEnergyValue (adaptedDomain hq t) (a.coeffOn (adaptedDomain hq t)) (diagonalWeakOptimizer hq t a p r))

The defining equation of the normalized optimizer energy.

theorem HCPolySupport.HighContrast.Response.diagonalWeakEnergy_nonneg {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (p r : Vec d) : 0 ≤ diagonalWeakEnergy hq t a p r

The normalized optimizer energy is nonnegative.

theorem HCPolySupport.HighContrast.Response.sq_diagonalWeakEnergy {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (p r : Vec d) : diagonalWeakEnergy hq t a p r ^ 2 = Book.Ch02.variationEnergyValue (adaptedDomain hq t) (a.coeffOn (adaptedDomain hq t)) (diagonalWeakOptimizer hq t a p r)

The square of the normalized optimizer energy is the variational energy.

theorem HCPolySupport.HighContrast.Response.responseJ_eq_sq_diagonalWeakEnergy {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (p r : Vec d) : Book.Ch02.responseJ (adaptedDomain hq t) (a.coeffOn (adaptedDomain hq t)) p r = 1 / 2 * diagonalWeakEnergy hq t a p r ^ 2

The response value is one half of the squared optimizer energy.

theorem HCPolySupport.HighContrast.Response.diagonalWeakState_memVectorL2 {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (p r : Vec d) : (MemVectorL2 (adaptedCell q t) fun (x : Vec d) => (diagonalWeakState hq t a p r x).1) ∧ MemVectorL2 (adaptedCell q t) fun (x : Vec d) => (diagonalWeakState hq t a p r x).2

The two slots of the optimizer state are square integrable on the parent cell.

theorem HCPolySupport.HighContrast.Response.blockCellAverage_diagonalWeakState {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (p r : Vec d) : blockCellAverage (adaptedCell q t) (diagonalWeakState hq t a p r) = (Book.Ch02.averageGradient (adaptedDomain hq t) (a.coeffOn (adaptedDomain hq t)) (diagonalWeakOptimizer hq t a p r), Book.Ch02.averageFlux (adaptedDomain hq t) (a.coeffOn (adaptedDomain hq t)) (diagonalWeakOptimizer hq t a p r))

The parent average of the optimizer state is the average-gradient/average- flux pair used by the variational identities.

theorem HCPolySupport.HighContrast.Response.blockCellAverage_diagonalWeakState_eq_response {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (p r : Vec d) : blockCellAverage (adaptedCell q t) (diagonalWeakState hq t a p r) = blockMatVecMul (Book.Ch02.blockR d) (blockMatVecMul (coarseBlock (adaptedCell q t) a) (-p, r)) + (-p, r)

The source average formula (X_t)_{U_t} = (R A_t + I)(-p,r).

The source adjoint state

noncomputable def HCPolySupport.HighContrast.Response.diagonalWeakAdjointState {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (p r : Vec d) : Vec d → BlockVec d

The adjoint doubled state X_t⁺ = (∇v_t⁺,aᵗ∇v_t⁺).

Equations

• HCPolySupport.HighContrast.Response.diagonalWeakAdjointState hq t a p r = HCPolySupport.HighContrast.Response.diagonalWeakState hq t a.transpose p r

noncomputable def HCPolySupport.HighContrast.Response.diagonalWeakAdjointEnergy {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (p r : Vec d) : ℝ

The adjoint optimizer energy.

Equations

• HCPolySupport.HighContrast.Response.diagonalWeakAdjointEnergy hq t a p r = HCPolySupport.HighContrast.Response.diagonalWeakEnergy hq t a.transpose p r

theorem HCPolySupport.HighContrast.Response.diagonalWeakAdjointState_eq {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (p r : Vec d) : diagonalWeakAdjointState hq t a p r = diagonalWeakState hq t a.transpose p r

theorem HCPolySupport.HighContrast.Response.diagonalWeakAdjointEnergy_eq {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (p r : Vec d) : diagonalWeakAdjointEnergy hq t a p r = diagonalWeakEnergy hq t a.transpose p r