OAI/Analysis/Conductivity/Flux/FiberDivergenceC1.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.wallAlong_pullback line 12
2. lemma OAI.ScalarConductivity.wallAlong_normal line 20
3. lemma OAI.ScalarConductivity.wallAlong_sub line 28
4. lemma OAI.ScalarConductivity.wallAlong_opNorm_bound line 34
5. lemma OAI.ScalarConductivity.fderiv_normal_tangent line 41
6. theorem OAI.ScalarConductivity.compact_fiber_decomposition_C1 line 48