High-contrast homogenization: Provider.PolynomialHomogenization.ConvexHardyRowScales

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

Common chain lengths for Whitney rows

When the top triadic scale is no larger than the sandwich radius, every finer row has a unique compatible dyadic chain length. Distinct triadic rows have distinct lengths because consecutive triadic scales differ by more than the factor allowed in the initial chain radius.

theorem HCPolySupport.HighContrast.exists_injective_convexHardyRowChainLengths {rho : ℝ} (hrho : 0 < rho) {n : ℤ} (hnrho : 3 ^ n ≤ rho) : ∃ (N : { a : ℤ // a ≤ n } → ℕ), (∀ (a : { a : ℤ // a ≤ n }), 3 ^ ↑a ≤ convexHardyBallChainRadius rho (N a) 0 ∧ convexHardyBallChainRadius rho (N a) 0 < 2 * 3 ^ ↑a) ∧ Function.Injective N

All rows below a triadic top scale admit compatible initial dyadic radii, and their chain lengths can be selected injectively.