English
The image of normLeOne under normAtAllPlaces equals the intersection described by the log map preimage and the positivity/norm constraints.
Русский
Образ normLeOne под normAtAllPlaces совпадает с описанием, задаваемым через предобраз logMap и ограничения нормы.
LaTeX
$$$\\operatorname{normAtAllPlaces}''(\\operatorname{normLeOne} K) = \\cdots$$$
Lean4
theorem normAtAllPlaces_normLeOne :
normAtAllPlaces '' (normLeOne K) =
mixedSpaceOfRealSpace ⁻¹'
(logMap ⁻¹' ZSpan.fundamentalDomain ((basisUnitLattice K).ofZLatticeBasis ℝ (unitLattice K))) ∩
{x | (∀ w, 0 ≤ x w)} ∩
{x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≠ 0} ∩
{x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≤ 1} :=
by
ext x
refine ⟨?_, fun ⟨⟨⟨h₁, h₂⟩, h₃⟩, h₄⟩ ↦ ?_⟩
· rintro ⟨y, ⟨⟨h₁, h₂⟩, h₃⟩, rfl⟩
refine ⟨⟨⟨?_, ?_⟩, ?_⟩, ?_⟩
· rwa [Set.mem_preimage, ← logMap_normAtAllPlaces] at h₁
· exact fun w ↦ normAtPlace_nonneg w y
· rwa [Set.mem_setOf_eq, ← norm_normAtAllPlaces] at h₂
· rwa [Set.mem_setOf_eq, ← norm_normAtAllPlaces] at h₃
· exact ⟨mixedSpaceOfRealSpace x, ⟨⟨h₁, h₃⟩, h₄⟩, normAtAllPlaces_mixedSpaceOfRealSpace h₂⟩
