OAI/Geometry/SmoothYau/Smoothness/ContinuousCompactSmoothJets.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.metricMatrixFormCLM line 33
  2. lemma OAI.YauCounterexamples.metricMatrixFormCLM_apply line 44
  3. lemma OAI.YauCounterexamples.matrix_fderiv_norm_le line 48
  4. theorem OAI.YauCounterexamples.metricMatrixForm_first_jet_bound line 64
  5. abbrev OAI.YauCounterexamples.HessianJetData line 124
  6. def OAI.YauCounterexamples.christoffelFromJet line 130
  7. def OAI.YauCounterexamples.metricHessianFromFullJet line 134
  8. lemma OAI.YauCounterexamples.continuous_coordinateKoszul line 137
  9. lemma OAI.YauCounterexamples.continuousAt_metricHessianFromFullJet line 143
  10. def OAI.YauCounterexamples.metricScalarJet line 156
  11. lemma OAI.YauCounterexamples.metricHessianFromFullJet_metricScalarJet line 160
  12. lemma OAI.YauCounterexamples.continuous_metricScalarJet line 164
  13. def OAI.YauCounterexamples.hessianJetMarginSet line 171
  14. lemma OAI.YauCounterexamples.metricScalarJet_margin_interior line 174
  15. lemma OAI.YauCounterexamples.dist_metricScalarJet_lt line 185
  16. lemma OAI.YauCounterexamples.compact_map_uniform_interior line 197
  17. theorem OAI.YauCounterexamples.compact_hessianMargins_stability line 209
  18. lemma OAI.YauCounterexamples.sphere_metricCoefficients_smooth line 253
  19. theorem OAI.YauCounterexamples.sphere_metric_first_jet_neighborhood line 262
  20. theorem OAI.YauCounterexamples.sphericalBaseProfile_neighborhood line 303
  21. lemma OAI.YauCounterexamples.IsSmoothNeighborhood.mono line 354
  22. lemma OAI.YauCounterexamples.IsSmoothNeighborhood.inter line 361
  23. lemma OAI.YauCounterexamples.chartMetricForm_domination_transfer line 374
  24. lemma OAI.YauCounterexamples.small_bilinear_difference_domination line 394
  25. def OAI.YauCounterexamples.sphericalHalf line 410
  26. lemma OAI.YauCounterexamples.sphericalHalf_compact line 413
  27. lemma OAI.YauCounterexamples.sphericalHalf_in_source line 416
  28. lemma OAI.YauCounterexamples.sphericalHalves_cover line 427
  29. lemma OAI.YauCounterexamples.sphericalHalf_domination_neighborhood line 433
  30. theorem OAI.YauCounterexamples.spherical_domination_neighborhood line 448
  31. lemma OAI.YauCounterexamples.matrix_iteratedFDeriv_norm_le line 466
  32. lemma OAI.YauCounterexamples.metricMatrixForm_iterated_jet_bound line 494
  33. lemma OAI.YauCounterexamples.continuous_compactSmooth_of_jets line 514
  34. lemma OAI.YauCounterexamples.ContinuousSmoothFamilyOn.pi line 545
  35. lemma OAI.YauCounterexamples.continuous_chartTensorOfMetric line 566