The generator domain of the phase group is the multiplication domain

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #154 (out of #129).

PhaseGenerator.lean proved the forward half: if κ·f ∈ L² then the orbit t ↦ e^{−itκ} f is differentiable with derivative −i κ f (hasDerivAt_phaseGroup_apply), and the phase group preserves that domain (phaseGroup_mem_mulDomain). This file proves the converse: if the orbit has a right derivative at 0 in L² — HasGeneratorAt (phaseGroup hκ) f w — then κ·f ∈ L². The generator domain of the phase group is the multiplication domain.

• ★★ mem_mulDomain_of_hasGeneratorAt — the Fatou argument. Along hₙ = 1/(n+1) the quotients qₙ = hₙ⁻¹(e^{−ihₙκ} − 1) f converge to w in L², so ‖qₙ‖² → ‖w‖²; pointwise their squared moduli converge to |κ f|² (tendsto_phaseDefect); Fatou's lemma (lintegral_liminf_le') gives ∫ |κ f|² ≤ liminf ∫ |qₙ|² = ‖w‖² < ∞.
• ★ hasGeneratorAt_phaseGroup_iff: the two readings of the domain agree, with the generator value −i κ f (L2.mulOp), uniqueness of the right derivative identifying w.
• The free Hamiltonian: ★★ mem_freePositionOp_domain_of_hasGeneratorAt carries the statement across the Fourier transform — a vector whose free orbit has a right derivative at 0 lies in freePositionOp.domain.
• ★★★ schrodinger_mem_freePositionOp_domain: the interacting orbit stays in dom H₀, now in the operator sense; and ★★★ hasDerivAt_schrodinger_orbit: i ∂ₜ U(t)ψ = (H₀ + V)(U(t)ψ) with H₀ the self-adjoint operator freePositionOp acting on the orbit point. This closes the gap #129 left: the mild solution is classical in the operator-theoretic sense.

Honest scope

• The potential remains the bounded multiplier potential VL; the identification with schrodingerOp's mulCLM for a real V is a coeFn statement not made here.
• One dimension and κ = freeSymbol for the Schrödinger part, as throughout; the Fatou lemma is for any measurable κ on any E.

References: Reed–Simon I §VIII.4 (the generator of a multiplication group); PhaseGenerator.lean (phaseDefect, tendsto_phaseDefect, coeFn_slope_phaseGroup, norm_sq_eq_integral), PerturbedGenerator.lean (HasGeneratorAt), SchrodingerGenerator.lean (hasGeneratorAt_freeGroup_schrodinger, schrodinger_classical); Mathlib MeasureTheory.lintegral_liminf_le'; specs/BACKLOG.md #154, #129.

The quotients, pointwise

theorem SchrodingerGroup.coeFn_quotient_phaseGroup {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {κ : E → ℝ} (hκ : Measurable κ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (h : ℝ) : ↑↑(h⁻¹ • ((phaseGroup hκ h) f - f)) =ᵐ[MeasureTheory.volume] fun (x : E) => ↑↑f x * h⁻¹ • (phaseFun κ h x - 1)

The right quotient of the phase group at 0, pointwise: f · h⁻¹(e^{−ihκ} − 1).

★★ The Fatou argument

theorem SchrodingerGroup.mem_mulDomain_of_hasGeneratorAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {κ : E → ℝ} (hκ : Measurable κ) (f w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hw : HasGeneratorAt (phaseGroup hκ) f w) : f ∈ (MeasureTheory.L2.mulOp κ).domain

★★ A vector whose phase-group orbit has a right derivative at 0 lies in the multiplication domain: κ·f ∈ L². Fatou along hₙ = 1/(n+1).

theorem SchrodingerGroup.hasGeneratorAt_phaseGroup_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {κ : E → ℝ} (hκ : Measurable κ) (f w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : HasGeneratorAt (phaseGroup hκ) f w ↔ ∃ (hf : f ∈ (MeasureTheory.L2.mulOp κ).domain), w = -Complex.I • ↑(MeasureTheory.L2.mulOp κ) ⟨f, hf⟩

★ The two readings of the domain agree. A vector is in the generator domain of the phase group with value w iff it is in the multiplication domain and w = −i κ f.

The free Hamiltonian in position space

theorem SchrodingerGroup.hasGeneratorAt_phaseGroup_fourierL2 (χ w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hw : HasGeneratorAt (fun (t : ℝ) => if 0 ≤ t then fourierGroup ⋯ t else 1) χ w) : HasGeneratorAt (phaseGroup ⋯) (fourierL2 χ) (fourierL2 w)

The free generator statement transports across the Fourier transform to the phase group.

theorem SchrodingerGroup.mem_freePositionOp_domain_of_hasGeneratorAt (χ w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hw : HasGeneratorAt (fun (t : ℝ) => if 0 ≤ t then fourierGroup ⋯ t else 1) χ w) : χ ∈ freePositionOp.domain

★★ A vector whose free orbit has a right derivative at 0 lies in dom H₀.

theorem SchrodingerGroup.schrodinger_mem_freePositionOp_domain (VL : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)) (f : ↥freeSymbolOp.domain) (h : fourierL2.symm ↑f ∈ freePositionOp.domain) {t : ℝ} (ht : 0 ≤ t) : (schrodinger ⋯ VL t) (fourierL2.symm ↑f) ∈ freePositionOp.domain

★★★ The interacting orbit stays in dom H₀, in the operator sense.

theorem SchrodingerGroup.hasGeneratorAt_freeGroup_of_mem (χ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hχ : χ ∈ freePositionOp.domain) : HasGeneratorAt (fun (t : ℝ) => if 0 ≤ t then fourierGroup ⋯ t else 1) χ (-Complex.I • ↑freePositionOp ⟨χ, hχ⟩)

The free generator value at a point of dom H₀ is −i H₀ of it.

theorem SchrodingerGroup.hasDerivAt_schrodinger_orbit (VL : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)) (f : ↥freeSymbolOp.domain) (h : fourierL2.symm ↑f ∈ freePositionOp.domain) {t : ℝ} (ht : 0 < t) : HasDerivAt (fun (s : ℝ) => (schrodinger ⋯ VL s) (fourierL2.symm ↑f)) (-Complex.I • ↑(freePositionOp.addCLM (HeatSemigroup.potential VL)) ⟨(schrodinger ⋯ VL t) (fourierL2.symm ↑f), ⋯⟩) t

★★★ The interacting Schrödinger equation with H₀ acting on the orbit: d/dt U(t)ψ = −i (H₀ + V)(U(t)ψ) at every t > 0, where H₀ = freePositionOp is applied to the orbit point, which lies in its domain. The mild solution is classical in the operator sense.