OAI/Geometry/CAT0Fillings/Minimizers/CriticalEnergy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.AnalyticMinimizer.inner_tendsto_map line 18
2. lemma OAI.CAT0Fillings.AnalyticMinimizer.exists_weak_strong_subsequence line 23
3. def OAI.CAT0Fillings.AnalyticMinimizer.energy line 57
4. lemma OAI.CAT0Fillings.AnalyticMinimizer.energy_nonneg line 61
5. lemma OAI.CAT0Fillings.AnalyticMinimizer.energy_smul line 67
6. lemma OAI.CAT0Fillings.AnalyticMinimizer.energy_defect line 73
7. lemma OAI.CAT0Fillings.AnalyticMinimizer.energy_le_limit line 91