High-contrast homogenization: Provider.PolynomialHomogenization.RootInterface.CertificateMonotone

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

Monotonicity of the printed-order certificate, and fold arithmetic

Two facts make the root's certificate instantiation possible.

• The printed-order quantitative certificate is upward closed in the scale and downward closed in the rate: its power tail is read above the scale with a negative exponent, so enlarging the scale and shrinking the rate both weaken it. Consequently the certificate produced at the raw quenched scale and the quenched row rate is available at every larger scale and every smaller positive rate — which is exactly what is needed to place it at the common affine scale the rate-bearing predicate forces, and at a rate inside the frozen order window κ ≤ (1 + g) / 4.

• Two eccentricity fold factors multiply into one: fold p * fold q ≤ fold (p+q). The certificate leg and the provider leg can therefore be carried by a single power.

Fold arithmetic

theorem HCPolySupport.HighContrast.RootInterface.max_one_mul_le {u v : ℝ} (_hu : 0 ≤ u) (hv : 0 ≤ v) : max 1 (u * v) ≤ max 1 u * max 1 v

max 1 is submultiplicative on nonnegative reals.

theorem HCPolySupport.HighContrast.RootInterface.max_one_rpow {u t : ℝ} (hu : 0 ≤ u) (ht : 0 ≤ t) : max 1 u ^ t = max 1 (u ^ t)

max 1 commutes with nonnegative real powers on nonnegative arguments.

theorem HCPolySupport.HighContrast.RootInterface.eccentricityFoldFactor_mul_le {d : ℕ} (abar : Mat d) {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) : RowSupply.eccentricityFoldFactor abar p * RowSupply.eccentricityFoldFactor abar q ≤ RowSupply.eccentricityFoldFactor abar (p + q)

Two fold factors multiply into one.

theorem HCPolySupport.HighContrast.RootInterface.max_one_mul_rpow_le_fold {d : ℕ} {abar : Mat d} {A t p : ℝ} (hA : 0 ≤ A) (ht : 0 ≤ t) (_hp : 0 ≤ p) : max 1 (A * witnessEccentricity (symmPart abar) ^ p) ^ t ≤ max 1 (A ^ t) * RowSupply.eccentricityFoldFactor abar (p * t)

A law-free amplitude times an eccentricity power, raised to a nonnegative power, is again of that shape.

The certificate is upward closed in the scale

theorem HCPolySupport.HighContrast.RootInterface.ScalarIdentityPowerTail.mono_scale {d : ℕ} {a : Book.Ch02.TriadicCoeffFamily d} {s amplitude kappa x y : ℝ} (h : ScalarIdentityPowerTail a s amplitude kappa x) (hamp : 0 ≤ amplitude) (hkappa : 0 < kappa) (hx : 0 < x) (hxy : x ≤ y) : ScalarIdentityPowerTail a s amplitude kappa y

The certificate is downward closed in the rate

theorem HCPolySupport.HighContrast.RootInterface.ScalarIdentityPowerTail.mono_rate {d : ℕ} {a : Book.Ch02.TriadicCoeffFamily d} {s amplitude kappa kappa' x : ℝ} (h : ScalarIdentityPowerTail a s amplitude kappa x) (hamp : 0 ≤ amplitude) (hx : 0 < x) (hkappa : kappa' ≤ kappa) : ScalarIdentityPowerTail a s amplitude kappa' x

theorem HCPolySupport.HighContrast.RootInterface.PrintOrderQuantitativeNormalizedReferenceCertificate.mono {d : ℕ} [NeZero d] {abar : Mat d} {g amplitude kappa kappa' x y : ℝ} {a : CoeffSpace d} (h : PrintOrderQuantitativeNormalizedReferenceCertificate abar g amplitude kappa x a) (hkappa' : 0 < kappa') (hkappa : kappa' ≤ kappa) (hxy : x ≤ y) : PrintOrderQuantitativeNormalizedReferenceCertificate abar g amplitude kappa' y a

The printed-order certificate is available at every larger scale and every smaller positive rate.

The physical block row is downward closed in the rate

theorem HCPolySupport.HighContrast.RootInterface.hasAllLaterPhysicalBlockRow_mono_rate {d : ℕ} {rho kappa kappa' C : ℝ} {Abar : BlockMat d} {S X : CoeffSpace d → ℝ} {a : CoeffSpace d} (h : Quenched.HasAllLaterPhysicalBlockRow rho kappa C Abar S X a) (hC : 0 ≤ C) (hX : 0 < X a) (hkappa : kappa' ≤ kappa) : Quenched.HasAllLaterPhysicalBlockRow rho kappa' C Abar S X a