Computing `gradient`

Stream: PhysLean

[Tomas Skrivan]

IRight now, it is quite difficult computing gradient f as the API in mathlib is not well developed. I think gradient is not even the good primitive to work with. I made a PR622 that defines

   adjFDeriv 𝕜 f x = (fderiv 𝕜 f x).adjoint

then we have gradient f x = adjFDeriv 𝕜 f x 1 and working with adjFDeriv is easier as we can formulate composition theorem

theorem adjFDeriv_comp {f : F → G} {g : E → F} {x : E}
    (hf : DifferentiableAt 𝕜 f (g x)) (hg : DifferentiableAt 𝕜 g x) :
    adjFDeriv 𝕜 (fun x => f (g x)) x = fun dy => adjFDeriv 𝕜 g x (adjFDeriv 𝕜 f (g x) dy)

One difficulty when working with gradient/adjFDeriv is that X×Y is not an inner product space so we have to work with WithLp 2 (X×Y) which does not have as well developed API. Part of the PR is to define ProdL2 X Y := WithLp 2 (X×Y) and corresponding API to make our life easier.

The PR is just a draft and there a bunch of sorry, any help would be appreciated.
@ZhiKai Pong I think this PR would help you to do bunch of calculations you have been doing.

[Tomas Skrivan]

This PR is also necessary to derive Euler-Lagrange equations by using variational calculus.

[ZhiKai Pong]

I have been quite busy recently and haven't been following very closely on what you and Joseph are working on, but many thanks for those and I'll definitely go through them when I have time :)

[Joseph Tooby-Smith]

Great! Somewhat related, I made PR620 a couple of days ago which relates Space.grad to gradient.

[Tomas Skrivan]

I have significantly reworked how adjoint works. I really hate the situation with X×Y vs WithLp 2 (X×Y) so instead I have introduced the class

class InnerProductSpace' (𝕜 : Type*) (E : Type*) [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    extends Norm₂ E where
  core : InnerProductSpace.Core 𝕜 E
  /-- Norm induced by inner is topologicaly equivalent to the given norm -/
  inner_top_equiv_norm : ∃ c d : ℝ,
    c > 0 ∧ d > 0 ∧
    ∀ x : E, (c • ‖x‖^2 ≤ re (core.inner x x)) ∧ (re (core.inner x x) ≤ d • ‖x‖^2)

which attaches inner product to normed space and requires that the norm induced by the inner product is topologically equivalent to the existing norm on the space. This way we can have inner product on X×Y and not faff around with WithLp. For example, for f : ℝ → ℝ → ℝ we can write adjFDeriv ℝ ↿f and Lean will not complain that the is no instance InnerProductSpace 𝕜 (ℝ×ℝ) as it does when we write gradient ↿f.

The only sorries are related to the topological equivalence between X equipped with its norm topology and the topology induced by the inner product.

[Joseph Tooby-Smith]

How should I think of the difference between InnerProductSpace' and InnerProductSpace?
Is one more general than the other, or are they secretly equivalent?

[Tomas Skrivan]

I added doc string to InnerProductSpace'

---

Effectively as InnerProductSpace 𝕜 E but it does not requires that ‖x‖^2 = ⟪x,x⟫. It is
only required that they are equivalent ∃ (c > 0) (d > 0), c • ‖x‖^2 ≤ ⟪x,x⟫ ≤ d • ‖x‖^2. The main
purpose of this class is to provide inner product space structure on product types ExF and
pi types ι → E without using WithLp gadget.

If you want to access L₂ norm use ‖x‖₂ := √⟪x,x⟫.

This class induces InnerProductSpace 𝕜 (WithLp 2 E) which equips ‖·‖ on X with L₂ norm.
This is very useful when translating results from InnerProductSpace to InnerProductSpace'
together with toL2 : E →L[𝕜] (WithLp 2 E) and fromL2 : (WithL2 2 E) →L[𝕜] E.

