High-contrast homogenization: Provider.Regularity.EffectiveScalePowerAbsorption

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

Effective-scale absorption of a power-law prefactor

This module isolates the route-independent real algebra for absorbing a positive multiplicative loss into the reference scale of a negative power.

noncomputable def HCPolySupport.HighContrast.powerLossEffectiveScale (A kappa x : ℝ) : ℝ

The scale enlargement that absorbs a prefactor A from a decay rate with positive exponent kappa.

Equations

• HCPolySupport.HighContrast.powerLossEffectiveScale A kappa x = A ^ kappa⁻¹ * x

theorem HCPolySupport.HighContrast.le_powerLossEffectiveScale {A kappa x : ℝ} (hA : 1 ≤ A) (hkappa : 0 < kappa) (hx : 0 ≤ x) : x ≤ powerLossEffectiveScale A kappa x

A prefactor at least one only enlarges a nonnegative base scale.

theorem HCPolySupport.HighContrast.prefactor_mul_rpow_ratio_eq_rpow_effectiveScale {A kappa x r : ℝ} (hA : 0 < A) (hkappa : 0 < kappa) (hx : 0 < x) (hr : 0 < r) : A * (r / x) ^ (-kappa) = (r / powerLossEffectiveScale A kappa x) ^ (-kappa)

Absorbing A into the effective scale is an exact identity for a negative power-law profile.