OAI/Topology/CoarseAssembly/RegularConstants.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoarseAssembly.leftTranslationHom line 16

   Source documentation

   Left translations form a unitary representation, with the ample coefficient space unchanged.

   def leftTranslationHom : Q →* (lp (fun _ : Q => H) 2 ≃ₗᵢ[ℂ] lp (fun _ : Q => H) 2) where
   …

2. theorem OAI.CoarseAssembly.regular_fixed_projection line 27
3. theorem OAI.CoarseAssembly.regular_fixed_iff_projection line 52
4. theorem OAI.CoarseAssembly.inner_eq_zero_of_projection_zero line 62

   Source documentation

   The kernel of the constant projection is orthogonal to every invariant vector of the regular representation.

   theorem inner_eq_zero_of_projection_zero (x y : lp (fun _ : Q => H) 2)
       (hx : constantProjection Q x = 0) (hy : constantProjection Q y = y) :
       inner ℂ y x = 0 := by
   …

   Mentions: OAI.CoarseAssembly.constantProjection