UpperPolyProfile

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

The polynomial finite-q upper profile

This module isolates the deterministic depth arithmetic in the upper half of ABK26. After the grid maximum, the ordinary lane has the profile

A * (n + 1)^2 * 3^(gamma n).

For every finite exponent q >= 2, its defining weighted ell^(q/2) aggregate is bounded by a dimension-free multiple of

A * s * (2s - gamma)^(-3).

The proof keeps the ell^(q/2) aggregate intact. In particular it does not use the false uniform estimate gridSumConst s q <= C * s at large q. Instead, half of the collar pays the quadratic polynomial, after which the already-proved exact geometric-profile estimate applies with gap (2s - gamma) / 2.

This is only model-free profile arithmetic. It does not manufacture the per-depth random variables or a joint Gamma_1 certificate for their ell^(q/2) aggregate.

Source and provenance

• ABK26, especially the ordinary profile and its cubic pole.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.upperPolyProfile (A gamma : ℝ) (n : ℕ) : ℝ

The quadratic-times-geometric profile produced by the ordinary upper per-depth estimate after the grid maximum.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.upperPolyProfile A gamma n = A * (↑n + 1) ^ 2 * 3 ^ (gamma * ↑n)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperPolyProfile_nonneg {A : ℝ} (hA : 0 ≤ A) (gamma : ℝ) (n : ℕ) : 0 ≤ upperPolyProfile A gamma n

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.natCast_succ_sq_le_inv_sq_mul_three_rpow {rho : ℝ} (hrho : 0 < rho) (hrho2 : rho ≤ 2) (n : ℕ) : (↑n + 1) ^ 2 ≤ 96 * rho⁻¹ ^ 2 * 3 ^ (rho / 2 * ↑n)

Half of a positive collar absorbs the quadratic depth factor. The constant is deliberately coarse and dimension-free.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperPolyProfile_le_finiteQGeometricProfile {A rho : ℝ} (hA : 0 ≤ A) (hrho : 0 < rho) (hrho2 : rho ≤ 2) (gamma : ℝ) (n : ℕ) : upperPolyProfile A gamma n ≤ finiteQGeometricProfile (96 * A * rho⁻¹ ^ 2) (gamma + rho / 2) n

The quadratic upper profile is pointwise dominated by a pure geometric profile after spending half of the positive gap.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperPolyProfile_aggregate_le_of_two_le {A gamma s q : ℝ} (hA : 0 ≤ A) (hgamma : 0 ≤ gamma) (hs : 0 < s) (hs1 : s ≤ 1) (hq : 2 ≤ q) (hgap : 0 < 2 * s - gamma) : (∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s q n * upperPolyProfile A gamma n ^ (q / 2)) ^ (2 / q) ≤ 384 * A * s * (2 * s - gamma)⁻¹ ^ 3

The source's quadratic ordinary profile has the printed cubic pole at every finite exponent q >= 2.