OAI/Geometry/EinsteinFour/ScalarH1EllipticGain.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local H3 elliptic gain for an actual first-order Sobolev source.

  1. theorem OAI.PositiveEinsteinFour.Geometry.scalar_localize_eq_of_tests line 20
  2. theorem OAI.PositiveEinsteinFour.Geometry.scalar_ball_H1_forcing_gain line 33