Differentiation in Fourier coordinates, and the twisted Laplacian on L²(S¹)

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #93(b)(c), closing #93.

AharonovBohmCircle.lean states the Aharonov–Bohm eigenvalue equation −(∂ − iΦ)²ψₙ = (n − Φ)²ψₙ pointwise on the Fourier modes, and says honestly that "spectrum" there means the level set of those modes. DiagonalOperator.lean supplies the missing operator theory in general: the diagonal operator of a real weight family on a Hilbert basis is self-adjoint with spectrum the closure of the weights. This file is the bridge between them, and it needs one identity that the pin has only in boundary-term form.

Differentiation in Fourier coordinates

• ★★ fourierCoeffOn_deriv — for a T-periodic function, cₙ(f') = (2πin/T) cₙ(f). The boundary term of Mathlib's fourierCoeffOn_of_hasDerivAt vanishes by periodicity, and the n = 0 case is the fundamental theorem of calculus; ★★ fourierCoeffOn_deriv_two_pi is the T = 2π form, where the factor is exactly in;
• fourierCoeffOn_add, fourierCoeffOn_neg — the linearity the pin leaves out;
• ★★★ fourierCoeffOn_twistedLap — −(∂ − iΦ)² is multiplication by (n − Φ)² in Fourier coordinates. This is the eigenvalue equation in the form spectral theory needs: not "the modes are eigenvectors" but "the operator is diagonal in the modes".

The operator, its spectrum, and the flux

• twistedOp Φ — the twisted Laplacian on L²(ℝ/2πℤ) as fourierBasis.diagOp (circleEigval Φ). Its domain is H² of the circle: the vectors whose weighted Fourier coefficients are still square-summable, which is what diagDomain is;
• ★★★ isSelfAdjoint_twistedOp and ★★★ spectrum_twistedOp — self-adjoint, with spectrum the closure of the level set, inherited from the generic brick;
• toL2 and ★ fourierCoeff_toL2 — a continuous periodic function on the line as an element of L²(ℝ/2πℤ), with the coefficients it came with;
• ★★★ twistedOp_apply_of_fourierCoeff and ★★★ twistedOp_toL2 — the operator acts on every C² periodic function exactly as −(∂ − iΦ)² does, which is what makes the two theorems above statements about the differential operator and not only about a multiplier;
• ★★★ exists_eq_of_spectrum_twistedOp_eq — the flux is determined by the spectrum, modulo a whole quantum and up to sign. AharonovBohmCircle.exists_eq_of_range_circleEigval_eq said this of a chosen level set; this says it of the spectrum of a self-adjoint operator on L²(S¹). The extraction is isLeast_norm_image_spectrum: the ground level survives the closure because the bound that produced it is a closed condition.

Honest scope

⚠️ The identification is on C² periodic functions, not on the whole domain. twistedOp_toL2 covers every twice-differentiable periodic function with continuous second derivative — a dense set containing all the modes and all trigonometric polynomials — and twistedOp_apply_of_fourierCoeff covers any pair of L² functions with the right coefficients. What is not proved is that every element of the domain is twice differentiable in any classical sense: that is a Sobolev embedding (H²(S¹) ↪ C¹), which the pin does not have and which nothing here needs.

⚠️ No functional calculus and no eigenfunction expansion theorem. The spectrum is computed as a set; hasSum_fourier_series_L2 is Mathlib's, and is not re-proved or used.

⚠️ The flux quantum here is 1 and the spatial period 2π, as in AharonovBohmCircle.lean; the lattice ring of AharonovBohmRing.lean is an analogue, not an instance, and nothing here changes that.

References: the identity cₙ(f') = in·cₙ(f) is the classical one behind the H^k scale — e.g. Katznelson, An Introduction to Harmonic Analysis I.§4 — and the multiplication-operator model of a self-adjoint operator with prescribed spectrum is Reed–Simon I, Theorem VIII.4; Y. Aharonov, D. Bohm, Phys. Rev. 115 (1959) 485; specs/BACKLOG.md #90, #93.

Preliminaries

theorem CircleFourier.continuous_fourier_coe (T : ℝ) (n : ℤ) : Continuous fun (x : ℝ) => (fourier n) ↑x

The character, read on the line, is continuous.

theorem CircleFourier.intervalIntegrable_fourier_smul {a b : ℝ} (n : ℤ) {f : ℝ → ℂ} (hf : Continuous f) : IntervalIntegrable (fun (x : ℝ) => (fourier (-n)) ↑x • f x) MeasureTheory.volume a b

theorem CircleFourier.fourierCoeffOn_add {a b : ℝ} (hab : a < b) {f g : ℝ → ℂ} (hf : Continuous f) (hg : Continuous g) (n : ℤ) : fourierCoeffOn hab (fun (x : ℝ) => f x + g x) n = fourierCoeffOn hab f n + fourierCoeffOn hab g n

fourierCoeffOn is additive.

theorem CircleFourier.fourierCoeffOn_neg {a b : ℝ} (hab : a < b) (f : ℝ → ℂ) (n : ℤ) : fourierCoeffOn hab (fun (x : ℝ) => -f x) n = -fourierCoeffOn hab f n

fourierCoeffOn commutes with negation.

The Fourier coefficients of a derivative

theorem CircleFourier.fourierCoeffOn_deriv {a T : ℝ} (hT : 0 < T) {f f' : ℝ → ℂ} (hper : Function.Periodic f T) (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) (hf' : Continuous f') (n : ℤ) : fourierCoeffOn ⋯ f' n = 2 * ↑Real.pi * Complex.I * ↑n / ↑T * fourierCoeffOn ⋯ f n

★★ Differentiation multiplies the n-th Fourier coefficient by 2πin/T. The boundary term of the integration by parts vanishes because the function is periodic; this is the identity the H^k scale of spaces is built on, and the pin has it only in the boundary-term form fourierCoeffOn_of_hasDerivAt.

theorem CircleFourier.two_pi_lt (a : ℝ) : a < a + 2 * Real.pi

The interval of one period.

theorem CircleFourier.fourierCoeffOn_deriv_two_pi {a : ℝ} {f f' : ℝ → ℂ} (hper : Function.Periodic f (2 * Real.pi)) (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) (hf' : Continuous f') (n : ℤ) : fourierCoeffOn ⋯ f' n = Complex.I * ↑n * fourierCoeffOn ⋯ f n

★★ The same at the period 2π, where the factor is exactly in.

The twisted Laplacian in Fourier coordinates

def CircleFourier.twistedLap (Φ : ℝ) (f f' f'' : ℝ → ℂ) : ℝ → ℂ

−(∂ − iΦ)²f = −f'' + 2iΦ f' + Φ² f, written out.

Equations

• CircleFourier.twistedLap Φ f f' f'' x = -f'' x + 2 * Complex.I * ↑Φ * f' x + ↑Φ ^ 2 * f x

theorem CircleFourier.twistedLap_apply (Φ : ℝ) (f f' f'' : ℝ → ℂ) (x : ℝ) : twistedLap Φ f f' f'' x = -f'' x + 2 * Complex.I * ↑Φ * f' x + ↑Φ ^ 2 * f x

theorem CircleFourier.fourierCoeffOn_twistedLap {a : ℝ} (Φ : ℝ) {f f' f'' : ℝ → ℂ} (hper : Function.Periodic f (2 * Real.pi)) (hper' : Function.Periodic f' (2 * Real.pi)) (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) (hf' : ∀ (x : ℝ), HasDerivAt f' (f'' x) x) (hf'' : Continuous f'') (n : ℤ) : fourierCoeffOn ⋯ (twistedLap Φ f f' f'') n = ↑(QuantumInfo.AharonovBohmCircle.circleEigval Φ n) * fourierCoeffOn ⋯ f n

★★★ The twisted Laplacian is multiplication by (n − Φ)² in Fourier coordinates. This is the content of the eigenvalue equation of AharonovBohmCircle.lean in the form spectral theory needs: not "the modes are eigenvectors" but "the operator is diagonal in the modes".

The twisted Laplacian as a self-adjoint operator on L²(ℝ/2πℤ)

theorem CircleFourier.instTwoPiPos : Fact (0 < 2 * Real.pi)

noncomputable def CircleFourier.twistedOp (Φ : ℝ) : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle) →ₗ.[ℂ] ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)

The twisted Laplacian −(∂ − iΦ)² on L²(ℝ/2πℤ): the diagonal operator of the levels (n − Φ)² in the Fourier basis, on the domain where those weighted coefficients are still square-summable. That domain is H² of the circle, by definition rather than by construction.

Equations

• CircleFourier.twistedOp Φ = fourierBasis.diagOp (QuantumInfo.AharonovBohmCircle.circleEigval Φ)

theorem CircleFourier.twistedOp_eq (Φ : ℝ) : twistedOp Φ = fourierBasis.diagOp (QuantumInfo.AharonovBohmCircle.circleEigval Φ)

theorem CircleFourier.isSelfAdjoint_twistedOp (Φ : ℝ) : IsSelfAdjoint (twistedOp Φ)

★★★ The twisted Laplacian is self-adjoint on that domain.

theorem CircleFourier.spectrum_twistedOp (Φ : ℝ) : (twistedOp Φ).spectrum = closure (Set.range fun (n : ℤ) => ↑(QuantumInfo.AharonovBohmCircle.circleEigval Φ n))

★★★ Its spectrum is the closure of the level set — the honest spectrum of a self-adjoint operator, not the set of eigenvalues of a chosen family.

theorem CircleFourier.twistedOp_apply_fourierBasis (Φ : ℝ) (n : ℤ) : ↑(twistedOp Φ) ⟨fourierBasis n, ⋯⟩ = ↑(QuantumInfo.AharonovBohmCircle.circleEigval Φ n) • fourierBasis n

★ Each Fourier mode is an eigenvector with eigenvalue (n − Φ)².

theorem CircleFourier.twistedOp_apply_of_fourierCoeff (Φ : ℝ) (F G : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) (h : ∀ (n : ℤ), fourierCoeff (↑↑G) n = ↑(QuantumInfo.AharonovBohmCircle.circleEigval Φ n) * fourierCoeff (↑↑F) n) : ∃ (hF : F ∈ (twistedOp Φ).domain), ↑(twistedOp Φ) ⟨F, hF⟩ = G

★★★ The operator is the twisted Laplacian. Whenever two L² functions have the Fourier coefficients that −(∂ − iΦ)² relates — which is what fourierCoeffOn_twistedLap says of a C² periodic function and its twisted Laplacian — the first is in the domain and the second is its image. This is the step that makes spectrum_twistedOp a statement about the differential operator.

From a C² periodic function on the line to the operator

theorem CircleFourier.continuous_of_hasDerivAt {f f' : ℝ → ℂ} (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) : Continuous f

theorem CircleFourier.periodic_deriv {T : ℝ} {f f' : ℝ → ℂ} (hp : Function.Periodic f T) (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) : Function.Periodic f' T

The derivative of a periodic function is periodic.

theorem CircleFourier.continuous_twistedLap (Φ : ℝ) {f f' f'' : ℝ → ℂ} (hfc : Continuous f) (hf'c : Continuous f') (hf''c : Continuous f'') : Continuous (twistedLap Φ f f' f'')

theorem CircleFourier.periodic_twistedLap {T : ℝ} (Φ : ℝ) {f f' f'' : ℝ → ℂ} (hp : Function.Periodic f T) (hp' : Function.Periodic f' T) (hp'' : Function.Periodic f'' T) : Function.Periodic (twistedLap Φ f f' f'') T

noncomputable def CircleFourier.toL2 (f : ℝ → ℂ) (hc : Continuous f) (hp : Function.Periodic f (2 * Real.pi)) : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)

A continuous 2π-periodic function on the line, as an element of L²(ℝ/2πℤ).

Equations

• CircleFourier.toL2 f hc hp = (ContinuousMap.toLp 2 AddCircle.haarAddCircle ℂ) { toFun := AddCircle.liftIoc (2 * Real.pi) 0 f, continuous_toFun := ⋯ }

theorem CircleFourier.fourierCoeff_toL2 (f : ℝ → ℂ) (hc : Continuous f) (hp : Function.Periodic f (2 * Real.pi)) (n : ℤ) : fourierCoeff (↑↑(toL2 f hc hp)) n = fourierCoeffOn ⋯ f n

★ Its Fourier coefficients are the interval coefficients of the function it came from.

theorem CircleFourier.twistedOp_toL2 (Φ : ℝ) {f f' f'' : ℝ → ℂ} (hp : Function.Periodic f (2 * Real.pi)) (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) (hf' : ∀ (x : ℝ), HasDerivAt f' (f'' x) x) (hf'' : Continuous f'') : ∃ (h : toL2 f ⋯ hp ∈ (twistedOp Φ).domain), ↑(twistedOp Φ) ⟨toL2 f ⋯ hp, h⟩ = toL2 (twistedLap Φ f f' f'') ⋯ ⋯

★★★ The operator applied to a C² periodic function is its twisted Laplacian. This closes the loop: spectrum_twistedOp and isSelfAdjoint_twistedOp are statements about an operator that acts on every C² periodic function exactly as −(∂ − iΦ)² does.

The flux is determined by the spectrum

theorem CircleFourier.isLeast_norm_image_spectrum (Φ : ℝ) : IsLeast ((fun (z : ℂ) => ‖z‖) '' (twistedOp Φ).spectrum) ((Φ - ↑(round Φ)) ^ 2)

The smallest modulus in the spectrum is the squared distance from the flux to the nearest whole quantum: the ground level survives the closure, because the bound that produced it is closed.

theorem CircleFourier.exists_eq_of_spectrum_twistedOp_eq {Φ Φ' : ℝ} (h : (twistedOp Φ).spectrum = (twistedOp Φ').spectrum) : ∃ (k : ℤ), Φ' = Φ + ↑k ∨ Φ' = -Φ + ↑k

★★★ The flux is determined by the spectrum of the operator, modulo a whole quantum and up to sign. This is AharonovBohmCircle.exists_eq_of_range_circleEigval_eq upgraded from a statement about a chosen level set to a statement about the spectrum of a self-adjoint operator on L²(S¹).