English
A variant asserting the sum of functions with individual C^N regularity forms a C^N function, under suitable uniform bounds.
Русский
Вариант утверждает, что сумма функций с локальным C^N сохраняет C^N-регулярность при подходящих условиях на границы произвольного порядка.
LaTeX
$$$\text{If each } f_i\in C^N\text{ and }\text{the derivatives are uniformly controlled},\ \sum_i f_i\in C^N.$$$
Lean4
/-- Consider a series of functions `∑' i, f i x`. Assume that each individual function `f i` is of
class `C^N`, and moreover there is a uniform summable upper bound on the `k`-th derivative
for each `k ≤ N` (except maybe for finitely many `i`s). Then the series is also `C^N`. -/
theorem contDiff_tsum_of_eventually (hf : ∀ i, ContDiff 𝕜 N (f i)) (hv : ∀ k : ℕ, k ≤ N → Summable (v k))
(h'f : ∀ k : ℕ, k ≤ N → ∀ᶠ i in (Filter.cofinite : Filter α), ∀ x : E, ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i) :
ContDiff 𝕜 N fun x => ∑' i, f i x := by
classical
refine contDiff_iff_forall_nat_le.2 fun m hm => ?_
let t : Set α := {i : α | ¬∀ k : ℕ, k ∈ Finset.range (m + 1) → ∀ x, ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
have ht : Set.Finite t :=
haveI A :
∀ᶠ i in (Filter.cofinite : Filter α),
∀ k : ℕ, k ∈ Finset.range (m + 1) → ∀ x : E, ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i :=
by
rw [eventually_all_finset]
intro i hi
apply h'f
simp only [Finset.mem_range_succ_iff] at hi
exact (WithTop.coe_le_coe.2 hi).trans hm
eventually_cofinite.2 A
let T : Finset α := ht.toFinset
have : (fun x => ∑' i, f i x) = (fun x => ∑ i ∈ T, f i x) + fun x => ∑' i : { i // i ∉ T }, f i x :=
by
ext1 x
refine (Summable.sum_add_tsum_subtype_compl ?_ T).symm
refine .of_norm_bounded_eventually (hv 0 (zero_le _)) ?_
filter_upwards [h'f 0 (zero_le _)] with i hi
simpa only [norm_iteratedFDeriv_zero] using hi x
rw [this]
apply (ContDiff.sum fun i _ => (hf i).of_le (mod_cast hm)).add
have h'u : ∀ k : ℕ, (k : ℕ∞) ≤ m → Summable (v k ∘ ((↑) : { i // i ∉ T } → α)) := fun k hk =>
(hv k (hk.trans hm)).subtype _
refine contDiff_tsum (fun i => (hf i).of_le (mod_cast hm)) h'u ?_
rintro k ⟨i, hi⟩ x hk
simp only [t, T, Finite.mem_toFinset, mem_setOf_eq, Finset.mem_range, not_forall, not_le, exists_prop, not_exists,
not_and, not_lt] at hi
exact hi k (Nat.lt_succ_iff.2 (WithTop.coe_le_coe.1 hk)) x
