English
The basis completeBasis is equal to the image of completeFamily via the w0 coordinate, i.e., completeBasis K w0 equals the vector (mult w).
Русский
Базис completeBasis равен образу completeFamily через координату w0, то есть completeBasis K w0 = (mult w).
LaTeX
$$$completeBasis(K)\, w_0 = (w \mapsto \operatorname{mult} w)$$$
Lean4
theorem linearIndependent_completeFamily : LinearIndependent ℝ (completeFamily K) := by
classical
have h₁ : LinearIndependent ℝ (fun w : { w // w ≠ w₀ } ↦ completeFamily K w.1) :=
by
refine LinearIndependent.of_comp realSpaceToLogSpace ?_
simp_rw [Function.comp_def, realSpaceToLogSpace_completeFamily_of_ne]
convert (((basisUnitLattice K).ofZLatticeBasis ℝ _).reindex equivFinRank).linearIndependent
simp
have h₂ : completeFamily K w₀ ∉ Submodule.span ℝ (Set.range (fun w : { w // w ≠ w₀ } ↦ completeFamily K w.1)) :=
by
intro h
have := sum_eq_zero_of_mem_span_completeFamily h
rw [completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq, Nat.cast_eq_zero] at this
exact Module.finrank_pos.ne' this
rw [← linearIndependent_equiv (Equiv.optionSubtypeNe w₀), linearIndependent_option]
exact ⟨h₁, h₂⟩
