feat(NumberField/CanonicalEmbedding): define the plusPart of a set

[xroblot]

Let A be a subset of the mixedSpace K of a number field K. We say that A is symmetric at real places if it satisfies:

∀ x, x ∈ A ↔ (fun w ↦ |x.1 w|, x.2) ∈ A

If A is measurable and symmetric at real places, we prove that

volume A = 2 ^ nrRealPlaces K * volume (plusPart A)

where plusPart is the subset of elements of A that are positive at all real places.

This PR is part of the proof of the Analytic Class Number Formula.

---

• depends on: [Merged by Bors] - feat(NumberField/CanonicalEmbedding): define the negAt map #18234

[github-actions]

PR summary 69aabc2248

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ iUnion_negAt_plusPart_ae
+ iUnion_negAt_plusPart_union
+ instance : IsAddHaarMeasure (volume : Measure (mixedSpace K))
+ instance : NoAtoms (volume : Measure (mixedSpace K)) := by
+ measurableSet_negAt_plusPart
+ measurableSet_plusPart
+ mem_negAt_plusPart_of_mem
+ neg_of_mem_negA_plusPart
+ plusPart
+ volume_eq_two_pow_mul_volume_plusPart
+ volume_eq_zero
+ volume_negAt_plusPart

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.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(NumberField/CanonicalEmbedding): define the negAt map #18234
  By Dependent Issues (🤖). Happy coding!