High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.HomotheticEllipsoidVolume

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

Homothetic ellipsoid volume comparisons

Positive scalar dilation preserves the ellipsoid shape and scales its volume by the dimension power. Consequently normalized weighted energies compare uniformly across a bounded ratio of radii, independently of the matrix.

theorem HCPolySupport.HighContrast.Root.matImage_smul_one_ellipsoid {d : ℕ} (abar : Mat d) {q : ℝ} (hq : 0 < q) (r : ℝ) : matImage (q • 1) (ellipsoid abar r) = ellipsoid abar (q * r)

An ellipsoid at a positively dilated radius is the image of the original ellipsoid by the same scalar dilation.

theorem HCPolySupport.HighContrast.Root.volume_ellipsoid_mul {d : ℕ} (abar : Mat d) {q : ℝ} (hq : 0 < q) (r : ℝ) : MeasureTheory.volume (ellipsoid abar (q * r)) = ENNReal.ofReal (q ^ d) * MeasureTheory.volume (ellipsoid abar r)

Positive scalar dilation multiplies ellipsoid volume by q^d.

theorem HCPolySupport.HighContrast.Root.ellipsoid_mono_of_nonneg {d : ℕ} (abar : Mat d) {r R : ℝ} (hr : 0 ≤ r) (hrR : r ≤ R) : ellipsoid abar r ⊆ ellipsoid abar R

Ellipsoids are monotone in a nonnegative radius.

theorem HCPolySupport.HighContrast.Root.volume_ellipsoid_div_le_of_le_mul {d : ℕ} (abar : Mat d) {r R q : ℝ} (hS : Matrix.PosDef (symmPart abar)) (hr : 0 < r) (hrR : r ≤ R) (hq : 1 ≤ q) (hRq : R ≤ q * r) : MeasureTheory.volume (ellipsoid abar R) / MeasureTheory.volume (ellipsoid abar r) ≤ ENNReal.ofReal (q ^ d)

The volume ratio of two positive-radius ellipsoids is bounded only by a prescribed dilation factor, not by the defining matrix.