OAI/Analysis/Conductivity/Sobolev/LpExtension.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.lpZeroExtensionL line 17
  2. lemma OAI.ScalarConductivity.lpZeroExtensionL_ae line 45
  3. lemma OAI.ScalarConductivity.lpZeroExtensionL_norm line 49
  4. def OAI.ScalarConductivity.lpZeroExtensionCLM line 54
  5. lemma OAI.ScalarConductivity.lpZeroExtensionCLM_ae line 57
  6. lemma OAI.ScalarConductivity.lpZeroExtensionCLM_ae_of_ae line 60
  7. def OAI.ScalarConductivity.lpRestrictionCLM line 69
  8. lemma OAI.ScalarConductivity.lpRestrictionCLM_ae line 72
  9. lemma OAI.ScalarConductivity.lpMultiplier_mem line 84
  10. def OAI.ScalarConductivity.lpMultiplierL line 91
  11. def OAI.ScalarConductivity.lpMultiplierCLM line 111
  12. lemma OAI.ScalarConductivity.lpMultiplierCLM_ae line 120
  13. def OAI.ScalarConductivity.compactMultiplierCLM line 124
  14. lemma OAI.ScalarConductivity.compactMultiplierCLM_ae line 129