In short we have these implications:

  InnerProductSpace 𝕜 E → InnerProductSpace' 𝕜 E
  InnerProductSpace' 𝕜 E → InnerProductSpace 𝕜 (WithLp 2 E)

The reason behind this type class is that with current mathlib design the requirement
‖x‖^2 = ⟪x,x⟫ prevents us to give inner product space structure on product type E×F and pi
type ι → E as they are equipped with max norm. One has to work with WithLp 2 (E×F) and
WithLp 2 (ι → E). This places quite a bit inconvenience on users in certain scenarios,
in particular the main motivation behind this class is to make computations of adjFDeriv and
gradient easy.

[Joseph Tooby-Smith]

This makes sense! Thanks for the explanation.

[Tomas Skrivan]

I really tried making adjFDeriv working with WithLp but it was really painful and I was constantly accidentally causing defeq abuse between X⨯Y and WithLp 2 (X×Y). If I can't get it right then there is no hope for beginners to get it right.

[Tomas Skrivan]

I would like to have InnerProductSpace' in mathlib and ideally InnerProductSpace just extends it and most of the results are formulated in terms of InnerProductSpace'. However, when I talked about it I did not get any meaningful response to the proposed change.

[Joseph Tooby-Smith]

Yeah, I agree with the philosophy here. Anything that avoids defeq abuse or having to worry about things being the correct type, I think is a massive benefits to usability - and is a massive turn-off using Lean when it's not done right.

[Joseph Tooby-Smith]

I think this is especially true for physicists where the tolerance for dealing with this type of thing is much lower than it is for mathematicians.

[Tomas Skrivan]

Yeah, I feel that sometimes complains like that falls on deaf ears as people actually deciding on changing mathlib got used to lots of the idiosyncrasies.

[Kevin Buzzard]

My reading of the conversation about inner products was that Tomas said "for what I'm doing the following set up would be good" and the implicit response was "for other projects doing different things this wouldn't be good". But I might be misreading. Tomas never wants this max distance on a product but other people do

[Kevin Buzzard]

Maybe it's similar to how Tomas doesn't want to bundle things like group homomorphisms because they're inconvenient for FunProp but people doing other things think they're great.

I think it's basically impossible to make one system which is perfect for everyone

[Tomas Skrivan]

Kevin Buzzard said:

I think it's basically impossible to make one system which is perfect for everyone

Yeah I understand that and I use mathlib/Lean in a quite different way than most people so it makes sense I don't get my way and I try my best to find workarounds.

[Kevin Buzzard]

I agree that the inner product conversation just petered out though rather than people having a sensible discussion. Is there a way of taking it further e.g. making a PR or would this be very time-consuming?

[Tomas Skrivan]

I will draft a PR to mathlib if I find the time. The core of it will be this PR to PhysLean but I'm not sure about the downstream effects/generalizations in mathlib.

[Dominic Steinitz]

In my head, gradients are the differential 1-form of a 0-form. I thought someone was working on differential forms but maybe both my premises are wrong.

[Tomas Skrivan]

This you get already with fderiv, for f : X → ℝ you have (fderiv ℝ f x) : X →L[ℝ] ℝ which is effectively 1-form.

[Tomas Skrivan]

The goal of gradient is also include the identification (X →L[ℝ] ℝ) ≃ X given by inner product.

[Tomas Skrivan]

For example this expression often encountered in optimization x + s • ∇ f x type checks only if ∇ f x has the same type as x thus it can't be 1-form.

Same for ODE ẋ = ∇ f x. It makes sense only if x has the same type as ∇ f x

[Dominic Steinitz]

Do we not normally do this via a Riemannian metric? But I know they don't quite exist in Mathlib yet.

[Tomas Skrivan]

Well I'm doing everything only on vector spaces, so it needs inner product structure. But yes, on manifolds you need Riemannian metric.