feat(Analysis/Distribution): the Laplacian on Schwartz functions

[mcdoll]

We introduce a notation type-class for the Laplacian, change the definition of InnerProductSpace.laplacian to Laplacian.laplacian and define the Laplacian using the sum of second derivatives on Schwartz functions.
We define an abstract Laplacian for any space with LineDeriv in order to avoid duplication for other function spaces (in particular, this will be reused for the tempered distribution Laplacian).

---

• depends on: chore(Analysis/Distribution): split off derivatives from SchwartzSpace and create new folder #34027

[github-actions]

PR summary bb55063693

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
12 files Mathlib.Analysis.Complex.Harmonic.Analytic Mathlib.Analysis.Complex.Harmonic.MeanValue Mathlib.Analysis.Complex.JensenFormula Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction Mathlib.Analysis.Complex.ValueDistribution.CountingFunction Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem Mathlib.Analysis.InnerProductSpace.Harmonic.Basic Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions Mathlib.Analysis.InnerProductSpace.Laplacian Mathlib.Analysis.Polynomial.MahlerMeasure Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage Mathlib.NumberTheory.MahlerMeasure	1
Mathlib.Analysis.Distribution.Laplacian (new file)	2662

---

Declarations diff

+ InnerProduct.laplacian
+ Laplacian
+ LineDerivLeftAdd
+ LineDerivLeftSMul
+ bilinearLineDerivTwo
+ instLineDerivLeftAdd
+ instLineDerivLeftSMul
+ instLineDerivSMul'
+ integral_bilinear_laplacian_right_eq_left
+ integral_clm_comp_laplacian_right_eq_left
+ integral_mul_laplacian_right_eq_left
+ integral_smul_laplacian_right_eq_left
+ laplacianCLM
+ laplacianCLM_eq
+ laplacianCLM_eq'
+ laplacianCLM_eq_sum
+ laplacian_apply
+ laplacian_eq_sum
+ tensorLineDerivTwo
+ tensorLineDerivTwo_canonicalCovariantTensor_eq_sum
+ tensorLineDerivTwo_eq_lineDerivOp_lineDerivOp
++ instLaplacian
- laplacian

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.

---

No changes to technical debt.

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).

[sgouezel]

Thanks, I am much more happy with the new approach!

[sgouezel]

This is not up to date, right?

[mcdoll]

I think (noting the fact that the basic file for Schwartz functions is too big (again)), that I will factor out all of the derivatives statements and then put the Laplacian in that new file. Seems more sensible from the import graph than just having the Laplacian in a separate file.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• chore(Analysis/Distribution): split off derivatives from SchwartzSpace and create new folder #34027
  By Dependent Issues (🤖). Happy coding!