OAI/Analysis/Conductivity/Variational/CentralEuclideanBridge.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.centralEuclideanCLE line 14
  2. lemma OAI.ScalarConductivity.centralEuclidean_volume line 17
  3. lemma OAI.ScalarConductivity.centralEuclidean_integral line 20
  4. lemma OAI.ScalarConductivity.centralEuclidean_direction line 24
  5. lemma OAI.ScalarConductivity.centralEuclidean_partial line 30
  6. lemma OAI.ScalarConductivity.centralEuclidean_laplacian line 39
  7. def OAI.ScalarConductivity.centralHarmonicRegion line 66
  8. def OAI.ScalarConductivity.centralZeroExtension line 69
  9. lemma OAI.ScalarConductivity.centralZeroExtension_memLp line 72
  10. def OAI.ScalarConductivity.centralWholeL2 line 76
  11. lemma OAI.ScalarConductivity.centralWholeL2_ae line 79
  12. theorem OAI.ScalarConductivity.central_variational_euclidean_weak line 82