I've recently started working on formalising some proofs of the [reflectionless potential](https://arxiv.org/pdf/2411.14941) in [PhysLean](https://physlean.com/). I do this because I hope that, if we do have some generative approach to creating physical laws with AI, then But the issue is that Lean is hard The first non-trivial thing I tried to do is show that multiplying pointwise by tanh preserves function decay. This is true because tanh is bounded and continuous. But I need a theorem - the first theorem is that pointwise multiplication by a continuous, bounded function takes a rapidly decaying function to a rapidly decaying function. $\psi(x) \mapsto \tanh(x) \psi (x)$ 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