OAI/Analysis/RecursivePotentials/TreeGeometry.lean

GitHub source file

121 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RecursivePotentials.leastPair_tight line 13
  2. lemma OAI.RecursivePotentials.energy_nonneg line 19
  3. lemma OAI.RecursivePotentials.energy_symm line 24
  4. lemma OAI.RecursivePotentials.energy_factor line 29
  5. lemma OAI.RecursivePotentials.holder_two_thirds line 37
  6. lemma OAI.RecursivePotentials.energy_step_first line 61
  7. lemma OAI.RecursivePotentials.energy_step line 107
  8. lemma OAI.RecursivePotentials.energy_zero_base line 122
  9. lemma OAI.RecursivePotentials.sq_rpow_three_halves line 128
  10. lemma OAI.RecursivePotentials.energy_rpow_three_halves line 133
  11. lemma OAI.RecursivePotentials.cube_le_of_sq_le_energy line 139
  12. def OAI.RecursivePotentials.FiniteRootedTree.leaves line 155
  13. lemma OAI.RecursivePotentials.FiniteRootedTree.sum_children line 157
  14. lemma OAI.RecursivePotentials.FiniteRootedTree.sum_leaves_le_root line 178
  15. theorem OAI.RecursivePotentials.FiniteRootedTree.two_field_energy_all_leaves line 193
  16. theorem OAI.RecursivePotentials.FiniteRootedTree.two_field_energy line 227
  17. lemma OAI.RecursivePotentials.FiniteRootedTree.fields_tight line 240
  18. lemma OAI.RecursivePotentials.FiniteRootedTree.fields_zero line 253
  19. lemma OAI.RecursivePotentials.FiniteRootedTree.Upper.add line 260
  20. lemma OAI.RecursivePotentials.FiniteRootedTree.Upper.smul line 265
  21. lemma OAI.RecursivePotentials.FiniteRootedTree.fields_add_le line 271
  22. lemma OAI.RecursivePotentials.FiniteRootedTree.fields_neg line 289
  23. lemma OAI.RecursivePotentials.FiniteRootedTree.fields_smul_le line 301
  24. lemma OAI.RecursivePotentials.FiniteRootedTree.fields_smul line 314
  25. def OAI.RecursivePotentials.FiniteRootedTree.rootSum line 328
  26. lemma OAI.RecursivePotentials.FiniteRootedTree.rootSum_nonneg line 331
  27. lemma OAI.RecursivePotentials.FiniteRootedTree.rootSum_zero line 334
  28. lemma OAI.RecursivePotentials.FiniteRootedTree.rootSum_neg line 337
  29. lemma OAI.RecursivePotentials.FiniteRootedTree.rootSum_add_le line 340
  30. lemma OAI.RecursivePotentials.FiniteRootedTree.rootSum_smul_nonneg line 345
  31. lemma OAI.RecursivePotentials.FiniteRootedTree.Initial.child_not_mem line 349
  32. theorem OAI.RecursivePotentials.FiniteRootedTree.fields_eq_off_head line 356
  33. lemma OAI.RecursivePotentials.FiniteRootedTree.fields_head_zero line 372
  34. def OAI.RecursivePotentials.FiniteRootedTree.defect line 376
  35. lemma OAI.RecursivePotentials.FiniteRootedTree.averaged_feasible line 379
  36. lemma OAI.RecursivePotentials.FiniteRootedTree.defect_representation line 392
  37. lemma OAI.RecursivePotentials.FiniteRootedTree.defect_nonneg line 404
  38. lemma OAI.RecursivePotentials.FiniteRootedTree.defect_energy_step line 418
  39. lemma OAI.RecursivePotentials.FiniteRootedTree.defect_off_head line 430
  40. lemma OAI.RecursivePotentials.FiniteRootedTree.max_fields_sq_le_children line 440
  41. theorem OAI.RecursivePotentials.FiniteRootedTree.tail_energy line 462
  42. lemma OAI.RecursivePotentials.FiniteRootedTree.rootSum_defect line 494
  43. lemma OAI.RecursivePotentials.FiniteRootedTree.rootSum_eq_twice_max_of_root_zero line 501
  44. theorem OAI.RecursivePotentials.FiniteRootedTree.rootSum_cubic line 508
  45. theorem OAI.RecursivePotentials.FiniteRootedTree.rootSum_finite_midpoint_gap line 528
  46. lemma OAI.RecursivePotentials.FiniteRootedTree.Upper.le_root line 546
  47. lemma OAI.RecursivePotentials.FiniteRootedTree.abs_coordinate_le_rootSum line 558
  48. lemma OAI.RecursivePotentials.FiniteRootedTree.rootSum_pos line 569
  49. def OAI.RecursivePotentials.FiniteRootedTree.rootCommon line 578
  50. lemma OAI.RecursivePotentials.FiniteRootedTree.rootCommon_eq_half_sum line 580
  51. theorem OAI.RecursivePotentials.FiniteRootedTree.commonRoot_finite_cubic line 587
  52. lemma OAI.RecursivePotentials.FiniteRootedTree.root_mem_ancestors line 638
  53. lemma OAI.RecursivePotentials.FiniteRootedTree.ancestors_subset_of_initial line 646
  54. lemma OAI.RecursivePotentials.FiniteRootedTree.ancestorClosure_subset_of_initial line 655
  55. theorem OAI.RecursivePotentials.FiniteRootedTree.potentials_on_head line 662
  56. lemma OAI.RecursivePotentials.FiniteRootedTree.P_eq_zero_off_head line 688
  57. lemma OAI.RecursivePotentials.FiniteRootedTree.Q_eq_zero_off_head line 693
  58. lemma OAI.RecursivePotentials.FiniteRootedTree.normSum_on_head line 698
  59. lemma OAI.RecursivePotentials.FiniteRootedTree.potentials_le_normSum line 703
  60. lemma OAI.RecursivePotentials.FiniteRootedTree.potentials_lipschitz line 712
  61. lemma OAI.RecursivePotentials.TreeVector.norm_def line 731
  62. lemma OAI.RecursivePotentials.TreeVector.coordinate_apply line 733
  63. lemma OAI.RecursivePotentials.TreeVector.lipschitz_P line 735
  64. lemma OAI.RecursivePotentials.TreeVector.lipschitz_Q line 741
  65. lemma OAI.RecursivePotentials.TreeVector.projection_apply line 747
  66. lemma OAI.RecursivePotentials.TreeVector.projection_idem line 750
  67. lemma OAI.RecursivePotentials.TreeSpace.coordinate_coe line 768
  68. lemma OAI.RecursivePotentials.TreeSpace.P_coe line 772
  69. lemma OAI.RecursivePotentials.TreeSpace.Q_coe line 775
  70. lemma OAI.RecursivePotentials.TreeSpace.continuous_P line 778
  71. lemma OAI.RecursivePotentials.TreeSpace.continuous_Q line 781
  72. lemma OAI.RecursivePotentials.TreeSpace.P_nonneg line 784
  73. lemma OAI.RecursivePotentials.TreeSpace.Q_nonneg line 789
  74. lemma OAI.RecursivePotentials.TreeSpace.P_sub_Q line 794
  75. theorem OAI.RecursivePotentials.TreeSpace.norm_eq line 801
  76. lemma OAI.RecursivePotentials.TreeSpace.abs_coordinate_le line 806
  77. lemma OAI.RecursivePotentials.TreeSpace.fields_lipschitz line 812
  78. lemma OAI.RecursivePotentials.TreeSpace.projection_coe line 828
  79. lemma OAI.RecursivePotentials.TreeSpace.projection_contracts line 832
  80. lemma OAI.RecursivePotentials.TreeSpace.projection_idem line 839
  81. lemma OAI.RecursivePotentials.TreeSpace.coordinate_projection line 845
  82. lemma OAI.RecursivePotentials.TreeSpace.tail_closed line 858
  83. theorem OAI.RecursivePotentials.TreeSpace.finite_tail_dense line 861
  84. lemma OAI.RecursivePotentials.FiniteRootedTree.restrict_initial line 888
  85. def OAI.RecursivePotentials.FiniteRootedTree.meanExcess line 897
  86. theorem OAI.RecursivePotentials.FiniteRootedTree.normSum_cubic line 900
  87. def OAI.RecursivePotentials.TreeSpace.meanExcess line 941
  88. lemma OAI.RecursivePotentials.TreeSpace.meanExcess_coe line 943
  89. lemma OAI.RecursivePotentials.TreeSpace.continuous_meanExcess line 949
  90. lemma OAI.RecursivePotentials.TreeSpace.meanExcess_nonneg line 954
  91. lemma OAI.RecursivePotentials.TreeSpace.meanExcess_le line 962
  92. theorem OAI.RecursivePotentials.TreeSpace.cubic_projected_tail line 968
  93. theorem OAI.RecursivePotentials.TreeSpace.cubic_tail line 986
  94. theorem OAI.RecursivePotentials.TreeSpace.finite_center_midpoint_gap line 995
  95. theorem OAI.RecursivePotentials.TreeSpace.homogeneous_cubic_tail line 1016
  96. def OAI.RecursivePotentials.TreeVector.ofHeadLinear line 1043
  97. def OAI.RecursivePotentials.TreeVector.ofHead line 1058
  98. lemma OAI.RecursivePotentials.TreeVector.ofHead_apply line 1061
  99. lemma OAI.RecursivePotentials.TreeVector.ofHead_support line 1066
  100. def OAI.RecursivePotentials.TreeVector.basisVector line 1073
  101. lemma OAI.RecursivePotentials.TreeVector.basisVector_apply line 1075
  102. lemma OAI.RecursivePotentials.TreeVector.not_finite_dimensional line 1078
  103. def OAI.RecursivePotentials.TreeSpace.headCoordinates line 1092
  104. lemma OAI.RecursivePotentials.TreeSpace.headCoordinates_apply line 1095
  105. theorem OAI.RecursivePotentials.TreeSpace.projection_reconstructs line 1098
  106. lemma OAI.RecursivePotentials.TreeSpace.tail_eq_coordinate_kernel line 1119
  107. theorem OAI.RecursivePotentials.TreeSpace.tail_finite_codimension line 1136
  108. theorem OAI.RecursivePotentials.TreeSpace.supported_is_finite line 1141
  109. theorem OAI.RecursivePotentials.TreeSpace.not_finite_dimensional line 1147
  110. def OAI.RecursivePotentials.CofiniteSubspace.top line 1161
  111. instance OAI.RecursivePotentials.CofiniteSubspace.(instance at line 1166) line 1166
  112. lemma OAI.RecursivePotentials.CofiniteSubspace.nontrivial_space line 1168
  113. lemma OAI.RecursivePotentials.CofiniteSubspace.exists_unit line 1175
  114. lemma OAI.RecursivePotentials.averagedGain_lower line 1187
  115. lemma OAI.RecursivePotentials.averagedInner_bddBelow line 1195
  116. lemma OAI.RecursivePotentials.averagedInner_nonempty line 1201
  117. lemma OAI.RecursivePotentials.averagedInner_le line 1207
  118. theorem OAI.RecursivePotentials.averagedModulus_lower_of_witness line 1219
  119. def OAI.RecursivePotentials.TreeSpace.cofiniteTail line 1253
  120. lemma OAI.RecursivePotentials.TreeSpace.finite_unit_dense line 1258
  121. theorem OAI.RecursivePotentials.TreeSpace.averaged_modulus_cubic line 1289