OAI/Geometry/EinsteinFour/ScalarHalfBallH2Gain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local H4 gain where only the smaller-ball forcing is H2. This avoids assuming any regularity of the forcing outside the coordinate neighborhood.

  1. theorem OAI.PositiveEinsteinFour.Geometry.scalar_half_ball_H2_forcing_gain line 22