import Omega.Constants
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Algebra.Order.Floor.Ring

namespace Omega
noncomputable section

def T (x : ℝ) : ℝ := 1 + lam * (x - 1)
def Tk (k x : ℝ) : ℝ := 1 + k * (x - 1)

theorem weighted_mean (a x : ℝ) (ha : 0 < a) :
    (a * phi * x + a * Real.pi) / (a * phi + a * Real.pi) = T x := by
  have hd : a * phi + a * Real.pi ≠ 0 := by
    have := mul_pos ha denominator_pos
    nlinarith
  unfold T lam
  field_simp [hd, ne_of_gt denominator_pos]
  <;> ring

theorem displacement_conjugacy (x : ℝ) : T x - 1 = lam * (x - 1) := by
  unfold T
  ring

theorem affine_iterate (n : ℕ) (x : ℝ) :
    T^[n] x = 1 + lam^n * (x - 1) := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [Function.iterate_succ_apply', ih]
    unfold T
    rw [pow_succ]
    ring

variable {V : Type*} [AddCommGroup V] [Module ℝ V]

def homothety (k : ℝ) (α z : V) : V := α + k • (z - α)
def observation (L : V →ₗ[ℝ] ℝ) (α z : V) : ℝ := 1 + L (z - α)

theorem homothety_comp (k l : ℝ) (α z : V) :
    homothety k α (homothety l α z) = homothety (k*l) α z := by
  simp [homothety, smul_smul]

theorem homothety_one (α z : V) : homothety 1 α z = z := by
  simp [homothety]

theorem observation_commutes (L : V →ₗ[ℝ] ℝ) (k : ℝ) (α z : V) :
    observation L α (homothety k α z) = Tk k (observation L α z) := by
  simp [observation, homothety, Tk]

theorem observation_iterate (L : V →ₗ[ℝ] ℝ) (n : ℕ) (α z : V) :
    observation L α (homothety (lam^n) α z) = T^[n] (observation L α z) := by
  rw [observation_commutes, affine_iterate]
  rfl

theorem real_time_semigroup (t u : ℝ) (α z : V) :
    homothety (lam^t) α (homothety (lam^u) α z) = homothety (lam^(t+u)) α z := by
  rw [homothety_comp, Real.rpow_add lam_pos]

theorem arbitrary_intercept_defect (L : V →ₗ[ℝ] ℝ) (k b : ℝ) (α z : V) :
    (b + L (homothety k α z - α)) - Tk k (b + L (z - α)) =
      (1-k)*(b-1) := by
  simp only [homothety, Tk, add_sub_cancel_left, map_smul,smul_eq_mul]
  ring

def quantize (h y : ℝ) : ℝ := h * (Int.floor (y/h) : ℝ)
def quantizedStep (h y : ℝ) : ℝ := quantize h (lam*y)

theorem grid_interface (h : ℝ) (hh : 0 < h) (d : ℤ) :
    quantizedStep h (h*d) = h * (Int.floor (lam*d) : ℝ) := by
  unfold quantizedStep quantize
  have he : lam*(h*(d:ℝ))/h=lam*d := by
    field_simp
    <;> ring
  rw [he]

end
end Omega