[Merged by Bors] - feat: shorthand lemmas for the L1 norm

[eric-wieser]

These are consistent with the existing lemmas about the L2 norm.

---

[github-actions]

PR summary 51a921e5b8

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ dist_eq_of_L1
+ edist_eq_of_L1
+ nndist_eq_of_L1
+ nnnorm_eq_of_L1
+ norm_eq_of_L1
+ prod_dist_eq_of_L1
+ prod_edist_eq_of_L1
+ prod_nndist_eq_of_L1
+ prod_nnnorm_eq_of_L1
+ prod_norm_eq_of_L1

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.

---

Decrease in tech debt: (relative, absolute) = (3.00, 0.00)

Current number	Change	Type
4828	-3	porting notes

Current commit 51a921e5b8
Reference commit 504007f6f7

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]

You could clean up the Prod versions (as well as the L2 versions) using only simp like I have done. I think it's much nicer to do it that way. It was the rfl in

  simp_rw [dist_eq_norm, prod_norm_eq_of_L1]
  rfl

that particularly caught my eye. This is exactly using the defeq where we have the simp lemma that explicitly sees through this defeq on purpose.

Otherwise, this is fine.

bors d+

[j-loreaux]

These could be a single section since they share the same variables. But if you prefer to keep them separate for the sake of readability that's fine.

[eric-wieser]

This file is a bit of a mess section-wise, so I'd prefer to insulate myself from any other typeclasses floating around.

[j-loreaux]

Suggested change

	theorem nnnorm_eq_of_L1 (x : PiLp 1 β) : ‖x‖₊ = ∑ i : ι, ‖x i‖₊ :=
	NNReal.eq <| by push_cast; exact norm_eq_of_L1 x
	theorem nnnorm_eq_of_L1 (x : PiLp 1 β) : ‖x‖₊ = ∑ i : ι, ‖x i‖₊ := by
	simp [nnnorm_eq_sum]

[j-loreaux]

Suggested change

	theorem nndist_eq_of_L1 (x y : PiLp 1 β) : nndist x y = ∑ i, nndist (x i) (y i) :=
	NNReal.eq <| by push_cast; exact dist_eq_of_L1 _ _
	theorem nndist_eq_of_L1 (x y : PiLp 1 β) : nndist x y = ∑ i, nndist (x i) (y i) := by
	simp [nndist_eq_nnnorm, nnnorm_eq_of_L1]

[mathlib-bors]

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[eric-wieser]

It was the rfl in [...] that particularly caught my eye.

I've removed this, it was copy-pasted from the L2 version, presumably predating the simp lemma.

I slightly prefer the push_cast proof, because:

• It's slightly faster
• It makes it a little harder for the norm and nnnorm lemmas to go out of sync.

[j-loreaux]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style