HomLiftTelescope

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

Theorem B, §4.5, Step 3c: the telescoping Hölder lifting

What this module proves

The intended mechanism of the Step-3c bridge is the following.

"Obviously W^{-s,∞} for the gradient ∇u implies L^∞ for u. W^{-s,∞} for the gradient is like C^{0,1-s} for the function u. Which is stronger than L^∞."

The classical proof of that implication is a telescoping argument over the triadic scales. Write W_n for the regularization of w at scale 3^n (mollification, or the running cube average). A negative-order bound on ∇w of order -s at the (∞,∞) indices is exactly the pair of scale-by-scale estimates

  (L)  |W_n(x) - W_n(y)| ≤ A · 3^{-ns} · |x - y|      (the scale-n gradient bound)
  (I)  |W_n(x) - W_{n-1}(x)| ≤ A · 3^{n(1-s)}         (the scale-n increment)

and (L) + (I) + W_n → w give the Hölder bound [w]_{C^{0,1-s}} ≤ C A with an absolute constant. This module proves exactly that implication, in the Hölder carrier Support.HolderSeminormBoundOn.

The split is deliberate: (L) and (I) are the only places where the negative-order gradient bound enters, and they are the classical mollifier estimates. Everything downstream of them — the scale cut, the geometric series, the modulus — is proved here unconditionally.

The carrier pin, and what is NOT discharged here

The manuscript never defines ‖·‖_{W_hat^{-s,∞}(□_m)}: only the order -1 dual seminorms and the negative-order Besov seminorm [·]_{B^{-s}_{p,q}} (the negative Besov seminorm definition) are defined. Under the Besov--Sobolev dictionary W^{-s,p} ≃ B^{-s}_{p,p} the Step-3 object is the (∞,∞) member of that family,

  3^{-ms} ‖F‖_{W_hat^{-s,∞}(□_m)} ≍ sup_{n ≤ m} 3^{-(m-n)s} max_{z} |(F)_{z+□_n}|,

