OAI/Analysis/Conductivity/Sobolev/SobolevChain.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ScalarConductivity.sobolevChainLp line 14
2. lemma OAI.ScalarConductivity.sobolevChainLp_continuous line 19
3. lemma OAI.ScalarConductivity.sobolevChainLp_coe_ae line 22
4. lemma OAI.ScalarConductivity.sobolevChainLp_smooth line 28
5. lemma OAI.ScalarConductivity.sobolevChainLp_preserves_H1 line 41
6. lemma OAI.ScalarConductivity.sobolevChainLp_preserves_H10 line 51
7. def OAI.ScalarConductivity.sobolevChain line 62
8. lemma OAI.ScalarConductivity.sobolevChain_value line 66
9. lemma OAI.ScalarConductivity.sobolevChain_gradient line 75
10. lemma OAI.ScalarConductivity.sobolevChain_H10 line 85