Turn `Complex.abs` into `Norm`

Stream: mathlib4

[Yaël Dillies]

Xavier Roblot said:

In any case, how would we do that explicitly?

1. Move the Norm Complex instance earlier.
2. Decide whether we duplicate basic norm API lemmas or move the NormedAddCommGroup Complex and NormedRing instances earlier.
3. Make all the Complex.abs lemmas be one-liners from norm lemmas.
4. Deprecate the Complex.abs lemmas.

[Xavier Roblot]

It would be interesting to know if there is a consensus that this is something we should do and if so, that this the way to do it.

[Bhavik Mehta]

I'm in favour of this

[David Loeffler]

I'd also be happy to see Complex.abs gotten rid of.

[Frédéric Dupuis]

Reversing the simp lemmas such as docs#Complex.norm_eq_abs should probably be its own step in that process.

[Yaël Dillies]

Frédéric, I think that can only be done after step 2 of my plan above. So maybe step 2bis

[Xavier Roblot]

Ok, so I'd be interested in working on this but I'll probably need some guidance. Would it be possible to move the relevant messages to a new topic? I tried to do it but I don't have the rights.

[Notification Bot]

7 messages were moved here from #PR reviews > #21454 Protect some results about Complex.abs by Johan Commelin.

[Johan Commelin]

Link is broken. This one should work: #PR reviews > #21454 Protect some results about `Complex.abs`

[Xavier Roblot]

So I made #21494 as a first step. This PR does the following:

• Create the new file Data/Complex/Norm with the minimal imports so that Complex.norm could be defined and related to Complex.abs.
• Move to Data/Complex/Norm all the results from Analysis/Complex/Basic.lean, where Complex.norm was defined, that depends only on the imports of Data/Complex/Norm.

This is only code moving. No results was changed in this PR except the definition of the norm that I changed to:

instance : Norm ℂ :=   ⟨fun z ↦ Real.sqrt (normSq z)⟩

so it still defeq to Complex.abs.

Still, we are already getting to step 2 in Yaël's plan above. Indeed, docs#Norm is defined in Mathlib.Analysis.Normed.Group.Basic which has some quite heavy imports. The file Mathlib.Data.Complex.Abs which would eventually be replaced by Mathlib.Data.Complex.Norm is imported by two files: Mathlib.Data.Complex.Order and Mathlib.Data.Complex.Exponential.

The file Mathlib.Data.Complex.Order is only imported by Mathlib.Analysis.Complex.Basic so the added imports would not cause any problem in this direction, but in the other direction of the file Mathlib.Data.Complex.Exponential, the new imports could make a significant difference.

So at this point we have to decide if adding these extra imports to all the basic Complex analysis files is acceptable or we should move the definition of Norm somewhere else to reduce the imports (and then, as mentioned by Yaël above), some API would probably need to be duplicated for the complex norm.

[Johan Commelin]

I think we could have a very lightweight file that introduces docs#Norm and similar notions, without any extra structure/axioms, just to provide the notation.

[Yaël Dillies]

Note that an extra option is to find a way to reduce the imports to Analysis.Normed.Group.Basic, which is independently useful

[Yaël Dillies]

Johan Commelin said:

I think we could have a very lightweight file that introduces docs#Norm and similar notions, without any extra structure/axioms, just to provide the notation.

Yes, but soon after you'll also want the very basic theorems... I am of the opinion that you should split the file a bit further down to make it useful

[Johan Commelin]

Notation classes for 0, 1, +, *, ^, etc are done at a very low level, and basic lemmas are in different files that import the notations. I think the same can be done here.

[Yaël Dillies]

Sure, but eg ‖a * b‖ = ‖a‖ * ‖b‖ for a b : ℂ is something we want really early on, I think

[Xavier Roblot]

If we prove early on IsAbsoluteValue Complex.norm, we should get all the basic properties that we need.

[Johan Commelin]

Yaël Dillies said:

Sure, but eg ‖a * b‖ = ‖a‖ * ‖b‖ for a b : ℂ is something we want really early on, I think

