OAI/Analysis/Conductivity/Sobolev/VoltageH1Completion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ScalarConductivity.smoothVoltageJets line 13
2. def OAI.ScalarConductivity.voltageH1Jets line 18
3. lemma OAI.ScalarConductivity.zeroVoltageJets_le_H1 line 22
4. lemma OAI.ScalarConductivity.voltageH1_gradient_mem line 30
5. lemma OAI.ScalarConductivity.divergence_pairing_compact_voltage line 43
6. lemma OAI.ScalarConductivity.divergence_pairing_zeroVoltageJets line 74
7. theorem OAI.ScalarConductivity.exact_scalarization_H1 line 87