-- Mathlib/NumberTheory/AbelSummation.lean
theorem _root_.integrableOn_mul_sum_Icc {m : ℕ} (ha : 0 ≤ a) {g : ℝ → 𝕜}
    (hg_int : IntegrableOn g (Set.Icc a b)) :
    IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b)

Proof state:
case inl.inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ},
    t₁ ≤ t₂ →
      ↑n ≤ t₁ → t₂ ≤ ↑n + 1 → a ≤ t₁ → t₂ ≤ b → IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
aux2 : ↑⌊a⌋₊ + 1 ≤ b
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : a ≤ ↑⌊b⌋₊
⊢ IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a b

Tactic:
have I1 : IntervalIntegrable _ volume a ↑(⌊a⌋₊ + 1) :=
  h_locint (mod_cast aux3) (Nat.floor_le ha) (mod_cast le_rfl) le_rfl (mod_cast aux2)

Result:
case inl.inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ},
    t₁ ≤ t₂ →
      ↑n ≤ t₁ → t₂ ≤ ↑n + 1 → a ≤ t₁ → t₂ ≤ b → IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
aux2 : ↑⌊a⌋₊ + 1 ≤ b
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : a ≤ ↑⌊b⌋₊
I1 : IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a ↑(⌊a⌋₊ + 1)
⊢ IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a b

Proof state:
case inl.inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
⊢ IntegrableOn (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume

Tactic:
have h_locint {t₁ t₂ : ℝ} {n : ℕ} (h : t₁ ≤ t₂) (h₁ : n ≤ t₁) (h₂ : t₂ ≤ n + 1)
    (h₃ : a ≤ t₁) (h₄ : t₂ ≤ b) :
    IntervalIntegrable (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂ := by
  rw [intervalIntegrable_iff_integrableOn_Icc_of_le h]
  exact (IntegrableOn.mono_set (hg_int.mul_const _) (Set.Icc_subset_Icc h₃ h₄)).congr
    <| ae_restrict_of_ae_restrict_of_subset (Set.Icc_subset_Icc h₁ h₂)
      <| (ae_restrict_iff' measurableSet_Icc).mpr
        (by filter_upwards [sumlocc c n] with t h ht using by rw [h ht])

Result:
case inl.inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ},
    t₁ ≤ t₂ →
      ↑n ≤ t₁ → t₂ ≤ ↑n + 1 → a ≤ t₁ → t₂ ≤ b → IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
⊢ IntegrableOn (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume

Proof state:
case inl.inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ},
    t₁ ≤ t₂ →
      ↑n ≤ t₁ → t₂ ≤ ↑n + 1 → a ≤ t₁ → t₂ ≤ b → IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
aux2 : ↑⌊a⌋₊ + 1 ≤ b
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : a ≤ ↑⌊b⌋₊
I1 : IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a ↑(⌊a⌋₊ + 1)
⊢ IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a b

Tactic:
have I2 : IntervalIntegrable _ volume ↑(⌊a⌋₊ + 1) ⌊b⌋₊ :=
  trans_iterate_Ico hb fun k hk ↦ h_locint (mod_cast k.le_succ)
    le_rfl (mod_cast le_rfl) (ineqofmemIco hk).1 (mod_cast (ineqofmemIco hk).2)

Result:
case inl.inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ},
    t₁ ≤ t₂ →
      ↑n ≤ t₁ → t₂ ≤ ↑n + 1 → a ≤ t₁ → t₂ ≤ b → IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
aux2 : ↑⌊a⌋₊ + 1 ≤ b
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : a ≤ ↑⌊b⌋₊
I1 : IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a ↑(⌊a⌋₊ + 1)
I2 : IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume ↑(⌊a⌋₊ + 1) ↑⌊b⌋₊
⊢ IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a b

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
⊢ IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂

Tactic:
rw [intervalIntegrable_iff_integrableOn_Icc_of_le h]

Result:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
⊢ IntegrableOn (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc t₁ t₂) volume

Proof state:
case inl.inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ = ⌊b⌋₊
⊢ IntegrableOn (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume

Tactic:
have : ∀ᵐ t, t ∈ Set.Icc a b → ∑ k ∈ Icc m ⌊a⌋₊, c k = ∑ k ∈ Icc m ⌊t⌋₊, c k := by
  filter_upwards [sumlocc c ⌊a⌋₊] with t ht₁ ht₂
  rw [ht₁ ⟨(Nat.floor_le ha).trans ht₂.1, hb ▸ ht₂.2.trans (Nat.lt_floor_add_one b).le⟩]

Result:
case inl.inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ = ⌊b⌋₊
this : ∀ᵐ (t : ℝ), t ∈ Set.Icc a b → ∑ k ∈ Icc m ⌊a⌋₊, c k = ∑ k ∈ Icc m ⌊t⌋₊, c k
⊢ IntegrableOn (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
⊢ ∀ᵐ (x : ℝ), x ∈ Set.Icc (↑n) (↑n + 1) → (fun x => g x * ?m.16438) x = (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) x

Tactic:
filter_upwards [sumlocc c n] with t h ht using by rw [h ht]

Result:
no goals

Proof state:
case inl.inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ},
    t₁ ≤ t₂ →
      ↑n ≤ t₁ → t₂ ≤ ↑n + 1 → a ≤ t₁ → t₂ ≤ b → IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
⊢ IntegrableOn (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume

Tactic:
have aux1 : 0 ≤ b := (Nat.pos_of_floor_pos <| (Nat.zero_le _).trans_lt hb).le

Result:
case inl.inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ},
    t₁ ≤ t₂ →
      ↑n ≤ t₁ → t₂ ≤ ↑n + 1 → a ≤ t₁ → t₂ ≤ b → IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
⊢ IntegrableOn (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ},
    t₁ ≤ t₂ →
      ↑n ≤ t₁ → t₂ ≤ ↑n + 1 → a ≤ t₁ → t₂ ≤ b → IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
⊢ ↑⌊a⌋₊ + 1 ≤ b

Tactic:
rwa [← Nat.cast_add_one, ← Nat.le_floor_iff aux1]

Result:
no goals