Right. But that doesn't have to live in Mathlib/Data/Norm.lean, whereas having that file provide the notation typeclass could work well imho.

[Yaël Dillies]

I am saying that having the notation and nothing is basically useless. Happy to be proven wrong :smiley:

[Kevin Buzzard]

But that's exactly what the situation is for most common notation, right? eg LE, Zero, Add, ...

[Xavier Roblot]

Anyway, I made #21541 to see what it would look like.

[Yaël Dillies]

Kevin Buzzard said:

But that's exactly what the situation is for most common notation, right? eg LE, Zero, Add, ...

file#Algebra/Group/Defs contains theorems, and those notations are much more foundational than norms.

[Johan Commelin]

It also doesn't provide new notation.

[Xavier Roblot]

I did some experiments and the imports of Analysis.Normed.Group.Basic could reduced to just:

import Mathlib.Analysis.Normed.Group.Seminorm
import Mathlib.Topology.Instances.ENNReal.Defs

if the two results

controlled_prod_of_mem_closure
controlled_prod_of_mem_closure_range

are moved somewhere else. So maybe a refactor of this file should be the first step.

[Johan Commelin]

Yeah, that sounds like an independently good idea

[Yaël Dillies]

Xavier Roblot said:

I did some experiments and the imports of Analysis.Normed.Group.Basic could reduced to just:

import Mathlib.Analysis.Normed.Group.Seminorm
import Mathlib.Topology.Instances.ENNReal.Defs

if the two results

controlled_prod_of_mem_closure
controlled_prod_of_mem_closure_range

are moved somewhere else. So maybe a refactor of this file should be the first step.

I should note that this doesn't reduce the transitive imports very much. Topology.Instances.ENNReal.Defs is unfortunately quite heavy

[Yaël Dillies]

I was the one adding the Topology.Instances.ENNReal.Defs import (so 115 extra transitive imports) in #20966 simply because to get access to docs#ENNReal.isOpenEmbedding_coe to prove docs#continuous_enorm. See https://github.com/leanprover-community/mathlib4/pull/20966/files#diff-67009df17b3a5774f47588bb4973789873c7d5227867d14f5adeede906f17e90R907-R908. Hopefully, we can split Topology.Instances.ENNReal.Defs so as to make this lemma available with less imports

[Yaël Dillies]

Alternatively, I was contemplating making the first few files about MetricSpace and NormedGroup topology-less, in the sense that we need to import the definition of a topological space and of a uniform space because that's part of the definition of a metric space, but we could try to import nothing more, and delay continuity results and similar to later files

[Xavier Roblot]

We could also move all the stuff about nnnorm and enorm in another file. Then, it would not be necessary to import Topology.Instances.ENNReal.Defs into Analysis.Normed.Group.Basic

[Yaël Dillies]

I am explicitly against that since I want people to think of (and prove theorems about!) norm, nnnorm and enorm on an equal footing. Else their APIs will drift apart beyond recognition

[Xavier Roblot]

Yeah, I agree that would probably not be a good idea.

[Xavier Roblot]

#21554 is a tentative to split Analysis.Normed.Group.Basic into three files.

[Xavier Roblot]

Now, that #21554 has been merged, I have modified accordingly #21494. In this PR, the definition of the complex norm is moved from Analysis.Complex.Norm to a new file Data.Complex.Norm with minimal imports (but with the definition of Norm still in Mathlib.Analysis.Normed.Group.Basic) together with all the results from Analysis.Complex.Norm that could be moved to the new file.

Since the plan is eventually to replace Data.Complex.Abs by Data.Complex.Norm, I have, as an experiment, done that and replacedData.Complex.Abs by Data.Complex.Norm in the two files that import Data.Complex.Abs. The result are here. If we think that this is acceptable, -- and in my opinion it is --, then it is not necessary to move the definition of Norm to a new file and it can stay in Mathlib.Analysis.Normed.Group.Basic.

