OAI/Analysis/Conductivity/Sobolev/SobolevMaximum.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.energy_integrable line 12
  2. lemma OAI.ScalarConductivity.zero_of_weakGradient_zero line 21
  3. lemma OAI.ScalarConductivity.chain_zero line 31
  4. def OAI.ScalarConductivity.upperTransitionFun line 43
  5. lemma OAI.ScalarConductivity.upperTransitionFun_smooth line 45
  6. lemma OAI.ScalarConductivity.upperTransitionFun_deriv line 48
  7. def OAI.ScalarConductivity.upperTransition line 55
  8. lemma OAI.ScalarConductivity.upperTransition_nonneg line 64
  9. lemma OAI.ScalarConductivity.upperTransition_zero_iff line 67
  10. lemma OAI.ScalarConductivity.upperTransition_deriv_nonneg line 72
  11. lemma OAI.ScalarConductivity.upperTransition_deriv_zero line 78
  12. theorem OAI.ScalarConductivity.harmonic_le_of_trace_le line 86
  13. lemma OAI.ScalarConductivity.harmonic_neg line 128
  14. lemma OAI.ScalarConductivity.weakValue_neg line 135
  15. theorem OAI.ScalarConductivity.harmonic_bounded_of_trace_bounded line 140