Polar coordinate change of variables for the mixed space of a number field

We define two polar coordinate changes of variables for the mixed space ℝ^r₁ × ℂ^r₂ associated to a number field K of signature (r₁, r₂). The first one is mixedEmbedding.polarCoord and has value in realMixedSpace K defined as ℝ^r₁ × (ℝ ⨯ ℝ)^r₂, the second is mixedEmbedding.polarSpaceCoord and has value in polarSpace K defined as ℝ^(r₁+r₂) × ℝ^r₂.

The change of variables with the polarSpace is useful to compute the volume of subsets of the mixed space with enough symmetries, see volume_eq_two_pi_pow_mul_integral and volume_eq_two_pow_mul_two_pi_pow_mul_integral

Main definitions and results

• mixedEmbedding.polarCoord: the polar coordinate change of variables between the mixed space ℝ^r₁ × ℂ^r₂ and ℝ^r₁ × (ℝ × ℝ)^r₂ defined as the identity on the first component and mapping (zᵢ)ᵢ to (‖zᵢ‖, Arg zᵢ)ᵢ on the second component.

• mixedEmbedding.integral_comp_polarCoord_symm: the change of variables formula for mixedEmbedding.polarCoord

• mixedEmbedding.polarSpaceCoord: the polar coordinate change of variables between the mixed space ℝ^r₁ × ℂ^r₂ and the polar space ℝ^(r₁ + r₂) × ℝ^r₂ defined by sending x to x w or ‖x w‖ depending on whether w is real or complex for the first component, and to Arg (x w), w complex, for the second component.

• mixedEmbedding.integral_comp_polarSpaceCoord_symm: the change of variables formula for mixedEmbedding.polarSpaceCoord

• mixedEmbedding.volume_eq_two_pi_pow_mul_integral: if the measurable set A of the mixed space is norm-stable at complex places in the sense that normAtComplexPlaces⁻¹ (normAtComplexPlaces '' A) = A, then its volume can be computed via an integral over normAtComplexPlaces '' A.

• mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral: if the measurable set A of the mixed space is norm-stable in the sense that normAtAllPlaces⁻¹ (normAtAllPlaces '' A) = A, then its volume can be computed via an integral over normAtAllPlaces '' A.

@[reducible, inline]

abbrev NumberField.mixedEmbedding.realMixedSpace (K : Type u_1) [Field K] : Type u_1

The real mixed space ℝ^r₁ × (ℝ × ℝ)^r₂ with (r₁, r₂) the signature of K.

noncomputable def NumberField.mixedEmbedding.mixedSpaceToRealMixedSpace (K : Type u_1) [Field K] : mixedSpace K ≃ₜ realMixedSpace K

The natural homeomorphism between the mixed space ℝ^r₁ × ℂ^r₂ and the real mixed space ℝ^r₁ × (ℝ × ℝ)^r₂.

@[simp]

