OAI/Geometry/EinsteinFour/ScalarL4ProductConvergence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Strong convergence of the quadratic gradient term in the local H2 chain rule. The coefficient is bounded and converges almost everywhere; the two first-derivative factors converge in L4.

  1. def OAI.PositiveEinsteinFour.Geometry.scalarL4Product line 28
  2. theorem OAI.PositiveEinsteinFour.Geometry.scalarL4Product_coe line 31
  3. theorem OAI.PositiveEinsteinFour.Geometry.scalarL4Product_tendsto line 35
  4. theorem OAI.PositiveEinsteinFour.Geometry.scalarL4Product_coefficient_tendsto line 43