[Yaël Dillies]

Looks great! Thanks, Xavier

[Xavier Roblot]

Note that the PR does not compile for the moment since the imports are not optimal. I'll fix that once there is a consensus that this is the way to do it.

[Xavier Roblot]

At this point, I think I need some guidance because I am not sure on how to proceed next. I made #21730 with

• All the basic results about Complex.abs proved directly for Complex.norm
• Complex.abs defined by

noncomputable abbrev abs (z : ℂ) : ℝ := ‖z‖

• All basic results about Complex.abs directly deduced from their Complex.norm counterparts.

Here, by basic results, I mean all the results in Data.Complex.Abs.

At this point, many things do not compile anymore mainly because Complex.abs was a docs#AbsoluteValue and that's not the case anymore. For example, let's have a look at Data.Complex.Orderaround L102. There was:

  have : 0 ≤ abs z := apply_nonneg abs z

that's easy, I can just replace it by

  have : 0 ≤ abs z := norm_nonneg z

and everything's fine. But then, a couple lines down (L109):

  rw [← neg_re, ← abs.map_neg, re_eq_abs]

Here, abs.map_neg worked because Complex.abs was a docs#AbsoluteValue, but I does not work anymore. I want to replace it with docs#norm_neg but that fails because, well, abs z is not ‖z‖. I can get around that using a rewrite lemma that replacesabs by ‖z‖ but that adds extra rewrites that we'll eventually have to delete when Complex.absis removed for good. So it does not feel like the right solution.

Thus, I'd like to ask: is there something I'm missing? Is there a better way to proceed?

[Ruben Van de Velde]

Does rw not see through an abbrev?

[Michael Rothgang]

Yaël Dillies said:

I am explicitly against that since I want people to think of (and prove theorems about!) norm, nnnorm and enorm on an equal footing. Else their APIs will drift apart beyond recognition

As a more explicit example, I'm currently generalising mathlib theorems from norm or nnnorm to enorm when possible, as that will include ENNReal. (In the carleson project, we would like to talk about e.g. L^p-norms of a function which can be infinite; this refactor is needed to make this not too painful.) So, I'd like to place enorm theorems next to nnnorm theorems (and even investigate removing the nnnorm ones for an enorm statement).

[Michael Rothgang]

#21670 is the next open PR towards that effort, by the way.

[Xavier Roblot]

Ruben Van de Velde said:

Does rw not see through an abbrev?

Nope.

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ‖z‖

The goal is

⊢ (-z).re = z.abs ↔ z ≤ 0

[Xavier Roblot]

Ok, so I found a way to proceed which I think is correct: for any result about Complex.abs, prove it first for the Complex.norm and then use it to prove directly the corresponding Complex.abs result. In this way, no rewrite from Complex.abs to Complex.norm is necessary and, eventually, we will just deprecate the Complex.abs results to their Complex.norm counterparts.

[Xavier Roblot]

The next PR in the series is #21730. It is a big one.

There is however a problem with MathlibTest.Bound.bound where a test is unsuccessful. This is due to the fact that Complex.abs used to be defined as a docs#AbsoluteValue and thus docs#AbsoluteValue.le_add could be used there. Since it is now defined as equal to Complex.norm, the test now fails. I am not sure about what is the best way to fix that... (I did reformulate the test in terms of Complex.norm though).

[Xavier Roblot]

Pinging @Geoffrey Irving that wrote the tactic bound

[Geoffrey Irving]

Fixing this requires registering the analogous norm lemmas with bound. For AbsoluteValue.le_add, this is almost but not quite docs#norm_sub_norm_le, so I think we need to add the new norm lemma.

[Xavier Roblot]

Ok. I’ll do that. I thought about doing something like that but I was wondering if there was a reason why these lemmas were not already tagged with ‘bound’.

[Xavier Roblot]

#21821

[Xavier Roblot]

The final PR is available #21995 and supersede the previous one.

[Johan Commelin]

Thanks a lot for doing this! I think the result looks really nice!