OAI/Analysis/SymmetricDomains/ScaledModelC1Limit.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Release061.Wiener.RealDiscParams line 25
  2. def OAI.Release061.Wiener.normalSlice line 27
  3. def OAI.Release061.Wiener.discSlice line 30
  4. def OAI.Release061.Wiener.scaledModel line 34
  5. def OAI.Release061.Wiener.limitModel line 39
  6. def OAI.Release061.Wiener.scaledDisc line 43
  7. lemma OAI.Release061.Wiener.scaledDisc_eq_model line 47
  8. lemma OAI.Release061.Wiener.normalSlice_contDiffAt line 74
  9. theorem OAI.Release061.Wiener.scaledModel_C1_limit line 82