The Lean 4 theorem `hasDerivAt_apply` in the `?` chapter of the timepiece formalization

import Definitions.Def_ChapterNonnegResolvent
import Definitions.Def_ChapterClosureUniqueness
import Definitions.Def_ChapterNonnegSquareRoot
import Definitions.Def_ChapterPositiveSquareRootUnique
import Mathlib

import Mathlib.Analysis.SpecialFunctions.Exponential
import Mathlib.Analysis.Calculus.MeanValue
import Mathlib.Analysis.Calculus.UniformLimitsDeriv
import Mathlib.Analysis.InnerProductSpace.Calculus

/-!
# The unitary group `e^{-itT}` of a non-negative self-adjoint linear relation

`BookProof.ChapterNonnegResolvent` produced, for a non-negative self-adjoint linear
relation `T` on a complex Hilbert space `F`, the resolvent family
`R a = (T + a)⁻¹` and the **Yosida approximation** `T_a = a (1 − a R a)`: bounded,
self-adjoint, non-negative operators with `T_a h → k` for `(h, k) ∈ T`.  This chapter
turns that approximation into the **one-parameter unitary group** `e^{-itT}` — the
Schrödinger dynamics generated by `T` — which is the object the Hashimoto–SIRK
shift-invert layer of this development consumes (a *unitary group*, not a semigroup:
the generator enters as `-iT`).

## The exponential of a bounded self-adjoint operator

`expU B t = e^{-itB}` for a bounded `B`.  For self-adjoint `B` it is unitary
(`expU_mem_unitary`) and isometric (`norm_expU_apply`); it satisfies `expU B 0 = 1`
(`expU_zero`), the group law `expU B (s + t) = expU B s * expU B t` (`expU_add`) and
the differential equation `d/dt e^{-itB} x = e^{-itB} (-iB) x`
(`hasDerivAt_expU_apply`).  The key quantitative statement is the **Duhamel estimate**
`‖(e^{-itB} − e^{-itC}) x‖ ≤ |t| ‖(B − C) x‖` for *commuting* bounded self-adjoint
`B, C` (`norm_expU_sub_apply_le`), with the special case
`‖e^{-itB} x − x‖ ≤ |t| ‖B x‖` (`norm_expU_sub_self_le`).

## The limit group

The Yosida approximations commute (`commute_yosidaCLM`, `commute_yosidaAt`) and
commute with every resolvent (`commute_yosidaCLM_invCLMAt`), so the approximating
groups `approxU hT n t = e^{-itT_{n+1}}` form a Cauchy sequence at every point of the
domain (`approxU_cauchy_of_mem`) and — the domain being dense for a single-valued `T`
(`BookProof.NonnegResolvent.dense_domain`) — at every vector (`approxU_cauchy`).  Its
limit is

* **`unitaryU hT hsv t = e^{-itT}`**, a bounded operator (`tendsto_unitaryU`) which is
  isometric (`norm_unitaryU_apply`) and unitary (`unitaryU_mem_unitary`,
  `unitaryU_surjective`), with `U 0 = 1` (`unitaryU_zero`) and the **group law**
  `U (s + t) = U s U t` (`unitaryU_add`, `unitaryU_apply_unitaryU`,
  `unitaryU_neg_eq_star`);
* **strongly continuous**: `‖U t h − h‖ ≤ |t| ‖k‖` on the domain
  (`norm_unitaryU_sub_of_mem`), whence `U t x → x` as `t → 0`
  (`tendsto_unitaryU_zero`) and `t ↦ U t x` is continuous
  (`continuous_unitaryU_apply`);
* approximated at the rate `‖U t h − e^{-itT_m} h‖ ≤ |t| ‖k − T_m h‖` on the domain
  (`norm_unitaryU_sub_approxU_le`) and **uniformly on bounded time intervals** at every
  vector (`tendstoUniformlyOn_approxU`).

## The dynamics

`e^{-itT}` commutes with every resolvent (`unitaryU_invCLMAt`), hence **leaves the
relation invariant**: `(h, k) ∈ T` implies `(U t h, U t k) ∈ T` (`mem_unitaryU`), so
the orbit of a point of the domain stays in the domain.  Along such an orbit the
**Schrödinger equation** holds globally in `t`,
`d/dt (e^{-itT} h) = -i e^{-itT} k` (`hasDerivAt_unitaryU`), and the inner products
— in particular the energy `⟪h, k⟫` — are conserved (`inner_unitaryU`,
`inner_unitaryU_of_mem`).  Conversely the orbits are the **only** solutions: a
differentiable curve staying in the relation and satisfying `u' = -i k` equals
`u s = e^{-isT} (u 0)` (`eq_unitaryU_of_hasDerivAt`), because the norm of a solution is
constant — the quadratic form of a symmetric relation being real
(`inner_mem_conj_eq`).

## Honest boundary

This is the abstract operator-theoretic statement for a *non-negative* self-adjoint
linear relation; nothing is claimed here about the project's physical Hamiltonians
beyond what follows once their hypotheses are checked.  The single-valuedness
hypothesis `hsv` is what makes the domain dense, and is the only place where the
relation is required to be an operator.  A functional calculus for unbounded
self-adjoint operators — and the spectral theorem behind it — is still not formalized
here; the group is built from the *bounded* Yosida approximants only.
-/

namespace BookProof.NonnegUnitaryGroup

open BookProof.ClosureUniqueness BookProof.PositiveSquareRoot BookProof.NonnegSquareRoot
open BookProof.NonnegResolvent
open Filter Topology NormedSpace
open scoped InnerProductSpace

variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]

noncomputable local instance ratNormedAlgebra : NormedAlgebra ℚ (F →L[ℂ] F) :=
  NormedAlgebra.restrictScalars ℚ ℂ (F →L[ℂ] F)

