OAI/Geometry/EinsteinFour/ScalarMinimizingSequence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Strong convergence of a minimizing sequence once its actual Lp values converge. This is the Hilbert-space closure step for taking absolute values.

  1. theorem OAI.PositiveEinsteinFour.Geometry.scalar_energy_minimizing_sequence_cauchy line 18
  2. theorem OAI.PositiveEinsteinFour.Geometry.scalar_energy_minimizing_sequence_limit line 56