integral_le_sub_of_hasDeriv_right_of_le

English

Under appropriate hypotheses, ∫_{a}^{b} g'(y) dy = g(b) − g(a).

Русский

При подходящих гипотезах имеет место равенство ∫_{a}^{b} g'(y) dy = g(b) − g(a).

LaTeX

$$$\\int_{a}^{b} g'(y)\\,dy = g(b)-g(a)$$$

Lean4

/-- Auxiliary lemma in the proof of `integral_eq_sub_of_hasDeriv_right_of_le`. -/
theorem integral_le_sub_of_hasDeriv_right_of_le (hab : a ≤ b) (hcont : ContinuousOn g (Icc a b))
    (hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x) (φint : IntegrableOn φ (Icc a b))
    (hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x) : (∫ y in a..b, φ y) ≤ g b - g a :=
  by
  rw [← neg_le_neg_iff]
  convert
    sub_le_integral_of_hasDeriv_right_of_le hab hcont.neg (fun x hx => (hderiv x hx).neg) φint.neg fun x hx =>
      neg_le_neg (hφg x hx) using
    1
  · abel
  · simp only [← integral_neg]; rfl

Похожие утверждения