High-contrast homogenization:

Provider.PolynomialHomogenization.Root.EnergyPrice.WitnessCubeSideGeometry

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

Gate R2-geo: the gauge cube side is at most 2‖L⁻¹‖

The bound ell ≤ 2 * ‖(matSqrt (symmPart abar))⁻¹‖ is not a hypothesis of the frame bound: it is a consequence of the inner-ellipsoid normalization premise U ⊆ ellipsoid abar 1, because ellipsoid is normalized by specBound (symmPart abar)⁻¹:

ellipsoid abar r = {x | x · (symmPart abar)⁻¹ x ≤ specBound (symmPart abar)⁻¹ · r²}

so the gauge image of ellipsoid abar 1 lies in the Euclidean ball of radius √(specBound (symmPart abar)⁻¹) = ‖(matSqrt (symmPart abar))⁻¹‖, and a translated triadic cube inside a ball of radius r has side at most 2r.

Coordinate bounds from the Euclidean square

theorem HCPolySupport.HighContrast.EnergyPrice.sq_le_vecNormSq {d : ℕ} (x : Vec d) (i : Fin d) : x i ^ 2 ≤ vecNormSq x

One coordinate square is at most the Euclidean square.

theorem HCPolySupport.HighContrast.EnergyPrice.abs_le_of_vecNormSq_le {d : ℕ} {x : Vec d} {r : ℝ} (hr : 0 ≤ r) (h : vecNormSq x ≤ r ^ 2) (i : Fin d) : |x i| ≤ r

A Euclidean bound gives a coordinate bound.

The gauge image of the unit ellipsoid

theorem HCPolySupport.HighContrast.EnergyPrice.norm_inv_matSqrt_sq {d : ℕ} {S : Mat d} (hS : Matrix.PosDef S) : ‖(matSqrt S)⁻¹‖ ^ 2 = specBound S⁻¹

‖(matSqrt S)⁻¹‖ ^ 2 = specBound S⁻¹.

theorem HCPolySupport.HighContrast.EnergyPrice.vecNormSq_le_of_mem_matImage_inv_matSqrt_ellipsoid {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {y : Vec d} (hy : y ∈ matImage (matSqrt (symmPart abar))⁻¹ (ellipsoid abar 1)) : vecNormSq y ≤ ‖(matSqrt (symmPart abar))⁻¹‖ ^ 2

The gauge image of the unit ellipsoid lies in the ball of radius ‖L⁻¹‖.

A translated cube inside a ball

theorem HCPolySupport.HighContrast.EnergyPrice.cubeScaleFactor_le_two_mul_of_translateSet_subset {d : ℕ} [NeZero d] {j : ℤ} {w : Vec d} {r : ℝ} (hr : 0 ≤ r) (hsub : translateSet w (openCubeSet (originCube d j)) ⊆ {y : Vec d | vecNormSq y ≤ r ^ 2}) : 3 ^ j ≤ 2 * r

A translate of a triadic cube contained in a Euclidean ball of radius r has side at most 2r.

The witness instance

theorem HCPolySupport.HighContrast.EnergyPrice.witnessCubeSide_le_two_mul_norm_inv_matSqrt {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} {j : ℤ} {z : Vec d} (hU : U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j)) (hinner : U ⊆ ellipsoid abar 1) : cubeScaleFactor (originCube d j) ≤ 2 * ‖(matSqrt (symmPart abar))⁻¹‖

Gate R2-geo, closed. At the frozen witness the gauge cube side is at most 2‖(matSqrt (symmPart abar))⁻¹‖, from the inner-ellipsoid normalization premise alone.