which is exactly the multiscale negative norm. The (∞,∞) inner index — the maximum over the subcubes at each scale, not an ℓ^p average — is essential: a bound on the ℓ^2-averaged variant B^{-s}_{2,∞} (CoarseGraining's scaleNormalizedNegativeBesovVectorNorm Q s.infinity) does not imply a pointwise Hölder bound, since a gradient concentrated on one subcube at depth j has its ℓ^2 average smaller by 3^{-jd/2}.

(L) and (I) are the two scale-by-scale estimates that the multiscale negative norm supplies for the mollifications W_n of w. They are caller-supplied obligations: this module does not derive them. Producing them from the negative Besov bound is the classical mollifier calculus (∇(w ⋆ φ_r) = (∇w) ⋆ φ_r together with the kernel's negative-norm pairing), which is not built in this tree.

Main results

• holderSeminormBoundOn_of_regularization — (L) at constant AL and the approximation bound |W_n - w| ≤ AA · 3^{n(1-s)} give [w]_{C^{0,1-s}(U)} ≤ 2·AA + 2·AL.
• regularizationApprox_of_increments — (I) plus convergence gives the approximation bound at constant A · liftGeomFactor s.
• holderSeminormBoundOn_of_increments — the composition, at the absolute constant 8 · A for 0 < s ≤ 1/2.

The s-dependence

Every constant produced here is 2·liftGeomFactor s + 2 ≤ 8 on the whole range 0 < s ≤ 1/2; see HomLiftScaleArith. In particular the §4.5 pin s = |log γ|⁻¹ and Step 3's own s < 1/10 sit deep inside the range where the constant is absolute, and no (1-s)^{-1} factor is incurred.

References

• ABK26, Theorem B Step 3.
• ABK26 (the W^{s,∞} ↔ C^{0,s} identification).

1. The lifting from the two scale estimates

theorem Algsuperdiff.Section4.Provider.Homogenization.holderSeminormBoundOn_of_regularization {d : ℕ} {U : Set (HCPolySupport.Vec d)} {w : HCPolySupport.Vec d → ℝ} {W : ℤ → HCPolySupport.Vec d → ℝ} {m : ℤ} {s AL AA : ℝ} (hs0 : 0 < s) (hs2 : s ≤ 1 / 2) (hAL : 0 ≤ AL) (hAA : 0 ≤ AA) (hdiam : ∀ x ∈ U, ∀ y ∈ U, ‖x - y‖ ≤ 3 ^ ↑m) (hLip : ∀ n ≤ m, ∀ x ∈ U, ∀ y ∈ U, |W n x - W n y| ≤ AL * 3 ^ (-(↑n * s)) * ‖x - y‖) (hApp : ∀ n ≤ m, ∀ x ∈ U, |W n x - w x| ≤ AA * 3 ^ (↑n * (1 - s))) : Support.HolderSeminormBoundOn U (1 - s) (2 * AA + 2 * AL) w

The telescoping Hölder lifting.

Let w: Vec d → ℝ and let W: ℤ → Vec d → ℝ be a family of regularizations indexed by the triadic scales n ≤ m. Assume, on a set U of diameter at most 3^m:

• hLip — the scale-n Lipschitz bound |W_n(x) - W_n(y)| ≤ AL 3^{-ns}|x-y|;
• hApp — the scale-n approximation bound |W_n(x) - w(x)| ≤ AA 3^{n(1-s)}.

Then w is Hölder continuous of exponent 1 - s on U, with constant 2·AA + 2·AL.

This is the (∞,∞)-index lifting: hLip and hApp are precisely what a negative-order bound of order -s on ∇w supplies at scale 3^n. The exponent 1 - s is the Hölder exponent asserted in.

2. The approximation bound from the increments

theorem Algsuperdiff.Section4.Provider.Homogenization.regularizationApprox_of_increments {d : ℕ} {U : Set (HCPolySupport.Vec d)} {w : HCPolySupport.Vec d → ℝ} {W : ℤ → HCPolySupport.Vec d → ℝ} {m : ℤ} {s A : ℝ} (hs1 : s < 1) (hA : 0 ≤ A) (hInc : ∀ n ≤ m, ∀ x ∈ U, |W n x - W (n - 1) x| ≤ A * 3 ^ (↑n * (1 - s))) (hLim : ∀ x ∈ U, ∀ n ≤ m, Filter.Tendsto (fun (k : ℕ) => W (n - ↑k) x) Filter.atTop (nhds (w x))) (n : ℤ) : n ≤ m → ∀ x ∈ U, |W n x - w x| ≤ A * liftGeomFactor s * 3 ^ (↑n * (1 - s))

The telescoping series. If the increments of the regularization family obey |W_n(x) - W_{n-1}(x)| ≤ A · 3^{n(1-s)} and W_{n-k}(x) → w(x) as k → ∞, then the approximation bound holds at the constant A · liftGeomFactor s.

liftGeomFactor s = (1 - 3^{-(1-s)})⁻¹ is the sum of the geometric series; it is at most 3 on s ≤ 1/2 (liftGeomFactor_le_three).

3. The composed lifting

theorem Algsuperdiff.Section4.Provider.Homogenization.holderSeminormBoundOn_of_increments {d : ℕ} {U : Set (HCPolySupport.Vec d)} {w : HCPolySupport.Vec d → ℝ} {W : ℤ → HCPolySupport.Vec d → ℝ} {m : ℤ} {s A : ℝ} (hs0 : 0 < s) (hs2 : s ≤ 1 / 2) (hA : 0 ≤ A) (hdiam : ∀ x ∈ U, ∀ y ∈ U, ‖x - y‖ ≤ 3 ^ ↑m) (hLip : ∀ n ≤ m, ∀ x ∈ U, ∀ y ∈ U, |W n x - W n y| ≤ A * 3 ^ (-(↑n * s)) * ‖x - y‖) (hInc : ∀ n ≤ m, ∀ x ∈ U, |W n x - W (n - 1) x| ≤ A * 3 ^ (↑n * (1 - s))) (hLim : ∀ x ∈ U, ∀ n ≤ m, Filter.Tendsto (fun (k : ℕ) => W (n - ↑k) x) Filter.atTop (nhds (w x))) : Support.HolderSeminormBoundOn U (1 - s) (8 * A) w

The lifting from the two primitive scale estimates. The Lipschitz bound (L) and the increment bound (I), both at constant A, give the Hölder bound at the absolute constant 8 A for 0 < s ≤ 1/2.