English
logMap applied to mixedEmbedding.fundamentalCone.expMapBasis lies in the fundamental domain precisely when all coordinates lie in [0,1).
Русский
logMap применённый к expMapBasis лежит в базисной фундаментальной области тогда и только тогда, когда все координаты лежат в промежутке [0,1).
LaTeX
$$$\text{logMap}(\text{mixedSpaceOfRealSpace}(\text{expMapBasis})) \in ZSpan.fundamentalDomain(\cdot) \iff \forall w, w\neq w_0 \rightarrow x_w \in [0,1)$$$
Lean4
theorem logMap_expMapBasis (x : realSpace K) :
logMap (mixedSpaceOfRealSpace (expMapBasis x)) ∈
ZSpan.fundamentalDomain ((basisUnitLattice K).ofZLatticeBasis ℝ (unitLattice K)) ↔
∀ w, w ≠ w₀ → x w ∈ Set.Ico 0 1 :=
by
classical
simp_rw [ZSpan.mem_fundamentalDomain, equivFinRank.forall_congr_left, Subtype.forall]
refine forall₂_congr fun w hw ↦ ?_
rw [expMapBasis_apply'', map_smul, logMap_real_smul (norm_expMapBasis_ne_zero _) (Real.exp_ne_zero _),
expMapBasis_apply,
logMap_expMap (by rw [← expMapBasis_apply, norm_expMapBasis, if_pos rfl, Real.exp_zero, one_pow]),
Basis.equivFun_symm_apply, Fintype.sum_eq_add_sum_subtype_ne _ w₀, if_pos rfl, zero_smul, zero_add]
conv_lhs =>
enter [2, 1, 2, w, 2, i]
rw [if_neg i.prop]
simp_rw [sum_apply, ← sum_fn, map_sum, Pi.smul_apply, ← Pi.smul_def, map_smul, completeBasis_apply_of_ne,
expMap_symm_apply, normAtAllPlaces_mixedEmbedding, ← logEmbedding_component, logEmbedding_fundSystem,
Finsupp.coe_finset_sum, Finsupp.coe_smul, sum_apply, Pi.smul_apply, Basis.ofZLatticeBasis_repr_apply,
Basis.repr_self, Finsupp.single_apply, EmbeddingLike.apply_eq_iff_eq, Int.cast_ite, Int.cast_one, Int.cast_zero,
smul_ite, smul_eq_mul, mul_one, mul_zero, Fintype.sum_ite_eq']
