OAI/Analysis/Conductivity/Variational/WeakHarmonicClassical.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.compact_weak_harmonic_laplacian line 15
2. lemma OAI.ScalarConductivity.smooth_weak_harmonic_laplacian line 40
3. theorem OAI.ScalarConductivity.weakWeyl_pair_ae_regular line 65
4. lemma OAI.ScalarConductivity.compactCrossMoment_eval line 94
5. theorem OAI.ScalarConductivity.compactMoment_uniform_inverse line 113
6. theorem OAI.ScalarConductivity.wall_moment_uniform_inverse line 143