Skip to content

feat(Dynamics/BirkhoffSum): add the maximal ergodic theorem#34031

Open
lua-vr wants to merge 2 commits intoleanprover-community:masterfrom
lua-vr:maximal-ergodic-theorem
Open

feat(Dynamics/BirkhoffSum): add the maximal ergodic theorem#34031
lua-vr wants to merge 2 commits intoleanprover-community:masterfrom
lua-vr:maximal-ergodic-theorem

Conversation

@lua-vr
Copy link
Copy Markdown
Contributor

@lua-vr lua-vr commented Jan 16, 2026 •
edited
Loading

This file exports three constants:

public def birkhoffAverageSupSet (f : α → α) (g : α → ℝ) (a : ℝ) : Set α :=
  {x | ∃ n : ℕ, a < birkhoffAverage ℝ f g n x}

public theorem meas_birkhoffAverageSupSet_smul_const_le_integral (a : ℝ) (ha : 0 < a) :
    μ.real (birkhoffAverageSupSet f g a) • a ≤ ∫ x in birkhoffAverageSupSet f g a, g x ∂μ

public theorem meas_birkhoffAverageSupSet_smul_const_le_norm (a : ℝ) (ha : 0 < a) :
    μ.real (birkhoffAverageSupSet f (fun x ↦ ‖g x‖) a) • a ≤ ∫ x, ‖g x‖ ∂μ

In my interpretation, the other constants are auxiliary, so I did not make them public. If it's of independent interest, birkhoffMax could be exported or moved to a dedicated file, but I'm not sure of that at the moment.

Open in Gitpod

@github-actions
Copy link
Copy Markdown

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

PR summary 592989bdba

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Dynamics.BirkhoffSum.Maximal (new file) 2353

Declarations diff

+ birkhoffAverageSupSet_eq_birkhoffSupSet
+ birkhoffAverage_iff_birkhoffSum
+ birkhoffMax
+ birkhoffMax_aestronglyMeasurable
+ birkhoffMax_comp_le_succ
+ birkhoffMax_integrable
+ birkhoffMax_integral_le
+ birkhoffMax_le_birkhoffMax
+ birkhoffMax_measurable
+ birkhoffMax_nonneg
+ birkhoffMax_pos_of_mem_support
+ birkhoffMax_succ
+ birkhoffMax_succ'
+ birkhoffSum_aestronglyMeasurable
+ birkhoffSum_integrable
+ birkhoffSum_measurable
+ birkhoffSupSet
+ birkhoffSupSet_eq_iSup_birkhoffMax_support
+ setIntegral_nonneg_on_birkhoffMax_support
+ setIntegral_nonneg_on_birkhoffSupSet
+ tendsto_setIntegral_on_birkhoffMax_support_birkhoffSupSet

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
632 3 erw

Current commit 0075a18aa8
Reference commit 592989bdba

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-dynamics Dynamical Systems label Jan 16, 2026
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 16, 2026
lua-vr
lua-vr commented Jan 16, 2026
View reviewed changes
Mathlib/Dynamics/BirkhoffSum/Maximal.lean
Comment on lines +89 to +94
-- TODO: move elsewhere
@[measurability]
lemma birkhoffSum_measurable [MeasurableSpace α] {f : α → α} (hf : Measurable f) {g : α → ℝ}
(hg : Measurable g) {n} : Measurable (birkhoffSum f g n) := by
apply Finset.measurable_sum
measurability
Copy link
Copy Markdown
Contributor Author

@lua-vr lua-vr Jan 16, 2026

Choose a reason for hiding this comment

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

Where do these lemmas belong? I don't want to add MeasureTheory and Integrable to the imports of BirkhoffSum.Basic...

@lua-vr lua-vr force-pushed the maximal-ergodic-theorem branch 2 times, most recently from 0845c36 to d5addf3 Compare January 17, 2026 01:55
@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 3, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Mar 3, 2026

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

@lua-vr lua-vr force-pushed the maximal-ergodic-theorem branch from d5addf3 to 0215e41 Compare March 5, 2026 01:09
@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 5, 2026
@lua-vr lua-vr force-pushed the maximal-ergodic-theorem branch from 0215e41 to 2bb1464 Compare March 5, 2026 01:26
@mathlib-dependent-issues mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 5, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Mar 5, 2026

This PR/issue depends on:

@lua-vr lua-vr force-pushed the maximal-ergodic-theorem branch from 2bb1464 to cc1da7f Compare March 5, 2026 12:22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

t-dynamics Dynamical Systems

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@lua-vr @urkud @mathlib4-dependent-issues-bot