OAI/Analysis/Conductivity/Variational/CompactDepthReductionTwo.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ScalarConductivity.exists_compact_depth_reduction_two line 25
2. theorem OAI.ScalarConductivity.exists_compact_depth_reduction_selected line 79
3. lemma OAI.ScalarConductivity.gradientColumns_surjective line 134
4. lemma OAI.ScalarConductivity.exists_independent_pairedPotential_at line 145
5. lemma OAI.ScalarConductivity.pairedPotential_contDiffOn line 154
6. lemma OAI.ScalarConductivity.column_derivative_ne_zero_of_independent line 163
7. lemma OAI.ScalarConductivity.conductivityFlux_affine_column line 177
8. lemma OAI.ScalarConductivity.active_flux_harmonic_of_affine line 191
9. def OAI.ScalarConductivity.TwoFieldRankRegular line 210
10. lemma OAI.ScalarConductivity.TwoFieldRankRegular.mono line 218