OAI/Analysis/Mahler/HolomorphicLogC2.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SymmetricMahler.uniform_C2_log_sumNormSq_of_holomorphic line 14
2. def OAI.SymmetricMahler.logCompactAnnulus line 39

   Source documentation

   A fixed closed annulus containing the unit sphere in its interior.

   def logCompactAnnulus (n : ℕ) : Set (EuclideanSpace ℂ (Fin n)) :=
   …

3. lemma OAI.SymmetricMahler.isCompact_logCompactAnnulus line 42
4. lemma OAI.SymmetricMahler.logCompactAnnulus_subset_ball line 45
5. lemma OAI.SymmetricMahler.logCompactAnnulus_ne_zero line 49