OAI/Geometry/Kahler/BaseModelSign.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PinchedHartogs.BaseConstruction.modelIntegrand line 19
2. def OAI.PinchedHartogs.BaseConstruction.modelMean line 23
3. lemma OAI.PinchedHartogs.BaseConstruction.modelIntegrand_continuous line 26
4. lemma OAI.PinchedHartogs.BaseConstruction.modelIntegrand_continuous_y line 40
5. lemma OAI.PinchedHartogs.BaseConstruction.RadialProfiles.log_lt_cutoff line 46
6. lemma OAI.PinchedHartogs.BaseConstruction.modelIntegrand_zero_low line 52
7. lemma OAI.PinchedHartogs.BaseConstruction.modelIntegrand_zero_high line 65
8. lemma OAI.PinchedHartogs.BaseConstruction.RadialProfiles.model_weight_zero line 74
9. lemma OAI.PinchedHartogs.BaseConstruction.model_small_integral line 82
10. lemma OAI.PinchedHartogs.BaseConstruction.model_large_integral line 112
11. lemma OAI.PinchedHartogs.BaseConstruction.modelMean_zero line 125