OAI/Analysis/Conductivity/Variational/PairedPotential.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.exists_coordinate_nonzero line 24
2. def OAI.ScalarConductivity.pairedPotential line 36
3. def OAI.ScalarConductivity.pairedFunctional line 39
4. lemma OAI.ScalarConductivity.pairedPotential_hasFDerivAt line 42
5. lemma OAI.ScalarConductivity.pairedPotential_contDiff line 51
6. lemma OAI.ScalarConductivity.pairedFunctional_surjective line 60
7. lemma OAI.ScalarConductivity.exists_independent_pairedPotential line 76
8. lemma OAI.ScalarConductivity.exists_smooth_compact_majorant line 91
9. lemma OAI.ScalarConductivity.chart_pullback_measure_le line 111
10. theorem OAI.ScalarConductivity.exists_chart_pure_profile line 137