High-contrast homogenization: Provider.Transport.TransportCoefficients

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

The transport source coefficients

The source residual the transport pays at a target level of the new grid is measured by the two source coefficients of the transport estimate: the continued one 𝖣_cont^{tr,𝒮}(q,q') = C_dK(q,q')κ_𝐄B_qB_{q'}χ_g𝒰², which the old-times-new orientation of the boundary rows produces, and the early one 𝖣_early^{tr,𝒮}(q') = C_dκ_𝐄B_{q'}²𝒰², which the new-squared orientation of the whole-cell rows produces. The total coefficient 𝖣_src^{tr,𝒮} = 1 + 𝖣_cont^{tr,𝒮} + 𝖣_early^{tr,𝒮} is what the transported source majorant is built from.

This file records the order relations between the three that every source estimate reads. Each factor of the two rows is nonnegative — the cross-grid factor is at least one, the reference ratio is an infimum of nonnegative numbers, the boundary constant is a nonnegative multiple of a square root, and the geometric series χ_g is positive below the critical exponent — so the two rows are nonnegative, the total is at least one, and it dominates each of them. Without the last two the printed majorant would not majorize the printed rows and the source estimate would be false as written.

theorem HCPolySupport.HighContrast.Transport.zero_le_kappaRef {d : ℕ} (E : BlockMat d) : 0 ≤ kappaRef E

The reference ratio is nonnegative, being an infimum of nonnegative numbers.

theorem HCPolySupport.HighContrast.Transport.zero_lt_chiG {g : ℝ} (hg : g < 1) : 0 < chiG g

The geometric series χ_g = (3^{1-g} - 1)^{-1} is positive below the critical exponent.

theorem HCPolySupport.HighContrast.Transport.zero_le_transportContCoeff {d : ℕ} {Cd g : ℝ} (hCd : 0 ≤ Cd) (hg : g < 1) (E : BlockMat d) (jStar : ℤ) (mu mu' : Mat d) : 0 ≤ transportContCoeff Cd g E jStar mu mu'

The continued transport coefficient 𝖣_cont^{tr,𝒮}(q,q') = C_dK(q,q')κ_𝐄B_qB_{q'}χ_g𝒰² is nonnegative.

theorem HCPolySupport.HighContrast.Transport.zero_le_transportEarlyCoeff {d : ℕ} {Cd g : ℝ} (hCd : 0 ≤ Cd) (hg : g < 1) (E : BlockMat d) (mu' : Mat d) : 0 ≤ transportEarlyCoeff Cd g E mu'

The early transport coefficient 𝖣_early^{tr,𝒮}(q') = C_dκ_𝐄B_{q'}²𝒰² is nonnegative.

theorem HCPolySupport.HighContrast.Transport.one_le_transportSrcCoeff {d : ℕ} {Cd g : ℝ} (hCd : 0 ≤ Cd) (hg : g < 1) (E : BlockMat d) (jStar : ℤ) (mu mu' : Mat d) : 1 ≤ transportSrcCoeff Cd g E jStar mu mu'

The total transport source coefficient is at least one, being one plus the two nonnegative rows.

theorem HCPolySupport.HighContrast.Transport.transportContCoeff_le_transportSrcCoeff {d : ℕ} {Cd g : ℝ} (hCd : 0 ≤ Cd) (hg : g < 1) (E : BlockMat d) (jStar : ℤ) (mu mu' : Mat d) : transportContCoeff Cd g E jStar mu mu' ≤ transportSrcCoeff Cd g E jStar mu mu'

The continued row is dominated by the total source coefficient.

theorem HCPolySupport.HighContrast.Transport.transportEarlyCoeff_le_transportSrcCoeff {d : ℕ} {Cd g : ℝ} (hCd : 0 ≤ Cd) (hg : g < 1) (E : BlockMat d) (jStar : ℤ) (mu mu' : Mat d) : transportEarlyCoeff Cd g E mu' ≤ transportSrcCoeff Cd g E jStar mu mu'

The early row is dominated by the total source coefficient.