volume_eq_two_pow_mul_volume_plusPart

English

If A is symmetric at real places, then the volume of A equals 2^{nrRealPlaces(K)} times the volume of plusPart A: vol(A) = 2^{nrRealPlaces(K)} · vol(plusPart(A)).

Русский

Если A симметрично по вещественным местам, то объем A равен 2^{nrRealPlaces(K)} умножить на объем plusPart(A).

LaTeX

$$volume(A) = 2^{nrRealPlaces(K)} \cdot volume(plusPart(A))$$

Lean4

/-- If a subset `A` of the `mixedSpace` is symmetric at real places, then its volume is
`2^ nrRealPlaces K` times the volume of its `plusPart`. -/
theorem volume_eq_two_pow_mul_volume_plusPart (hm : MeasurableSet A) :
    volume A = 2 ^ nrRealPlaces K * volume (plusPart A) := by
  simp only [← measure_congr (iUnion_negAt_plusPart_ae A hA),
    measure_iUnion (disjoint_negAt_plusPart A) (fun _ ↦ measurableSet_negAt_plusPart _ A hm), volume_negAt_plusPart hm,
    tsum_fintype, sum_const, card_univ, Fintype.card_set, nsmul_eq_mul, Nat.cast_pow, Nat.cast_ofNat, nrRealPlaces]

Похожие утверждения