OAI/Analysis/AllenCahn/JetCompactness.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DeGiorgiCompactness.Space line 10
  2. lemma OAI.DeGiorgiCompactness.equicontinuous_of_local_fderiv_bound line 12
  3. lemma OAI.DeGiorgiCompactness.compact_closure_of_local_bounds line 40
  4. theorem OAI.DeGiorgiCompactness.countable_local_compactness line 78
  5. lemma OAI.DeGiorgiCompactness.locallyUniform_pi line 96
  6. def OAI.DeGiorgiCompactness.coordDeriv line 107
  7. def OAI.DeGiorgiCompactness.coordinateDual line 110
  8. lemma OAI.DeGiorgiCompactness.coordinateDual_fderiv line 113
  9. theorem OAI.DeGiorgiCompactness.first_jet_limit line 125
  10. theorem OAI.DeGiorgiCompactness.first_jet_subsequence line 153
  11. lemma OAI.DeGiorgiCompactness.coordDeriv_const_mul line 193
  12. theorem OAI.DeGiorgiCompactness.normalized_first_jet_subsequence line 199
  13. abbrev OAI.DeGiorgiCompactness.JetSpace line 243
  14. def OAI.DeGiorgiCompactness.CoherentJets line 245
  15. lemma OAI.DeGiorgiCompactness.coherentJets_smooth line 249
  16. lemma OAI.DeGiorgiCompactness.coherentJets_closed line 268
  17. lemma OAI.DeGiorgiCompactness.fderiv_norm_le_coord_bound line 282
  18. lemma OAI.DeGiorgiCompactness.jetSet_compact_of_local_bounds line 290