Documentation

Lean 4 Proof

theorem generalKeff_reduction_equal_weights
    {J : ℕ} (hJ : 0 < J) (ρ T Tstar : ℝ) :
    generalEffectiveCurvatureKeff J ρ (fun _ => (1 : ℝ) / J) T Tstar
    = effectiveCurvatureKeff J ρ T Tstar := by
  unfold generalEffectiveCurvatureKeff effectiveCurvatureKeff
  rw [K_reduction_equal_weights hJ]

Dependency Graph

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:309

Module Section

## General-Weight Effective Curvature Theorems

In the same file