High-contrast homogenization: Provider.Initialization.Reference

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

Reference-block facts used by source initialization

The coarse ellipticity assumption reaches an actual centered coarse block. That block is self-dominating under sharp, and sharp reverses the reference comparison, which yields the printed order E♯ ≤ E.

theorem HCPolySupport.HighContrast.Initialization.blockMatLoewnerLE_blockSharp_reference {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) : BlockMatLoewnerLE (blockSharp E) E

The reference block dominates its sharp whenever it occurs in a coarse ellipticity assumption at a probability law.

theorem HCPolySupport.HighContrast.Initialization.one_le_kappaRef {d : ℕ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (hsharp : BlockMatLoewnerLE (blockSharp E) E) [Nonempty (Fin d)] : 1 ≤ kappaRef E

A positive block above its sharp has reference ratio at least one.

theorem HCPolySupport.HighContrast.Initialization.blockMatLoewnerLE_reference_kappaRef_blockSharp {d : ℕ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) : BlockMatLoewnerLE E (blockScale (kappaRef E) (blockSharp E))

The reference block is bounded by its sharp with the intrinsic reference ratio as the exact dilation.

theorem HCPolySupport.HighContrast.Initialization.one_le_initIdentityConst {d : ℕ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (hsharp : BlockMatLoewnerLE (blockSharp E) E) [Nonempty (Fin d)] : 1 ≤ initIdentityConst E

The identity-grid constant is at least one under the reference sharp order.

theorem HCPolySupport.HighContrast.Initialization.one_add_six_refContrast_sub_one_le {d : ℕ} {E : BlockMat d} (haspect : refContrast E ≤ aspectRatio E) : 1 + 6 * (refContrast E - 1) ≤ 6 * aspectRatio E

The last reference comparison is the arithmetic consequence of the two intrinsic-contrast comparisons preceding it.

theorem HCPolySupport.HighContrast.Initialization.initIdentityConst_le {d : ℕ} {E : BlockMat d} (hkappa : kappaRef E ≤ 6 * aspectRatio E) : initIdentityConst E ≤ 24 * aspectRatio E

The printed identity-grid upper bound follows once the canonical entry ratio is bounded by six times the aspect ratio.