OAI/Analysis/NodalLength/MetricFamilies.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpNodal.Profiles.Elliptic.smooth_family_partial line 303
  2. lemma OAI.SharpNodal.Profiles.Elliptic.smooth_family_wordPartial line 310
  3. lemma OAI.SharpNodal.Profiles.Elliptic.wordPartial_zero line 317
  4. lemma OAI.SharpNodal.Profiles.Elliptic.uniform_family_small line 325
  5. lemma OAI.SharpNodal.Profiles.Elliptic.uniform_wordPartial_small line 338
  6. def OAI.SharpNodal.Profiles.Elliptic.metricCutoff line 346
  7. def OAI.SharpNodal.Profiles.Elliptic.flatCut line 348
  8. lemma OAI.SharpNodal.Profiles.Elliptic.good_flatCut line 351
  9. lemma OAI.SharpNodal.Profiles.Elliptic.smooth_flatCut_family line 357
  10. lemma OAI.SharpNodal.Profiles.Elliptic.flatCut_zero line 362
  11. lemma OAI.SharpNodal.Profiles.Elliptic.flatCut_inner line 365
  12. lemma OAI.SharpNodal.Profiles.Elliptic.exists_small_flatCut line 369
  13. lemma OAI.SharpNodal.Profiles.Elliptic.good_neg line 392
  14. lemma OAI.SharpNodal.Profiles.Elliptic.good_sum line 395
  15. def OAI.SharpNodal.Profiles.Elliptic.coeffs line 400
  16. def OAI.SharpNodal.Profiles.Elliptic.perturbation line 404
  17. lemma OAI.SharpNodal.Profiles.Elliptic.good_coeffs line 407
  18. lemma OAI.SharpNodal.Profiles.Elliptic.differential_coeffs line 412
  19. lemma OAI.SharpNodal.Profiles.Elliptic.coeffs_bounds line 423
  20. lemma OAI.SharpNodal.Profiles.Elliptic.good_l2_bound line 445
  21. lemma OAI.SharpNodal.Profiles.Elliptic.coeffs_source_bound line 449
  22. lemma OAI.SharpNodal.Profiles.Elliptic.operator_small line 459
  23. lemma OAI.SharpNodal.Profiles.Elliptic.smooth_coordinate line 470
  24. lemma OAI.SharpNodal.Profiles.Elliptic.coordPartial_coordinate line 473
  25. lemma OAI.SharpNodal.Profiles.Elliptic.laplacian_coordinate line 480
  26. lemma OAI.SharpNodal.Profiles.Elliptic.perturbation_coordinate_add line 488
  27. theorem OAI.SharpNodal.Profiles.Elliptic.small_metric_harmonic_coordinate line 500
  28. def OAI.SharpNodal.Profiles.Elliptic.oneForm line 551
  29. lemma OAI.SharpNodal.Profiles.Elliptic.smooth_oneForm line 554
  30. lemma OAI.SharpNodal.Profiles.Elliptic.fderiv_apply_coords line 558
  31. lemma OAI.SharpNodal.Profiles.Elliptic.fderiv_oneForm line 563
  32. lemma OAI.SharpNodal.Profiles.Elliptic.exists_smooth_primitive line 575
  33. def OAI.SharpNodal.Profiles.Elliptic.metricFlux line 590
  34. lemma OAI.SharpNodal.Profiles.Elliptic.smooth_metricFlux line 593
  35. lemma OAI.SharpNodal.Profiles.Elliptic.divergence_metricFlux line 597
  36. lemma OAI.SharpNodal.Profiles.Elliptic.metric_conjugate line 607
  37. lemma OAI.SharpNodal.Profiles.Elliptic.metricFlux_positive line 620
  38. def OAI.SharpNodal.Profiles.Elliptic.coordMap line 645
  39. lemma OAI.SharpNodal.Profiles.Elliptic.coordMap_zero line 648
  40. lemma OAI.SharpNodal.Profiles.Elliptic.coordMap_one line 649
  41. lemma OAI.SharpNodal.Profiles.Elliptic.smoothOn_coordMap line 651
  42. lemma OAI.SharpNodal.Profiles.Elliptic.hasFDerivAt_coordMap line 655
  43. lemma OAI.SharpNodal.Profiles.Elliptic.plane_clm_injective line 661
  44. lemma OAI.SharpNodal.Profiles.Elliptic.local_smooth_diffeomorph line 681
  45. lemma OAI.SharpNodal.Profiles.Elliptic.coordMap_injective_derivative line 703
  46. theorem OAI.SharpNodal.Profiles.Elliptic.normalized_metric_coordinates line 711