OAI/Analysis/Conductivity/Sobolev/LocalPiolaFlux.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ScalarConductivity.localPiolaFlux line 17
2. lemma OAI.ScalarConductivity.localPiolaFlux_support line 24
3. lemma OAI.ScalarConductivity.localPiolaFlux_hasCompactSupport line 34
4. lemma OAI.ScalarConductivity.localPiolaFlux_tsupport line 41
5. lemma OAI.ScalarConductivity.local_fderiv_symm_comp line 50
6. lemma OAI.ScalarConductivity.local_fderiv_det_ne_zero line 63
7. lemma OAI.ScalarConductivity.integral_eq_setIntegral_of_zero_off line 72
8. theorem OAI.ScalarConductivity.localPiolaFlux_pairing line 79