OAI/MathematicalPhysics/NavierStokes/BalancedTransport/EnergyCurve.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BalancedTransport.Analysis.coordinateL2 line 10
2. lemma OAI.BalancedTransport.Analysis.coordinateL2_coe line 14
3. lemma OAI.BalancedTransport.Analysis.coordinateL2_hasDerivWithinAt line 18
4. def OAI.BalancedTransport.Analysis.l2Energy line 24
5. def OAI.BalancedTransport.Analysis.l2EnergyRate line 27
6. lemma OAI.BalancedTransport.Analysis.l2Energy_nonneg line 30
7. lemma OAI.BalancedTransport.Analysis.l2Energy_continuous line 33
8. lemma OAI.BalancedTransport.Analysis.l2Energy_hasDerivWithinAt line 37
9. lemma OAI.BalancedTransport.Analysis.l2Inner_integral line 45
10. lemma OAI.BalancedTransport.Analysis.l2Energy_integral line 55
11. lemma OAI.BalancedTransport.Analysis.l2Energy_eq_zero_of_bound line 64
12. lemma OAI.BalancedTransport.Analysis.l2Energy_zero_pointwise line 86