OAI/Analysis/Conductivity/Geometry/TorusExponential.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ScalarConductivity.torusSize line 10
2. def OAI.ScalarConductivity.torusRate line 11
3. lemma OAI.ScalarConductivity.torusSize_nonneg line 13
4. lemma OAI.ScalarConductivity.torusRate_lower line 15
5. lemma OAI.ScalarConductivity.int_exp_summable line 29
6. lemma OAI.ScalarConductivity.torus_exp_summable line 36
7. lemma OAI.ScalarConductivity.torusRate_exp_summable line 46
8. lemma OAI.ScalarConductivity.pow_mul_exp_bound line 55
9. lemma OAI.ScalarConductivity.torusRate_poly_exp_summable line 82