OAI/MathematicalPhysics/NavierStokes/BalancedTransport/RhoAlgorithms.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BalancedTransport.Effectivity.rhoCoeffStep line 12
  2. def OAI.BalancedTransport.Effectivity.rhoCoeffs line 16
  3. lemma OAI.BalancedTransport.Effectivity.primrec_rhoCoeffStep line 20
  4. lemma OAI.BalancedTransport.Effectivity.primrec_rhoCoeffs line 33
  5. lemma OAI.BalancedTransport.Effectivity.getD_zero_of_length_le line 44
  6. lemma OAI.BalancedTransport.Effectivity.rhoCoeffStep_getD line 49
  7. lemma OAI.BalancedTransport.Effectivity.rhoCoeffs_spec line 60
  8. lemma OAI.BalancedTransport.Effectivity.rhoCoeffs_length line 75
  9. lemma OAI.BalancedTransport.Effectivity.rhoPolynomial_coeff_zero line 81
  10. lemma OAI.BalancedTransport.Effectivity.rhoPolynomial_support_subset line 85
  11. def OAI.BalancedTransport.Effectivity.rhoBound line 92
  12. lemma OAI.BalancedTransport.Effectivity.primrec_sum_range_nat line 96
  13. lemma OAI.BalancedTransport.Effectivity.primrec_rhoBound line 110
  14. lemma OAI.BalancedTransport.Effectivity.rhoBound_eq line 121
  15. lemma OAI.BalancedTransport.Effectivity.rhoJet_bound_computable line 129
  16. def OAI.BalancedTransport.Effectivity.rhoPolyValue line 133
  17. lemma OAI.BalancedTransport.Effectivity.computable_rhoPolyValue line 136
  18. lemma OAI.BalancedTransport.Effectivity.rhoPolyValue_cast line 146
  19. lemma OAI.BalancedTransport.Effectivity.rat_abs_le_num line 157
  20. def OAI.BalancedTransport.Effectivity.rhoApprox line 169
  21. lemma OAI.BalancedTransport.Effectivity.computable_rhoApprox line 173
  22. lemma OAI.BalancedTransport.Effectivity.rhoApprox_spec line 184
  23. lemma OAI.BalancedTransport.Effectivity.rhoJet_lipschitz line 198