import Omega.Geometry
import Omega.Affine
import Omega.Ledger

namespace Omega
noncomputable section
open Complex Set

variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]

def place (α : V) (E : ℂ →ₗᵢ[ℝ] V) (z : ℂ) : V := α+E z
def placedOutline (α : V) (E : ℂ →ₗᵢ[ℝ] V) (a : ℝ) : Set V :=
  place α E '' outline a
def placedArc (α : V) (E : ℂ →ₗᵢ[ℝ] V) (a t : ℝ) : V :=
  place α E (circleMap 0 a t)

theorem placed_distance (α : V) (E : ℂ →ₗᵢ[ℝ] V) (z w : ℂ) :
    dist (place α E z) (place α E w)=dist z w := by
  simp [place,E.dist_map]

theorem placed_arc_derivative (α : V) (E : ℂ →ₗᵢ[ℝ] V) (a t : ℝ) :
    HasDerivAt (placedArc α E a) (E (circleMap 0 a t*I)) t := by
  exact (E.toContinuousLinearMap.hasFDerivAt.comp_hasDerivAt t
    (hasDerivAt_circleMap 0 a t)).const_add α

def placedC (α : V) (E : ℂ →ₗᵢ[ℝ] V) (a : ℝ) : ℝ :=
  ∫ t in (Real.pi/2)..(3*Real.pi/2), ‖deriv (placedArc α E a) t‖
def placedG (α : V) (E : ℂ →ₗᵢ[ℝ] V) (a : ℝ) : ℝ :=
  (dist (place α E (mark a (-(phi^2+s)))) (place α E (mark a (-(1+s))))+
   dist (place α E (mark a (phi^2+s))) (place α E (mark a (1+s))))/2

theorem placed_G (α : V) (E : ℂ →ₗᵢ[ℝ] V) (a : ℝ) : placedG α E a=G a := by
  simp only [placedG,placed_distance,G]

theorem placed_C (α : V) (E : ℂ →ₗᵢ[ℝ] V) (a : ℝ) : placedC α E a=C a := by
  unfold placedC C arcLength
  congr 1
  funext t
  rw [(placed_arc_derivative α E a t).deriv,deriv_circleMap]
  exact E.norm_map _

theorem provenance_all_placements (α : V) (E : ℂ →ₗᵢ[ℝ] V)
    (a : ℝ) (ha : 0 < a) :
    placedG α E a=a*phi ∧ placedC α E a=a*Real.pi ∧
    placedG α E a/(placedG α E a+placedC α E a)=lam := by
  rw [placed_G,placed_C,G_eq a ha,C_eq a ha]
  refine ⟨rfl,rfl,?_⟩
  have h := (geometric_provenance a ha).1
  simpa [W,G_eq a ha,C_eq a ha] using h

theorem mark_scale (k a z : ℝ) : (k:ℝ) • mark a z=mark (k*a) z := by
  simp only [mark,Complex.real_smul,ofReal_mul]
  ring

theorem circle_scale (k a t : ℝ) : (k:ℝ) • circleMap 0 a t=circleMap 0 (k*a) t := by
  simp [circleMap,Complex.real_smul,mul_assoc]

theorem outline_scale (k a : ℝ) : ((k:ℝ) • ·) '' outline a=outline (k*a) := by
  unfold outline majorArc extensionPlus extensionMinus
  simp only [Set.image_union,← Set.image_comp,Function.comp_def,mark_scale,circle_scale]

theorem placed_homothety (α : V) (E : ℂ →ₗᵢ[ℝ] V) (k a : ℝ) :
    homothety k α '' placedOutline α E a=placedOutline α E (k*a) := by
  unfold placedOutline
  rw [← outline_scale k a]
  simp only [← Set.image_comp,Function.comp_def,place,homothety,
    add_sub_cancel_left,map_smul]

theorem readout_scale (k a : ℝ) (hk : 0 < k) (ha : 0 < a) :
    G (k*a)=k*G a ∧ C (k*a)=k*C a := by
  rw [G_eq _ (mul_pos hk ha),G_eq a ha,C_eq _ (mul_pos hk ha),C_eq a ha]
  constructor <;> ring

/-- This explicitly reconstructs the whole radius-requantized marked curve
when center, ordered isometric frame, grid scale and ordered ledger survive. -/
theorem curve_reconstruction (α : V) (E : ℂ →ₗᵢ[ℝ] V)
    (h : ℝ) (n : ℕ) (d : ℤ) :
    placedOutline α E
      (h*Ledger.recover Q S (Ledger.encode Q S n d).1 (Ledger.encode Q S n d).2)=
    placedOutline α E (h*d) := by
  rw [Ledger.roundtrip (Q:ℤ) (S:ℤ) (by norm_num [Q])]

end
end Omega