ch5.5 - two definitions of |.|

Stream: Analysis I

[Rado Kirov]

Screenshot 2025-09-12 at 7.01.14 AM.png

(Sometimes I feel Lean is just trolling me :)) After some more hovering around turns out somehow we ended up with two incompatible definitions of |.|

the one I am working with generally coming from LinearOrder Real (I think)

@_root_.abs Real inst_conditionallyCompleteLattice.toLattice addGroup_inst (x ^ n * x) : Real

the one that abs_mul from mathlib creates

@_root_.abs Real instDistribLatticeOfLinearOrder.toLattice instField.toDivisionRing.toAddGroupWithOne.toAddGroup
  (x ^ n * x) : Real

(note noone of those are the custom abs in ch5.4, which we have swapped for mathlib |.| at this point, while still working with custom Reals)

I unblocked myself by copying over the custom proof I have from chapter 4 for abs_mul, but this would be a stumbling block for future users, so would like to contribute a fix or hint once I understand this better.

[Aaron Liu]

Probably some typeclass diamond

[Rado Kirov]

Do you think this is 1) general mathlib issue, 2) issue with the setup for Reals in the companion 3) issue with the proof I am writing.

[Rado Kirov]

I guess 4) non-issue, just don't use abs_mul

[Ruben Van de Velde]

If you control-click the two inst* expressions you found by hovering, are they both in mathlib?

[Kevin Buzzard]

docs#inst_conditionallyCompleteLattice docs#instDistribLatticeOfLinearOrder

[Kevin Buzzard]

Looks like the first one isn't in mathlib so maybe is defined in the analysis project and is causing trouble.

[Aaron Liu]

Well the second one is forgetful inheritance so we would need to see the linear order instance it's taking to find out if it's causing trouble

[Rado Kirov]

The instance of the first one is defined in the Analysis project, but the definition of ConditionallyCompleteLattice is in mathlib.

https://github.com/teorth/analysis/blob/main/analysis/Analysis/Section_5_5.lean#L321-L326
and
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/ConditionallyCompleteLattice/Basic.html

the second one similarly starts with an instance of LinearOrder in Analysis here - https://github.com/teorth/analysis/blob/main/analysis/Analysis/Section_5_4.lean#L200-L206 and through some other chain build abs in a not defeq way.

[Rado Kirov]

Real.inst_conditionallyCompleteLattice is towards the end of the file so not sure if we even need it for anything, so will try to remove it.

[Rado Kirov]

Yep, no errors in 5.5 or 5.6 so far after removing inst_conditionallyCompleteLattice. AFAIKT, that instance was added to show that we can have mathlibs sSup work on all custom Real sets. At some point we will be swapping with mathlib R so that instance doesn't seem important, other than showing that it is possible (albeit at the cost of picking up two incompatible |.|)

[Aaron Liu]

Rado Kirov said:

Real.inst_conditionallyCompleteLattice is towards the end of the file so not sure if we even need it for anything, so will try to remove it.

oh yeah that's the bad instance

[Aaron Liu]

this one? https://github.com/teorth/analysis/blob/31e7e41b5fd092c2ab10ad3747ec4245f54712a1/analysis/Analysis/Section_5_5.lean#L320-L325

[Aaron Liu]

the problem is docs#conditionallyCompleteLatticeOfsSup

[Aaron Liu]

it explains why it's bad in the docstring

[Terence Tao]

It might be useful for the chapter 5 epilogue but I haven’t playtested this. But I would hope there is some way to impose this structure on Real that doesnt cause diamonds

[Terence Tao]

Does this work better?

/-- Use the `sSup` operation to build a conditionally complete lattice structure on `Real`-/
noncomputable instance Real.inst_conditionallyCompleteLattice :
    ConditionallyCompleteLattice Real :=
  conditionallyCompleteLatticeOfLatticeOfsSup Real
  (by intros; solve_by_elim [ExtendedReal.sup_of_bounded])

[Aaron Liu]

Terence Tao said:

Does this work better?

/-- Use the `sSup` operation to build a conditionally complete lattice structure on `Real`-/
noncomputable instance Real.inst_conditionallyCompleteLattice :
    ConditionallyCompleteLattice Real :=
  conditionallyCompleteLatticeOfLatticeOfsSup Real
  (by intros; solve_by_elim [ExtendedReal.sup_of_bounded])

maybe

[Aaron Liu]

I'll have a look at what fields we have here

[Aaron Liu]

no actually that should probably fix the diamond

[Aaron Liu]

assuming you don't also have some other diamond

[Terence Tao]

