Operator norm

Stream: mathlib4

[Patrick Massot]

The following mystery is blocking calculus in mathlib4:

import Mathlib.Analysis.Calculus.ContDiffDef
import Mathlib.Analysis.Calculus.Deriv.Inverse
import Mathlib.Analysis.Calculus.MeanValue
import Mathlib.Analysis.NormedSpace.FiniteDimension
import Mathlib.Data.Nat.Choose.Cast

variable {𝕜 : Type _} [NontriviallyNormedField 𝕜] {Du Eu Fu Gu : Type u}
    [NormedAddCommGroup Du] [NormedSpace 𝕜 Du] [NormedAddCommGroup Eu] [NormedSpace 𝕜 Eu]
    [NormedAddCommGroup Fu] [NormedSpace 𝕜 Fu] [NormedAddCommGroup Gu] [NormedSpace 𝕜 Gu]

#check (Eu →L[𝕜] (Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu)

#check (Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu

set_option trace.Meta.synthInstance true in
#synth Norm (Du →L[𝕜] Fu)

#synth Norm ((Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu)


set_option trace.Meta.synthInstance true in
#synth Norm (Eu →L[𝕜] ((Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu))

[Ruben Van de Velde]

Not the operator norm again :see_no_evil:

[Patrick Massot]

Lean has no trouble finding the operator norm until (Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu but fails with Eu →L[𝕜] ((Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu)

[Patrick Massot]

This is the first error in !4#4532.

[Patrick Massot]

Ruben, you seem to be a specialist in this issue, it would be very nice to have a fix.

[Patrick Massot]

This file is the main remaining roadblock to restoring the calculus chapter in MIL.

[Ruben Van de Velde]

I'm not sure any such reputation is deserved, but I'll try to find some time later today

[Eric Wieser]

Is it able to find this instance if given the expression to construct it explicitly?

[Eric Wieser]

Answer: no :fear:

-- type mismatch
example : Norm (Eu →L[𝕜] ((Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu)) := ContinuousLinearMap.hasOpNorm

Going through the isDefEq trace suggests thar the problem is that itfound stuck MVar.

[Eric Wieser]

I think there's some weird universe problem:

set_option pp.universes true in
example : Norm (Eu →L[𝕜] ((Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu)) :=
    let foo : NormedAddCommGroup ((Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu) := by infer_instance
    ContinuousLinearMap.hasOpNorm

This has an error on both the last two lines, but the error goes away if you replace the last line with sorry

[Kevin Buzzard]

I'm assuming it's just a coincidence that mathlib's longest declaration name is about these objects.

[Eric Wieser]

Note that that instance is already a porting hack, so probably this is related

[Johan Commelin]

@Eric Wieser Why do you think it is related to universes?

[Eric Wieser]

Because the metavariable has an unresolved universe argument

[Eric Wieser]

And the error in the above code sample complains about unifying max ? ? with u

[Patrick Massot]

I pushed a hack feeding this instance into the first failing proof, but I need to give up on the next proof for now (the issue seems different). But working on this file is almost impossible because everything is so slow. So probably we can't avoid facing that issue for real.

[Kevin Buzzard]

   [tryResolve] ❌ RingHomIsometric (RingHom.id 𝕜) ≟ RingHomIsometric (RingHom.id ?m.51913)

:-(

I don't really know what a stuck metavariable is but this shows up a few times in the trace:

          [synthInstance] ❌ SeminormedAddCommGroup ((Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu) ▶
          [] ❌ ContinuousLinearMap.topologicalSpace =?= UniformSpace.toTopologicalSpace ▼
            [] ❌ ContinuousLinearMap.strongTopology (RingHom.id 𝕜) (Du →L[𝕜] Gu)
                  {S | Bornology.IsVonNBounded 𝕜 S} =?= UniformSpace.toTopologicalSpace ▼
              [] ❌ TopologicalSpace.induced FunLike.coe
                    (UniformOnFun.topologicalSpace (Du →L[𝕜] Fu) (Du →L[𝕜] Gu)
                      {S | Bornology.IsVonNBounded 𝕜 S}) =?= UniformSpace.toTopologicalSpace ▼
                [] ❌ { IsOpen := fun s ↦ ∃ s', IsOpen s' ∧ FunLike.coe ⁻¹' s' = s,
                      isOpen_univ := (_ : ∃ s', IsOpen s' ∧ FunLike.coe ⁻¹' s' = Set.univ),
                      isOpen_inter :=
                        (_ :
                          ∀ (s₁ s₂ : Set ((Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu)),
                            (∃ s', IsOpen s' ∧ FunLike.coe ⁻¹' s' = s₁) →
                              (∃ s', IsOpen s' ∧ FunLike.coe ⁻¹' s' = s₂) →
                                (fun s ↦ ∃ s', IsOpen s' ∧ FunLike.coe ⁻¹' s' = s) (s₁ ∩ s₂)),
                      isOpen_sUnion :=
                        (_ :
                          ∀ (S : Set (Set ((Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu))),
                            (∀ (t : Set ((Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu)),
                                t ∈ S → (fun s ↦ ∃ s', IsOpen s' ∧ FunLike.coe ⁻¹' s' = s) t) →
                              ∃ s', IsOpen s' ∧ FunLike.coe ⁻¹' s' = ⋃₀ S) } =?= UniformSpace.toTopologicalSpace ▼
                  [] ❌ { IsOpen := fun s ↦ ∃ s', IsOpen s' ∧ FunLike.coe ⁻¹' s' = s,
                        isOpen_univ := (_ : ∃ s', IsOpen s' ∧ FunLike.coe ⁻¹' s' = Set.univ),
                        isOpen_inter :=
                          (_ :
                            ∀ (s₁ s₂ : Set ((Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu)),
                              (∃ s', IsOpen s' ∧ FunLike.coe ⁻¹' s' = s₁) →
                                (∃ s', IsOpen s' ∧ FunLike.coe ⁻¹' s' = s₂) →
                                  (fun s ↦ ∃ s', IsOpen s' ∧ FunLike.coe ⁻¹' s' = s) (s₁ ∩ s₂)),
                        isOpen_sUnion :=
                          (_ :
                            ∀ (S : Set (Set ((Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu))),
                              (∀ (t : Set ((Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu)),
                                  t ∈ S → (fun s ↦ ∃ s', IsOpen s' ∧ FunLike.coe ⁻¹' s' = s) t) →
                                ∃ s', IsOpen s' ∧ FunLike.coe ⁻¹' s' = ⋃₀ S) } =?= PseudoMetricSpace.toUniformSpace.1 ▼
                    [] ✅ TopologicalSpace ((Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu) =?= TopologicalSpace ((Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu) ▶
                    [] ❌ TopologicalSpace.IsOpen =?= fun s ↦ ∃ s', IsOpen s' ∧ FunLike.coe ⁻¹' s' = s ▶
                    [onFailure] ❌ { IsOpen := fun s ↦ ∃ s', IsOpen s' ∧ FunLike.coe ⁻¹' s' = s,
                          isOpen_univ := (_ : ∃ s', IsOpen s' ∧ FunLike.coe ⁻¹' s' = Set.univ),
                          isOpen_inter :=
                            (_ :
                              ∀ (s₁ s₂ : Set ((Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu)),
                                (∃ s', IsOpen s' ∧ FunLike.coe ⁻¹' s' = s₁) →
                                  (∃ s', IsOpen s' ∧ FunLike.coe ⁻¹' s' = s₂) →
                                    (fun s ↦ ∃ s', IsOpen s' ∧ FunLike.coe ⁻¹' s' = s) (s₁ ∩ s₂)),
                          isOpen_sUnion :=
                            (_ :
                              ∀ (S : Set (Set ((Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu))),
                                (∀ (t : Set ((Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu)),
                                    t ∈ S → (fun s ↦ ∃ s', IsOpen s' ∧ FunLike.coe ⁻¹' s' = s) t) →
                                  ∃ s', IsOpen s' ∧ FunLike.coe ⁻¹' s' = ⋃₀ S) } =?= PseudoMetricSpace.toUniformSpace.1 ▼
                      [stuckMVar] found stuck MVar ?m.51846 : SeminormedAddCommGroup ((Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu)

[Eric Wieser]

I think a lot of these traces would become easier to navigate with set_option pp.proofs false or whatever the name is

[Kevin Buzzard]

Maybe the problem is this:

/-
[tryResolve] ❌ RingHomIsometric (RingHom.id 𝕜) ≟ RingHomIsometric (RingHom.id ?m.52368) ▶

LHS

@RingHomIsometric 𝕜 𝕜 DivisionSemiring.toSemiring DivisionSemiring.toSemiring NormedField.toNorm NormedField.toNorm
  (RingHom.id 𝕜) : Prop

RHS

@RingHomIsometric ?m.52368 ?m.52368 Ring.toSemiring Ring.toSemiring SeminormedRing.toNorm SeminormedRing.toNorm
  (RingHom.id ?m.52368) : Prop

-/

[Eric Wieser]

Does setting a default instance on RingHomIsometric for RingHom.id help at all?

[Kevin Buzzard]

(The above issue would align with the general picture of Lean 4 being a bit crap at the way we've set up ring theory and now this problem is leaking over to anything which uses fields :-/)

[Kevin Buzzard]

Eric Wieser said:

Does setting a default instance on RingHomIsometric for RingHom.id help at all?

Yes, it changes the issue to

              [] ❌ apply smulCommClass_self to SMulCommClass 𝕜 𝕜 Fu ▼
                [tryResolve] ❌ SMulCommClass 𝕜 𝕜 Fu ≟ SMulCommClass ?m.53239 ?m.53239 ?m.53240

[Eric Wieser]

That failure is expected, that's the wrong instance

[Kevin Buzzard]

LHS is @SMulCommClass 𝕜 𝕜 Fu SMulZeroClass.toSMul SMulZeroClass.toSMul : Prop, RHS is @SMulCommClass ?m.53239 ?m.53239 ?m.53240 MulAction.toSMul MulAction.toSMul : Prop

[Eric Wieser]

I assume it's stuck because MulAction.toSMul on the RHS has more metavariables?

[Eric Wieser]

Is the LHS metavariable-free?

[Kevin Buzzard]

Sorry I'm finding it a bit hard to read these traces, ultimately Lean seems to reduce it to IsScalarTower 𝕜 𝕜 Fu. The "goal" of the traces keeps changing and I have to unfold things to find out where we're going

[Kevin Buzzard]

And

              [] ❌ apply IsScalarTower.left to IsScalarTower 𝕜 𝕜 Fu ▼
                [tryResolve] ❌ IsScalarTower 𝕜 𝕜 Fu ≟ IsScalarTower ?m.53455 ?m.53455 ?m.53456

fails because LHS is @IsScalarTower 𝕜 𝕜 Fu Algebra.toSMul SMulZeroClass.toSMul SMulZeroClass.toSMul : Prop and RHS is @IsScalarTower ?m.53455 ?m.53455 ?m.53456 MulAction.toSMul MulAction.toSMul MulAction.toSMul : Prop. And at this point it goes back and tries to find another way to make NormedSpace 𝕜 Fu other than _inst_2 :-/

[Kevin Buzzard]

Eric Wieser said:

I assume it's stuck because MulAction.toSMul on the RHS has more metavariables?

It does have more metavariables: @MulAction.toSMul ?m.55677 ?m.55678 CommMonoid.toMonoid ?m.55680 : SMul ?m.55677 ?m.55678

[Kevin Buzzard]

OK so here's some kind of solution:

import Mathlib.Analysis.Calculus.ContDiffDef
import Mathlib.Analysis.Calculus.Deriv.Inverse
import Mathlib.Analysis.Calculus.MeanValue
import Mathlib.Analysis.NormedSpace.FiniteDimension
import Mathlib.Data.Nat.Choose.Cast

variable {𝕜 : Type v} [NontriviallyNormedField 𝕜] {Du Eu Fu Gu : Type u}
    [NormedAddCommGroup Du] [NormedSpace 𝕜 Du] [NormedAddCommGroup Eu] [NormedSpace 𝕜 Eu]
    [NormedAddCommGroup Fu] [NormedSpace 𝕜 Fu] [NormedAddCommGroup Gu] [NormedSpace 𝕜 Gu]

instance : RingHomIsometric (RingHom.id 𝕜) := inferInstance

instance : SMulCommClass 𝕜 𝕜 Fu := inferInstance

#synth Norm (Eu →L[𝕜] ((Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu)) -- works

If you comment out either instance then #synth fails. Should that happen? I am only adding instances which typeclass inference can already find. That's a bit weird.

[Patrick Massot]

It's not super weird since it probably change the order in which instances are tried.

[Kevin Buzzard]

Oh OK. We also do this sort of thing occasionally in Lean 3, e.g. here in data.rat.basic (and I didn't really understand why we had to do that either)

[Patrick Massot]

It doesn't mean this isn't a problem. I only meant that it's not paranormal.

[Kevin Buzzard]

"Lean does not do magic" -- Kenny Lau

[Ruben Van de Velde]

I seem to have it building, but please don't judge how :)