import Omega.Geometry
import Mathlib.Data.Matrix.Rank

namespace Omega
noncomputable section
open Complex

theorem seeds_distinct (a : ℝ) (ha : 0 < a) : mark a s ≠ mark a (-s) := by
  intro h
  have hi := congrArg Complex.im h
  simp only [mark_im,mul_neg] at hi
  nlinarith [mul_pos ha s_pos]

theorem marks_collinear (a : ℝ) : Collinear ℝ (Set.range (marks a)) := by
  rw [collinear_iff_exists_forall_eq_smul_vadd]
  refine ⟨(a*c:ℝ),I,?_⟩
  rintro p ⟨i,rfl⟩
  refine ⟨a*heights i,?_⟩
  simp [marks,mark,Complex.real_smul,vadd_eq_add,add_comm]

theorem marks_affine_dimension (a : ℝ) (ha : 0 < a) :
    Module.finrank ℝ (affineSpan ℝ (Set.range (marks a))).direction=1 := by
  have h0 : mark a s ∈ Set.range (marks a) := ⟨3,rfl⟩
  have h1 : mark a (-s) ∈ Set.range (marks a) := ⟨2,rfl⟩
  rw [← (marks_collinear a).affineSpan_eq_of_ne h0 h1 (seeds_distinct a ha),
    direction_affineSpan,vectorSpan_pair]
  exact finrank_span_singleton (sub_ne_zero.mpr (seeds_distinct a ha))

theorem seed_linear_combination (a : ℝ) (ha : 0 < a) (z : ℂ) :
    ((z.re/(a*c)+z.im/(a*s))/2) • mark a s+
    ((z.re/(a*c)-z.im/(a*s))/2) • mark a (-s)=z := by
  have hac : a*c≠0 := ne_of_gt (mul_pos ha c_pos)
  have has : a*s≠0 := ne_of_gt (mul_pos ha s_pos)
  apply Complex.ext <;> simp only [Complex.add_re,Complex.add_im,
    Complex.smul_re,Complex.smul_im,mark_re,mark_im,smul_eq_mul]
  · field_simp
    <;> ring
  · field_simp
    <;> ring

theorem centered_span (a : ℝ) (ha : 0 < a) :
    Submodule.span ℝ (Set.range (marks a))=⊤ := by
  apply top_unique
  intro z _
  have h0 : mark a s ∈ Submodule.span ℝ (Set.range (marks a)) :=
    Submodule.subset_span ⟨3,rfl⟩
  have h1 : mark a (-s) ∈ Submodule.span ℝ (Set.range (marks a)) :=
    Submodule.subset_span ⟨2,rfl⟩
  rw [← seed_linear_combination a ha z]
  exact Submodule.add_mem _ (Submodule.smul_mem _ _ h0) (Submodule.smul_mem _ _ h1)

theorem center_relative_rank (a : ℝ) (ha : 0 < a) :
    Module.finrank ℝ (Submodule.span ℝ (Set.range (marks a)))=2 := by
  rw [centered_span a ha,finrank_top,Complex.finrank_real_complex]

theorem center_adjoined_affine_dimension (a : ℝ) (ha : 0 < a) :
    Module.finrank ℝ (affineSpan ℝ (insert 0 (Set.range (marks a)))).direction=2 := by
  rw [direction_affineSpan,vectorSpan_eq_span_vsub_set_right ℝ (Set.mem_insert 0 _)]
  change Module.finrank ℝ (Submodule.span ℝ ((fun x : ℂ => x-0) ''
    insert 0 (Set.range (marks a))))=2
  have hf : (fun x : ℂ => x-0)=id := by funext x; exact sub_zero x
  rw [hf,Set.image_id,Submodule.span_insert_zero]
  exact center_relative_rank a ha

/-- Rows are the two real coordinates, columns are the six marks. -/
def coordinates (a : ℝ) : Matrix (Fin 2) (Fin 6) ℝ :=
  ![(fun _ => a*c),(fun i => a*heights i)]
def gram (a : ℝ) : Matrix (Fin 6) (Fin 6) ℝ :=
  (coordinates a).transpose * coordinates a
def moment (a : ℝ) : Matrix (Fin 2) (Fin 2) ℝ :=
  coordinates a * (coordinates a).transpose

theorem moment_matrix (a : ℝ) :
    moment a=!![6*(a*c)^2,0;0,2*a^2*(s^2+(1+s)^2+(phi^2+s)^2)] := by
  ext i j
  fin_cases i <;> fin_cases j <;>
    simp [moment,coordinates,Matrix.mul_apply,Fin.sum_univ_six,heights] <;> ring

theorem coordinates_rank (a : ℝ) (ha : 0 < a) : (coordinates a).rank=2 := by
  have hc := c_pos
  have hs := s_pos
  have hx : 6*(a*c)^2≠0 := by positivity
  have hy : 2*a^2*(s^2+(1+s)^2+(phi^2+s)^2)≠0 := by positivity
  have hm : moment a=Matrix.diagonal ![6*(a*c)^2,
      2*a^2*(s^2+(1+s)^2+(phi^2+s)^2)] := by
    rw [moment_matrix]
    ext i j
    fin_cases i <;> fin_cases j <;> simp [Matrix.diagonal]
  rw [← Matrix.rank_self_mul_transpose (coordinates a)]
  change (moment a).rank=2
  rw [hm,Matrix.rank_diagonal]
  have hn : ∀ i : Fin 2, ![6*(a*c)^2,
      2*a^2*(s^2+(1+s)^2+(phi^2+s)^2)] i ≠ 0 := by
    intro i
    fin_cases i <;> simp [hx,hy]
  have hz : Fintype.card {i : Fin 2 // ![6*(a*c)^2,
      2*a^2*(s^2+(1+s)^2+(phi^2+s)^2)] i=0}=0 := by
    apply Fintype.card_eq_zero_iff.mpr
    exact ⟨fun x => hn x.1 x.2⟩
  simp [hz]

theorem gram_rank (a : ℝ) (ha : 0 < a) : (gram a).rank=2 := by
  rw [gram,Matrix.rank_transpose_mul_self,coordinates_rank a ha]

theorem gram_entries (a : ℝ) (i j : Fin 6) :
    gram a i j=a^2*(c^2+heights i*heights j) := by
  simp [gram,coordinates,Matrix.mul_apply,Fin.sum_univ_two]
  ring

/-- Injectively embedding into any real vector space preserves the dimension
of the spanned geometric plane; its ambient dimension is a separate quantity. -/
theorem embedded_center_relative_rank {V : Type*} [AddCommGroup V] [Module ℝ V]
    (E : ℂ →ₗ[ℝ] V) (hE : Function.Injective E) (a : ℝ) (ha : 0 < a) :
    Module.finrank ℝ (Submodule.span ℝ (E '' Set.range (marks a)))=2 := by
  rw [Submodule.span_image,centered_span a ha,Submodule.map_top,
    LinearMap.finrank_range_of_inj hE,Complex.finrank_real_complex]

end
end Omega