Lean 4 Proof

private lemma harmonic_mean_ge_half_min {a b : ℝ} (ha : 0 < a) (hb : 0 < b) :
    min a b / 2 ≤ a * b / (a + b) := by
  rw [div_le_div_iff₀ two_pos (by linarith : 0 < a + b)]
  by_cases h : a ≤ b
  · rw [min_eq_left h]
    nlinarith [mul_le_mul_of_nonneg_left h ha.le]
  · push_neg at h
    rw [min_eq_right h.le]
    nlinarith [mul_le_mul_of_nonneg_left h.le hb.le]

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/Superadditivity.lean:98

Module Section

Superadditivity of CES (Paper 1, Section 6):

In the same file