Source indexedlemma · leanprover/lean4:v4.32.0

Ramanujan.integral_Icc_split

PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations · PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:179 to 200

Mathematical statement

Exact Lean statement

lemma integral_Icc_split
    (f : ℝ → ℝ) {a b c : ℝ}
    (hab : a ≤ b) (hbc : b ≤ c)
    (hInt : IntegrableOn f (Set.Icc a c) volume) :
    ∫ t in Set.Icc a c, f t = (∫ t in Set.Icc a b, f t) + (∫ t in Set.Icc b c, f t)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma integral_Icc_split    (f : ℝ → ℝ) {a b c : ℝ}    (hab : a ≤ b) (hbc : b ≤ c)    (hInt : IntegrableOn f (Set.Icc a c) volume) :    ∫ t in Set.Icc a c, f t = (∫ t in Set.Icc a b, f t) + (∫ t in Set.Icc b c, f t) := by  have h_int_left : IntegrableOn f (Set.Icc a b) volume :=    hInt.mono_set (by intro t ht; exact ⟨ht.1, le_trans ht.2 hbc⟩)  have h_int_right : IntegrableOn f (Set.Icc b c) volume :=    hInt.mono_set (by intro t ht; exact ⟨le_trans hab ht.1, ht.2⟩)  have h_int_left_u : IntegrableOn f (Set.uIcc a b) volume := by    simpa [Set.uIcc_of_le hab] using h_int_left  have h_int_right_u : IntegrableOn f (Set.uIcc b c) volume := by    simpa [Set.uIcc_of_le hbc] using h_int_right  have h_split_interval :      ∫ t in a..c, f t = (∫ t in a..b, f t) + (∫ t in b..c, f t) := by    exact (intervalIntegral.integral_add_adjacent_intervals      (MeasureTheory.IntegrableOn.intervalIntegrable h_int_left_u)      (MeasureTheory.IntegrableOn.intervalIntegrable h_int_right_u)).symm  simpa [MeasureTheory.integral_Icc_eq_integral_Ioc,      intervalIntegral.integral_of_le (le_trans hab hbc),      intervalIntegral.integral_of_le hab,      intervalIntegral.integral_of_le hbc] using h_split_interval