wip

Author: b-mehta

Mathlib/Algebra/Module/LinearMap/End.lean

@@ -149,6 +149,7 @@ theorem id_pow (n : ℕ) : (id : End R M) ^ n = .id :=
 variable {f' : End R M}
 
 theorem iterate_succ (n : ℕ) : f' ^ (n + 1) = .comp (f' ^ n) f' := by rw [pow_succ, mul_eq_comp]
+theorem iterate_succ' (n : ℕ) : f' ^ (n + 1) = .comp f' (f' ^ n) := by rw [pow_succ', mul_eq_comp]
 
 theorem iterate_surjective (h : Surjective f') : ∀ n : ℕ, Surjective (f' ^ n)
   | 0 => surjective_id

Mathlib/Algebra/Module/Submodule/Range.lean

@@ -145,13 +145,11 @@ end
 @[simps]
 def iterateRange (f : M →ₗ[R] M) : ℕ →o (Submodule R M)ᵒᵈ where
   toFun n := LinearMap.range (f ^ n)
-  monotone' n m w x h := by
-    obtain ⟨c, rfl⟩ := Nat.exists_eq_add_of_le w
-    rw [LinearMap.mem_range] at h
-    obtain ⟨m, rfl⟩ := h
-    rw [LinearMap.mem_range]
-    use (f ^ c) m
-    rw [pow_add, Module.End.mul_apply]
+  monotone' := monotone_nat_of_le_succ fun | n, _, ⟨x, rfl⟩ => ⟨f x, rfl⟩
+
+lemma iterateRange_succ {f : M →ₗ[R] M} {n : ℕ} :
+    iterateRange f (n + 1) = (iterateRange f n).map f := by
+  simp only [iterateRange_coe, range_eq_map, ← map_comp, Module.End.iterate_succ']
 
 /-- Restrict the codomain of a linear map `f` to `f.range`.
 

Mathlib/Analysis/SpecialFunctions/Log/Compact.lean

@@ -1,29 +1,64 @@
-import Mathlib
+/-
+Copyright (c) 2026 Bhavik Mehta. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta
+-/
+import Mathlib.Algebra.Order.Ring.Star
+import Mathlib.Analysis.Normed.Module.RCLike.Basic
+import Mathlib.Analysis.Normed.Module.RieszLemma
+import Mathlib.Analysis.Normed.Operator.Banach
+import Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
+import Mathlib.Analysis.Normed.Operator.Compact
+import Mathlib.LinearAlgebra.Eigenspace.Basic
+
+/-!
+# Spectral theory of compact operators
+
+This file develops the spectral theory of compact operators on Banach spaces.
+The main result is the Fredholm alternative for compact operators.
+
+## Main results
+
+* `antilipschitz_of_not_hasEigenvalue`: if `T` is a compact operator and `μ ≠ 0` is not an
+  eigenvalue, then `T - μI` is antilipschitz.
+* `fredholm_alternative`: the Fredholm alternative for compact operators.
+-/
 
 -- let X be a Banach space
-variable {X : Type*} [NormedAddCommGroup X] [NormedSpace ℂ X]
+variable {𝕜 X : Type*} [RCLike 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X]
 -- and T be a compact operator on it
-variable {T : X →L[ℂ] X} (hT : IsCompactOperator T)
+variable {T : X →L[𝕜] X}
 
-open Module.End
+open Module End
+
+/-- If a continuous linear map `f` satisfies `‖x‖ = 1 → 1 ≤ K * ‖f x‖`, then `f` is
+antilipschitz with constant `K`. -/
+lemma ContinuousLinearMap.antilipschitz_of_bound_of_norm_one {X Y : Type*}
+    [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]
+    (f : X →L[𝕜] Y) {K : NNReal} (h : ∀ x, ‖x‖ = 1 → 1 ≤ K * ‖f x‖) :
+    AntilipschitzWith K f :=
+  ContinuousLinearMap.antilipschitz_of_bound _ fun x ↦ by
+    obtain rfl | hx := eq_or_ne x 0
+    · simp
+    simpa [norm_smul, field] using h ((‖x‖⁻¹ : 𝕜) • x) (norm_smul_inv_norm hx)
 
 open Filter Topology in
-theorem far_away {μ : ℂ} (hμ : μ ≠ 0) (hT : IsCompactOperator T)
-    (h : ¬ HasEigenvalue (T : X →ₗ[ℂ] X) μ) :
-    ∃ c > 0, ∀ x, c * ‖x‖ ≤ ‖(T - μ • 1) x‖ := by
-  -- By homogeneity, it suffices to establish the claim for unit vectors x.
+/-- If `T : X →L[𝕜] X` is a compact operator on a Banach space `X`, and `μ ≠ 0` is not an
+eigenvalue of `T`, then `T - μ • 1` is antilipschitz.
+
+This is a useful step in the proof of the Fredholm alternative. -/
+theorem antilipschitz_of_not_hasEigenvalue (hT : IsCompactOperator T)
+    {μ : 𝕜} (hμ : μ ≠ 0) (h : ¬ HasEigenvalue (T : End 𝕜 X) μ) :
+    ∃ K > 0, AntilipschitzWith K (T - μ • 1 : X →L[𝕜] X) := by
   suffices ∃ c > 0, ∀ x, ‖x‖ = 1 → c ≤ ‖(T - μ • 1) x‖ by
     obtain ⟨c, hc', hc⟩ := this
-    refine ⟨c, hc', fun x ↦ ?_⟩
-    obtain h | h := eq_or_ne x 0
-    · simp [h]
-    simpa [norm_smul, le_inv_mul_iff₀', norm_pos_iff, h] using hc _ (norm_smul_inv_norm (𝕜 := ℂ) h)
+    refine ⟨c.toNNReal⁻¹, by positivity, ?_⟩
+    apply ContinuousLinearMap.antilipschitz_of_bound_of_norm_one
+    simpa [NNReal.coe_inv, le_inv_mul_iff₀', hc'] using hc
   -- Suppose not, then we can find a sequence of unit vectors xₙ such that (T - μ • 1) xₙ → 0.
   by_contra!
   obtain ⟨φ, hφ_anti, hφ_pos, hφ⟩ := exists_seq_strictAnti_tendsto (0 : ℝ)
-  have : ∀ n, ∃ x, ‖x‖ = 1 ∧ ‖(T - μ • 1) x‖ < φ n := by
-    intro n
-    exact this (φ n) (hφ_pos n)
+  have (n : ℕ) : ∃ x, ‖x‖ = 1 ∧ ‖(T - μ • 1) x‖ < φ n := this (φ n) (hφ_pos n)
   choose x hx_norm hx_bound using this
   have hx_lim : Tendsto (fun n ↦ (T - μ • 1) (x n)) atTop (𝓝 0) := squeeze_zero_norm (by grind) hφ
   -- Define the sequence of vectors yₙ := T xₙ
@@ -39,14 +74,14 @@ theorem far_away {μ : ℂ} (hμ : μ ≠ 0) (hT : IsCompactOperator T)
   -- since T is, so we can extract a convergent subsequence, and say y_ (ψ n) → y.
   obtain ⟨K, hK, hK'⟩ := hT.image_closedBall_subset_compact 1
   obtain ⟨y, hyK, ψ, hψ, hψy⟩ := hK.tendsto_subseq (x := y_) (fun n ↦ hK' ⟨x n, by simp [*], rfl⟩)
-  -- However (T - μ) yₙ = T (T - μ • 1) xₙ → 0
+  -- However (T - μ • 1) yₙ = T ((T - μ • 1) xₙ) → 0
   have hy_lim : Tendsto (fun n ↦ (T - μ • 1) (y_ n)) atTop (nhds 0) := by
     have : Tendsto (fun n ↦ _) _ _ := T.continuous.continuousAt.tendsto.comp hx_lim
     simpa using this
-  -- so (T - μ) y = 0.
+  -- so (T - μ • 1) y = 0.
   have hy_eigen' : (T - μ • 1) y = 0 := by
     apply tendsto_nhds_unique _ (hy_lim.comp hψ.tendsto_atTop)
-    have : Continuous (T - μ • 1 : X →L[ℂ] X) := by fun_prop
+    have : Continuous (T - μ • 1 : X →L[𝕜] X) := by fun_prop
     exact this.continuousAt.tendsto.comp hψy
   -- Since yₙ are bounded away from 0, we must have y ≠ 0.
   have hy_ne : y ≠ 0 := by
@@ -56,24 +91,95 @@ theorem far_away {μ : ℂ} (hμ : μ ≠ 0) (hT : IsCompactOperator T)
     specialize hψy (‖μ‖ / 2) (by positivity)
     filter_upwards [hψ.tendsto_atTop.eventually hy_lower, hψy] using by grind
   -- So y is an eigenvector of T with eigenvalue μ,
-  have : HasEigenvector (T : X →ₗ[ℂ] X) μ y := by
-    rw [hasEigenvector_iff]
-    rw [mem_genEigenspace_one]
-    simpa [hy_ne, sub_eq_zero] using hy_eigen'
+  have : HasEigenvector (T : End 𝕜 X) μ y := by
+    simpa [hasEigenvector_iff, mem_genEigenspace_one, hy_ne, sub_eq_zero] using hy_eigen'
   -- which is a contradiction.
   exact h (hasEigenvalue_of_hasEigenvector this)
 
-theorem fredholm_alternative [CompleteSpace X] {μ : ℂ} (hμ : μ ≠ 0) :
-    HasEigenvalue (T : X →ₗ[ℂ] X) μ ∨ μ ∈ resolventSet ℂ T := by
+/-- A variation of Riesz's lemma where we get a vector `x₀` of norm exactly 1. -/
+theorem riesz_lemma_one
+    {𝕜 : Type*} [RCLike 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+    {F : Subspace 𝕜 E} (hFc : IsClosed (F : Set E)) (hF : ∃ (x : E), x ∉ F) {r : ℝ} (hr : r < 1) :
+    ∃ x₀ ∉ F, ‖x₀‖ = 1 ∧ ∀ y ∈ F, r ≤ ‖x₀ - y‖ := by
+  obtain ⟨x₀, hx₀, h⟩ := riesz_lemma hFc hF hr
+  have hx₀' : x₀ ≠ 0 := by rintro rfl; simp at hx₀
+  refine ⟨(‖x₀‖⁻¹ : 𝕜) • x₀, ?_, norm_smul_inv_norm hx₀', ?_⟩
+  · rwa [Submodule.smul_mem_iff]
+    simpa
+  intro y hy
+  have h₂ : ‖(‖x₀‖ : 𝕜)⁻¹ • (x₀ - (‖x₀‖ : 𝕜) • y)‖ = ‖x₀‖⁻¹ * ‖x₀ - (‖x₀‖ : 𝕜) • y‖ := by
+    rw [norm_smul, norm_inv, norm_algebraMap', norm_norm]
+  have h₁ := h ((‖x₀‖ : 𝕜) • y) (F.smul_mem _ hy)
+  rwa [← le_inv_mul_iff₀' (by simpa), ← h₂, smul_sub, inv_smul_smul₀] at h₁
+  simpa using hx₀'
+
+-- theorem riesz_lemma_of_norm_lt {c : 𝕜} (hc : 1 < ‖c‖) {R : ℝ} (hR : ‖c‖ < R) {F : Subspace 𝕜 E}
+--     (hFc : IsClosed (F : Set E)) (hF : ∃ x : E, x ∉ F) :
+--     ∃ x₀ : E, ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖ := by
+
+theorem thing {𝕜 X : Type*} [RCLike 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X]
+    {S : X →L[𝕜] X}
+    (hS_not_surj : ¬ (S : X → X).Surjective)
+    (hS_inj : (S : X → X).Injective)
+    (hT_anti : Topology.IsClosedEmbedding S) :
+    ∃ f : ℕ → X, (∀ n, ‖f n‖ = 1) ∧ Pairwise (2⁻¹ ≤ ‖f · - f ·‖) := by
+  obtain ⟨x, hx⟩ : ∃ x : X, ∀ y, S y ≠ x := by simpa [Function.Surjective] using hS_not_surj
+  let V (n : ℕ) : Submodule 𝕜 X := S.iterateRange n
+  have hV_succ (n : ℕ) : V (n + 1) = (V n).map (S : End 𝕜 X) := LinearMap.iterateRange_succ
+  have hV_closed (n : ℕ) : IsClosed (V n : Set X) := by
+    induction n with
+    | zero => simp [V, Module.End.one_eq_id]
+    | succ n ih =>
+      rw [hV_succ]
+      apply hT_anti.isClosedMap _ ih
+  have x (n : ℕ) : ∃ x ∈ V n, ‖x‖ = 1 ∧ ∀ y ∈ V (n + 1), 2⁻¹ ≤ ‖x - y‖ := by
+    have h₁ : IsClosed (Submodule.comap (V n).subtype (V (n + 1)) : Set (V n)) := by
+      simpa using (hV_closed (n + 1)).preimage_val
+    have h₂ : ∃ x : V n, x ∉ (V (n + 1)).comap (V n).subtype := by
+      suffices ∃ a, ∀ y, S y ≠ a by simpa [iterate_succ, V, (iterate_injective hS_inj n).eq_iff]
+      use x
+    obtain ⟨⟨x, hx⟩, hx', hxn, hxy⟩ := riesz_lemma_one h₁ h₂ (show 2⁻¹ < 1 by norm_num)
+    simp only [Submodule.mem_comap, Submodule.subtype_apply, AddSubgroupClass.coe_norm,
+      AddSubgroupClass.coe_sub, Subtype.forall] at hx' hxn hxy
+    exact ⟨x, hx, hxn, fun y hy ↦ hxy y (S.iterateRange.monotone (by simp) hy) hy⟩
+  choose x hxv hxn hxy using x
+  refine ⟨x, hxn, ?_⟩
+  intro m n hmn
+  wlog! hmn' : m < n generalizing m n
+  · rw [norm_sub_rev]
+    exact this hmn.symm (by order)
+  exact hxy m (x n) (S.iterateRange.monotone hmn' (hxv n))
+
+/-- The Fredholm alternative for compact operators: if `T` is a compact operator and `μ ≠ 0`,
+then either `μ` is an eigenvalue of `T`, or `μ` is in the resolvent set of `T`. -/
+theorem fredholm_alternative [CompleteSpace X] (hT : IsCompactOperator T)
+    {μ : 𝕜} (hμ : μ ≠ 0) :
+    HasEigenvalue (T : End 𝕜 X) μ ∨ μ ∈ resolventSet 𝕜 T := by
   by_contra!
   obtain ⟨h₁, h₂⟩ := this
-  let S := (T - μ • 1)
+  let (eq := hS) S := (T - μ • 1)
   replace h₂ : ¬ (S : X → X).Bijective := by
     rw [spectrum.mem_resolventSet_iff, ← IsUnit.neg_iff,
       ContinuousLinearMap.isUnit_iff_bijective] at h₂
     convert h₂
     ext x
     simp [S]
-  have : (S : X → X).Injective := by
+  obtain ⟨K, -, hK : AntilipschitzWith K S⟩ := antilipschitz_of_not_hasEigenvalue hT hμ h₁
+  obtain ⟨f, hf_norm, hf_pair⟩ := thing (mt (.intro hK.injective) h₂) hK.injective
+    (hK.isClosedEmbedding S.uniformContinuous)
+  have : Pairwise fun x₁ x₂ ↦ 2⁻¹ * K ≤ ‖T (f x₁) - T (f x₂)‖ := by
+    intro m n hmn
+    have := hK.le_mul_dist (f m) (f n)
+    simp [dist_eq_norm_sub] at this
     sorry
   sorry
+
+
+  -- have S_inj : (S : X → X).Injective := by
+  --   rw [hasEigenvalue_iff, eigenspace_def, not_not, LinearMap.ker_eq_bot] at h₁
+  --   exact h₁
+  -- let V (n : ℕ) : Submodule ℂ X := (S ^ n).range
+
+  -- sorry
+
+-- #min_imports