A362583

⟲by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
  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.

 h1Summable fun p => χ ↑↑p * ↑↑p ^ (-s) : SummableSummable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α)
  (L : SummationFilter β := SummationFilter.unconditional β) : Prop`Summable f` means that `f` has some (infinite) sum with respect to `L`. Use `tsum` to get the
value.  (fun pNat.Primes : Nat.PrimesNat.Primes : TypeThe type of prime numbers  ↦ χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  ((pNat.Primes : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  4ℕ) * ((pNat.Primes : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-sℂ)) :=
    summable_layerA_termA362583.summable_layerA_term {s : ℂ} (hs : 1 < s.re) : Summable fun p => χ ↑↑p * ↑↑p ^ (-s)Summability of the `layerA` integrand for `Re s > 1`.  hs1 < 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.

 h2Summable fun p => χ ↑↑p ^ 2 * ↑↑p ^ (-(2 * s)) / 2 : SummableSummable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α)
  (L : SummationFilter β := SummationFilter.unconditional β) : Prop`Summable f` means that `f` has some (infinite) sum with respect to `L`. Use `tsum` to get the
value. 
      (fun pNat.Primes : Nat.PrimesNat.Primes : TypeThe type of prime numbers  ↦ χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  ((pNat.Primes : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  4ℕ) ^ 2ℕ * ((pNat.Primes : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-(2ℂ * sℂ)) / 2ℂ) :=
    (summable_norm_term_twoA362583.summable_norm_term_two {s : ℂ} (hs : 1 / 2 < s.re) : Summable fun p => ‖χ ↑↑p ^ 2 * ↑↑p ^ (-(2 * s)) / 2‖Absolute summability of the `k = 2` terms for `Re s > 1/2`
(domination by `p^(-2 Re s)`).  (by`by tac` constructs a term of the expected type by running the tactic(s) `tac`.  linarith`linarith` attempts to find a contradiction between hypotheses that are linear (in)equalities.
Equivalently, it can prove a linear inequality by assuming its negation and proving `False`.

In theory, `linarith` should prove any goal that is true in the theory of linear arithmetic over
the rationals. While there is some special handling for non-dense orders like `Nat` and `Int`,
this tactic is not complete for these theories and will not prove every true goal. It will solve
goals over arbitrary types that instantiate `CommRing`, `LinearOrder` and `IsStrictOrderedRing`.

An example:
```lean
example (x y z : ℚ) (h1 : 2*x < 3*y) (h2 : -4*x + 2*z < 0)
        (h3 : 12*y - 4* z < 0) : False := by
  linarith
```

`linarith` will use all appropriate hypotheses and the negation of the goal, if applicable.
Disequality hypotheses require case splitting and are not normally considered
(see the `splitNe` option below).

`linarith [t1, t2, t3]` will additionally use proof terms `t1, t2, t3`.

`linarith only [h1, h2, h3, t1, t2, t3]` will use only the goal (if relevant), local hypotheses
`h1`, `h2`, `h3`, and proofs `t1`, `t2`, `t3`. It will ignore the rest of the local context.

`linarith!` will use a stronger reducibility setting to try to identify atoms. For example,
```lean
example (x : ℚ) : id x ≥ x := by
  linarith
```
will fail, because `linarith` will not identify `x` and `id x`. `linarith!` will.
This can sometimes be expensive.

`linarith (config := { .. })` takes a config object with five
optional arguments:
* `discharger` specifies a tactic to be used for reducing an algebraic equation in the
  proof stage. The default is `ring`. Other options include `simp` for basic
  problems.
* `transparency` controls how hard `linarith` will try to match atoms to each other. By default
  it will only unfold `reducible` definitions.
* If `splitHypotheses` is true, `linarith` will split conjunctions in the context into separate
  hypotheses.
* If `splitNe` is `true`, `linarith` will case split on disequality hypotheses.
  For a given `x ≠ y` hypothesis, `linarith` is run with both `x < y` and `x > y`,
  and so this runs linarith exponentially many times with respect to the number of
  disequality hypotheses. (`false` by default.)
* If `exfalso` is `false`, `linarith` will fail when the goal is neither an inequality nor `False`.
  (`true` by default.)
* If `minimize` is `false`, `linarith?` will report all hypotheses appearing in its initial
  proof without attempting to drop redundancies. (`true` by default.)
* `restrict_type` (not yet implemented in mathlib4)
  will only use hypotheses that are inequalities over `tp`. This is useful
  if you have e.g. both integer- and rational-valued inequalities in the local context, which can
  sometimes confuse the tactic.

A variant, `nlinarith`, does some basic preprocessing to handle some nonlinear goals.

The option `set_option trace.linarith true` will trace certain intermediate stages of the `linarith`
routine.
)).of_normSummable.of_norm.{u_1, u_3} {ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E] [CompleteSpace E] {f : ι → E}
  (hf : Summable fun a => ‖f a‖) : Summable f
  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.

 h3Summable fun p => tp p s : SummableSummable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α)
  (L : SummationFilter β := SummationFilter.unconditional β) : Prop`Summable f` means that `f` has some (infinite) sum with respect to `L`. Use `tsum` to get the
value.  (fun pNat.Primes : Nat.PrimesNat.Primes : TypeThe type of prime numbers  ↦ tpA362583.tp (p : Nat.Primes) (s : ℂ) : ℂPer-prime `k ≥ 3` tail `t_p(s) = Σ_{k≥0} (χ(p) p^(-s))^(k+3) / (k+3)`.
The compact form `z_p^(k+3)/(k+3)` (rather than the expanded
`χ(p)^(k+3) p^(-(k+3)s)/(k+3)`) is chosen so that the tail produced by peeling three
terms off `hasSum_neg_log_one_sub` is *definitionally* `tp p s` (see `neg_log_split`).  pNat.Primes sℂ) := summable_tpA362583.summable_tp {s : ℂ} (hs : 1 / 2 ≤ s.re) : Summable fun p => tp p sPlain summability of the `layerT` integrand on `Re s ≥ 1/2`.  (by`by tac` constructs a term of the expected type by running the tactic(s) `tac`.  linarith`linarith` attempts to find a contradiction between hypotheses that are linear (in)equalities.
Equivalently, it can prove a linear inequality by assuming its negation and proving `False`.

In theory, `linarith` should prove any goal that is true in the theory of linear arithmetic over
the rationals. While there is some special handling for non-dense orders like `Nat` and `Int`,
this tactic is not complete for these theories and will not prove every true goal. It will solve
goals over arbitrary types that instantiate `CommRing`, `LinearOrder` and `IsStrictOrderedRing`.

An example:
```lean
example (x y z : ℚ) (h1 : 2*x < 3*y) (h2 : -4*x + 2*z < 0)
        (h3 : 12*y - 4* z < 0) : False := by
  linarith
```

`linarith` will use all appropriate hypotheses and the negation of the goal, if applicable.
Disequality hypotheses require case splitting and are not normally considered
(see the `splitNe` option below).

`linarith [t1, t2, t3]` will additionally use proof terms `t1, t2, t3`.

`linarith only [h1, h2, h3, t1, t2, t3]` will use only the goal (if relevant), local hypotheses
`h1`, `h2`, `h3`, and proofs `t1`, `t2`, `t3`. It will ignore the rest of the local context.

`linarith!` will use a stronger reducibility setting to try to identify atoms. For example,
```lean
example (x : ℚ) : id x ≥ x := by
  linarith
```
will fail, because `linarith` will not identify `x` and `id x`. `linarith!` will.
This can sometimes be expensive.

`linarith (config := { .. })` takes a config object with five
optional arguments:
* `discharger` specifies a tactic to be used for reducing an algebraic equation in the
  proof stage. The default is `ring`. Other options include `simp` for basic
  problems.
* `transparency` controls how hard `linarith` will try to match atoms to each other. By default
  it will only unfold `reducible` definitions.
* If `splitHypotheses` is true, `linarith` will split conjunctions in the context into separate
  hypotheses.
* If `splitNe` is `true`, `linarith` will case split on disequality hypotheses.
  For a given `x ≠ y` hypothesis, `linarith` is run with both `x < y` and `x > y`,
  and so this runs linarith exponentially many times with respect to the number of
  disequality hypotheses. (`false` by default.)
* If `exfalso` is `false`, `linarith` will fail when the goal is neither an inequality nor `False`.
  (`true` by default.)
* If `minimize` is `false`, `linarith?` will report all hypotheses appearing in its initial
  proof without attempting to drop redundancies. (`true` by default.)
* `restrict_type` (not yet implemented in mathlib4)
  will only use hypotheses that are inequalities over `tp`. This is useful
  if you have e.g. both integer- and rational-valued inequalities in the local context, which can
  sometimes confuse the tactic.

A variant, `nlinarith`, does some basic preprocessing to handle some nonlinear goals.

The option `set_option trace.linarith true` will trace certain intermediate stages of the `linarith`
routine.
)
  calcStep-wise reasoning over transitive relations.
```
calc
  a = b := pab
  b = c := pbc
  ...
  y = z := pyz
```
proves `a = z` from the given step-wise proofs. `=` can be replaced with any
relation implementing the typeclass `Trans`. Instead of repeating the right-
hand sides, subsequent left-hand sides can be replaced with `_`.
```
calc
  a = b := pab
  _ = c := pbc
  ...
  _ = z := pyz
```
It is also possible to write the *first* relation as `<lhs>\n  _ = <rhs> :=
<proof>`. This is useful for aligning relation symbols, especially on longer
identifiers:
```
calc abc
  _ = bce := pabce
  _ = cef := pbcef
  ...
  _ = xyz := pwxyz
```

`calc` works as a term, as a tactic or as a `conv` tactic.

See [Theorem Proving in Lean 4][tpil4] for more information.

[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#calculational-proofs
 ∑' pNat.Primes : Nat.PrimesNat.Primes : TypeThe type of prime numbers , -Complex.logComplex.log (x : ℂ) : ℂInverse of the `exp` function. Returns values such that `(log x).im > - π` and `(log x).im ≤ π`.
`log 0 = 0`  (1ℂ - χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  ((pNat.Primes : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  4ℕ) * ((pNat.Primes : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-sℂ))
      = ∑' pNat.Primes : Nat.PrimesNat.Primes : TypeThe type of prime numbers , (χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  ((pNat.Primes : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  4ℕ) * ((pNat.Primes : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-sℂ)
          + χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  ((pNat.Primes : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  4ℕ) ^ 2ℕ * ((pNat.Primes : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-(2ℂ * sℂ)) / 2ℂ + tpA362583.tp (p : Nat.Primes) (s : ℂ) : ℂPer-prime `k ≥ 3` tail `t_p(s) = Σ_{k≥0} (χ(p) p^(-s))^(k+3) / (k+3)`.
The compact form `z_p^(k+3)/(k+3)` (rather than the expanded
`χ(p)^(k+3) p^(-(k+3)s)/(k+3)`) is chosen so that the tail produced by peeling three
terms off `hasSum_neg_log_one_sub` is *definitionally* `tp p s` (see `neg_log_split`).  pNat.Primes sℂ) :=
        tsum_congrtsum_congr.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β}
  {f g : β → α} (hfg : ∀ (b : β), f b = g b) : ∑'[L] (b : β), f b = ∑'[L] (b : β), g b fun pNat.Primes ↦ neg_log_splitA362583.neg_log_split (p : Nat.Primes) {s : ℂ} (hs : 1 < s.re) :
  -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s)) = χ ↑↑p * ↑↑p ^ (-s) + χ ↑↑p ^ 2 * ↑↑p ^ (-(2 * s)) / 2 + tp p s**Per-prime split**: for `Re s > 1`,
`-log(1 - χ(p) p^(-s)) = χ(p) p^(-s) + χ(p)² p^(-2s)/2 + t_p(s)`.
Proof: peel three terms off the log series with `Summable.sum_add_tsum_nat_add 3`
+ `Finset.sum_range_succ`; the `k = 0` term is `0`, the tail is definitionally
`tp p s`.  No rearrangement is involved.  pNat.Primes hs1 < s.re
    _ = (∑' pNat.Primes : Nat.PrimesNat.Primes : TypeThe type of prime numbers , (χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  ((pNat.Primes : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  4ℕ) * ((pNat.Primes : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-sℂ)
          + χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  ((pNat.Primes : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  4ℕ) ^ 2ℕ * ((pNat.Primes : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-(2ℂ * sℂ)) / 2ℂ))
          + ∑' pNat.Primes : Nat.PrimesNat.Primes : TypeThe type of prime numbers , tpA362583.tp (p : Nat.Primes) (s : ℂ) : ℂPer-prime `k ≥ 3` tail `t_p(s) = Σ_{k≥0} (χ(p) p^(-s))^(k+3) / (k+3)`.
The compact form `z_p^(k+3)/(k+3)` (rather than the expanded
`χ(p)^(k+3) p^(-(k+3)s)/(k+3)`) is chosen so that the tail produced by peeling three
terms off `hasSum_neg_log_one_sub` is *definitionally* `tp p s` (see `neg_log_split`).  pNat.Primes sℂ := (h1Summable fun p => χ ↑↑p * ↑↑p ^ (-s).addSummable.add.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f g : β → α}
  {L : SummationFilter β} [ContinuousAdd α] (hf : Summable f L) (hg : Summable g L) : Summable (fun b => f b + g b) L h2Summable fun p => χ ↑↑p ^ 2 * ↑↑p ^ (-(2 * s)) / 2).tsum_addSummable.tsum_add.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f g : β → α}
  {L : SummationFilter β} [T2Space α] [ContinuousAdd α] [L.NeBot] (hf : Summable f L) (hg : Summable g L) :
  ∑'[L] (b : β), (f b + g b) = ∑'[L] (b : β), f b + ∑'[L] (b : β), g b h3Summable fun p => tp p s
    _ = ((∑' pNat.Primes : Nat.PrimesNat.Primes : TypeThe type of prime numbers , χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  ((pNat.Primes : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  4ℕ) * ((pNat.Primes : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-sℂ))
          + ∑' pNat.Primes : Nat.PrimesNat.Primes : TypeThe type of prime numbers , χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  ((pNat.Primes : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  4ℕ) ^ 2ℕ * ((pNat.Primes : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-(2ℂ * sℂ)) / 2ℂ)
          + ∑' pNat.Primes : Nat.PrimesNat.Primes : TypeThe type of prime numbers , tpA362583.tp (p : Nat.Primes) (s : ℂ) : ℂPer-prime `k ≥ 3` tail `t_p(s) = Σ_{k≥0} (χ(p) p^(-s))^(k+3) / (k+3)`.
The compact form `z_p^(k+3)/(k+3)` (rather than the expanded
`χ(p)^(k+3) p^(-(k+3)s)/(k+3)`) is chosen so that the tail produced by peeling three
terms off `hasSum_neg_log_one_sub` is *definitionally* `tp p s` (see `neg_log_split`).  pNat.Primes sℂ := 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.
 [h1Summable fun p => χ ↑↑p * ↑↑p ^ (-s).tsum_addSummable.tsum_add.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f g : β → α}
  {L : SummationFilter β} [T2Space α] [ContinuousAdd α] [L.NeBot] (hf : Summable f L) (hg : Summable g L) :
  ∑'[L] (b : β), (f b + g b) = ∑'[L] (b : β), f b + ∑'[L] (b : β), g b h2Summable fun p => χ ↑↑p ^ 2 * ↑↑p ^ (-(2 * s)) / 2]
    _ = layerAA362583.layerA (s : ℂ) : ℂThe `k = 1` layer `A(s) = Σ_p χ(p) p^(-s)`.  sℂ + layerBA362583.layerB (s : ℂ) : ℂThe `k = 2` layer `B(s) = (1/2) Σ_{p odd} p^(-2s)`, with an `if`-mask at
`p = 2` (`χ(2)² = 0`, `χ(p)² = 1` for odd `p`; see `χ_sq_eq_ite`,
`tsum_term_two_eq_layerB`).  Exponent convention: `-(2 * s)`.  sℂ + layerTA362583.layerT (s : ℂ) : ℂThe `k ≥ 3` layer `T(s) = Σ_p t_p(s)`.  sℂ := 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.
 [tsum_term_two_eq_layerBA362583.tsum_term_two_eq_layerB (s : ℂ) : ∑' (p : Nat.Primes), χ ↑↑p ^ 2 * ↑↑p ^ (-(2 * s)) / 2 = layerB sSumming the `k = 2` terms over primes gives exactly `layerB` (via
`χ_sq_eq_ite`; unconditional). ]; rflThis tactic applies to a goal whose target has the form `x ~ x`,
where `~` is equality, heterogeneous equality or any relation that
has a reflexivity lemma tagged with the attribute @[refl].