New Smooth Take-Off planet

[WenrongZou]

• depends on new planet Slope #151
• depends on New planet Cartan to introduce Filter #156

[TentativeConvert]

Overall structure with Boss = (derivative computation) and final level = (main statement as easy corollary) looks good to me. Still has a number of tactics that we haven't introduced in the game (like refine and convert). You could introduce these, but that would require additional levels for practising these tactics. So it might be easier to try to find alternative proofs that avoid them.

[WenrongZou]

I think refine and convert only exist in the Branch of the proof, where I use them to record the mathlib proof. In the main branch of the proof, I have already avoided to use these two tactics.

[TentativeConvert]

I think refine and convert only exist in the Branch of the proof, where I use them to record the mathlib proof. In the main branch of the proof, I have already avoided to use these two tactics.

Indeed. Sorry I didn't notice this.

[WenrongZou]

Yes, you're right. By the way, I think we could also introduce the variant syntax of obtain:

obtain ⟨x, hx⟩ : ∃ x, p x := proof 

Here proof can be either a proof term or a tactic proof.

[WenrongZou]

On simp_rw: it's useful whenever we need to rw repeatedly, or when we need to rewrite under a binder, where plain rw fails or simply can't see the term. That second case is exactly why it's needed on this planet: the rewrites happen under the binder inside Tendsto (i.e. inside the fun x => …).

[TentativeConvert]

Yes, you're right. By the way, I think we could also introduce the variant syntax of obtain:

obtain ⟨x, hx⟩ : ∃ x, p x := proof 

Ah, right, I see your point about obtain now. We do actually have "term style" proofs in the game, secretly, which we use in a very rudimentary form with the obtain tactic. In fact, have and obtain have similar syntax, and so far we've only introduced have the syntax for each of them. That does not seem natural. Thanks for pointing this out!

[TentativeConvert]

Just for the moment, please don't push any further commits here while I'm reviewing the next levels.

[TentativeConvert]

I'm still playing around with how the derivatives are computed. This all culminates in the last third of L08.

The syntax HasDerivAt f f' x annoying in that you cannot really do „calculations“ with it. The docs mention

deriv f x

as a functional alternative, but I guess working with this we would need to make additional statements that f is actually differentiable, which in this world is the whole point.

[TentativeConvert]

Anyway, here's a more constructive idea. I came up with a variant for computation in L08. Starting from the proof state

p : ℝ[X]
x : ℝ
hx : 0 < x
hf : f x = rexp (-x⁻¹)
⊢ HasDerivAt (fun (y : ℝ) ↦ eval y⁻¹ p * rexp (-y⁻¹)) (eval x⁻¹ (X ^ 2 * (p - derivative p)) * f x) x

I do:

have h_comp : (fun (y : ℝ) ↦ eval y⁻¹ p * Real.exp (-y⁻¹)) = (fun y ↦ p.eval y * Real.exp (-y)) ∘ Inv.inv := by
  rfl    
rw [h_comp]
clear h_comp
have h₁ := p.hasDerivAt x⁻¹
have h_neg := hasDerivAt_neg x⁻¹
have h₂ := HasDerivAt.exp h_neg
have h_mul := HasDerivAt.mul h₁ h₂
have h₃ := hasDerivAt_inv (x := x) (by grind)  -- or hasDerivAt_inv hx.ne.symm
have h_comp := HasDerivAt.comp x h_mul h₃
convert! h_comp using 1
simp [hf]
ring

The advantage is that I don't need to write out a single derivative by hand. I only need to write out in full how I want to view the function as a composition, but that part follows the current solution. All the computations are done for me.

The disadvantage is that I need this new tactic convert, which I'm not experienced with, and which I only got to do the right thing with a lot of trial and error. The ! appears to be mandatory, and so does using 1. Not nice syntax …

What's your take on this?

[TentativeConvert]

The syntax HasDerivAt f f' x annoying in that you cannot really do „calculations“ with it. The docs mention deriv f x as a functional alternative, but I guess working with this we would need to make additional statements that f is actually differentiable, which in this world is the whole point.

Actually, the final levels do use the functional version of the derivative, and its iterated generalization. My reading is that, as it stands, the final result iteratedDeriv n f 0 = 0 is not mathematically meaningful because it might simply mean that the n-th interated derivative does not exist.

[WenrongZou]

Suggested change

	convert! h_comp using 1
	simp [hf]
	ring
	convert h_comp using 1
	· rfl
	· rfl
	· simp [hf]
	ring

We can close the goal without !, but there will be two more subgoals. Plain convert only tries rfl at reducible transparency, meaning it will only unfold definitions marked @[reducible]. convert! uses default transparency, so it can also unfold ordinary definitions and instances. Therefore, it closed the first two subgoals when using convert h_comp using 1.

