Question about `formal_multilinear_series`

Stream: general

[Kevin Wilson]

In my ongoing saga of merging in a proof that the density of squarefree integers is ζ(2)⁻¹, I was wondering about the best way to approach the formal_multilinear_series API. In particular, I wanted to formalize the fact that a uniform limit of holomorphic functions is holomorphic in a different way than #13500.

Specifically, let $f_n : \mathbb{C} → \mathbb{C}$ be a sequence of functions which are analytic on the disk of radius $r > 0$ centered at $0$ and which converge uniformly to some $f$ on that disk. Then $f_n (z) = \sum a_{ni} z^i / i!$ for some $a_{ni} \in \mathbb{C}$ and all $|z| < r$. Let $f_n^M(z) = \sum_{i=0}^M a_{ni} z^i / i!$ be the partial sums.

Define $F_n (z) = \sum a_{ni} z^{i+1} / (i + 1)!$ and $F_n^M$ the partial sums. By the fundamental theorem of calculus and linearity of integration, for all $|z| < r$ we have $F_n^M(z) = z\int_0^1 f_n^M(tz)dt$.

With these definitions in hand, you can apply #14090, dominated convergence, and the fact that the partial sums of power series converge uniformly on all closed balls within their radius of convergence several times to show that the $F_n^M$ converge (necessarily to $F_n$), the $F_n$ converge to some $F$, thus $F' = f$ and so $f$ is holomorphic.

My difficulty is that I'm finding the formal_multilinear_series API to be very difficult to grok. I was curious if someone could give me a hint toward defining the partial sums $F_n^M$ above?

[Eric Wieser]

Does looking at the definition of src#exp and src#exp_series help at all?

[Eric Wieser]

Once you've managed to construct the series object, the partial sums should be docs#formal_multilinear_series.partial_sum

[Vincent Beffara]

I am having a similar experience trying to prove the isolated zeros theorem for analytic functions, that manipulating formal_multilinear_series explicitly (in my case, to extract a (z-z0)^n factor) is a little painful. src#exp_series is nice, but as far as I can tell the series provided from analytic_at for a function from C to C is not of that form so it does not really help...

[Sebastien Gouezel]

formal_multilinear_series is specifically designed for functions of several variables. For functions of one variable, one should definitely build a simplified and easier to use API, in the same way that we have fderiv for the general Fréchet derivative, and deriv for the more specific one-dimensional version.

[Eric Wieser]

I don't agree that it's for multiple variables, things like docs#formal_multilinear_series.sum are in terms of a single variable

[Eric Wieser]

Oh, I guess your point is that using multilinear maps internally is overkill for a ring?

[Anatole Dedecker]

Yes but your « single variable » lives in a vector space over K, not in K, so it is indeed multivariable calculus

[Sebastien Gouezel]

Yes, using multilinear maps over a ring or a field is definitely overkill: you just have one coefficient, so instead of writing p_n (x, ..., x), you should just use a_n x^n. Of course, we should keep the definition of analytic_at (in the same way that differentiable_at is always expressed in terms of fderiv, whether in one or higher dimension), but we should be able to construct a function from a list of coefficients instead of a list of multilinear maps, for instance.

[Anatole Dedecker]

Vincent Beffara said:

I am having a similar experience trying to prove the isolated zeros theorem for analytic functions, that manipulating formal_multilinear_series explicitly (in my case, to extract a (z-z0)^n factor) is a little painful. src#exp_series is nice, but as far as I can tell the series provided from analytic_at for a function from C to C is not of that form so it does not really help...

Indeed I can imagine this to be a bit painful. The following should help you (maybe some of it is already in mathlib, feel free to PR the rest if you need it).

import analysis.analytic.basic
import ring_theory.power_series.basic

open_locale big_operators

variables {ι 𝕜 E F : Type*} [fintype ι] [decidable_eq ι]

