OAI/MathematicalPhysics/RapidForcing/Uniqueness.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RapidForcing.spaceD line 10
  2. lemma OAI.RapidForcing.spaceD_sub line 13
  3. lemma OAI.RapidForcing.spaceD_contDiff line 19
  4. lemma OAI.RapidForcing.spaceD_coordinate line 23
  5. lemma OAI.RapidForcing.spaceD_smul line 27
  6. lemma OAI.RapidForcing.memLp_coordinate line 33
  7. lemma OAI.RapidForcing.memLp_inner_integrable line 37
  8. lemma OAI.RapidForcing.memLp_mul_integrable line 44
  9. lemma OAI.RapidForcing.memLp_smul_bounded line 50
  10. lemma OAI.RapidForcing.memLp_smul_l2_bounded line 57
  11. lemma OAI.RapidForcing.integral_inner_spaceD line 66
  12. lemma OAI.RapidForcing.integral_mul_spaceD line 75
  13. lemma OAI.RapidForcing.inner_basis line 84
  14. lemma OAI.RapidForcing.inner_basis_left line 87
  15. lemma OAI.RapidForcing.sum_basis line 90
  16. lemma OAI.RapidForcing.spaceD_sum line 94
  17. lemma OAI.RapidForcing.integral_laplace_dissipation line 100
  18. lemma OAI.RapidForcing.integral_pressure_orthogonal line 113
  19. lemma OAI.RapidForcing.integral_transport_zero line 135
  20. lemma OAI.RapidForcing.memLp_drift line 194
  21. lemma OAI.RapidForcing.integral_drift_bound line 204
  22. lemma OAI.RapidForcing.spatial_energy_bound line 222