Documentation

Lean 4 Proof

theorem rg_stability_summary {k : ℕ} (hk : 2 ≤ k) (m : ℕ) :
    (m ≤ 2 → modeRate k m = 1) ∧
    (3 ≤ m → 0 < modeRate k m ∧ modeRate k m < 1) ∧
    (0 ≤ scalingDimension m) :=
  ⟨fun hm => by simp [modeRate, if_pos hm],
   fun hm => modeRate_in_unit_interval hk hm,
   no_relevant_perturbations m⟩

Dependency Graph

Location

thesis/CESProofs/Hierarchy/RenormalizationGroup.lean:302

Module Section

Renormalization Group for CES:

In the same file