OscillationTelescope

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

The nested-recentring accumulation behind e.nablaw.oscillations

ABK26 states e.nablaw.oscillations on the triadic cubes z + cu_n subset z + cu_{m-h}, and proves it by writing down a one-step estimate on the concentric Euclidean balls B_r(z) subset B_{3r}(z) followed by the words "and iterating this yields".

So the adjacent-cube recurrence that a naive cube reading of the manuscript would iterate simply does not hold.

Concretely, on the nested triadic cubes U_j := z + cu_{n+j}, 0 <= j <= N, one writes the fine-scale field as a finite sum of harmonic increments born at each scale,

  g = u_N + sum_{j < N} (u_j - u_{j+1}) + (g - u_0)   on U_0 ,

and estimates the oscillation on U_0 of each summand directly from its own birth scale, never through a chain of adjacent-scale contractions. Each increment born at scale j is therefore hit once by the arbitrary-gap factor 3^{-j} and once by the birth-scale forcing size 3^{n+j}; the two cancel, so the forcing accumulates linearly in N while the coarse term keeps the full geometric factor 3^{-N}. That is exactly the shape of the printed display, obtained without the false adjacent-cube contraction.

Contents

• zpow_neg_natCast_mul_zpow_add -- the single cancellation 3^{-j} * 3^{n+j} = 3^n on which the whole mechanism rests.
• sum_zpow_neg_mul_le_nsmul_of_triadic_bound -- the accumulation sum_{j < N} A * 3^{-j} * (E j + rho * E (j+1)) <= N * A (1 + 3 rho) * 3^n * c under the birth-scale bound E j <= c * 3^{n+j}.
• le_zpow_mul_add_nsmul_of_nested_decomposition -- the display-shaped assembly Phi 0 <= A * 3^{-N} * Phi N + (A (1 + 3 rho) N + A + 2) * 3^n * c.

References

• ABK26, e.nablaw.oscillations, statement and the ball one-step estimate and the word "iterating".

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.zpow_neg_natCast_mul_zpow_add (n : ℤ) (j : ℕ) : 3 ^ (-↑j) * 3 ^ (n + ↑j) = 3 ^ n

3^{-j} * 3^{n+j} = 3^n: the arbitrary-gap harmonic factor for an increment born at scale j exactly cancels the birth-scale size of the forcing. This one cancellation is the reason the forcing in e.nablaw.oscillations accumulates linearly rather than geometrically.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.sum_zpow_neg_mul_le_nsmul_of_triadic_bound {E : ℕ → ℝ} {n : ℤ} {N : ℕ} {A rho c : ℝ} (hA : 0 ≤ A) (hrho : 0 ≤ rho) (hE : ∀ j ≤ N, E j ≤ c * 3 ^ (n + ↑j)) : ∑ j ∈ Finset.range N, A * 3 ^ (-↑j) * (E j + rho * E (j + 1)) ≤ ↑N * (A * (1 + 3 * rho) * (3 ^ n * c))

The birth-scale accumulation.

If the per-scale error E j obeys the birth-scale bound E j <= c * 3^{n+j} for every j <= N, then weighting the scale-j term by the arbitrary-gap factor 3^{-j} makes every summand equal in size, so the sum grows only linearly:

  sum_{j < N} A * 3^{-j} * (E j + rho * E (j+1))
    <= N * (A * (1 + 3 rho) * (3^n * c)) .

The rho * E (j+1) term carries the volume ratio incurred when the harmonic approximation born at scale j+1 is restricted to the cube of scale j.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.le_zpow_mul_add_nsmul_of_nested_decomposition {Phi E S : ℕ → ℝ} {T : ℝ} {n : ℤ} {N : ℕ} {A rho c : ℝ} (hA : 0 ≤ A) (hrho : 0 ≤ rho) (hE : ∀ j ≤ N, E j ≤ c * 3 ^ (n + ↑j)) (hsplit : Phi 0 ≤ T + ∑ j ∈ Finset.range N, S j + 2 * E 0) (hT : T ≤ A * 3 ^ (-↑N) * (Phi N + E N)) (hS : ∀ j < N, S j ≤ A * 3 ^ (-↑j) * (E j + rho * E (j + 1))) : Phi 0 ≤ A * 3 ^ (-↑N) * Phi N + (A * (1 + 3 * rho) * ↑N + A + 2) * (3 ^ n * c)

The display-shaped assembly of the nested-recentring route.

Suppose the fine-scale oscillation Phi 0 has a decomposition into a coarse harmonic term T, finitely many harmonic increments S j born at the intermediate scales j < N, and a fine-scale approximation defect (hsplit); suppose the coarse term obeys the arbitrary-gap estimate from scale N directly to scale 0 (hT); suppose each increment obeys the arbitrary-gap estimate from its own birth scale j directly to scale 0 (hS); and suppose the approximation errors obey the birth-scale bound E j <= c * 3^{n+j} (hE). Then

  Phi 0 <= A * 3^{-N} * Phi N + (A (1 + 3 rho) N + A + 2) * (3^n * c) ,

which is the shape of e.nablaw.oscillations with N = m - h - n: the full geometric gain 3^{-(m-h-n)} on the coarse oscillation and a forcing term linear in m - h - n carrying the single factor 3^n.

Every hypothesis is an input to be discharged elsewhere; see the module disclosure. Nothing here asserts that any of them holds, and this statement claims no source node.