QM reflectionless potential

Stream: PhysLean

[Afiq Hatta]

Hey folks I'm starting to work on the reflectionless potential just to get myself acquianted with lean

[Afiq Hatta]

@Joseph Tooby-Smith

[Joseph Tooby-Smith]

Just for some context Afiq and I have being discussing this 'offline', so this is a place to discuss things related to the QM reflectionless potential in the open.

[Afiq Hatta]

hey @Joseph Tooby-Smith was just thinking of an easy next step - i'm guessing defining the creation and annihilation operators in the paper?

[Joseph Tooby-Smith]

Yes, this seems like a good next step to me, that or writing down the full Hamiltonian as a operator on ordinary functions

[Afiq Hatta]

@Joseph Tooby-Smith we can discuss this on the call later but I need to use the position and momentum operators, for the creation / annihilation stuff - I guess those are good to import from the Operators module?

[Joseph Tooby-Smith]

Yep, it is best to import them from the operators module, if you need any properties of them which aren't yet proven, these should go into the operators module.

[Afiq Hatta]

awesomesauce

[Afiq Hatta]

pull request made

[Afiq Hatta]

i guess the next dumb thing to do would be to prove creation operator is conjugate to the annihilation one!

[Joseph Tooby-Smith]

This might be tricky, but it is certainly doable. It is tricky because by conjugate here you really mean hermitian conjugate (if you don't then it's not true anyway).
The way your operators are currently defined, they are defined on the normal functions from ℝ → ℂ, but to define their hermitian conjugate you need them defined on the Hilbert space (at least part of the Hilbert space).
An example of this type of thing is done in the momentumOperator file, see e.g. the lemma

momentumOperatorUnbounded_isSelfAdjoint

In particular, in addition to creationOperator you should also define creationOperatorSchwartz and creationOperatorUnbounded copying what is in the momentum operator module.

[Afiq Hatta]

agreed to all - will get cracking

[Afiq Hatta]

To do:

• do the Schwartz Space operator versions

[Afiq Hatta]

so @Joseph Tooby-Smith to even create these Schwartz versions of creation and annihilation operators, we need to prove that they're linear right?

[Afiq Hatta]

ie what you did here:

/-- The parity operator on the Schwartz maps is defined as the linear map from
  `𝓢(ℝ, ℂ)` to itself, such that `ψ` is taken to `fun x => - I ℏ * ψ' x`. -/
def momentumOperatorSchwartz : 𝓢(ℝ, ℂ) →L[ℂ] 𝓢(ℝ, ℂ) where
  toFun ψ := (- Complex.I * ℏ) • SchwartzMap.derivCLM ℂ ψ
  map_add' ψ1 ψ2 := by
    simp only [neg_mul, map_add, smul_add, neg_smul]
  map_smul' a ψ := by
    simp only [neg_mul, map_smul, neg_smul, RingHom.id_apply]
    rw [smul_comm]
    simp
  cont := by fun_prop

[Afiq Hatta]

in the case of the creation and annihilation operators, would the cleanest way be to prove that the tanh operator is Schwartz, and then since their linear combinations of the tanh operator and the momentum operator => creation and annihilation operators are aalso schwartz

[Joseph Tooby-Smith]

Afiq Hatta said:

so Joseph Tooby-Smith to even create these Schwartz versions of creation and annihilation operators, we need to prove that they're linear right?

Yes, exactly, the →L[ℂ] is the notation for a continuous linear map.

[Joseph Tooby-Smith]

Afiq Hatta said:

in the case of the creation and annihilation operators, would the cleanest way be to prove that the tanh operator is Schwartz, and then since their linear combinations of the tanh operator and the momentum operator => creation and annihilation operators are aalso schwartz

Yep that sounds like the best way to me.

[Afiq Hatta]

really dumb question

I know what is required for a continuous linear map, but how in general can i find the 'requirements' needed to define a particular structure?

