OAI/Geometry/SmoothYau/Estimates/LpInverseGramFstContraction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.YauCounterexamples.gram_mul_repr line 38
2. lemma OAI.YauCounterexamples.inverse_gram_inner line 47
3. theorem OAI.YauCounterexamples.inverse_gram_contraction line 53
4. lemma OAI.YauCounterexamples.inverse_gram_trace line 68
5. lemma OAI.YauCounterexamples.lp_inverse_gram_fst_contraction line 83
6. lemma OAI.YauCounterexamples.lp_inverse_gram_snd_contraction line 87
7. lemma OAI.YauCounterexamples.lp_inverse_gram_mixed_contraction line 91
8. lemma OAI.YauCounterexamples.lp_inverse_gram_fst_trace line 95
9. lemma OAI.YauCounterexamples.lp_inverse_gram_snd_trace line 120