SchrodingerFourier.lean

1 import Mathlib.LinearAlgebra.Pi
2 import Mathlib.Basic.Complex.Basic
3 import Mathlib.Algebra.BigOperators.Pi
4 import Mathlib.Tactic.FieldSimp
5 import Mathlib.Tactic.Ring
6 
7 /-! Exact coordinate projections from a separating family of diagonal operators.
8 The finite elimination argument supplies the projector; orthogonality is not a hypothesis. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.SchrodingerFourier
12 
13 variable {I X : Type*}
14 
15 /-- Remove finitely many coordinates while preserving the distinguished coordinate. -/
16 theorem finite_elimination (χ : I → X → ℂ)
17     (hsep : ∀ u v : X, u ≠ v → ∃ i : I, χ i u ≠ χ i v)
18     (S : Submodule ℂ (X → ℂ))
19     (hS : ∀ i f, f ∈ S → (fun x => χ i x * f x) ∈ S)
20     (u : X) (f : X → ℂ) (hf : f ∈ S) (t : Finset X) :
21     ∃ g : X → ℂ, g ∈ S ∧ g u = f u ∧ ∀ v ∈ t, v ≠ u → g v = 0 := by
22   classical
23   induction t using Finset.induction_on with
24   | empty => exact ⟨f, hf, rfl, by simp⟩
25   | @insert v t _ ih =>
26     obtain ⟨g, hg, hgu, hgt⟩ := ih
27     by_cases hv : v = u
28     · refine ⟨g, hg, hgu, ?_⟩
29       intro w hw hwu
30       rcases Finset.mem_insert.mp hw with rfl | hw
31       · exact (hwu hv).elim
32       · exact hgt w hw hwu
33     · obtain ⟨i, hi⟩ := hsep u v (Ne.symm hv)
34       let g' : X → ℂ := (χ i u - χ i v)⁻¹ •
35         ((fun x => χ i x * g x) - χ i v • g)
36       have hg' : g' ∈ S :=
37         S.smul_mem _ (S.sub_mem (hS i g hg) (S.smul_mem _ hg))
38       have hgu' : g' u = f u := by
39         dsimp [g']
40         rw [← sub_mul, inv_mul_cancel_left₀ (sub_ne_zero.mpr hi), hgu]
41       refine ⟨g', hg', hgu', ?_⟩
42       intro w hw hwu
43       rcases Finset.mem_insert.mp hw with rfl | hw
44       · simp [g']
45       · simp [g', hgt w hw hwu]
46 
47 /-- Stability under a separating diagonal family implies stability under every
48 coordinate projector, with no spectral theorem assumed. -/
49 theorem coordinate_projection_mem [Fintype X] [DecidableEq X] (χ : I → X → ℂ)
50     (hsep : ∀ u v : X, u ≠ v → ∃ i : I, χ i u ≠ χ i v)
51     (S : Submodule ℂ (X → ℂ))
52     (hS : ∀ i f, f ∈ S → (fun x => χ i x * f x) ∈ S)
53     (u : X) (f : X → ℂ) (hf : f ∈ S) :
54     (fun x => if x = u then f u else 0) ∈ S := by
55   classical
56   obtain ⟨g, hg, hgu, hgt⟩ := finite_elimination χ hsep S hS u f hf Finset.univ
57   have heq : g = (fun x => if x = u then f u else 0) := by
58     funext x
59     by_cases hx : x = u
60     · subst x; simpa using hgu
61     · simp [hx, hgt x (Finset.mem_univ x) hx]
62   rwa [← heq]
63 
64 /-- A nonzero distinguished coordinate gives its unit coordinate vector. -/
65 theorem coordinate_unit_mem [Fintype X] [DecidableEq X] (χ : I → X → ℂ)
66     (hsep : ∀ u v : X, u ≠ v → ∃ i : I, χ i u ≠ χ i v)
67     (S : Submodule ℂ (X → ℂ))
68     (hS : ∀ i f, f ∈ S → (fun x => χ i x * f x) ∈ S)
69     (u : X) (f : X → ℂ) (hf : f ∈ S) (hfu : f u ≠ 0) :
70     (fun x => if x = u then (1 : ℂ) else 0) ∈ S := by
71   classical
72   have h := S.smul_mem (f u)⁻¹ (coordinate_projection_mem χ hsep S hS u f hf)
73   convert h using 1
74   funext x
75   by_cases hx : x = u <;> simp [hx, hfu]
76 
77 end PaperXI.SchrodingerFourier

Back to source controls