Documentation

Lean 4 Proof

theorem universality {J₁ J₂ : ℕ} {ρ₁ ρ₂ : ℝ}
    {T₁ Tstar₁ T₂ Tstar₂ : ℝ}
    (hK1 : curvatureK J₁ ρ₁ ≠ 0)
    (hK2 : curvatureK J₂ ρ₂ ≠ 0)
    (hratio : T₁ / Tstar₁ = T₂ / Tstar₂) :
    effectiveCurvatureKeff J₁ ρ₁ T₁ Tstar₁ / curvatureK J₁ ρ₁ =
    effectiveCurvatureKeff J₂ ρ₂ T₂ Tstar₂ / curvatureK J₂ ρ₂ := by
  rw [keff_reduced_universal J₁ ρ₁ T₁ Tstar₁ hK1,
      keff_reduced_universal J₂ ρ₂ T₂ Tstar₂ hK2]
  unfold reducedOrderParam
  rw [hratio]

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/PhaseTransition.lean:292

Module Section

Phase Transition at T* (Gap #8)

In the same file