OAI/Analysis/Conductivity/Sobolev/FiniteEndPhysicalH1.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ScalarConductivity.compact_localLip_H1_pi line 14
2. theorem OAI.ScalarConductivity.cut_physicalPeriodicField_H10 line 32
3. lemma OAI.ScalarConductivity.cut_physicalPeriodicField_lineDeriv line 54
4. lemma OAI.ScalarConductivity.flatEndCoordinates_shift line 86
5. lemma OAI.ScalarConductivity.AngularPeriodic.flatEnd line 91
6. def OAI.ScalarConductivity.attachedPeriodicField line 98
7. lemma OAI.ScalarConductivity.attachedPeriodicField_zero_nhds line 101
8. theorem OAI.ScalarConductivity.attachedPeriodicCorrection_H10 line 110