Design choice for an `MemLp.Const` class

Stream: mathlib4

[Jon Bannon]

In order to reduce the need for Lean to unfold definitions to find a One instance for LpSpaces in the p=infty versus IsFiniteMeasure case, we introduce in this PR the class

class MemLp.Const {α : Type u_1} (ε : Type u_2) {m0 : MeasurableSpace α} [ENorm ε] (p : ℝ≥0∞)
  (μ : Measure α) where
  eLpNorm_const_lt_top' (c : ε) (hc : ‖c‖ₑ ≠ ∞) : eLpNorm (fun _ ↦ c) p μ < ∞

Would it be better for the field in this class to just be the disjunction p = ∞ ∨ IsFiniteMeasure μ to allow for case splits in proofs?

See also the thread here.

[Jireh Loreaux]

@Eric Wieser do you have an opinion here? I guess one reason to maybe not do the disjunction is that, at least with the current definition of eLpNorm, the value is finite when p := 0 too. So if we use the class as listed above we could also have a MemLp.Const instance when p := 0.

[Eric Wieser]

If the motivation is to make proofs easier we should just have a theorem that concludes the Or

[Eric Wieser]

I don't think we should change the generality just to make proofs easier, the justification needs to be stronger for that.

[Yury G. Kudryashov]

Why do we need ε, not just α? Do you want to have an instance in the case ε is a subsingleton?

[Yury G. Kudryashov]

Otherwise it looks like everything depends on the norm of c only, so you can assume that c is a real number.

[Jon Bannon]

@Yury G. Kudryashov It seems @Jireh Loreaux is on board with what you said above, but I don't yet understand your point. Would you mind elaborating a bit?

[Yury G. Kudryashov]

If you define

class MemLp.Const {α : Type u_1} {m0 : MeasurableSpace α} (p : ℝ≥0∞)
  (μ : Measure α) where
  eLpNorm_const_lt_top' (c : Real) : eLpNorm (fun _ ↦ c) p μ < ∞

then it will imply your MemLp.Const for all \eps.