Documentation

Lean 4 Proof

theorem scalingDimension_monotone {m₁ m₂ : ℕ} (_hm₁ : 3 ≤ m₁) (hm₂ : m₁ ≤ m₂) :
    scalingDimension m₁ ≤ scalingDimension m₂ := by
  simp only [scalingDimension, if_neg (show ¬ m₁ ≤ 2 by omega),
             if_neg (show ¬ m₂ ≤ 2 by omega)]
  apply div_le_div_of_nonneg_right _ (by norm_num : (0 : ℝ) ≤ 2)
  exact_mod_cast (show m₁ - 2 ≤ m₂ - 2 by omega)

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/RenormalizationGroup.lean:132

Module Section

Renormalization Group for CES:

In the same file