Scaling Dimension

def proved Hierarchy

Documentation

Lean 4 Proof

def scalingDimension (m : ℕ) : ℝ :=
  if m ≤ 2 then 0
  else (↑(m - 2) : ℝ) / 2

Dependency Graph

Used by

no_relevant_perturbations scalingDimension_monotone modeRate_eq_rpow_neg_scaling modeAfterL_eq_rpow_scaling scalingDimension_zero_iff_ces scaling_dimension_zero_iff_ces scaling_dimension_cubic slowest_irrelevant_is_cubic scalingDimension_cubic rg_stability_summary scaling_dimension_monotone

Location

thesis/CESProofs/Hierarchy/RenormalizationGroup.lean:47

Module Section

Renormalization Group for CES: