OAI/Geometry/PrescribedPotential/RealSmoothCompactness.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Real Smooth Compactness.

  1. lemma OAI.GlobalElliptic.Localizers.smooth_tendsto_real_order line 25
  2. lemma OAI.GlobalElliptic.Localizers.smooth_value_tendsto line 33
  3. lemma OAI.GlobalElliptic.Localizers.smooth_limit_real line 43
  4. theorem OAI.GlobalElliptic.GluingData.real_smooth_sequence_compact line 65