[Merged by Bors] - feat(MeasureTheory\Group\Action): add μ(c • s ∩ t) = μ(s ∩ c⁻¹ • t) and similar

[ster99]

Adding lemmas (and their symmetric version thereof)
μ(c • s ∩ t) = μ(s ∩ c⁻¹ • t)
μ(c • s ∪ t) = μ(s ∪ c⁻¹ • t)
μ(c • s ∖ t) = μ(s ∖ c⁻¹ • t)
μ(c • s Δ t) = μ(s Δ c⁻¹ • t)
for μ a SMulInvariantMeasure.

---

[github-actions]

PR summary 4e321186bf

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ measure_inter_inv_smul
+ measure_inv_smul_inter
+ measure_inv_smul_sdiff
+ measure_inv_smul_symmDiff
+ measure_inv_smul_union
+ measure_sdiff_inv_smul
+ measure_symmDiff_inv_smul
+ measure_union_inv_smul

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

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

[ocfnash]

I think these would make good simp lemmas if you flipped the LHS and RHS.

[ster99]

I think these would make good simp lemmas if you flipped the LHS and RHS.

Yep you are right, thanks. Do you think the naming measure_smul_inter for μ (s ∩ c⁻¹ • t) = μ (c • s ∩ t) would still be appropriate?

[ocfnash]

I think these would make good simp lemmas if you flipped the LHS and RHS.

Yep you are right, thanks. Do you think the naming measure_smul_inter for μ (s ∩ c⁻¹ • t) = μ (c • s ∩ t) would still be appropriate?

I think I'd try to get an _inv into the name. So for the lemma you mention I suggest measure_inter_inv_smul.

[ocfnash]

Thanks!

bors merge

[mathlib-bors]

Canceled.

[ocfnash]

@ster99 You have taken this out of the bors queue by merging master. Was this intentional?

[ster99]

@ocfnash Yep, but I didn't know that merging master would have put it out of queue. Sorry, my bad. It is indeed ready to be merged and I won't touch anything this time

[ocfnash]

No need to apologise!

Let's try again:

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build
• Post-Build Step