High-contrast homogenization: Provider.Response.DiagonalWeakNormPrimal

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

theorem HCPolySupport.HighContrast.Response.diagonalWeakNorm_primal_le {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (H : ℕ) {S m : Mat d} (hsymm : matTranspose S = S) (hsq : S * S = m) (hm : Matrix.PosDef m) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {rho s delta : ℝ} (hrho : 0 < rho) (hrho2 : rho < 2) (hs : rho / 2 < s) (hs1 : s ≤ 1) (hdelta : 0 < delta) (hdelta1 : delta ≤ 1) {a : CoeffSpace d} (p r : Vec d) : (ENNReal.ofReal (3 ^ (-(s * ↑t))) * adaptedWeakSeminorm q t s fun (x : Vec d) => blockMatVecMul (Book.Ch02.blockDiag S S⁻¹) (diagonalWeakState hq t a p r x - blockCellAverage (adaptedCell q t) (diagonalWeakState hq t a p r))) ≤ if diagonalWeakMaximum rho q t E a = ⊤ then ⊤ else ENNReal.ofReal (16 * diagonalWeakMetricFactor m E * diagonalWeakLoadMinus E p r * (diagonalWeakCellSum q t H s E a + diagonalWeakAverageSum q t H s rho E a) + (16 * (√delta)⁻¹ / (2 * s - rho) * diagonalWeakMetricFactor m E * if delta < (diagonalWeakMaximum rho q t E a).toReal then √(diagonalWeakMaximum rho q t E a).toReal else 3 ^ (-((s - rho / 2) * ↑H))) * diagonalWeakEnergy hq t a p r)

The released split level

noncomputable def HCPolySupport.HighContrast.Response.maxGroupConstantAtLevel (delta : ℝ) : ℝ

The maximum-group coefficient at a released split level. It is 16 at the fixed level.

Equations

• HCPolySupport.HighContrast.Response.maxGroupConstantAtLevel delta = 8 * (1 + √delta) * max 1 (√delta)⁻¹

theorem HCPolySupport.HighContrast.Response.zero_le_maxGroupConstantAtLevel (delta : ℝ) : 0 ≤ maxGroupConstantAtLevel delta

theorem HCPolySupport.HighContrast.Response.diagonalWeakNorm_primal_at_level_le {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (H : ℕ) {S m : Mat d} (hsymm : matTranspose S = S) (hsq : S * S = m) (hm : Matrix.PosDef m) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {rho s delta : ℝ} (hrho : 0 < rho) (hs : rho / 2 < s) (hs1 : s ≤ 1) (hdelta : 0 < delta) {a : CoeffSpace d} (p r : Vec d) : (ENNReal.ofReal (3 ^ (-(s * ↑t))) * adaptedWeakSeminorm q t s fun (x : Vec d) => blockMatVecMul (Book.Ch02.blockDiag S S⁻¹) (diagonalWeakState hq t a p r x - blockCellAverage (adaptedCell q t) (diagonalWeakState hq t a p r))) ≤ if diagonalWeakMaximum rho q t E a = ⊤ then ⊤ else ENNReal.ofReal (recentConstantAtLevel delta * diagonalWeakMetricFactor m E * diagonalWeakLoadMinus E p r * (diagonalWeakCellSum q t H s E a + diagonalWeakAverageSum q t H s rho E a) + (maxGroupConstantAtLevel delta / (2 * s - rho) * diagonalWeakMetricFactor m E * if delta < (diagonalWeakMaximum rho q t E a).toReal then √(diagonalWeakMaximum rho q t E a).toReal else 3 ^ (-((s - rho / 2) * ↑H))) * diagonalWeakEnergy hq t a p r)

The primal all-scale estimate at a released split level.