OAI/Analysis/Conductivity/Sobolev/SobolevSmoothOperations.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ScalarConductivity.SmoothLipZero line 12
  2. instance OAI.ScalarConductivity.(instance at line 20) line 20
  3. lemma OAI.ScalarConductivity.SmoothLipZero.growth line 24
  4. lemma OAI.ScalarConductivity.SmoothLipZero.derivative line 30
  5. def OAI.ScalarConductivity.SmoothLipZero.onLp line 33
  6. lemma OAI.ScalarConductivity.SmoothLipZero.onLp_continuous line 36
  7. lemma OAI.ScalarConductivity.SmoothLipZero.onLp_ae line 39
  8. lemma OAI.ScalarConductivity.SmoothLipZero.preserves_H1 line 43
  9. lemma OAI.ScalarConductivity.SmoothLipZero.preserves_H10 line 47
  10. def OAI.ScalarConductivity.SmoothLipZero.onH1 line 51
  11. lemma OAI.ScalarConductivity.SmoothLipZero.onH1_continuous line 53
  12. lemma OAI.ScalarConductivity.SmoothLipZero.onH1_value line 56
  13. lemma OAI.ScalarConductivity.SmoothLipZero.onH1_gradient line 60
  14. lemma OAI.ScalarConductivity.SmoothLipZero.fixes_of_eq line 64
  15. def OAI.ScalarConductivity.SmoothLipZero.ofCompact line 75
  16. lemma OAI.ScalarConductivity.SmoothLipZero.ofCompact_apply line 82
  17. def OAI.ScalarConductivity.valueBump line 89
  18. def OAI.ScalarConductivity.clippedValue line 92
  19. lemma OAI.ScalarConductivity.clippedValue_smooth line 94
  20. lemma OAI.ScalarConductivity.clippedValue_compact line 97
  21. lemma OAI.ScalarConductivity.clippedValue_zero line 100
  22. lemma OAI.ScalarConductivity.clippedValue_eventually line 102
  23. lemma OAI.ScalarConductivity.clippedValue_eq line 110
  24. lemma OAI.ScalarConductivity.clippedValue_deriv line 113
  25. lemma OAI.ScalarConductivity.exists_clippedValue_bound line 117
  26. def OAI.ScalarConductivity.squaredValue line 122
  27. lemma OAI.ScalarConductivity.squaredValue_smooth line 124
  28. lemma OAI.ScalarConductivity.squaredValue_compact line 127
  29. lemma OAI.ScalarConductivity.squaredValue_zero line 130
  30. lemma OAI.ScalarConductivity.squaredValue_eventually line 132
  31. lemma OAI.ScalarConductivity.squaredValue_eq line 141
  32. lemma OAI.ScalarConductivity.squaredValue_deriv line 144
  33. def OAI.ScalarConductivity.squareOperation line 148
  34. def OAI.ScalarConductivity.clipOperation line 152
  35. lemma OAI.ScalarConductivity.jet_squareOperation line 156
  36. def OAI.ScalarConductivity.jetProduct line 163
  37. lemma OAI.ScalarConductivity.gradient_product line 167
  38. lemma OAI.ScalarConductivity.smoothJet_product line 174
  39. lemma OAI.ScalarConductivity.square_polarization line 183
  40. def OAI.ScalarConductivity.clippedProductLp line 205
  41. lemma OAI.ScalarConductivity.clippedProductLp_continuous line 210
  42. lemma OAI.ScalarConductivity.clippedProductLp_preserves_H1 line 217
  43. lemma OAI.ScalarConductivity.clippedProductLp_ae line 230
  44. lemma OAI.ScalarConductivity.clippedProductLp_smooth line 245
  45. lemma OAI.ScalarConductivity.clippedProductLp_smooth_compact line 261
  46. lemma OAI.ScalarConductivity.clippedProductLp_preserves_H10 line 271