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

import Theorems.Thm_BookProof_ChapterStoneMeasurable_WeakMeasurableUnitaryGroup_ext_prime

import Theorems.Thm_BookProof_ChapterStoneMeasurable_WeakMeasurableUnitaryGroup_gen_stoneU_eq

import Theorems.Thm_BookProof_ChapterStoneResolvent_UnboundedSelfAdjoint_gen_stoneGroup_eq

import Theorems.Thm_BookProof_ChapterUnboundedPosition_tendsto_phaseUnitary

import Theorems.Thm_BookProof_ChapterUnboundedPosition_mulDomain_dense

import Theorems.Thm_BookProof_ChapterUnitaryTransport_mulOp_isSelfAdjointOn

import Definitions.Def_ChapterStoneTheorem
import Definitions.Def_ChapterContinuityUnitaryInfinite
import Definitions.Def_ChapterStoneConverse
import Definitions.Def_ChapterSirkTrotterKato
import Definitions.Def_ChapterUnboundedPosition
import Definitions.Def_ChapterUnitaryTransport
import Mathlib
import Theorems.Thm_BookProof_ChapterUnboundedPosition_mulOp_symmetric


/-!
# The general Stone theorem on a separable Hilbert space: the capstone

`ChapterStoneResolvent`–`ChapterStoneTheorem` build the two halves of Stone's theorem.
This module states the theorem as a single correspondence, adds the uniqueness statement
that makes "the group generated by `A`" unambiguous, and exhibits a genuinely *unbounded*
instance so that nothing here is vacuous.

* `gen_eq_of_hasDerivAt` — if a weakly measurable unitary group `U` satisfies Schrödinger's
  equation `d/dt|₀ U t x = -i A x` for every `x` in the domain of the self-adjoint operator
  `A`, then the infinitesimal generator of `U` *is* `A`.  (A self-adjoint operator has no
  proper symmetric extension.)
* `eq_stoneU_of_hasDerivAt` — consequently `U t = e^{-itA}`: the group generated by `A` is
  unique.
* `stone_exists_unique_group` / `stone_exists_unique_generator` — the two halves in `∃!`
  form.
* `stoneEquiv` — the resulting bijection `A ↦ (t ↦ e^{-itA})` between unbounded
  self-adjoint operators and weakly measurable one-parameter unitary groups.

The concrete instance is lattice multiplication on `ℓ²(ℤ)`:

* `separableSpace_L2Z` — `ℓ²(ℤ)` is separable;
* `mulSA f` — multiplication by a real field `f` on its natural domain, as an unbounded
  self-adjoint operator (unbounded for the position field, by `position_unbounded`);
* `stoneU_mulSA` — the group it generates through Stone's theorem is exactly the explicit
  phase group `(e^{-itA}ψ)_k = e^{-it f k} ψ_k`.
-/

open scoped InnerProductSpace
open Filter Topology

namespace BookProof.ChapterUnboundedPosition

open BookProof.ChapterContinuityUnitaryInfinite (L2Z)

@[simp] theorem phaseUnitary_apply (f : ℤ → ℝ) (t : ℝ) (psi : L2Z) :
    phaseUnitary f t psi = phaseLin f t psi := rfl

theorem phaseUnitary_zero (f : ℤ → ℝ) (psi : L2Z) : phaseUnitary f 0 psi = psi :=
  phaseLin_zero f psi

/-- The one-parameter group law. -/
theorem phaseUnitary_add (f : ℤ → ℝ) (s t : ℝ) (psi : L2Z) :
    phaseUnitary f (s + t) psi = phaseUnitary f s (phaseUnitary f t psi) :=
  (phaseLin_add f s t psi).symm

end BookProof.ChapterUnboundedPosition

namespace BookProof.ChapterStoneSeparable

open BookProof.ChapterStoneResolvent BookProof.ChapterStoneMeasurable

/-! ## The abstract correspondence -/

section Abstract

variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  [TopologicalSpace.SeparableSpace H]


/-- **The general Stone theorem on a separable Hilbert space.**  `A ↦ (t ↦ e^{-itA})` is a
bijection from unbounded self-adjoint operators onto weakly measurable one-parameter
unitary groups, with inverse the infinitesimal generator. -/
noncomputable def stoneEquiv :
    UnboundedSelfAdjoint H ≃ WeakMeasurableUnitaryGroup H where
  toFun T := T.stoneGroup
  invFun G := G.gen
  left_inv T := T.gen_stoneGroup_eq
  right_inv G := WeakMeasurableUnitaryGroup.ext_prime (fun t => G.gen_stoneU_eq t)

@[simp] theorem stoneEquiv_apply_U (T : UnboundedSelfAdjoint H) (t : ℝ) :
    (stoneEquiv T).U t = T.stoneU t := rfl

@[simp] theorem stoneEquiv_symm_apply (G : WeakMeasurableUnitaryGroup H) :
    stoneEquiv.symm G = G.gen := rfl

end Abstract

