High-contrast homogenization: Entry.Multiscale.Global.DeterminantBounds

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

Determinant bounds for the adapted mean

The determinant bounds of the entry generation, serving p.global.selection: the reference comparison 𝐄 ≤ 6Π · 𝐑𝐄⁻¹𝐑, the resulting upper bound blockLogDet 𝐀 ≤ d log (24Π) under the initialization sandwich 𝐀 ≤ 2𝐄, and the symmetry and positivity of the adapted mean.

Local reconstructions of the private helpers of HCPoly/Entry/Analysis/ReferenceComparison.lean and HCPoly/Entry/Analysis/InverseJensen.lean, needed here because those declarations are private there.

Reference-comparison and inverse-Jensen goals of p.global.selection, built from the rc_* helpers above.

theorem HCPolySupport.HighContrast.Multiscale.refBlock_le_six_aspect {d : ℕ} (E : BlockMat d) (hEs : IsSymmetricBlockMat E) (hE : Book.Ch02.BlockPosDef E) : BlockMatLoewnerLE E (blockScale (6 * aspectRatio E) (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat E)⁻¹ * toFullBlockMat (blockSwap d))))

p.global.selection reference comparison 𝐄 ≤ 6Π · 𝐑 𝐄⁻¹ 𝐑, Π = aspectRatio E, proved directly from exists_isSkewMat_bigLambdaRef_eq and the rc_* reconstructions below.

theorem HCPolySupport.HighContrast.Multiscale.blockLogDet_le_of_initial_sandwich {d : ℕ} (E A : BlockMat d) (hEs : IsSymmetricBlockMat E) (hE : Book.Ch02.BlockPosDef E) (hAs : IsSymmetricBlockMat A) (hA : Book.Ch02.BlockPosDef A) (hAR : 0 < aspectRatio E) (hsix : BlockMatLoewnerLE E (blockScale (6 * aspectRatio E) (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat E)⁻¹ * toFullBlockMat (blockSwap d))))) (hup : BlockMatLoewnerLE A (blockScale 2 E)) : blockLogDet A ≤ ↑d * Real.log (24 * aspectRatio E)

p.global.selection upper bound: det 𝐀 ≤ 2^{2d} det 𝐄 ≤ (24Π)^d from 𝐀 ≤ 2𝐄, 𝐄 ≤ 6Π 𝐑𝐄⁻¹𝐑 and det 𝐄 · det(𝐑𝐄⁻¹𝐑) = 1.