OAI/Analysis/AffineBernstein/ParametricTransport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.variationConormal_mul line 13
2. lemma OAI.AffineBernstein.graphParamConormal_null line 21
3. lemma OAI.AffineBernstein.contDiffAt_graphParamVariation line 42
4. lemma OAI.AffineBernstein.parametricJacobian_det line 50
5. lemma OAI.AffineBernstein.eventually_uniform_compact_zero line 59
6. lemma OAI.AffineBernstein.eventually_graphVariation_positive line 73
7. def OAI.AffineBernstein.coordinateAffineVariationArea line 97
8. lemma OAI.AffineBernstein.coordinateAffineVariationArea_eq line 105