theorem NumberField.mixedEmbedding.mixedSpaceToRealMixedSpace_apply (K : Type u_1) [Field K] (x : mixedSpace K) : (mixedSpaceToRealMixedSpace K) x = (x.1, fun (w : { w : InfinitePlace K // w.IsComplex }) => Complex.equivRealProd (x.2 w))

theorem NumberField.mixedEmbedding.volume_preserving_mixedSpaceToRealMixedSpace_symm (K : Type u_1) [Field K] [NumberField K] : MeasureTheory.MeasurePreserving (⇑(mixedSpaceToRealMixedSpace K).symm) MeasureTheory.volume MeasureTheory.volume

instance NumberField.mixedEmbedding.instIsAddHaarMeasureRealMixedSpaceVolume (K : Type u_1) [Field K] [NumberField K] : MeasureTheory.volume.IsAddHaarMeasure

def NumberField.mixedEmbedding.polarCoordReal (K : Type u_1) [Field K] [NumberField K] : PartialHomeomorph (realMixedSpace K) (realMixedSpace K)

The polar coordinate partial homeomorphism of ℝ^r₁ × (ℝ × ℝ)^r₂ defined as the identity on the first component and mapping (rᵢ cos θᵢ, rᵢ sin θᵢ)ᵢ to (rᵢ, θᵢ)ᵢ on the second component.

@[simp]

theorem NumberField.mixedEmbedding.polarCoordReal_target (K : Type u_1) [Field K] [NumberField K] : (polarCoordReal K).target = Set.univ ×ˢ Set.univ.pi fun (i : { w : InfinitePlace K // w.IsComplex }) => Set.Ioi 0 ×ˢ Set.Ioo (-Real.pi) Real.pi

@[simp]

theorem NumberField.mixedEmbedding.polarCoordReal_apply (K : Type u_1) [Field K] [NumberField K] (p : ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)) : ↑(polarCoordReal K) p = (p.1, Pi.map (fun (i : { w : InfinitePlace K // w.IsComplex }) => ↑polarCoord) p.2)

theorem NumberField.mixedEmbedding.measurable_polarCoordReal_symm (K : Type u_1) [Field K] [NumberField K] : Measurable ↑(polarCoordReal K).symm

theorem NumberField.mixedEmbedding.polarCoordReal_source (K : Type u_1) [Field K] [NumberField K] : (polarCoordReal K).source = Set.univ ×ˢ Set.univ.pi fun (x : { w : InfinitePlace K // w.IsComplex }) => polarCoord.source

def NumberField.mixedEmbedding.FDerivPolarCoordRealSymm (K : Type u_1) [Field K] : realMixedSpace K → realMixedSpace K →L[ℝ] realMixedSpace K

The derivative of polarCoordReal.symm, see hasFDerivAt_polarCoordReal_symm.

theorem NumberField.mixedEmbedding.hasFDerivAt_polarCoordReal_symm (K : Type u_1) [Field K] [NumberField K] (x : realMixedSpace K) : HasFDerivAt (↑(polarCoordReal K).symm) (FDerivPolarCoordRealSymm K x) x

theorem NumberField.mixedEmbedding.det_fderivPolarCoordRealSymm (K : Type u_1) [Field K] [NumberField K] (x : realMixedSpace K) : (FDerivPolarCoordRealSymm K x).det = ∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1

theorem NumberField.mixedEmbedding.polarCoordReal_symm_target_ae_eq_univ (K : Type u_1) [Field K] [NumberField K] : ↑(polarCoordReal K).symm '' (polarCoordReal K).target =ᵐ[MeasureTheory.volume] Set.univ

theorem NumberField.mixedEmbedding.integral_comp_polarCoordReal_symm (K : Type u_1) [Field K] [NumberField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : realMixedSpace K → E) : ∫ (x : realMixedSpace K) in (polarCoordReal K).target, (∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1) • f (↑(polarCoordReal K).symm x) = ∫ (x : realMixedSpace K), f x

theorem NumberField.mixedEmbedding.lintegral_comp_polarCoordReal_symm (K : Type u_1) [Field K] [NumberField K] (f : realMixedSpace K → ENNReal) : ∫⁻ (x : realMixedSpace K) in (polarCoordReal K).target, (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) * f (↑(polarCoordReal K).symm x) = ∫⁻ (x : realMixedSpace K), f x

noncomputable def NumberField.mixedEmbedding.polarCoord (K : Type u_1) [Field K] [NumberField K] : PartialHomeomorph (mixedSpace K) (realMixedSpace K)

The polar coordinate partial homeomorphism between the mixed space ℝ^r₁ × ℂ^r₂ and ℝ^r₁ × (ℝ × ℝ)^r₂ defined as the identity on the first component and mapping (zᵢ)ᵢ to (‖zᵢ‖, Arg zᵢ)ᵢ on the second component.

@[simp]

theorem NumberField.mixedEmbedding.polarCoord_apply (K : Type u_1) [Field K] [NumberField K] (p : ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)) : ↑(mixedEmbedding.polarCoord K) p = (p.1, Pi.map (fun (i : { w : InfinitePlace K // w.IsComplex }) => ↑Complex.polarCoord) p.2)

@[simp]

theorem NumberField.mixedEmbedding.polarCoord_target (K : Type u_1) [Field K] [NumberField K] : (mixedEmbedding.polarCoord K).target = Set.univ ×ˢ Set.univ.pi fun (i : { w : InfinitePlace K // w.IsComplex }) => Complex.polarCoord.target

@[simp]

theorem NumberField.mixedEmbedding.polarCoord_symm_apply (K : Type u_1) [Field K] [NumberField K] (p : ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)) : ↑(mixedEmbedding.polarCoord K).symm p = (p.1, Pi.map (fun (i : { w : InfinitePlace K // w.IsComplex }) => ↑Complex.polarCoord.symm) p.2)

@[simp]

theorem NumberField.mixedEmbedding.polarCoord_source (K : Type u_1) [Field K] [NumberField K] : (mixedEmbedding.polarCoord K).source = Set.univ ×ˢ Set.univ.pi fun (i : { w : InfinitePlace K // w.IsComplex }) => Complex.polarCoord.source

theorem NumberField.mixedEmbedding.polarCoord_target_eq_polarCoordReal_target (K : Type u_1) [Field K] [NumberField K] : (mixedEmbedding.polarCoord K).target = (polarCoordReal K).target

theorem NumberField.mixedEmbedding.polarCoord_symm_eq (K : Type u_1) [Field K] [NumberField K] : ↑(mixedEmbedding.polarCoord K).symm = ⇑(mixedSpaceToRealMixedSpace K).symm ∘ ↑(polarCoordReal K).symm

theorem NumberField.mixedEmbedding.measurable_polarCoord_symm (K : Type u_1) [Field K] [NumberField K] : Measurable ↑(mixedEmbedding.polarCoord K).symm

theorem NumberField.mixedEmbedding.normAtPlace_polarCoord_symm_of_isReal (K : Type u_1) [Field K] [NumberField K] (x : realMixedSpace K) {w : InfinitePlace K} (hw : w.IsReal) : (normAtPlace w) (↑(mixedEmbedding.polarCoord K).symm x) = ‖x.1 ⟨w, hw⟩‖

theorem NumberField.mixedEmbedding.normAtPlace_polarCoord_symm_of_isComplex (K : Type u_1) [Field K] [NumberField K] (x : realMixedSpace K) {w : InfinitePlace K} (hw : w.IsComplex) : (normAtPlace w) (↑(mixedEmbedding.polarCoord K).symm x) = ‖(x.2 ⟨w, hw⟩).1‖

theorem NumberField.mixedEmbedding.integral_comp_polarCoord_symm (K : Type u_1) [Field K] [NumberField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : mixedSpace K → E) : ∫ (x : realMixedSpace K) in (mixedEmbedding.polarCoord K).target, (∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1) • f (↑(mixedEmbedding.polarCoord K).symm x) = ∫ (x : mixedSpace K), f x

theorem NumberField.mixedEmbedding.lintegral_comp_polarCoord_symm (K : Type u_1) [Field K] [NumberField K] (f : mixedSpace K → ENNReal) : ∫⁻ (x : realMixedSpace K) in (mixedEmbedding.polarCoord K).target, (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) * f (↑(mixedEmbedding.polarCoord K).symm x) = ∫⁻ (x : mixedSpace K), f x

@[reducible, inline]

abbrev NumberField.mixedEmbedding.polarSpace (K : Type u_1) [Field K] : Type u_1

The space ℝ^(r₁+r₂) × ℝ^r₂, it is homeomorph to the realMixedSpace, see homeoRealMixedSpacePolarSpace.

def NumberField.mixedEmbedding.measurableEquivRealMixedSpacePolarSpace (K : Type u_1) [Field K] : realMixedSpace K ≃ᵐ polarSpace K

The measurable equivalence between the realMixedSpace and the polarSpace. It is actually an homeomorphism, see homeoRealMixedSpacePolarSpace, but defining it in this way makes it easier to prove that it is volume preserving, see volume_preserving_homeoRealMixedSpacePolarSpace.

def NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace (K : Type u_1) [Field K] : realMixedSpace K ≃ₜ polarSpace K

The homeomorphism between the realMixedSpace and the polarSpace.

theorem NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply (K : Type u_1) [Field K] (x : realMixedSpace K) : (homeoRealMixedSpacePolarSpace K) x = (fun (w : InfinitePlace K) => if hw : w.IsReal then x.1 ⟨w, hw⟩ else (x.2 ⟨w, ⋯⟩).1, fun (w : { w : InfinitePlace K // w.IsComplex }) => (x.2 w).2)

theorem NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal (K : Type u_1) [Field K] (x : realMixedSpace K) (w : { w : InfinitePlace K // w.IsReal }) : ((homeoRealMixedSpacePolarSpace K) x).1 ↑w = x.1 w

theorem NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex (K : Type u_1) [Field K] (x : realMixedSpace K) (w : { w : InfinitePlace K // w.IsComplex }) : ((homeoRealMixedSpacePolarSpace K) x).1 ↑w = (x.2 w).1

theorem NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_snd (K : Type u_1) [Field K] (x : realMixedSpace K) (w : { w : InfinitePlace K // w.IsComplex }) : ((homeoRealMixedSpacePolarSpace K) x).2 w = (x.2 w).2

@[simp]

theorem NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_symm_apply (K : Type u_1) [Field K] (x : polarSpace K) : (homeoRealMixedSpacePolarSpace K).symm x = (fun (w : { w : InfinitePlace K // w.IsReal }) => x.1 ↑w, fun (w : { w : InfinitePlace K // w.IsComplex }) => (x.1 ↑w, x.2 w))

theorem NumberField.mixedEmbedding.volume_preserving_homeoRealMixedSpacePolarSpace (K : Type u_1) [Field K] [NumberField K] : MeasureTheory.MeasurePreserving (⇑(homeoRealMixedSpacePolarSpace K)) MeasureTheory.volume MeasureTheory.volume

def NumberField.mixedEmbedding.polarSpaceCoord (K : Type u_1) [Field K] [NumberField K] : PartialHomeomorph (mixedSpace K) (polarSpace K)

The polar coordinate partial homeomorphism between the mixed space ℝ^r₁ × ℂ^r₂ and the polar space ℝ^(r₁ + r₂) × ℝ^r₂ defined by sending x to x w or ‖x w‖ depending on whether w is real or complex for the first component, and to Arg (x w), w complex, for the second component.

@[simp]

theorem NumberField.mixedEmbedding.polarSpaceCoord_apply (K : Type u_1) [Field K] [NumberField K] (a✝ : mixedSpace K) : ↑(polarSpaceCoord K) a✝ = (homeoRealMixedSpacePolarSpace K) (a✝.1, Pi.map (fun (i : { w : InfinitePlace K // w.IsComplex }) => ↑Complex.polarCoord) a✝.2)

@[simp]

theorem NumberField.mixedEmbedding.polarSpaceCoord_symm_apply (K : Type u_1) [Field K] [NumberField K] (a✝ : polarSpace K) : ↑(polarSpaceCoord K).symm a✝ = (fun (w : { w : InfinitePlace K // w.IsReal }) => a✝.1 ↑w, Pi.map (fun (i : { w : InfinitePlace K // w.IsComplex }) => ↑Complex.polarCoord.symm) fun (w : { w : InfinitePlace K // w.IsComplex }) => (a✝.1 ↑w, a✝.2 w))

@[simp]

theorem NumberField.mixedEmbedding.polarSpaceCoord_target (K : Type u_1) [Field K] [NumberField K] : (polarSpaceCoord K).target = ⇑(homeoRealMixedSpacePolarSpace K).symm ⁻¹' Set.univ ×ˢ Set.univ.pi fun (i : { w : InfinitePlace K // w.IsComplex }) => Complex.polarCoord.target

@[simp]

theorem NumberField.mixedEmbedding.polarSpaceCoord_source (K : Type u_1) [Field K] [NumberField K] : (polarSpaceCoord K).source = Set.univ ×ˢ Set.univ.pi fun (i : { w : InfinitePlace K // w.IsComplex }) => Complex.polarCoord.source

theorem NumberField.mixedEmbedding.measurable_polarSpaceCoord_symm (K : Type u_1) [Field K] [NumberField K] : Measurable ↑(polarSpaceCoord K).symm

theorem NumberField.mixedEmbedding.polarSpaceCoord_target' (K : Type u_1) [Field K] [NumberField K] : (polarSpaceCoord K).target = (Set.univ.pi fun (w : InfinitePlace K) => if w.IsReal then Set.univ else Set.Ioi 0) ×ˢ Set.univ.pi fun (x : { w : InfinitePlace K // w.IsComplex }) => Set.Ioo (-Real.pi) Real.pi

theorem NumberField.mixedEmbedding.integral_comp_polarSpaceCoord_symm (K : Type u_1) [Field K] [NumberField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : mixedSpace K → E) : ∫ (x : polarSpace K) in (polarSpaceCoord K).target, (∏ w : { w : InfinitePlace K // w.IsComplex }, x.1 ↑w) • f (↑(polarSpaceCoord K).symm x) = ∫ (x : mixedSpace K), f x

theorem NumberField.mixedEmbedding.lintegral_comp_polarSpaceCoord_symm (K : Type u_1) [Field K] [NumberField K] (f : mixedSpace K → ENNReal) : ∫⁻ (x : polarSpace K) in (polarSpaceCoord K).target, (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.1 ↑w)) * f (↑(polarSpaceCoord K).symm x) = ∫⁻ (x : mixedSpace K), f x

theorem NumberField.mixedEmbedding.normAtComplexPlaces_polarSpaceCoord_symm {K : Type u_1} [Field K] [NumberField K] (x : polarSpace K) : normAtComplexPlaces (↑(polarSpaceCoord K).symm x) = normAtComplexPlaces (mixedSpaceOfRealSpace x.1)

theorem NumberField.mixedEmbedding.volume_eq_two_pi_pow_mul_integral {K : Type u_1} [Field K] {A : Set (mixedSpace K)} [NumberField K] (hA : normAtComplexPlaces ⁻¹' (normAtComplexPlaces '' A) = A) (hm : MeasurableSet A) : MeasureTheory.volume A = ENNReal.ofReal (2 * Real.pi) ^ InfinitePlace.nrComplexPlaces K * ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x ↑w)

If the measurable set A is norm-stable at complex places in the sense that normAtComplexPlaces⁻¹ (normAtComplexPlaces '' A) = A, then its volume can be computed via an integral over normAtComplexPlaces '' A.

theorem NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral {K : Type u_1} [Field K] {A : Set (mixedSpace K)} [NumberField K] (hA : normAtAllPlaces ⁻¹' (normAtAllPlaces '' A) = A) (hm : MeasurableSet A) : MeasureTheory.volume A = 2 ^ InfinitePlace.nrRealPlaces K * ENNReal.ofReal (2 * Real.pi) ^ InfinitePlace.nrComplexPlaces K * ∫⁻ (x : realSpace K) in normAtAllPlaces '' A, ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x ↑w)

If the measurable set A is norm-stable in the sense that normAtAllPlaces⁻¹ (normAtAllPlaces '' A) = A, then its volume can be computed via an integral over normAtAllPlaces '' A.