Source indexedlemma · leanprover/lean4:v4.32.0

BKLNW.G1_convexOn

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean:485 to 491

Mathematical statement

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

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