Part of: Dirichlet series with bounded partial sums: the by-parts series is the analytic continuation to the right half-plane.
TheoremdifferentiableOn_bpSeries
Holomorphy. If the partial sums satisfy
\bigl\| \sum_{k \le n} f(k) \bigr\| \le C for all n, then \tilde A_f is holomorphic
on the open right half-plane \{\mathrm{Re}\, s > 0\}.
Lean code for Theorem differentiableOn_bpSeries
-
⟲
theorem differentiableOn_bpSeries (hC
∀ (n : ℕ), ‖∑ k ∈ Finset.range (n + 1), f k‖ ≤ C: ∀ nℕ, ‖∑ kℕ∈ Finset.rangeFinset.range (n : ℕ) : Finset ℕ`range n` is the set of natural numbers less than `n`.(nℕ+ 1ℕ), fℕ → ℂkℕ‖ ≤ Cℝ) : DifferentiableOnDifferentiableOn.{u_1, u_2, u_3} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E → F) (s : Set E) : Prop`DifferentiableOn 𝕜 f s` means that `f` is differentiable within `s` at any point of `s`.ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.(bpSeriesbpSeries (f : ℕ → ℂ) (s : ℂ) : ℂThe **by-parts series** attached to `f : ℕ → ℂ`: `bpSeries f s = ∑' n, (∑ k ∈ Finset.range (n + 1), f k) * ((n : ℂ) ^ (-s) - ((n : ℂ) + 1) ^ (-s))`. If the partial sums `∑ k ∈ Finset.range (n + 1), f k = ∑_{k ≤ n} f k` are bounded, this series converges and is holomorphic on `{s | 0 < s.re}` (`differentiableOn_bpSeries`) and it agrees with the Dirichlet series `∑' n, f n * (n : ℂ) ^ (-s)` for `1 < s.re` (`tsum_mul_cpow_neg_eq_bpSeries`): it is the analytic continuation of that Dirichlet series to the right half-plane. This is the analytic-continuation object `Ã` of the proof.fℕ → ℂ) {sℂ: ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.| 0ℝ< sℂ.reComplex.re (self : ℂ) : ℝThe real part of a complex number.}theorem differentiableOn_bpSeries (hC
∀ (n : ℕ), ‖∑ k ∈ Finset.range (n + 1), f k‖ ≤ C: ∀ nℕ, ‖∑ kℕ∈ Finset.rangeFinset.range (n : ℕ) : Finset ℕ`range n` is the set of natural numbers less than `n`.(nℕ+ 1ℕ), fℕ → ℂkℕ‖ ≤ Cℝ) : DifferentiableOnDifferentiableOn.{u_1, u_2, u_3} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E → F) (s : Set E) : Prop`DifferentiableOn 𝕜 f s` means that `f` is differentiable within `s` at any point of `s`.ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.(bpSeriesbpSeries (f : ℕ → ℂ) (s : ℂ) : ℂThe **by-parts series** attached to `f : ℕ → ℂ`: `bpSeries f s = ∑' n, (∑ k ∈ Finset.range (n + 1), f k) * ((n : ℂ) ^ (-s) - ((n : ℂ) + 1) ^ (-s))`. If the partial sums `∑ k ∈ Finset.range (n + 1), f k = ∑_{k ≤ n} f k` are bounded, this series converges and is holomorphic on `{s | 0 < s.re}` (`differentiableOn_bpSeries`) and it agrees with the Dirichlet series `∑' n, f n * (n : ℂ) ^ (-s)` for `1 < s.re` (`tsum_mul_cpow_neg_eq_bpSeries`): it is the analytic continuation of that Dirichlet series to the right half-plane. This is the analytic-continuation object `Ã` of the proof.fℕ → ℂ) {sℂ: ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.| 0ℝ< sℂ.reComplex.re (self : ℂ) : ℝThe real part of a complex number.}
Holomorphy is local. Around any s_0 with \mathrm{Re}\, s_0 > 0, choose
0 < \delta < \mathrm{Re}\, s_0 and R \ge 1 with \|s_0\| < R; the previous theorem makes
\tilde A_f holomorphic on the box \{\mathrm{Re}\, s > \delta\} \cap B(0, R), hence at
s_0. As s_0 was arbitrary, \tilde A_f is holomorphic on all of
\{\mathrm{Re}\, s > 0\}. Consumers needing a smaller half-plane, such as
\Omega = \{\mathrm{Re}\, s > 1/2\} downstream, simply restrict. \blacksquare
⟲by`by tac` constructs a term of the expected type by running the tactic(s) `tac`.
introIntroduces one or more hypotheses, optionally naming and/or pattern-matching them.
For each hypothesis to be introduced, the remaining main goal's target type must
be a `let` or function type.
* `intro` by itself introduces one anonymous hypothesis, which can be accessed
by e.g. `assumption`. It is equivalent to `intro _`.
* `intro x y` introduces two hypotheses and names them. Individual hypotheses
can be anonymized via `_`, given a type ascription, or matched against a pattern:
```lean
-- ... ⊢ α × β → ...
intro (a, b)
-- ..., a : α, b : β ⊢ ...
```
* `intro rfl` is short for `intro h; subst h`, if `h` is an equality where the left-hand or right-hand side
is a variable.
* Alternatively, `intro` can be combined with pattern matching much like `fun`:
```lean
intro
| n + 1, 0 => tac
| ...
```
s₀ℂ hs₀s₀ ∈ {s | 0 < s.re}
haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.
* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
where `_` stands for the tactics that follow this one.
It is convenient for types that have only one applicable constructor.
For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
which adds the equation `h : e = pat` to the local context.
The tactic supports all the same syntax variants and options as the `have` term.
## Properties and relations
* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
which may be important for performance reasons.
Consider using the equivalent `let +nondep` to indicate the intent.
hs₀re0 < s₀.re : 0ℝ < s₀ℂ.reComplex.re (self : ℂ) : ℝThe real part of a complex number. := hs₀s₀ ∈ {s | 0 < s.re}
obtainThe `obtain` tactic is a combination of `have` and `rcases`. See `rcases` for
a description of supported patterns.
```lean
obtain ⟨patt⟩ : type := proof
```
is equivalent to
```lean
have h : type := proof
rcases h with ⟨patt⟩
```
If `⟨patt⟩` is omitted, `rcases` will try to infer the pattern.
If `type` is omitted, `:= proof` is required.
⟨δℝ, hδ0 < δ, hδs₀δ < s₀.re⟩ : ∃ δℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. , 0ℝ < δℝ ∧ δℝ < s₀ℂ.reComplex.re (self : ℂ) : ℝThe real part of a complex number. :=
⟨Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists pExistential introduction. If `a : α` and `h : p a`,
then `⟨a, h⟩` is a proof that `∃ x : α, p x`. s₀ℂ.reComplex.re (self : ℂ) : ℝThe real part of a complex number. / 2ℝ,Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists pExistential introduction. If `a : α` and `h : p a`,
then `⟨a, h⟩` is a proof that `∃ x : α, p x`. half_poshalf_pos.{u_2} {α : Type u_2} [Semifield α] [PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α]
(h : 0 < a) : 0 < a / 2 hs₀re0 < s₀.re,Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists pExistential introduction. If `a : α` and `h : p a`,
then `⟨a, h⟩` is a proof that `∃ x : α, p x`. half_lt_selfhalf_lt_self.{u_2} {α : Type u_2} [Semifield α] [PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α] :
0 < a → a / 2 < a**Alias** of the reverse direction of `half_lt_self_iff`. hs₀re0 < s₀.re⟩Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists pExistential introduction. If `a : α` and `h : p a`,
then `⟨a, h⟩` is a proof that `∃ x : α, p x`.
obtainThe `obtain` tactic is a combination of `have` and `rcases`. See `rcases` for
a description of supported patterns.
```lean
obtain ⟨patt⟩ : type := proof
```
is equivalent to
```lean
have h : type := proof
rcases h with ⟨patt⟩
```
If `⟨patt⟩` is omitted, `rcases` will try to infer the pattern.
If `type` is omitted, `:= proof` is required.
⟨Rℝ, hR1 ≤ R, hs₀R‖s₀‖ < R⟩ : ∃ Rℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. , 1ℝ ≤ Rℝ ∧ ‖s₀ℂ‖ < Rℝ :=
⟨Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists pExistential introduction. If `a : α` and `h : p a`,
then `⟨a, h⟩` is a proof that `∃ x : α, p x`. ‖s₀ℂ‖ + 1ℝ,Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists pExistential introduction. If `a : α` and `h : p a`,
then `⟨a, h⟩` is a proof that `∃ x : α, p x`. le_add_of_nonneg_leftle_add_of_nonneg_left.{u_1} {α : Type u_1} [AddZeroClass α] [LE α] [AddRightMono α] {a b : α} (h : 0 ≤ b) : a ≤ b + a (norm_nonnegnorm_nonneg.{u_5} {E : Type u_5} [SeminormedAddGroup E] (a : E) : 0 ≤ ‖a‖ _),Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists pExistential introduction. If `a : α` and `h : p a`,
then `⟨a, h⟩` is a proof that `∃ x : α, p x`. lt_add_onelt_add_one.{u_1} {α : Type u_1} [One α] [AddZeroClass α] [PartialOrder α] [ZeroLEOneClass α] [NeZero 1]
[AddLeftStrictMono α] (a : α) : a < a + 1 _⟩Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists pExistential introduction. If `a : α` and `h : p a`,
then `⟨a, h⟩` is a proof that `∃ x : α, p x`.
haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.
* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
where `_` stands for the tactics that follow this one.
It is convenient for types that have only one applicable constructor.
For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
which adds the equation `h : e = pat` to the local context.
The tactic supports all the same syntax variants and options as the `have` term.
## Properties and relations
* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
which may be important for performance reasons.
Consider using the equivalent `let +nondep` to indicate the intent.
hVopenIsOpen ({s | δ < s.re} ∩ Metric.ball 0 R) : IsOpenIsOpen.{u} {X : Type u} [TopologicalSpace X] : Set X → Prop`IsOpen s` means that `s` is open in the ambient topological space on `X` ({sℂ : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. | δℝ < sℂ.reComplex.re (self : ℂ) : ℝThe real part of a complex number. } ∩ Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε` 0ℂ Rℝ) :=
(isOpen_ltisOpen_lt.{u, v} {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α]
[TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) : IsOpen {b | f b < g b} continuous_constcontinuous_const.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {y : Y} :
Continuous fun x => y Complex.continuous_reComplex.continuous_re : Continuous Complex.re).interIsOpen.inter.{u} {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s ∩ t) Metric.isOpen_ballMetric.isOpen_ball.{u} {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : IsOpen (Metric.ball x ε)
haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.
* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
where `_` stands for the tactics that follow this one.
It is convenient for types that have only one applicable constructor.
For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
which adds the equation `h : e = pat` to the local context.
The tactic supports all the same syntax variants and options as the `have` term.
## Properties and relations
* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
which may be important for performance reasons.
Consider using the equivalent `let +nondep` to indicate the intent.
hs₀Vs₀ ∈ {s | δ < s.re} ∩ Metric.ball 0 R : s₀ℂ ∈ {sℂ : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. | δℝ < sℂ.reComplex.re (self : ℂ) : ℝThe real part of a complex number. } ∩ Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε` 0ℂ Rℝ :=
⟨And.intro {a b : Prop} (left : a) (right : b) : a ∧ b`And.intro : a → b → a ∧ b` is the constructor for the And operation. hδs₀δ < s₀.re,And.intro {a b : Prop} (left : a) (right : b) : a ∧ b`And.intro : a → b → a ∧ b` is the constructor for the And operation. by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
[Metric.mem_ballMetric.mem_ball.{u} {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} : y ∈ Metric.ball x ε ↔ dist y x < ε, dist_zero_rightdist_zero_right.{u_5} {E : Type u_5} [SeminormedAddGroup E] (a : E) : dist a 0 = ‖a‖]; exact`exact e` closes the main goal if its target type matches that of `e`.
hs₀R‖s₀‖ < R⟩And.intro {a b : Prop} (left : a) (right : b) : a ∧ b`And.intro : a → b → a ∧ b` is the constructor for the And operation.
exact`exact e` closes the main goal if its target type matches that of `e`.
(((differentiableOn_bpSeries_boxdifferentiableOn_bpSeries_box {f : ℕ → ℂ} {C : ℝ} (hC : ∀ (n : ℕ), ‖∑ k ∈ Finset.range (n + 1), f k‖ ≤ C) {δ R : ℝ}
(hδ : 0 < δ) (hR : 1 ≤ R) : DifferentiableOn ℂ (bpSeries f) ({s | δ < s.re} ∩ Metric.ball 0 R)**Bounded partial sums give a holomorphic by-parts series on a box**: the Weierstrass
`M`-test packaged from `summable_bpSeries_boxBound`, `differentiableOn_bpSeries_term`, and
`norm_bpSeries_term_le_boxBound`. A box is used because no summable bound is uniform on the
whole half-plane `{0 < s.re}`; `differentiableOn_bpSeries` glues the boxes together. hC∀ (n : ℕ), ‖∑ k ∈ Finset.range (n + 1), f k‖ ≤ C hδ0 < δ hR1 ≤ R) s₀ℂ hs₀Vs₀ ∈ {s | δ < s.re} ∩ Metric.ball 0 R).differentiableAtDifferentiableWithinAt.differentiableAt.{u_1, u_2, u_3} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2}
[AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F]
{f : E → F} {x : E} {s : Set E} (h : DifferentiableWithinAt 𝕜 f s x) (hs : s ∈ nhds x) : DifferentiableAt 𝕜 f x
(hVopenIsOpen ({s | δ < s.re} ∩ Metric.ball 0 R).mem_nhdsIsOpen.mem_nhds.{u} {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} (hs : IsOpen s) (hx : x ∈ s) : s ∈ nhds x hs₀Vs₀ ∈ {s | δ < s.re} ∩ Metric.ball 0 R)).differentiableWithinAtDifferentiableAt.differentiableWithinAt.{u_1, u_2, u_3} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2}
[AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F]
{f : E → F} {x : E} {s : Set E} (h : DifferentiableAt 𝕜 f x) : DifferentiableWithinAt 𝕜 f s x