OAI/Analysis/Conductivity/Sobolev/CompactLipschitzH1.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.lipschitz_weakDirection line 12
2. lemma OAI.ScalarConductivity.WeakL2Direction.congr line 23
3. lemma OAI.ScalarConductivity.lineDeriv_zero_outside line 34
4. lemma OAI.ScalarConductivity.bounded_support_compact line 44
5. lemma OAI.ScalarConductivity.lipschitz_lineDeriv_memLp line 52
6. theorem OAI.ScalarConductivity.compact_lipschitz_H1 line 61
7. lemma OAI.ScalarConductivity.segment_meets_frontier line 86
8. lemma OAI.ScalarConductivity.lipschitz_piecewise_frontier line 99
9. lemma OAI.ScalarConductivity.piecewise_lineDeriv_off_frontier line 133
10. theorem OAI.ScalarConductivity.compact_lipschitz_seam_H1 line 155