English
The set normLeOne is the preimage under normAtAllPlaces of the image under expMapBasis of paramSet.
Русский
Множество normLeOne есть предобразие normAtAllPlaces под образ expMapBasis paramSet.
LaTeX
$$normLeOne K = normAtAllPlaces^{-1}(expMapBasis''(paramSet K))$$
Lean4
theorem normAtAllPlaces_normLeOne_eq_image : normAtAllPlaces '' (normLeOne K) = expMapBasis '' (paramSet K) :=
by
ext x
by_cases hx : ∀ w, 0 < x w
· rw [← expMapBasis.right_inv (Set.mem_univ_pi.mpr hx), (injective_expMapBasis K).mem_set_image]
simp only [normAtAllPlaces_normLeOne, Set.mem_inter_iff, Set.mem_setOf_eq, expMapBasis_nonneg, Set.mem_preimage,
logMap_expMapBasis, implies_true, and_true, norm_expMapBasis,
pow_le_one_iff_of_nonneg (Real.exp_nonneg _) Module.finrank_pos.ne', Real.exp_le_one_iff, ne_eq, pow_eq_zero_iff',
Real.exp_ne_zero, false_and, not_false_eq_true, Set.mem_univ_pi]
refine ⟨fun ⟨h₁, h₂⟩ w ↦ ?_, fun h ↦ ⟨fun w hw ↦ by simpa [hw] using h w, by simpa using h w₀⟩⟩
· split_ifs with hw
· exact hw ▸ h₂
· exact h₁ w hw
· refine ⟨?_, ?_⟩
· rintro ⟨a, ⟨ha, _⟩, rfl⟩
exact (hx fun w ↦ fundamentalCone.normAtPlace_pos_of_mem ha w).elim
· rintro ⟨a, _, rfl⟩
exact (hx fun w ↦ expMapBasis_pos a w).elim
