SmallGammaRpow

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Smallness of the amplitude γ^{1/2}|log γ|^q

The accuracy windows of the percolation estimates have a lower endpoint of the form

  C γ^{1/2} |log γ|^q

with a real exponent q, and are useful only when that endpoint lies below the fixed upper endpoints the estimates impose. This file supplies the elementary fact that makes those windows nonempty: for a fixed multiplier and a fixed exponent the amplitude falls below any prescribed positive bound once the disorder parameter is small enough.

The proof is quantitative. For 0 < r and 0 < γ ≤ 1 the logarithm obeys

  |log γ| ≤ r⁻¹ γ^{-r} ,

which is log x ≤ x - 1 read at x = γ^{-r}. Taking the q-th power with r = (4(q+1))⁻¹ and multiplying by γ^{1/2} gives

  γ^{1/2} |log γ|^q ≤ (4(q+1))^q γ^{1/4} ,

so the threshold can be taken to be a fourth power.

Main results

• abs_log_le_inv_mul_rpow_neg — the logarithm against a small negative power.
• sqrt_mul_abs_log_rpow_le_rpow_quarter — the amplitude against γ^{1/4}.
• exists_sqrt_mul_abs_log_rpow_le — any multiple of the amplitude is below any prescribed positive bound once γ is below an explicit threshold.

theorem Algsuperdiff.Section5.Support.abs_log_le_inv_mul_rpow_neg {gamma r : ℝ} (hgamma : 0 < gamma) (hgamma1 : gamma ≤ 1) (hr : 0 < r) : |Real.log gamma| ≤ r⁻¹ * gamma.rpow (-r)

The logarithm is dominated by any small negative power. For 0 < γ ≤ 1 and 0 < r,

  |log γ| ≤ r⁻¹ γ^{-r} .

This is the inequality log x ≤ x - 1 read at x = γ^{-r}.

theorem Algsuperdiff.Section5.Support.sqrt_mul_abs_log_rpow_le_rpow_quarter {q : ℝ} (hq : 0 ≤ q) {gamma : ℝ} (hgamma : 0 < gamma) (hgamma1 : gamma ≤ 1) : √gamma * |Real.log gamma|.rpow q ≤ (4 * (q + 1)).rpow q * gamma.rpow (1 / 4)

The amplitude γ^{1/2}|log γ|^q is a bounded multiple of γ^{1/4}. For every real exponent q ≥ 0 and every 0 < γ ≤ 1,

  γ^{1/2} |log γ|^q ≤ (4(q+1))^q γ^{1/4} .

theorem Algsuperdiff.Section5.Support.exists_sqrt_mul_abs_log_rpow_le {K q eps : ℝ} (hK : 0 ≤ K) (hq : 0 ≤ q) (heps : 0 < eps) : ∃ (gamma0 : ℝ), 0 < gamma0 ∧ ∀ (gamma : ℝ), 0 < gamma → gamma ≤ gamma0 → K * (√gamma * |Real.log gamma|.rpow q) ≤ eps

Any multiple of the amplitude γ^{1/2}|log γ|^q is uniformly small for small disorder. For every nonnegative multiplier K, every real exponent q ≥ 0 and every prescribed positive bound eps there is a threshold below which

  K γ^{1/2}|log γ|^q ≤ eps .

The threshold is explicit: with C = (4(q+1))^q and B = K C + 1 it is min 1 ((eps / B)^4), because γ^{1/2}|log γ|^q ≤ C γ^{1/4}.