OAI/Topology/CoarseAssembly/FiniteHeadNormalization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoarseAssembly.DiscreteRoe.finiteHeadRadius line 19
2. theorem OAI.CoarseAssembly.DiscreteRoe.finiteHeadRadius_nonneg line 22
3. theorem OAI.CoarseAssembly.DiscreteRoe.finiteHeadRadius_diam line 27
4. theorem OAI.CoarseAssembly.DiscreteRoe.finiteHead_propagation line 41
5. def OAI.CoarseAssembly.DiscreteRoe.componentHilbert line 52
6. theorem OAI.CoarseAssembly.DiscreteRoe.exists_finiteHead_involution line 61

   Source documentation

   Only finitely many components are changed. Their new operators are involutions, their differences are compact, and all propagation stays bounded.

   theorem exists_finiteHead_involution (J : Finset ℕ) (A : ∀ i, Operator (V i) H)
       (C : ℝ) (hA : ∀ i, ‖A i‖ ≤ C) (r : ℝ)
       (hp : ∀ i, PropagationLE r (A i))
       (hs : ∀ i, IsSelfAdjoint (A i))
       (hc : ∀ i, IsCompactOperator (A i * A i - (1 : Operator (V i) H))) :
       ∃ B : ∀ i, Operator (V i) H,
         (∀ i, IsSelfAdjoint (B i)) ∧
         (∀ i, ‖B i‖ ≤ max C 1) ∧
         (∀ i, PropagationLE (max r (finiteHeadRadius (V := V) J)) (B i)) ∧
   …

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

7. structure OAI.CoarseAssembly.DiscreteRoe.FiniteHeadReplacement line 104
8. def OAI.CoarseAssembly.DiscreteRoe.finiteHeadReplacement line 113
9. theorem OAI.CoarseAssembly.DiscreteRoe.FiniteHeadReplacement.square_compact line 128