OAI/Analysis/AncientFlat/Regularity/HolderAlgebra.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ParabolicInterior.pdist_nonneg line 11
2. lemma OAI.ParabolicInterior.HolderBound.mono line 13
3. lemma OAI.ParabolicInterior.HolderBound.restrict line 18
4. lemma OAI.ParabolicInterior.HolderBound.add line 22
5. lemma OAI.ParabolicInterior.HolderBound.clm line 29
6. lemma OAI.ParabolicInterior.HolderBound.smul line 36
7. lemma OAI.ParabolicInterior.supported_freezing_error line 51