SeparatedFamilyPerturbation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Compact changes on components give Roe perturbations on the whole union

theorem OAI.CoarseAssembly.DiscreteRoe.diagonalFamily_sub_mem_roe line 18

theorem OAI.CoarseAssembly.DiscreteRoe.separatedFamilyBoundary_eq_of_component_compact line 56

Source documentation

Componentwise compact changes preserve the whole-union class, even when these compact operators do not tend to zero in norm.

theorem separatedFamilyBoundary_eq_of_component_compact (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)))
    (hAB : ∀ i, IsCompactOperator (A i - B i)) :
    letI := separatedMetric o
…

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