Source indexedtheorem · leanprover/lean4:v4.32.0

RS.Integ.MVThms.MV_Theorem_A3a

PrimeNumberTheoremAnd.Unused.MyMV_A3a · PrimeNumberTheoremAnd/Unused/MyMV_A3a.lean:1504 to 1522

Mathematical statement

Exact Lean statement

theorem MV_Theorem_A3a
  {a b : ℝ} (hab : a < b)
  (g g' : ℝ → ℝ)
  (hg  : ∀ x ∈ Set.Icc a b, HasDerivAt g (g' x) x)
  (hg' : ContinuousOn g' (Set.Icc a b)) :
  ∃ I,
    HasRSIntegral (fun x => |g' x|) id a b I ∧
    BoundedVariationOn g (Set.Icc a b) ∧
    (eVariationOn g (Set.Icc a b)).toReal = I

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem MV_Theorem_A3a  {a b : ℝ} (hab : a < b)  (g g' : ℝ → ℝ)  (hg  : ∀ x ∈ Set.Icc a b, HasDerivAt g (g' x) x)  (hg' : ContinuousOn g' (Set.Icc a b)) :  ∃ I,    HasRSIntegral (fun x => |g' x|) id a b I ∧    BoundedVariationOn g (Set.Icc a b) ∧    (eVariationOn g (Set.Icc a b)).toReal = I := by  obtain ⟨I, hI⟩ := exists_integral_abs_deriv (a := a) (b := b) hab (g' := g') hg'  have hg_bv : BoundedVariationOn g (Set.Icc a b) :=    boundedVariationOn_of_hasRSIntegral_abs_deriv (a := a) (b := b) hab g g' hg I hI  have hVar_le : (eVariationOn g (Set.Icc a b)).toReal ≤ I :=    variation_le_integral_abs_deriv (a := a) (b := b) hab g g' hg hg' I hI  have hI_le : I ≤ (eVariationOn g (Set.Icc a b)).toReal :=    integral_le_variation (a := a) (b := b) hab g g' hg hg_bv I hI  refine ⟨I, ?_, hg_bv, ?_⟩  · simpa [id] using hI  exact (le_antisymm hVar_le hI_le)