I'm not against introducing convert in the game. I think it's a useful tactic, and it can simplify some of the derivative computations. In practice, we could encourage players to try convert! first: it produces the same goals as convert but closes more of the trivial ones automatically, so it usually just works. I'm happy to discuss where we could introduce it.

[TentativeConvert]

We need to solve the other issue first (deriv & iteratedDeriv versus HasDerivAt). Do you have an idea for how to fix the planet so that we have a mathematically meaningful result at the end? Once it's fixed, we need to analyse whether it pays off to keep HasDerivAt, or whether we can switch to deriv. If we switch to deriv, then we probably won't need convert. If we need to keep HasDerivAt, then yes, I would vote to introduce convert.

[WenrongZou]

Right. If we use deriv then we need to introduce DifferentiableAt, which "equals" to HasDerivAt.

[WenrongZou]

The reason we need DifferentiableAt is that we need this for derivative calculations. For example, deriv_mul.

[WenrongZou]

Ah, I got your point. We can rephrase L08 via deriv as follows:

example (p : ℝ[X]) (x : ℝ) (hx : 0 < x) :
  deriv (fun x ↦ p.eval x⁻¹ * f x) x =
      ((X ^ 2 * (p - derivative p)).eval x⁻¹ * f x) := by
  have hf : f x = rexp (-x⁻¹) := by
    unfold f
    rw [if_neg]
    grind
  have hev : f =ᶠ[𝓝 x] fun y ↦ rexp (-y⁻¹) := by
    filter_upwards [eventually_gt_nhds hx] with y hy
    unfold f
    rw [if_neg]
    grind
  rw [deriv_fun_mul]
  · rw [hev.deriv_eq]
    rw [show (fun y ↦ p.eval y⁻¹) = (fun y ↦ p.eval y) ∘ Inv.inv from rfl,
      deriv_comp x p.differentiableAt (differentiableAt_inv hx.ne')]
    have hn : DifferentiableAt ℝ (fun y : ℝ ↦ -y⁻¹) x := (differentiableAt_inv hx.ne').neg
    rw [deriv_exp hn, deriv.fun_neg, Polynomial.deriv, deriv_inv, hf]
    simp
    ring
  · exact p.differentiableAt.comp x (differentiableAt_inv hx.ne')
  · rw [hev.differentiableAt_iff]
    exact (differentiableAt_inv hx.ne').neg.exp

Please excuse the rough proof. I had Claude put together a quick one to see how far deriv can take the calculation. It seems to simplify the derivative computations quite a bit! :)

[TentativeConvert]

That would certainly be the cleanest solution, if its doable.

[WenrongZou]

Yes, it is doable. The solution only contains 6 lines of code. However, this requires our original design in L08 (HasDerivAt version).

Statement : ContDiff ℝ ∞ f := by
  apply contDiff_of_differentiable_iteratedDeriv
  intro m _
  rw [iteratedDeriv_eq_poly]
  intro x
  apply HasDerivAt.differentiableAt
  apply hasDerivAt_polynomial_eval_inv_mul

[TentativeConvert]

OK, then I guess we should keep HasDerivAt, but introduce convert. Feel free to start work on this; I'll ping you before I start editing here again.

[WenrongZou]

Thanks! I will do it.

[WenrongZou]

I resolved our previous discussion. While I was rewriting the third case in current level 8, I came up an alternative proof using DifferentiableAt.hasDerivAt, which I recorded in a branch.

[TentativeConvert]

Thanks for the update! I'm just making some last adjustments now.

[TentativeConvert]

I'm tending now towards calling this planet "Cauchy". I wasn't previously aware of this, but it turns out that essentially this example was one of Cauchy's motivations to work out his theory of derivatives. See the first page of this preprint:

However, Cauchy was already becoming aware of the limitations of these techniques. He was aware
of examples such as $e^{−1/x^2}$ where the Taylor series at the origin does not reproduce the function […].

And here's a primary source: Cauchy mentions this example in his Résumé des leçons données à l'École royale polytechnique sur le calcul infinitésimal, see the last paragraph of the printed page 152:

On pourrait croire que la série (6) a toujours F(x) pour somme, quand elle est convergente, et que, dans le cas où ses différens termes s'évanouissent l'un après l'autre, la fonction F(x) s'évanouit elle-même. Mais, pour s'assurer du contraire, il suffit d'observer que la seconde condition sera remplie, si l'on suppose F(x) = e^(−(1/x)²) …

[TentativeConvert]

In the story, I think Cauchy will be a fierce dragon living in an egg. The formalosophers living on the egg don't want the egg to crack and the dragon to come out. So our heroes need to land and take off very, very softly …