CubeAmplitude

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

The amplitude of the localized Hölder estimate

The Campanato characterisation delivers a C^{0,beta} seminorm bound whose constant is the one produced by the clipped-window family; the localized estimate asks instead for the normalized seminorm 3 ^ (beta m) [·]_{C^{0,beta}} against the seed ‖u - (u)_{□_m}‖_{L²} and the force leg sigma^{-1} 3 ^ (3m/2) [g]_{C^{0,1/2}}. This file performs that rearrangement once, as an inequality between real numbers.

Three things happen. The weight 3 ^ (beta m) cancels the factor 3 ^ ((1 - beta) m) carried by the family's constant against the normalization 3 ^ (-m) of the seed, leaving the seed and the force leg unweighted. The residual scale factor 3 ^ ((1 - beta)(X + 1)/2) is absorbed into 3 ^ ((1 - alpha) 2X) for every exponent alpha below beta, at the fixed price 3. And the two weights of the bracket are replaced by their maximum.

Main results

• rpow_mul_campanatoGridConstant_le — the rearrangement.

theorem Algsuperdiff.Section4.Provider.Holder.rpow_mul_campanatoGridConstant_le {alpha beta Cosc Cdata S Kg sigma G Ud P2 : ℝ} {m : ℤ} {Xn : ℕ} (halpha0 : 0 < alpha) (hab : alpha ≤ beta) (hbeta1 : beta ≤ 1) (hCosc : 0 ≤ Cosc) (hCdata : 0 ≤ Cdata) (hS : 0 ≤ S) (hKg : 0 ≤ Kg) (hsigma : 0 < sigma) (hP2 : 0 ≤ P2) (hG : 0 ≤ G) (hGU : G ≤ Ud) (hUd : 0 ≤ Ud) : Real.rpow 3 (beta * ↑m) * (G * campanatoGridConstant beta m Xn Cosc (3 ^ (-m) * (P2 * S) + Cdata * (sigma⁻¹ * Real.rpow 3 (↑m / 2) * Kg))) ≤ 6 * Ud * Cosc * max P2 Cdata * Real.rpow 3 ((1 - alpha) * ↑(2 * Xn)) * (S + sigma⁻¹ * Real.rpow 3 (3 * ↑m / 2) * Kg)

The scalar rearrangement of the estimate.