Skip to content

feat(Analysis/Distribution): Sobolev distributions#36754

Open
mcdoll wants to merge 10 commits intoleanprover-community:masterfrom
mcdoll:mem_sobolev
Open

feat(Analysis/Distribution): Sobolev distributions#36754
mcdoll wants to merge 10 commits intoleanprover-community:masterfrom
mcdoll:mem_sobolev

Conversation

@mcdoll
Copy link
Copy Markdown
Member

@mcdoll mcdoll commented Mar 16, 2026

This is the first part of the definition of the Sobolev space. Here we only define the predicate MemSobolev, the subsequent PR will define the space of all Sobolev functions with the correct topology.

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 16, 2026 •
edited
Loading

PR summary 4ec5d95aa6

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Analysis.Distribution.Sobolev (new file) 2685

Declarations diff

+ MemSobolev
+ MemSobolev.add
+ MemSobolev.fourierMultiplierCLM_of_bounded
+ MemSobolev.fourier_memL1
+ MemSobolev.laplacian
+ MemSobolev.lineDerivOp
+ MemSobolev.mono
+ MemSobolev.smul
+ _root_.SchwartzMap.memSobolev
+ besselPotential
+ besselPotential_besselPotential_apply
+ besselPotential_compL_besselPotential
+ besselPotential_neg_apply_eq_iff
+ besselPotential_neg_one_lineDerivOp_eq
+ besselPotential_neg_two_laplacian_eq
+ besselPotential_zero
+ fourier_besselPotential_eq_smulLeftCLM_fourierInv_apply
+ memSobolev_besselPotential_iff
+ memSobolev_two_iff_fourier
+ memSobolev_zero
+ memSobolev_zero_iff
+ memSobolev_zero_two_iff_fourier

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

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

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

Increase in tech debt: (relative, absolute) = (3.00, 0.00)
Current number Change Type
6898 3 backward.isDefEq

Current commit 107260ab29
Reference commit 4ec5d95aa6

You can run this locally as

./scripts/reporting/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).

@github-actions github-actions bot added the t-analysis Analysis (normed *, calculus) label Mar 16, 2026
@mcdoll mcdoll added the WIP Work in progress label Mar 16, 2026
@mcdoll mcdoll removed WIP Work in progress labels Mar 17, 2026
j-loreaux
j-loreaux reviewed Mar 24, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@j-loreaux j-loreaux left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this looks quite reasonable, although I did not look closely at the proof techniques other than that they seemed to make sense, but I would like to get someone more expert in this area to have a look.

Maybe @grunweg would be willing?

@j-loreaux j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 24, 2026
@j-loreaux j-loreaux requested a review from grunweg March 24, 2026 17:40
@mcdoll mcdoll removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 25, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 30, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Mar 30, 2026

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

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 30, 2026
@j-loreaux
Copy link
Copy Markdown
Contributor

j-loreaux commented Mar 31, 2026

another ping for @grunweg. Michael, if you don't have time, just let me know and I'll try to find someone else.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@j-loreaux j-loreaux j-loreaux left review comments

@grunweg grunweg Awaiting requested review from grunweg

Assignees

@j-loreaux j-loreaux

Labels

t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@mcdoll @j-loreaux