refactor(Channel/FixedPoint): use CLMs in Cesaro limits

Author: texra-ai

TNLean/Channel/FixedPoint/Cesaro.lean

@@ -289,10 +289,11 @@ theorem IsChannel.exists_posSemidef_fixedPoint
   have hρ_psd : ρ.PosSemidef := hρ_mem.1
   have hρ_tr : trace ρ = 1 := hρ_mem.2
   -- Step 6: Show E(ρ) = ρ via telescoping + convergence
-  have hE_cont : Continuous E := LinearMap.continuous_of_finiteDimensional E
+  let E' : Matrix (Fin D) (Fin D) ℂ →L[ℂ] Matrix (Fin D) (Fin D) ℂ :=
+    LinearMap.toContinuousLinearMap E
   -- σ ∘ φ → ρ, E ∘ σ ∘ φ → E(ρ)
-  have h_Eσ : Filter.Tendsto (E ∘ σ ∘ φ) Filter.atTop (nhds (E ρ)) :=
-    (hE_cont.tendsto ρ).comp hφ_tendsto
+  have h_Eσ : Filter.Tendsto (E ∘ σ ∘ φ) Filter.atTop (nhds (E ρ)) := by
+    simpa [E'] using (E'.continuous.tendsto ρ).comp hφ_tendsto
   -- (E(σ(φ k)) - σ(φ k)) → E(ρ) - ρ
   have h_diff : Filter.Tendsto (fun k => (E ∘ σ ∘ φ) k - (σ ∘ φ) k)
       Filter.atTop (nhds (E ρ - ρ)) :=

TNLean/Channel/Irreducible/Ergodicity.lean

@@ -97,10 +97,13 @@ theorem IsChannel.cesaroMean_subseq_limit_fixedPoint
   have hσ_mem : σ ∈ densityMatrices D :=
     (densityMatrices_isCompact (D := D)).isClosed.mem_of_tendsto hσ_tendsto <|
       Filter.Eventually.of_forall fun k => hces_mem (ψ k)
-  have hE_cont : Continuous E := LinearMap.continuous_of_finiteDimensional E
+  let E' : Matrix (Fin D) (Fin D) ℂ →L[ℂ] Matrix (Fin D) (Fin D) ℂ :=
+    LinearMap.toContinuousLinearMap E
   have h_Eσ : Filter.Tendsto (fun k => E (cesaroMean E ρ (ψ k + 1)))
-      Filter.atTop (nhds (E σ)) :=
-    (hE_cont.tendsto σ).comp hσ_tendsto
+      Filter.atTop (nhds (E σ)) := by
+    change Filter.Tendsto (E ∘ fun k => cesaroMean E ρ (ψ k + 1))
+      Filter.atTop (nhds (E σ))
+    simpa [E'] using (E'.continuous.tendsto σ).comp hσ_tendsto
   have h_diff : Filter.Tendsto
       (fun k => E (cesaroMean E ρ (ψ k + 1)) - cesaroMean E ρ (ψ k + 1))
       Filter.atTop (nhds (E σ - σ)) :=