OAI/Analysis/RecursivePotentials/JoinedGeometry.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RecursivePotentials.FiniteRootedTree.descEnergy line 18
  2. lemma OAI.RecursivePotentials.FiniteRootedTree.descEnergy_eq line 23
  3. lemma OAI.RecursivePotentials.FiniteRootedTree.descEnergy_nonneg line 27
  4. lemma OAI.RecursivePotentials.FiniteRootedTree.descEnergy_root line 33
  5. lemma OAI.RecursivePotentials.FiniteRootedTree.max_fields_le line 39
  6. lemma OAI.RecursivePotentials.FiniteRootedTree.max_fields_square_le line 58
  7. lemma OAI.RecursivePotentials.FiniteRootedTree.weighted_sum_children line 93
  8. lemma OAI.RecursivePotentials.FiniteRootedTree.upper_sum_square_le line 113
  9. lemma OAI.RecursivePotentials.FiniteRootedTree.block_square_comparison line 138
  10. lemma OAI.RecursivePotentials.isReflexive_iff line 172
  11. lemma OAI.RecursivePotentials.IsReflexive.of_equiv line 182
  12. lemma OAI.RecursivePotentials.hilbert_isReflexive line 200
  13. lemma OAI.RecursivePotentials.SquareSum.pairing_apply line 223
  14. lemma OAI.RecursivePotentials.SquareSum.pairing_single_right line 228
  15. lemma OAI.RecursivePotentials.SquareSum.pairing_single_left line 236
  16. def OAI.RecursivePotentials.SquareSum.restrictAt line 245
  17. lemma OAI.RecursivePotentials.SquareSum.restrictAt_apply line 248
  18. lemma OAI.RecursivePotentials.SquareSum.exists_half_norming line 251
  19. lemma OAI.RecursivePotentials.SquareSum.restriction_square_bound line 266
  20. lemma OAI.RecursivePotentials.SquareSum.restriction_mem line 313
  21. def OAI.RecursivePotentials.SquareSum.restrict line 318
  22. lemma OAI.RecursivePotentials.SquareSum.restrict_apply line 320
  23. lemma OAI.RecursivePotentials.SquareSum.restrict_norm line 323
  24. lemma OAI.RecursivePotentials.SquareSum.pairing_restrict line 328
  25. theorem OAI.RecursivePotentials.SquareSum.isReflexive line 334
  26. lemma OAI.RecursivePotentials.IsReflexive.prod line 369
  27. lemma OAI.RecursivePotentials.SquareSum.closedSubmodule_eq_top line 399
  28. lemma OAI.RecursivePotentials.SquareSum.denseRange_of_single line 406
  29. lemma OAI.RecursivePotentials.TreeVector.toSquareLinear_norm_sq line 427
  30. lemma OAI.RecursivePotentials.TreeVector.toSquareLinear_single line 434
  31. lemma OAI.RecursivePotentials.TreeVector.toSquareLinear_apply line 440
  32. lemma OAI.RecursivePotentials.TreeVector.block_square_comparison line 447
  33. lemma OAI.RecursivePotentials.TreeVector.hilbert_comparisons line 469
  34. def OAI.RecursivePotentials.TreeVector.toSquare line 496
  35. lemma OAI.RecursivePotentials.TreeVector.toSquare_dense line 501
  36. def OAI.RecursivePotentials.TreeSpace.hilbertEquiv line 517
  37. theorem OAI.RecursivePotentials.TreeSpace.finite_height_isReflexive line 523
  38. abbrev OAI.RecursivePotentials.Joined.Component line 536
  39. abbrev OAI.RecursivePotentials.Joined.Outer line 538
  40. def OAI.RecursivePotentials.Joined.embed line 540
  41. lemma OAI.RecursivePotentials.Joined.embed_apply line 544
  42. lemma OAI.RecursivePotentials.Joined.embed_ne_root line 546
  43. lemma OAI.RecursivePotentials.Joined.embed_parent line 549
  44. lemma OAI.RecursivePotentials.Joined.embed_root_parent line 556
  45. def OAI.RecursivePotentials.Joined.rootEmbed line 559
  46. lemma OAI.RecursivePotentials.Joined.root_child line 566
  47. lemma OAI.RecursivePotentials.Joined.component_child line 581
  48. lemma OAI.RecursivePotentials.Joined.upper_pull line 600
  49. def OAI.RecursivePotentials.Joined.partLinear line 610
  50. lemma OAI.RecursivePotentials.Joined.partLinear_apply line 615
  51. lemma OAI.RecursivePotentials.Joined.part_potentials_le line 618
  52. lemma OAI.RecursivePotentials.Joined.part_square_bound line 629
  53. lemma OAI.RecursivePotentials.Joined.parts_mem line 664
  54. def OAI.RecursivePotentials.Joined.components line 670
  55. lemma OAI.RecursivePotentials.Joined.components_apply line 673
  56. lemma OAI.RecursivePotentials.Joined.components_norm_le line 676
  57. def OAI.RecursivePotentials.Joined.componentsLinear line 681
  58. def OAI.RecursivePotentials.Joined.componentsMap line 692
  59. def OAI.RecursivePotentials.Joined.field line 697
  60. lemma OAI.RecursivePotentials.Joined.field_root line 701
  61. lemma OAI.RecursivePotentials.Joined.field_embed line 704
  62. lemma OAI.RecursivePotentials.Joined.field_nonneg line 707
  63. lemma OAI.RecursivePotentials.Joined.field_upper line 713
  64. lemma OAI.RecursivePotentials.Joined.part_squares_le_outer line 742
  65. lemma OAI.RecursivePotentials.Joined.part_field_squares_le_outer line 747
  66. def OAI.RecursivePotentials.Joined.liftP line 758
  67. def OAI.RecursivePotentials.Joined.liftQ line 762
  68. lemma OAI.RecursivePotentials.Joined.liftP_nonneg line 766
  69. lemma OAI.RecursivePotentials.Joined.liftQ_nonneg line 769
  70. lemma OAI.RecursivePotentials.Joined.lift_difference line 772
  71. lemma OAI.RecursivePotentials.Joined.lifts_upper line 783
  72. lemma OAI.RecursivePotentials.Joined.potentials_le_lifts line 797
  73. lemma OAI.RecursivePotentials.Joined.component_potentials line 802
  74. lemma OAI.RecursivePotentials.Joined.norm_le_root_add_outer line 809
  75. def OAI.RecursivePotentials.Joined.put line 823
  76. lemma OAI.RecursivePotentials.Joined.put_root line 826
  77. lemma OAI.RecursivePotentials.Joined.part_put_same line 831
  78. lemma OAI.RecursivePotentials.Joined.part_put_other line 836
  79. lemma OAI.RecursivePotentials.Joined.components_put line 845
  80. def OAI.RecursivePotentials.Joined.rootVector line 854
  81. lemma OAI.RecursivePotentials.Joined.components_rootVector line 856
  82. def OAI.RecursivePotentials.Joined.splitting line 869
  83. lemma OAI.RecursivePotentials.Joined.splitting_apply line 872
  84. lemma OAI.RecursivePotentials.Joined.norm_le_splitting line 875
  85. lemma OAI.RecursivePotentials.Joined.splitting_put line 882
  86. lemma OAI.RecursivePotentials.Joined.splitting_rootVector line 886
  87. lemma OAI.RecursivePotentials.Joined.splitting_dense line 891
  88. def OAI.RecursivePotentials.Joined.freeEquiv line 916
  89. lemma OAI.RecursivePotentials.Joined.components_reflexive line 919
  90. theorem OAI.RecursivePotentials.Joined.outer_isReflexive line 922
  91. theorem OAI.RecursivePotentials.XJoined_isReflexive line 928
  92. def OAI.RecursivePotentials.Joined.zeroComponents line 937
  93. lemma OAI.RecursivePotentials.Joined.zero_norm_le_components line 940
  94. def OAI.RecursivePotentials.Joined.zeroPut line 947
  95. lemma OAI.RecursivePotentials.Joined.zeroComponents_zeroPut line 950
  96. lemma OAI.RecursivePotentials.Joined.zeroComponents_dense line 953
  97. def OAI.RecursivePotentials.Joined.zeroEquiv line 966
  98. theorem OAI.RecursivePotentials.XZero_isReflexive line 975
  99. lemma OAI.RecursivePotentials.logarithmicGamma_pos line 979
  100. lemma OAI.RecursivePotentials.logarithmicGamma_le line 985
  101. theorem OAI.RecursivePotentials.FiniteRootedTree.logarithmic_propagation line 1018
  102. theorem OAI.RecursivePotentials.TreeSpace.logarithmic_tail_gap line 1052
  103. lemma OAI.RecursivePotentials.finite_dimensional_image_close_pair line 1082
  104. theorem OAI.RecursivePotentials.TreeSpace.averaged_modulus_all_radii_lower line 1105
  105. theorem OAI.RecursivePotentials.TreeSpace.averaged_modulus_pos line 1132
  106. lemma OAI.RecursivePotentials.norm_center_le line 1145
  107. lemma OAI.RecursivePotentials.norm_perturbation_le line 1152
  108. lemma OAI.RecursivePotentials.lens_half_difference line 1157
  109. theorem OAI.RecursivePotentials.TreeSpace.separated_midpoint_families line 1179
  110. theorem OAI.RecursivePotentials.XJoined_separated_families line 1250