OAI/Analysis/Conductivity/Variational/RadialLaplacian.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.radial_fderiv line 16
  2. lemma OAI.ScalarConductivity.radial_second line 24
  3. lemma OAI.ScalarConductivity.radial_laplacian line 41
  4. abbrev OAI.ScalarConductivity.WeylSpace line 75
  5. def OAI.ScalarConductivity.radialEta line 77
  6. def OAI.ScalarConductivity.radialTheta line 80
  7. lemma OAI.ScalarConductivity.hasDerivAt_radialEta line 83
  8. lemma OAI.ScalarConductivity.radialTheta_laplacian line 95
  9. theorem OAI.ScalarConductivity.radial_scale_laplacian line 115
  10. def OAI.ScalarConductivity.radialOneBump line 127
  11. def OAI.ScalarConductivity.radialRaw line 130
  12. lemma OAI.ScalarConductivity.normsq_smooth line 132
  13. lemma OAI.ScalarConductivity.radialRaw_smooth line 137
  14. lemma OAI.ScalarConductivity.radialOneBump_zero line 140
  15. lemma OAI.ScalarConductivity.radialRaw_zero line 147
  16. lemma OAI.ScalarConductivity.radialRaw_compact line 151
  17. lemma OAI.ScalarConductivity.radialRaw_zero_value line 157
  18. lemma OAI.ScalarConductivity.radialRaw_nonneg line 161
  19. def OAI.ScalarConductivity.radialMass line 163
  20. lemma OAI.ScalarConductivity.radialMass_pos line 165
  21. def OAI.ScalarConductivity.radialProfile line 171
  22. def OAI.ScalarConductivity.radialProfilePrimitive line 173
  23. lemma OAI.ScalarConductivity.radialProfile_smooth line 175
  24. lemma OAI.ScalarConductivity.radialProfile_nonneg line 178
  25. lemma OAI.ScalarConductivity.radialProfile_zero line 181
  26. lemma OAI.ScalarConductivity.radialProfilePrimitive_deriv line 184
  27. lemma OAI.ScalarConductivity.radialProfilePrimitive_smooth line 189
  28. lemma OAI.ScalarConductivity.radialProfilePrimitive_zero line 197
  29. lemma OAI.ScalarConductivity.radialEta_smooth line 205
  30. lemma OAI.ScalarConductivity.radialTheta_smooth line 208
  31. lemma OAI.ScalarConductivity.radialEta_zero line 211
  32. lemma OAI.ScalarConductivity.radialTheta_zero line 216
  33. lemma OAI.ScalarConductivity.radialEta_compact line 221
  34. lemma OAI.ScalarConductivity.radialTheta_compact line 227
  35. lemma OAI.ScalarConductivity.radialEta_nonneg line 233
  36. lemma OAI.ScalarConductivity.radialEta_integral line 236