DiscreteScales

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

Triadic radii and cube half-sides

Main results

• triadicRadius_half_zpow — the dictionary between the telescope radii based at 3 ^ m / 2 and the half-sides 3 ^ (m - k) / 2 of the cubes of the underlying scale range.

Dictionary with cube half-sides

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicRadius_half_zpow (m : ℤ) (k : ℕ) : triadicRadius (3 ^ m / 2) k = 3 ^ (m - ↑k) / 2

The telescope based at the half-side 3 ^ m / 2 of the top cube visits exactly the half-sides of the cubes of the scale range below it.