OAI/Topology/CoarseAssembly/RipsEmbeddingIndependence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoarseAssembly.Rips.ripsFamilyBoundaryWithEmbeddings line 18
2. theorem OAI.CoarseAssembly.Rips.ripsFamilyBoundaryWithEmbeddings_independent line 32
3. theorem OAI.CoarseAssembly.Rips.ampleRipsFamilyBoundary_eq_withEmbeddings line 44

   Source documentation

   The previously constructed ample boundary is the representative with the chosen embeddings.

   theorem ampleRipsFamilyBoundary_eq_withEmbeddings (o : ∀ i, Q i) (r : ℝ) (hr : 0 ≤ r)
       (c : ∀ i, OddCycle C(Point (Q i) r, ℂ)) (hπ : ∀ i, (c i).representation 1 = 1)
       (hF : ∀ i, IsSelfAdjoint (c i).operator)
       (C : ℝ) (hC : 0 ≤ C) (hc : ∀ i, ‖(c i).operator‖ ≤ C) :
       letI := separatedMetric o
   …

   Mentions: OAI.CoarseAssembly.Rips.Point, OAI.CoarseAssembly.separatedMetric

4. theorem OAI.CoarseAssembly.Rips.ampleRipsFamilyBoundary_embeddings line 58

   Source documentation

   In particular, every choice of ample embeddings gives the existing whole-union class.

   theorem ampleRipsFamilyBoundary_embeddings (o : ∀ i, Q i) (r : ℝ) (hr : 0 ≤ r)
       (c : ∀ i, OddCycle C(Point (Q i) r, ℂ)) (hπ : ∀ i, (c i).representation 1 = 1)
       (hF : ∀ i, IsSelfAdjoint (c i).operator)
       (C : ℝ) (hC : 0 ≤ C) (hc : ∀ i, ‖(c i).operator‖ ≤ C)
       (V : ∀ i, (c i).space →ₗᵢ[ℂ] lp (fun _ : ℕ => ℂ) 2) :
       letI := separatedMetric o
   …

   Mentions: OAI.CoarseAssembly.Rips.Point, OAI.CoarseAssembly.separatedMetric