UpperSaturatedBlockProfile

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

Saturated upper-profile budgets after the triadic grid maximum

This module performs deterministic arithmetic on a proposed per-descendant saturated amplitude. If the ordinary lane on the strict descendant row m - 1 - k has scale

C * cstar⁻¹ * min 1 (gamma * (k + 1)) * 3^(gamma * (k + 1)),

then the Gamma_1 grid price contributes gridNetConst d 1 * (k + 1). Their product is exactly upperSaturatedProfile with a head whose grid multiplier is dimension-only and whose remaining dependence is C * cstar⁻¹ * 3^gamma. On gamma <= 1, the last factor is at most three.

The row index k corresponds to literal source depth r = k + 1, so the source strict-tail weight is geometricWeight s q (k + 1). The convenient k-weighted profile sum is a deliberate enlargement: it drops the additional one-step factor 3^(-s*q) but retains the source normalizer c_{s,q}. The depth-zero/root term r = 0 is separate and is not bounded here.

The analytic per-descendant estimate and the root estimate are not proved here.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.upperSaturatedPerCubeAmplitude (C cstar gamma : ℝ) (k : ℕ) : ℝ

The algebraic saturated scale assigned to strict-descendant row k. This definition does not assert an analytic estimate for that row.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.upperSaturatedPerCubeAmplitude C cstar gamma k = C * cstar⁻¹ * min 1 (gamma * (↑k + 1)) * 3 ^ (gamma * (↑k + 1))

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.upperSaturatedGridProfileConst (d : ℕ) (C cstar gamma : ℝ) : ℝ

The algebraic head constant after factoring the Gamma_1 grid price.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.upperSaturatedGridProfileConst d C cstar gamma = Algsuperdiff.Section3.Provider.CoarseEllipticity.gridNetConst d 1 * C * cstar⁻¹ * 3 ^ gamma

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.upperSaturatedGridProfileBound (d : ℕ) (C cstar : ℝ) : ℝ

An enlargement of the exact head on gamma <= 1; it retains the explicit C * cstar⁻¹ dependence and only its grid multiplier is dimension-only.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.upperSaturatedGridProfileBound d C cstar = 3 * Algsuperdiff.Section3.Provider.CoarseEllipticity.gridNetConst d 1 * C * cstar⁻¹

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gamma_le_min_one_mul_natCast_succ {gamma : ℝ} (hgamma : 0 ≤ gamma) (hgamma1 : gamma ≤ 1) (k : ℕ) : gamma ≤ min 1 (gamma * (↑k + 1))

A plain factor gamma fits inside the saturated depth factor on 0 <= gamma <= 1.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.plainGammaPerCubeAmplitude_le_upperSaturated {C cstar gamma : ℝ} (hC : 0 ≤ C) (hcstar : 0 ≤ cstar⁻¹) (hgamma : 0 ≤ gamma) (hgamma1 : gamma ≤ 1) (k : ℕ) : C * cstar⁻¹ * gamma * 3 ^ (gamma * (↑k + 1)) ≤ upperSaturatedPerCubeAmplitude C cstar gamma k

Consequently, an ordinary per-cube term carrying a bare gamma is dominated by the saturated target amplitude.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperSaturatedPerCubeAmplitude_nonneg {C cstar gamma : ℝ} (hC : 0 ≤ C) (hcstar : 0 ≤ cstar⁻¹) (hgamma : 0 ≤ gamma) (k : ℕ) : 0 ≤ upperSaturatedPerCubeAmplitude C cstar gamma k

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperSaturatedPerCubeAmplitude_pos {C cstar gamma : ℝ} (hC : 0 < C) (hcstar : 0 < cstar) (hgamma : 0 < gamma) (k : ℕ) : 0 < upperSaturatedPerCubeAmplitude C cstar gamma k

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperSaturatedGridProfileConst_nonneg (d : ℕ) {C cstar gamma : ℝ} (hC : 0 ≤ C) (hcstar : 0 ≤ cstar⁻¹) : 0 ≤ upperSaturatedGridProfileConst d C cstar gamma

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gridNetConst_mul_upperSaturatedPerCubeAmplitude_eq (d : ℕ) (C cstar gamma : ℝ) (k : ℕ) : gridNetConst d 1 * (↑k + 1) ^ 1⁻¹ * upperSaturatedPerCubeAmplitude C cstar gamma k = upperSaturatedProfile (upperSaturatedGridProfileConst d C cstar gamma) gamma k

Exact algebraic identity for the grid-priced row. This indexes the enlarged profile by k; literal source depth for the row is k + 1.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperSaturatedGridProfileConst_le_bound (d : ℕ) {C cstar gamma : ℝ} (hC : 0 ≤ C) (hcstar : 0 ≤ cstar⁻¹) (hgamma1 : gamma ≤ 1) : upperSaturatedGridProfileConst d C cstar gamma ≤ upperSaturatedGridProfileBound d C cstar

On the standing small-gamma range, the exact grid-profile head is at most the enlargement retaining C * cstar⁻¹; only the grid multiplier is dimension-only.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.geometricWeight_succ_eq_decay_mul (s q : ℝ) (k : ℕ) : HCPolySupport.Book.Ch02.geometricWeight s q (k + 1) = 3 ^ (-s * q) * HCPolySupport.Book.Ch02.geometricWeight s q k

Advancing literal source depth by one extracts exactly one factor 3^(-s*q) from the geometric weight. The normalizer c_{s,q} remains on both sides.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.geometricWeight_succ_le_self {s q : ℝ} (hsq : 0 ≤ s * q) (k : ℕ) : HCPolySupport.Book.Ch02.geometricWeight s q (k + 1) ≤ HCPolySupport.Book.Ch02.geometricWeight s q k

On 0 <= s*q, the literal strict-tail weight at source depth k+1 is at most the enlarged budget weight at index k.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperSaturatedGridProfile_enlarged_aggregate_le (d : ℕ) {C cstar gamma s q : ℝ} (hC : 0 ≤ C) (hcstar : 0 ≤ cstar⁻¹) (hgamma : 0 ≤ gamma) (hgamma1 : gamma ≤ 1) (hs : 0 < s) (hs1 : s ≤ 1) (hq1 : 1 ≤ q) (hq2 : q ≤ 2) (hgap : 0 < 2 * s - gamma) : (∑' (k : ℕ), HCPolySupport.Book.Ch02.geometricWeight s q k * (gridNetConst d 1 * (↑k + 1) ^ 1⁻¹ * upperSaturatedPerCubeAmplitude C cstar gamma k) ^ (q / 2)) ^ (2 / q) ≤ 3072 * upperSaturatedGridProfileBound d C cstar * s * gamma * (2 * s - gamma)⁻¹ ^ 3

The normalized 1 <= q <= 2 aggregate of the k-weighted enlarged strict-tail budget has the cubic pole. This theorem is about the displayed enlargement, not the literal source-depth carrier.