Coercion is smooth and smul is smooth?

Stream: new members

[Riyaz Ahuja]

Hi all,
I'm trying to prove that the following function is continuously differentiable (smooth) as follows:

def ruffle : ℝ → ℂ := fun x ↦ -Complex.sin (4 * ↑π * ↑x) + (2 * Complex.sin (2 * ↑π * ↑x)) • I

And am almost done, except for two small subclaims I need to prove. Firstly:

ContDiff ℝ ⊤ (fun x ↦ ↑x)

Seems to be less straightforward than what I expected. (Note the function is ℝ → ℂ). How do I account for the coersion here?

Similarly:

ContDiff ℝ ⊤ fun x ↦ (2 * Complex.sin (2 * ↑π * ↑x)) • I

I'm just trying to apply ContDiff.smul, but it's not recognizing the I as a valid function. Any tips or fixes?

Thanks!

[Ruben Van de Velde]

Please post a #mwe

[Riyaz Ahuja]

import Mathlib

open Analysis Complex

lemma coer_diff : ContDiff ℝ ⊤ fun (x:ℝ) ↦ (x:ℂ) := by
  sorry

lemma smul_sin_diff : ContDiff ℝ ⊤ fun (x:ℝ) ↦ (2 * Complex.sin (2 * ↑π * ↑x)) • I := by
  sorry

[Ruben Van de Velde]

For the second:

import Mathlib

open  Complex Real

set_option autoImplicit false

lemma coer_diff : ContDiff ℝ ⊤ fun (x:ℝ) ↦ (x:ℂ) := by
  sorry

lemma smul_sin_diff : ContDiff ℝ ⊤ fun (x:ℝ) ↦ (2 * Complex.sin (2 * ↑π * ↑x)) • I := by
  simp only [smul_eq_mul]
  apply ContDiff.mul ?_ contDiff_const
  apply ContDiff.mul contDiff_const ?_
  simp_rw [← Complex.ofReal_ofNat, ← Complex.ofReal_mul, ←Complex.ofReal_sin]
  apply coer_diff.comp
  apply ContDiff.sin
  apply ContDiff.mul contDiff_const ?_
  apply contDiff_id

(note that in your mwe, it treated π as a variable)

[Alex J. Best]

for the first, I just spammed apply? and clicked things and got to this proof :wink:

lemma coer_diff : ContDiff ℝ ⊤ fun (x:ℝ) ↦ (x:ℂ) := by
  refine IsBoundedLinearMap.contDiff ?hf
  refine IsLinearMap.with_bound ?hf.hf 1 ?hf.h
  refine { map_add := ?hf.hf.map_add, map_smul := ?hf.hf.map_smul }
  simp
  simp
  simp

[Ruben Van de Velde]

I tried that but clicked the wrong things

[Ruben Van de Velde]

Does docs#ofRealClm help?

[Kevin Buzzard]

or docs#ContinuousLinearMap.contDiff (plus continuity)?

[Ruben Van de Velde]

Shirley it's not called that anymore :)

[Kevin Buzzard]

I found it in an old thread and didn't grok that it was Lean 3 :-) Fixed now.

[Kevin Buzzard]

lemma coer_diff : ContDiff ℝ ⊤ fun (x:ℝ) ↦ (x:ℂ) :=
  ContinuousLinearMap.contDiff ofRealClm

[Kevin Buzzard]

indeed both of those things help :-)

[Patrick Massot]

@Riyaz Ahuja Why do you use Complex.sin only to feed it a real number coerced into a complex number. You could do

lemma smul_sin_diff : ContDiff ℝ ⊤ fun (x:ℝ) ↦ (2 * Real.sin (2 * π * x)) • I := by
  apply ContDiff.smul ?_ contDiff_const
  apply ContDiff.smul contDiff_const
  apply ContDiff.sin
  apply ContDiff.mul contDiff_const
  exact contDiff_id

[Patrick Massot]

And then you can try to impress your professor by compressing it down to

lemma smul_sin_diff : ContDiff ℝ ⊤ fun (x:ℝ) ↦ (2 * Real.sin (2 * π * x)) • I :=
  (contDiff_const.smul (contDiff_const.mul contDiff_id).sin).smul contDiff_const