Documentation

Lean 4 Proof

theorem scalingDimension_zero_iff_ces (m : ℕ) :
    scalingDimension m = 0 ↔ m ≤ 2 := by
  constructor
  · intro h
    by_contra hm
    push_neg at hm
    simp only [scalingDimension, if_neg (show ¬ m ≤ 2 by omega)] at h
    have : (0 : ℝ) < ↑(m - 2) := by exact_mod_cast (show 0 < m - 2 by omega)
    linarith [div_pos this two_pos]
  · intro h
    simp [scalingDimension, if_pos h]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/RenormalizationGroup.lean:112

Module Section

Renormalization Group for CES:

In the same file