OAI/Analysis/CoulombIonization/Localization/WeightedMoments.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombObservation.weighted_pow_sum_le line 17
  2. lemma OAI.CoulombObservation.integral_weighted_pow_sum_le line 49
  3. def OAI.CoulombObservation.signFlip line 67
  4. def OAI.CoulombObservation.signFlipPi line 70
  5. lemma OAI.CoulombObservation.signFlip_preserving line 73
  6. lemma OAI.CoulombObservation.signFlipPi_preserving line 79
  7. lemma OAI.CoulombObservation.odd_signFlip line 85
  8. lemma OAI.CoulombObservation.even_moment_integrable_of_memLp line 89
  9. lemma OAI.CoulombObservation.coordinate_sum_even_integrable line 95
  10. lemma OAI.CoulombObservation.odd_coordinate_sum_moment_invariant line 103
  11. lemma OAI.CoulombObservation.integral_finite_swap line 122
  12. lemma OAI.CoulombObservation.integral_comp_preserving_of_measurable line 135
  13. theorem OAI.CoulombObservation.symmetric_directional_moment_le line 143