OAI/Geometry/SmoothYau/Smoothness/CompactMetricAllJets.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.YauCounterexamples.scalar_composition_jet_bound_on line 42
2. theorem OAI.YauCounterexamples.sqrt_near_one_jet_bound line 68
3. lemma OAI.YauCounterexamples.near_one_product_jet_bound_on line 163
4. theorem OAI.YauCounterexamples.conductivity_response_jet_bound line 191
5. theorem OAI.YauCounterexamples.conductivity_response_all_jets line 301
6. lemma OAI.YauCounterexamples.conductivity_tensor_jet_bound_on line 372
7. theorem OAI.YauCounterexamples.conductivity_metric_realization_jets line 477
8. theorem OAI.YauCounterexamples.conductivity_metric_realization_uniform_all_jets line 572
9. lemma OAI.YauCounterexamples.compact_metric_all_jets line 697
10. theorem OAI.YauCounterexamples.conductivity_metric_in_smooth_neighborhood line 716