High-contrast homogenization:

Provider.PolynomialHomogenization.RootInterface.ScaleFactorArithmetic

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

The root-interface length factor

The root's exported homogenization length is the quenched length multiplied by one common positive factor. Two independent sources contribute to that factor:

• the certificate factor, paid once when the printed-order certificate is read at the common affine scale rather than at the raw quenched scale;
• the provider factor, paid once by the Dirichlet provider, which is free to choose a law-free g-dependent amplitude together with an eccentricity power.

Both are of the same shape — a law-free real at least one, times a power of the homogenized witness eccentricity — so the whole factor is again of that shape. This module records the arithmetic of such a factor: it is at least one, it is polynomial in the printed length base, and it transfers every clause of the frozen statement exactly as the single fold factor of HCPoly.Provider.PolynomialHomogenization.Root.Dirichlet.EccentricityFoldFactor does.

A law-free amplitude is polynomial in the printed base

theorem HCPolySupport.HighContrast.RootInterface.le_rpow_logb_two {base L : ℝ} (hbase : 2 ≤ base) (hL : 1 ≤ L) : L ≤ base ^ Real.logb 2 L

A real at least one is below any base at least two raised to its binary logarithm. This converts a law-free amplitude into a polynomial-length exponent.

theorem HCPolySupport.HighContrast.RootInterface.logb_two_nonneg {L : ℝ} (hL : 1 ≤ L) : 0 ≤ Real.logb 2 L

The composite root factor

noncomputable def HCPolySupport.HighContrast.RootInterface.rootLengthFactor {d : ℕ} (abar : Mat d) (Lcert pCert Lprov pProv : ℝ) : ℝ

The root's length factor: a law-free amplitude times an eccentricity power, paid once by the certificate and once by the Dirichlet provider.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.RootInterface.one_le_rootLengthFactor {d : ℕ} {abar : Mat d} {Lcert pCert Lprov pProv : ℝ} (hLcert : 1 ≤ Lcert) (hLprov : 1 ≤ Lprov) : 1 ≤ rootLengthFactor abar Lcert pCert Lprov pProv

theorem HCPolySupport.HighContrast.RootInterface.rootLengthFactor_pos {d : ℕ} {abar : Mat d} {Lcert pCert Lprov pProv : ℝ} (hLcert : 1 ≤ Lcert) (hLprov : 1 ≤ Lprov) : 0 < rootLengthFactor abar Lcert pCert Lprov pProv

noncomputable def HCPolySupport.HighContrast.RootInterface.rootLengthExponent (Lcert pCert Lprov pProv : ℝ) : ℝ

The composite exponent the polynomial-length clause closes at.

Equations

• HCPolySupport.HighContrast.RootInterface.rootLengthExponent Lcert pCert Lprov pProv = Real.logb 2 Lcert + 5 * pCert + (Real.logb 2 Lprov + 5 * pProv)

theorem HCPolySupport.HighContrast.RootInterface.rootLengthExponent_nonneg {Lcert pCert Lprov pProv : ℝ} (hLcert : 1 ≤ Lcert) (hpCert : 0 ≤ pCert) (hLprov : 1 ≤ Lprov) (hpProv : 0 ≤ pProv) : 0 ≤ rootLengthExponent Lcert pCert Lprov pProv

theorem HCPolySupport.HighContrast.RootInterface.rootLengthFactor_le_rpow {d : ℕ} {abar : Mat d} {base Lcert pCert Lprov pProv : ℝ} (hbase : 2 ≤ base) (hLcert : 1 ≤ Lcert) (hpCert : 0 ≤ pCert) (hLprov : 1 ≤ Lprov) (hpProv : 0 ≤ pProv) (hecc : witnessEccentricity (symmPart abar) ≤ base ^ 5) : rootLengthFactor abar Lcert pCert Lprov pProv ≤ base ^ rootLengthExponent Lcert pCert Lprov pProv

The root factor is polynomial in the printed length base. The law-free halves are absorbed by their binary logarithms and the eccentricity halves by the law-level eccentricity bound.

Generic clause transfers at a common factor

theorem HCPolySupport.HighContrast.RootInterface.le_mul_factor {x F : ℝ} (hx : 0 ≤ x) (hF : 1 ≤ F) : x ≤ x * F

theorem HCPolySupport.HighContrast.RootInterface.one_le_mul_factor {x F : ℝ} (hx : 1 ≤ x) (hF : 1 ≤ F) : 1 ≤ x * F

theorem HCPolySupport.HighContrast.RootInterface.measurable_mul_factor {Omega : Type u_1} [MeasurableSpace Omega] {X : Omega → ℝ} {F : ℝ} (hX : Measurable X) : Measurable fun (a : Omega) => X a * F