Constant functions are analytic

Stream: Is there code for X?

[Vincent Beffara]

This has to be in mathlib somewhere, but I couldn't find it:

def const_formal_multilinear_series (c : E) : formal_multilinear_series 𝕜 𝕜 E :=
λ n, dite (n = 0) (λ h, by { rw h; exact continuous_multilinear_map.curry0 _ _ c }) (λ _, 0)

lemma has_fpower_series_at_const {c : E} {z : 𝕜} :
  has_fpower_series_at (λ _, c) (const_formal_multilinear_series c) z :=
begin
  simp only [has_fpower_series_at_iff],
  refine eventually_of_forall (λ z, _),
  convert has_sum_single 0 _,
  { simp [const_formal_multilinear_series, formal_multilinear_series.coeff] },
  { rintro n hn,
    simp [const_formal_multilinear_series, formal_multilinear_series.coeff, hn] }
end

lemma analytic_at_const {c : E} {z : 𝕜} : analytic_at 𝕜 (λ _, c) z :=
⟨const_formal_multilinear_series c, has_fpower_series_at_const⟩

lemma analytic_on_const {c : E} : analytic_on 𝕜 (λ _, c) U :=
λ z _, analytic_at_const

Where should I look?

[Eric Rodriguez]

ctrl+f-ing analytic_on on all of mathlib doesn't inspire much hope for this existing

[Vincent Beffara]

I applied the same algorithm and failed too :-(

[Sebastien Gouezel]

Yes, it doesn't seem to be here!

[Anatole Dedecker]

Yes we don’t have this (see this comment)

[Vincent Beffara]

Hm, it was a comment on my own PR. I should have done what you asked :sweat_smile: