High-contrast homogenization: Provider.Response.DiagonalWeakNormCarriers

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

Carriers for the diagonal adapted-cube weak norm

This file records the scalar and matrix quantities of the weak-norm estimate for the optimizer state used in p.response.transfer, from its normalization prefactors to its recent-scale sums. Infinite maxima take values in ℝ≥0∞; all recent-scale sums remain finite real sums.

Metric and load factors

noncomputable def HCPolySupport.HighContrast.Response.diagonalWeakMetricFactor {d : ℕ} (m0 : Mat d) (E : BlockMat d) : ℝ

The metric comparison factor K_{M,E} = |M₀⁻¹_prime² E M₀⁻¹_prime²|¹_prime², one of the normalization prefactors of the weak-norm estimate.

Equations

• HCPolySupport.HighContrast.Response.diagonalWeakMetricFactor m0 E = √(HCPolySupport.HighContrast.blockSize E (HCPolySupport.Book.Ch02.blockDiag m0 m0⁻¹))

theorem HCPolySupport.HighContrast.Response.diagonalWeakMetricFactor_eq {d : ℕ} (m0 : Mat d) (E : BlockMat d) : diagonalWeakMetricFactor m0 E = √(blockSize E (Book.Ch02.blockDiag m0 m0⁻¹))

The defining equation for K_{M,E}.

noncomputable def HCPolySupport.HighContrast.Response.diagonalWeakLoadMinus {d : ℕ} (E : BlockMat d) (p q : Vec d) : ℝ

The primal load factor L_E⁻(p,q) = |E¹_prime²(-p,q)|, the first of the two load sizes of the weak-norm estimate.

Equations

• HCPolySupport.HighContrast.Response.diagonalWeakLoadMinus E p q = √(HCPolySupport.blockVecDot (-p, q) (HCPolySupport.blockMatVecMul E (-p, q)))

theorem HCPolySupport.HighContrast.Response.diagonalWeakLoadMinus_eq {d : ℕ} (E : BlockMat d) (p q : Vec d) : diagonalWeakLoadMinus E p q = √(blockVecDot (-p, q) (blockMatVecMul E (-p, q)))

The defining equation for L_E⁻.

noncomputable def HCPolySupport.HighContrast.Response.diagonalWeakLoadPlus {d : ℕ} (E : BlockMat d) (p q : Vec d) : ℝ

The adjoint load factor L_E⁺(p,q) = |E¹_prime²(p,q)|, the second of the two load sizes of the weak-norm estimate.

Equations

• HCPolySupport.HighContrast.Response.diagonalWeakLoadPlus E p q = √(HCPolySupport.blockVecDot (p, q) (HCPolySupport.blockMatVecMul E (p, q)))

theorem HCPolySupport.HighContrast.Response.diagonalWeakLoadPlus_eq {d : ℕ} (E : BlockMat d) (p q : Vec d) : diagonalWeakLoadPlus E p q = √(blockVecDot (p, q) (blockMatVecMul E (p, q)))

The defining equation for L_E⁺.

theorem HCPolySupport.HighContrast.Response.diagonalWeakMetricFactor_nonneg {d : ℕ} (m0 : Mat d) (E : BlockMat d) : 0 ≤ diagonalWeakMetricFactor m0 E

theorem HCPolySupport.HighContrast.Response.diagonalWeakLoadMinus_nonneg {d : ℕ} (E : BlockMat d) (p q : Vec d) : 0 ≤ diagonalWeakLoadMinus E p q

theorem HCPolySupport.HighContrast.Response.diagonalWeakLoadPlus_nonneg {d : ℕ} (E : BlockMat d) (p q : Vec d) : 0 ≤ diagonalWeakLoadPlus E p q

The all-scale maximum

noncomputable def HCPolySupport.HighContrast.Response.diagonalWeakMaximum {d : ℕ} (rho : ℝ) (q : Mat d) (t : ℤ) (E : BlockMat d) (a : CoeffSpace d) : ENNReal

The all-scale maximum ℳ_{t,ρ}(E), the weighted maximum of the positive parts of the normalized block defects over the lower generations. The supremum ranges over every integer k ≤ t, so its fail-closed value is extended real.

Equations

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

theorem HCPolySupport.HighContrast.Response.diagonalWeakMaximum_eq {d : ℕ} (rho : ℝ) (q : Mat d) (t : ℤ) (E : BlockMat d) (a : CoeffSpace d) : diagonalWeakMaximum rho q t E a = ⨆ (k : ℤ), ⨆ (_ : k ≤ t), ⨆ w ∈ alignedIndex q k t, ENNReal.ofReal (3 ^ (-rho * (↑t - ↑k)) * blockExcess (adaptedResponse q k w a) E)

The defining equation for the all-scale maximum.

theorem HCPolySupport.HighContrast.Response.weighted_excess_le_diagonalWeakMaximum {d : ℕ} (rho : ℝ) (q : Mat d) (t k : ℤ) (E : BlockMat d) (a : CoeffSpace d) (hkt : k ≤ t) (w : Fin d → ℤ) (hw : w ∈ alignedIndex q k t) : ENNReal.ofReal (3 ^ (-rho * (↑t - ↑k)) * blockExcess (adaptedResponse q k w a) E) ≤ diagonalWeakMaximum rho q t E a