The docstring docs#conditionallyCompleteLatticeOfLatticeOfsSup seems to discourage its use which is probably why I didn't use it initially

[Aaron Liu]

the best thing to do is to provide both sSup and sInf yourself

[Aaron Liu]

this doesn't seem to hard

[Aaron Liu]

but for sSup and sInf on the reals you really don't care about the defeqs

[Aaron Liu]

so it probably doesn't matter

[Terence Tao]

In the file I defined sSup explicitly but didn't bother with sInf, was planning to outsource that to the conditionallyCompleteLattice instance

[Terence Tao]

yeah I doubt that defeq for either is going to be relevant for anything

[Terence Tao]

I'll let @Rado Kirov take the lead on seeing if this patches the problem (if so, please send an appropriate PR).

[Rado Kirov]

Does this work better?

Yes, that fixes it. Should I send PR with just that or attempt to define sInf and skip conditionallyCompleteLattice?

[Rado Kirov]

OOC, this is my first diamond issue in Lean, so would like to learn a bit more about what is happening.

What I can tell so far

• the |.| notation is driven by the abs function which needs [Lattice α] instance (because lattice gives max and abs is max of x and -x.
• in the companion code we provide two other type class instances
  • LinearOrder pretty early on in 5.4
  • ConditionallyCompleteLattice
• each one of those independently creates a Lattice instance automatically.
  • LinearOrder creates instance of DistribLattice which extends Lattice
  • ConditionallyCompleteLattice straight up extends Lattice

So now Lean's type class search algorithm finds two instances of Lattice Real. What I don't get is how come the original statement theorem Real.pow_abs (x:Real) (n:ℕ) : |x|^n = |x^n| picked up the second instance, while the mathlib abs_mul theorem picks up the first?

I see how the fix going from conditionallyCompleteLatticeOfLatticeOfsSup to conditionallyCompleteLatticeOfLatticeOfsSup fixes the problem, because the second takes the already existing Lattice instance and persumably uses it instead of creating a new Lattice insteance.

I don't follow what are the concerns left with that solution?

the best thing to do is to provide both sSup and sInf yourself

why is this better than using conditionallyCompleteLatticeOfLatticeOfsSup?

yeah I doubt that defeq for either is going to be relevant for anything

defeq between which objects?

[Rado Kirov]

https://github.com/teorth/analysis/pull/355

[Kevin Buzzard]

Rado Kirov said:

What I don't get is how come the original statement theorem Real.pow_abs (x:Real) (n:ℕ) : |x|^n = |x^n| picked up the second instance, while the mathlib abs_mul theorem picks up the first?

You can't control the typeclass inference algorithm, it's solving some big logic problem using the facts it knows at the time it has to solve it, in the order which the system finds them when answering this specific question, and the only thing you can guarantee is that once it finds a solution, it stops looking. So if you use different definitions or theorems which have different combinations of typeclass assumptions (and remember that mathlib will have a gazillion different classes which extend LE, and each lemma or definition will use precisely the minimal connection needed to make the lemma valid) and if you have a diamond then there's no way to guarantee that all these different theorems are going to find the same lattice structure if there are two non-syntactically-equal lattice structures in the system.

I don't follow what are the concerns left with that solution?

Is there definitely only one max,min,sSup,sInf etc etc in the system, up to syntactic equality?
All data fields definitely match?

[Terence Tao]

@Rado Kirov I think your analysis of the situation is broadly correct. Tools such as docs#conditionallyCompleteLatticeOfLatticeOfsSup take advantage of the mathematical fact that in a lattice, one can define sInf in terms of sSup in a moderately complicated fashion (basically, the sInf of a set E is the sSup of the lower bounds of E). However, if one does so, the actual definition of sInf is likely to be a mess, so that one would not be advised to unfold sInf for instance, and that any statement involving sInf would probably need to be proven via the ConditionallyCompleteLattice API rather than the literal definition of sInf (this API for instance will tell you that sInf E is the greatest lower bound on E as long as E is non-empty and bounded from below). But in the case of Real, this is basically what one wants to do anyways, so there should be no harm in sending a PR with the proposed fix.

[Rado Kirov]

Thank you both for the detailed answers! The PR is sent.

Is there definitely only one max,min,sSup,sInf etc etc in the system, up to syntactic equality?

I think with the PR there is only a single Lattice Real so single max and min, and a single ConditionallyCompleteLattice - so single sSup sInf. The trick was passing the existing Lattice instance into the other ConditionallyCompleteLattice instance constructor method.

There are separate concerns around sInf and that method, but these are moot in the context of this project it seems.