OAI/Geometry/SmoothYau/Smoothness/JointMetricDet.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.YauCounterexamples.joint_metricDet line 21
2. lemma OAI.YauCounterexamples.joint_metricDensity line 32
3. lemma OAI.YauCounterexamples.joint_metricInverse line 36
4. lemma OAI.YauCounterexamples.joint_metricFirstCoefficient line 54
5. lemma OAI.YauCounterexamples.contDiff_joint_cutoff line 75
6. lemma OAI.YauCounterexamples.tendsto_schwartz_family line 89
7. lemma OAI.YauCounterexamples.CompactMetricAtlas.metricCoefficientSchwartz_common_support line 112
8. lemma OAI.YauCounterexamples.CompactMetricAtlas.varyingCoefficientSchwartz_a_value line 117
9. lemma OAI.YauCounterexamples.CompactMetricAtlas.varyingCoefficientSchwartz_c_value line 127
10. theorem OAI.YauCounterexamples.CompactMetricAtlas.smoothFamily_varyingLaplacian_tendsto line 137