Every aligned cell term is bounded by the all-scale maximum.

Recent defects

noncomputable def HCPolySupport.HighContrast.Response.diagonalWeakCellDefect {d : ℕ} (q : Mat d) (k t : ℤ) (E : BlockMat d) (a : CoeffSpace d) : ℝ

The recent cell defect C_{k,t}(E) of the weak-norm estimate.

Equations

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

theorem HCPolySupport.HighContrast.Response.diagonalWeakCellDefect_eq {d : ℕ} (q : Mat d) (k t : ℤ) (E : BlockMat d) (a : CoeffSpace d) : diagonalWeakCellDefect q k t E a = √(avsum (alignedIndex q k t) fun (w : Fin d → ℤ) => blockSize (blockSub (adaptedResponse q k w a) (coarseBlock (adaptedCell q t) a)) E ^ 2)

The defining equation for C_{k,t}(E).

noncomputable def HCPolySupport.HighContrast.Response.diagonalWeakAverageDefect {d : ℕ} (q : Mat d) (k t : ℤ) (E : BlockMat d) (a : CoeffSpace d) : BlockMat d

The recent averaged normalized defect D_{k,t}(E) of the weak-norm estimate.

Equations

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

theorem HCPolySupport.HighContrast.Response.diagonalWeakAverageDefect_eq {d : ℕ} (q : Mat d) (k t : ℤ) (E : BlockMat d) (a : CoeffSpace d) : diagonalWeakAverageDefect q k t E a = ofFullBlockMat ((↑(alignedIndex q k t).card)⁻¹ • ∑ w ∈ alignedIndex q k t, toFullBlockMat (normalizedBlock (blockSub (adaptedResponse q k w a) (coarseBlock (adaptedCell q t) a)) E))

The defining equation for D_{k,t}(E).

theorem HCPolySupport.HighContrast.Response.diagonalWeakCellDefect_nonneg {d : ℕ} (q : Mat d) (k t : ℤ) (E : BlockMat d) (a : CoeffSpace d) : 0 ≤ diagonalWeakCellDefect q k t E a

Recent finite sums

noncomputable def HCPolySupport.HighContrast.Response.diagonalWeakCellSum {d : ℕ} (q : Mat d) (t : ℤ) (H : ℕ) (s : ℝ) (E : BlockMat d) (a : CoeffSpace d) : ℝ

The recent cell sum 𝒰_cell, the weighted sum of the recent cell defects over the finite window. The index j represents the scale k = t-j; range (H+1) includes both endpoints.

Equations

• HCPolySupport.HighContrast.Response.diagonalWeakCellSum q t H s E a = ∑ j ∈ Finset.range (H + 1), 3 ^ (-s * ↑j) * HCPolySupport.HighContrast.Response.diagonalWeakCellDefect q (t - ↑j) t E a

theorem HCPolySupport.HighContrast.Response.diagonalWeakCellSum_eq {d : ℕ} (q : Mat d) (t : ℤ) (H : ℕ) (s : ℝ) (E : BlockMat d) (a : CoeffSpace d) : diagonalWeakCellSum q t H s E a = ∑ j ∈ Finset.range (H + 1), 3 ^ (-s * ↑j) * diagonalWeakCellDefect q (t - ↑j) t E a

The defining equation for 𝒰_cell.

noncomputable def HCPolySupport.HighContrast.Response.diagonalWeakAverageSum {d : ℕ} (q : Mat d) (t : ℤ) (H : ℕ) (s rho : ℝ) (E : BlockMat d) (a : CoeffSpace d) : ℝ

The recent averaged-defect sum 𝒰_av, the weighted sum of the averaged recent defects over the finite window.

Equations

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

theorem HCPolySupport.HighContrast.Response.diagonalWeakAverageSum_eq {d : ℕ} (q : Mat d) (t : ℤ) (H : ℕ) (s rho : ℝ) (E : BlockMat d) (a : CoeffSpace d) : diagonalWeakAverageSum q t H s rho E a = ∑ j ∈ Finset.range (H + 1), 3 ^ (-(s - rho / 2) * ↑j) * √(blockSize (diagonalWeakAverageDefect q (t - ↑j) t E a) (Book.Ch02.blockIdentity d))

The defining equation for 𝒰_av.

theorem HCPolySupport.HighContrast.Response.diagonalWeakCellSum_nonneg {d : ℕ} (q : Mat d) (t : ℤ) (H : ℕ) (s : ℝ) (E : BlockMat d) (a : CoeffSpace d) : 0 ≤ diagonalWeakCellSum q t H s E a

theorem HCPolySupport.HighContrast.Response.diagonalWeakAverageSum_nonneg {d : ℕ} (q : Mat d) (t : ℤ) (H : ℕ) (s rho : ℝ) (E : BlockMat d) (a : CoeffSpace d) : 0 ≤ diagonalWeakAverageSum q t H s rho E a