RateOptimization

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

Balancing an averaged term against a Hölder term

The interior pointwise estimate bounds a value by an L² average on a ball of radius rho plus a Hölder modulus of order rho ^ alpha. When the L² term already carries an exponential factor exp (-(kappa * s)), choosing rho = R * exp (-(kappa * s) / (alpha + d / 2)) balances the two and produces the reduced exponential rate kappa * alpha / (alpha + d / 2).

The cap R on the admissible radii is a parameter, so the statement is scale free: it may be as small as the consumer's ball allows, and the constant is simply the two-term bound evaluated at R. Because the balancing radius is R times a factor at most one, it is always admissible, so there is no case distinction and no lost constant factor.

Main results

• DivergenceFormProcess.Decay.sqrt_exp_eq
• DivergenceFormProcess.Decay.le_mul_exp_of_two_term_bound

theorem DivergenceFormProcess.Decay.sqrt_exp_eq (y : ℝ) : √(Real.exp y) = Real.exp (y / 2)

The square root of an exponential.

theorem DivergenceFormProcess.Decay.le_mul_exp_of_two_term_bound {d : ℕ} {A B kappa alpha s R F : ℝ} (hR : 0 < R) (halpha0 : 0 < alpha) (hkappa : 0 ≤ kappa) (hs : 0 ≤ s) (hF : ∀ (rho : ℝ), 0 < rho → rho ≤ R → F ≤ A * Real.exp (-(kappa * s)) / √(rho ^ d) + B * rho ^ alpha) : F ≤ (A / √(R ^ d) + B * R ^ alpha) * Real.exp (-(kappa * alpha / (alpha + ↑d / 2) * s))

Balancing the averaged term against the Hölder term. A bound valid for every radius up to R yields an exponential bound at the reduced rate, with the constant read off at the radius R.