OAI/Analysis/Conductivity/Variational/CompactBridge.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ScalarConductivity.SpatialBump line 15
  2. def OAI.ScalarConductivity.bumpProbability line 17
  3. instance OAI.ScalarConductivity.bumpProbability_isProbability line 20
  4. lemma OAI.ScalarConductivity.bumpProbability_integral line 26
  5. lemma OAI.ScalarConductivity.bumpProbability_ball line 32
  6. def OAI.ScalarConductivity.mollifyReal line 41
  7. lemma OAI.ScalarConductivity.mollifyReal_smooth line 44
  8. lemma OAI.ScalarConductivity.mollifyReal_eq_average line 49
  9. lemma OAI.ScalarConductivity.mollifyReal_sub line 54
  10. lemma OAI.ScalarConductivity.mollifyReal_memLp line 64
  11. theorem OAI.ScalarConductivity.mollifyReal_approx line 68
  12. def OAI.ScalarConductivity.WeakL2Direction line 79
  13. lemma OAI.ScalarConductivity.mollifyReal_fderiv_eq line 83
  14. lemma OAI.ScalarConductivity.mollifyReal_direction line 101
  15. lemma OAI.ScalarConductivity.mollifyReal_zero_outside line 130
  16. lemma OAI.ScalarConductivity.mollifyReal_support line 150
  17. lemma OAI.ScalarConductivity.mollifyReal_compact line 158
  18. def OAI.ScalarConductivity.dyadicBump line 168
  19. lemma OAI.ScalarConductivity.dyadicBump_radius line 177
  20. def OAI.ScalarConductivity.mollifyL2 line 180
  21. lemma OAI.ScalarConductivity.mollifyL2_ae line 183
  22. lemma OAI.ScalarConductivity.mollifyL2_norm_sq line 187
  23. lemma OAI.ScalarConductivity.mollifyL2_tendsto line 194
  24. abbrev OAI.ScalarConductivity.WholeJetSpace line 209
  25. def OAI.ScalarConductivity.jetCoordinateL line 211
  26. lemma OAI.ScalarConductivity.jetCoordinateL_apply line 214
  27. def OAI.ScalarConductivity.wholeJet line 218
  28. lemma OAI.ScalarConductivity.wholeJet_ae line 221
  29. lemma OAI.ScalarConductivity.wholeJet_continuous line 235
  30. def OAI.ScalarConductivity.ballJet line 241
  31. lemma OAI.ScalarConductivity.ballJet_ae line 244
  32. lemma OAI.ScalarConductivity.ballJet_continuous line 251
  33. lemma OAI.ScalarConductivity.ballJet_mollify_tendsto line 254
  34. lemma OAI.ScalarConductivity.mollifiedJet_eq line 259
  35. theorem OAI.ScalarConductivity.compact_weakJet_mem_zeroTrace line 288
  36. lemma OAI.ScalarConductivity.zeroTraceAmbient_le_H1Space line 311
  37. theorem OAI.ScalarConductivity.compact_weak_H1 line 317