Source indexedlemma · leanprover/lean4:v4.32.0

BKLNW.Pp_convexOn

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean:630 to 636

Mathematical statement

Exact Lean statement

lemma Pp_convexOn {A₁ A₂ E : ℝ} (m : ℕ) (b b' : ℝ) (_hbb' : b ≤ b') (hb20 : 20 ≤ b) (hm : m ≤ 3)
    (hA1 : 0 ≤ A₁) (hA2 : 0 ≤ A₂) (hE : 0 ≤ E) :
    ConvexOn ℝ (Set.Icc b b') (Pp m A₁ A₂ E)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

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