OAI/Analysis/Conductivity/Variational/L2TranslationAverage.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ScalarConductivity.WholeL2 line 11
  2. def OAI.ScalarConductivity.translateL2 line 13
  3. lemma OAI.ScalarConductivity.translateL2_ae line 16
  4. lemma OAI.ScalarConductivity.translateL2_norm line 20
  5. lemma OAI.ScalarConductivity.translateL2_zero line 23
  6. lemma OAI.ScalarConductivity.continuous_translateL2 line 28
  7. lemma OAI.ScalarConductivity.wholeL2_norm_sq line 33
  8. lemma OAI.ScalarConductivity.translate_difference_sq line 37
  9. lemma OAI.ScalarConductivity.whole_translation_memLp line 44
  10. lemma OAI.ScalarConductivity.whole_difference_memLp line 61
  11. theorem OAI.ScalarConductivity.translation_average_sq_le line 74
  12. lemma OAI.ScalarConductivity.small_translation_radius line 90
  13. def OAI.ScalarConductivity.radialProbability line 103
  14. lemma OAI.ScalarConductivity.radialProbability_probability line 106
  15. lemma OAI.ScalarConductivity.radialProbability_integral line 114
  16. lemma OAI.ScalarConductivity.radialProbability_ball line 121
  17. lemma OAI.ScalarConductivity.radialMollify_eq_average line 129
  18. lemma OAI.ScalarConductivity.radialMollify_sub line 136
  19. lemma OAI.ScalarConductivity.radialMollify_memLp line 147
  20. theorem OAI.ScalarConductivity.radialMollify_approx line 153