OAI/Analysis/Conductivity/Variational/CentralVariational.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ScalarConductivity.spectralGraphWeight line 11
2. def OAI.ScalarConductivity.spectralGraphMean line 16
3. def OAI.ScalarConductivity.centralForm line 25
4. lemma OAI.ScalarConductivity.centralForm_apply line 31
5. lemma OAI.ScalarConductivity.centralForm_lower line 37
6. theorem OAI.ScalarConductivity.solve_form_mod_constants line 43
7. theorem OAI.ScalarConductivity.central_variational_exists line 92
8. theorem OAI.ScalarConductivity.central_variational_exists_graph line 138