feat: define Sobolev Spaces

[faenuccio]

Nothing to see yet.

---

• [ ] depends on: #32250

[github-actions[bot]]

PR summary 45f9a2993d

Import changes exceeding 2%

%	File
+32.20%	Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
+27.43%	Mathlib.Analysis.Distribution.Distribution
+27.46%	Mathlib.Analysis.Distribution.TestFunction

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Distribution.ContDiffMapSupportedIn	1531	2024	+493 (+32.20%)
Mathlib.Analysis.Distribution.TestFunction	1595	2033	+438 (+27.46%)
Mathlib.Analysis.Distribution.Distribution	1597	2035	+438 (+27.43%)

Import changes for all files

Files	Import difference
Mathlib.Analysis.Distribution.Distribution Mathlib.Analysis.Distribution.TestFunction	438
Mathlib.Analysis.Distribution.ContDiffMapSupportedIn	493
Mathlib.Analysis.Distribution.WeakDeriv (new file)	2034
Mathlib.Analysis.FunctionalSpaces.Sobolev.Basic (new file)	2039

---

Declarations diff

+ HasWTaylorSeriesUpTo + HasWeakDeriv + IsRegular + IsRepresentedBy + LocallyIntegrableOn.smul + MeasureTheory.ae_eq_iff + MemLp + MemSobolev.ae_eq + MemSobolev.aestronglyMeasurable + MemSobolev.indicator + MemSobolev.restrict + PiLp.instENorm + Set.EqOn.ae_eq + Set.EqOn.ae_eq_restrict + Sobolev + _root_.hasWTaylorSeriesUpTo_neg + _root_.locallyIntegrableOn_neg_iff + _root_.locallyIntegrableOn_smul_iff + _root_.locallyIntegrableOn_smul_iff' + coeFn_mk + coeFn_toSobolev + coe_mk + const + differentiable + differentiable_withOrder + ext + fderivLM_ofSupportedIn + fderivWithOrderLM_ofSupportedIn + hasWTaylorSeriesUpTo_congr_ae + hasWeakDeriv_congr_ae + hasWeakDeriv_of_ae + hasWeakDeriv_zero + hasWeakderiv_const + instCoeFun + instance [hμ : IsLocallyFiniteMeasure μ] : IsLocallyFiniteMeasure (μ.restrict Ω) + integrable_smul + integralAgainstBilinCLM_eq_zero + integralAgainstBilinLM_eq_zero + integralAgainstBilinLM_ofSupportedIn + isRepresentedBy_congr_ae + isRepresentedBy_of_ae + isRepresentedBy_zero + iteratedFDerivCLM + lineDerivCLM_eq_withOrder + lineDerivWithOrderCLM_apply_of_gt + lineDerivWithOrderCLM_apply_of_le + locallyIntegrableOn_succ + locallyIntegrableOn_zero + memLp + memSobolev + memSobolev_congr_ae + memSobolev_zero + mem_sobolev_iff_memSobolev + mem_sobolev_iff_sobolevNorm_lt_top + mono + mono_exponent + mono_k + mono_p_of_measure_lt_top + norm_integralAgainstBilinLM_le + ofFun + ofFunWithOrder + ofFunWithOrder_ae_congr + ofFunWithOrder_apply + ofFunWithOrder_of_not_locallyIntegrable + ofFunWithOrder_zero + ofFun_add + ofFun_ae_congr + ofFun_apply + ofFun_inj + ofFun_neg + ofFun_of_not_locallyIntegrable + ofFun_smul + ofFun_zero + out + postcompLM + postcompLM_apply + postcompLM_ofSupportedIn + seminorm_fderivLM + seminorm_fderivWithOrderLM_le + shrink_measure + sobolevNormAux + sobolevNorm_lt_top_iff + toSobolev + toSobolev_add + toSobolev_coeFn + toSobolev_congr + toSobolev_eq_toSobolev_iff + toSobolev_neg + toSobolev_sub + toSobolev_val + toSobolev_zero + weakDeriv + weakDeriv_add + weakDeriv_apply + weakDeriv_congr_ae + weakDeriv_const + weakDeriv_neg + weakDeriv_of_not_locallyIntegrableOn + weakDeriv_smul + weakDeriv_sub + weakDeriv_zero ++ MemSobolev ++ aestronglyMeasurable ++ continuous ++ fderivCLM_apply ++ fderivCLM_eq_of_scalars ++ fderivCLM_eq_withOrder ++ fderivLM ++ fderivLM_apply ++ fderivLM_eq_of_scalars ++ fderivLM_eq_withOrder ++ fderivWithOrderCLM ++ fderivWithOrderCLM_apply ++ fderivWithOrderCLM_apply_of_gt ++ fderivWithOrderCLM_apply_of_le ++ fderivWithOrderCLM_eq_of_scalars ++ fderivWithOrderLM ++ fderivWithOrderLM_apply ++ fderivWithOrderLM_apply_of_gt ++ fderivWithOrderLM_apply_of_le ++ fderivWithOrderLM_eq_of_scalars ++ integrable ++ integrable_bilin ++ integralAgainstBilinCLM ++ integralAgainstBilinCLM_apply ++ integralAgainstBilinLM ++ integralAgainstBilinLM_apply ++ lineDerivCLM ++ lineDerivCLM_apply ++ lineDerivWithOrderCLM ++ lineDerivWithOrderCLM_apply ++ memLp_top ++ mono_measure ++ sobolevNorm ++ stronglyMeasurable ++ zero +++ fderivCLM ++++ neg ++++ sub +++++ add +++++ smul - injective_toBoundedContinuousFunctionCLM - instance : T3Space 𝓓^{n}(Ω, F) - mkCLM - toBoundedContinuousFunctionCLM - toBoundedContinuousFunctionCLM_eq_of_scalars

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

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• leanprover-community/mathlib4#32250 By Dependent Issues (🤖). Happy coding!

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.