lemma foo₁ [comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (f : multilinear_map 𝕜 (λ i : ι, 𝕜) E)
  (x : ι → 𝕜) : f x = (∏ i, x i) • (f 1) :=
begin
  rw ← multilinear_map.map_smul_univ,
  exact congr_arg f (funext $ λ i, by simp)
end

lemma foo₂ [comm_semiring 𝕜] (f : multilinear_map 𝕜 (λ i : ι, 𝕜) 𝕜)
  (x : ι → 𝕜) : f x = (f 1) * (∏ i, x i) :=
by rw [foo₁, smul_eq_mul, mul_comm]

lemma bar₁ [comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E]
  [topological_space 𝕜] [topological_space E]
  (f : continuous_multilinear_map 𝕜 (λ i : ι, 𝕜) E)
  (x : ι → 𝕜) : f x = (∏ i, x i) • (f 1) :=
foo₁ f.to_multilinear_map x

lemma bar₂ [comm_semiring 𝕜] [topological_space 𝕜]
  (f : continuous_multilinear_map 𝕜 (λ i : ι, 𝕜) 𝕜)
  (x : ι → 𝕜) : f x = (f 1) * (∏ i, x i) :=
foo₂ f.to_multilinear_map x

lemma sum₁ [comm_ring 𝕜] [add_comm_group E] [module 𝕜 E]
  [topological_space 𝕜] [topological_add_group 𝕜] [has_continuous_const_smul 𝕜 𝕜]
  [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E]
  (φ : formal_multilinear_series 𝕜 𝕜 E) (x : 𝕜) :
  φ.sum x = ∑' (n : ℕ), x^n • (φ n 1) :=
begin
  rw formal_multilinear_series.sum,
  congr,
  ext n,
  rw [bar₁, fin.prod_const]
end

lemma sum₂ [comm_ring 𝕜]
  [topological_space 𝕜] [topological_add_group 𝕜] [has_continuous_const_smul 𝕜 𝕜]
  (φ : formal_multilinear_series 𝕜 𝕜 𝕜) (x : 𝕜) :
  φ.sum x = ∑' (n : ℕ), (φ n 1) * x^n :=
begin
  rw formal_multilinear_series.sum,
  congr,
  ext n,
  rw [bar₂, fin.prod_const]
end

lemma partial_sum₁ [comm_ring 𝕜] [add_comm_group E] [module 𝕜 E]
  [topological_space 𝕜] [topological_add_group 𝕜] [has_continuous_const_smul 𝕜 𝕜]
  [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E]
  (φ : formal_multilinear_series 𝕜 𝕜 E) (x : 𝕜) (n : ℕ) :
  φ.partial_sum n x = ∑ k in finset.range n, x^k • (φ k 1) :=
begin
  rw formal_multilinear_series.partial_sum,
  congr,
  ext n,
  rw [bar₁, fin.prod_const]
end

lemma partial_sum₂ [comm_ring 𝕜]
  [topological_space 𝕜] [topological_add_group 𝕜] [has_continuous_const_smul 𝕜 𝕜]
  (φ : formal_multilinear_series 𝕜 𝕜 𝕜) (x : 𝕜) (n : ℕ) :
  φ.partial_sum n x = ∑ k in finset.range n, (φ k 1) * x^k :=
begin
  rw formal_multilinear_series.partial_sum,
  congr,
  ext n,
  rw [bar₂, fin.prod_const]
end

[Anatole Dedecker]

Oh, do we not have docs#continuous_multilinear_map.smul_right ?

[Eric Wieser]

What would smul_right be?

[Eric Wieser]

Ah, docs#multilinear_map.smul_right

[Anatole Dedecker]

Okay with that you can also add

lemma eq_mk_pi_algebra₁ [comm_ring 𝕜] [add_comm_group E] [module 𝕜 E]
  [topological_space 𝕜] [topological_add_group 𝕜] [has_continuous_mul 𝕜]
  [topological_space E] [topological_add_group E] [has_continuous_smul 𝕜 E]
  (φ : formal_multilinear_series 𝕜 𝕜 E) :
  φ = λ n, (continuous_multilinear_map.mk_pi_algebra 𝕜 (fin n) 𝕜).smul_right (φ n 1) :=
begin
  ext n x,
  rw [continuous_multilinear_map.smul_right_apply,
      continuous_multilinear_map.mk_pi_algebra_apply, bar₁]
end

lemma eq_mk_pi_algebra₂ [comm_ring 𝕜] [add_comm_group E] [module 𝕜 E]
  [topological_space 𝕜] [topological_add_group 𝕜] [has_continuous_mul 𝕜]
  (φ : formal_multilinear_series 𝕜 𝕜 𝕜) :
  φ = λ n, (φ n 1) • (continuous_multilinear_map.mk_pi_algebra 𝕜 (fin n) 𝕜) :=
begin
  ext n x,
  rw [continuous_multilinear_map.smul_apply,
      continuous_multilinear_map.mk_pi_algebra_apply, bar₂, smul_eq_mul]
end

Which means you don't have to make a lemma for each definition in the API of docs#formal_multilinear_series like I did for sum and partial_sum (unfortunately you need a little bit stronger assumptions, but I think it won't be a big deal in practice)