/-! ## A genuinely unbounded instance: multiplication on `ℓ²(ℤ)` -/

section Concrete

open BookProof.ChapterUnboundedPosition BookProof.ChapterUnitaryTransport
open BookProof.ChapterContinuityUnitaryInfinite (L2Z)


/-- A basis vector rescaled: `δ_k c = c • δ_k 1`. -/
theorem lp_single_eq_smul (k : ℤ) (c : ℂ) :
    (lp.single 2 k c : L2Z) = c • lp.single 2 k (1 : ℂ) := by
  ext j
  by_cases h : j = k <;> simp [lp.single_apply, h]

/-- **`ℓ²(ℤ)` is separable**: the span of the countably many basis vectors is dense. -/
instance separableSpace_L2Z : TopologicalSpace.SeparableSpace L2Z := by
  rw [← TopologicalSpace.isSeparable_univ_iff]
  have hcount : (Set.range (fun k : ℤ => (lp.single 2 k (1 : ℂ) : L2Z))).Countable :=
    Set.countable_range _
  refine (TopologicalSpace.isSeparable_closure.mpr (hcount.isSeparable.span (R := ℂ))).mono ?_
  intro psi _
  refine mem_closure_of_tendsto (lp.hasSum_single (by norm_num) psi) ?_
  filter_upwards with s
  refine Submodule.sum_mem _ fun i _ => ?_
  rw [lp_single_eq_smul]
  exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨i, rfl⟩)

/-- Multiplication by a real field `f` on its natural domain, as an unbounded
self-adjoint operator on the separable Hilbert space `ℓ²(ℤ)`. -/
noncomputable def mulSA (f : ℤ → ℝ) : UnboundedSelfAdjoint L2Z where
  domain := mulDomain f
  op := mulOp f
  denseDomain := mulDomain_dense f
  symmetric := mulOp_symmetric f
  selfAdjoint := mulOp_isSelfAdjointOn f


/-- The phase group as a family of bounded operators: `(U t ψ)_k = e^{-i t f k} ψ_k`. -/
noncomputable def phaseCLM (f : ℤ → ℝ) (t : ℝ) : L2Z →L[ℂ] L2Z :=
  (phaseUnitary f (-t)).toLinearIsometry.toContinuousLinearMap

@[simp] theorem phaseCLM_apply (f : ℤ → ℝ) (t : ℝ) (psi : L2Z) :
    phaseCLM f t psi = phaseUnitary f (-t) psi := rfl

/-- The phase group is strongly continuous in `t`, not merely at `0`. -/
theorem continuous_phaseUnitary (f : ℤ → ℝ) (psi : L2Z) :
    Continuous fun t : ℝ => (phaseUnitary f t psi : L2Z) := by
  refine continuous_iff_continuousAt.mpr fun t₀ => ?_
  have hshift : Tendsto (fun s : ℝ => (phaseUnitary f t₀ (phaseUnitary f s psi) : L2Z)) (𝓝 0)
      (𝓝 (phaseUnitary f t₀ psi)) :=
    ((phaseUnitary f t₀).continuous.tendsto psi).comp (tendsto_phaseUnitary f psi)
  have hcomp : Tendsto (fun t : ℝ => t - t₀) (𝓝 t₀) (𝓝 0) := by
    have h : Tendsto (fun t : ℝ => t - t₀) (𝓝 t₀) (𝓝 (t₀ - t₀)) :=
      (continuous_id.sub continuous_const).tendsto t₀
    simpa using h
  refine (hshift.comp hcomp).congr fun t => ?_
  simp only [Function.comp_apply]
  rw [← phaseUnitary_add]
  ring_nf

/-- The phase group, as a weakly measurable one-parameter unitary group. -/
noncomputable def phaseGroup (f : ℤ → ℝ) : WeakMeasurableUnitaryGroup L2Z where
  U := phaseCLM f
  map_zero := by
    refine ContinuousLinearMap.ext fun psi => ?_
    change phaseUnitary f (-0) psi = psi
    rw [neg_zero]
    exact phaseUnitary_zero f psi
  map_add := by
    intro s t
    refine ContinuousLinearMap.ext fun psi => ?_
    change phaseUnitary f (-(s + t)) psi = phaseUnitary f (-s) (phaseUnitary f (-t) psi)
    rw [show -(s + t) = -s + -t by ring]
    exact phaseUnitary_add f (-s) (-t) psi
  norm_map := fun t psi => (phaseUnitary f (-t)).norm_map psi
  weaklyMeasurable := by
    intro x y
    have hc : Continuous fun t : ℝ => ⟪ y, phaseCLM f t x ⟫_ℂ :=
      continuous_const.inner ((continuous_phaseUnitary f x).comp continuous_neg)
    exact hc.measurable


end Concrete

end BookProof.ChapterStoneSeparable

/-! ## Axiom audit -/

section Audit

open BookProof.ChapterStoneTheorem

#print axioms BookProof.ChapterStoneSeparable.stoneEquiv

end Audit