OscillationDecayGap

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

The arbitrary-gap oscillation decay for a harmonic gradient

This module proves the estimate that the nested-recentring route of OscillationTelescope consumes once per birth scale: for a function u which is harmonic on the coarse concentric cube z + cu_{n+k} and for any constant vector c,

  || grad u - (grad u)_{z + cu_n} ||_{L2bar (z + cu_n)}
      <= C (d) 3^{-k} || grad u - c ||_{L2bar (z + cu_{n+k})} ,      k >= d + 2 .

The gain is the full factor 3^{-k} for an arbitrary gap k, obtained by one direct estimate from the coarse scale to the fine scale. The 3^{-k} above is honest precisely because k is large: the estimate is a single interior estimate on a Euclidean ball of radius comparable to 3^{n+k}, never an iterated one.

The argument

1. Geometry. For k >= d + 2 and y in the fine cube, the Euclidean ball B (y, 3^{n+k}/8) is contained in the coarse cube. This uses only the free (sup-norm) inclusion closedBall (y, rho) subset y + cu_m for rho < 3^m/2 together with the concentric containment criterion of OscillationCubeFamily; no sqrt d is paid, and the restriction k >= 2 suffices for this step alone. The genuine k >= d + 2 restriction enters through HarmonicGauge where the fine cube must sit inside the ball.
2. Interior estimate. d_i u - c_i is harmonic wherever u is (euclideanCoordLaplacian_euclideanCoordDeriv_eq_zero, plus the fact that a constant shift changes neither the Laplacian nor the derivative), so exists_interior_gradient_bound bounds every second derivative d_j d_i u (y) by C (d) / r times the average of |d_i u - c_i| over B (y, r), and that average is dominated by the coarse-cube integral.
3. Mean value inequality. Vec d carries the sup norm, and norm_clm_le_sum_basisVec_apply turns the d coordinate bounds of step 2 into a bound for the operator norm of fderiv (d_i u). The convex mean-value inequality on the cube then gives the pointwise oscillation bound with the sup-norm diameter 3^n.
4. Averaging. OscillationDecayAverage converts the resulting L^1 average into the normalized L^2 deviation (Cauchy--Schwarz), integrates the pointwise bound, and recentres at the volume average.

The scaling that makes the whole thing work is 3^n / (3^{n+k}/8) = 8 * 3^{-k}, i.e. the fine-cube diameter divided by the interior radius.

Contents

• euclideanBall_eighth_subset_openCubeAtScale_of_gap -- the geometric step.
• gap_constant_identity -- the one algebraic rearrangement of the constants.
• exists_gradient_oscillation_gap_decay -- the arbitrary-gap estimate.

Divergences from the printed proof

• A gap restriction k >= d + 2 is imposed. The manuscript's proof runs on Euclidean balls and supplies no cube transfer; on cubes a small gap genuinely fails.
• The estimate is stated for a concentric cube family, which is what the nested-recentring argument needs; the printed one-step display is on balls.

References

• ABK26, e.nablaw.oscillations (the eventual consumer).

The geometric step

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.euclideanBall_eighth_subset_openCubeAtScale_of_gap {d : ℕ} {z : HCPolySupport.Vec d} {n : ℤ} {k : ℕ} (hk : d + 2 ≤ k) {y : HCPolySupport.Vec d} (hy : y ∈ HCPolySupport.Book.Ch03.openCubeAtScale z n) : HCPolySupport.euclideanBall y (3 ^ (n + ↑k) / 8) ⊆ HCPolySupport.Book.Ch03.openCubeAtScale z (n + ↑k)

Interior balls of the fine cube stay inside the coarse cube.

For a triadic gap k >= 2 and a centre y in the fine cube z + cu_n, the Euclidean ball of radius 3^{n+k}/8 around y is contained in the coarse cube z + cu_{n+k}. Only the free sup-norm inclusion is used, so no dimensional factor is paid here.

The constant bookkeeping

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.gap_constant_identity (d : ℕ) {S P ω C avg : ℝ} (hS : S ≠ 0) (hω : ω ≠ 0) : ↑d * (C / (S / 8) * (S ^ d * avg / ((S / 8) ^ d * ω))) * P = 8 ^ (d + 1) * ↑d * C / ω * (P / S) * avg

The single algebraic rearrangement behind the arbitrary-gap constant: the interior radius S/8, the coarse-cube volume S^d and the ball volume (S/8)^d omega_d combine so that the fine-cube diameter P produces exactly the prefactor 8^{d+1} d C / omega_d times P / S.

The arbitrary-gap oscillation estimate

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.exists_gradient_oscillation_gap_decay {d : ℕ} (hd : 0 < d) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (u : HCPolySupport.Vec d → ℝ), ContDiff ℝ (↑⊤) u → ∀ (z : HCPolySupport.Vec d) (n : ℤ) (k : ℕ), d + 2 ≤ k → (∀ x ∈ HCPolySupport.Book.Ch03.openCubeAtScale z (n + ↑k), HCPolySupport.euclideanCoordLaplacian u x = 0) → ∀ (c : HCPolySupport.Vec d), √(HCPolySupport.Book.Ch01.meanSquareOscillationVecOn (HCPolySupport.Book.Ch03.openCubeAtScale z n) (HCPolySupport.euclideanGradient u)) ≤ C * 3 ^ (-↑k) * √(HCPolySupport.Book.Ch01.meanSquareDeviationVecOn (HCPolySupport.Book.Ch03.openCubeAtScale z (n + ↑k)) (HCPolySupport.euclideanGradient u) c)

The arbitrary-gap oscillation decay for a harmonic gradient.

If u is smooth and harmonic on the coarse concentric cube z + cu_{n+k} with gap k >= d + 2, then for every constant vector c the normalized mean-square gradient oscillation on the fine cube z + cu_n is at most C (d) 3^{-k} times the normalized L^2 deviation of grad u from c on the coarse cube. The constant depends only on the dimension.

The estimate is a direct one from the coarse scale to the fine scale. No adjacent-scale cube recurrence is formed anywhere, and none could be:.