OAI/Geometry/EinsteinFour/ScalarFullBallIntegerGain.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The nested-cutoff estimate gains two derivatives from an integer-order source. This is the finite-order bootstrap used for the linear harmonic two-form equation.

  1. theorem OAI.PositiveEinsteinFour.Geometry.scalar_finite_cutoff_chain_source_gain line 31
  2. theorem OAI.PositiveEinsteinFour.Geometry.scalar_ball_integer_forcing_gain line 58