OAI/Topology/CoarseAssembly/FamilyEmbeddingIndependence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoarseAssembly.DiscreteRoe.coefficientFamilyBoundary line 18

   Source documentation

   Boundary of a family after specified coefficient embeddings.

   def coefficientFamilyBoundary (o : ∀ i, Q i) (A : ∀ i, Operator (Q i) (E i))
       (C : ℝ) (hC : 0 ≤ C) (hA : ∀ i, ‖A i‖ ≤ C)
       (r : ℝ) (hr : 0 ≤ r) (hp : ∀ i, PropagationLE r (A i))
       (hs : ∀ i, IsSelfAdjoint (A i))
       (hsq : ∀ i, IsCompactOperator (A i * A i - (1 : Operator (Q i) (E i))))
       (V : ∀ i, E i →ₗᵢ[ℂ] H) :
       letI := separatedMetric o
   …

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

2. theorem OAI.CoarseAssembly.DiscreteRoe.coefficientFamilyBoundary_independent line 35

   Source documentation

   This compares whole-union classes directly, without passing to component K₁ classes.

   theorem coefficientFamilyBoundary_independent (o : ∀ i, Q i)
       (A : ∀ i, Operator (Q i) (E i)) (C : ℝ) (hC : 0 ≤ C) (hA : ∀ i, ‖A i‖ ≤ C)
       (r : ℝ) (hr : 0 ≤ r) (hp : ∀ i, PropagationLE r (A i))
       (hs : ∀ i, IsSelfAdjoint (A i))
       (hsq : ∀ i, IsCompactOperator (A i * A i - (1 : Operator (Q i) (E i))))
       (V W : ∀ i, E i →ₗᵢ[ℂ] H) :
       letI := separatedMetric o
   …

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