OAI/Topology/CoarseAssembly/FiniteTailIndependence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CoarseAssembly.DiscreteRoe.separatedFamilyBoundary_eq_of_tail line 20

   Source documentation

   Finite-head independence is proved within the single Roe algebra, using controlled compact perturbations and equality of rational unitaries.

   theorem separatedFamilyBoundary_eq_of_tail (o : ∀ i, V i)
       (A B : ∀ i, Operator (V i) H) (C D : ℝ) (hC : 0 ≤ C) (hD : 0 ≤ D)
       (hA : ∀ i, ‖A i‖ ≤ C) (hB : ∀ i, ‖B i‖ ≤ D)
       (r s : ℝ) (hr : 0 ≤ r) (hs : 0 ≤ s)
       (hp : ∀ i, PropagationLE r (A i)) (hq : ∀ i, PropagationLE s (B i))
       (hAs : ∀ i, IsSelfAdjoint (A i)) (hBs : ∀ i, IsSelfAdjoint (B i))
       (hAsq : ∀ i, IsCompactOperator (A i * A i - (1 : Operator (V i) H)))
       (hBsq : ∀ i, IsCompactOperator (B i * B i - (1 : Operator (V i) H)))
       (J : Finset ℕ) (htail : ∀ i, i ∉ J → A i = B i) :
       letI := separatedMetric o
   …

   Mentions: OAI.CoarseAssembly.DiscreteRoe.Operator, OAI.CoarseAssembly.DiscreteRoe.PropagationLE, OAI.CoarseAssembly.separatedMetric