OAI/Analysis/CoulombIonization/Variational/TensorLp.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.memLp_tensor_of_aemeasurable line 111
  2. lemma OAI.CoulombAtom.memLp_tensor_of_sfinite_right line 166
  3. lemma OAI.CoulombAtom.not_aemeasurable_count_restrict_prodMk line 171
  4. lemma OAI.CoulombAtom.not_memLp_tensor_count_restrict_of_choice line 204
  5. lemma OAI.CoulombAtom.volume_prod_eq_choice_of_not_aemeasurable line 233
  6. lemma OAI.CoulombAtom.memLp_tensor_iff_choice line 247
  7. lemma OAI.CoulombAtom.memLp_tensor line 271

    Source documentation

    Right s-finiteness makes the product kernel measurable, so L² factors have an L² tensor. Without an a.e. measurable kernel, Mathlib's product uses an arbitrary chosen measure, whose integrability is characterized by memLp_tensor_iff_choice, not guaranteed by the factors. The finite-dimensional Haar hypotheses in the applications imply right s-finiteness.

    lemma memLp_tensor {f : E → ℂ} {g : F → ℂ} (hf : MemLp f 2) (hg : MemLp g 2) :
    MemLp (fun point : E × F => f point.1 * g point.2) 2 :=
…
  8. lemma OAI.CoulombAtom.integral_tensor_sq line 275
  9. lemma OAI.CoulombAtom.lineDeriv_slice_left line 294
  10. lemma OAI.CoulombAtom.IsWeakDerivative.tensor_left line 305
  11. lemma OAI.CoulombAtom.IsWeakDerivative.tensor_right line 330
  12. def OAI.CoulombAtom.leftList line 349
  13. def OAI.CoulombAtom.rightList line 351
  14. lemma OAI.CoulombAtom.leftList_join line 354
  15. lemma OAI.CoulombAtom.rightList_join line 356
  16. lemma OAI.CoulombAtom.join_list_parts line 358
  17. lemma OAI.CoulombAtom.configurationJoin_symm_apply line 366
  18. lemma OAI.CoulombAtom.configurationJoin_symm_preserving line 371
  19. lemma OAI.CoulombAtom.configurationJoin_direction_right line 376
  20. def OAI.CoulombAtom.tensorForm line 389
  21. lemma OAI.CoulombAtom.tensorForm_value_join line 396
  22. lemma OAI.CoulombAtom.tensorForm_gradient_left line 401
  23. lemma OAI.CoulombAtom.tensorForm_gradient_right line 408
  24. lemma OAI.CoulombAtom.SobolevVector.tensor line 415
  25. lemma OAI.CoulombAtom.formMass_tensor line 452