OAI/Geometry/SmoothYau/Limits/ScalarCauchyCross.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.YauCounterexamples.weightedLaplacian_congr_nhds line 42
2. lemma OAI.YauCounterexamples.weightedLaplacian_const line 71
3. lemma OAI.YauCounterexamples.coordinateGradientPair_cauchy line 75
4. lemma OAI.YauCounterexamples.conjugate_gradient_nonzero line 95
5. def OAI.YauCounterexamples.cutoffFactor line 123
6. lemma OAI.YauCounterexamples.cutoffFactor_pos line 126
7. theorem OAI.YauCounterexamples.cutoff_conductivity_exactification line 135
8. lemma OAI.YauCounterexamples.scalar_cauchy_cross line 272
9. lemma OAI.YauCounterexamples.coordinateGradientPair_mul_self_le line 278
10. lemma OAI.YauCounterexamples.annular_conjugate_gradient_lower line 296
11. theorem OAI.YauCounterexamples.roundPower_conjugate_gradient_lower line 331