OAI/Analysis/Conductivity/Variational/WeakWeyl.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.closedBall_near_subset line 11
2. theorem OAI.ScalarConductivity.weakWeyl_local line 18
3. def OAI.ScalarConductivity.radialAverageF line 69
4. def OAI.ScalarConductivity.RadialMeanOn line 72
5. lemma OAI.ScalarConductivity.radialAverageF_fderiv line 77
6. lemma OAI.ScalarConductivity.RadialMeanOn.derivative line 86
7. lemma OAI.ScalarConductivity.RadialMeanOn.derivative_bound line 96