Cutting a reflection-invariant subset of the mixed space at a finset of real places

Let S be a finset of real places and A a subset of the mixed space preserved by the reflection negAt {w} of the real coordinate at each single place w of S. The 2 ^ S.card sign patterns along S then cut A into pieces of equal volume, exhausting A up to the null set where some coordinate of S vanishes.

Cutting A down to the points that are positive at every place of S therefore divides its volume by 2 ^ S.card, the real coordinates outside S staying free. A set whose membership depends on the real coordinates only through their absolute values is invariant at every real place, and for S all of the real places the statement is then Mathlib's NumberField.mixedEmbedding.volume_eq_two_pow_mul_volume_plusPart.

Main results

• TauCeti.NumberField.mixedEmbedding.isOpen_setOfPred_forall_mem_pos: the points positive at every place of a finset of real places form an open set.
• TauCeti.NumberField.mixedEmbedding.volume_eq_two_pow_mul_volume_inter_pos: for a set invariant under reflection at each place of S, the volume is 2 ^ S.card times the volume of the part that is positive at every place of S.

theorem TauCeti.NumberField.mixedEmbedding.isOpen_setOfPred_forall_mem_pos {K : Type u_1} [Field K] (S : Finset { w : NumberField.InfinitePlace K // w.IsReal }) : IsOpen {x : NumberField.mixedEmbedding.mixedSpace K | ∀ w ∈ S, 0 < x.1 w}

The points positive at every place of S form an open set: it is a finite intersection of open half spaces.

theorem TauCeti.NumberField.mixedEmbedding.volume_eq_two_pow_mul_volume_inter_pos {K : Type u_1} [Field K] [NumberField K] (S : Finset { w : NumberField.InfinitePlace K // w.IsReal }) {A : Set (NumberField.mixedEmbedding.mixedSpace K)} (hA : ∀ w ∈ S, ∀ (x : NumberField.mixedEmbedding.mixedSpace K), (NumberField.mixedEmbedding.negAt {w}) x ∈ A ↔ x ∈ A) (hm : MeasurableSet A) : MeasureTheory.volume A = 2 ^ S.card * MeasureTheory.volume (A ∩ {x : NumberField.mixedEmbedding.mixedSpace K | ∀ w ∈ S, 0 < x.1 w})

The volume of a sign cut at a finset of real places. If reflecting the real coordinate at any one place of S preserves A, then prescribing a positive sign at each place of S divides the volume of A by 2 ^ S.card.