OAI/Analysis/Conductivity/Geometry/TorusLipschitzTrace.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.torus_lipschitz_H1_summable line 16
2. lemma OAI.ScalarConductivity.torus_coordinate_H1_summable line 34
3. lemma OAI.ScalarConductivity.torusRate_polynomial_bound line 52
4. theorem OAI.ScalarConductivity.torus_lipschitz_trace_summable line 89
5. theorem OAI.ScalarConductivity.torus_coordinate_trace_summable line 96
6. theorem OAI.ScalarConductivity.torus_lipschitz_trace_exists line 104