Source indexedlemma · leanprover/lean4:v4.32.0

BKLNW.Gp_convexOn

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean:174 to 180

Mathematical statement

Exact Lean statement

lemma Gp_convexOn {A₁ A₂ E : ℝ} (b b' : ℝ) (_hbb' : b ≤ b') (hb20 : 20 ≤ b)
    (hA1 : 0 ≤ A₁) (hA2 : 0 ≤ A₂) (hE : 0 ≤ E) :
    ConvexOn ℝ (Set.Icc b b') (Gp A₁ A₂ E)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Gp_convexOn {A₁ A₂ E : ℝ} (b b' : ℝ) (_hbb' : b ≤ b') (hb20 : 20 ≤ b)    (hA1 : 0 ≤ A₁) (hA2 : 0 ≤ A₂) (hE : 0 ≤ E) :    ConvexOn ℝ (Set.Icc b b') (Gp A₁ A₂ E) := by  apply convexOn_of_hasDerivWithinAt2_nonneg (convex_Icc _ _) (Gp_continuous A₁ A₂ E).continuousOn  · intro y _; exact (Gp_hasDerivAt A₁ A₂ E y).hasDerivWithinAt  · intro y _; exact (Gp'_hasDerivAt A₁ A₂ E y).hasDerivWithinAt  · intro y hy; rw [interior_Icc] at hy; exact Gp''_nonneg hA1 hA2 hE (by linarith [hy.1])