FiniteHeadBoundary.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Removing finitely many components from the whole-union boundary

The argument works with the actual rational boundary unitary. Involutive components contribute the identity in that unitary, before taking K-theory.

theorem OAI.CoarseAssembly.DiscreteRoe.relativeClass_congr line 23
theorem OAI.CoarseAssembly.DiscreteRoe.separatedFamilyBoundary_eq_of_rational line 30

theorem OAI.CoarseAssembly.DiscreteRoe.separatedFamilyBoundary_eq_of_involutive_head line 66

Source documentation

The finite head can differ arbitrarily when its operators are exact involutions. Equality is proved for the entire Roe boundary.

theorem separatedFamilyBoundary_eq_of_involutive_head (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)
    (hAi : ∀ i, i ∈ J → A i * A i = 1) (hBi : ∀ i, i ∈ J → B i * B i = 1) :
    letI := separatedMetric o
…

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