OAI/Geometry/SmoothYau/Smoothness/CoordinateMetricFlux.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.YauCounterexamples.coordinateMetricFlux line 41
2. def OAI.YauCounterexamples.coordinateMetricLaplacian line 45
3. def OAI.YauCounterexamples.pullbackMetricMatrix line 49
4. lemma OAI.YauCounterexamples.pullbackMetricMatrix_density line 54
5. lemma OAI.YauCounterexamples.pullbackMetricMatrix_inverse_left line 65
6. lemma OAI.YauCounterexamples.mixed_fderiv_comp_scalar line 77
7. lemma OAI.YauCounterexamples.coordinateMetricFlux_pullback line 88
8. lemma OAI.YauCounterexamples.differentiableAt_coordinateMetricFlux line 114
9. theorem OAI.YauCounterexamples.coordinateMetricLaplacian_pullback line 130