omit [CompleteSpace F] in
/-- Evaluating a differentiable curve of bounded operators at a fixed vector. -/
theorem hasDerivAt_apply {f : ℝ → (F →L[ℂ] F)} {f' : F →L[ℂ] F} {t : ℝ} (x : F)
    (h : HasDerivAt f f' t) : HasDerivAt (fun s => f s x) (f' x) t :=
  ((ContinuousLinearMap.apply ℂ F x).restrictScalars ℝ).hasFDerivAt.comp_hasDerivAt t h

/-! ## The exponential of a bounded self-adjoint operator -/

/-- The unitary `e^{-itB}` generated by a bounded self-adjoint operator `B`. -/
noncomputable def expU (B : F →L[ℂ] F) (t : ℝ) : F →L[ℂ] F := exp (t • ((-Complex.I) • B))

variable {B C : F →L[ℂ] F} {s t : ℝ}

theorem smul_neg_I_mem_skewAdjoint (hB : IsSelfAdjoint B) (t : ℝ) :
    t • ((-Complex.I) • B) ∈ skewAdjoint (F →L[ℂ] F) := by
  have hB' : star B = B := hB
  rw [skewAdjoint.mem_iff, star_smul, star_trivial, star_smul, hB']
  simp only [star_neg, Complex.star_def, Complex.conj_I, neg_neg]
  module

theorem expU_mem_unitary (hB : IsSelfAdjoint B) (t : ℝ) : expU B t ∈ unitary (F →L[ℂ] F) :=
  exp_mem_unitary_of_mem_skewAdjoint (smul_neg_I_mem_skewAdjoint hB t)

@[simp] theorem expU_zero (B : F →L[ℂ] F) : expU B 0 = 1 := by simp [expU]

theorem expU_add (B : F →L[ℂ] F) (s t : ℝ) : expU B (s + t) = expU B s * expU B t := by
  rw [expU, expU, expU, add_smul]
  exact exp_add_of_commute (((Commute.refl ((-Complex.I) • B)).smul_left s).smul_right t)

theorem norm_expU_apply (hB : IsSelfAdjoint B) (t : ℝ) (x : F) : ‖expU B t x‖ = ‖x‖ := by
  have hu : (star (expU B t)) * expU B t = 1 :=
    (Unitary.mem_iff.mp (expU_mem_unitary hB t)).1
  have hadj : ContinuousLinearMap.adjoint (expU B t) (expU B t x) = x := by
    have := congrArg (fun (S : F →L[ℂ] F) => S x) hu
    simpa [ContinuousLinearMap.star_eq_adjoint] using this
  have hinner : ⟪expU B t x, expU B t x⟫_ℂ = ⟪x, x⟫_ℂ := by
    rw [← ContinuousLinearMap.adjoint_inner_left, hadj]
  have h3 : (⟪expU B t x, expU B t x⟫_ℂ).re = (⟪x, x⟫_ℂ).re := by rw [hinner]
  simpa [inner_self_eq_norm_sq, ← Complex.ofReal_pow] using h3

theorem expU_zero_op (t : ℝ) : expU (0 : F →L[ℂ] F) t = 1 := by
  simp [expU]

theorem hasDerivAt_expU (B : F →L[ℂ] F) (t : ℝ) :
    HasDerivAt (fun s : ℝ => expU B s) (expU B t * ((-Complex.I) • B)) t :=
  hasDerivAt_exp_smul_const (𝕂 := ℝ) ((-Complex.I) • B) t

theorem hasDerivAt_expU_apply (B : F →L[ℂ] F) (t : ℝ) (x : F) :
    HasDerivAt (fun s : ℝ => expU B s x) ((expU B t) (((-Complex.I) • B) x)) t :=
  hasDerivAt_apply x (hasDerivAt_expU B t)

/-- **The fundamental estimate** `‖(e^{-itB} - e^{-itC}) x‖ ≤ |t| ‖(B - C) x‖` for commuting
bounded self-adjoint operators. -/
theorem norm_expU_sub_apply_le (hB : IsSelfAdjoint B) (hC : IsSelfAdjoint C)
    (hcomm : Commute B C) (t : ℝ) (x : F) :
    ‖expU B t x - expU C t x‖ ≤ |t| * ‖B x - C x‖ := by
  set gB : F →L[ℂ] F := (-Complex.I) • B with hgB
  set gC : F →L[ℂ] F := (-Complex.I) • C with hgC
  have hgcomm : Commute gB gC := (hcomm.smul_left _).smul_right _
  have hcommU : ∀ r : ℝ, gB * expU C r = expU C r * gB :=
    fun r => ((hgcomm.smul_right r).exp_right).eq
  set K : ℝ := ‖B x - C x‖ with hK
  set P : ℝ → (F →L[ℂ] F) := fun r => expU B (t - r) * expU C r with hP
  set D : ℝ → (F →L[ℂ] F) := fun r => (expU B (t - r) * expU C r) * (gC - gB) with hD
  have hderiv : ∀ r : ℝ, HasDerivAt (fun r => P r x) (D r x) r := by
    intro r
    have hc : HasDerivAt (fun r : ℝ => expU B (t - r)) (-(expU B (t - r) * gB)) r := by
      have h1 := hasDerivAt_expU B (t - r)
      have h2 : HasDerivAt (fun r : ℝ => t - r) (-1 : ℝ) r := by
        simpa using (hasDerivAt_id r).const_sub t
      have h3 := h1.scomp r h2
      have he : -(expU B (t - r) * gB) = Complex.I • (expU B (t - r) * B) := by
        rw [hgB, mul_smul_comm, neg_smul, neg_neg]
      rw [he]
      convert h3 using 1 <;>
        (first | rfl | simp only [neg_smul, one_smul, mul_neg, neg_neg, mul_smul_comm])
    have hd : HasDerivAt (fun r : ℝ => expU C r) (expU C r * gC) r := hasDerivAt_expU C r
    have hmul := hc.mul hd
    have hEq : -(expU B (t - r) * gB) * expU C r + expU B (t - r) * (expU C r * gC) = D r := by
      calc -(expU B (t - r) * gB) * expU C r + expU B (t - r) * (expU C r * gC)
          = -(expU B (t - r) * (gB * expU C r)) + expU B (t - r) * (expU C r * gC) := by
            noncomm_ring
        _ = -(expU B (t - r) * (expU C r * gB)) + expU B (t - r) * (expU C r * gC) := by
            rw [hcommU r]
        _ = D r := by rw [hD]; noncomm_ring
    rw [hP]
    exact hasDerivAt_apply x (hEq ▸ hmul)
  have hnorm : ∀ r : ℝ, ‖D r x‖ = K := by
    intro r
    have h1 : D r x = expU B (t - r) (expU C r ((gC - gB) x)) := rfl
    rw [h1, norm_expU_apply hB, norm_expU_apply hC]
    have h2 : (gC - gB) x = (-Complex.I) • (C x - B x) := by
      simp [hgB, hgC, smul_sub]
    rw [h2, norm_smul, hK]
    simp [norm_sub_rev]
  have hmvt : ‖P t x - P 0 x‖ ≤ K * ‖t - 0‖ :=
    Convex.norm_image_sub_le_of_norm_hasDerivWithin_le
      (f := fun r => P r x) (f' := fun r => D r x) (C := K) (s := Set.univ)
      (fun r _ => (hderiv r).hasDerivWithinAt) (fun r _ => le_of_eq (hnorm r)) convex_univ
      (Set.mem_univ 0) (Set.mem_univ t)
  have hPt : P t x = expU C t x := by simp [hP]
  have hP0 : P 0 x = expU B t x := by simp [hP]
  rw [hPt, hP0] at hmvt
  calc ‖expU B t x - expU C t x‖
      = ‖expU C t x - expU B t x‖ := norm_sub_rev _ _
    _ ≤ K * ‖t - 0‖ := hmvt
    _ = |t| * K := by rw [sub_zero, Real.norm_eq_abs]; ring

/-- `‖e^{-itB} x - x‖ ≤ |t| ‖B x‖`. -/
theorem norm_expU_sub_self_le (hB : IsSelfAdjoint B) (t : ℝ) (x : F) :
    ‖expU B t x - x‖ ≤ |t| * ‖B x‖ := by
  have h := norm_expU_sub_apply_le hB (C := 0) (IsSelfAdjoint.zero _) (Commute.zero_right B) t x
  simpa [expU_zero_op] using h

omit [CompleteSpace F] in
/-- A sequence of isometric operators which converges pointwise on a dense set converges
pointwise everywhere (Cauchy version). -/
theorem cauchySeq_of_dense_of_isometry {G : ℕ → F →L[ℂ] F} (hiso : ∀ n y, ‖G n y‖ = ‖y‖)
    {D : Set F} (hD : Dense D) (hC : ∀ y ∈ D, CauchySeq (fun n => G n y)) (y : F) :
    CauchySeq (fun n => G n y) := by
  rw [Metric.cauchySeq_iff]
  intro ε hε
  obtain ⟨z, hz, hyz⟩ := hD.exists_dist_lt y (ε := ε / 3) (by linarith)
  obtain ⟨N, hN⟩ := Metric.cauchySeq_iff.mp (hC z hz) (ε / 3) (by linarith)
  refine ⟨N, fun k hk l hl => ?_⟩
  have hkz : dist (G k y) (G k z) = dist y z := by
    rw [dist_eq_norm, dist_eq_norm, ← map_sub, hiso]
  have hlz : dist (G l z) (G l y) = dist y z := by
    rw [dist_eq_norm, dist_eq_norm, ← map_sub, hiso, norm_sub_rev]
  calc dist (G k y) (G l y)
      ≤ dist (G k y) (G k z) + dist (G k z) (G l z) + dist (G l z) (G l y) :=
        dist_triangle4 _ _ _ _
    _ < ε / 3 + ε / 3 + ε / 3 := by
        rw [hkz, hlz]
        have := hN k hk l hl
        linarith
    _ = ε := by ring

/-! ## The approximating unitary groups `e^{-itT_a}` -/

variable {T : Submodule ℂ (F × F)} {a b : ℝ}

/-- The Yosida approximations of a non-negative self-adjoint relation commute. -/
theorem commute_invCLMAt (hT : IsNonnegSelfAdjoint T) (ha : 0 < a) (hb : 0 < b) :
    Commute (invCLMAt hT ha) (invCLMAt hT hb) := by
  change invCLMAt hT ha * invCLMAt hT hb = invCLMAt hT hb * invCLMAt hT ha
  ext x
  simpa using invCLMAt_comm hT ha hb x

theorem commute_yosidaCLM (hT : IsNonnegSelfAdjoint T) (ha : 0 < a) (hb : 0 < b) :
    Commute (yosidaCLM hT ha) (yosidaCLM hT hb) := by
  have hc := commute_invCLMAt hT ha hb
  have h1 : Commute ((a : ℂ) • invCLMAt hT ha) (1 - (b : ℂ) • invCLMAt hT hb) :=
    (Commute.one_right _).sub_right ((hc.smul_left (a : ℂ)).smul_right (b : ℂ))
  have h2 : Commute (1 - (a : ℂ) • invCLMAt hT ha) (1 - (b : ℂ) • invCLMAt hT hb) :=
    (Commute.one_left _).sub_left h1
  simpa only [yosidaCLM] using (h2.smul_left (a : ℂ)).smul_right (b : ℂ)

/-- The Yosida approximation commutes with every resolvent. -/
theorem commute_yosidaCLM_invCLMAt (hT : IsNonnegSelfAdjoint T) (ha : 0 < a) (hb : 0 < b) :
    Commute (yosidaCLM hT ha) (invCLMAt hT hb) := by
  have hc := commute_invCLMAt hT ha hb
  have h1 : Commute ((a : ℂ) • invCLMAt hT ha) (invCLMAt hT hb) := hc.smul_left (a : ℂ)
  have h2 : Commute (1 - (a : ℂ) • invCLMAt hT ha) (invCLMAt hT hb) :=
    (Commute.one_left _).sub_left h1
  simpa only [yosidaCLM] using h2.smul_left (a : ℂ)

theorem commute_yosidaAt (hT : IsNonnegSelfAdjoint T) (n m : ℕ) :
    Commute (yosidaAt hT n) (yosidaAt hT m) :=
  commute_yosidaCLM hT _ _

theorem isSelfAdjoint_yosidaAt (hT : IsNonnegSelfAdjoint T) (n : ℕ) :
    IsSelfAdjoint (yosidaAt hT n) :=
  isSelfAdjoint_yosidaCLM hT _

/-- The approximating unitary group `e^{-itT_n}` built from the Yosida approximation. -/
noncomputable def approxU (hT : IsNonnegSelfAdjoint T) (n : ℕ) (t : ℝ) : F →L[ℂ] F :=
  expU (yosidaAt hT n) t

@[simp] theorem approxU_zero (hT : IsNonnegSelfAdjoint T) (n : ℕ) : approxU hT n 0 = 1 :=
  expU_zero _

theorem approxU_add (hT : IsNonnegSelfAdjoint T) (n : ℕ) (s t : ℝ) :
    approxU hT n (s + t) = approxU hT n s * approxU hT n t :=
  expU_add _ s t

theorem norm_approxU_apply (hT : IsNonnegSelfAdjoint T) (n : ℕ) (t : ℝ) (x : F) :
    ‖approxU hT n t x‖ = ‖x‖ :=
  norm_expU_apply (isSelfAdjoint_yosidaAt hT n) t x

/-- The fundamental estimate `‖(e^{-itT_n} - e^{-itT_m}) x‖ ≤ |t| ‖(T_n - T_m) x‖`. -/
theorem norm_approxU_sub_apply_le (hT : IsNonnegSelfAdjoint T) (n m : ℕ) (t : ℝ) (x : F) :
    ‖approxU hT n t x - approxU hT m t x‖ ≤ |t| * ‖yosidaAt hT n x - yosidaAt hT m x‖ :=
  norm_expU_sub_apply_le (isSelfAdjoint_yosidaAt hT n) (isSelfAdjoint_yosidaAt hT m)
    (commute_yosidaAt hT n m) t x

/-! ## The limit group -/

theorem approxU_cauchy_of_mem (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) {h k : F} (hk : (h, k) ∈ T) (t : ℝ) :
    CauchySeq (fun n : ℕ => approxU hT n t h) := by
  have hy : CauchySeq (fun n : ℕ => yosidaAt hT n h) := (tendsto_yosidaAt hT hsv hk).cauchySeq
  rw [Metric.cauchySeq_iff]
  intro ε hε
  have hpos : (0 : ℝ) < ε / (|t| + 1) := by positivity
  obtain ⟨N, hN⟩ := Metric.cauchySeq_iff.mp hy _ hpos
  refine ⟨N, fun n hn m hm => ?_⟩
  have hnm := hN n hn m hm
  rw [dist_eq_norm] at hnm ⊢
  have habs : (0 : ℝ) ≤ |t| := abs_nonneg t
  calc ‖approxU hT n t h - approxU hT m t h‖
      ≤ |t| * ‖yosidaAt hT n h - yosidaAt hT m h‖ := norm_approxU_sub_apply_le hT n m t h
    _ ≤ |t| * (ε / (|t| + 1)) := by gcongr
    _ < ε := by
        rw [mul_div_assoc', div_lt_iff₀ (by positivity)]
        nlinarith

theorem approxU_cauchy (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) (t : ℝ) (x : F) :
    CauchySeq (fun n : ℕ => approxU hT n t x) := by
  refine cauchySeq_of_dense_of_isometry (G := fun n => approxU hT n t)
    (fun n y => norm_approxU_apply hT n t y) (dense_domain hT hsv) ?_ x
  intro y hy
  obtain ⟨p, hp, hp1⟩ := Submodule.mem_map.1 hy
  have hpy : (y, p.2) ∈ T := by
    have hpe : p = (y, p.2) := by
      rw [← hp1]
      simp
    rwa [← hpe]
  exact approxU_cauchy_of_mem hT hsv hpy t

/-- The unitary group `e^{-itT}` generated by a non-negative self-adjoint linear relation,
as a function. -/
noncomputable def unitaryFun (hT : IsNonnegSelfAdjoint T) (t : ℝ) (x : F) : F :=
  limUnder atTop (fun n : ℕ => approxU hT n t x)

theorem tendsto_unitaryFun (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) (t : ℝ) (x : F) :
    Tendsto (fun n : ℕ => approxU hT n t x) atTop (𝓝 (unitaryFun hT t x)) := by
  obtain ⟨z, hz⟩ := cauchySeq_tendsto_of_complete (approxU_cauchy hT hsv t x)
  rw [unitaryFun, hz.limUnder_eq]
  exact hz

theorem norm_unitaryFun (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) (t : ℝ) (x : F) :
    ‖unitaryFun hT t x‖ = ‖x‖ := by
  have h1 : Tendsto (fun n : ℕ => ‖approxU hT n t x‖) atTop (𝓝 ‖unitaryFun hT t x‖) :=
    (tendsto_unitaryFun hT hsv t x).norm
  have h2 : (fun n : ℕ => ‖approxU hT n t x‖) = fun _ : ℕ => ‖x‖ := by
    funext n; exact norm_approxU_apply hT n t x
  rw [h2] at h1
  exact tendsto_nhds_unique h1 tendsto_const_nhds

/-- `e^{-itT}` as a linear map. -/
noncomputable def unitaryLinear (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) (t : ℝ) : F →ₗ[ℂ] F where
  toFun x := unitaryFun hT t x
  map_add' x y := by
    refine tendsto_nhds_unique (tendsto_unitaryFun hT hsv t (x + y)) ?_
    have h : (fun n : ℕ => approxU hT n t (x + y))
        = fun n : ℕ => approxU hT n t x + approxU hT n t y := by
      funext n; rw [map_add]
    rw [h]
    exact (tendsto_unitaryFun hT hsv t x).add (tendsto_unitaryFun hT hsv t y)
  map_smul' c x := by
    refine tendsto_nhds_unique (tendsto_unitaryFun hT hsv t (c • x)) ?_
    have h : (fun n : ℕ => approxU hT n t (c • x))
        = fun n : ℕ => c • approxU hT n t x := by
      funext n; rw [map_smul]
    rw [h]
    exact (tendsto_unitaryFun hT hsv t x).const_smul c

/-- **The unitary group `e^{-itT}`** generated by a non-negative self-adjoint linear
relation. -/
noncomputable def unitaryU (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) (t : ℝ) : F →L[ℂ] F :=
  (unitaryLinear hT hsv t).mkContinuous 1 (fun x => by
    simp only [unitaryLinear, LinearMap.coe_mk, AddHom.coe_mk, one_mul]
    exact le_of_eq (norm_unitaryFun hT hsv t x))

@[simp] theorem unitaryU_apply (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) (t : ℝ) (x : F) :
    unitaryU hT hsv t x = unitaryFun hT t x := rfl

theorem tendsto_unitaryU (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) (t : ℝ) (x : F) :
    Tendsto (fun n : ℕ => approxU hT n t x) atTop (𝓝 (unitaryU hT hsv t x)) :=
  tendsto_unitaryFun hT hsv t x

theorem norm_unitaryU_apply (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) (t : ℝ) (x : F) :
    ‖unitaryU hT hsv t x‖ = ‖x‖ :=
  norm_unitaryFun hT hsv t x

@[simp] theorem unitaryU_zero (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) : unitaryU hT hsv 0 = 1 := by
  ext x
  refine tendsto_nhds_unique (tendsto_unitaryU hT hsv 0 x) ?_
  have h : (fun n : ℕ => approxU hT n 0 x) = fun _ : ℕ => x := by
    funext n; simp
  rw [h]
  simp

/-- **The one-parameter group law** `U (s + t) = U s U t`. -/
theorem unitaryU_add (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) (s t : ℝ) :
    unitaryU hT hsv (s + t) = unitaryU hT hsv s * unitaryU hT hsv t := by
  ext x
  refine tendsto_nhds_unique (tendsto_unitaryU hT hsv (s + t) x) ?_
  have h : (fun n : ℕ => approxU hT n (s + t) x)
      = fun n : ℕ => approxU hT n s (approxU hT n t x) := by
    funext n
    rw [approxU_add]
    rfl
  rw [h]
  rw [Metric.tendsto_atTop]
  intro ε hε
  obtain ⟨N₁, hN₁⟩ := Metric.tendsto_atTop.mp (tendsto_unitaryU hT hsv t x) (ε / 2) (by linarith)
  obtain ⟨N₂, hN₂⟩ :=
    Metric.tendsto_atTop.mp (tendsto_unitaryU hT hsv s (unitaryU hT hsv t x)) (ε / 2)
      (by linarith)
  refine ⟨max N₁ N₂, fun n hn => ?_⟩
  have hn1 : N₁ ≤ n := le_trans (le_max_left _ _) hn
  have hn2 : N₂ ≤ n := le_trans (le_max_right _ _) hn
  have h1 : dist (approxU hT n s (approxU hT n t x)) (approxU hT n s (unitaryU hT hsv t x))
      < ε / 2 := by
    rw [dist_eq_norm, ← map_sub, norm_approxU_apply]
    have := hN₁ n hn1
    rwa [dist_eq_norm] at this
  have h2 : dist (approxU hT n s (unitaryU hT hsv t x))
      (unitaryU hT hsv s (unitaryU hT hsv t x)) < ε / 2 := hN₂ n hn2
  calc dist (approxU hT n s (approxU hT n t x)) (unitaryU hT hsv s (unitaryU hT hsv t x))
      ≤ dist (approxU hT n s (approxU hT n t x)) (approxU hT n s (unitaryU hT hsv t x))
        + dist (approxU hT n s (unitaryU hT hsv t x))
            (unitaryU hT hsv s (unitaryU hT hsv t x)) := dist_triangle _ _ _
    _ < ε := by linarith

theorem unitaryU_apply_unitaryU (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) (s t : ℝ) (x : F) :
    unitaryU hT hsv s (unitaryU hT hsv t x) = unitaryU hT hsv (s + t) x := by
  rw [unitaryU_add hT hsv]; rfl

theorem unitaryU_surjective (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) (t : ℝ) :
    Function.Surjective (unitaryU hT hsv t) := by
  intro y
  refine ⟨unitaryU hT hsv (-t) y, ?_⟩
  rw [unitaryU_apply_unitaryU]
  simp

/-- **`e^{-itT}` is unitary.** -/
theorem unitaryU_mem_unitary (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) (t : ℝ) :
    unitaryU hT hsv t ∈ unitary (F →L[ℂ] F) := by
  have hiso : ∀ x y : F, ⟪unitaryU hT hsv t x, unitaryU hT hsv t y⟫_ℂ = ⟪x, y⟫_ℂ := by
    intro x y
    have hn : ∀ z : F, ‖(unitaryU hT hsv t : F →ₗ[ℂ] F) z‖ = ‖z‖ :=
      fun z => norm_unitaryU_apply hT hsv t z
    exact (LinearIsometry.mk (unitaryU hT hsv t : F →ₗ[ℂ] F) hn).inner_map_map x y
  have hstar : star (unitaryU hT hsv t) * unitaryU hT hsv t = 1 := by
    ext x
    have : ContinuousLinearMap.adjoint (unitaryU hT hsv t) (unitaryU hT hsv t x) = x := by
      refine ext_inner_right ℂ ?_
      intro y
      rw [ContinuousLinearMap.adjoint_inner_left, hiso]
    simpa [ContinuousLinearMap.star_eq_adjoint] using this
  refine Unitary.mem_iff.mpr ⟨hstar, ?_⟩
  ext y
  obtain ⟨x, hx⟩ := unitaryU_surjective hT hsv t y
  have hxx : (star (unitaryU hT hsv t)) (unitaryU hT hsv t x) = x := by
    have h := congrArg (fun (S : F →L[ℂ] F) => S x) hstar
    simpa using h
  rw [← hx]
  simp only [ContinuousLinearMap.mul_apply, ContinuousLinearMap.one_apply, hxx]

/-! ## Rate of convergence, strong continuity -/

/-- Rate of convergence of the approximations on the domain. -/
theorem norm_unitaryU_sub_approxU_le (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) {h k : F} (hk : (h, k) ∈ T) (m : ℕ) (t : ℝ) :
    ‖unitaryU hT hsv t h - approxU hT m t h‖ ≤ |t| * ‖k - yosidaAt hT m h‖ := by
  have hf : Tendsto (fun n : ℕ => ‖approxU hT n t h - approxU hT m t h‖) atTop
      (𝓝 ‖unitaryU hT hsv t h - approxU hT m t h‖) :=
    ((tendsto_unitaryU hT hsv t h).sub tendsto_const_nhds).norm
  have hg : Tendsto (fun n : ℕ => |t| * ‖yosidaAt hT n h - yosidaAt hT m h‖) atTop
      (𝓝 (|t| * ‖k - yosidaAt hT m h‖)) :=
    ((((tendsto_yosidaAt hT hsv hk).sub tendsto_const_nhds).norm).const_mul _)
  exact le_of_tendsto_of_tendsto' hf hg (fun n => norm_approxU_sub_apply_le hT n m t h)

/-- On the domain, `‖e^{-itT} h - h‖ ≤ |t| ‖k‖`. -/
theorem norm_unitaryU_sub_of_mem (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) {h k : F} (hk : (h, k) ∈ T) (t : ℝ) :
    ‖unitaryU hT hsv t h - h‖ ≤ |t| * ‖k‖ := by
  have hf : Tendsto (fun n : ℕ => ‖approxU hT n t h - h‖) atTop
      (𝓝 ‖unitaryU hT hsv t h - h‖) :=
    ((tendsto_unitaryU hT hsv t h).sub tendsto_const_nhds).norm
  refine le_of_tendsto hf (Filter.Eventually.of_forall fun n => ?_)
  calc ‖approxU hT n t h - h‖ ≤ |t| * ‖yosidaAt hT n h‖ :=
        norm_expU_sub_self_le (isSelfAdjoint_yosidaAt hT n) t h
    _ ≤ |t| * ‖k‖ := by
        have := norm_yosidaCLM_le_of_mem hT (a := (n : ℝ) + 1) (by positivity) hk
        gcongr
        exact this

/-- **Strong continuity at `0`.** -/
theorem tendsto_unitaryU_zero (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) (x : F) :
    Tendsto (fun t : ℝ => unitaryU hT hsv t x) (𝓝 0) (𝓝 x) := by
  rw [Metric.tendsto_nhds_nhds]
  intro ε hε
  obtain ⟨z, hz, hxz⟩ := (dense_domain hT hsv).exists_dist_lt x (ε := ε / 3) (by linarith)
  obtain ⟨p, hp, hp1⟩ := Submodule.mem_map.1 hz
  have hpz : (z, p.2) ∈ T := by
    have hpe : p = (z, p.2) := by
      rw [← hp1]
      simp
    rwa [← hpe]
  refine ⟨ε / (3 * (‖p.2‖ + 1)), by positivity, fun t ht => ?_⟩
  rw [Real.dist_eq, sub_zero] at ht
  have hzx : ‖x - z‖ < ε / 3 := by rw [dist_eq_norm] at hxz; exact hxz
  have h1 : ‖unitaryU hT hsv t (x - z)‖ = ‖x - z‖ := norm_unitaryU_apply hT hsv t _
  have h2 : ‖unitaryU hT hsv t z - z‖ ≤ |t| * ‖p.2‖ := norm_unitaryU_sub_of_mem hT hsv hpz t
  have hsplit : unitaryU hT hsv t x - x
      = unitaryU hT hsv t (x - z) + (unitaryU hT hsv t z - z) + (z - x) := by
    rw [map_sub]
    abel
  have h3 : |t| * ‖p.2‖ < ε / 3 := by
    have hden : (0 : ℝ) < 3 * (‖p.2‖ + 1) := by positivity
    have h4 : |t| * (3 * (‖p.2‖ + 1)) < ε := by
      rw [← lt_div_iff₀ hden]; exact ht
    nlinarith [norm_nonneg p.2, abs_nonneg t]
  rw [dist_eq_norm]
  calc ‖unitaryU hT hsv t x - x‖
      ≤ ‖unitaryU hT hsv t (x - z)‖ + ‖unitaryU hT hsv t z - z‖ + ‖z - x‖ := by
        rw [hsplit]
        exact (norm_add_le _ _).trans (by gcongr; exact norm_add_le _ _)
    _ < ε := by
        rw [h1, norm_sub_rev z x]
        linarith [h2.trans_lt h3]

/-- **The group `e^{-itT}` is strongly continuous.** -/
theorem continuous_unitaryU_apply (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) (x : F) :
    Continuous (fun t : ℝ => unitaryU hT hsv t x) := by
  refine continuous_iff_continuousAt.mpr (fun t₀ => ?_)
  have h1 : Tendsto (fun t : ℝ => t - t₀) (𝓝 t₀) (𝓝 0) := by
    simpa using (continuous_sub_right t₀).tendsto t₀
  have h2 : Tendsto (fun t : ℝ => unitaryU hT hsv (t - t₀) x) (𝓝 t₀) (𝓝 x) :=
    (tendsto_unitaryU_zero hT hsv x).comp h1
  have h3 : Tendsto (fun t : ℝ => unitaryU hT hsv t₀ (unitaryU hT hsv (t - t₀) x)) (𝓝 t₀)
      (𝓝 (unitaryU hT hsv t₀ x)) :=
    ((unitaryU hT hsv t₀).continuous.tendsto x).comp h2
  have heq : (fun t : ℝ => unitaryU hT hsv t₀ (unitaryU hT hsv (t - t₀) x))
      = fun t : ℝ => unitaryU hT hsv t x := by
    funext t
    rw [unitaryU_apply_unitaryU]
    have hts : t₀ + (t - t₀) = t := by ring
    rw [hts]
  rw [heq] at h3
  exact h3

/-- The approximating groups converge **uniformly on bounded time intervals**. -/
theorem tendstoUniformlyOn_approxU (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) (z : F) (R : ℝ) :
    TendstoUniformlyOn (fun (n : ℕ) (t : ℝ) => approxU hT n t z)
      (fun t : ℝ => unitaryU hT hsv t z) atTop {t : ℝ | |t| ≤ R} := by
  rw [Metric.tendstoUniformlyOn_iff]
  intro ε hε
  obtain ⟨y, hy, hzy⟩ := (dense_domain hT hsv).exists_dist_lt z (ε := ε / 3) (by linarith)
  obtain ⟨p, hp, hp1⟩ := Submodule.mem_map.1 hy
  have hpy : (y, p.2) ∈ T := by
    have hpe : p = (y, p.2) := by
      rw [← hp1]
      simp
    rwa [← hpe]
  set R' : ℝ := max R 0 with hR'
  have hR'0 : (0 : ℝ) ≤ R' := le_max_right _ _
  have hten : Tendsto (fun n : ℕ => ‖p.2 - yosidaAt hT n y‖) atTop (𝓝 0) := by
    have h := (tendsto_const_nhds (x := p.2) (f := atTop (α := ℕ))).sub
      (tendsto_yosidaAt hT hsv hpy)
    simpa using h.norm
  have hev : ∀ᶠ n : ℕ in atTop, ‖p.2 - yosidaAt hT n y‖ < ε / (3 * (R' + 1)) := by
    have hpos : (0 : ℝ) < ε / (3 * (R' + 1)) := by positivity
    obtain ⟨N, hN⟩ := Metric.tendsto_atTop.mp hten _ hpos
    filter_upwards [eventually_ge_atTop N] with n hn
    simpa [Real.dist_eq, abs_of_nonneg (norm_nonneg _)] using hN n hn
  filter_upwards [hev] with n hn t ht
  have htR : |t| ≤ R' := le_trans ht (le_max_left _ _)
  have hsplit : unitaryU hT hsv t z - approxU hT n t z
      = unitaryU hT hsv t (z - y) + (unitaryU hT hsv t y - approxU hT n t y)
        + approxU hT n t (y - z) := by
    rw [map_sub, map_sub]
    abel
  have h1 : ‖unitaryU hT hsv t (z - y)‖ = ‖z - y‖ := norm_unitaryU_apply hT hsv t _
  have h2 : ‖approxU hT n t (y - z)‖ = ‖y - z‖ := norm_approxU_apply hT n t _
  have h3 : ‖unitaryU hT hsv t y - approxU hT n t y‖ ≤ |t| * ‖p.2 - yosidaAt hT n y‖ :=
    norm_unitaryU_sub_approxU_le hT hsv hpy n t
  have h4 : |t| * ‖p.2 - yosidaAt hT n y‖ < ε / 3 := by
    have hR1 : (0 : ℝ) < R' + 1 := by linarith
    calc |t| * ‖p.2 - yosidaAt hT n y‖ ≤ (R' + 1) * ‖p.2 - yosidaAt hT n y‖ := by
          gcongr
          linarith
      _ < (R' + 1) * (ε / (3 * (R' + 1))) := mul_lt_mul_of_pos_left hn hR1
      _ = ε / 3 := by field_simp
  have hzy' : ‖z - y‖ < ε / 3 := by rw [dist_eq_norm] at hzy; exact hzy
  rw [dist_eq_norm]
  calc ‖unitaryU hT hsv t z - approxU hT n t z‖
      ≤ ‖unitaryU hT hsv t (z - y)‖ + ‖unitaryU hT hsv t y - approxU hT n t y‖
          + ‖approxU hT n t (y - z)‖ := by
        rw [hsplit]
        exact (norm_add_le _ _).trans (by gcongr; exact norm_add_le _ _)
    _ < ε := by
        rw [h1, h2, norm_sub_rev y z]
        linarith [h3.trans_lt h4]

/-! ## The group leaves the relation invariant and solves the Schrödinger equation -/

/-- `e^{-itT}` commutes with the resolvent `(T + a)⁻¹`. -/
theorem unitaryU_invCLMAt (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) (ha : 0 < a) (t : ℝ) (y : F) :
    unitaryU hT hsv t (invCLMAt hT ha y) = invCLMAt hT ha (unitaryU hT hsv t y) := by
  have hcomm : ∀ n : ℕ,
      approxU hT n t (invCLMAt hT ha y) = invCLMAt hT ha (approxU hT n t y) := by
    intro n
    have hc : Commute (yosidaAt hT n) (invCLMAt hT ha) := commute_yosidaCLM_invCLMAt hT _ ha
    have hexp : Commute (approxU hT n t) (invCLMAt hT ha) :=
      ((hc.smul_left (-Complex.I)).smul_left t).exp_left
    have h := congrArg (fun S : F →L[ℂ] F => S y) hexp.eq
    simpa using h
  refine tendsto_nhds_unique (tendsto_unitaryU hT hsv t (invCLMAt hT ha y)) ?_
  have h2 : Tendsto (fun n : ℕ => invCLMAt hT ha (approxU hT n t y)) atTop
      (𝓝 (invCLMAt hT ha (unitaryU hT hsv t y))) :=
    ((invCLMAt hT ha).continuous.tendsto _).comp (tendsto_unitaryU hT hsv t y)
  have heq : (fun n : ℕ => approxU hT n t (invCLMAt hT ha y))
      = fun n : ℕ => invCLMAt hT ha (approxU hT n t y) := funext hcomm
  rw [heq]
  exact h2

/-- **The group leaves the relation invariant**: `(h, k) ∈ T` implies
`(e^{-itT} h, e^{-itT} k) ∈ T`. -/
theorem mem_unitaryU (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) {h k : F} (hk : (h, k) ∈ T) (t : ℝ) :
    (unitaryU hT hsv t h, unitaryU hT hsv t k) ∈ T := by
  have h1 : (0 : ℝ) < 1 := one_pos
  have hy : invCLMAt hT h1 (h + k) = h := by
    refine invCLMAt_eq_of_mem hT h1 ?_
    have hrw : h + k - ((1 : ℝ) : ℂ) • h = k := by push_cast; module
    rw [hrw]
    exact hk
  have hmem := invCLMAt_mem hT h1 (unitaryU hT hsv t (h + k))
  rw [← unitaryU_invCLMAt hT hsv h1 t (h + k), hy] at hmem
  have hrw2 : unitaryU hT hsv t (h + k) - ((1 : ℝ) : ℂ) • unitaryU hT hsv t h
      = unitaryU hT hsv t k := by
    rw [map_add]
    push_cast
    module
  rwa [hrw2] at hmem

/-- **The Schrödinger equation** `d/dt e^{-itT} h = -i e^{-itT} k` for `(h, k) ∈ T`. -/
theorem hasDerivAt_unitaryU (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) {h k : F} (hk : (h, k) ∈ T) (t : ℝ) :
    HasDerivAt (fun s : ℝ => unitaryU hT hsv s h)
      ((-Complex.I) • unitaryU hT hsv t k) t := by
  have hsub : Set.Ioo (t - 1) (t + 1) ⊆ {s : ℝ | |s| ≤ |t| + 1} := by
    intro s hs
    simp only [Set.mem_setOf_eq, abs_le]
    constructor
    · linarith [neg_abs_le t, hs.1]
    · linarith [le_abs_self t, hs.2]
  have hderiv : ∀ (n : ℕ) (s : ℝ), HasDerivAt (fun r : ℝ => approxU hT n r h)
      (approxU hT n s (((-Complex.I) • yosidaAt hT n) h)) s :=
    fun n s => hasDerivAt_expU_apply (yosidaAt hT n) s h
  have huniform : TendstoUniformlyOn
      (fun (n : ℕ) (s : ℝ) => approxU hT n s (((-Complex.I) • yosidaAt hT n) h))
      (fun s : ℝ => (-Complex.I) • unitaryU hT hsv s k) atTop (Set.Ioo (t - 1) (t + 1)) := by
    rw [Metric.tendstoUniformlyOn_iff]
    intro ε hε
    have hU := (Metric.tendstoUniformlyOn_iff.1 (tendstoUniformlyOn_approxU hT hsv k (|t| + 1)))
      (ε / 2) (by linarith)
    have hy : ∀ᶠ n : ℕ in atTop, ‖k - yosidaAt hT n h‖ < ε / 2 := by
      obtain ⟨N, hN⟩ := Metric.tendsto_atTop.mp (tendsto_yosidaAt hT hsv hk) (ε / 2)
        (by linarith)
      filter_upwards [eventually_ge_atTop N] with n hn
      have := hN n hn
      rwa [dist_eq_norm, norm_sub_rev] at this
    filter_upwards [hU, hy] with n hn hn2 s hs
    have hsR : s ∈ {s : ℝ | |s| ≤ |t| + 1} := hsub hs
    have hsm : approxU hT n s (((-Complex.I) • yosidaAt hT n) h)
        = (-Complex.I) • approxU hT n s (yosidaAt hT n h) := by
      simp [map_smul]
    have hsplit : (-Complex.I) • unitaryU hT hsv s k
          - (-Complex.I) • approxU hT n s (yosidaAt hT n h)
        = (-Complex.I) • ((unitaryU hT hsv s k - approxU hT n s k)
            + approxU hT n s (k - yosidaAt hT n h)) := by
      rw [map_sub]
      module
    have hnormI : ‖(-Complex.I)‖ = 1 := by simp
    rw [dist_eq_norm, hsm, hsplit, norm_smul, hnormI, one_mul]
    have hb1 : ‖unitaryU hT hsv s k - approxU hT n s k‖ < ε / 2 := by
      have := hn s hsR
      rwa [dist_eq_norm] at this
    have hb2 : ‖approxU hT n s (k - yosidaAt hT n h)‖ < ε / 2 := by
      rw [norm_approxU_apply]
      exact hn2
    calc ‖(unitaryU hT hsv s k - approxU hT n s k) + approxU hT n s (k - yosidaAt hT n h)‖
        ≤ ‖unitaryU hT hsv s k - approxU hT n s k‖
            + ‖approxU hT n s (k - yosidaAt hT n h)‖ := norm_add_le _ _
      _ < ε := by linarith
  exact hasDerivAt_of_tendstoUniformlyOn (f := fun (n : ℕ) (s : ℝ) => approxU hT n s h)
    (f' := fun (n : ℕ) (s : ℝ) => approxU hT n s (((-Complex.I) • yosidaAt hT n) h))
    (g := fun s : ℝ => unitaryU hT hsv s h)
    (g' := fun s : ℝ => (-Complex.I) • unitaryU hT hsv s k)
    isOpen_Ioo huniform (Filter.Eventually.of_forall fun n s _ => hderiv n s)
    (fun s _ => tendsto_unitaryU hT hsv s h) (by constructor <;> linarith)

/-! ## Conservation laws -/

/-- `e^{-itT}` preserves the inner product. -/
theorem inner_unitaryU (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) (t : ℝ) (x y : F) :
    ⟪unitaryU hT hsv t x, unitaryU hT hsv t y⟫_ℂ = ⟪x, y⟫_ℂ := by
  have hn : ∀ z : F, ‖(unitaryU hT hsv t : F →ₗ[ℂ] F) z‖ = ‖z‖ :=
    fun z => norm_unitaryU_apply hT hsv t z
  exact (LinearIsometry.mk (unitaryU hT hsv t : F →ₗ[ℂ] F) hn).inner_map_map x y

/-- **Conservation of energy**: the orbit `t ↦ e^{-itT} h` of a point `(h, k) ∈ T` stays in
the relation, and the quantity `⟪h, k⟫` — the expectation of `T` in the state `h` — is
constant along it. -/
theorem inner_unitaryU_of_mem (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) {h k : F} (hk : (h, k) ∈ T) (t : ℝ) :
    (unitaryU hT hsv t h, unitaryU hT hsv t k) ∈ T ∧
      ⟪unitaryU hT hsv t h, unitaryU hT hsv t k⟫_ℂ = ⟪h, k⟫_ℂ :=
  ⟨mem_unitaryU hT hsv hk t, inner_unitaryU hT hsv t h k⟩

omit [CompleteSpace F] in
/-- The inner product `⟪x, T x⟫` at a point of a non-negative self-adjoint relation is real. -/
theorem inner_mem_conj_eq (hT : IsNonnegSelfAdjoint T) {x y : F} (hxy : (x, y) ∈ T) :
    (starRingEnd ℂ) ⟪x, y⟫_ℂ = ⟪x, y⟫_ℂ := by
  have h := symm_inner hT hxy hxy
  simpa [inner_conj_symm] using h

/-- **Uniqueness of solutions of the Schrödinger equation.**  Any differentiable curve `u`
which stays in the relation, `(u s, k s) ∈ T`, and satisfies `u' s = -i k s`, is the orbit
`u s = e^{-isT} (u 0)` of the group. -/
theorem eq_unitaryU_of_hasDerivAt (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) {u kk : ℝ → F}
    (hmem : ∀ s : ℝ, (u s, kk s) ∈ T)
    (hu : ∀ s : ℝ, HasDerivAt u ((-Complex.I) • kk s) s) (t : ℝ) :
    u t = unitaryU hT hsv t (u 0) := by
  set w : ℝ → F := fun s => u s - unitaryU hT hsv s (u 0) with hwdef
  set kw : ℝ → F := fun s => kk s - unitaryU hT hsv s (kk 0) with hkwdef
  have hmemw : ∀ s : ℝ, (w s, kw s) ∈ T := fun s =>
    T.sub_mem (hmem s) (mem_unitaryU hT hsv (hmem 0) s)
  have hderivw : ∀ s : ℝ, HasDerivAt w ((-Complex.I) • kw s) s := by
    intro s
    have h2 := hasDerivAt_unitaryU hT hsv (hmem 0) s
    have h3 := (hu s).sub h2
    convert h3 using 1 <;>
      (first | rfl | rw [hkwdef, smul_sub])
  have hf : ∀ s : ℝ, HasDerivAt (fun r : ℝ => ‖w r‖ ^ 2) 0 s := by
    intro s
    have hin := (hderivw s).inner ℂ (hderivw s)
    have hzero : ⟪w s, (-Complex.I) • kw s⟫_ℂ + ⟪(-Complex.I) • kw s, w s⟫_ℂ = 0 := by
      have hreal := inner_mem_conj_eq hT (hmemw s)
      have hcs : (starRingEnd ℂ) ⟪kw s, w s⟫_ℂ = ⟪w s, kw s⟫_ℂ := inner_conj_symm _ _
      have hswap : ⟪kw s, w s⟫_ℂ = ⟪w s, kw s⟫_ℂ := by
        have h := congrArg (starRingEnd ℂ) hcs
        simp only [Complex.conj_conj] at h
        rw [h, hreal]
      have h1 : ⟪w s, (-Complex.I) • kw s⟫_ℂ = (-Complex.I) * ⟪w s, kw s⟫_ℂ := by
        rw [inner_smul_right]
      have h2 : ⟪(-Complex.I) • kw s, w s⟫_ℂ = Complex.I * ⟪kw s, w s⟫_ℂ := by
        rw [inner_smul_left]
        simp
      rw [h1, h2, hswap]
      ring
    rw [hzero] at hin
    have hre := Complex.reCLM.hasFDerivAt.comp_hasDerivAt s hin
    simp only [map_zero, Function.comp_def] at hre
    have hfun : (fun r : ℝ => Complex.reCLM (⟪w r, w r⟫_ℂ)) = fun r : ℝ => ‖w r‖ ^ 2 := by
      funext r
      simpa using inner_self_eq_norm_sq (𝕜 := ℂ) (w r)
    rwa [hfun] at hre
  have hconst : ‖w t‖ ^ 2 = ‖w 0‖ ^ 2 := by
    have hmvt := Convex.norm_image_sub_le_of_norm_hasDerivWithin_le
      (f := fun r : ℝ => ‖w r‖ ^ 2) (f' := fun _ : ℝ => (0 : ℝ)) (C := 0) (s := Set.univ)
      (fun r _ => (hf r).hasDerivWithinAt) (fun r _ => by simp) convex_univ
      (Set.mem_univ 0) (Set.mem_univ t)
    have h0 : ‖‖w t‖ ^ 2 - ‖w 0‖ ^ 2‖ ≤ 0 := by simpa using hmvt
    have := norm_le_zero_iff.1 h0
    linarith [sub_eq_zero.1 this]
  have hz : unitaryU hT hsv 0 (u 0) = u 0 := by
    rw [unitaryU_zero hT hsv]
    simp
  have hw0 : w 0 = 0 := by
    calc w 0 = u 0 - unitaryU hT hsv 0 (u 0) := rfl
      _ = 0 := by rw [hz]; simp
  rw [hw0] at hconst
  have hwt : u t - unitaryU hT hsv t (u 0) = 0 := by
    have hsq : ‖w t‖ ^ 2 = 0 := by simpa using hconst
    have hnorm : ‖w t‖ = 0 := by nlinarith [norm_nonneg (w t)]
    exact norm_eq_zero.1 hnorm
  exact sub_eq_zero.1 hwt

/-- The inverse of `e^{-itT}` is `e^{itT}`, i.e. its adjoint. -/
theorem unitaryU_neg_eq_star (hT : IsNonnegSelfAdjoint T)
    (hsv : ∀ w : F, ((0 : F), w) ∈ T → w = 0) (t : ℝ) :
    unitaryU hT hsv (-t) = star (unitaryU hT hsv t) := by
  have hone : unitaryU hT hsv (-t) * unitaryU hT hsv t = 1 := by
    rw [← unitaryU_add hT hsv]
    simp
  have hstar : star (unitaryU hT hsv t) * unitaryU hT hsv t = 1 :=
    (Unitary.mem_iff.mp (unitaryU_mem_unitary hT hsv t)).1
  have hsurj := unitaryU_surjective hT hsv t
  ext y
  obtain ⟨x, hx⟩ := hsurj y
  have h1 := congrArg (fun S : F →L[ℂ] F => S x) hone
  have h2 := congrArg (fun S : F →L[ℂ] F => S x) hstar
  simp only [ContinuousLinearMap.mul_apply, ContinuousLinearMap.one_apply] at h1 h2
  rw [← hx, h1, h2]

end BookProof.NonnegUnitaryGroup