Lp constant function issue

Stream: mathlib4

[Jon Bannon]

Suppose we have

variable {α : Type*} {m : MeasurableSpace α} {μ : Measure α}
variable {R : Type*} [NormedRing R]

For general p, we have constant functions in Lp R p μ provided we have IsFiniteMeasure μ. This requirement is unnecessary if p= \infty. There are many situations where we are going to want essentially bounded constant functions where the measure isn't finite, and to have an associated One instance in this case. How to best handle this so that we don't later end up with colliding One instances when we have L\infty over a finite measure space?

[Aaron Liu]

make the One instances defeq?

[Aaron Liu]

if you don't do anything weird this should just be automatic

[Jon Bannon]

I think they will be, but @Jireh Loreaux was wondering whether it would be better to generalize Lp.const to take either a finite measure or have p := ∞ (solved with an autoParam so the user need never supply it)

[Aaron Liu]

like (small : p = ⊤ ∨ IsFiniteMeasure μ := by first | exact Or.inl rfl | exact Or.inr inferInstance)?

[Eric Wieser]

Aaron Liu said:

make the One instances defeq?

This is safe, but you still end up having to repeat every lemma / downstream instance

[Eric Wieser]

Another option would be to instroduce an Lp.HasConst typeclass, instantiated for both cases

[Jireh Loreaux]

Eric Wieser said:

Aaron Liu said:

make the One instances defeq?

This is safe, but you still end up having to repeat every lemma / downstream instance

The thing I was worried about for this was actually performance. In particular, in the case when p := ∞ and μ.IsFiniteMeasure, then there would be two One instances, and Lean may have to unfold a lot sometimes to see they are equal (e.g., if one of them is embedded in a NormedCommRing instance).

[Eric Wieser]

I think that unfolding is not all that different to what it has to do anyway for two different paths fromNormedCommRing