PhsyLean suitable for a mathematics undergrad student

Stream: PhysLean

[Jard]

Today I officially started my bachelor thesis in mathematics on LEAN4 under the supervision of @Marcello Seri . As part of my thesis, I would love to make one or two contributions to the PhysLean library. Looking at the to-do list, I saw "divergence_smul" that is currently a sorryful result and looks to be within my scope of knowledge. Before I start working on that one however, I was wondering if anyone was already working on it, or if there are other results that are more pressing/in greater need by people to advance their own projects. I am so excited to be part of the community!

[Joseph Tooby-Smith]

Hi @Jard ! Welcome to the channel :). I think this is a great place to start, and I’m pretty confident no one else is working on this. If you do this and are keen to contribute more, I can help find somewhere for you to help :).

[Jard]

I have since almost finished this lemma, there is just one detail I am incredibly stuck on. I have the following goal

**𝕜** : Type u_1
**inst✝⁴** : RCLike 𝕜
**E** : Type u_2
**inst✝³** : NormedAddCommGroup E
**inst✝²** : NormedSpace 𝕜 E
**inst✝¹** : InnerProductSpace' 𝕜 E
**f** : E → 𝕜
**g** : E → E
**x** : E
**hf** : DifferentiableAt 𝕜 f x
**hg** : DifferentiableAt 𝕜 g x
**inst✝** : FiniteDimensional 𝕜 E
**s** : Set E
**s_fin** : Fintype ↑s
**basis** : Basis { x // x ∈ s.toFinset } 𝕜 E
**b** : Nonempty (Basis { x // x ∈ s } 𝕜 E)
**⊢** HasAdjoint 𝕜 (⇑(fderiv 𝕜 f x)) (adjoint 𝕜 ⇑(fderiv 𝕜 f x))

Would anyone be able to point me in the right direction on how to show this adjoint exists?

[Joseph Tooby-Smith]

Hi Jard! Could you possibly make a mwe for this, as it will allow us to more easily interact with the code?

BTW I think in the meantime @Miyahara Kō has added a proof of this result to PhysLean. But please don't let this stop you finishing your proof, as I think it will be a useful learning experience, and it would be great to have more people familiar with this part of the library.

[Jard]

Hi! I think this is a minimal working example:

lemma divergence_smul_mwe [InnerProductSpace' 𝕜 E] {f : E → 𝕜} {g : E → E} {x : E}
    (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x)
    [FiniteDimensional 𝕜 E] :
    divergence 𝕜 (fun x => f x • g x) x
    = f x * divergence 𝕜 g x + ⟪adjFDeriv 𝕜 f x 1, g x⟫ := by
  unfold divergence
  simp [fderiv_fun_smul hf hg]
  obtain ⟨s, b⟩ := Basis.exists_basis 𝕜 E
  let basis := Classical.choice b
  have s_fin : Fintype s := FiniteDimensional.fintypeBasisIndex basis
  have h_basis : Basis (↑s) 𝕜 E = Basis s.toFinset 𝕜 E := by
    simp only [Set.mem_toFinset]
  rw [h_basis] at basis
  have h₁ : ⟪adjoint 𝕜 (⇑(fderiv 𝕜 f x)) 1, g x⟫ = (fderiv 𝕜 f x)  (g x):= by
    rw [HasAdjoint.adjoint_inner_left]
    · simp_all only [RCLike.inner_apply, map_one, mul_one]
      rfl
    · sorry

It is then the last sorry point.

I did see the proof was added to physlean, and a much more elegant proof than I have at that! It has been an amazing learning experience indeed. Thank you for your help!

[Joseph Tooby-Smith]

Thanks - ideally one would want to make the mwe independent of PhysLean totally, but I think in this case this would be extremely difficult, so what you have done is great :).

Filling this last sorry is difficult, but there is a quick way of doing this. Let me give you a hint: there are parts of the proof of divergence_smul which appears in PhysLean which can be adapted to fill in this sorry. I'm happy to be more explicit if this would help.

[Jard]

I got it! Thanks for your help!

[Jard]

Hi again, and sorry for all the questions! My supervisor and I were looking at other places where I could contribute. We were thinking either working on something in the harmonic oscillator areas, or potentially working on "Module doc-string improvements #713". Do you have any other suggestions or do you think these are good places to work in?

[Joseph Tooby-Smith]

Hi Jard! Either of these would be amazing, and I think would be a good place to work. There are a number of things which need doing for the harmonic oscillator, and generalizations (e.g. including damping) which could be made.

If you end up doing one of these, I would recommend making a quick comment on the relevant threads here:

• #PhysLean > Priority documentation tracker for documentation.
• #PhysLean > Classical Harmonic Oscillator for the harmonic oscillator.

There is also some conversation there about each of these.

[Notification Bot]

5 messages were moved from this topic to #PhysLean > Quantum computing by Joseph Tooby-Smith.