Lambda notation for bundled morphisms

Stream: mathlib4

[Tomas Skrivan]

Now that fun_prop is in mathlib it would be worth considering adopting lambda notation for bundled morphisms e.g. fun x =>L[ℝ] x + 3•x. When we get fun_prop compiled my hope is that the additional overhead of reproving function property would be minimal.

fun_prop can compute derivatives via HasFDerivAt, consider this example:

#check ((by fun_prop (disch:=assumption)) : (@HasFDerivAt ℝ _ _ _ _ _ _ _ (fun x : ℝ => (x+3)*(x*x + 1)⁻¹) _ a))

which results in

(_ : HasFDerivAt (fun y => (y + 3) * (y * y + 1)⁻¹)
  ((a + 3) •  ContinuousLinearMap.comp (-((ContinuousLinearMap.mulLeftRight ℝ ℝ) (a * a + 1)⁻¹) (a * a + 1)⁻¹)
    (a • ContinuousLinearMap.id ℝ ℝ + a • ContinuousLinearMap.id ℝ ℝ) +  (a * a + 1)⁻¹ • ContinuousLinearMap.id ℝ ℝ)  a)

using lambda notation for bundled morphisms this would become

(_ : HasFDerivAt (fun y => (y + 3) * (y * y + 1)⁻¹)
     (fun dx =>L[ℝ] (((a + 3) • (-(a • dx + a • dx) * (a * a + 1)⁻¹ * (a * a + 1)⁻¹)  +  (a * a + 1)⁻¹ • dx)
     a)

I'm curious in people's opinion if this should be pursuit or not. The #2202 would be quite relevant for this, but likely a lot of work.

[Geoffrey Irving]

That lambda notation is quite nice. Currently I solve this with a huge number of abbreviation defs, which is way messier.

[Tomas Skrivan]

Do you end up with something like APL :) ? Point free notation is nice until it isn't.

[Geoffrey Irving]

No, it’s not really point free: https://github.com/girving/ray/blob/48d737369e856f925aa050a317d10ae95726804a/Ray/AnalyticManifold/Inverse.lean#L139

[Geoffrey Irving]

Just naming all the intermediate linear maps.

[Geoffrey Irving]

I mean, it’s not point-free if you consider “dx” a “point”.

[Eric Wieser]

@Geoffrey Irving, are you aware of ∘L notation for composition?

[Eric Wieser]

@Tomas Skrivan: is there any hope of this working for bi- or tri-linear maps, perhaps with nested binders?

[Tomas Skrivan]

I definitely had it at some point, you could write

fun (x y : K) =>L[K] x * y  :  K →L[K] K →L[K] K

[Tomas Skrivan]

I think it boils down to providing this theorem

@[fun_prop]
theorem clm_mk' (f : X → Y → Z) (hf : Continuous (fun (x,y) => f x y)) (hf₁ : ∀ y, IsLinearMap (f · y)) (hf₁ : ∀ x, IsLinearMap (f x ·)) :
    IsContinuousLinearMap R (fun x => fun y =>L[K] f x y) := sorry

[Tomas Skrivan]

On notation side I just used expandExplicitBinders

[Patrick Massot]

This looks promising. It only needs to use ↦ to become usable.

[Tomas Skrivan]

No problem :)

[Geoffrey Irving]

Eric Wieser said:

Geoffrey Irving, are you aware of ∘L notation for composition?

I was not! Thank you!