Documentation

Lean 4 Proof

theorem modeRate_eq_rpow_neg_scaling {k : ℕ} (_hk : 1 ≤ k) (m : ℕ) :
    modeRate k m = (↑k : ℝ) ^ (-scalingDimension m) := by
  by_cases hm : m ≤ 2
  · simp [modeRate, scalingDimension, if_pos hm, neg_zero, rpow_zero]
  · have hm3 : ¬ m ≤ 2 := by omega
    simp only [modeRate, scalingDimension, if_neg hm3]
    congr 1; ring

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/RenormalizationGroup.lean:159

Module Section

Renormalization Group for CES:

In the same file