High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.WitnessCubeTwoSidedGeometry

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

The two-sided witness cube/ball geometry

The sign condition 0 ≤ j is false in general and is replaced by a bound 3 ^ (−r j) ≤ Cgeo, with the law-free Cgeo left as a residue: it needs the lower companion of witnessCubeSide_le_two_mul_norm_inv_matSqrt.

In gauge coordinates the frozen witness domain is the translated open triadic cube of generation j (matImage_inv_affineImage), and ellipsoid abar r pulls back to the exact Euclidean sublevel set of radius α r, α = √(specBound (symmPart abar)⁻¹) = ‖(matSqrt (symmPart abar))⁻¹‖ (matImage_matSqrt_inv_ellipsoid_eq). A ball inside an open cube of side ℓ forces 2 · radius ≤ ℓ — the antipodal-coordinate argument below — and this is the exact converse of the energy's cube-inside-ball estimate.

Hence, from surface:

2 α / (3 √d)  ≤  3 ^ j  ≤  2 α        (inner-ellipsoid normalization inner premise;
inner-ellipsoid normalization outer premise)
2 ρ           ≤  3 ^ j                (the frozen ball sandwich)
ρ             ≤  α                    (the two combined)

and Cgeo := (ρ / (3 √d)) ^ (−r) is a function of (d, ρ, r) alone, which is exactly C₀ s₀ ρ Rad's permitted dependence.

The cube-side convention is the coordinate one: openCubeSet (originCube d j) is (−3^j/2, 3^j/2)^d, so a contained ball of radius t obeys 2 t ≤ 3^j with no √d; the √d in Cgeo is the one carried by the printed inner radius 1/(3√d), not by the cube.

A ball inside an open triadic cube

theorem HCPolySupport.HighContrast.RowSupply.two_mul_le_cubeScale_of_antipodal_mem {d : ℕ} [NeZero d] {j : ℤ} {w cc : Vec d} {t : ℝ} (hmem : ∀ (v : Vec d), vecNormSq v ≤ t ^ 2 → cc + v ∈ translateSet w (openCubeSet (originCube d j))) : 2 * t ≤ 3 ^ j

A Euclidean ball inside a translated open triadic cube has diameter at most the side. This is the converse of the energy's cubeScaleFactor_le_two_mul_of_translateSet_subset.

The gauge picture of the frozen witness

theorem HCPolySupport.HighContrast.RowSupply.gaugeDomain_eq_translateSet {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)) : matImage (matSqrt (symmPart abar))⁻¹ U = translateSet (matVecMul (matSqrt (symmPart abar))⁻¹ z) (openCubeSet (originCube d j))

The gauge domain of the frozen witness is the translated open cube.

theorem HCPolySupport.HighContrast.RowSupply.norm_inv_matSqrt_eq_sqrt_specBound {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) : ‖(matSqrt (symmPart abar))⁻¹‖ = √(specBound (symmPart abar)⁻¹)

The gauge scale α = ‖(matSqrt (symmPart abar))⁻¹‖ is the square root of the normalizing spectral bound.

The lower companion, from the inner-ellipsoid normalization inner premise

theorem HCPolySupport.HighContrast.RowSupply.two_mul_gaugeInnerRadius_le_cubeScale {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 : ellipsoid abar (1 / (3 * √↑d)) ⊆ U) : 2 * (√(specBound (symmPart abar)⁻¹) * (1 / (3 * √↑d))) ≤ 3 ^ j

The lower companion of witnessCubeSide_le_two_mul_norm_inv_matSqrt. The printed inner ellipsoid, pulled to gauge coordinates, is the ball of radius α / (3 √d), and it sits inside the witness cube.

theorem HCPolySupport.HighContrast.RowSupply.two_mul_rho_le_cubeScale {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} {j : ℤ} {z : Vec d} {rho Rad : ℝ} (hU : U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j)) (hsandwich : HasBallSandwich (matImage (matSqrt (symmPart abar))⁻¹ U) rho Rad) : 2 * rho ≤ 3 ^ j

The sandwich companion. The frozen ball sandwich's inner ball also sits inside the witness cube, so the cube side is at least 2 ρ.

The two-sided statement and the law-free geometric factor

theorem HCPolySupport.HighContrast.RowSupply.witnessCubeScale_two_sided {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} {j : ℤ} {z : Vec d} {rho Rad : ℝ} (hU : U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j)) (hUsub : U ⊆ ellipsoid abar 1) (hinner : ellipsoid abar (1 / (3 * √↑d)) ⊆ U) (hsandwich : HasBallSandwich (matImage (matSqrt (symmPart abar))⁻¹ U) rho Rad) : 2 * (√(specBound (symmPart abar)⁻¹) * (1 / (3 * √↑d))) ≤ 3 ^ j ∧ 3 ^ j ≤ 2 * √(specBound (symmPart abar)⁻¹) ∧ rho ≤ √(specBound (symmPart abar)⁻¹)

The two-sided witness cube/ball geometry. Both premises of the frozen inner-ellipsoid normalization pin the witness generation between two multiples of the gauge scale α, and the ball sandwich's inner radius is below α.

noncomputable def HCPolySupport.HighContrast.RowSupply.witnessGeometricFactor (d : ℕ) (rho r : ℝ) : ℝ

The law-free geometric factor: a function of (d, ρ, r) only.

Equations

• HCPolySupport.HighContrast.RowSupply.witnessGeometricFactor d rho r = (rho / (3 * √↑d)) ^ (-r)

theorem HCPolySupport.HighContrast.RowSupply.rpow_three_neg_order_le_witnessGeometricFactor {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} {j : ℤ} {z : Vec d} {rho Rad r : ℝ} (hr : 0 ≤ r) (hU : U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j)) (hsandwich : HasBallSandwich (matImage (matSqrt (symmPart abar))⁻¹ U) rho Rad) : 3 ^ (-r * ↑j) ≤ witnessGeometricFactor d rho r

The geometric factor bound. The 3 ^ (−r j) factor of the λ-route is below the law-free Cgeo = (ρ / (3 √d)) ^ (−r), from binder surface.