OAI/Geometry/EinsteinFour/ScalarL2BoundedMultiplier.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A bounded scalar coefficient acts continuously and linearly on L2. This permits passage of local coordinate gradient bounds through H1 closure.

  1. def OAI.PositiveEinsteinFour.Geometry.scalarL2BoundedMultiplier line 17
  2. theorem OAI.PositiveEinsteinFour.Geometry.scalarL2BoundedMultiplier_coe line 45