Tychonov's Counterexample for the Heat Equation

Stream: mathlib4

[Yongxi Lin (Aaron)]

Tychonov's counterexamples are nonzero solutions to the heat equation on $\mathbb{R}_+\times \mathbb{R}$ that satisfies the zero initial conditions. As an attempt to use Lean for PDEs, I have almost formalized that these counterexamples are solutions to the heat equation over here: https://github.com/CoolRmal/mathlib4/blob/c68bf629c0c3a2e5c5989b39d9bb6ca4e73667d8/Mathlib/tychonov_counterexample.lean (with help from ChatGPT, Aristotle, and people who participated in these posts: #Is there code for X? > Derivative of Holomorphic Functions, #Is there code for X? > Upper and Lower Bounds of Cosine , #Is there code for X? > Cauchy's integral formula). I decided to formalize this because these solutions are given by power series and we do have some tools about differentiating power series in Mathlib. I need some help for the remaining sorries:

1. The first sorry is about the local uniform convergence of the tail series:

import Mathlib

theorem HasSumLocallyUniformlyOn_iff_tailsumHasSumLocallyUniformlyOn
    (f : ℕ → ℝ → ℝ) (s : Set ℝ) (k : ℕ) :
    HasSumLocallyUniformlyOn f (fun b => ∑' (i : ℕ), f i b) s ↔
    HasSumLocallyUniformlyOn (fun n ↦ f (n + k)) (fun b => ∑' (i : ℕ), f (i + k) b) s := by
  sorry

I have also asked about this in this post: #Is there code for X? > Convergence of Series of Tail Sequence . I got stuck because local uniform convergence seems to be defined a little bit differently in Mathlib and I have some trouble using the existing results in Mathlib.

2. For the second sorry, I need an analogue of contDiff_tsum for local uniform convergence.

My code definitely needs some improvements and I think it can be shorten a lot by formalizing some more general theorems. Feel free to give me some advice!

[Yongxi Lin (Aaron)]

I also wish that eventually this goes to the Counterexample section in Mathlib4. Does anybody know how this works?

[Ruben Van de Velde]

Yongxi Lin (Aaron) said:

I also wish that eventually this goes to the Counterexample section in Mathlib4. Does anybody know how this works?

You make a pull request and hopefully someone reviews :)

[Michael Rothgang]

Every pull request to mathlib gets reviewed eventually. Some faster, some take a while longer.

[Patrick Massot]

And anything relying on AI formalization is bound to take a lot more time than the average PR, simply because of the code quality.

[Michael Rothgang]

I would put it differently: your code gets reviewed much faster if you clean it up before making a PR. (And, of course, if you learn something during review, you apply it to the remaining code in your project also.)

[Michael Rothgang]

I would like your result to get in, but my review time is also limited. Can we make a deal? You do your very best to clean up your code, by hand, using all the Lean knowledge you know, and then I'll take a look promptly at your first PR?

[Michael Rothgang]

Indeed, finding the correct generality for your results is a very good first step. Please do that first (and if this raises questions you'd like input on, you can ask on zulip).

[Yongxi Lin (Aaron)]

Thank you Michael for your help. Most of my code is done by hand as AI is not that powerful...I will try my best to clean up my code before I make a PR.