Skip to content

feat(MeasureTheory): add Resolvent (Stieltjes/Cauchy) Transform #37245

Open
DavidLedvinka wants to merge 15 commits intoleanprover-community:masterfrom
DavidLedvinka:stieltjes_transform
Open

feat(MeasureTheory): add Resolvent (Stieltjes/Cauchy) Transform #37245
DavidLedvinka wants to merge 15 commits intoleanprover-community:masterfrom
DavidLedvinka:stieltjes_transform

Conversation

@DavidLedvinka
Copy link
Collaborator

This PR adds the definition of the resolventTransform of a measure and some API. This is a non-standard notion that generalizes both the Stieltjes Transform and Cauchy Transform of a (real-valued) measure so that (for example) the proof that these transforms define holomorphic functions off the support of the measure can be given for both at once. Perhaps these important special cases could be made into abbrevs?

@github-actions
Copy link

github-actions bot commented Mar 26, 2026

PR summary 772c92fec9

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.MeasureTheory.Measure.ResolventTransform (new file) 2626

Declarations diff

+ analyticOn_resolventTransform
+ hasDerivAt_resolvent'
+ hasDerivAt_resolventTransform
+ hasFDerivAt_resolvent
+ integrable_resolvent
+ measurable_resolvent
+ norm_resolvent_le_inv_infDist_support
+ resolventTransform
+ resolventTransform_apply
+ resolventTransform_def
+ resolventTransform_dirac
+ resolventTransform_zero_measure
+ resolvent_zero_of_mem_spectrum

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.


No changes to technical debt.

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

@mathlib-dependent-issues mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 26, 2026
@mathlib-dependent-issues
Copy link

This PR/issue depends on:

David Ledvinka added 2 commits March 26, 2026 22:07
@DavidLedvinka DavidLedvinka marked this pull request as ready for review March 27, 2026 00:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant