Documentation

Lean 4 Proof

theorem no_relevant_perturbations (m : ℕ) :
    0 ≤ scalingDimension m := by
  simp only [scalingDimension]
  split
  · exact le_refl 0
  · exact div_nonneg (by exact_mod_cast (Nat.zero_le _)) (by norm_num)

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/RenormalizationGroup.lean:142

Module Section

Renormalization Group for CES:

In the same file