OAI/Analysis/Conductivity/Sobolev/SobolevSmoothTests.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.continuous_gradient_of_smooth line 12
  2. lemma OAI.ScalarConductivity.smoothJet_continuous line 18
  3. lemma OAI.ScalarConductivity.continuous_bound_ball line 27
  4. lemma OAI.ScalarConductivity.smoothJet_memLp line 34
  5. def OAI.ScalarConductivity.smoothH1 line 39
  6. lemma OAI.ScalarConductivity.smoothH1_value line 43
  7. lemma OAI.ScalarConductivity.smoothH1_gradient line 48
  8. lemma OAI.ScalarConductivity.smoothH1_bounded line 53
  9. lemma OAI.ScalarConductivity.smoothH1_mem_H10 line 60
  10. lemma OAI.ScalarConductivity.smoothH1_dense line 65
  11. lemma OAI.ScalarConductivity.compactH1_dense_H10 line 76
  12. lemma OAI.ScalarConductivity.harmonic_of_compact_tests line 89
  13. def OAI.ScalarConductivity.inverseBump line 108
  14. def OAI.ScalarConductivity.inverseClip line 109
  15. def OAI.ScalarConductivity.inverseCorrection line 111
  16. lemma OAI.ScalarConductivity.inverseClip_smooth line 113
  17. lemma OAI.ScalarConductivity.inverseClip_bound line 116
  18. lemma OAI.ScalarConductivity.inverseClip_denominator_pos line 127
  19. lemma OAI.ScalarConductivity.inverseCorrection_smooth line 131
  20. lemma OAI.ScalarConductivity.inverseCorrection_compact line 134
  21. lemma OAI.ScalarConductivity.inverseCorrection_zero line 141
  22. def OAI.ScalarConductivity.inverseOperation line 144
  23. lemma OAI.ScalarConductivity.inverseCorrection_eventually line 147
  24. lemma OAI.ScalarConductivity.inverseCorrection_eq line 156
  25. lemma OAI.ScalarConductivity.inverseCorrection_deriv line 159
  26. lemma OAI.ScalarConductivity.inverseCorrection_bound line 166
  27. theorem OAI.ScalarConductivity.inverseOperation_spec line 176