OAI/Geometry/Kahler/BaseLogApproximation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PinchedHartogs.BaseConstruction.logFactor_complex_identity line 19
  2. lemma OAI.PinchedHartogs.BaseConstruction.logFactor_ratio_bound line 34
  3. def OAI.PinchedHartogs.BaseConstruction.logMean line 47
  4. def OAI.PinchedHartogs.BaseConstruction.logNormalized line 48
  5. def OAI.PinchedHartogs.BaseConstruction.logTerm line 49
  6. def OAI.PinchedHartogs.BaseConstruction.logTruncation line 50
  7. lemma OAI.PinchedHartogs.BaseConstruction.logNormalized_norm_lt line 52
  8. lemma OAI.PinchedHartogs.BaseConstruction.regularizedLog_hasSum line 56
  9. lemma OAI.PinchedHartogs.BaseConstruction.logTerm_bound line 82
  10. lemma OAI.PinchedHartogs.BaseConstruction.logTruncation_error line 93
  11. lemma OAI.PinchedHartogs.BaseConstruction.logNormalized_continuous line 117
  12. lemma OAI.PinchedHartogs.BaseConstruction.logMean_continuous line 123
  13. lemma OAI.PinchedHartogs.BaseConstruction.logTerm_continuous line 128
  14. lemma OAI.PinchedHartogs.BaseConstruction.logTruncation_continuous line 132