Documentation

Lean 4 Proof

private lemma concaveOn_nonneg_of_endpoints {f : ℝ → ℝ}
    (hc : ConcaveOn ℝ (Set.Icc 0 1) f)
    (h0 : 0 ≤ f 0) (h1 : 0 ≤ f 1)
    {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : 0 ≤ f t := by
  have h1_mem : (1 : ℝ) ∈ Set.Icc (0 : ℝ) 1 := ⟨zero_le_one, le_refl _⟩
  have h0_mem : (0 : ℝ) ∈ Set.Icc (0 : ℝ) 1 := ⟨le_refl _, zero_le_one⟩
  have hc2 := hc.2 h1_mem h0_mem ht0 (by linarith : 0 ≤ 1 - t) (by linarith : t + (1 - t) = 1)
  simp only [smul_eq_mul, mul_one, mul_zero, add_zero] at hc2
  linarith [mul_nonneg ht0 h1, mul_nonneg (by linarith : 0 ≤ 1 - t) h0]

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/Superadditivity.lean:114

Module Section

Superadditivity of CES (Paper 1, Section 6):

In the same file