OAI/Geometry/EinsteinFour/ScalarLocalL2Source.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compact-test forcing with an L2 localization gives a genuine order-zero Sobolev source, without requiring a smooth right-hand side.

  1. theorem OAI.PositiveEinsteinFour.Geometry.scalar_localize_memSobolev_zero_of_L2_source line 19