[Anatole Dedecker]

But anyway this is just a temporary fix, the good solution would definitely be to have a dedicated API for the one dimensional case

[Eric Wieser]

What's bar₁?

[Eric Wieser]

Also, would the continuous_multilinear_map version of docs#multilinear_map.pi_ring_equiv be helpful here?

[Vincent Beffara]

@Anatole Dedecker Thanks a lot! I ended up starting something similar (though in a more specific case, like this:

noncomputable def coef (p : formal_multilinear_series ℂ ℂ ℂ) (n : ℕ) : ℂ := p n (λ i, 1)

lemma to_coef {p : formal_multilinear_series ℂ ℂ ℂ} {n : ℕ} {y : ℂ} :
  p n (λ i, y) = (coef p n) * y^n := sorry

to go back and forth. I'll see what turns out...

[Anatole Dedecker]

Eric Wieser said:

Also, would the continuous_multilinear_map version of docs#multilinear_map.pi_ring_equiv be helpful here?

I don't know the exact setup Vincent is working with, but I thnik it would just be a longer way to write f 1 in this case, because I can't see how the fact that it's a linear isomorphism would help here

[Anatole Dedecker]

#14218 adds continuous_multilinear_map.smul_right

[Anatole Dedecker]

Anatole Dedecker said:

Eric Wieser said:

Also, would the continuous_multilinear_map version of docs#multilinear_map.pi_ring_equiv be helpful here?

I don't know the exact setup Vincent is working with, but I thnik it would just be a longer way to write f 1 in this case, because I can't see how the fact that it's a linear isomorphism would help here

That said it will certainly be useful when setting up the full one-dimensional theory

[Eric Wieser]

One thing that I should have done but didn't is generalized docs#map_exp to arbitrary single-variable series

[Kevin Wilson]

Hi y'all. Sorry for abandoning this at the time. Some family things came up and I never got around to working on it. However, I've used @Anatole Dedecker 's original suggestions and I got very far, until I hit a problem where Lean's not able to figure out what's going on with continuous_multilinear_map's op_norm? See here: https://gist.github.com/khwilson/42ab431f7c0f8eb397b4cc9f9a787440#file-example-lean-L166

[Kevin Wilson]

Specifically, I end up with this state:

  /-
  type mismatch at application
    (φ n).unit_le_op_norm
  term
    φ n
  has type
    continuous_multilinear_map ℂ (λ (i : fin n), ℂ) ℂ : Type
  but is expected to have type
    continuous_multilinear_map ?m_1 ?m_3 ?m_4 : Type (max ? ? ?)
  state:
  φ : formal_multilinear_series ℂ ℂ ℂ,
  r : nnreal,
  hr : ↑r < φ.radius,
  C : ℝ,
  hC : C > 0,
  hm : ∀ (n : ℕ), ∥φ n∥ * ↑r ^ n ≤ C,
  n : ℕ,
  hn : ∥pad φ n∥ * ↑r ^ n ≤ C * ↑r,
  this : n.succ = n + 1,
  this : C = 1 * C
  ⊢ ∥(↑n + 1)⁻¹∥ * (∥⇑(φ n) 1∥ * ↑r ^ n) ≤ 1 * C
  -/

[Kevin Wilson]

Any thoughts?

[Anatole Dedecker]

I will have a deeper look later, but often that means that you don’t have all the typeclass hypotheses to apply the lemma

[Jireh Loreaux]

This might be the type class inference problem for Π-types. I think I ran into this several months ago with formal_multilinear_series.

[Anatole Dedecker]

Yep that seems plausible

[Kevin Wilson]

Yeah, ∥φ n∥ is getting resolved to continuous_multilinear_map.has_op_norm' (note the ')

[Kevin Wilson]

I think I need to get rid of the ', but not exactly sure what yoga is necessary to do so

