Documentation

Lean 4 Proof

theorem general_weight_degradation_ordering
    {K K_eff : ℝ} (hK : 0 < K) (hKeff : 0 < K_eff) (hlt : K_eff < K) :
    (K_eff / K) ^ 2 < K_eff / K := by
  have hratio_pos : 0 < K_eff / K := div_pos hKeff hK
  have hratio_lt_one : K_eff / K < 1 := (div_lt_one hK).mpr hlt
  calc (K_eff / K) ^ 2 = K_eff / K * (K_eff / K) := by ring
    _ < K_eff / K * 1 := by
        apply mul_lt_mul_of_pos_left hratio_lt_one hratio_pos
    _ = K_eff / K := by ring

Dependency Graph

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:411

Module Section

## General-Weight Effective Curvature Theorems

In the same file