Documentation

Lean 4 Proof

theorem modeAfterL_eq_rpow_scaling {k : ℕ} (hk : 1 ≤ k) (m L : ℕ) (a₀ : ℝ) :
    modeAfterL k m L a₀ =
    ((↑k : ℝ) ^ (-scalingDimension m)) ^ L * a₀ := by
  simp only [modeAfterL, modeRate_eq_rpow_neg_scaling hk]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/RenormalizationGroup.lean:170

Module Section

Renormalization Group for CES:

In the same file