English
If the family of sup-norms of the translated restrictions of a continuous map on Icc(0,1) is summable, then the map is integrable on the whole real line.
Русский
Если сумма максимумов норм переноса ограничений функции на Icc(0,1) конечна, то функция интегрируема по всей прямой.
LaTeX
$$$\text{Integrable}(f) \quad\Longrightarrow\quad \text{Summable}(f|_{Icc}) \Rightarrow \text{Integrable}(f|_{\mathbb{R}})$$$
Lean4
/-- If the sequence with `n`-th term the sup norm of `fun x ↦ f (x + n)` on the interval `Icc 0 1`,
for `n ∈ ℤ`, is summable, then `f` is integrable on `ℝ`. -/
theorem integrable_of_summable_norm_Icc {E : Type*} [NormedAddCommGroup E] {f : C(ℝ, E)}
(hf : Summable fun n : ℤ => ‖(f.comp <| ContinuousMap.addRight n).restrict (Icc 0 1)‖) : Integrable f :=
by
refine
integrable_of_summable_norm_restrict
(.of_nonneg_of_le
(fun n : ℤ =>
mul_nonneg (norm_nonneg (f.restrict (⟨Icc (n : ℝ) ((n : ℝ) + 1), isCompact_Icc⟩ : Compacts ℝ)))
ENNReal.toReal_nonneg)
(fun n => ?_) hf)
?_
· simp only [Compacts.coe_mk, le_add_iff_nonneg_right, zero_le_one, volume_real_Icc_of_le, add_sub_cancel_left,
mul_one, norm_le _ (norm_nonneg _), ContinuousMap.restrict_apply]
intro x
have :=
((f.comp <| ContinuousMap.addRight n).restrict (Icc 0 1)).norm_coe_le_norm
⟨x - n, ⟨sub_nonneg.mpr x.2.1, sub_le_iff_le_add'.mpr x.2.2⟩⟩
simpa only [ContinuousMap.restrict_apply, comp_apply, coe_addRight, Subtype.coe_mk, sub_add_cancel] using this
· exact iUnion_Icc_intCast ℝ
