Groups

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

The rpow / geometric-power bridge of the shell groups

Local helper for ABK26, Section 4.1, the right-hand side of e.mathcalE.annular.decomp. threeRpow_neg_natMul rewrites the real power 3^(-c j) at a natural index j as the j-th power of 3^(-c), which is the form the geometric shell sums of the annular decomposition are stated in.

The rpow / geometric-power bridge

theorem Algsuperdiff.Section4.Provider.Annular.threeRpow_neg_natMul (c : ℝ) (j : ℕ) : 3 ^ (-(c * ↑j)) = (3 ^ (-c)) ^ j

3 ^ (-(c * j)) = (3 ^ (-c)) ^ j for a natural j.