English
Let 𝕜 be a complex-like field, c: ℕ → 𝕜, f: ℝ → 𝕜, a ≤ b in ℝ, with f differentiable on [a, b] and f' integrable on [a, b]. Then the weighted sum ∑_{k=⌊a⌋+1}^{⌊b⌋} f(k)c(k) equals f(b)∑_{k≤⌊b⌋} c(k) − f(a)∑_{k≤⌊a⌋} c(k) − ∫_{t∈(a,b)} f'(t) ∑_{k≤⌊t⌋} c(k) dt.
Русский
Пусть 𝕜 — поле подобное комплексному, c: ℕ → 𝕜, f: ℝ → 𝕜, a ≤ b, и f дифференцируема на [a,b] с интегрируемой производной. Тогда взвешенная сумма ∑_{k=⌊a⌋+1}^{⌊b⌋} f(k)c(k) равна f(b)∑_{k≤⌊b⌋} c(k) − f(a)∑_{k≤⌊a⌋} c(k) − ∫_{t∈(a,b)} f'(t)∑_{k≤⌊t⌋} c(k) dt.
LaTeX
$$$\\sum_{k \\in Ioc \\lfloor a \\rfloor_+ \\lfloor b \\rfloor_+} f(k) c(k) = f(b) \\sum_{k \\in Icc 0 \\lfloor b \\rfloor_+} c(k) - f(a) \\sum_{k \\in Icc 0 \\lfloor a \\rfloor_+} c(k) - \\int_{t \\in Ioc a b} f'(t) \\sum_{k \\in Icc 0 \\lfloor t \\rfloor_+} c(k) \\, dt$$$
Lean4
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) :=
by
obtain hab | hab := le_or_gt a b
· obtain hb | hb := eq_or_lt_of_le (Nat.floor_le_floor hab)
· 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⟩]
rw [← ae_restrict_iff' measurableSet_Icc] at this
exact IntegrableOn.congr_fun_ae (hg_int.mul_const _) ((Filter.EventuallyEq.refl _ g).mul this)
· 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])
have aux1 : 0 ≤ b := (Nat.pos_of_floor_pos <| (Nat.zero_le _).trans_lt hb).le
have aux2 : ⌊a⌋₊ + 1 ≤ b := by rwa [← Nat.cast_add_one, ← Nat.le_floor_iff aux1]
have aux3 : a ≤ ⌊a⌋₊ + 1 := (Nat.lt_floor_add_one _).le
have aux4 : a ≤ ⌊b⌋₊ :=
le_of_lt
(by rwa [← Nat.floor_lt ha])
-- now break up into 3 subintervals
rw [← intervalIntegrable_iff_integrableOn_Icc_of_le (aux3.trans aux2)]
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)
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)
have I3 : IntervalIntegrable _ volume ⌊b⌋₊ b :=
h_locint (Nat.floor_le aux1) le_rfl (Nat.lt_floor_add_one _).le aux4 le_rfl
exact (I1.trans I2).trans I3
· rw [Set.Icc_eq_empty_of_lt hab]
exact integrableOn_empty
