OAI/Topology/CoarseAssembly/FiberConstants.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The normalized constant subspace of a finite fiber

The fiber embedding sends h to the constant vector |Q|⁻¹ᐟ² h. It is an actual linear isometry, including for singleton boundary fibers.

  1. def OAI.CoarseAssembly.fiberNormalization line 19
  2. theorem OAI.CoarseAssembly.fiberNormalization_nonneg line 21
  3. theorem OAI.CoarseAssembly.fiberNormalization_sq line 24
  4. def OAI.CoarseAssembly.fiberConstant line 31
  5. theorem OAI.CoarseAssembly.fiberConstant_apply line 34
  6. theorem OAI.CoarseAssembly.fiberConstant_norm line 37
  7. def OAI.CoarseAssembly.fiberConstantIsometry line 49
  8. theorem OAI.CoarseAssembly.fiberNormalization_of_unique line 62

    Source documentation

    Singleton boundary fibers have normalization one.

    @[simp] theorem fiberNormalization_of_unique [Unique Q] : fiberNormalization Q = 1 := by
…

    Mentions: OAI.CoarseAssembly.fiberNormalization