OAI/Analysis/AncientFlat/Regularity/CompactHolder.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.ParabolicLocalization.norm_pair_sub_le_pdistline 12 - lemma
OAI.ParabolicLocalization.holder_of_bounded_lipschitzline 23 - lemma
OAI.ParabolicLocalization.compact_lipschitzline 40 - lemma
OAI.ParabolicLocalization.compact_contDiff_holderline 52