feat(MeasureTheory): add MemLp.Const class and instances to unify p = ∞ and μ.IsFiniteMeasure cases

[JonBannon]

Although it is possible to ensure that, for example, the One instances for p=∞ and μ.IsFiniteMeasure are defeq, introducing an MemLp.Const typeclass removes the need to unfold extensively to check this definitional equality, improving performance. cf. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Lp.20constant.20function.20issue/with/537563137

This PR introduces the requisite class and associated instances.

---

[github-actions]

PR summary 07e431564c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ MemLp.Const
+ eLpNorm_const_lt_top
+ instance : MemLp.Const ∞ μ
+ instance [IsFiniteMeasure μ] : MemLp.Const p μ
+ memLpConst_iff_top_or_isFiniteMeasure_of_ne_zero
+ memLpConst_iff_zero_or_top_or_isFiniteMeasure
+ memLpConst_of_eq_zero_or_top_or_isFiniteMeasure
+ memLp_const_of_enorm

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.25)

Current number	Change	Type
4	1	large files

Current commit b8dd863c65
Reference commit 07e431564c

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[j-loreaux]

🤔 I do wonder whether or not it makes more sense to have the field in this class be p = ∞ ∨ IsFiniteMeasure μ. There's no other context in which we'll be able to have this class, right? The advantage is that it would allow to do case splits in proofs about this class. For instance, then indicatorConstLp could take an argument that μ s ≠ ∞ ∨ p = ∞.

I'm not sure how valuable this would be. Don't make this change without first consulting the opinions of others. It may not be a good idea.

[j-loreaux]

Suggested change

	/-- The class of constant Lp functions. Has only `p = ∞` and `μ.IsFiniteMeasure` instances. -/
	/-- A class which encodes that constant functions are members of `Lp`.
	This has instances when `p := ∞` or `μ.IsFiniteMeasure`. -/

[JonBannon]

🤔 I do wonder whether or not it makes more sense to have the field in this class be p = ∞ ∨ IsFiniteMeasure μ. There's no other context in which we'll be able to have this class, right? The advantage is that it would allow to do case splits in proofs about this class. For instance, then indicatorConstLp could take an argument that μ s ≠ ∞ ∨ p = ∞.

I'm not sure how valuable this would be. Don't make this change without first consulting the opinions of others. It may not be a good idea.

How to raise this issue? Should I more aggressively prod more people to review this PR, or does it rise to the level of a Zulip thread?

[j-loreaux]

@JonBannon ask on Zulip.

[j-loreaux]

It's looking pretty good, but I think we can do even better.

[j-loreaux]

Can you generalize the hypothesis of indicatorConstLp to hμs : p = ∞ ∨ μ s ≠ ∞ with minimal breakage. It would be nice to generalize the rest of this too, and it should be possible if you do that. For instance, where it gets used below in Lp.constL, one could assume MemLp.const p μ instead of μ.IsFiniteMeasure, then you could use Fact (1 ≤ p) to conclude p ≠ 0, and then you could use the disjunction I mentioned in another comment to conclude that p = ∞ ∨ μ.IsFiniteMeasure, which would then allow you to apply the necessary lemmas with a modified version of indicatorConstLp_univ.

[JonBannon]

This should work, but I'm having some trouble. I first made the following modification, which then allowed your suggested change to hμs to be introduced (not the one below, but the one in ndicatorConstLp) with no change to the proof.

lemma memLp_indicator_const (p : ℝ≥0∞) (hs : MeasurableSet s) (c : E)
    (hμsc : c = 0 ∨ p = ∞ ∨ μ s ≠ ∞) : MemLp (s.indicator fun _ => c) p μ := by
  rw [memLp_indicator_iff_restrict hs]
  obtain rfl | hμi | hμs := hμsc
  · exact MemLp.zero
  · rw [hμi]
    apply memLp_const
  · have := Fact.mk hμs.lt_top
    apply memLp_const

But after this change I'm facing a bunch of weird breakage below it because Lean doesn't like ∞=∞ instead of p=∞. So I'll keep plugging at this...