OAI/MathematicalPhysics/NavierStokes/BalancedTransport/FlatBounds.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BalancedTransport.Effectivity.rhoPolynomial line 9
  2. def OAI.BalancedTransport.Effectivity.rhoWeight line 13
  3. def OAI.BalancedTransport.Effectivity.rhoJet line 16
  4. lemma OAI.BalancedTransport.Effectivity.rhoJet_zero line 19
  5. lemma OAI.BalancedTransport.Effectivity.rhoJet_hasDerivAt line 22
  6. lemma OAI.BalancedTransport.Effectivity.rhoJet_contDiff line 30
  7. lemma OAI.BalancedTransport.Effectivity.rhoJet_eq_iteratedDeriv line 36
  8. lemma OAI.BalancedTransport.Effectivity.rhoJet_zero_of_nonpos line 43
  9. lemma OAI.BalancedTransport.Effectivity.inv_pow_mul_rho_le line 46
  10. lemma OAI.BalancedTransport.Effectivity.polynomial_rho_seam_bound line 61
  11. lemma OAI.BalancedTransport.Effectivity.rhoJet_bound line 82
  12. lemma OAI.BalancedTransport.Effectivity.rhoJet_seam_bound line 88
  13. lemma OAI.BalancedTransport.Effectivity.transition_denom_lower line 96
  14. def OAI.BalancedTransport.Effectivity.transitionWeight line 115
  15. def OAI.BalancedTransport.Effectivity.transitionDenom line 124
  16. lemma OAI.BalancedTransport.Effectivity.transitionDenom_contDiff line 126
  17. lemma OAI.BalancedTransport.Effectivity.transitionDenom_jet_bound line 130
  18. lemma OAI.BalancedTransport.Effectivity.transition_mul_denom line 148
  19. lemma OAI.BalancedTransport.Effectivity.transition_jet_bound line 152