High-contrast homogenization: Provider.Response.WeakNormAPI

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

The scale-average seminorm: the estimates its proofs read

The weak-norm estimate for the optimizer state uses the concrete scale-average seminorm through five operations, all recorded here.

• At each scale, the normalized ℓ^2 length (avsum_z|·|^2)^{1/2} obeys Cauchy-Schwarz and the triangle inequality; the triangle inequality is what the recent-scale decomposition `(X_t){U_k(z)} - (X_t){U_t} = ((X(U_k(z))){U_k(z)} - (X_t){U_t})
  • (X_t - X(U_k(z)))_{U_k(z)}` is summed through, and the uniform bound is what turns the cell-averaged energy bound into the scale-by-scale energy bound.
• Across scales, a scalewise majorant majorizes the seminorm, and a scalewise splitting splits it; this is the passage from the scale-by-scale energy bound to the weak-norm bound on the bad event and to the contribution of the old scales.
• The normalization 3^{-st}[·] of the printed left side is the seminorm with 3^{sk} replaced by 3^{-s(t-k)}.
• The value is recovered as a real number exactly on the summable branch, the estimate being asserted also when the sum diverges; the geometric sum that makes both scale sums converge is the companion module.

The ℓ^2 inequalities are proved once on the flattened index 𝒵 × (d ⊕ d), where the doubled Euclidean structure of ℝ^{2d} and the normalized counting structure of the aligned index are a single finite sum.

The normalized ℓ^2 length of one scale

theorem HCPolySupport.HighContrast.Response.sum_blockVecDot_eq_sum_prod {d : ℕ} {ι : Type u_1} (Z : Finset ι) (u v : ι → BlockVec d) : ∑ z ∈ Z, blockVecDot (u z) (v z) = ∑ p ∈ Z ×ˢ Finset.univ, Sum.elim (fun (i : Fin d) => (u p.1).1 i) (fun (i : Fin d) => (u p.1).2 i) p.2 * Sum.elim (fun (i : Fin d) => (v p.1).1 i) (fun (i : Fin d) => (v p.1).2 i) p.2

The doubled Euclidean pairing expands on the flattened index.

theorem HCPolySupport.HighContrast.Response.sq_sum_blockVecDot_le {d : ℕ} {ι : Type u_1} (Z : Finset ι) (u v : ι → BlockVec d) : (∑ z ∈ Z, blockVecDot (u z) (v z)) ^ 2 ≤ (∑ z ∈ Z, blockVecDot (u z) (u z)) * ∑ z ∈ Z, blockVecDot (v z) (v z)

Cauchy-Schwarz for the doubled pairing over a finite index set.

theorem HCPolySupport.HighContrast.Response.sq_avsum_blockVecDot_le {d : ℕ} {ι : Type u_1} (Z : Finset ι) (u v : ι → BlockVec d) : (avsum Z fun (z : ι) => blockVecDot (u z) (v z)) ^ 2 ≤ (avsum Z fun (z : ι) => blockVecDot (u z) (u z)) * avsum Z fun (z : ι) => blockVecDot (v z) (v z)

Cauchy-Schwarz for the normalized cell average.

theorem HCPolySupport.HighContrast.Response.blockVecDot_add_self {d : ℕ} (u v : BlockVec d) : blockVecDot (u + v) (u + v) = blockVecDot u u + 2 * blockVecDot u v + blockVecDot v v

The doubled Euclidean square of a sum.

theorem HCPolySupport.HighContrast.Response.blockAvsumL2_add_le {d : ℕ} {ι : Type u_1} (Z : Finset ι) (u v : ι → BlockVec d) : (blockAvsumL2 Z fun (z : ι) => u z + v z) ≤ blockAvsumL2 Z u + blockAvsumL2 Z v

The triangle inequality of one scale: the normalized ℓ^2 length is subadditive. This is the inequality the recent-scale decomposition of the weak-norm estimate is summed through.

The seminorm across scales

theorem HCPolySupport.HighContrast.Response.ofReal_rpow_mul_adaptedWeakSeminorm {d : ℕ} (q : Mat d) (t : ℤ) (s : ℝ) (F : Vec d → BlockVec d) : ENNReal.ofReal (3 ^ (-(s * ↑t))) * adaptedWeakSeminorm q t s F = ∑' (j : ℕ), ENNReal.ofReal (3 ^ (-(s * ↑j)) * blockAvsumL2 (alignedIndex q (t - ↑j) t) fun (z : Fin d → ℤ) => blockCellAverage (adaptedCellAt q (t - ↑j) z) F)

The normalized left side 3^{-st}[F]_{B^{-s}_{2,1}(U_t)} of the weak-norm estimate: the scale weights become the decay factors 3^{-s(t-k)}.

The value on the summable branch