OAI/Analysis/RecursivePotentials/VariableEstimates.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RecursivePotentials.FiniteRootedTree.uniform_sequential_separation line 25
  2. lemma OAI.RecursivePotentials.ChildExponent.agg_le_iff line 63
  3. lemma OAI.RecursivePotentials.ChildExponent.agg_neg line 68
  4. lemma OAI.RecursivePotentials.FiniteRootedTree.pfields_tight line 82
  5. lemma OAI.RecursivePotentials.FiniteRootedTree.PUpper.zero line 89
  6. lemma OAI.RecursivePotentials.FiniteRootedTree.PUpper.add line 91
  7. lemma OAI.RecursivePotentials.FiniteRootedTree.PUpper.smul line 94
  8. lemma OAI.RecursivePotentials.FiniteRootedTree.PUpper.le_root line 98
  9. lemma OAI.RecursivePotentials.FiniteRootedTree.pfields_zero line 107
  10. lemma OAI.RecursivePotentials.FiniteRootedTree.pfields_add_le line 113
  11. lemma OAI.RecursivePotentials.FiniteRootedTree.pfields_neg line 125
  12. lemma OAI.RecursivePotentials.FiniteRootedTree.pfields_smul_le line 139
  13. lemma OAI.RecursivePotentials.FiniteRootedTree.pfields_smul line 149
  14. lemma OAI.RecursivePotentials.FiniteRootedTree.pRootSum_zero line 161
  15. lemma OAI.RecursivePotentials.FiniteRootedTree.pRootSum_neg line 162
  16. lemma OAI.RecursivePotentials.FiniteRootedTree.pRootSum_add_le line 165
  17. lemma OAI.RecursivePotentials.FiniteRootedTree.pRootSum_smul_nonneg line 168
  18. lemma OAI.RecursivePotentials.FiniteRootedTree.pRootSum_coordinate line 172
  19. lemma OAI.RecursivePotentials.FiniteRootedTree.pfields_eq_off_head line 180
  20. lemma OAI.RecursivePotentials.FiniteRootedTree.pfields_head_zero line 189
  21. lemma OAI.RecursivePotentials.FiniteRootedTree.pfields_head_le line 193
  22. lemma OAI.RecursivePotentials.VariableExponent.heightExponent_le_two line 218
  23. lemma OAI.RecursivePotentials.VariableExponent.heightExponent_pow_le_exp line 223
  24. def OAI.RecursivePotentials.VariableExponent.recurrenceCeiling line 232
  25. lemma OAI.RecursivePotentials.VariableExponent.recurrenceCeiling_one_le line 234
  26. lemma OAI.RecursivePotentials.VariableExponent.recurrenceCeiling_pos line 237
  27. lemma OAI.RecursivePotentials.VariableExponent.recurrence_coefficient_le line 239
  28. lemma OAI.RecursivePotentials.VariableExponent.accumulated_bound line 254
  29. lemma OAI.RecursivePotentials.VariableExponent.cubic_of_accumulated line 286
  30. def OAI.RecursivePotentials.FiniteRootedTree.firstExit line 333
  31. def OAI.RecursivePotentials.FiniteRootedTree.stoppedExit line 335
  32. def OAI.RecursivePotentials.FiniteRootedTree.exitCut line 337
  33. lemma OAI.RecursivePotentials.FiniteRootedTree.exitCut_zero line 339
  34. lemma OAI.RecursivePotentials.FiniteRootedTree.exitCut_succ line 348
  35. lemma OAI.RecursivePotentials.FiniteRootedTree.exitCut_succ_disjoint line 370
  36. lemma OAI.RecursivePotentials.FiniteRootedTree.headLevel_stopped_disjoint line 380
  37. lemma OAI.RecursivePotentials.FiniteRootedTree.sum_exitCut_succ line 386
  38. lemma OAI.RecursivePotentials.VariableExponent.rpow_increment_le line 398
  39. lemma OAI.RecursivePotentials.VariableExponent.holder_powers line 411
  40. lemma OAI.RecursivePotentials.FiniteRootedTree.sum_exitCut_le_root line 440
  41. lemma OAI.RecursivePotentials.FiniteRootedTree.root_le_sum_exitCut line 455
  42. lemma OAI.RecursivePotentials.VariableExponent.holder_powers_two line 471
  43. lemma OAI.RecursivePotentials.VariableExponent.rpow_sub_one_mul line 481
  44. def OAI.RecursivePotentials.VariableExponent.cutEnergy line 494
  45. lemma OAI.RecursivePotentials.VariableExponent.cutEnergy_nonneg line 497
  46. lemma OAI.RecursivePotentials.VariableExponent.cutEnergy_pow line 503
  47. lemma OAI.RecursivePotentials.VariableExponent.accumulated_cut_recursion line 509
  48. def OAI.RecursivePotentials.FiniteRootedTree.pField line 557
  49. lemma OAI.RecursivePotentials.FiniteRootedTree.pField_nonneg line 560
  50. lemma OAI.RecursivePotentials.FiniteRootedTree.pField_power_upper line 564
  51. lemma OAI.RecursivePotentials.FiniteRootedTree.exists_tight_label line 571
  52. def OAI.RecursivePotentials.FiniteRootedTree.tightLabel line 585
  53. lemma OAI.RecursivePotentials.FiniteRootedTree.tightLabel_spec line 587
  54. lemma OAI.RecursivePotentials.FiniteRootedTree.pField_power_sum_le_norm line 592
  55. def OAI.RecursivePotentials.VariableExponent.signed line 607
  56. lemma OAI.RecursivePotentials.VariableExponent.signed_true line 609
  57. lemma OAI.RecursivePotentials.VariableExponent.signed_false line 611
  58. def OAI.RecursivePotentials.VariableExponent.increment line 618
  59. def OAI.RecursivePotentials.VariableExponent.coefficient line 622
  60. lemma OAI.RecursivePotentials.VariableExponent.endpoint_on_head line 629
  61. lemma OAI.RecursivePotentials.VariableExponent.head_field_le line 634
  62. lemma OAI.RecursivePotentials.VariableExponent.increment_nonneg line 641
  63. lemma OAI.RecursivePotentials.VariableExponent.coefficient_nonneg line 648
  64. lemma OAI.RecursivePotentials.VariableExponent.common_increment line 655
  65. lemma OAI.RecursivePotentials.VariableExponent.prefix_child_increment line 667
  66. lemma OAI.RecursivePotentials.VariableExponent.layer_increment line 680
  67. lemma OAI.RecursivePotentials.VariableExponent.outside_field_eq line 708
  68. lemma OAI.RecursivePotentials.VariableExponent.exit_sign_mass line 715
  69. lemma OAI.RecursivePotentials.FiniteRootedTree.fields_cut_mass line 734
  70. lemma OAI.RecursivePotentials.FiniteRootedTree.fields_subcut_mass line 746
  71. lemma OAI.RecursivePotentials.FiniteRootedTree.pRootSum_tail_midpoint line 756
  72. lemma OAI.RecursivePotentials.VariableExponent.total_coefficient_mass line 782
  73. def OAI.RecursivePotentials.VariableExponent.tailFlux line 826
  74. lemma OAI.RecursivePotentials.VariableExponent.tailFlux_dominates line 831
  75. lemma OAI.RecursivePotentials.VariableExponent.tailFlux_local line 848
  76. lemma OAI.RecursivePotentials.VariableExponent.tailFlux_head_terminal line 866
  77. lemma OAI.RecursivePotentials.VariableExponent.tail_le_cutEnergy line 884
  78. lemma OAI.RecursivePotentials.VariableExponent.cutEnergy_zero_le_gap line 917
  79. theorem OAI.RecursivePotentials.VariableExponent.finite_cubic_normalized line 937
  80. lemma OAI.RecursivePotentials.VariableExponent.signed_smul line 965
  81. theorem OAI.RecursivePotentials.VariableExponent.finite_cubic line 969