is it the 'fields' section of what i get when i type ```
#print ContinuousLinearMap

structure ContinuousLinearMap.{u_1, u_2, u_3, u_4} {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (σ : R →+* S)
  (M : Type u_3) [TopologicalSpace M] [AddCommMonoid M] (M₂ : Type u_4) [TopologicalSpace M₂] [AddCommMonoid M₂]
  [Module R M] [Module S M₂] : Type (max u_3 u_4)
number of parameters: 13
parents:
  ContinuousLinearMap.toLinearMap : M →ₛₗ[σ] M₂
fields:
  AddHom.toFun : M → M₂
  AddHom.map_add' : ∀ (x y : M), (↑self).toFun (x + y) = (↑self).toFun x + (↑self).toFun y
  MulActionHom.map_smul' : ∀ (m : R) (x : M), (↑self).toFun (m • x) = σ m • (↑self).toFun x
  ContinuousLinearMap.cont : Continuous (↑self).toFun := by
    continuity
constructor:
  ContinuousLinearMap.mk.{u_1, u_2, u_3, u_4} {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {σ : R →+* S}
    {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] {M₂ : Type u_4} [TopologicalSpace M₂] [AddCommMonoid M₂]
    [Module R M] [Module S M₂] (toLinearMap : M →ₛₗ[σ] M₂) (cont : Continuous toLinearMap.toFun := by continuity) :
    M →SL[σ] M₂
field notation resolution order:
  ContinuousLinearMap, LinearMap, AddHom, MulActionHom

[Joseph Tooby-Smith]

The way I do it is just start typing the definition, e.g.

def momentumOperatorSchwartz : 𝓢(ℝ, ℂ) →L[ℂ] 𝓢(ℝ, ℂ) where

This will then give an error on the where because things are incomplete, and the error will list the fields needed.

[Afiq Hatta]

got it - thanks Joe for the flag

[Afiq Hatta]

really dumb question @Joseph Tooby-Smith but i can't get this to work - just even the definition part

noncomputable def tanhOperatorSchwartz : 𝓢(ℝ, ℂ) →L[ℂ] 𝓢(ℝ, ℂ) where
  toFun ψ := (fun x ↦ (Real.tanh (Q.κ * x) : ℂ) * ψ x)

I am getting this error
type mismatch
fun x => ↑(tanh (Q.κ * x)) * ψ x
has type
ℝ → ℂ : Type
but is expected to have type
𝓢(ℝ, ℂ) : Type

[Afiq Hatta]

I don't see anything wrong with the definition itself - where am I falling over?

[Afiq Hatta]

am i not 'casting' the function correctly here?

[Kenny Lau]

@Afiq Hatta you're misinterpreting what toFun means

[Kenny Lau]

toFun requires you to make a function 𝓢(ℝ, ℂ) -> 𝓢(ℝ, ℂ) first

[Kenny Lau]

and prove that this function is linear and continuous

[Kenny Lau]

it does not mean, first make a function 𝓢(ℝ, ℂ) -> (ℝ -> ℂ), and prove that every result is Schwarz

[Kenny Lau]

in other words, you need two layers of toFun here

[Afiq Hatta]

ahhh i hear you - i need to first prove that pointwise multiplication by tanh ( x ) is itself - 𝓢(ℝ, ℂ) -> 𝓢(ℝ, ℂ) (by boundedness, continuity) ? @Kenny Lau

[Afiq Hatta]

apologies - beginner here!! :p

[Afiq Hatta]

if thats the case - then there should be an inductive proof that all derivatives of (tanh (x) psi (x) ) don't blow up - i don't think theres a general result that we can apply here from other places in the library?

[Kenny Lau]

what's the maths proof?

[Afiq Hatta]

writing it down now...

[Kenny Lau]

I feel like it should follow from tanh(x) itself being Schwartz?

[Afiq Hatta]

its not though right, since -> +- 1 at +- infty?

[Kenny Lau]

oh...

[Kenny Lau]

well, it should then follow from tanh(x) being bounded and its derivatives vanishing

[Afiq Hatta]

yeah - actually thats the best way - but trying to see if there's already a ready made proof here on that result

[Afiq Hatta]

Just breaking this down - need to prove the lemma that tanh (x) has bounded derivatives

[Afiq Hatta]

can you guys tell im an absolute noob.. hahaha

[Joseph Tooby-Smith]

Sorry, jumping into this conversation half way through: Something like

• this

might be useful here, all though I think it would need generalizing.

[Kenny Lau]

wow you've added a lot of lemmas, nice

[Joseph Tooby-Smith]

Yeah, they are all probably not as general as they could be - but I did a start :).

[Afiq Hatta]

keen to talk about this tomorrow!

[Afiq Hatta]

an excuritatingly dumb question which I've spent too much time on

I want to prove | tanh x | < 1
ok, so start with
lemma : tanh x < 1
there's an equality rewrite so that the goal transforms to

sinh x / cosh x < 1

but i can't for the life of me find the right package / technique that transforms this to
sinh x < cosh x

there's a preset theorem already in mathlib for sinh x < cosh x, so I just need to do the above
@Joseph Tooby-Smith

[Kenny Lau]

https://loogle.lean-lang.org/?q=_+%2F+_+<+1

[Afiq Hatta]

thanks kenny, sorry for being an idiot, still getting used to searching for things

[Afiq Hatta]

ah wait - those are for the natural numbers

[Kenny Lau]

well, not the first one

[Kenny Lau]

the 6th one should be what you need

[Afiq Hatta]

this is where im falling over the syntax a bit

[Afiq Hatta]

lemma tanh_le_one (x : ℝ) : Real.tanh x < 1 := by
  rw [Real.tanh_eq_sinh_div_cosh]
  apply div_lt_one

[Afiq Hatta]

Expected type
x : ℝ
⊢ ∀ {α : Type ?u.1166} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α}, 0 < b → (a / b < 1 ↔ a < b)

Messages (1)

Basic.lean:68:2

tactic 'apply' failed, could not unify the conclusion of @div_lt_one
?a / ?b < 1 ↔ ?a < ?b
with the goal
sinh x / cosh x < 1
Note: The full type of @div_lt_one is
∀ {α : Type ?u.1166} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α},
0 < b → (a / b < 1 ↔ a < b)
x : ℝ
⊢ sinh x / cosh x < 1

All Messages (1)

[Kenny Lau]

it's not an apply, it's a rw

[Afiq Hatta]

got it - this creates a subgoal where now i need to prove 0 < cosh x as expected, and then sinh x < cosh x

[Afiq Hatta]

thanks kenny

[Afiq Hatta]

woohoo!!

lemma tanh_le_one (x : ℝ) : Real.tanh x < 1 := by
  rw [Real.tanh_eq_sinh_div_cosh]
  rw [div_lt_one]
  apply Real.sinh_lt_cosh
  apply Real.cosh_pos

[Kenny Lau]

@Afiq Hatta rw rewrites an iff, apply is for applying P -> Q to a goal Q to get a goal P

[Afiq Hatta]

got it, and rw also works for equalities too right

[Kenny Lau]

yes

[Afiq Hatta]

one thing im finding hard is that i often want to apply results on the reals,
but most of the theorems that i get from loogle / searching mathlib or defined on like rings / fields / monoids (?!!)

[Afiq Hatta]

so i have to do the mental gymnastics to remember what's what

[Kenny Lau]

you can try to separate it out into a clean environment (i.e. example) and then use apply?:

import Mathlib

example (x y : ℝ) : x / y < 1 ↔ x < y := by
  apply?

[Afiq Hatta]

@Joseph Tooby-Smith in the process of linting:
https://github.com/HEPLean/PhysLean/pull/694/files

[Joseph Tooby-Smith]

Going back to the problem of showing that

fun x => tanh (x) * ψ(x)

is Schwartz if ψ is, I think the general version of this result is docs#SchwartzMap.bilinLeftCLM with the bilinear map B : ℝ →L[ℝ] ℝ →L[ℝ] ℝ taking x, y to x * y, and with g(x) = tanh(x). Thus to prove this result 'all' one would need to do is prove that Function.HasTemperateGrowth Real.tanh, which is essentially what you are trying to show anyway @Afiq Hatta .

[Afiq Hatta]

ooooh

[Afiq Hatta]

yeah good point - lets use that - thats perfect±

[Afiq Hatta]

btw @Joseph Tooby-Smith linters passed on last commit

[Joseph Tooby-Smith]

Yeah,

Afiq Hatta said:

yeah good point - lets use that - thats perfect±

Yeah - still need to show that tanh has bounded iterated derivatives for this, but it takes care of the 'SchwartzMap' side of the problem for you, and reduces it to a properties of 'tanh' problem.

[Afiq Hatta]

yeah exactly, we don't have to do the leg work of the closure stuff since we cn just use this. but still, need to prove that we have bounded iterated derivs

[Afiq Hatta]

@Joseph Tooby-Smith the mission here is to prove temperate growth, as a warm up going to commit these that i just did

/-
Copyright (c) 2025 Afiq Hatta. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Afiq Hatta
-/
import Mathlib.Analysis.Calculus.IteratedDeriv.Defs
import Mathlib.Data.Complex.Trigonometric
import PhysLean.Meta.Linters.Sorry

/-!
# Properties of Tanh
We want to prove that the reflectionless potential is a Schwartz map.
This means proving that pointwise multiplication of a Schwartz map with tanh is a Schwartz map.
This means we need to prove that all derivatives of tanh are bounded and continuous, so that
the nth derivative of a function multiplied by tanh decays faster than any polynomial.

## TODO
- Add these to mathlib eventually
- Fill in the proofs for the properties of tanh
-/

open Real
open NNReal
open Field


/-- tanh(x) is less than 1 for all x -/
lemma tanh_lt_one (x : ℝ) : Real.tanh x < 1 := by
  rw [Real.tanh_eq_sinh_div_cosh]
  rw [div_lt_one]
  apply Real.sinh_lt_cosh
  apply Real.cosh_pos

/-- tanh(x) is greater than -1 for all x -/
lemma minus_one_lt_tanh (x : ℝ) : -1 < Real.tanh x := by
  rw [Real.tanh_eq_sinh_div_cosh]
  rw [lt_div_iff₀]
  rw [← sub_pos]
  rw [neg_one_mul]
  simp
  apply Real.exp_pos
  apply Real.cosh_pos

/-- The absolute value of tanh is bounded by 1 -/
lemma abs_tanh_lt_one (x: ℝ) : |Real.tanh x| < 1 := by
  rw [abs_lt]
  constructor
  apply minus_one_lt_tanh
  apply tanh_lt_one

[Joseph Tooby-Smith]

Sounds good! I would maybe update the module doc-string with a comment about docs#SchwartzMap.bilinLeftCLM as well. Also, this is not necessary but it maybe good to know, you can combine rewrites e.g.

lemma minus_one_lt_tanh (x : ℝ) : -1 < Real.tanh x := by
  rw [Real.tanh_eq_sinh_div_cosh, lt_div_iff₀, ← sub_pos, neg_one_mul]
  simp
  apply Real.exp_pos
  apply Real.cosh_pos

[ZhiKai Pong]

Not the most experienced user here but some minor style comments:

1. if you opened namespace Real, you don't have to type Real.xxx
2. The cosh_pos goal arises as a result of using lemmas related to division by cosh, since it's an additional condition associated with the division lemma rather than part of the main proof personally I'd just inline it
3. I prefer using exact to close goals which indicates more clearly where the proof ends
4. if the proof itself does require multiple goals use centerdot (\.) to structure the proof for better clarity (e.g. after constructor).

for example, this is how I'd write your code:

import Mathlib

open Real

lemma tanh_lt_one (x : ℝ) : tanh x < 1 := by
  rw [tanh_eq_sinh_div_cosh, div_lt_one (cosh_pos x)]
  exact sinh_lt_cosh x

lemma minus_one_lt_tanh (x : ℝ) : -1 < tanh x := by
  rw [tanh_eq_sinh_div_cosh, lt_div_iff₀ (cosh_pos x), ← sub_pos, neg_one_mul]
  simp [exp_pos x]

lemma abs_tanh_lt_one (x : ℝ) : |tanh x| < 1 := by
  rw [abs_lt]
  constructor
  · exact minus_one_lt_tanh x
  · exact tanh_lt_one x

[Afiq Hatta]

this is great @Joseph Tooby-Smith @ZhiKai Pong thank you for the tips

[ZhiKai Pong]

(I guess you can also do this once you're more comfortable)

lemma abs_tanh_lt_one (x : ℝ) : |tanh x| < 1 := by
  rw [abs_lt]
  exact ⟨minus_one_lt_tanh x, tanh_lt_one x⟩

[Joseph Tooby-Smith]

Aside concerning the center dots: there is this open issue which I attempted to do complete here, but one thing or another got in the way

[Afiq Hatta]

guys i have a mega dumb question

/-- Tanh(x) is n times continuously differentiable for all n -/
lemma contDiff_tanh {n : ℕ} : ContDiff ℝ n tanh := by
  have hdiv : ContDiff ℝ n (fun x => Real.sinh x / Real.cosh x) := by
    apply ContDiff.div
    · exact contDiff_sinh
    · exact contDiff_cosh
    · intro x
      exact ne_of_gt (Real.cosh_pos x)

  simpa [tanh_eq_sinh_div_cosh] using hdiv

the last line is throwing error -

type mismatch, term
hdiv
after simplification has type
ContDiff ℝ ↑n fun x => sinh x / cosh x : Prop
but is expected to have type
ContDiff ℝ (↑n) tanh : Prop

what is the syntax to use the tanh = sinh / coosh to finally prove this thing?

[Afiq Hatta]

rewriting the goal with rw [ tanh_eq_sinh_div_cosh] doesn't work

[ZhiKai Pong]

here's a possible solution (there might be an easier way) (also I'm surprised this isn't in Mathlib)

import Mathlib

open Real

/-- Tanh(x) is n times continuously differentiable for all n -/
lemma contDiff_tanh {n : ℕ} : ContDiff ℝ n tanh := by
  have hdiv : ContDiff ℝ n (fun x => sinh x / cosh x) := by
    apply ContDiff.div
    · exact contDiff_sinh
    · exact contDiff_cosh
    · intro x
      exact ne_of_gt (cosh_pos x)
  conv =>
    enter [3, x]
    rw [tanh_eq_sinh_div_cosh]
  exact hdiv

[ZhiKai Pong]

there are two layers of issue here:

1. rw can't see through what's inside ContDiff
2. tanh_eq_sinh_div_cosh has to be of the form tanh x = sinh x / cosh x, so you have to give it an x. Not sure if you're familiar with ext, the enter is just doing that in a similar fashion

[Afiq Hatta]

ah - yeah i wanted to figure out how to do the replacement of tanh within ContDiff

[Afiq Hatta]

thank you for this

[ZhiKai Pong]

No worries!

[Afiq Hatta]

btw i couldn't find this in mathlib - do you agree it's not there? still trying to build my searching skills

[ZhiKai Pong]

(sorry first time trying to do this in zulip)

[ZhiKai Pong]

@loogle tanh

[loogle]

:exclamation: unknown identifier 'tanh'
Did you mean "tanh", Float.tanh, or something else?

[ZhiKai Pong]

@loogle Real.tanh

[loogle]

:search: Real.tanh, Complex.ofReal_tanh, and 7 more

[ZhiKai Pong]

@loogle Real.sinh

[loogle]

:search: Real.sinh, Real.sinh_lt_cosh, and 117 more

[ZhiKai Pong]

It's quite clear that a lot is missing for tanh :)

[ZhiKai Pong]

(this is https://loogle.lean-lang.org/)

[Afiq Hatta]

yeah - reflectionless potential sidequests to the rescue!! XD

[Afiq Hatta]

@Joseph Tooby-Smith i submitted a pull request but no rush - its fridayyy night!!!

[Joseph Tooby-Smith]

Ha - no worries, was literally doing it as I got this message :)

[Afiq Hatta]

@Joseph Tooby-Smith to prove the derivative of tanh x - will using the identity below make this a bit easier, then using the chain rule on this - or will there be shenanigans with Real / Complex

theorem tanh_mul_I : tanh (x * I) = tan x * I := by
rw [tanh_eq_sinh_div_cosh, cosh_mul_I, sinh_mul_I, mul_div_right_comm, tan]

[Joseph Tooby-Smith]

This might work, it really depends on how good the API is around real to complex numbers - if I recall it is quite good.

[Afiq Hatta]

@Joseph Tooby-Smith really DUMB q i cant seem to rewrite the goal here so that i can use my h result

/-- The derivative of tanh(x) is 1 - tanh(x)^2 -/
lemma deriv_tanh (x: ℝ) : deriv Real.tanh = fun x => 1 - Real.tanh x ^ 2 := by
  have h: deriv (sinh / cosh) x = 1 - Real.tanh x ^ 2 := by
    rw [deriv_div, Real.deriv_sinh, Real.deriv_cosh]
    field_simp
    rw [sq, sq, tanh_eq_sinh_div_cosh, mul_sub_right_distrib]
    field_simp
    · apply Real.differentiable_sinh
    · apply Real.differentiable_cosh
    · exact ne_of_gt (Real.cosh_pos x)

tanh_eq_sinh_div_cosh is the result tanh x = sinh x / cosh x

using funext x i think rewrites that goal as (deriv Real.tanh) x , so the pesky symbols aren't in the right place

[Afiq Hatta]

i have this

unsolved goals
x : ℝ
h : deriv (sinh / cosh) x = 1 - tanh x ^ 2
⊢ deriv tanh = fun x => 1 - tanh x ^ 2

[Afiq Hatta]

i could make a functional version of

tanh_eq_sinh_div_cosh such that tanh = sinh / cosh, and then change the form of h to make it "functional" but i m not sure how to do that

[Afiq Hatta]

(deleted)

[Joseph Tooby-Smith]

try funext x :)

[Afiq Hatta]

OH WAIT I GOT IT i think

[Afiq Hatta]

i think i answered my own question by asking it hah

[Afiq Hatta]

boom

/-- The derivative of tanh(x) is 1 - tanh(x)^2 -/
lemma deriv_tanh : deriv Real.tanh = fun x => 1 - Real.tanh x ^ 2 := by
  have h: deriv (sinh / cosh) = fun x => 1 - Real.tanh x ^ 2 := by
    funext x
    rw [deriv_div, Real.deriv_sinh, Real.deriv_cosh]
    field_simp
    rw [sq, sq, tanh_eq_sinh_div_cosh, mul_sub_right_distrib]
    field_simp
    · apply Real.differentiable_sinh
    · apply Real.differentiable_cosh
    · exact ne_of_gt (Real.cosh_pos x)
  have h': Real.tanh = (sinh / cosh) := by
    funext x
    rw [Pi.div_apply, tanh_eq_sinh_div_cosh]
  nth_rewrite 1 [h']
  apply h

[Afiq Hatta]

one big leap for tanh

[Afiq Hatta]

okay will commit this

[Joseph Tooby-Smith]

Nice, congrats! :grinning:

[Joseph Tooby-Smith]

So I don't have an explanation for this, other then 'field_simp' is an awesome tactic, but your proof of h can be golfed to:

import Mathlib
open Real
/-- The derivative of tanh(x) is 1 - tanh(x)^2 -/
lemma deriv_tanh : deriv Real.tanh = fun x => 1 - Real.tanh x ^ 2 := by
  have h: deriv (sinh / cosh) = fun x => 1 - Real.tanh x ^ 2 := by
    funext x
    field_simp [deriv_div, Real.deriv_sinh, Real.deriv_cosh, sq,
       tanh_eq_sinh_div_cosh, mul_sub_right_distrib]
  have h': Real.tanh = (sinh / cosh) := by
    funext x
    rw [Pi.div_apply, tanh_eq_sinh_div_cosh]
  nth_rewrite 1 [h']
  apply h

(I think this is something one would only find given an already complete proof)

[Afiq Hatta]

awesome.

i also have another dumb question: if, in an inductive proof, we use the inductive hypothesis, how do we 'obtain' that object from it and use it.

example:

/-- The nth derivative of Tanh(x) is a polynomial of Tanh(x) -/
lemma iteratedDeriv_tanh_is_polynomial_of_tanh (n : ℕ) (x : ℝ) : ∃ P : Polynomial ℝ, ∀ x,
    iteratedDeriv n Real.tanh x = P.eval (Real.tanh x) := by
  induction n
  rw [iteratedDeriv_zero]
  use Polynomial.X
  simp

  rw [iteratedDeriv_succ]

im trying to 'use' the polynomial in the induction hypothesis
case succ
x : ℝ
n✝ : ℕ
a✝ : ∃ P, ∀ (x : ℝ), iteratedDeriv n✝ tanh x = Polynomial.eval (tanh x) P
⊢ ∃ P, ∀ (x : ℝ), deriv (iteratedDeriv n✝ tanh) x = Polynomial.eval (tanh x) P

[Afiq Hatta]

so here we have in a✝ that there is some polynomial such that nth iterated deriv is a polynomial of tan, and i want to sub that into the goal

[Joseph Tooby-Smith]

I think the tactic you want is obtain. I would set this up as follows:

import Mathlib
open Real

/-- The nth derivative of Tanh(x) is a polynomial of Tanh(x) -/
lemma iteratedDeriv_tanh_is_polynomial_of_tanh (n : ℕ) (x : ℝ) : ∃ P : Polynomial ℝ, ∀ x,
    iteratedDeriv n Real.tanh x = P.eval (Real.tanh x) := by
  induction n with
  | zero =>
    rw [iteratedDeriv_zero]
    use Polynomial.X
    simp
  | succ n ih =>
    obtain ⟨P, h'⟩ := ih
    rw [iteratedDeriv_succ]
    sorry

[Afiq Hatta]

dumb question so where does ih come from here ?

[Afiq Hatta]

ah no worries, got it

[Joseph Tooby-Smith]

More generally you can get rid of the ✝'s with the expose_names tactic.

[Afiq Hatta]

got it, thanks joe

[Afiq Hatta]

okok so i have to modify P then use it

[Joseph Tooby-Smith]

Yeah, the P in your goal is not going to be the same one you obtain from the induction hypothesis.
Namely I think the one in your goal should be (1 - X ^ 2) * Polynomial.derivative P or something along those lines

[Afiq Hatta]

yeah

[Afiq Hatta]

need to rewrite deriv (iteratedDeriv n tanh) x as deriv (Polynomial.eval (tanh x) P ), then apply chain rule, then use modified ploynomail

[Joseph Tooby-Smith]

Yep, this seems right to me.

[Afiq Hatta]

hm - im pretty sure i've got this rewrite correct, but still getting a fail

⊢ ∃ P_1, ∀ (x : ℝ), deriv ((fun t => Polynomial.eval t P) ∘ tanh) x = Polynomial.eval (tanh x) P_1

Tanh.lean:92:8

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
deriv (?h₂ ∘ ?h) ?x
*

[Afiq Hatta]

applying the derivative composition theorem here

[Joseph Tooby-Smith]

Could you paste a code snippet with the failing rewrite?

[Afiq Hatta]

lemma iteratedDeriv_tanh_is_polynomial_of_tanh (n : ℕ) (x : ℝ) : ∃ P : Polynomial ℝ, ∀ x,
    iteratedDeriv n Real.tanh x = P.eval (Real.tanh x) := by
  induction n with
  | zero =>
    rw [iteratedDeriv_zero]
    use Polynomial.X
    simp
  | succ n ih =>
    obtain ⟨P, h'⟩ := ih
    rw [iteratedDeriv_succ]
    have h'': iteratedDeriv n tanh = (fun x => Polynomial.eval (tanh x) P) := by
      funext x
      apply h'
    have h_comp : (fun x => Polynomial.eval (tanh x) P) = (fun t => P.eval t) ∘ tanh := by
      funext x
      simp [Function.comp_apply]
    rw [h'']
    rw [h_comp]
    rw [deriv_comp]

[Afiq Hatta]

its that last deriv_comp that fails

[Afiq Hatta]

is this a teachable moment - the symbols match up, but the match isn't working, is there something else that has to match, like the type on t?

[ZhiKai Pong]

get rid of the quantifiers first, i.e. use P and intro x(I'm just guessing from the infoview)

[Kevin Buzzard]

rw sometimes doesn't work under binders. You could try simp_rw or simp only instead.

[Afiq Hatta]

thank you both @ZhiKai Pong and @Kevin Buzzard and also @Joseph Tooby-Smith

this ended up working. now on the way to prove that tanh has temperate growth and therefore is a schwartz operator!

lemma iteratedDeriv_tanh_is_polynomial_of_tanh (n : ℕ) : ∃ P : Polynomial ℝ, ∀ x,
    iteratedDeriv n Real.tanh x = P.eval (Real.tanh x) := by
  induction n with
  | zero =>
    rw [iteratedDeriv_zero]
    use Polynomial.X
    simp
  | succ n ih =>
    obtain ⟨P, h'⟩ := ih
    rw [iteratedDeriv_succ]
    have h'': iteratedDeriv n tanh = (fun x => Polynomial.eval (tanh x) P) := by
      funext x
      apply h'
    have h_comp : (fun x => Polynomial.eval (tanh x) P) = (fun t => P.eval t) ∘ tanh := by
      funext x
      simp [Function.comp_apply]
    rw [h'', h_comp]
    use Polynomial.derivative P * (1 - Polynomial.X^2)
    intro x
    rw [deriv_comp, Polynomial.deriv, deriv_tanh]
    simp
    case h.hh =>
      have h': Real.tanh = (sinh / cosh) := by
        funext x
        rw [Pi.div_apply, tanh_eq_sinh_div_cosh]
      rw [h']
      apply DifferentiableAt.div
      · apply Real.differentiable_sinh
      · apply Real.differentiable_cosh
      · exact ne_of_gt (Real.cosh_pos x)
    case h.hh₂ =>
      apply Polynomial.differentiableAt

[Daniel Morrison]

Joseph Tooby-Smith said:

import Mathlib
open Real

/-- The nth derivative of Tanh(x) is a polynomial of Tanh(x) -/
lemma iteratedDeriv_tanh_is_polynomial_of_tanh (n : ℕ) (x : ℝ) : ∃ P : Polynomial ℝ, ∀ x,
    iteratedDeriv n Real.tanh x = P.eval (Real.tanh x) := by
  induction n with
  | zero =>
    rw [iteratedDeriv_zero]
    use Polynomial.X
    simp
  | succ n ih =>
    obtain ⟨P, h'⟩ := ih
    rw [iteratedDeriv_succ]
    sorry

I will add that it is useful to use induction' rather than induction. It does essentially the same thing but is a bit more user friendly. You can name the variable in the induction line by saying for example induction' n with n ih in this example. It also separates the goals more nicely so you can rewrite this as

  induction' n with n ih
  . rw [iteratedDeriv_zero]
    use Polynomial.X
    simp
  . obtain ⟨P, h'⟩ := ih
    rw [iteratedDeriv_succ]
    sorry

which I find a little bit nicer to read. (I haven't checked this code but I think it should be right)

[Matteo Cipollina]

Joseph Tooby-Smith ha scritto:

More generally you can get rid of the ✝'s with the expose_names tactic.

While a great heuristic, eventually it would be preferable safer to get rid of expose_names as well

[Afiq Hatta]

thanks for the tips team :) will clean the code up tomorrow morning with the alternative induction syntax

[Joseph Tooby-Smith]

Matteo Cipollina said:

Joseph Tooby-Smith ha scritto:

More generally you can get rid of the ✝'s with the expose_names tactic.

While a great heuristic, eventually it would be preferable safer to get rid of expose_names as well

It is better to use e.g. rename?

[Matteo Cipollina]

Joseph Tooby-Smith ha scritto:

Matteo Cipollina said:

Joseph Tooby-Smith ha scritto:

More generally you can get rid of the ✝'s with the expose_names tactic.

While a great heuristic, eventually it would be preferable safer to get rid of expose_names as well

It is better to use e.g. rename?

Yes, or combination of rw-exact often works for me

[Afiq Hatta]

hey @Joseph Tooby-Smith - im falling over a bit on how to formalise 'this function has temperate growth'

[Afiq Hatta]

not sure which exact property to use - brain is not braining

[Afiq Hatta]

if you have an example or hint i can take it from there

[Joseph Tooby-Smith]

I think the next step would be to show that for any polynomial P, Polynomial.eval (tanh x) P is bounded. I'm not actually sure the best way of doing this though.

[Afiq Hatta]

cool, i can do that first

[Afiq Hatta]

presumably there is some property in mathlib that represents 'bounded for all x in \R'

[Afiq Hatta]

ah actually i reckon can just do this

lemma polynomials_tanh_bounded : ∀ P : Polynomial ℝ, ∃ C : ℝ, ∀ x : ℝ, |P.eval (Real.tanh x)| < C :=
  sorry

[Joseph Tooby-Smith]

I think if there is it would be then the temperate growth proposition would us it (and I don't think it does). But I think the thing you want is:

import Mathlib

open Real Polynomial

example (P : Polynomial ℝ) : ∃ C, ∀ x, P.eval (tanh x) ≤ C := by sorry

[Afiq Hatta]

omg hahah

[Afiq Hatta]

we literally wrote that at the same time

[Joseph Tooby-Smith]

haha yep, either of these would work, actually I think yours is better because you have abs :).

[Joseph Tooby-Smith]

Btw when putting code snippets into Zulip it helps to put the necessary preamble e.g.

import Mathlib

open Real Polynomial

...

That way people can open the code snippet in https://live.lean-lang.org by pressing the pop-up in the top right corner of the snippet, and everything will compile nicely :).

[Afiq Hatta]

ah - didn't realise you could do that - awesome

[Afiq Hatta]

this all works - i proved that the iteratived derivative of tanh is bounded

import PhysLean.Meta.Linters.Sorry
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
import Mathlib.Data.Complex.Trigonometric
import Mathlib.Analysis.Calculus.Deriv.Polynomial
import Mathlib.Topology.Algebra.Polynomial
/-!
# Properties of Tanh
We want to prove that the reflectionless potential is a Schwartz map.
This means proving that pointwise multiplication of a Schwartz map with tanh is a Schwartz map.
This means we need to prove that all derivatives of tanh are bounded and continuous, so that
the nth derivative of a function multiplied by tanh decays faster than any polynomial.

## TODO
- Add these to mathlib eventually
- Fill in the proofs for the properties of tanh
-/

open Real
open NNReal
open Field

/-- tanh(x) is less than 1 for all x -/
lemma tanh_lt_one (x : ℝ) : tanh x < 1 := by
  rw [tanh_eq_sinh_div_cosh, div_lt_one (cosh_pos x)]
  exact sinh_lt_cosh x

/-- tanh(x) is greater than -1 for all x -/
lemma minus_one_lt_tanh (x : ℝ) : -1 < tanh x := by
  rw [tanh_eq_sinh_div_cosh, lt_div_iff₀ (cosh_pos x), ← sub_pos, neg_one_mul]
  simp [exp_pos x]

/-- The absolute value of tanh is bounded by 1 -/
lemma abs_tanh_lt_one (x : ℝ) : |tanh x| < 1 := by
  rw [abs_lt]
  constructor
  · exact minus_one_lt_tanh x
  · exact tanh_lt_one x

/-- The derivative of tanh(x) is 1 - tanh(x)^2 -/
lemma deriv_tanh : deriv Real.tanh = fun x => 1 - Real.tanh x ^ 2 := by
  have h: deriv (sinh / cosh) = fun x => 1 - Real.tanh x ^ 2 := by
    funext x
    rw [deriv_div, Real.deriv_sinh, Real.deriv_cosh]
    field_simp
    rw [sq, sq, tanh_eq_sinh_div_cosh, mul_sub_right_distrib]
    field_simp
    · apply Real.differentiable_sinh
    · apply Real.differentiable_cosh
    · exact ne_of_gt (Real.cosh_pos x)
  have h': Real.tanh = (sinh / cosh) := by
    funext x
    rw [Pi.div_apply, tanh_eq_sinh_div_cosh]
  nth_rewrite 1 [h']
  apply h

/-- Tanh(x) is n times continuously differentiable for all n -/
lemma contDiff_tanh {n : ℕ} : ContDiff ℝ n tanh := by
  have hdiv : ContDiff ℝ n (fun x => Real.sinh x / Real.cosh x) := by
    apply ContDiff.div
    · exact contDiff_sinh
    · exact contDiff_cosh
    · intro x
      exact ne_of_gt (Real.cosh_pos x)
  conv =>
    enter [3, x]
    rw [tanh_eq_sinh_div_cosh]
  exact hdiv

/-- The nth derivative of Tanh(x) is a polynomial of Tanh(x) -/
lemma iteratedDeriv_tanh_is_polynomial_of_tanh (n : ℕ) : ∃ P : Polynomial ℝ, ∀ x,
    iteratedDeriv n Real.tanh x = P.eval (Real.tanh x) := by
  induction n with
  | zero =>
    rw [iteratedDeriv_zero]
    use Polynomial.X
    simp
  | succ n ih =>
    obtain ⟨P, h'⟩ := ih
    rw [iteratedDeriv_succ]
    have h'': iteratedDeriv n tanh = (fun x => Polynomial.eval (tanh x) P) := by
      funext x
      apply h'
    have h_comp : (fun x => Polynomial.eval (tanh x) P) = (fun t => P.eval t) ∘ tanh := by
      funext x
      simp [Function.comp_apply]
    rw [h'', h_comp]
    use Polynomial.derivative P * (1 - Polynomial.X^2)
    intro x
    rw [deriv_comp, Polynomial.deriv, deriv_tanh]
    simp
    case h.hh =>
      have h': Real.tanh = (sinh / cosh) := by
        funext x
        rw [Pi.div_apply, tanh_eq_sinh_div_cosh]
      rw [h']
      apply DifferentiableAt.div
      · apply Real.differentiable_sinh
      · apply Real.differentiable_cosh
      · exact ne_of_gt (Real.cosh_pos x)
    case h.hh₂ =>
      apply Polynomial.differentiableAt
-- For a polynomial P, show it's bounded on any bounded interval
lemma polynomial_bounded_on_interval (P : Polynomial ℝ) (a b : ℝ):
  ∃ M : ℝ, ∀ x : ℝ, x ∈ Set.Icc a b → |P.eval x| ≤ M := by
  -- Polynomials are continuous
  have hcont : Continuous (fun x => P.eval x) := P.continuous  -- Closed bounded intervals are compact
  have hcompact : IsCompact (Set.Icc a b) := isCompact_Icc
  -- Continuous functions on compact sets are bounded
  obtain ⟨M, hM⟩ := hcompact.exists_bound_of_continuousOn hcont.continuousOn
  use M
  exact hM
-- For a polynomial P, show that P (tanh x) is bounded on the real line
theorem polynomial_tanh_bounded (P : Polynomial ℝ) :
  ∃ C : ℝ, ∀ x : ℝ, |P.eval (Real.tanh x)| ≤ C := by
  have h_range : ∀ x : ℝ, Real.tanh x ∈ Set.Icc (-1) 1 := by
    intro x
    constructor
    · exact le_of_lt (minus_one_lt_tanh x)
    · exact le_of_lt (tanh_lt_one x)
  -- Apply polynomial boundedness on [-1, 1]
  obtain ⟨M, hM⟩ := polynomial_bounded_on_interval P (-1) 1
  use M
  intro x
  exact hM (Real.tanh x) (h_range x)
-- The nth derivative of tanh is bounded on the real line
theorem iteratedDeriv_tanh_bounded (n : ℕ) :
  ∃ C : ℝ, ∀ x : ℝ, |iteratedDeriv n Real.tanh x| ≤ C := by
  obtain ⟨P, hP⟩ := iteratedDeriv_tanh_is_polynomial_of_tanh n
  obtain ⟨C, hC⟩ := polynomial_tanh_bounded P
  use C
  intro x
  rw [hP]
  exact hC x

[Joseph Tooby-Smith]

Nice! This looks great! Proving that tanh has temperate growth should now follow fairly trivially right?

[Afiq Hatta]

dumb question - where is the 'temperate growth' property?

[Joseph Tooby-Smith]

(deleted)

[Joseph Tooby-Smith]

@loogle Function.HasTemperateGrowth

[loogle]

:search: Function.HasTemperateGrowth, Function.HasTemperateGrowth.const, and 9 more

[Joseph Tooby-Smith]

So "Mathlib.Analysis.Distribution.SchwartzSpace"

[Afiq Hatta]

btw is anyone else getting 404s accessing https://leanprover-community.github.io/?

[Afiq Hatta]

got it - will prove that and then commit this soup

[Joseph Tooby-Smith]

Afiq Hatta said:

btw is anyone else getting 404s accessing https://leanprover-community.github.io/?

Works for me.

[Afiq Hatta]

really dumb question - i'm struggling with going from 'for all n' to 'infinitely differentiable' here - why is there a token error on the \infty part of this lemma?

import PhysLean.Meta.Linters.Sorry
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
import Mathlib.Data.Complex.Trigonometric
import Mathlib.Analysis.Calculus.Deriv.Polynomial
import Mathlib.Topology.Algebra.Polynomial
import Mathlib.Analysis.Distribution.SchwartzSpace

open Real
open NNReal
open Field

-- Alternative approach for the smoothness part:
/-- tanh is infinitely differentiable -/
lemma contDiff_top_tanh : ContDiff ℝ ∞ Real.tanh x := by
  -- Show that tanh is ContDiff for all finite orders, which implies ContDiff ⊤
  -- apply ContDiff.of_le

  -- · exact contDiff_tanh
  -- · exact le_top
  sorry

[Afiq Hatta]

A bit confused on the type of infty here it expects. the code says n can also be N\infty but that doesn't work either

[Afiq Hatta]

The goal i'm aiming for here is
ContDiff ℝ (↑⊤) tanh

[ZhiKai Pong]

from a previous conversation:

Aaron Liu: Read carefully: docs#ContDiff takes a WithTop ENat, which has two tops. The higher top ("omega") is for analytic functions, and the lower top ("infinity") is for smooth (infinitely differentiable) functions.

Aaron Liu: If you open scoped ContDiff it'll print these differently.

[Afiq Hatta]

works! thankas @ZhiKai Pong

[Afiq Hatta]

hey @Joseph Tooby-Smith I was wondering if there was a theorem on compositions of two temperate growth functions having temperate growth

[Afiq Hatta]

i couldn't find it - and needed it to easily show that tanh ( k x ) is temperate for all k real

[Afiq Hatta]

if not, i can sketch up a proof?

[Joseph Tooby-Smith]

I don't think so, but it might just be easier to show that tanh ( k x ) has temperate growth given tanh x has temperate growth.

[Afiq Hatta]

yeah

[Afiq Hatta]

i actually don't know if the composition of two temperate growth functions has temperate growth anyway.

[Joseph Tooby-Smith]

I think it probably is true - because the iterated derivative of the composition becomes the sum of iterated derivatives of each part via the chain rule, which should be bounded. Proving it formally is a different matter though.

[Joseph Tooby-Smith]

It may also be possible/quickest to modify your proofs for tanh x and turn them into proofs of tanh (k * x)

[Afiq Hatta]

Hey guys, I have a dumb question. To show that tanh is a Schwartz map: after I apply tanh, there has to be a trivial embedding of Real.tanh into the complex numbers. I then need to show that this composition has temperate growth. Is there any easier way of doing this besides proving that the composition of temperate growth maps is also temperate, or redoing the whole proof of temperateGrowth of tanh in \C ?

-- Scaled tanh embedded into the complex numbers has temperate growth
theorem scaled_tanh_complex_hasTemperateGrowth (κ : ℝ) :
    Function.HasTemperateGrowth (fun x => (Real.tanh (κ * x) : ℂ)) := by
  sorry

/-- Define tanh(κ X) multiplication pointwise as a Schwartz map -/
noncomputable def tanhOperatorSchwartz (Q : ReflectionlessPotential) :
    𝓢(ℝ, ℂ) →L[ℂ] 𝓢(ℝ, ℂ) := by
  -- We need to handle the Real → Complex coercion
  let scaled_tanh_real : ℝ → ℝ := fun x => Real.tanh (Q.κ * x)
  let scaled_tanh_complex : ℝ → ℂ := fun x => (Real.tanh (Q.κ * x) : ℂ)
  have h2 : Function.HasTemperateGrowth scaled_tanh_complex
    := scaled_tanh_complex_hasTemperateGrowth Q.κ
  exact bilinLeftCLM (ContinuousLinearMap.mul ℂ ℂ) h2

[ZhiKai Pong]

The way you phrase this makes me think you should probably have a separate lemma that proves any trivial embedding of real Schwartz maps into the complex also has temperate growth and just apply that, but I'm not sure how feasible as I'm not that familiar with the Schwartz map API at the moment

[Afiq Hatta]

yeah that's what i was thinking as well. I am still new to lean so was wondering if there was any quick keyword that does this for me, but I guess not

[Afiq Hatta]

@Joseph Tooby-Smith i wrote a pull request for definitions for the creation and operation operators, leaving a sorry statement for the proof of the embedding thing that I need

[Joseph Tooby-Smith]

I think this is what you want:

Code

import Mathlib

example (f : ℝ → ℝ) (h : Function.HasTemperateGrowth f) :
    Function.HasTemperateGrowth (fun x => (f x : ℂ)) := by
  refine And.intro (Complex.ofRealCLM.contDiff.fun_comp h.1) (fun n => ?_)
  obtain ⟨k, C, hn⟩ := h.2 n
  refine ⟨k, C, fun x => (le_of_eq ?_).trans (hn x)⟩
  exact (RCLike.ofRealLI (K := ℂ)).norm_iteratedFDeriv_comp_left
     h.1.contDiffAt (WithTop.le_coe_iff.mpr ⟨n, by simp⟩)

Found it by loogling iteratedFDeriv, "comp" and spotting LinearIsometry.norm_iteratedFDeriv_comp_left.

(Edits: Golf)

[Afiq Hatta]

Thanks! I'll take some go through this example because I actually don't know a lot of these keywords. Btw - I see that you're a fan of using 'refine' - what kinds of problems lend well to using that keyword?

[Afiq Hatta]

like why use refine And.intro, vs something like constructor?

[Joseph Tooby-Smith]

refine is basically exact but you can have holes in it which are the ?_. Your goal then becomes what is needed to fill in the ?_. In some interactive theorem provers like Agda this sort of manipulation is basically all that is used. I like to view refine, exact and apply as sitting in the same collection of tactics.

I personally tend not to use constructor that often because for some reason I only recently learnt about it - and I have a habit of using refine And.intro ?_ ?_ or apply And.intro etc.

[Afiq Hatta]

got it - makes sense

[Afiq Hatta]

Where do we think is an appropriate place to put the embedding theorem that you wrote?

[Joseph Tooby-Smith]

I would probably just put it as a private lemma just before you need it for now.

[Joseph Tooby-Smith]

(FYI - I just cleaned it up some more)

[Joseph Tooby-Smith]

I should also say - for reference that my proof above is after golfing to make it shorter and nice - I started with something a lot longer and messier.

[Afiq Hatta]

got it. that's good to know, because when i read some solutions i'm like 'how...!!'. the way I've been trying to get at solutions is by doing

constructor
apply
apply
apply

till the cows come home, just trying to match goals with theorems in mathlib and then only golfing after.

[Joseph Tooby-Smith]

Yeah I think this is common and this is what I do too. Once you have a working proof it is relatively easy to make it shorter - that said there are lots of proofs within PhysLean that have never been golfed :).

[Afiq Hatta]

yeah. ok my mission for today is to add this and also maybe just write some words on my blog about the general strategy of just apply apply apply then golfing later.

[Afiq Hatta]

@Joseph Tooby-Smith here's a really dumb question - I often get stuck on rewrites not matching the target but it does take a lot of time to figure out what's going on. Is there anything that I can do to make the trouble shooting a bit easier? For example, I'm trying to do the proof on my own and I don't know why this final rewrite is failing?

lemma complex_embedding_of_temperate_growth(f : ℝ → ℝ) (h : Function.HasTemperateGrowth f) :
    Function.HasTemperateGrowth (fun x => (f x : ℂ)) := by
  constructor
  apply ContDiff.fun_comp
  apply ContinuousLinearMap.contDiff Complex.ofRealCLM
  obtain ⟨h1, h2⟩ := h
  apply h1
  obtain ⟨h1, h2⟩ := h
  intro n
  use 0
  use 0
  intro x
  have h : (fun x => ((f x) : ℂ)) = (Complex.ofRealCLM ∘ f) := by
    sorry
  rw [h]
  apply LinearIsometry.norm_iteratedFDeriv_comp_left

[Afiq Hatta]

i'm just as curious about the trouble shooting here (ie how to check if I got anything wrong with types etc, and obvious ways to spot errors) as well as what went wrong in this specific example

[Joseph Tooby-Smith]

You mean the finial apply? The last rw looks like it's working to me.

[Afiq Hatta]

sorry - the final apply!

[Afiq Hatta]

i can't seem to get it to work

[Joseph Tooby-Smith]

Two reasons:

1. You need RCLike.ofRealLI not Complex.ofRealCLM in h. The former is a linear isometry whilst the latter is a continuous linear map. As functions they are both equal, but have different types.
2. To use apply your goal has to be the same as the theorem given, in this case it is not. However, once you have made the change 1 here, then rw [LinearIsometry.norm_iteratedFDeriv_comp_left] should work.

[Afiq Hatta]

ah - so does the break come from the actual type being wrong? because usually, what happens is that i apply the theorem, and then a subgoal is created in which i prove that something satisfies that. but i guess that only applies to hypotheses

[Joseph Tooby-Smith]

Here is a short description of what apply does:

Let us say you have a proof h : A → B → C and your goal is equal to C, then apply h will great subgoals for A and B. But if your goal is not currently C then you can't use apply h.

I don't really use e.g. apply _ at _ so don't know how that works exactly.

[Afiq Hatta]

got it - that's clear - thanks Joe

[ZhiKai Pong]

@Joseph Tooby-Smith may I ask how do you inspect this code? since this depends on an open PR, is there a way to directly play around with it or do you just copy the relevant lemmas to your local PhysLean?

[Joseph Tooby-Smith]

For this specific example the lemma I ended up proving didn't actually need anything from the PR, so I just used https://live.lean-lang.org.

But more generally, if there is something I want to look at from a given PR or play around with in more detail, I will just check out the corresponding PR. Which on github desktop is done via:

Screenshot 2025-09-09 at 13.38.18.png

[Afiq Hatta]

@Joseph Tooby-Smith

my own attempt (learning)

lemma complex_embedding_of_temperate_growth(f : ℝ → ℝ) (h : Function.HasTemperateGrowth f) :
    Function.HasTemperateGrowth (fun x => (f x : ℂ)) := by
  constructor
  apply ContDiff.fun_comp
  apply ContinuousLinearMap.contDiff Complex.ofRealCLM
  obtain ⟨h1, h2⟩ := h
  apply h1
  obtain ⟨h1, h2⟩ := h
  intro n
  obtain ⟨k, C, j⟩ := h2 n
  use k
  use C
  intro x
  have h : (fun x => (Complex.ofReal ∘ f) x) = (RCLike.ofRealLI (K := ℂ) ∘ f) := by
    funext x
    simp
  have h'' : (fun x => (f x : ℂ)) = (fun x => (Complex.ofReal ∘ f) x) := rfl
  rw [h'']
  rw [h]
  rw [LinearIsometry.norm_iteratedFDeriv_comp_left (g := RCLike.ofRealLI (K := ℂ)) (hf := h1.contDiffAt)]
  apply j
  apply ENat.natCast_le_of_coe_top_le_withTop
  simp only [le_refl]

[Joseph Tooby-Smith]

Awesome! I would now play the game to see how much you can golf this, maybe using tactics you are less familiar with.

[Afiq Hatta]

yeah. i've starting writing some notes on useful go to tactics for beginners which i'll publish tonight

[Joseph Tooby-Smith]

Nice! I would be interested to see at some point what are the most common tactics used in e.g. PhysLean compared to Mathlib etc.

I would advocate for conv_lhs, conv_rhs to be part of that list - once I discovered them they were a life-changer.

[ZhiKai Pong]

@Afiq Hatta

I did the same earlier but waited for you to finish, just some minor comments:

import Mathlib

lemma complex_embedding_of_temperate_growth(f : ℝ → ℝ) (h : Function.HasTemperateGrowth f) :
    Function.HasTemperateGrowth (fun x => (f x : ℂ)) := by
  -- once you structure the code you'll see that the reason you had two of the same obtains was because they were in different branches so you can just put it before constructor
  -- in general always use dot notation to structure the proof whenever you use constructor and create multiple goals
  obtain ⟨h1, h2⟩ := h
  constructor
  · apply ContDiff.fun_comp
    apply ContinuousLinearMap.contDiff Complex.ofRealCLM
    exact h1
  · intro n
    obtain ⟨k, C, j⟩ := h2 n
    use k, C
    intro x
    -- actually this is also defeq so you can just combine into one
    -- have h : (fun x => (Complex.ofReal ∘ f) x) = (RCLike.ofRealLI (K := ℂ) ∘ f) := rfl
    /-
    have h'' : (fun x => (f x : ℂ)) = (RCLike.ofRealLI (K := ℂ) ∘ f) := rfl
    rw [h'']
    -/
    -- also for defeq expressions you can simply use `change`:
    change ‖iteratedFDeriv ℝ n (RCLike.ofRealLI ∘ f) x‖ ≤ C * (1 + ‖x‖) ^ k
    rw [LinearIsometry.norm_iteratedFDeriv_comp_left (g := RCLike.ofRealLI (K := ℂ)) (hf := h1.contDiffAt)]
    exact j x
    · apply ENat.natCast_le_of_coe_top_le_withTop
      simp only [le_refl]

also please include import Mathlib if it's a standalone lemma so others can just view it in the web playground :)

[Afiq Hatta]

Thanks @ZhiKai Pong - this kind of breakdown is really helpful.

[Afiq Hatta]

I was wondering about how to use change expressions - thank you for the flag. Need to learn more!!!

[Afiq Hatta]

@Joseph Tooby-Smith wrote a reply to one of the things you raised on my pull request btw

[Afiq Hatta]

@Joseph Tooby-Smith updated the pull request with the new proofs and also the requested refactors!

[Joseph Tooby-Smith]

Just approved it - I merged with master merged master into this PR to clean it up, I think you will have to wait for it to finish the workflows before you can merge it.

[Afiq Hatta]

sweet

[Afiq Hatta]

I think the next logical thing to prove would be that the Hamiltonian of the reflectionless potential satisfies
$H = a ^ \dagger a - \frac { \hbar ^ 2 \kappa ^ 2 } { 2m } \mathbb I$

For this, I reckon we also need

• the commutuation relations
• to formalise the Hamiltonian, and also prove that it is also a Schwartz map? In terms of formalising the Hamiltonian - is there a special template that I can follow elsewhere in the code?

Also - what is the convention for what a 'ground state' here? in the paper, it is just $a \ket 0$ = 0. is this a convention that we want to keep in physlean?

[Joseph Tooby-Smith]

I think the fact that the Hamiltonian is Schwartz should follow from the proof that the momentum operator is Schwartz and the tanh operator is.

[Afiq Hatta]

sweet. and in terms of the algebraic proof of the eigenvalues - i guess i can follow this quantum harmonic oscillator example as a rough guide