Documentation

Lean 4 Proof

theorem nontrivial_fixed_point_iff {J : ℕ} (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1) :
    0 < curvatureK J ρ :=
  curvatureK_pos hJ hρ

Dependency Graph

Location

thesis/CESProofs/Hierarchy/RenormalizationGroup.lean:251

Module Section

Renormalization Group for CES:

In the same file