OAI/Geometry/ProjectionBodies/SignSpectrum.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PettyProjection.Spherical.signFactor line 12
  2. lemma OAI.PettyProjection.Spherical.signFactor_abs_step line 15
  3. lemma OAI.PettyProjection.Spherical.signFactor_abs_le_four line 44
  4. lemma OAI.PettyProjection.Spherical.homogeneous_two_mem_harmonic_sup line 66
  5. lemma OAI.PettyProjection.Spherical.lowSpace_eq line 86
  6. lemma OAI.PettyProjection.Spherical.harmonic_inner_ne line 100
  7. lemma OAI.PettyProjection.Spherical.lowSpace_projection line 105
  8. lemma OAI.PettyProjection.Spherical.Q_eq_sub_projections line 127
  9. lemma OAI.PettyProjection.Spherical.harmonic_projection_of_mem_ne line 131
  10. lemma OAI.PettyProjection.Spherical.harmonic_projection_Q line 138
  11. lemma OAI.PettyProjection.hilbertSum_norm_le_of_projection_bound line 167
  12. lemma OAI.PettyProjection.inner_projection_both line 182
  13. lemma OAI.PettyProjection.hilbertSum_hasSum_inner line 187
  14. lemma OAI.PettyProjection.hilbertSum_multiplier_selfadj line 193
  15. lemma OAI.PettyProjection.Spherical.casimir_continuous line 212
  16. def OAI.PettyProjection.Spherical.casimirMap line 218
  17. lemma OAI.PettyProjection.Spherical.casimir_projection line 221
  18. def OAI.PettyProjection.Spherical.signOperator line 240
  19. lemma OAI.PettyProjection.Spherical.signOperator_projection_even line 243
  20. lemma OAI.PettyProjection.Spherical.signOperator_projection_odd line 253
  21. lemma OAI.PettyProjection.Spherical.norm_Q_signOperator_le line 258
  22. lemma OAI.PettyProjection.Spherical.signOperator_selfadj line 277
  23. lemma OAI.PettyProjection.Spherical.cosine_sub_smul line 306
  24. lemma OAI.PettyProjection.Spherical.signOperator_apply line 315
  25. lemma OAI.PettyProjection.Spherical.casimir_const line 322
  26. lemma OAI.PettyProjection.Spherical.mean_casimir_zero line 329
  27. lemma OAI.PettyProjection.Spherical.mean_signOperator line 334
  28. lemma OAI.PettyProjection.Spherical.mean_signOperator_expand line 349
  29. lemma OAI.PettyProjection.Spherical.cosine_casimir_selfadj line 364
  30. lemma OAI.PettyProjection.Spherical.inner_Q_Q line 386
  31. lemma OAI.PettyProjection.Spherical.inner_Q_Q_of_degree_two_zero line 393
  32. lemma OAI.PettyProjection.Spherical.sign_spectral_estimate line 402
  33. def OAI.PettyProjection.Spherical.radialField line 426
  34. def OAI.PettyProjection.Spherical.tangentField line 427
  35. def OAI.PettyProjection.Spherical.signField line 429
  36. lemma OAI.PettyProjection.Spherical.radialField_continuous line 432
  37. lemma OAI.PettyProjection.Spherical.tangentField_continuous line 435
  38. lemma OAI.PettyProjection.Spherical.signedPair_radial_radial line 438
  39. lemma OAI.PettyProjection.Spherical.signedPair_tangent_radial line 454
  40. lemma OAI.PettyProjection.Spherical.signedPair_tangent_tangent line 474
  41. lemma OAI.PettyProjection.Spherical.signField_continuous line 507
  42. lemma OAI.PettyProjection.Spherical.signedPair_fields line 511
  43. lemma OAI.PettyProjection.Spherical.sign_form_estimate line 542