OAI/Geometry/SplitTangent/BracketIntegrability.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

Bracket Integrability.

  1. abbrev OAI.SplitTangent.TangentSplitting.Field line 23
  2. def OAI.SplitTangent.TangentSplitting.projectField line 25
  3. def OAI.SplitTangent.TangentSplitting.complementAt line 28
  4. theorem OAI.SplitTangent.TangentSplitting.complementAt_apply line 31
  5. theorem OAI.SplitTangent.TangentSplitting.complementAt_projector line 34
  6. theorem OAI.SplitTangent.TangentSplitting.projectField_add line 38
  7. theorem OAI.SplitTangent.TangentSplitting.projectField_smul line 42
  8. theorem OAI.SplitTangent.TangentSplitting.mdifferentiableAt_projectField line 46
  9. def OAI.SplitTangent.TangentSplitting.bracketOperation line 57
  10. theorem OAI.SplitTangent.TangentSplitting.bracketOperation_tensorial_left line 61
  11. theorem OAI.SplitTangent.TangentSplitting.bracketOperation_tensorial_right line 73
  12. def OAI.SplitTangent.TangentSplitting.bracketTensor line 87
  13. theorem OAI.SplitTangent.TangentSplitting.bracketTensor_apply line 92
  14. theorem OAI.SplitTangent.TangentSplitting.mem_first_iff line 102
  15. theorem OAI.SplitTangent.TangentSplitting.mem_first_iff_complement_eq_zero line 108
  16. theorem OAI.SplitTangent.TangentSplitting.holomorphicSectionOn_projectField line 112
  17. theorem OAI.SplitTangent.TangentSplitting.integrable_first_of_bracketTensor_eq_zero line 118
  18. theorem OAI.SplitTangent.TangentSplitting.bracketTensor_eq_zero_of_integrable_first line 138
  19. theorem OAI.SplitTangent.TangentSplitting.integrable_first_iff_bracketTensor_eq_zero line 161
  20. theorem OAI.SplitTangent.TangentSplitting.holomorphicSectionOn_bracketOperation line 167
  21. theorem OAI.SplitTangent.TangentSplitting.holomorphicSectionOn_bracketTensor_apply line 185
  22. theorem OAI.SplitTangent.TangentSplitting.range_complementAt line 196
  23. theorem OAI.SplitTangent.TangentSplitting.ker_complementAt line 208
  24. theorem OAI.SplitTangent.TangentSplitting.holomorphic_complement line 213
  25. def OAI.SplitTangent.TangentSplitting.swap line 237
  26. theorem OAI.SplitTangent.TangentSplitting.swap_first line 252
  27. theorem OAI.SplitTangent.TangentSplitting.swap_second line 255
  28. theorem OAI.SplitTangent.TangentSplitting.integrable_both_iff_bracketTensors_eq_zero line 260
  29. theorem OAI.SplitTangent.AnalyticContinuation.eq_univ_of_local_analytic_zero_locus line 276
  30. theorem OAI.SplitTangent.TangentSplitting.bracketTensor_local_analytic_zero_locus line 315
  31. theorem OAI.SplitTangent.TangentSplitting.bracketTensor_eq_zero_of_open line 378
  32. structure OAI.SplitTangent.RationalFamily line 396
  33. structure OAI.SplitTangent.CurveTangentSection line 407
  34. def OAI.SplitTangent.RationalFamily.curve line 421
  35. def OAI.SplitTangent.RationalFamily.parameterDerivative line 430
  36. lemma OAI.SplitTangent.RationalFamily.parameterDerivative_eq line 434
  37. lemma OAI.SplitTangent.RationalFamily.parameterDerivative_holomorphic line 447
  38. def OAI.SplitTangent.RationalFamily.derivativeSection line 474
  39. def OAI.SplitTangent.RationalFamily.twoPointEvaluation line 485
  40. lemma OAI.SplitTangent.RationalFamily.twoPointEvaluation_holomorphic line 488
  41. lemma OAI.SplitTangent.RationalFamily.twoPointEvaluation_derivative line 494
  42. theorem OAI.SplitTangent.RationalFamily.exists_section_endpoints line 509
  43. def OAI.SplitTangent.CurveTangentSection.project line 525
  44. lemma OAI.SplitTangent.CurveTangentSection.project_mem_first_finite line 532
  45. lemma OAI.SplitTangent.CurveTangentSection.project_mem_first_infinity line 535
  46. theorem OAI.SplitTangent.RationalFamily.exists_first_section_zero_value line 545
  47. lemma OAI.SplitTangent.TangentSplitting.localFrame_sum line 568
  48. lemma OAI.SplitTangent.TangentSplitting.bracketTensor_holomorphic_along line 579
  49. def OAI.SplitTangent.CurveTangentSection.bracket line 639
  50. theorem OAI.SplitTangent.twoChart_holomorphic_constant line 654
  51. def OAI.SplitTangent.RationalCurve.constant line 668
  52. theorem OAI.SplitTangent.CurveTangentSection.constant_finite line 679
  53. lemma OAI.SplitTangent.TangentSplitting.bracketTensor_projectors line 706
  54. lemma OAI.SplitTangent.TangentSplitting.complementAt_bracketTensor line 724
  55. structure OAI.SplitTangent.CurveBundleMap line 739
  56. def OAI.SplitTangent.CurveBundleMap.mapSection line 756
  57. structure OAI.SplitTangent.NormalizedFactorTransport line 768
  58. theorem OAI.SplitTangent.RationalFamily.bracketTensor_zero_of_transport line 782
  59. theorem OAI.SplitTangent.RationalFamily.integrable_first_of_transport line 817
  60. lemma OAI.SplitTangent.map_nhds_eq_of_surjective_mfderiv line 839
  61. lemma OAI.SplitTangent.RationalFamily.endpoint_derivative_surjective line 881
  62. lemma OAI.SplitTangent.RationalFamily.endpoint_range_open line 893
  63. theorem OAI.SplitTangent.RationalFamily.integrable_first_of_submersive_transport line 909
  64. theorem OAI.SplitTangent.RationalFamily.integrable_both_of_submersive_transport line 924