[Eric Wieser]

This is definitely the pi type problem

[Eric Wieser]

docs#continuous_multilinear_map.has_op_norm' is defeq to docs#continuous_multilinear_map.has_op_norm from what I remember, but lean really struggles to remember that during typeclass inference

[Eric Wieser]

Not using dot notation might help you there

[Kevin Buzzard]

Is the pi type problem fixed in lean 4?

[Eric Wieser]

The another natural fallback is to call the lemma with an @ so that all the ?m_1 metavariables are gone, which if it doesn't solve it will at least give a clearer error

[Eric Wieser]

Optimistically it's the same as the (fixed) dfinsupp problem you reported ages ago

[Yakov Pechersky]

Have have and `convert help you:

  have : ∥φ n 1∥ ≤ ∥φ n∥,
  { convert continuous_multilinear_map.unit_le_op_norm _ 1 _,
    { refl },
    { sorry, }   }, -- now needs help here

[Kevin Wilson]

Oh, well, I can fill that sorry in:

  have : ∥φ n 1∥ ≤ ∥φ n∥,
  { convert continuous_multilinear_map.unit_le_op_norm _ 1 _,
    { refl },
    { have : (1 : fin n → ℂ) = (λ i, 1), { ext, refl, refl, },
      rw this,
      simp [has_norm.norm],
      norm_cast,
      rw finset.sup_le_iff,
      intros b hb,
      exact rfl.le, } },

[Kevin Wilson]

"Unwrapping 1" and "Unwrapping 0" have been themes of this journey

[Yakov Pechersky]

@[simp] lemma norm_const_zero {ι M : Type*} [fintype ι] [nonempty ι] [normed_add_comm_group M] :
  ∥(0 : ι → M)∥ = 0 :=
by { convert pi_norm_const (0 : M), rw norm_zero, apply_instance }

@[simp] lemma norm_const_one {ι M : Type*} [fintype ι] [nonempty ι] [has_one M]
  [normed_add_comm_group M] [norm_one_class M] :
  ∥(1 : ι → M)∥ = 1 :=
by { convert pi_norm_const (1 : M), rw norm_one, apply_instance }

@[simp] lemma norm_is_empty {ι M : Type*} [is_empty ι] [normed_add_comm_group M] (f : ι → M) :
  ∥f∥ = 0 :=
by { rw subsingleton.elim f 0, refl }

lemma antideriv_radius_mono {r : nnreal}
  (hr : ↑r < φ.radius) : ↑r ≤ (pad φ).radius :=
begin
  obtain ⟨C, hC, hm⟩ := φ.norm_mul_pow_le_of_lt_radius hr,
  refine formal_multilinear_series.le_radius_of_bound _ (C * r) _,
  intros n,
  have key : ∥φ n 1∥ ≤ ∥φ n∥,
  { convert continuous_multilinear_map.unit_le_op_norm _ 1 _,
    { refl },
    { casesI is_empty_or_nonempty (fin n),
      sorry { convert zero_le_one,
        sorry; exact norm_is_empty _, -- this gets upset
        any_goals { apply_instance } },
      { exact norm_const_one.le } } },
  induction n with n hn,
  simp only [pad, norm_zero, zero_mul],
  refine mul_nonneg hC.lt.le nnreal.zero_le_coe,
  rw nat.succ_eq_add_one,
  dunfold pad,
  rw norm_smul,
  simp only [continuous_multilinear_map.norm_mk_pi_algebra_fin, mul_one],
  rw [pow_add (r : ℝ) n 1, ←mul_assoc, pow_one],
  refine mul_le_mul _ rfl.le nnreal.zero_le_coe hC.lt.le,
  rw [norm_mul, mul_assoc],
  -- refine (hm _).trans' _,
  -- have : C = 1 * C, simp,
  -- rw this,
  -- Something is going horribly wrong with `(φ n).unit_le_op_norm` here
  sorry,
end

[Yakov Pechersky]

Probably the helper lemmas can be weakened in the constraints on M

[Yakov Pechersky]

More helper:

@[simp] lemma norm_pi_one_le {ι : Type*} [fintype ι] (M : Type*) [has_one M]
  [normed_add_comm_group M] [norm_one_class M] :
  ∥(1 : ι → M)∥ ≤ 1 :=
begin
  casesI is_empty_or_nonempty ι,
  { convert zero_le_one,
    convert norm_is_empty M 1,
    any_goals { apply_instance } },
  { exact norm_const_one.le }
end

lemma antideriv_radius_mono {r : nnreal}
  (hr : ↑r < φ.radius) : ↑r ≤ (pad φ).radius :=
begin
  obtain ⟨C, hC, hm⟩ := φ.norm_mul_pow_le_of_lt_radius hr,
  refine formal_multilinear_series.le_radius_of_bound _ (C * r) _,
  intros n,
  have key : ∥φ n 1∥ ≤ ∥φ n∥,
  { convert continuous_multilinear_map.unit_le_op_norm _ 1 _,
    { refl },
    { exact norm_pi_one_le _ } },
  induction n with n hn,
  simp only [pad, norm_zero, zero_mul],
  refine mul_nonneg hC.lt.le nnreal.zero_le_coe,
  rw nat.succ_eq_add_one,
  dunfold pad,
  rw norm_smul,
  simp only [continuous_multilinear_map.norm_mk_pi_algebra_fin, mul_one],
  rw [pow_add (r : ℝ) n 1, ←mul_assoc, pow_one],
  refine mul_le_mul _ rfl.le nnreal.zero_le_coe hC.lt.le,
  rw [norm_mul, mul_assoc],
  -- refine (hm _).trans' _,
  -- have : C = 1 * C, simp,
  -- rw this,
  -- Something is going horribly wrong with `(φ n).unit_le_op_norm` here
  sorry,
end

[Eric Wieser]

Isn't that last lemma just docs#pi.norm_one_class? Or does that not exist? nevermind, it avoids needing nonemptiness

[Jireh Loreaux]

Here is the thread from when I encountered this problem before, in case it's helpful: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.E2.9C.94.20norm.20on.20continuous_multilinear_map/near/266226728. And @Kevin Buzzard , there you mentioned lean4#509, so I think it's fixed in Lean 4.

[Kevin Wilson]

Nice. With all this in hand, I actually proved the lemma. Will add all this into the ultimate golfing. Onward to antiderivatives on analytic functions for the moment :-)

[Kevin Wilson]

Well, it needs a lot of cleaning and I still need to clean up a few sorrys, but the proof I was going for is basically here if anyone has any obvious suggestions for golfing (especially all the casts between reals, nnreals, and ennreals): https://github.com/leanprover-community/mathlib/pull/15815/files#diff-67a2ee3fa94c037e80f0346fc77c70e3e64737c3b019e2a174d69143e4a7d72b

[Kevin Wilson]

(If you do take a look, note that _only_ that file is part of this commit. The others are in other PRs awaiting review.)

[Vincent Beffara]

Nice! For the case of holomorphic functions, an alternative strategy is to use the Cauchy integral formula (like in the proof that holomorphic functions are analytic) and the fact that it is preserved under uniform limits:

lemma weierstrass_1 {ι : Type*} {p : filter ι} [p.ne_bot] (hr : 0 < r) {F : ι → ℂ → ℂ}
  (F_cont : ∀ i, continuous_on (F i) (closed_ball c r))
  (F_holo : ∀ i, differentiable_on ℂ (F i) (ball c r))
  (F_conv : tendsto_uniformly_on F f p (closed_ball c r)) :
  differentiable_on ℂ f (ball c r) :=
begin
  let R := r.to_nnreal,

  have h1 : ∀ (i : ι) (w ∈ ball c r),
    (2 * ↑real.pi * I)⁻¹ • ∮ z in C(c, r), (z - w)⁻¹ • F i z = F i w,
    by { rintro n z hz,
      refine two_pi_I_inv_smul_circle_integral_sub_inv_smul_of_differentiable_on_off_countable
        countable_empty hz (F_cont n) (λ x hx, _),
      rw diff_empty at hx,
      exact (F_holo n).differentiable_at (is_open_ball.mem_nhds hx) },
  have h2 : eq_on (λ w, (2 * ↑real.pi * I)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z) f
      (emetric.ball c R),
    by { rintro w hw,
      replace hw : w ∈ ball c r := by { rw ← emetric_ball; simpa [hr.le] using hw },
      have h := λ n, h1 n w hw,
      suffices : tendsto (λ n, (2 * ↑real.pi * I)⁻¹ • ∮ z in C(c, r), (z - w)⁻¹ • F n z)
        p (𝓝 ((2 * ↑real.pi * I)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z)),
      from tendsto_nhds_unique this ((tendsto_congr h).mpr
        (F_conv.tendsto_at (ball_subset_closed_ball hw))),
      apply tendsto.const_smul,
      simp only [hr.le, real.coe_to_nnreal', max_eq_left],
      refine tendsto_uniformly_on.tendsto_circle_integral hr _ _,
      { intro n,
        refine continuous_on.smul _ ((F_cont n).mono sphere_subset_closed_ball),
        refine continuous_on.inv₀ (continuous_on_id.sub continuous_on_const) _,
        rintro z hz hzw,
        rw [← sub_eq_zero.mp hzw] at hw,
        exact set.disjoint_iff.mp sphere_disjoint_ball ⟨hz, hw⟩ },
      { rw [tendsto_uniformly_on_iff] at ⊢ F_conv,
        rintro ε hε,
        simp only [mem_ball] at hw,
        have hh1 : ε * (r - dist w c) > 0 := (mul_pos hε.lt (sub_pos.mpr hw)).gt,
        specialize F_conv (ε * (r - dist w c)) hh1,
        filter_upwards [F_conv] with n h z hz,
        specialize h z (sphere_subset_closed_ball hz),
        have hh2 : r - dist w c ≤ abs (z - w) :=
          by { simp only [mem_sphere_iff_norm, norm_eq_abs] at hz,
            simpa [hz, complex.dist_eq] using norm_sub_norm_le (z - c) (w - c) },
        rw [dist_smul],
        simp only [norm_eq_abs, complex.abs_inv],
        rw [inv_mul_lt_iff'],
        { apply lt_of_lt_of_le h,
          exact (mul_le_mul_left hε.lt).mpr hh2 },
        { linarith } } },
  have h3 : has_fpower_series_on_ball f (cauchy_power_series f c R) c R,
    by { refine (has_fpower_series_on_cauchy_integral _ (by simpa)).congr h2,
      have := (F_conv.continuous_on (eventually_of_forall F_cont)).mono sphere_subset_closed_ball,
      exact continuous_on.circle_integrable (by simp) (by simpa [hr.le]) },
  convert ← h3.differentiable_on; exact emetric_ball
end

How much do you think is needed in your approach to show that derivatives also converge locally uniformly?

[Kevin Wilson]

Oh, that is nice and avoids rehashing the mean value theorem a bunch of times.

[Kevin Wilson]

And, sorry, When you say "that derivatives also converge locally uniformly," I don't quite grok what you mean

[Kevin Wilson]

The one advantage of this method is that a lot of facts carry over to R, though I was mostly intending to just use this for C :-)

[Vincent Beffara]

Kevin Wilson said:

And, sorry, When you say "that derivatives also converge locally uniformly," I don't quite grok what you mean

I mean, if a sequence f n of analytic functions converges locally uniformly to g, then the sequence of derivatives also converges locally uniformly and its limit is the derivative of g (I learned this as "le théorème de Weierstrass" but have no clue what the standard name in English would be). It is a direct consequence of the Cauchy representation of the derivative, and can also probably be obtained following your proof; I was wondering which way would be less painful.

[Kevin Wilson]

Oh I see. Hmm, I think it's doable, but I'm not sure its relative difficulty to the Cauchy representation proof....

[Vincent Beffara]

Hi @Kevin Wilson, I was just wondering about the status of your uniform limits code. I would like to move forwards on the locally uniform convergence part of complex analysis, potentially add Hurwitz's theorem and things like that, so if you PR analyticity of locally uniform limits that would be great. I can always PR the Cauchy formula approach, but it will definitely not generalize...

[Bhavik Mehta]

(cc @Chris Birkbeck and #13500)

[Kevin Wilson]

Hey @Vincent Beffara all the uniform limits things are merged. I’ve not had time to push through the full Morera, but the shell is on GitHub as a WIP

[Kevin Wilson]

This was the status of where I got to: https://github.com/leanprover-community/mathlib/pull/15815

[Kevin Wilson]

basically Morera was done but your suggestion for the locally uniform convergence I think may be easier working directly with Cauchy