OAI/Analysis/HardSphere/Orbitals/FieldApply.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.L2Contraction.unifIntegrable_of_domination line 14
  2. lemma OAI.L2Contraction.tendsto_toLp_of_domination line 23
  3. lemma OAI.L2Contraction.field_memLp line 41
  4. def OAI.L2Contraction.fieldApply line 47
  5. lemma OAI.L2Contraction.coe_fieldApply line 50
  6. lemma OAI.L2Contraction.norm_fieldApply_le line 54
  7. lemma OAI.L2Contraction.fieldApply_sub line 60
  8. lemma OAI.L2Contraction.norm_fieldApply_sub_le line 68
  9. lemma OAI.L2Contraction.coeff_meas line 76
  10. lemma OAI.L2Contraction.tendsto_fieldApply_fixed line 80
  11. lemma OAI.L2Contraction.tendsto_fieldApply line 96
  12. structure OAI.HardSphere.SmoothContraction line 119
  13. lemma OAI.HardSphere.SmoothContraction.lipschitz line 128
  14. lemma OAI.HardSphere.SmoothContraction.derivative_continuous line 132
  15. lemma OAI.HardSphere.SmoothContraction.coordDerivative_comp line 135
  16. def OAI.HardSphere.SmoothContraction.composeTest line 148
  17. def OAI.HardSphere.SmoothContraction.onScalar line 167
  18. def OAI.HardSphere.SmoothContraction.onPartial line 170
  19. def OAI.HardSphere.SmoothContraction.onJet line 175
  20. lemma OAI.HardSphere.SmoothContraction.coe_onScalar line 178
  21. lemma OAI.HardSphere.SmoothContraction.coe_onPartial line 181
  22. lemma OAI.HardSphere.SmoothContraction.jet_composeTest line 185
  23. lemma OAI.HardSphere.SmoothContraction.onJet_mem_domain line 207
  24. lemma OAI.HardSphere.SmoothContraction.energy_onJet_le line 228