feat: integral presentation of the proximity function of value distribution theory by kebekus · Pull Request #38500 · leanprover-community/mathlib4

kebekus · 2026-04-25T06:39:07Z

If f : ℂ → ℂ is meromorphic, establish a presentation of the proximity function proximity f ⊤ as iterated circle averages. This statement can be used to compare the proximity- and logarithmic counting functions, and is one of the key ingredients in the proof of Cartan's classic formula for the characteristic function.

This is the first section of a multi-part PR, establishing Cartan's formula.

github-actions · 2026-04-25T06:40:05Z

PR summary 7f007d8a78

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation` (new file)	2607

Declarations diff

+ cartanKernel
+ circleIntegrable_circleAverage_log_norm_sub
+ integrable_cartanKernel
+ integrable_cartanKernel_left
+ integrable_integral_norm_cartanKernel
+ integral_norm_cartanKernel_eq
+ integral_norm_eq_two_mul_integral_max_sub
+ measurable_cartanKernel
+ proximity_top_eq_circleAverage_circleAverage

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 7f007d8a78
Reference commit 6933418b3e

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

Co-authored-by: Weiyi Wang <wwylele@gmail.com>

…ebekus/cartan.1

kebekus · 2026-04-26T05:51:14Z

@wwylele Thank you for your helpful comments. I implemented all of them.

j-loreaux

looks pretty good!

The main thing I would have looked for here is where the automation could have been better. fun_prop was able to do some things, as was positivity, but it's important to try and make them work for you by tagging the correct lemmas, for example.

j-loreaux · 2026-06-02T22:50:20Z

+
+private lemma integral_norm_eq_two_mul_integral_max_sub
+    {α : Type*} [MeasurableSpace α] {μ : Measure α} {g : α → ℝ}
+    (hg : Integrable g μ) (hmax : Integrable (fun x ↦ max (g x) 0) μ) :


The hmax condition is redundant (see MeasureTheory.Integrable.sup). Note also that max (g x) 0 is the same thing as (g x)⁺. In fact, I just realized we have MeasureTheory.Integrable.pos_part.

It might be reasonable to write this as a lemma about |g x| and (g x)⁺, and not mark it private. In that case, it would belong in a different file. We could also have the corresponding lemma about |g x| and (g x)⁻.

j-loreaux · 2026-06-02T22:52:31Z

+    ((continuous_circleMap 0 1).measurable.comp measurable_fst)
+
+/- Formula for the `L¹` norm of an angular slice of the Cartan kernel. -/
+private lemma integral_norm_cartanKernel_eq (f : ℂ → ℂ) (R β : ℝ) :


Again, I don't think this needs to be private

j-loreaux · 2026-06-02T23:03:16Z

+theorem measurable_cartanKernel (hf : Measurable f) :
+    Measurable (fun p : ℝ × ℝ ↦ cartanKernel f R p.1 p.2) := by
+  apply measurable_log.comp (continuous_norm.measurable.comp _)
+  exact (hf.comp ((continuous_circleMap 0 R).measurable.comp measurable_snd)).sub
+    ((continuous_circleMap 0 1).measurable.comp measurable_fst)


Suggested change

theorem measurable_cartanKernel (hf : Measurable f) :

Measurable (fun p : ℝ × ℝ ↦ cartanKernel f R p.1 p.2) := by

apply measurable_log.comp (continuous_norm.measurable.comp _)

exact (hf.comp ((continuous_circleMap 0 R).measurable.comp measurable_snd)).sub

((continuous_circleMap 0 1).measurable.comp measurable_fst)

@[fun_prop]

theorem measurable_cartanKernel (hf : Measurable f) :

Measurable (fun p : ℝ × ℝ ↦ cartanKernel f R p.1 p.2) := by

unfold cartanKernel; fun_prop

j-loreaux · 2026-06-03T00:04:48Z

+  have h_meas_K : Measurable (fun p : ℝ × ℝ => cartanKernel f R p.1 p.2) :=
+    measurable_cartanKernel h.measurable


I'm not sure we should have it, but with attribute [fun_prop] Meromorphic.measurable this is provable by fun_prop. I think maybe we shouldn't have it because it is creating a transition theorem "between many layers". While investigating this and other measurability proofs here, I realized we should have the following things:

section PosPart open MeasureTheory variable {α M : Type*} {m : MeasurableSpace α} {μ : Measure α} {f g : α → M} variable [Lattice M] [AddGroup M] section MeasurableSup variable [MeasurableSpace M] [MeasurableSup M] @[fun_prop] theorem Measurable.posPart (hf : Measurable f) : Measurable fun x ↦ (f x)⁺ := hf.sup_const 0 @[fun_prop] theorem Measurable.negPart [MeasurableNeg M] (hf : Measurable f) : Measurable fun x ↦ (f x)⁻ := hf.neg.sup_const 0 @[fun_prop] theorem AEMeasurable.posPart (hf : AEMeasurable f μ) : AEMeasurable (fun x ↦ (f x)⁺) μ := hf.sup_const 0 @[fun_prop] theorem AEMeasurable.negPart [MeasurableNeg M] (hf : AEMeasurable f μ) : AEMeasurable (fun x ↦ (f x)⁻) μ := hf.neg.sup_const 0 end MeasurableSup section ContinuousSup variable [TopologicalSpace M] [ContinuousSup M] namespace MeasureTheory @[fun_prop] theorem StronglyMeasurable.posPart (hf : StronglyMeasurable f) : StronglyMeasurable fun x ↦ (f x)⁺ := hf.sup stronglyMeasurable_const @[fun_prop] theorem StronglyMeasurable.negPart [ContinuousNeg M] (hf : StronglyMeasurable f) : StronglyMeasurable fun x ↦ (f x)⁻ := hf.neg.sup stronglyMeasurable_const @[fun_prop] theorem AEStronglyMeasurable.posPart (hf : AEStronglyMeasurable f μ) : AEStronglyMeasurable (fun x ↦ (f x)⁺) μ := hf.sup aestronglyMeasurable_const @[fun_prop] theorem AEStronglyMeasurable.negPart [ContinuousNeg M] (hf : AEStronglyMeasurable f μ) : AEStronglyMeasurable (fun x ↦ (f x)⁻) μ := hf.neg.sup aestronglyMeasurable_const end MeasureTheory end ContinuousSup end PosPart

If you would like to open a separate PR with these, that would be great.

@j-loreaux I implemented the theorem you suggested in PR #40209. If you can find the time, I would appreciate it if you could have a look.

j-loreaux · 2026-06-03T00:08:02Z

+  simpa [uIoc_of_le two_pi_pos.le] using (integrable_prod_iff'
+    (measurable_cartanKernel h.measurable).stronglyMeasurable.aestronglyMeasurable).2


Suggested change

simpa [uIoc_of_le two_pi_pos.le] using (integrable_prod_iff'

(measurable_cartanKernel h.measurable).stronglyMeasurable.aestronglyMeasurable).2

have := h.measurable

simpa [uIoc_of_le two_pi_pos.le] using (integrable_prod_iff' (by fun_prop)).2

j-loreaux · 2026-06-03T00:11:00Z

+      simp only [circleAverage, mul_comm, mul_inv_rev, smul_eq_mul, mul_assoc,
+        intervalIntegral.integral_const_mul, mul_left_comm, mul_eq_mul_left_iff, inv_eq_zero,
+        OfNat.ofNat_ne_zero, or_false, pi_ne_zero, F]
+      aesop


Suggested change

simp only [circleAverage, mul_comm, mul_inv_rev, smul_eq_mul, mul_assoc,

intervalIntegral.integral_const_mul, mul_left_comm, mul_eq_mul_left_iff, inv_eq_zero,

OfNat.ofNat_ne_zero, or_false, pi_ne_zero, F]

aesop

simp [circleAverage, F, Cartan.cartanKernel, mul_assoc]

j-loreaux · 2026-06-03T00:17:16Z

+      calc ∫ x in 0..2 * π, ∫ y in 0..2 * π, F x y
+        _ = ∫ x, ∫ y, F x y ∂μ ∂μ := by
+          simp [μ, intervalIntegral.integral_of_le two_pi_pos.le]
+        _ = ∫ y, ∫ x, F x y ∂μ ∂μ := by
+          apply MeasureTheory.integral_integral_swap
+          simp only [← uIoc_of_le two_pi_pos.le, F, μ]
+          exact Cartan.integrable_cartanKernel h
+        _ = ∫ y in 0..2 * π, ∫ x in 0..2 * π, F x y := by
+          simp [μ, intervalIntegral.integral_of_le two_pi_pos.le]


I feel like we should have a version of MeasureTheory.integral_integral_swap for interval integrals (we have a version already for mixed ones), so that we don't need to do this dance back and forth.

j-loreaux · 2026-06-03T00:25:01Z

+  have integrable_intervalIntegral_cartanKernel_left :
+      Integrable (∫ β in 0..2 * π, Cartan.cartanKernel f R · β)
+        (volume.restrict (Ioc 0 (2 * π))) := by
+    have h_int := Cartan.integrable_cartanKernel (R := R) h
+    rw [uIoc_of_le two_pi_pos.le] at h_int
+    simpa [intervalIntegral.integral_of_le two_pi_pos.le, Cartan.cartanKernel]
+      using h_int.integral_prod_left


Should this be a convenience lemma?

add file

1e1bd99

github-actions Bot added the t-analysis Analysis (normed *, calculus) label Apr 25, 2026

kebekus marked this pull request as ready for review April 25, 2026 07:02

wwylele reviewed Apr 25, 2026

View reviewed changes

kebekus and others added 4 commits April 26, 2026 07:33

Apply suggestions from code review

8fdaabb

Co-authored-by: Weiyi Wang <wwylele@gmail.com>

[pre-commit.ci lite] apply automatic fixes

395a10f

Update IntegralPresentation.lean

4daba7f

Merge branch 'kebekus/cartan.1' of github.com:kebekus/mathlib4 into k…

378eb2c

…ebekus/cartan.1

mathlib-triage Bot assigned sgouezel Apr 28, 2026

Merge branch 'master' into kebekus/cartan.1

58d134e

mathlib-triage Bot assigned j-loreaux and unassigned sgouezel May 20, 2026

kebekus added 2 commits June 2, 2026 11:19

Merge branch 'master' into kebekus/cartan.1

a1e1b21

Update IntegralPresentation.lean

d9d9d25

j-loreaux reviewed Jun 3, 2026

View reviewed changes

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 3, 2026

kebekus added 2 commits June 3, 2026 06:24

Update IntegralPresentation.lean

feabb2f

Update IntegralPresentation.lean

7f007d8

		have h_meas_K : Measurable (fun p : ℝ × ℝ => cartanKernel f R p.1 p.2) :=
		measurable_cartanKernel h.measurable

		simpa [uIoc_of_le two_pi_pos.le] using (integrable_prod_iff'
		(measurable_cartanKernel h.measurable).stronglyMeasurable.aestronglyMeasurable).2

Conversation

kebekus commented Apr 25, 2026

Uh oh!

github-actions Bot commented Apr 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 7f007d8a78

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

kebekus commented Apr 26, 2026

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

github-actions Bot commented Apr 25, 2026 •

edited

Loading