OAI/Analysis/RecursivePotentials/Main.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RecursivePotentials.VariableTree.path_upper line 34
  2. lemma OAI.RecursivePotentials.VariableTree.path_fields line 45
  3. lemma OAI.RecursivePotentials.VariableTree.normSum_path line 54
  4. lemma OAI.RecursivePotentials.VariableTree.twice_coordinate_le_normSum line 58
  5. def OAI.RecursivePotentials.Variable.componentBasis line 78
  6. lemma OAI.RecursivePotentials.Variable.componentEquiv_basis line 81
  7. lemma OAI.RecursivePotentials.Variable.componentBasis_lower line 89
  8. lemma OAI.RecursivePotentials.Variable.componentBasis_weaklyNull line 96
  9. lemma OAI.RecursivePotentials.Variable.basis_weaklyNull line 109
  10. def OAI.RecursivePotentials.Variable.componentPath line 114
  11. lemma OAI.RecursivePotentials.Variable.componentPath_norm line 117
  12. lemma OAI.RecursivePotentials.Variable.componentPath_step line 122
  13. def OAI.RecursivePotentials.Variable.pathHeight line 132
  14. def OAI.RecursivePotentials.Variable.pathNode line 134
  15. def OAI.RecursivePotentials.Variable.pathVector line 137
  16. lemma OAI.RecursivePotentials.Variable.pathVector_norm line 140
  17. lemma OAI.RecursivePotentials.Variable.pathNode_child line 143
  18. def OAI.RecursivePotentials.Variable.children line 155
  19. lemma OAI.RecursivePotentials.Variable.pathVector_step line 164
  20. lemma OAI.RecursivePotentials.Variable.pathVector_increments line 172
  21. lemma OAI.RecursivePotentials.Variable.pathVector_increment_lower line 177
  22. lemma OAI.RecursivePotentials.Variable.not_finite_dimensional line 184
  23. theorem OAI.RecursivePotentials.Variable.one_sided_modulus_zero line 196
  24. theorem OAI.RecursivePotentials.Variable.no_equivalent_AUC line 205
  25. lemma OAI.RecursivePotentials.TreeSpace.eq_zero_of_coordinates_zero line 220
  26. lemma OAI.RecursivePotentials.TreeSpace.coordinates_ext line 250
  27. lemma OAI.RecursivePotentials.TreeSpace.projection_fixed_iff line 257
  28. lemma OAI.RecursivePotentials.TreeSpace.mem_tail_iff line 271
  29. lemma OAI.RecursivePotentials.TreeSpace.projection_finite_rank line 282
  30. lemma OAI.RecursivePotentials.ZeroTreeSpace.coordinate_coe line 296
  31. lemma OAI.RecursivePotentials.ZeroTreeSpace.P_coe line 302
  32. lemma OAI.RecursivePotentials.ZeroTreeSpace.Q_coe line 308
  33. lemma OAI.RecursivePotentials.ZeroTreeSpace.coordinates_ext line 314
  34. lemma OAI.RecursivePotentials.ZeroTreeSpace.projection_fixed_iff line 318
  35. lemma OAI.RecursivePotentials.ZeroTreeSpace.mem_tail_iff line 332
  36. lemma OAI.RecursivePotentials.ZeroTreeSpace.projection_finite_rank line 343
  37. theorem OAI.RecursivePotentials.XZero_cubic_of_support line 351
  38. lemma OAI.RecursivePotentials.rootSumCompletionStatement line 358
  39. lemma OAI.RecursivePotentials.zeroRootCompletionStatement line 372
  40. theorem OAI.RecursivePotentials.rec_completion line 387
  41. theorem OAI.RecursivePotentials.rec_main line 393
  42. theorem OAI.RecursivePotentials.stop_all_radii line 406
  43. lemma OAI.RecursivePotentials.Variable.component_recursion line 413
  44. lemma OAI.RecursivePotentials.Variable.norm_eq_nu line 424
  45. lemma OAI.RecursivePotentials.Variable.nu_comparisons line 428
  46. lemma OAI.RecursivePotentials.Variable.nu_eq_norm line 434
  47. lemma OAI.RecursivePotentials.Variable.sourceNormStatement line 438
  48. theorem OAI.RecursivePotentials.Variable.space line 454
  49. lemma OAI.RecursivePotentials.Variable.lpPotentials_recursion line 469
  50. lemma OAI.RecursivePotentials.Variable.recursion_unique line 479
  51. theorem OAI.RecursivePotentials.Variable.lp_model_exact line 520