ι : Type ?u.15491641
𝕜 : Type ?u.15491644
E : Type u_1
F : Type ?u.15491650
A : Type ?u.15491653
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ (∀ (k : ℕ), k ∈ Ico m n → IntervalIntegrable f μ (a k) (a (k + 1))) →
    (∑ k in Finset.Ico m n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a n, f x ∂μ
ι : Type ?u.15491641
𝕜 : Type ?u.15491644
E : Type u_1
F : Type ?u.15491650
A : Type ?u.15491653
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
hint : ∀ (k : ℕ), k ∈ Ico m n → IntervalIntegrable f μ (a k) (a (k + 1))
⊢ (∑ k in Finset.Ico m n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a n, f x ∂μ
revert hint
case refine'_1
ι : Type ?u.15491641
𝕜 : Type ?u.15491644
E : Type u_1
F : Type ?u.15491650
A : Type ?u.15491653
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ (∀ (k : ℕ), k ∈ Ico m m → IntervalIntegrable f μ (a k) (a (k + 1))) →
    (∑ k in Finset.Ico m m, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a m, f x ∂μ

case refine'_2
ι : Type ?u.15491641
𝕜 : Type ?u.15491644
E : Type u_1
F : Type ?u.15491650
A : Type ?u.15491653
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ ∀ (n : ℕ),
    m ≤ n →
      ((∀ (k : ℕ), k ∈ Ico m n → IntervalIntegrable f μ (a k) (a (k + 1))) →
          (∑ k in Finset.Ico m n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a n, f x ∂μ) →
        (∀ (k : ℕ), k ∈ Ico m (n + 1) → IntervalIntegrable f μ (a k) (a (k + 1))) →
          (∑ k in Finset.Ico m (n + 1), ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a (n + 1), f x ∂μ
ι : Type ?u.15491641
𝕜 : Type ?u.15491644
E : Type u_1
F : Type ?u.15491650
A : Type ?u.15491653
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ (∀ (k : ℕ), k ∈ Ico m n → IntervalIntegrable f μ (a k) (a (k + 1))) →
    (∑ k in Finset.Ico m n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a n, f x ∂μ
refine' Nat.le_induction _ _ n hmn
no goals
case refine'_1
ι : Type ?u.15491641
𝕜 : Type ?u.15491644
E : Type u_1
F : Type ?u.15491650
A : Type ?u.15491653
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ (∀ (k : ℕ), k ∈ Ico m m → IntervalIntegrable f μ (a k) (a (k + 1))) →
    (∑ k in Finset.Ico m m, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a m, f x ∂μ
simp
case refine'_2
ι : Type ?u.15491641
𝕜 : Type ?u.15491644
E : Type u_1
F : Type ?u.15491650
A : Type ?u.15491653
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ (k : ℕ), k ∈ Ico m p → IntervalIntegrable f μ (a k) (a (k + 1))) →
    (∑ k in Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ (k : ℕ), k ∈ Ico m (p + 1) → IntervalIntegrable f μ (a k) (a (k + 1))
⊢ (∑ k in Finset.Ico m (p + 1), ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a (p + 1), f x ∂μ
case refine'_2
ι : Type ?u.15491641
𝕜 : Type ?u.15491644
E : Type u_1
F : Type ?u.15491650
A : Type ?u.15491653
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ ∀ (n : ℕ),
    m ≤ n →
      ((∀ (k : ℕ), k ∈ Ico m n → IntervalIntegrable f μ (a k) (a (k + 1))) →
          (∑ k in Finset.Ico m n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a n, f x ∂μ) →
        (∀ (k : ℕ), k ∈ Ico m (n + 1) → IntervalIntegrable f μ (a k) (a (k + 1))) →
          (∑ k in Finset.Ico m (n + 1), ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a (n + 1), f x ∂μ
intro p hmp IH h
case refine'_2.hab
ι : Type ?u.15491641
𝕜 : Type ?u.15491644
E : Type u_1
F : Type ?u.15491650
A : Type ?u.15491653
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ (k : ℕ), k ∈ Ico m p → IntervalIntegrable f μ (a k) (a (k + 1))) →
    (∑ k in Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ (k : ℕ), k ∈ Ico m (p + 1) → IntervalIntegrable f μ (a k) (a (k + 1))
⊢ IntervalIntegrable (fun x => f x) μ (a m) (a p)

case refine'_2.hbc
ι : Type ?u.15491641
𝕜 : Type ?u.15491644
E : Type u_1
F : Type ?u.15491650
A : Type ?u.15491653
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ (k : ℕ), k ∈ Ico m p → IntervalIntegrable f μ (a k) (a (k + 1))) →
    (∑ k in Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ (k : ℕ), k ∈ Ico m (p + 1) → IntervalIntegrable f μ (a k) (a (k + 1))
⊢ IntervalIntegrable (fun x => f x) μ (a p) (a (p + 1))

case refine'_2
ι : Type ?u.15491641
𝕜 : Type ?u.15491644
E : Type u_1
F : Type ?u.15491650
A : Type ?u.15491653
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ (k : ℕ), k ∈ Ico m p → IntervalIntegrable f μ (a k) (a (k + 1))) →
    (∑ k in Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ (k : ℕ), k ∈ Ico m (p + 1) → IntervalIntegrable f μ (a k) (a (k + 1))
⊢ ∀ (k : ℕ), k ∈ Ico m p → IntervalIntegrable f μ (a k) (a (k + 1))
case refine'_2
ι : Type ?u.15491641
𝕜 : Type ?u.15491644
E : Type u_1
F : Type ?u.15491650
A : Type ?u.15491653
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ (k : ℕ), k ∈ Ico m p → IntervalIntegrable f μ (a k) (a (k + 1))) →
    (∑ k in Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ (k : ℕ), k ∈ Ico m (p + 1) → IntervalIntegrable f μ (a k) (a (k + 1))
⊢ (∑ k in Finset.Ico m (p + 1), ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a (p + 1), f x ∂μ
rw [Finset.sum_Ico_succ_top hmp, IH, integral_add_adjacent_intervals]
case refine'_2.hab
ι : Type ?u.15491641
𝕜 : Type ?u.15491644
E : Type u_1
F : Type ?u.15491650
A : Type ?u.15491653
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ (k : ℕ), k ∈ Ico m p → IntervalIntegrable f μ (a k) (a (k + 1))) →
    (∑ k in Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ (k : ℕ), k ∈ Ico m (p + 1) → IntervalIntegrable f μ (a k) (a (k + 1))
k : ℕ
hk : k ∈ Ico m p
⊢ k ∈ Ico m (p + 1)
case refine'_2.hab
ι : Type ?u.15491641
𝕜 : Type ?u.15491644
E : Type u_1
F : Type ?u.15491650
A : Type ?u.15491653
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ (k : ℕ), k ∈ Ico m p → IntervalIntegrable f μ (a k) (a (k + 1))) →
    (∑ k in Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ (k : ℕ), k ∈ Ico m (p + 1) → IntervalIntegrable f μ (a k) (a (k + 1))
⊢ IntervalIntegrable (fun x => f x) μ (a m) (a p)
refine IntervalIntegrable.trans_iterate_Ico hmp fun k hk => h k ?_
no goals
case refine'_2.hab
ι : Type ?u.15491641
𝕜 : Type ?u.15491644
E : Type u_1
F : Type ?u.15491650
A : Type ?u.15491653
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ (k : ℕ), k ∈ Ico m p → IntervalIntegrable f μ (a k) (a (k + 1))) →
    (∑ k in Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ (k : ℕ), k ∈ Ico m (p + 1) → IntervalIntegrable f μ (a k) (a (k + 1))
k : ℕ
hk : k ∈ Ico m p
⊢ k ∈ Ico m (p + 1)
exact (Ico_subset_Ico le_rfl (Nat.le_succ _)) hk
case refine'_2.hbc.a
ι : Type ?u.15491641
𝕜 : Type ?u.15491644
E : Type u_1
F : Type ?u.15491650
A : Type ?u.15491653
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ (k : ℕ), k ∈ Ico m p → IntervalIntegrable f μ (a k) (a (k + 1))) →
    (∑ k in Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ (k : ℕ), k ∈ Ico m (p + 1) → IntervalIntegrable f μ (a k) (a (k + 1))
⊢ p ∈ Ico m (p + 1)
case refine'_2.hbc
ι : Type ?u.15491641
𝕜 : Type ?u.15491644
E : Type u_1
F : Type ?u.15491650
A : Type ?u.15491653
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ (k : ℕ), k ∈ Ico m p → IntervalIntegrable f μ (a k) (a (k + 1))) →
    (∑ k in Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ (k : ℕ), k ∈ Ico m (p + 1) → IntervalIntegrable f μ (a k) (a (k + 1))
⊢ IntervalIntegrable (fun x => f x) μ (a p) (a (p + 1))
apply h
no goals
case refine'_2.hbc.a
ι : Type ?u.15491641
𝕜 : Type ?u.15491644
E : Type u_1
F : Type ?u.15491650
A : Type ?u.15491653
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ (k : ℕ), k ∈ Ico m p → IntervalIntegrable f μ (a k) (a (k + 1))) →
    (∑ k in Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ (k : ℕ), k ∈ Ico m (p + 1) → IntervalIntegrable f μ (a k) (a (k + 1))
⊢ p ∈ Ico m (p + 1)
simp [hmp]
case refine'_2
ι : Type ?u.15491641
𝕜 : Type ?u.15491644
E : Type u_1
F : Type ?u.15491650
A : Type ?u.15491653
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ (k : ℕ), k ∈ Ico m p → IntervalIntegrable f μ (a k) (a (k + 1))) →
    (∑ k in Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ (k : ℕ), k ∈ Ico m (p + 1) → IntervalIntegrable f μ (a k) (a (k + 1))
k : ℕ
hk : k ∈ Ico m p
⊢ IntervalIntegrable f μ (a k) (a (k + 1))
case refine'_2
ι : Type ?u.15491641
𝕜 : Type ?u.15491644
E : Type u_1
F : Type ?u.15491650
A : Type ?u.15491653
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ (k : ℕ), k ∈ Ico m p → IntervalIntegrable f μ (a k) (a (k + 1))) →
    (∑ k in Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ (k : ℕ), k ∈ Ico m (p + 1) → IntervalIntegrable f μ (a k) (a (k + 1))
⊢ ∀ (k : ℕ), k ∈ Ico m p → IntervalIntegrable f μ (a k) (a (k + 1))
intro k hk
no goals
case refine'_2
ι : Type ?u.15491641
𝕜 : Type ?u.15491644
E : Type u_1
F : Type ?u.15491650
A : Type ?u.15491653
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ (k : ℕ), k ∈ Ico m p → IntervalIntegrable f μ (a k) (a (k + 1))) →
    (∑ k in Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ (k : ℕ), k ∈ Ico m (p + 1) → IntervalIntegrable f μ (a k) (a (k + 1))
k : ℕ
hk : k ∈ Ico m p
⊢ IntervalIntegrable f μ (a k) (a (k + 1))
exact h _ (Ico_subset_Ico_right p.le_succ hk)