OAI/Analysis/Mahler/NormSquareJet.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SymmetricMahler.ComplexTwoJet line 13
  2. def OAI.SymmetricMahler.sumNormSq line 16
  3. def OAI.SymmetricMahler.sumNormSqD line 18
  4. def OAI.SymmetricMahler.sumNormSqD2 line 22
  5. lemma OAI.SymmetricMahler.continuous_sumNormSq line 27
  6. lemma OAI.SymmetricMahler.continuous_sumNormSqD line 31
  7. lemma OAI.SymmetricMahler.continuous_sumNormSqD2 line 44
  8. lemma OAI.SymmetricMahler.hasFDerivAt_sumNormSq line 67
  9. lemma OAI.SymmetricMahler.hasFDerivAt_sumNormSqD line 76