OAI/Analysis/Conductivity/Sobolev/LocalJoinedH1.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.gradient_of_pi_function line 10
2. lemma OAI.ScalarConductivity.compact_smooth_pi_H1 line 21
3. def OAI.ScalarConductivity.localJoinedValue line 44
4. def OAI.ScalarConductivity.localJoinedGradient line 47
5. theorem OAI.ScalarConductivity.smoothCollarTrace_localJoined_H1 line 52