chore(Dynamics/BirkhofSum): improve naming of birkhoffSum and birkhoffAverage lemmas

[lua-vr]

Previously, those two files used apostrophes ' for discerning the point-free or applied lemmas, in a non-consistent way. I changed the naming to use _apply to name the applied versions.

For birkhoffSum, the birkhoffSum_add and birkhoffSum_add' lemma names were inconsistent with birkhoffSum_sub. _add is now function addition g + g' (matching _sub and birkhoffAverage_add), and _add' is now index addition m + n.

Another cases of inconsistency was that the n was sometimes present in in the non-applied version, sometimes not. I changed it to generalize the n (not mention it) in the non-applied whenever possible.

I also added some missing point-free versions.

I did not add deprecation aliases as there are currently no other files using those lemmas, and since many names are swapped I'm not sure if adding deprecations is even possible.

Created with the help of Claude, iteratively reviewed by me.

---

[github-actions]

PR summary f86882c9d2

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ birkhoffAverage_apply_add
+ birkhoffAverage_apply_congr_ring
+ birkhoffAverage_apply_neg
+ birkhoffAverage_apply_of_comp_eq
+ birkhoffAverage_apply_one
+ birkhoffAverage_apply_sub
+ birkhoffAverage_apply_zero
+ birkhoffAverage_comp_sub_birkhoffAverage
+ birkhoffSum_apply_add
+ birkhoffSum_apply_add'
+ birkhoffSum_apply_neg
+ birkhoffSum_apply_of_comp_eq
+ birkhoffSum_apply_one
+ birkhoffSum_apply_sub
+ birkhoffSum_apply_succ
+ birkhoffSum_apply_succ'
+ birkhoffSum_apply_zero
+ birkhoffSum_comp_sub_birkhoffSum
+ map_comp_birkhoffAverage
+ map_comp_birkhoffSum
- birkhoffAverage_congr_ring'
- birkhoffAverage_one'
- birkhoffAverage_zero'
- birkhoffSum_one'
- birkhoffSum_zero'

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.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit f86882c).

• +20 new declarations
• −5 removed declarations

+birkhoffAverage_apply_add
+birkhoffAverage_apply_congr_ring
+birkhoffAverage_apply_neg
+birkhoffAverage_apply_of_comp_eq
+birkhoffAverage_apply_one
+birkhoffAverage_apply_sub
+birkhoffAverage_apply_zero
+birkhoffAverage_comp_sub_birkhoffAverage
-birkhoffAverage_congr_ring'
-birkhoffAverage_one'
-birkhoffAverage_zero'
+birkhoffSum_apply_add
+birkhoffSum_apply_add'
+birkhoffSum_apply_neg
+birkhoffSum_apply_of_comp_eq
+birkhoffSum_apply_one
+birkhoffSum_apply_sub
+birkhoffSum_apply_succ
+birkhoffSum_apply_succ'
+birkhoffSum_apply_zero
+birkhoffSum_comp_sub_birkhoffSum
-birkhoffSum_one'
-birkhoffSum_zero'
+map_comp_birkhoffAverage
+map_comp_birkhoffSum

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit f86882c9d2
Reference commit 9fb10993c1

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