High-contrast homogenization: Provider.Initialization.ReferenceComparison

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

The reference comparison κ_𝐄 ≤ 6 Π

The factor-six reference-block comparison states κ_𝐄 ≤ 1 + 6(Θ - 1) ≤ 6 Π for a reference block whose sharp it dominates. The printed derivation routes through the display preceding (2.98) of Armstrong–Kuusi, an inequality about the un-corrected Schur block; the route taken here reaches the final bound κ_𝐄 ≤ 6 Π directly from the reference aspect ratio, and it is elementary.

Write (σ, σ_*, k) for the Schur data of 𝐄, so that

• the quadratic form of 𝐄 at (x, y) is ⟨σ x, x⟩ + ⟨σ_*⁻¹ (y - k x), y - k x⟩;
• the sharp has Schur data (σ_*, σ, -kᵗ), so its quadratic form at (x, y) is ⟨σ_* x, x⟩ + ⟨σ⁻¹ (y + kᵗ x), y + kᵗ x⟩.

Three inputs are used, all already available. The ordering 𝐄^♯ ≤ 𝐄 gives σ_* ≤ σ on the lower-right blocks. The skew matrix realizing Λ_0 gives σ + mᵗ σ_*⁻¹ m ≤ Λ_0 · I with m = k - h, and I ≤ |σ_*⁻¹| σ_* turns that into σ + mᵗ σ_*⁻¹ m ≤ Π σ_*, whence both σ ≤ Π σ_* and mᵗ σ_*⁻¹ m ≤ (Π - 1) σ_*. Transposition preserves the second bound, and the symmetric part K = k + kᵗ = m + mᵗ therefore satisfies K σ_*⁻¹ K ≤ 4(Π - 1) σ_*.

The comparison is then one application of Young's inequality with the weight five: writing w = y + kᵗ x, so that y - k x = w - K x,

⟨σ_*⁻¹ (w - K x), w - K x⟩ ≤ 6 ⟨σ_*⁻¹ w, w⟩ + (6/5) ⟨σ_*⁻¹ K x, K x⟩,

and the three displayed bounds turn the left side of the comparison into (6Π - (Π/5 + 24/5)) ⟨σ_* x, x⟩ + 6 ⟨σ_*⁻¹ w, w⟩, which is below 6Π (⟨σ_* x, x⟩ + ⟨σ⁻¹ w, w⟩) because σ_*⁻¹ ≤ Π σ⁻¹. The slack Π/5 + 24/5 is why the printed constant six survives the cruder route.

Quadratic forms of a Schur block

theorem HCPolySupport.HighContrast.Initialization.dotProduct_mulVec_schurBlock {d : ℕ} (a b c : Mat d) (x y : Vec d) : Sum.elim x y ⬝ᵥ Matrix.mulVec (schurBlock a b c) (Sum.elim x y) = x ⬝ᵥ Matrix.mulVec a x + (y - Matrix.mulVec c x) ⬝ᵥ b⁻¹.mulVec (y - Matrix.mulVec c x)

The quadratic form of a Schur block. At (x, y) the block G_{-c}ᵗ diag(a, b⁻¹) G_{-c} reads ⟨a x, x⟩ + ⟨b⁻¹ (y - c x), y - c x⟩.

Two matrix inequalities

The Schur form of a symmetric positive block

theorem HCPolySupport.HighContrast.Initialization.toFullBlockMat_eq_schurBlock {d : ℕ} {E : BlockMat d} (hsymm : IsSymmetricBlockMat E) (hpos : Book.Ch02.BlockPosDef E) : toFullBlockMat E = schurBlock (schurSigma E) (schurSigmaStar E) (schurSkew E)

The Schur form. A symmetric positive definite doubled block is the Schur form of its own Schur data.

The reference comparison

theorem HCPolySupport.HighContrast.Initialization.kappaRef_le_six_mul_aspectRatio {d : ℕ} [NeZero d] {E : BlockMat d} (hsymm : IsSymmetricBlockMat E) (hpos : Book.Ch02.BlockPosDef E) (hsharp : BlockMatLoewnerLE (blockSharp E) E) : kappaRef E ≤ 6 * aspectRatio E

The factor-six reference-block comparison κ_𝐄 ≤ 6 Π, for a symmetric positive doubled block dominating its own sharp.

theorem HCPolySupport.HighContrast.Initialization.kappaRef_le_six_mul_aspectRatio_of_coarseEllipticityDagger {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) : kappaRef E ≤ 6 * aspectRatio E

The reference comparison under the coarse ellipticity assumption. At a probability law the reference block of e.coarse.ellipticity dominates its own sharp, so the factor-six reference-block comparison applies to it.