OAI/Analysis/Conductivity/Sobolev/SobolevTraceChain.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.continuous_binary_closure line 11
  2. lemma OAI.ScalarConductivity.smoothJet_sub line 26
  3. lemma OAI.ScalarConductivity.chainDifference_smooth_compact line 33
  4. lemma OAI.ScalarConductivity.chainDifference_H10 line 63
  5. lemma OAI.ScalarConductivity.chain_trace_eq line 76
  6. abbrev OAI.ScalarConductivity.weakValue line 84
  7. lemma OAI.ScalarConductivity.jet_clipped_of_bound line 86
  8. lemma OAI.ScalarConductivity.jetValue_product line 92
  9. lemma OAI.ScalarConductivity.jetGradient_product line 95
  10. theorem OAI.ScalarConductivity.exists_H1_product line 102
  11. lemma OAI.ScalarConductivity.smoothJet_constant line 128
  12. lemma OAI.ScalarConductivity.constantJet_memLp line 134
  13. def OAI.ScalarConductivity.constantH1 line 138
  14. lemma OAI.ScalarConductivity.constantH1_value line 142
  15. lemma OAI.ScalarConductivity.constantH1_gradient line 147
  16. lemma OAI.ScalarConductivity.weakValue_add line 153
  17. lemma OAI.ScalarConductivity.weakValue_sub line 158
  18. lemma OAI.ScalarConductivity.weakValue_smul line 163
  19. lemma OAI.ScalarConductivity.weakGradient_add line 168
  20. lemma OAI.ScalarConductivity.weakGradient_sub line 173
  21. lemma OAI.ScalarConductivity.weakGradient_smul line 178